1 2(*****************************************************************************) 3(* PrimitiveBddRules.sml *) 4(* --------------------- *) 5(* *) 6(* Types and rules implementing primitive axioms and rules *) 7(* of inference system for BDD representation judgements. *) 8(* *) 9(*****************************************************************************) 10(* *) 11(* BddThmOracle *) 12(* BddExtendVarmap *) 13(* BddSupportContractVarmap *) 14(* BddFreevarsContractVarmap *) 15(* BddEqMp *) 16(* BddReplace *) 17(* BddCompose *) 18(* BddListCompose *) 19(* BddRestrict *) 20(* BddCon *) 21(* BddVar *) 22(* BddNot *) 23(* BddOp *) 24(* BddIte *) 25(* BddForall *) 26(* BddExists *) 27(* BddAppall *) 28(* BddAppex *) 29(* BddSimplify *) 30(* BddFindModel *) 31(* *) 32(*****************************************************************************) 33(* *) 34(* Revision history: *) 35(* *) 36(* Tue Oct 2 15:03:11 BST 2001 -- created file *) 37(* Fri Oct 5 17:23:09 BST 2001 -- revised file *) 38(* Thu Nov 1 14:18:41 GMT 2001 -- added assumptions to term_bdd values *) 39(* Mon Mar 11 11:01:53 GMT 2002 -- added BddFindModel *) 40(* Thu Mar 28 09:40:05 GMT 2002 -- added signature file *) 41(* *) 42(*****************************************************************************) 43 44structure PrimitiveBddRules :> PrimitiveBddRules = struct 45 46(* 47load "bdd"; 48load "pairLib"; 49load "PairRules"; 50load "numLib"; 51load "Binarymap"; 52load "Varmap"; 53 54val _ = if not(bdd.isRunning()) then bdd.init 1000000 10000 else (); 55*) 56 57local 58 59open pairSyntax; 60open pairTools; 61open PairRules; 62open numLib; 63open Binarymap; 64open Varmap; 65open bdd; 66 67open HolKernel Parse boolLib BasicProvers Tag Feedback 68 69infixr 3 -->; 70infix ## |-> THEN THENL THENC ORELSE ORELSEC THEN_TCL ORELSE_TCL; 71 72(*****************************************************************************) 73(* Ken Larsen writes: *) 74(* In the current mosml release List.foldl is tail recursive but *) 75(* List.foldr isn't. In the upcomming mosml release foldr might be tail *) 76(* recursive. But a tail recursive version of foldr is easy to uptain *) 77(* (as Michael notes): *) 78(*****************************************************************************) 79 80fun foldr f start ls = List.foldl f start (rev ls); 81 82(*****************************************************************************) 83(* To enable HolBdd to track tags. HolBddTag:TermBdd :: empty_tag:THM *) 84(*****************************************************************************) 85 86val HolBddTag_string = "HolBdd" 87val HolBddTag = Tag.read HolBddTag_string 88 89(*****************************************************************************) 90(* Setup trace variable for controlling debug output *) 91(*****************************************************************************) 92 93val trace_level = ref 0 94 95val _ = register_trace("HolBdd",trace_level,5) 96 97in 98 99(*****************************************************************************) 100(* The constructor TermBdd is like mk_thm and is only used *) 101(* to create primitive term_bdd values. *) 102(* *) 103(* TermBdd should not be exported from this module. *) 104(*****************************************************************************) 105 106(* 107local 108*) 109 110type assums = term HOLset.set; 111type varmap = Varmap.varmap; 112datatype term_bdd = TermBdd of tag * assums * varmap * term * bdd.bdd; 113 114(* 115in 116*) 117 118(*****************************************************************************) 119(* Destructors for term_bdd *) 120(*****************************************************************************) 121 122fun dest_term_bdd(TermBdd(tg,ass,vm,tm,b)) = (tg,ass,vm,tm,b); 123 124fun getTag(TermBdd(tg,ass,vm,tm,b)) = tg 125and getAssums(TermBdd(tg,ass,vm,tm,b)) = ass 126and getVarmap(TermBdd(tg,ass,vm,tm,b)) = vm 127and getTerm(TermBdd(tg,ass,vm,tm,b)) = tm 128and getBdd(TermBdd(tg,ass,vm,tm,b)) = b; 129 130(*****************************************************************************) 131(* Name of a boolean variable (raises nameError on non boolean variables) *) 132(*****************************************************************************) 133 134exception nameError; 135 136fun name v = 137 if is_var v andalso type_of v = bool 138 then fst(dest_var v) 139 else (print_term v; print " is not a boolean variable\n"; raise nameError); 140 141(*****************************************************************************) 142(* Oracle function *) 143(* *) 144(* ass vm t |--> TRUE *) 145(* ------------------ *) 146(* ass |- t *) 147(*****************************************************************************) 148 149exception BddThmOracleError; 150 151fun BddThmOracle(TermBdd(tg,ass,_,tm,bdd)) = 152 if bdd.equal bdd bdd.TRUE 153 then add_tag(tg, mk_oracle_thm HolBddTag_string (HOLset.listItems ass, tm)) 154 else raise BddThmOracleError; 155 156(*****************************************************************************) 157(* Varmap.extends vm1 vm2 ass vm1 tm |--> b *) 158(* ------------------------------------------ *) 159(* ass vm2 tm |--> b *) 160(*****************************************************************************) 161 162exception BddExtendVarmapError; 163 164fun BddExtendVarmap vm2 (TermBdd(tg,ass,vm1,tm,b)) = 165 if Varmap.extends vm1 vm2 166 then TermBdd(tg,ass,vm2,tm,b) 167 else raise BddExtendVarmapError; 168 169(*****************************************************************************) 170(* ass vm tm |--> b not(mem (name v) (free_vars tm)) *) 171(* --------------------------------------------------- *) 172(* ass Varmap.remove(name v)vm |--> b *) 173(* *) 174(* Raises BddFreevarsContractVarmapError if v is free in tm, *) 175(* and is the identity otherwise *) 176(*****************************************************************************) 177 178exception BddFreevarsContractVarmapError; 179 180fun BddFreevarsContractVarmap v (TermBdd(tg,ass,vm,tm,b)) = 181 if mem v (free_vars tm) 182 then (print_term v; print " not in free_vars of\n"; print_term tm; print "\n"; 183 raise BddFreevarsContractVarmapError) 184 else TermBdd(tg,ass,Varmap.remove (name v) vm, tm, b); 185 186(*****************************************************************************) 187(* Test if a BDD variable is in the support of a bdd *) 188(*****************************************************************************) 189 190fun inSupport n b = 191 Vector.foldl 192 (fn (m,bv) => (m=n) orelse bv) 193 false 194 (bdd.scanset(bdd.support b)); 195 196(*****************************************************************************) 197(* ass vm tm |--> b Varmap.peek vm (name v) = SOME n not(inSupport n b) *) 198(* ------------------------------------------------------------------------ *) 199(* ass (Varmap.remove(name v)vm) tm |--> b *) 200(* *) 201(* Raises BddSupportContractVarmapError if vm maps v to a BDD variable in b, *) 202(* and is the idenetity of v is not mapped to anything by vm *) 203(* *) 204(*****************************************************************************) 205 206exception BddSupportContractVarmapError; 207 208fun BddSupportContractVarmap v (tb as (TermBdd(tg,ass,vm,tm,b))) = 209 let val s = name v 210 in 211 case Varmap.peek vm s of 212 SOME n => if inSupport n b 213 then raise BddSupportContractVarmapError 214 else TermBdd(tg,ass,Varmap.remove s vm, tm, b) 215 | NONE => tb 216 end; 217 218(*****************************************************************************) 219(* asl |- t1 = t2 ass vm t1 |--> b *) 220(* --------------------------------- *) 221(* (addList ass asl) vm t2 |--> b *) 222(*****************************************************************************) 223 224exception BddEqMpError; 225 226fun BddEqMp th (TermBdd(tg,ass,vm,t1,b)) = 227 let val (asl,c) = dest_thm th 228 val (l,r) = dest_eq c 229 in 230 if aconv l t1 231 then TermBdd(Tag.merge tg (Thm.tag th),HOLset.addList(ass,asl),vm,r,b) 232 else if (!trace_level)>=1 then 233 let val _ = print "BddEqMp Error\n" 234 val _ = print "Theorem:\n" 235 val _ = print_thm th 236 val _ = print "\n" 237 val _ = print "Term:\n" 238 val _ = print_term t1 239 val _ = print "\n" 240 in raise BddEqMpError end 241 else raise BddEqMpError 242 end; 243 244(*****************************************************************************) 245(* [(ass1 vm v1 |--> b1 , ass1' vm v1' |--> b1'), *) 246(* . *) 247(* . *) 248(* . *) 249(* (assi vm vi |--> bi , assi' vm vi' |--> bi')] *) 250(* ass vm tm |--> b *) 251(* ------------------------------------------------------------------------ *) 252(* (ass1 U ass1' ... assi U assi' U ass) *) 253(* vm *) 254(* (subst[v1 |-> v1', ... , vi |-> vi']tm) *) 255(* |--> *) 256(* replace b (makepairSet[(var b1, var b1'), ... , (var bi, var bi')]) *) 257(*****************************************************************************) 258 259exception BddReplaceError; 260 261fun BddReplace tbl (TermBdd(tg,ass,vm,tm,b)) = 262 let val (tg',ass_union,(l,l'),replacel) = 263 foldr 264 (fn(((TermBdd(tg1,ass1,vm1,v,b)), (TermBdd(tg2,ass2,vm2,v',b'))), 265 (tg,ass, (l,l'), replacel)) 266 => 267 if not(Varmap.eq(vm,vm1) andalso Varmap.eq(vm,vm2)) 268 then ( print "unequal varmaps\n"; 269 raise BddReplaceError) else 270 if not(is_var v) 271 then (print_term v ; print " should be a variable\n"; 272 raise BddReplaceError) else 273 if not(is_var v') 274 then (print_term v' ; print " should be a variable\n"; 275 raise BddReplaceError) else 276 if mem v l 277 then (print_term v ; print" repeated\n"; 278 raise BddReplaceError) else 279 if mem v' l' 280 then (print_term v' ; print" repeated\n"; 281 raise BddReplaceError) 282 else (Tag.merge tg (Tag.merge tg1 tg2), 283 HOLset.union(ass,HOLset.union(ass1,ass2)), 284 (v :: l, v' :: l'), 285 ((bdd.var b, bdd.var b')::replacel))) 286 (tg,ass, ([],[]), []) 287 tbl 288 in 289 TermBdd(tg', 290 ass_union, 291 vm, 292 subst (ListPair.map (fn(v,v')=>(v|->v')) (l,l')) tm, 293 bdd.replace b (bdd.makepairSet replacel)) 294 end; 295 296(* Test examples ================================================================== 297 298val tb1 = termToTermBdd ``x /\ y /\ z``; 299 300val tbx = termToTermBdd ``x:bool`` 301and tby = termToTermBdd ``y:bool`` 302and tbz = termToTermBdd ``z:bool`` 303and tbp = termToTermBdd ``p:bool`` 304and tbq = termToTermBdd ``q:bool``; 305 306(* Repeat to sync all the varmaps! *) 307 308val tb = tb1 and tbl = [(tbx,tbp),(tby,tbq)]; 309val tb = BddReplace tbl tb; 310 311val tb = tb1 and tbl = [(tbx,tby),(tby,tbz),(tbz,tbx)]; 312val tb = BddReplace tbl tb; 313 314val tb = tb1 and tbl = [(tbx,tby),(tby,tbz)]; 315val tb = BddReplace tbl tb; 316(* ! Fail "Trying to replace with variables already in the bdd" *) 317 318val tb = tb1 and tbl = [(tbx,tby),(tby,tbx)]; 319val tb = BddReplace tbl tb; 320 321val tb = tb1 and tbl = [(tbx,tbp),(tby,tbp)]; 322val tb4 = BddReplace tbl tb; 323(* p repeated *) 324 325======================================================= End of test examples *) 326 327(*****************************************************************************) 328(* (ass vm v |--> b, ass1 vm tm1 |--> b1) ass2 vm tm2 |--> b2 *) 329(* ------------------------------------------------------------- *) 330(* (ass U ass1 U ass2) vm *) 331(* (subst [v |-> tm1] tm2) |--> compose (var b, b1) b2 *) 332(*****************************************************************************) 333 334exception BddComposeError; 335 336fun BddCompose 337 (TermBdd(tg,ass,vm,v,b), TermBdd(tg1,ass1,vm1,tm1,b1)) 338 (TermBdd(tg2,ass2,vm2,tm2,b2)) = 339 if is_var v andalso Varmap.eq(vm,vm1) andalso Varmap.eq(vm1,vm2) 340 then TermBdd(Tag.merge tg (Tag.merge tg1 tg2), 341 HOLset.union(ass,HOLset.union(ass1,ass2)), 342 vm, 343 subst[v |-> tm1]tm2, 344 bdd.compose (bdd.var b, b1) b2) 345 else (print "different varmaps\n"; raise BddComposeError); 346 347(*****************************************************************************) 348(* [(ass1 vm v1 |--> b1 , ass1' vm tm1 |--> b1'), *) 349(* . *) 350(* . *) 351(* . *) 352(* (assi vm vi |--> bi , assi' vm tmi |--> bi')] *) 353(* ass vm tm |--> b *) 354(* ------------------------------------------------------------------------ *) 355(* (ass1 U ass1' ... assi U assi' U ass) *) 356(* vm *) 357(* (subst[v1 |-> tm1, ... , vi |-> tmi]tm) *) 358(* |--> *) 359(* veccompose (composeSet (map (var ## I) [(b1,b1'), ... , (bi,bi')])) b *) 360(*****************************************************************************) 361 362exception BddListComposeError; 363 364fun BddListCompose tbl (TermBdd(tg,ass,vm,tm,b)) = 365 let val (tg_merge,ass_union, (l,l') ,composel) = 366 foldr 367 (fn(((TermBdd(tg1,ass1,vm1,v,b)),(TermBdd(tg2,ass2,vm2,tm,b'))), 368 (tg,ass, (l,l'), composel)) 369 => 370 if not(Varmap.eq(vm,vm1) andalso Varmap.eq(vm,vm2)) 371 then ( print "unequal varmaps\n"; 372 raise BddListComposeError) else 373 if not(is_var v) 374 then (print_term v ; print " should be a variable\n"; 375 raise BddListComposeError) else 376 if mem v l 377 then (print_term v ; print" repeated\n"; 378 raise BddListComposeError) 379 else (Tag.merge tg (Tag.merge tg1 tg2), 380 HOLset.union(ass,HOLset.union(ass1,ass2)), 381 (v :: l, tm :: l'), 382 ((bdd.var b, b')::composel))) 383 (tg,ass, ([],[]), []) 384 tbl 385 in 386 TermBdd(tg_merge, 387 ass_union, 388 vm, 389 subst (ListPair.map (fn(v,tm)=>(v|->tm)) (l,l')) tm, 390 bdd.veccompose (bdd.composeSet composel) b) 391 end; 392 393 394(* Test examples ================================================================== 395 396val tb1 = termToTermBdd ``x /\ y /\ z``; 397 398val tbx = termToTermBdd ``x:bool`` 399and tby = termToTermBdd ``y:bool`` 400and tbz = termToTermBdd ``z:bool`` 401and tbp = termToTermBdd ``p:bool`` 402and tbq = termToTermBdd ``q:bool``; 403 404(* Repeat to sync all the varmaps! *) 405 406val tb = tb1 and tbl = [(tbx,tbp),(tby,tbq)]; 407val tb = BddListCompose tbl tb; 408 409val tb = tb1 and tbl = [(tbx,tby),(tby,tbz),(tbz,tbx)]; 410val tb = BddListCompose tbl tb; 411 412val tb = tb1 and tbl = [(tbx,tby),(tby,tbz)]; 413val tb = BddListCompose tbl tb; 414 415val tb = tb1 and tbl = [(tbx,tby),(tby,tbx)]; 416val tb = BddListCompose tbl tb; 417 418val tb = tb1 and tbl = [(tbx,tbp),(tby,tbp)]; 419val tb4 = BddListCompose tbl tb; 420(* p repeated *) 421 422======================================================= End of test examples *) 423 424 425(*****************************************************************************) 426(* BddRestrict *) 427(* [((ass1 vm v1 |--> b1),(ass1' vm c1 |--> b1')), *) 428(* *) 429(* ((assi vm vi |--> bi),(assi' vm ci |--> bi'))] *) 430(* (ass vm tm |--> b) *) 431(* (where c1,...,ci are T or F) *) 432(* *) 433(* ass1 vm v1 |--> b1 ... ass1' vm c1 |-> b1' *) 434(* . *) 435(* . *) 436(* . *) 437(* assi vm vi |--> bi ... assi' vm ci |-> bi' *) 438(* ass vm tm |--> b *) 439(* --------------------------------------------------------------- *) 440(* (ass1 U ass1' ... assi U assi' U ass) *) 441(* vm *) 442(* (subst[v1 |-> c1, ... , vi |-> ci]tm) *) 443(* |--> *) 444(* restrict b (assignment[(var b1,mlval c1),...,(var i, mlval ci)]) *) 445(*****************************************************************************) 446 447exception BddRestrictError; 448 449local 450 451fun mlval tm = 452 if tm=T 453 then true 454 else if tm=F then false else raise BddRestrictError 455 456in 457 458fun BddRestrict tbl tb = 459 let val TermBdd(tg,ass,vm,tm,b) = tb 460 val (tg_merge,ass_union, (l,l') ,restrictl) = 461 foldr 462 (fn(((TermBdd(tg1,ass1,vm1,v,b)),(TermBdd(tg2,ass2,vm2,c,_))), 463 (tg,ass, (l,l'), restrictl)) 464 => 465 if not(Varmap.eq(vm,vm1) andalso Varmap.eq(vm,vm2)) 466 then ( print "unequal varmaps\n"; 467 raise BddRestrictError) else 468 if not(is_var v) 469 then (print_term v ; print " should be a variable\n"; 470 raise BddRestrictError) else 471 if mem v l 472 then (print_term v ; print" repeated\n"; 473 raise BddRestrictError) 474 else (Tag.merge tg (Tag.merge tg1 tg2), 475 HOLset.union(ass,HOLset.union(ass1,ass2)), 476 (v :: l, c :: l'), 477 ((bdd.var b, mlval c)::restrictl))) 478 (tg,ass, ([],[]), []) 479 tbl 480 in 481 TermBdd(tg_merge, 482 ass_union, 483 vm, 484 subst (ListPair.map (fn(v,c)=>(v|->c)) (l,l')) tm, 485 bdd.restrict b (bdd.assignment restrictl)) 486 end 487 488end; 489 490(*****************************************************************************) 491(* BddCon true vm = ({} vm ``T`` |--> TRUE) *) 492(* BddCon false vm = ({} vm ``F`` |--> FALSE) *) 493(*****************************************************************************) 494 495fun BddCon tv vm = 496 if tv then TermBdd(HolBddTag,Term.empty_tmset,vm,T,bdd.TRUE) 497 else TermBdd(HolBddTag,Term.empty_tmset,vm,F,bdd.FALSE); 498 499(*****************************************************************************) 500(* *) 501(* Varmap.peek vm (name v) = SOME n *) 502(* --------------------------------- BddVar true *) 503(* {} vm v |--> ithvar n *) 504(* *) 505(* Varmap.peek vm (name v) = SOME n *) 506(* --------------------------------- BddVar false *) 507(* {} vm v |--> nithvar n *) 508(* *) 509(*****************************************************************************) 510 511exception BddVarError; 512 513fun BddVar tv vm v = 514 case Varmap.peek vm (name v) of 515 SOME n => if tv 516 then TermBdd(HolBddTag,Term.empty_tmset,vm, v, bdd.ithvar n) 517 else TermBdd(HolBddTag,Term.empty_tmset,vm, mk_neg v, bdd.nithvar n) 518 | NONE => (print_term v; print " not in varmap\n"; raise BddVarError); 519 520(*****************************************************************************) 521(* ass vm t |--> b *) 522(* -------------------- *) 523(* ass vm ~t |--> NOT b *) 524(*****************************************************************************) 525 526fun BddNot(TermBdd(tg,ass,vm,t,b)) = TermBdd(tg,ass,vm, mk_neg t, bdd.NOT b); 527 528(*****************************************************************************) 529(* Auxiliary function to perform on two terms the operation corresponding *) 530(* to a bddop *) 531(*****************************************************************************) 532 533fun termApply t1 t2 (bddop:bdd.bddop) = 534 case bddop of 535 And => mk_conj(t1,t2) 536 | Biimp => mk_eq(t1,t2) 537 | Diff => mk_conj(t1, mk_neg t2) 538 | Imp => mk_imp(t1,t2) 539 | Invimp => mk_imp(t2,t1) 540 | Lessth => mk_conj(mk_neg t1, t2) 541 | Nand => mk_neg(mk_conj(t1,t2)) 542 | Nor => mk_neg(mk_disj(t1,t2)) 543 | Or => mk_disj(t1,t2) 544 | Xor => mk_neg(mk_eq(t1,t2)); 545 546(*****************************************************************************) 547(* as1 vm t1 |--> b1 ass2 vm t2 |--> b2 *) 548(* ------------------------------------------------- *) 549(* (ass1 U ass2) vm (t1 <bddop> t2) |--> b1 bddop b2 *) 550(* *) 551(* where <bddop> is an operation of terms corresponding to the BDD *) 552(* binary operatiobn bddop (N.B. can't use "op" as it's an SML keyword) *) 553(*****************************************************************************) 554 555exception BddOpError; 556 557fun BddOp (bddop, TermBdd(tg1,ass1,vm1,t1,b1), TermBdd(tg2,ass2,vm2,t2,b2)) = 558if Varmap.eq(vm1,vm2) 559 then TermBdd(Tag.merge tg1 tg2, 560 HOLset.union(ass1,ass2), 561 vm1, 562 termApply t1 t2 bddop, 563 bdd.apply b1 b2 bddop) 564 else (print "different varmaps\n"; raise BddOpError); 565 566(*****************************************************************************) 567(* DISCH for term_bdd *) 568(*****************************************************************************) 569 570exception BddDischError; 571 572fun BddDisch (TermBdd(tg1,ass1,vm1,tm1,b1)) (TermBdd(tg,ass,vm,tm,b)) = 573 BddOp(Imp, 574 TermBdd(tg1,ass1,vm1,tm1,b1), 575 TermBdd(tg,HOLset.delete(ass,tm1) handle HOLset.NotFound => ass,vm,tm,b)) 576 577(*****************************************************************************) 578(* ass vm t |--> b ass1 vm t1 |--> b1 ass2 vm t2 |--> b2 *) 579(* -------------------------------------------------------------- *) 580(* (ass U ass1 U ass2) vm (if t then t1 else t2) |--> ITE b b1 b2 *) 581(*****************************************************************************) 582 583exception BddIteError; 584 585fun BddIte(TermBdd(tg,ass,vm,t,b), 586 TermBdd(tg1,ass1,vm1,t1,b1), 587 TermBdd(tg2,ass2,vm2,t2,b2)) = 588 if Varmap.eq(vm,vm1) andalso Varmap.eq(vm1,vm2) 589 then TermBdd(Tag.merge tg (Tag.merge tg1 tg2), 590 HOLset.union(ass,HOLset.union(ass1,ass2)), 591 vm, 592 mk_cond(t,t1,t2), 593 bdd.ITE b b1 b2) 594 else (print "different varmaps\n"; raise BddIteError); 595 596(*****************************************************************************) 597(* ass vm t |--> b *) 598(* ------------------------------------------------------- *) 599(* ass vm (!v1...vi. t) |--> forall (makeset[n1,...,ni]) b *) 600(* *) 601(* where the list [v1,...,vi] of variables is supplied as a parameter, *) 602(* [n1,...,ni] is the list of the corresponding BDD variable numbers in vm *) 603(* and vm is assumed to contain v1,...,vi. *) 604(* Raises BddForallError if any variable vj is not in the domain of vm or if *) 605(* any of v1,...,vi occur free in any assumption *) 606(*****************************************************************************) 607 608exception BddForallError; 609 610fun BddForall vl (TermBdd(tg,ass,vm,t,b)) = 611 let open HOLset bdd 612 val tml = intersection 613 (addList(empty_tmset, vl), 614 foldl (fn (t,s) => FVL [t] s) empty_tmset ass) 615(* Possibly less efficient code: 616 val tml = intersection 617 (addList(empty_tmset, vl), FVL (listItems ass) empty_tmset) 618*) 619 in 620 if isEmpty tml 621 then 622 let val bddvars = 623 List.map 624 (fn v => case Varmap.peek vm (name v) of 625 SOME n => n 626 | NONE => raise BddForallError) 627 vl 628 in 629 TermBdd(tg,ass,vm, list_mk_forall(vl,t), forall (makeset bddvars) b) 630 end 631 else 632 (print_term(hd(listItems tml)); 633 print " free in assumptions"; 634 raise BddForallError) 635 end; 636 637(*****************************************************************************) 638(* ass vm t |--> b *) 639(* ------------------------------------------------------ *) 640(* ass vm (?v1...vi. t) |--> exist (makeset[n1,...,ni]) b *) 641(* *) 642(* where the list [v1,...,vi] of variables is supplied as a parameter, *) 643(* [n1,...,ni] is the list of the corresponding BDD variable numbers in vm *) 644(* and vm is assumed to contain v1,...,vi. *) 645(* Raises BddExistsError if any variable vj is not in the domain of vm or if *) 646(* any of v1,...,vi occur free in any assumption *) 647(*****************************************************************************) 648 649exception BddExistsError; 650 651fun BddExists vl (TermBdd(tg,ass,vm,t,b)) = 652 let open HOLset bdd 653 val tml = intersection(ass, FVL vl empty_tmset) 654 in 655 if isEmpty tml 656 then 657 let val bddvars = 658 List.map 659 (fn v => case Varmap.peek vm (name v) of 660 SOME n => n 661 | NONE => raise BddExistsError) 662 vl 663 in 664 TermBdd(tg,ass,vm, list_mk_exists(vl,t), exist (makeset bddvars) b) 665 end 666 else 667 (print_term(hd(listItems tml)); 668 print " free in assumptions"; 669 raise BddExistsError) 670 end; 671 672(*****************************************************************************) 673(* ass1 vm t1 |--> b1 ass2 vm t2 |--> b2 *) 674(* ---------------------------------------- *) 675(* (ass1 U ass1) *) 676(* vm *) 677(* (!v1...vi. t1 <bddop> t2) *) 678(* |--> *) 679(* appall b1 b2 bddop (makeset[n1,...,ni]) *) 680(* *) 681(* where the list [v1,...,vi] of variables is supplied as a parameter, *) 682(* [n1,...,ni] is the list of the corresponding BDD variable numbers and *) 683(* vm is assumed to contain v1,...,vi *) 684(* Raises BddAppallError if any variable vj is not in the domain of vm or if *) 685(* any of v1,...,vi occur free in any assumption *) 686(*****************************************************************************) 687 688exception BddAppallError; 689 690fun BddAppall vl (bddop, TermBdd(tg1,ass1,vm1,t1,b1), TermBdd(tg2,ass2,vm2,t2,b2)) = 691 let open HOLset bdd 692 val tg = Tag.merge tg1 tg2 693 val ass = union(ass1,ass2) 694 val tml = intersection(ass, FVL vl empty_tmset) 695 in 696 if isEmpty tml 697 then 698 (if Varmap.eq(vm1,vm2) 699 then 700 TermBdd 701 (tg, 702 ass, 703 vm1, 704 list_mk_forall(vl, termApply t1 t2 bddop), 705 appall 706 b1 707 b2 708 bddop 709 (makeset 710 (List.map (fn v => case Varmap.peek vm1 (name v) of 711 SOME n => n 712 | NONE => raise BddAppallError) 713 vl))) 714 else (print "different varmaps\n"; raise BddAppallError)) 715 else 716 (print_term(hd(listItems tml)); 717 print " free in assumptions"; 718 raise BddAppallError) 719 end; 720 721(*****************************************************************************) 722(* ass1 vm t1 |--> b1 ass2 vm t2 |--> b2 *) 723(* ---------------------------------------- *) 724(* (ass1 U ass1) *) 725(* vm *) 726(* (?v1...vi. t1 <bddop> t2) *) 727(* |--> *) 728(* appex b1 b2 bddop (makeset[n1,...,ni]) *) 729(* *) 730(* where the list [v1,...,vi] of variables is supplied as a parameter, *) 731(* [n1,...,ni] is the list of the corresponding BDD variable numbers and *) 732(* vm is assumed to contain v1,...,vi *) 733(* Raises BddAppexError if any variable vj is not in the domain of vm or if *) 734(* any of v1,...,vi occur free in any assumption *) 735(*****************************************************************************) 736 737exception BddAppexError; 738 739fun BddAppex vl (bddop, TermBdd(tg1,ass1,vm1,t1,b1), TermBdd(tg2,ass2,vm2,t2,b2)) = 740 let open HOLset bdd 741 val tg = Tag.merge tg1 tg2 742 val ass = union(ass1,ass2) 743 val tml = intersection(ass, FVL vl empty_tmset) 744 in 745 if isEmpty tml 746 then 747 (if Varmap.eq(vm1,vm2) 748 then 749 TermBdd 750 (tg, 751 ass, 752 vm1, 753 list_mk_exists(vl, termApply t1 t2 bddop), 754 appex 755 b1 756 b2 757 bddop 758 (makeset 759 (List.map (fn v => case Varmap.peek vm1 (name v) of 760 SOME n => n 761 | NONE => raise BddAppexError) 762 vl))) 763 else (print "different varmaps\n"; raise BddAppexError)) 764 else 765 (print_term(hd(listItems tml)); 766 print " free in assumptions"; 767 raise BddAppexError) 768 end; 769 770(*****************************************************************************) 771(* Coudert, Berthet, Madre simplification *) 772(* *) 773(* ass1 vm1 t1 |--> b1 ass2 vm2 t2 |--> b2 *) 774(* --------------------------------------------------- *) 775(* (ass1 U ass2 U {t1}) vm1 t2 |--> bdd.simplify b1 b2 *) 776(* *) 777(* Raises BddSimplifyError if vm1 and vm2 are not pointer equal *) 778(*****************************************************************************) 779 780exception BddSimplifyError; 781 782fun BddSimplify (TermBdd(tg1,ass1,vm1,t1,b1), TermBdd(tg2,ass2,vm2,t2,b2)) = 783 let open HOLset bdd 784 val tg = Tag.merge tg1 tg2 785 val ass = add(union(ass1,ass2), t1) 786 val _ = if Varmap.eq(vm1,vm2) then () else raise BddSimplifyError 787 in 788 TermBdd(tg,ass,vm1,t2, simplify b1 b2) 789 end; 790 791 792(*****************************************************************************) 793(* If t is satifiable (i.e. b is not FALSE) *) 794(* *) 795(* a vm t |--> b *) 796(* -------------------------------------- *) 797(* (a U {v1=c1,...,vn=cn}) vm t |--> TRUE *) 798(* *) 799(*****************************************************************************) 800 801(* Test data 802 803val (TermBdd(ass,vm,t,b)) = termToTermBdd ``x /\ y /\ ~z /\ (p \/ q)``; 804 805val (TermBdd(ass1,vm1,t1,b1)) = BddfindModel (TermBdd(ass,vm,t,b)); 806 807fun test t = 808 let val (TermBdd(ass,vm,t,b)) = BddfindModel(termToTermBdd t) 809 in 810 (t,EVAL(subst (List.map ((Lib.|->) o dest_eq) (HOLset.listItems ass)) t)) 811 end; 812 813*) 814 815exception BddfindModelError; 816 817fun BddfindModel (TermBdd(tg,ass,vm,t,b)) = 818 let val assl = bdd.getAssignment(bdd.satone b) 819 val vml = Varmap.dest vm 820 val setl = List.map 821 (fn (n,tv) => 822 mk_eq 823 ((case assoc2 n vml of 824 SOME(s,_) => mk_var(s,bool) 825 | NONE => (print "This should not happen!\n"; 826 raise BddfindModelError)), 827 if tv then T else F)) 828 assl 829 in 830 TermBdd(tg,HOLset.addList(ass,setl),vm,t,TRUE) 831 end; 832 833end; 834 835(* 836end; 837*) 838 839end 840