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