1 2(*****************************************************************************) 3(* DerivedBddRules.sml *) 4(* ------------------- *) 5(* *) 6(* Some BDD utilities and derived rules using MuDDy and PrimitiveBddRules *) 7(* (builds on some of Ken Larsen's code) *) 8(*****************************************************************************) 9(* *) 10(* Revision history (major events only): *) 11(* *) 12(* Mon Oct 8 10:27:40 BST 2001 -- created file *) 13(* Thu Nov 1 21:04:27 GMT 2001 -- updated for judgement assumptions *) 14(* Mon Nov 5 11:15:51 GMT 2001 -- updated documentation in comments *) 15(* Wed Nov 7 11:38:19 GMT 2001 -- changed to MachineTransitionTheory *) 16(* Tue Nov 27 15:42:00 GMT 2001 -- added findTrace and BddRhsOracle *) 17(* Thu Mar 28 09:40:05 GMT 2002 -- added signature file *) 18(* *) 19(*****************************************************************************) 20 21structure DerivedBddRules :> DerivedBddRules = struct 22 23(* 24load "pairLib"; 25load "PairRules"; 26load "numLib"; 27load "PrimitiveBddRules"; 28load "MachineTransitionTheory"; 29 30val _ = if not(bdd.isRunning()) then bdd.init 1000000 10000 else (); 31*) 32 33(* 34local 35*) 36 37open pairSyntax; 38open pairTools; 39open PairRules; 40open numLib; 41open PrimitiveBddRules; 42open bdd; 43open Varmap; 44open Thm; 45open PrimitiveBddRules; 46 47open HolKernel Parse boolLib; 48infixr 3 -->; 49infix ## |-> THEN THENL THENC ORELSE ORELSEC THEN_TCL ORELSE_TCL; 50 51fun hol_err msg func = 52 (print "DerivedBddRules: hol_err \""; print msg; 53 print "\" \""; print func; print "\"\n"; 54 raise mk_HOL_ERR "HolBdd" func msg); 55 56(*****************************************************************************) 57(* Ken Larsen writes: *) 58(* In the current mosml release List.foldl is tail recursive but *) 59(* List.foldr isn't. In the upcomming mosml release foldr might be tail *) 60(* recursive. But a tail recursive version of foldr is easy to uptain *) 61(* (as Michael notes): *) 62(*****************************************************************************) 63 64fun foldr f start ls = List.foldl f start (rev ls); 65 66(* 67in 68*) 69 70(*****************************************************************************) 71(* Test equality of BDD component of two term_bdds and return true or false *) 72(*****************************************************************************) 73 74fun BddEqualTest tb1 tb2 = bdd.equal (getBdd tb1) (getBdd tb2); 75 76(*****************************************************************************) 77(* Test if the BDD part is TRUE or FALSE *) 78(*****************************************************************************) 79 80fun isTRUE tb = bdd.equal (getBdd tb) bdd.TRUE 81and isFALSE tb = bdd.equal (getBdd tb) bdd.FALSE; 82 83(*****************************************************************************) 84(* Count number of states (code from Ken Larsen) *) 85(*****************************************************************************) 86 87fun statecount b = 88 let val sat = bdd.satcount b 89 val total = Real.fromInt(bdd.getVarnum()) 90 val sup = bdd.scanset(bdd.support b) 91 val numsup = Real.fromInt(Vector.length sup) 92 val free = total - numsup 93 in if bdd.equal b bdd.TRUE 94 then 0.0 95 else sat / Math.pow(2.0, free) 96 end; 97 98(*****************************************************************************) 99(* Destruct a term corresponding to a BuDDY BDD binary operation (bddop). *) 100(* Fail if not such a term. *) 101(*****************************************************************************) 102 103exception dest_BddOpError; 104 105fun dest_BddOp tm = 106 if is_neg tm 107 then 108 let val t = dest_neg tm 109 in 110 if is_conj t 111 then let val (t1,t2) = dest_conj t in (Nand, t1, t2) end else 112 if is_disj t 113 then let val (t1,t2) = dest_disj t in (Nor, t1, t2) end 114 else raise dest_BddOpError 115 end 116 else 117 case strip_comb tm of 118 (opr, [t1,t2]) => (case fst(dest_const opr) of 119 "/\\" => if is_neg t1 120 then (Lessth, dest_neg t1, t2) else 121 if is_neg t2 122 then (Diff, t1, dest_neg t2) 123 else (And, t1, t2) 124 | "\\/" => (Or, t1, t2) 125 | "==>" => (Imp, t1, t2) 126 | "=" => (Biimp, t1, t2) 127 | _ => raise dest_BddOpError) 128 | _ => raise dest_BddOpError; 129 130 131(*****************************************************************************) 132(* Function that always raises exception fail *) 133(* (useful as argument (leaffn) to GenTermToTermBdd) *) 134(*****************************************************************************) 135 136exception fail; 137 138fun failfn _ = raise fail; 139 140(*****************************************************************************) 141(* Scan a term and construct a term_bdd using the primitive operations *) 142(* when applicable, and a supplied function otherwise *) 143(*****************************************************************************) 144 145local 146fun fn3(f1,f2,f3)(x1,x2,x3) = (f1 x1, f2 x2, f3 x3) 147in 148fun GenTermToTermBdd leaffn vm tm = 149 let fun recfn tm = 150 if tm ~~ T 151 then BddCon true vm else 152 if tm ~~ F 153 then BddCon false vm else 154 if is_var tm 155 then BddVar true vm tm else 156 if is_neg tm 157 then let val tm' = dest_neg tm 158 in 159 if is_var tm' then BddVar false vm tm' else BddNot(recfn tm') 160 end else 161 if is_cond tm 162 then (BddIte o fn3(recfn,recfn,recfn) o dest_cond) tm else 163 if is_forall tm 164 then let val (vars,bdy) = strip_forall tm 165 in 166 (BddAppall vars o fn3(I,recfn,recfn) o dest_BddOp) bdy 167 handle dest_BddOpError => (BddForall vars o recfn) bdy 168 end else 169 if is_exists tm 170 then let val (vars,bdy) = strip_exists tm 171 in 172 (BddAppex vars o fn3(I,recfn,recfn) o dest_BddOp) bdy 173 handle dest_BddOpError => (BddExists vars o recfn) bdy 174 end 175 else ((BddOp o fn3(I,recfn,recfn) o dest_BddOp) tm 176 handle dest_BddOpError => leaffn tm) 177 in 178 recfn tm 179 end 180end; 181 182(*****************************************************************************) 183(* Extend a varmap with a list of variables *) 184(*****************************************************************************) 185 186fun extendVarmap [] vm = vm 187 | extendVarmap (v::vl) vm = 188 case Varmap.peek vm (name v) of 189 SOME _ => extendVarmap vl vm 190 | NONE => let val n = getVarnum() 191 val _ = bdd.setVarnum(n+1) 192 in 193 extendVarmap vl (Varmap.insert (name v, n) vm) 194 end; 195 196(*****************************************************************************) 197(* Convert a BDD to a nested conditional term with respect to a varmap *) 198(*****************************************************************************) 199 200exception bddToTermError; 201 202fun bddToTerm varmap = 203 let val pairs = Varmap.dest varmap 204 fun get_node_name n = 205 case assoc2 n pairs of 206 SOME(str,_) => str 207 | NONE => (print("Node "^(Int.toString n)^" has no name"); 208 raise bddToTermError) 209 fun bddToTerm_aux bdd = 210 if (bdd.equal bdd bdd.TRUE) 211 then T 212 else 213 if (bdd.equal bdd bdd.FALSE) 214 then F 215 else Psyntax.mk_cond(mk_var(get_node_name(bdd.var bdd),bool), 216 bddToTerm_aux(bdd.high bdd), 217 bddToTerm_aux(bdd.low bdd)) 218 in 219 bddToTerm_aux 220 end; 221 222(*****************************************************************************) 223(* ass vm tm |--> b *) 224(* ----------------------------------------------- *) 225(* [oracles: HolBdd] ass |- tm = ^(bddToTerm vm b) *) 226(*****************************************************************************) 227 228fun TermBddToEqThm tb = 229 let val (_,_,vm,tm,b) = dest_term_bdd tb 230 val tm' = bddToTerm vm b 231 val tb' = GenTermToTermBdd failfn vm tm' 232 in 233 BddThmOracle(BddOp(bdd.Biimp,tb,tb')) 234 end; 235 236(*****************************************************************************) 237(* Global assignable varmap *) 238(*****************************************************************************) 239 240val global_varmap = ref(Varmap.empty); 241 242fun showVarmap () = Varmap.dest(!global_varmap); 243 244(*****************************************************************************) 245(* Add variables to global_varmap and then call GenTermToTermBdd *) 246(* using the global function !termToTermBddFun on leaves *) 247(*****************************************************************************) 248 249exception termToTermBddError; 250 251val termToTermBddFun = 252 ref(fn (tm:term) => (raise termToTermBddError)); 253 254fun termToTermBdd tm = 255 let val vl = rev(all_vars tm) (* all_vars returns vars in reverse order *) 256 val vm = extendVarmap vl (!global_varmap) 257 val _ = global_varmap := vm 258 in 259 GenTermToTermBdd (!termToTermBddFun) vm tm 260 end; 261 262(*****************************************************************************) 263(* MkPrevThm (|- R((v1,...,vn),(v1',...,vn')) = ...) = *) 264(* *) 265(* |- Prev R (Eq (v1',...,vn'))) (v1,...,vn) = ... *) 266(*****************************************************************************) 267 268fun MkPrevThm Rth = 269 let val (Rcon, s_s') = Term.dest_comb(lhs(concl(SPEC_ALL Rth))) 270 val (s,s') = pairSyntax.dest_pair s_s' 271 val _ = print "\nProving simplified backward image theorem ...\n" 272 val PrevTh = 273 (simpLib.SIMP_RULE 274 boolSimps.bool_ss 275 [pairTheory.EXISTS_PROD,MachineTransitionTheory.Eq_def,pairTheory.PAIR_EQ,Rth]) 276 (ISPECL[Rcon,``Eq ^s'``,s]MachineTransitionTheory.Prev_def) 277 in 278 PrevTh 279 end; 280 281(*****************************************************************************) 282(* Flatten a varstruct term into a list of variables (also in StateEnum). *) 283(*****************************************************************************) 284 285fun flatten_pair t = 286if is_pair t 287 then List.foldr (fn(t,l) => (flatten_pair t) @ l) [] (strip_pair t) 288 else [t]; 289 290(*****************************************************************************) 291(* MkIterThms ReachBy_rec``R((v1,...,vn),(v1',...,vn'))`` ``B(v1,...,vn)`` = *) 292(* ([|- ReachBy R B 0 (v1,...,vn) = B(v1,...,vn), *) 293(* |- !n. ReachBy R B (SUC n) (v1,...,vn) = *) 294(* ReachBy R B n (v1,...,vn) *) 295(* \/ *) 296(* ?v1'...vn'. ReachBy R B n (v1',...,vn') *) 297(* /\ *) 298(* R ((v1',...,vn'),(v1,...,vn))] *) 299(* *) 300(* *) 301(* MkIterThms ReachIn_rec``R((v1,...,vn),(v1',...,vn'))`` ``B(v1,...,vn)`` = *) 302(* ([|- ReachIn R B 0 (v1,...,vn) = B(v1,...,vn), *) 303(* |- !n. ReachIn R B (SUC n) (v1,...,vn) = *) 304(* ?v1'...vn'. ReachIn R B n (v1',...,vn') *) 305(* /\ *) 306(* R ((v1',...,vn'),(v1,...,vn))] *) 307(*****************************************************************************) 308 309fun MkIterThms reachth Rtm Btm = 310 let val (R,st_st') = dest_comb Rtm 311 val (st,st') = dest_pair st_st' 312 val (B,st0) = dest_comb Btm 313 val _ = Term.aconv st st0 314 orelse hol_err "R and B vars not consistent" "MkReachByIterThms" 315 val ty = type_of st 316 val th = INST_TYPE[(``:'a`` |-> ty),(``:'b`` |-> ty)]reachth 317 val (th1,th2) = (CONJUNCT1 th, CONJUNCT2 th) 318 val ntm = mk_var("n",num) 319 val th3 = SPECL[R,B,st]th1 320 val th4 = CONV_RULE 321 (RHS_CONV 322 (ONCE_DEPTH_CONV 323 (Ho_Rewrite.REWRITE_CONV[pairTheory.EXISTS_PROD] 324 THENC RENAME_VARS_CONV 325 (List.map (fst o dest_var) (flatten_pair st'))))) 326 (SPECL[R,B,ntm,st]th2) 327 328 in 329 (th3, GEN ntm th4) 330 end; 331 332(*****************************************************************************) 333(* Perform disjunctive partitioning *) 334(* The simplification assumes R is of the form: *) 335(* *) 336(* R((x,y,z),(x',y',z'))= *) 337(* ((x' = E1(x,y,z)) /\ (y' = y) /\ (z' = z)) *) 338(* \/ *) 339(* ((x' = x) /\ (y' = E2(x,y,z)) /\ (z' = z)) *) 340(* \/ *) 341(* ((x' = x) /\ (y' = y) /\ (z' = E3(x,y,z))) *) 342(* *) 343(* Then, for example, the equation: *) 344(* *) 345(* ReachBy R B (SUC n) (x,y,z) = *) 346(* ReachBy R B n (x,y,z) *) 347(* \/ *) 348(* (?x_ y_ z_. ReachBy n R B (x_,y_,z_) /\ R((x_,y_,z_),(x,y,z)))) *) 349(* *) 350(* is simplified to: *) 351(* *) 352(* ReachBy R B (SUC n) (x,y,z) = *) 353(* ReachBy R B n (x,y,z) *) 354(* \/ *) 355(* (?x_. ReachBy R B n (x_,y,z) /\ (x = E1(x_,y,z)) *) 356(* \/ *) 357(* (?y_. ReachBy R B n (x,y_,z) /\ (y = E2(x,y_,z)) *) 358(* \/ *) 359(* (?z_. ReachBy R B n (x,y,z_) /\ (z = E3(x,y,z_)) *) 360(* *) 361(* This avoids having to build the BDD of R((x,y,z),(x',y',z')) *) 362(*****************************************************************************) 363 364val MakeSimpRecThm = 365 time 366 (simpLib.SIMP_RULE boolSimps.bool_ss [LEFT_AND_OVER_OR,EXISTS_OR_THM]); 367 368(*****************************************************************************) 369(* ASSUME for term_bdd *) 370(*****************************************************************************) 371 372fun BddAssume tm = 373 BddEqMp ((SYM o EQT_INTRO o ASSUME) tm) (BddCon true Varmap.empty) 374 375(*****************************************************************************) 376(* Convert a theorem to a term_bdd *) 377(*****************************************************************************) 378 379fun thmToTermBdd th = 380 BddEqMp ((SYM o EQT_INTRO) th) (BddCon true Varmap.empty) 381 382(*****************************************************************************) 383(* asl |- t1 = t2 ass vm t1' |--> b *) 384(* ---------------------------------- *) 385(* (asl U ass) vm t2' |--> b' *) 386(* *) 387(* where t1 can be instantiated to t1' and t2' is the corresponding *) 388(* instance of t2 *) 389(*****************************************************************************) 390 391fun BddApThm th tb = 392 let val (_,_,vm,t1',b) = dest_term_bdd tb 393 in 394 BddEqMp (REWR_CONV th t1') tb 395 handle HOL_ERR _ => hol_err "REWR_CONV failed" "BddApthm" 396 end; 397 398(*****************************************************************************) 399(* BddApRestrict : term_bdd -> term -> term_bdd *) 400(* *) 401(* ass vm t |--> b *) 402(* ----------------- *) 403(* ass vm tm |--> b' *) 404(* *) 405(* Generates the BDD of a supplied term if it can be obtained by restricting *) 406(* a given term_bdd *) 407(*****************************************************************************) 408 409exception BddApRestrictError; 410 411fun BddApRestrict tb tm = 412 let val (_,_,vm,t,_) = dest_term_bdd tb 413 val (sub_tm,sub_ty) = match_term t tm 414 val _ = if null sub_ty 415 then () 416 else (print "match produced a non-empty type instasntiation\n"; 417 raise BddApRestrictError) 418 val sub_tb = List.map 419 (fn {redex = v, residue = c} => 420 (BddVar true vm v, 421 if c ~~ T then BddCon true vm else 422 if c ~~ F then BddCon false vm 423 else (print_term c; 424 print " not a boolean constant\n"; 425 raise BddApRestrictError))) 426 sub_tm 427 in 428 BddRestrict sub_tb tb 429 end; 430 431(*****************************************************************************) 432(* ass vm t |--> b *) 433(* ---------------- *) 434(* ass vm tm |--> b' *) 435(* *) 436(* where boolean variables in t can be renamed to get tm and b' is *) 437(* the corresponding replacement of BDD variables in b *) 438(*****************************************************************************) 439 440exception BddApReplaceError; 441 442fun BddApReplace tb tm = 443 let val (_,_,vm,t,b) = dest_term_bdd tb 444 val (tml,tyl) = match_term t tm 445 val _ = if null tyl then () else raise BddApReplaceError 446 val tbl = (List.map 447 (fn{redex=old,residue=new}=> 448 (BddVar true vm old, BddVar true vm new)) 449 tml 450 handle BddVarError => raise BddApReplaceError) 451 in 452 BddReplace tbl tb 453 end; 454 455(* 456** BddSubst defined below applies a substitution 457** 458** [(oldtb1,newtb1),...,(oldtni,newtbi)] 459** 460** to a term_bdd, where oldtbp (1 <= p <= i) must be of the form 461** 462** vm vp |--> bp 463** 464** where vp is a variable, and v1,...,vp,...,vi are all distinct. 465** 466** The preliminary version below separates the substitution 467** into a restriction (variables mapped to T or F) followed 468** by a variable renaming (replacement). 469** 470** A more elaborate scheme will be implemented after 471** BuDDy's bdd_veccompose is available in MuDDy. 472*) 473 474(*****************************************************************************) 475(* Split a substitution *) 476(* *) 477(* [(oldtb1,newtb1),...,(oldtni,newtbi)] *) 478(* *) 479(* into a restriction and variable renaming, *) 480(* failing if this isn't possible *) 481(*****************************************************************************) 482 483val split_subst = 484 List.partition 485 (fn (tb,tb')=> 486 let val tm' = getTerm tb' 487 in 488 (tm' ~~ T) orelse (tm' ~~ F) 489 end); 490 491(*****************************************************************************) 492(* [(ass1 vm v1 |--> b1 , ass1' vm tm1 |--> b1'), *) 493(* . *) 494(* . *) 495(* . *) 496(* (assi vm vi |--> bi , assi' vm tmi |--> bi')] *) 497(* ass vm tm |--> b *) 498(* ------------------------------------------------------------------------ *) 499(* (as1 U ass1' U ... U assi U assi' U ass) *) 500(* vm *) 501(* (subst[v1 |-> tm1, ... , vi |-> tmi]tm) *) 502(* |--> *) 503(* <appropriate BDD> *) 504(*****************************************************************************) 505 506fun BddSubst tbl tb = 507 let val (res,rep) = split_subst tbl 508 in 509 BddReplace rep (BddRestrict res tb) 510 end; 511 512(*****************************************************************************) 513(* ass vm t |--> b *) 514(* ----------------- *) 515(* ass vm tm |--> b' *) 516(* *) 517(* where boolean variables in t can be instantiated to get tm and b' is *) 518(* the corresponding replacement of BDD variables in b *) 519(*****************************************************************************) 520 521exception BddApSubstError; 522 523fun BddApSubst tb tm = 524 let val (_,_,vm,t,b) = dest_term_bdd tb 525 val (tml,tyl) = match_term t tm 526 val _ = if null tyl then () else (print "type match problem\n"; 527 raise BddApSubstError) 528 val tbl = (List.map 529 (fn{redex=old,residue=new}=> 530 (BddVar true vm old, 531 GenTermToTermBdd (!termToTermBddFun) vm new)) 532 tml 533 handle BddVarError => raise BddApSubstError) 534 in 535 BddSubst tbl tb 536 end; 537 538(* Test examples ================================================================== 539 540val tb1 = termToTermBdd ``x /\ y /\ z``; 541 542val tbx = termToTermBdd ``x:bool`` 543and tby = termToTermBdd ``y:bool`` 544and tbz = termToTermBdd ``z:bool`` 545and tbp = termToTermBdd ``p:bool`` 546and tbq = termToTermBdd ``q:bool`` 547and tbT = termToTermBdd T 548and tbF = termToTermBdd F; 549 550(* Repeat to sync all the varmaps! *) 551 552val tbl = [(tbx,tbp),(tby,tbq),(tbz,tbF)]; 553val tb2 = BddSubst tbl tb1; 554 555val tb3 = BddApSubst tb1 ``p /\ T /\ q``; 556======================================================= End of test examples *) 557 558(*****************************************************************************) 559(* asl |- t1 = t2 *) 560(* ------------------------------ *) 561(* (addList ass []) vm t1 |--> b *) 562(* *) 563(* Fails if t2 is not built from variables using bddops *) 564(*****************************************************************************) 565 566fun eqToTermBdd leaffn vm th = 567 let val th' = SPEC_ALL th 568 val tm = rhs(concl th') 569 in 570 BddEqMp (SYM th') (GenTermToTermBdd leaffn vm tm) 571 end; 572 573(*****************************************************************************) 574(* Convert an ml positive integer to a HOL numeral *) 575(*****************************************************************************) 576 577fun intToTerm n = numSyntax.mk_numeral(Arbnum.fromInt n); 578 579(*****************************************************************************) 580(* ass vm tm |--> b conv tm = asl |- tm = tm' *) 581(* ---------------------------------------------- *) 582(* (addList ass asl) vm tm' |--> b *) 583(*****************************************************************************) 584 585fun BddApConv conv tb = BddEqMp (conv(getTerm tb)) tb; 586 587(*****************************************************************************) 588(* |- t1 = t2 *) 589(* ---------- *) 590(* |- t1 *) 591(* *) 592(* if the BDD of t2 (using GenTermToTermBdd) is TRUE *) 593(*****************************************************************************) 594 595fun BddRhsOracle leaffn vm eqth = 596 let val (t1,t2) = dest_eq(concl(SPEC_ALL eqth)) 597 in 598 EQ_MP (SYM eqth) (BddThmOracle(GenTermToTermBdd leaffn vm t2)) 599 end; 600 601(*****************************************************************************) 602(* Iterate a function *) 603(* *) 604(* f : int -> 'a -> 'a *) 605(* *) 606(* from an initial value, applying it successively to 0,1,2,... until *) 607(* *) 608(* p : 'a -> bool *) 609(* *) 610(* is true (at least one iteration is always performed) *) 611(* *) 612(*****************************************************************************) 613 614fun iterate p f = 615 let fun iter n x = 616 let val x' = f n x 617 in 618 if p x' then x' else iter (n+1) x' 619 end 620 in 621 iter 0 622 end; 623 624(*****************************************************************************) 625(* |- f 0 s = ... s ... |- !n. f (SUC n) s = ... f n ... s ... *) 626(* --------------------------------------------------------------- *) 627(* (vm ``f i s`` |--> bi, vm ``f (SUC i) s`` |--> bsuci) *) 628(* *) 629(* where i is the first number such that |- f (SUC i) s = f i s *) 630(* and the function *) 631(* *) 632(* report : int -> term_bdd -> 'a *) 633(* *) 634(* is applied to the iteration level and current term_bdd and can be used *) 635(* for tracing. *) 636(* *) 637(* A state of the iteration is a pair (tb,tb') consisting of the *) 638(* previous term_bdd tb and the current one tb'. The initial state *) 639(* is (somewhat arbitarily) taken to be (tb0,tb0). *) 640(*****************************************************************************) 641 642exception computeFixedpointError; 643 644fun computeFixedpoint report vm (th0,thsuc) = 645 let val tb0 = eqToTermBdd (fn tm => raise computeFixedpointError) vm th0 646 fun f n (tb,tb') = 647 let val tb'simp = BddApConv reduceLib.REDUCE_CONV tb' 648 val _ = report n tb'simp 649 val tb'' = 650 eqToTermBdd (BddApSubst tb'simp) vm (SPEC (intToTerm n) thsuc) 651 in 652 (tb'simp,tb'') 653 end 654 in 655 iterate (uncurry BddEqualTest) f (tb0,tb0) 656 end; 657 658(*****************************************************************************) 659(* ass vm tm |--> b *) 660(* ---------------------------------------------- *) 661(* [((ass1 vm v1 |--> b1),(ass1' vm c1 |--> b1')), *) 662(* . *) 663(* . *) 664(* . *) 665(* ((assi vm vi |--> bi),(assi' vm ci |--> bi')] *) 666(* *) 667(* with the property that *) 668(* *) 669(* BddRestrict [((ass1 vm v1 |--> b1),(ass1' vm c1 |--> b1')), *) 670(* . *) 671(* . *) 672(* . , *) 673(* ((assi vm vi |--> bi),(assi' vm ci |--> bi'))] *) 674(* (ass vm tm |--> b) *) 675(* = *) 676(* (ass1 U ass1' U ... U assi U assi' U ass) *) 677(* vm *) 678(* (subst[v1|->ci,...,vi|->ci]tm) *) 679(* |--> *) 680(* TRUE *) 681(*****************************************************************************) 682 683exception BddSatoneError; 684 685fun BddSatone tb = 686 let val (_,_,vm,tm,b) = dest_term_bdd tb 687 val assl = bdd.getAssignment(bdd.satone b) 688 val vml = Varmap.dest vm 689 in 690 List.map 691 (fn (n,tv) => ((case assoc2 n vml of 692 SOME(s,_) => BddVar true vm (mk_var(s,bool)) 693 | NONE => (print "this should not happen!\n"; 694 raise BddSatoneError)), 695 BddCon tv vm)) 696 assl 697 end; 698 699(*****************************************************************************) 700(* *) 701(* |- p s = ... s ... *) 702(* |- f 0 s = ... s ... *) 703(* |- f (SUC n) s = ... f n ... s ... *) 704(* --------------------------------------------------------- *) 705(* [{} vm ``f i s`` |--> bi, ... , {} vm ``f 0 s`` |--> b0] *) 706(* *) 707(* where i is the first number such that |- f i s ==> p s *) 708(*****************************************************************************) 709 710exception computeTraceError; 711 712fun computeTrace report vm pth (th0,thsuc) = 713 let val ptb = eqToTermBdd (fn tm => raise computeFixedpointError) vm pth 714 val tb0 = eqToTermBdd (fn tm => raise computeFixedpointError) vm th0 715 fun p tbl = not(isFALSE(BddOp(bdd.And, hd tbl, ptb))) 716 fun f n tbl = 717 (report n (hd tbl); 718 let val tb = 719 BddApConv 720 reduceLib.REDUCE_CONV 721 (eqToTermBdd (BddApSubst(hd tbl)) vm (SPEC (intToTerm n) thsuc)) 722 in 723 tb :: tbl 724 end) 725 in 726 if p[tb0] then [tb0] else iterate p f [tb0] 727 end; 728 729 730(* Test example (Solitaire) 731 732val vm = solitaire_varmap; 733 734val pth = SolitaireFinish_def; 735 736val (th0,thsuc) = (in_th0,in_thsuc); 737 738val trl = computeTrace report vm pth (th0,thsuc); 739 740*) 741 742(*****************************************************************************) 743(* Given a list *) 744(* *) 745(* [((vm v1 |--> bj1),(vm c1 |--> b1')), *) 746(* . *) 747(* . *) 748(* . , *) 749(* ((vm vn |--> bn),(vm cn |--> bn'))]) *) 750(* *) 751(* in which not every vi is mapped to a constant, extend it *) 752(* by mapping any unspecified variables to F. Used *) 753(* to complete an assignment to generated by BddSatone *) 754(* *) 755(* *) 756(*****************************************************************************) 757 758fun extendSat varlist vm tbl = 759 List.map 760 (fn v => case List.find (fn (tb,tb') => getTerm tb ~~ v) tbl of 761 SOME tb_tb' => tb_tb' 762 | NONE => (BddVar true vm v, BddCon true vm)) 763 varlist; 764 765(*****************************************************************************) 766(* traceBack *) 767(* vm *) 768(* [{} vm ``f i s`` |--> bi, ... , {} vm ``f 0 s`` |--> b0] *) 769(* (|- p s = ... s ...) *) 770(* (|- R((v1,...,vn),(v1',...,vn')) = ...) *) 771(* *) 772(* computes a list of pairs of the form (with j = 0,1,...,i-1) *) 773(* *) 774(* ((vm ``ReachIn R B j s_vec /\ Prev R (Eq c_vec) s_vec`` |--> bdd), *) 775(* [((vm v1 |--> bj1),(vm cj1 |--> bj1')), *) 776(* . *) 777(* . *) 778(* . , *) 779(* ((vm vn |--> bjn),(vm cjn |--> bjn'))]) *) 780(* *) 781(* where s_vec = (v1,...,vn) and c_vec = (c(j+1)1,...,c(i+1)n) *) 782(* *) 783(* where ci is T or F and the second element specifies a state satisfying *) 784(* the first element and in which state variable vj has value cj *) 785(* (where 0 <= j <= n). *) 786(* *) 787(* The last element of the list has the form *) 788(* (({} vm ``ReachIn R B j s_vec /\ p(v1,...,vn)`` |--> bdd), *) 789(* [(({} vm v1 |--> bi1),{} vm ci1 |--> bi1')), *) 790(* . *) 791(* . *) 792(* . , *) 793(* (({} vm vn |--> bin),({} vm cin |--> bin'))]) *) 794(* *) 795(* If [s0,...,si] is the sequence of states, then *) 796(* R(s0,s1), R(s1,s2),...,R(s(i-1),si) and for j such that 1 <= j <= i *) 797(* sj satisfies bj and p si *) 798(*****************************************************************************) 799 800val traceBackPrevThm = ref TRUTH; 801 802fun traceBack vm trl pth Rth = 803 let val svars = strip_pair(Term.rand(lhs(concl(SPEC_ALL pth)))) 804 val PrevTh = MkPrevThm Rth 805 val _ = (traceBackPrevThm := PrevTh) 806 val vl = filter (fn v => type_of v = bool) (all_vars(concl PrevTh)) @ svars 807 val prime_var = mk_var o (prime ## I) o dest_var 808 val vm' = extendVarmap (vl @ List.map prime_var vl) vm 809 val trl' = map (BddExtendVarmap vm') trl 810 val ptb = eqToTermBdd (fn tm => raise computeFixedpointError) vm' pth 811 val PrevThTb = eqToTermBdd failfn vm' PrevTh 812 val lasttb = BddOp(And, hd trl', ptb) 813 val prime_ass = List.map (fn (tb,tb') => (BddVar true vm' (prime_var(getTerm tb)), tb')) 814 fun satfn tb = extendSat svars vm' (BddSatone tb) 815 fun stepback(tb, ass) = 816 let val tb' = BddOp(And, tb, BddRestrict (prime_ass ass) PrevThTb) 817 in 818 (tb', satfn tb') 819 end 820 val _ = print "Computing trace: " 821 val assl = 822 List.foldl 823 (fn (tb,assl) => (print "."; stepback(tb, snd(hd assl)) :: assl)) 824 [(lasttb, satfn lasttb)] 825 (tl trl') 826 val _ = print " done.\n" 827in 828 assl 829end; 830 831(*****************************************************************************) 832(* findTrace *) 833(* (|- R((v1,...,vn),(v1',...,vn')) = ...) *) 834(* (|- P(v1,...,vn) = ...) *) 835(* (|- Q(v1,...,vn) = ...) *) 836(* = *) 837(* ((|- P s_0), [(|- R(s_0,s_1)),...,(|- R(s_(n-1),s_n))], (|- Q s_n)) *) 838(*****************************************************************************) 839 840fun findTrace vm Rth Pth Qth = 841 let val (in_th0,in_thsuc) = 842 (REWRITE_RULE[Pth,pairTheory.PAIR_EQ] ## REWRITE_RULE[Rth]) 843 (MkIterThms 844 MachineTransitionTheory.ReachIn_rec 845 (lhs(concl(SPEC_ALL Rth))) 846 (lhs(concl(SPEC_ALL Pth)))) 847 val (Rcon, s_s') = Term.dest_comb(lhs(concl(SPEC_ALL Rth))) 848 val (s,s') = pairSyntax.dest_pair s_s' 849 val tr = computeTrace (fn n=>fn tb=>print".") vm Qth (in_th0,in_thsuc) 850 val soln = traceBack vm tr Qth Rth 851 val cl = 852 List.map 853 (fn(_,tbl)=> list_mk_pair(List.map (fn(_,tb)=> getTerm tb) tbl)) 854 soln 855 val initth = BddRhsOracle 856 failfn 857 vm 858 (SPECL (strip_pair(hd cl)) (GENL(strip_pair s)(SPEC_ALL Pth))) 859 val transthl = 860 map 861 (fn (t,t') => 862 BddRhsOracle 863 failfn 864 vm 865 (SPECL 866 (strip_pair t @ strip_pair t') 867 (GENL(strip_pair s @ strip_pair s')(SPEC_ALL Rth)))) 868 (zip (List.take(cl, length cl - 1)) (tl cl)) 869 val finalth = BddRhsOracle failfn 870 vm 871 (SPECL (strip_pair(last cl)) 872 (GENL(strip_pair s)(SPEC_ALL Qth))) 873 in 874 (initth, transthl, finalth) 875 end; 876 877 878(*****************************************************************************) 879(* If t is satifiable (i.e. b is not FALSE) *) 880(* *) 881(* a vm t |--> b *) 882(* -------------------------- *) 883(* a U {v1=c1,...,vn=cn} |- t *) 884(* *) 885(* Similar to BddFindModel followed by BddThmOracle, but checks the *) 886(* assignment found by satone using CBV_CONV, so is pure *) 887(* (i.e. result not tagged with HolBdd) *) 888(* *) 889(*****************************************************************************) 890 891exception findModelError; 892 893local 894open computeLib 895val compset = bool_compset() 896in 897fun findModel tb = 898 let val (_,ass,vm,t,b) = dest_term_bdd tb 899 val assl = bdd.getAssignment(bdd.satone b) 900 val vml = Varmap.dest vm 901 val setl = List.map 902 (fn (n,tv) => 903 ((case assoc2 n vml of 904 SOME(s,_) => mk_var(s,bool) 905 | NONE => (print "This should not happen!\n"; 906 raise findModelError)), 907 if tv then T else F)) 908 assl 909 in 910 EQT_ELIM 911 (RIGHT_CONV_RULE 912 (CBV_CONV compset) 913 (SUBST_CONV (List.map (fn(l,r) => (l |-> ASSUME(mk_eq(l,r)))) setl) t t)) 914 end 915end; 916 917(* 918end; 919*) 920 921end 922