(*  Title:       BDD
    Author:      Veronika Ortner and Norbert Schirmer, 2004
    Maintainer:  Norbert Schirmer,  norbert.schirmer at web de
    License:     LGPL
*)

(*  
ProcedureSpecs.thy

Copyright (C) 2004-2008 Veronika Ortner and Norbert Schirmer 
Some rights reserved, TU Muenchen

This library is free software; you can redistribute it and/or modify
it under the terms of the GNU Lesser General Public License as
published by the Free Software Foundation; either version 2.1 of the
License, or (at your option) any later version.

This library is distributed in the hope that it will be useful, but
WITHOUT ANY WARRANTY; without even the implied warranty of
MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU
Lesser General Public License for more details.

You should have received a copy of the GNU Lesser General Public
License along with this library; if not, write to the Free Software
Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA 02111-1307
USA
*)

section ‹Definitions of Procedures›
theory ProcedureSpecs
imports General Simpl.Vcg
begin

record "globals" =
  var_' :: "ref → nat"
  low_' :: "ref → ref"
  high_' :: "ref → ref"
  rep_' :: "ref → ref"
  mark_' :: "ref → bool"
  next_' ::"ref → ref"


record 'g bdd_state = "'g state" +
  varval_' :: "bool list"
  p_' :: "ref"
  R_' :: "bool"
  levellist_' :: "ref list"
  nodeslist_' :: "ref"
  node_':: "ref"
  m_' :: "bool"
  n_' :: "nat"


(*Evaluation even of unsymmetric dags. 
If a child is unexpectedly Null Eval returns False*)


procedures
  Eval (p, varval | R) = 
    "IF (🚫p→🚫var = 0) THEN 🚫R :==False
     ELSE IF (🚫p→🚫var = 1) THEN 🚫R :==True
       ELSE IF (🚫varval ! (🚫p→🚫var)) THEN CALL Eval (🚫p→🚫high, 🚫varval, 🚫R)
         ELSE CALL Eval (🚫p→🚫low, 🚫varval, 🚫R)
         FI
       FI
     FI"
  


procedures 
  Levellist (p, m, levellist | levellist) = 
    "IF (🚫p ≠ Null)
     THEN
       IF (🚫p → 🚫mark ≠ 🚫m)
       THEN
         🚫levellist :== CALL Levellist ( 🚫p → 🚫low, 🚫m, 🚫levellist );;
         🚫levellist :== CALL Levellist ( 🚫p → 🚫high, 🚫m, 🚫levellist );;
         🚫p → 🚫next :== 🚫levellist ! (🚫p→🚫var);;
         🚫levellist ! (🚫p→🚫var) :== 🚫p;;
         🚫p → 🚫mark :==🚫m
       FI
     FI"


procedures
  ShareRep (nodeslist, p) =
  "IF (isLeaf_pt 🚫p 🚫low 🚫high)
   THEN 🚫p → 🚫rep :== 🚫nodeslist
   ELSE
        WHILE (🚫nodeslist ≠ Null) DO
          IF (repNodes_eq 🚫nodeslist 🚫p 🚫low 🚫high 🚫rep)
          THEN 🚫p→🚫rep :== 🚫nodeslist;; 🚫nodeslist :== Null
          ELSE 🚫nodeslist :== 🚫nodeslist→🚫next
          FI
        OD
   FI"



procedures
  ShareReduceRepList (nodeslist | ) =
  "🚫node :== 🚫nodeslist;;
   WHILE (🚫node ≠ Null) DO
     IF (¬ isLeaf_pt 🚫node 🚫low 🚫high ∧
         🚫node → 🚫low → 🚫rep = 🚫node → 🚫high → 🚫rep )
     THEN 🚫node → 🚫rep :== 🚫node → 🚫low → 🚫rep
     ELSE CALL ShareRep (🚫nodeslist , 🚫node )
     FI;;
     🚫node :==🚫node → 🚫next
   OD"


procedures 
  Repoint (p|p) = 
  "IF ( 🚫p ≠ Null )
   THEN
     🚫p :== 🚫p → 🚫rep;;
     IF ( 🚫p ≠ Null )
     THEN 🚫p → 🚫low :== CALL Repoint (🚫p → 🚫low);;
          🚫p → 🚫high :== CALL Repoint (🚫p → 🚫high)
     FI
   FI"


procedures 
  Normalize (p|p) =
  "🚫levellist :==replicate (🚫p→🚫var +1) Null;;
    🚫levellist :== CALL Levellist (🚫p, (¬ 🚫p→🚫mark) , 🚫levellist);;
   (🚫n :==0;;
   WHILE (🚫n < length 🚫levellist) DO
     CALL ShareReduceRepList(🚫levellist ! 🚫n);;
     🚫n :==🚫n + 1
   OD);;
   🚫p :== CALL Repoint (🚫p)"

end