1signature DerivedBddRules = sig 2 3 type thm = Thm.thm 4 type term = Term.term 5 type bdd = bdd.bdd 6 type bddop = bdd.bddop 7 type term_bdd = PrimitiveBddRules.term_bdd 8 type varmap = Varmap.varmap 9 10 exception findModelError 11 exception dest_BddOpError 12 exception computeTraceError 13 exception termToTermBddError 14 exception BddApRestrictError 15 exception BddSatoneError 16 exception BddApReplaceError 17 exception fail 18 exception BddApSubstError 19 exception computeFixedpointError 20 exception bddToTermError 21 22 val isTRUE : term_bdd -> bool 23 val MkPrevThm : thm -> thm 24 val traceBack : varmap -> term_bdd list -> thm -> thm -> (term_bdd * (term_bdd * term_bdd) list) list 25 val BddEqualTest : term_bdd -> term_bdd -> bool 26 val TermBddToEqThm : term_bdd -> thm 27 val statecount : bdd -> real 28 val flatten_pair : term -> term list 29 val BddSatone : term_bdd -> (term_bdd * term_bdd) list 30 val bddToTerm : varmap -> bdd -> term 31 val findTrace : varmap -> thm -> thm -> thm -> thm * thm list * thm 32 val termToTermBddFun : (term -> term_bdd) ref 33 val BddRhsOracle : (term -> term_bdd) -> varmap -> thm -> thm 34 val computeTrace : (int -> term_bdd -> 'a) -> varmap -> thm -> thm * thm -> term_bdd list 35 val findModel : term_bdd -> thm 36 val MakeSimpRecThm : thm -> thm 37 val GenTermToTermBdd : (term -> term_bdd) -> varmap -> term -> term_bdd 38 val iterate : ('a -> bool) -> (int -> 'a -> 'a) -> 'a -> 'a 39 val BddSubst : (term_bdd * term_bdd) list -> term_bdd -> term_bdd 40 val BddApReplace : term_bdd -> term -> term_bdd 41 val eqToTermBdd : (term -> term_bdd) -> varmap -> thm -> term_bdd 42 val extendVarmap : term list -> varmap -> varmap 43 val isFALSE : term_bdd -> bool 44 val showVarmap : unit -> (string * int) list 45 val BddApConv : (term -> thm) -> term_bdd -> term_bdd 46 val computeFixedpoint : (int -> term_bdd -> 'a) -> varmap -> thm * thm -> term_bdd * term_bdd 47 val dest_BddOp : term -> bddop * term * term 48 val BddApSubst : term_bdd -> term -> term_bdd 49 val extendSat : term list -> varmap -> (term_bdd * term_bdd) list -> (term_bdd * term_bdd) list 50 val failfn : 'a -> 'b 51 val global_varmap : varmap ref 52 val split_subst : (term_bdd * term_bdd) list -> (term_bdd * term_bdd) list * (term_bdd * term_bdd) list 53 val BddAssume : term -> term_bdd 54 val thmToTermBdd : thm -> term_bdd 55 val BddApThm : thm -> term_bdd -> term_bdd 56 val BddApRestrict : term_bdd -> term -> term_bdd 57 val MkIterThms : thm -> term -> term -> thm * thm 58 val termToTermBdd : term -> term_bdd 59 val intToTerm : int -> term 60 val traceBackPrevThm : thm ref 61 62end 63