Theory ProcedureSpecs

(*  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