1signature PrimitiveBddRules = sig
2
3  type assums = Term.term HOLset.set
4  type varmap = Varmap.varmap
5  type term_bdd
6
7  exception BddAppallError
8  exception nameError
9  exception BddSupportContractVarmapError
10  exception BddEqMpError
11  exception BddForallError
12  exception BddfindModelError
13  exception BddReplaceError
14  exception BddExtendVarmapError
15  exception BddIteError
16  exception BddExistsError
17  exception BddThmOracleError
18  exception BddVarError
19  exception BddRestrictError
20  exception BddSimplifyError
21  exception BddAppexError
22  exception BddComposeError
23  exception BddOpError
24  exception BddFreevarsContractVarmapError
25  exception BddListComposeError
26
27  val BddDisch : term_bdd -> term_bdd -> term_bdd
28  val BddListCompose : (term_bdd * term_bdd) list -> term_bdd -> term_bdd
29  val BddVar : bool -> varmap -> Term.term -> term_bdd
30  val getTag : term_bdd -> Thm.tag
31  val getAssums : term_bdd -> assums
32  val BddThmOracle : term_bdd -> Thm.thm
33  val getVarmap : term_bdd -> varmap
34  val BddNot : term_bdd -> term_bdd
35  val BddEqMp : Thm.thm -> term_bdd -> term_bdd
36  val BddfindModel : term_bdd -> term_bdd
37  val getTerm : term_bdd -> Term.term
38  val dest_term_bdd : term_bdd -> Thm.tag * assums * varmap * Term.term * bdd.bdd
39  val BddExists : Term.term list -> term_bdd -> term_bdd
40  val BddAppex : Term.term list -> bdd.bddop * term_bdd * term_bdd -> term_bdd
41  val getBdd : term_bdd -> bdd.bdd
42  val name : Term.term -> string
43  val inSupport : int -> bdd.bdd -> bool
44  val BddForall : Term.term list -> term_bdd -> term_bdd
45  val BddFreevarsContractVarmap : Term.term -> term_bdd -> term_bdd
46  val BddAppall : Term.term list -> bdd.bddop * term_bdd * term_bdd -> term_bdd
47  val BddCon : bool -> varmap -> term_bdd
48  val BddExtendVarmap : varmap  -> term_bdd -> term_bdd
49  val BddSimplify : term_bdd * term_bdd -> term_bdd
50  val BddCompose : term_bdd * term_bdd -> term_bdd -> term_bdd
51  val BddOp : bdd.bddop * term_bdd * term_bdd -> term_bdd
52  val BddRestrict : (term_bdd * term_bdd) list -> term_bdd -> term_bdd
53  val BddReplace : (term_bdd * term_bdd) list -> term_bdd -> term_bdd
54  val BddSupportContractVarmap : Term.term -> term_bdd -> term_bdd
55  val termApply : Term.term -> Term.term -> bdd.bddop -> Term.term
56  val BddIte : term_bdd * term_bdd * term_bdd -> term_bdd
57end
58