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