Quelle  ProcedureSpecs.thy

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