1(* Title: Tools/Argo/argo_core.ML 2 Author: Sascha Boehme 3 4Core of the Argo theorem prover implementing the DPLL(T) loop. 5 6The implementation is based on: 7 8 Harald Ganzinger, George Hagen, Robert Nieuwenhuis, Albert Oliveras, 9 Cesare Tinelli. DPLL(T): Fast decision procedures. In Lecture Notes in 10 Computer Science, volume 3114, pages 175-188. Springer, 2004. 11 12 Robert Nieuwenhuis, Albert Oliveras, Cesare Tinelli. Solving SAT and 13 SAT modulo theories: From an abstract Davis-Putnam-Logemann-Loveland 14 procedure to DPLL(T). In Journal of the ACM, volume 53(6), pages 15 937-977. ACM, 2006. 16*) 17 18signature ARGO_CORE = 19sig 20 (* context *) 21 type context 22 val context: context 23 24 (* enriching the context *) 25 val identify: Argo_Term.item -> context -> Argo_Term.identified * context 26 val add_atom: Argo_Term.item -> context -> Argo_Term.identified * context 27 val add_axiom: Argo_Cls.clause -> context -> context 28 29 (* DPLL(T) loop *) 30 val run: context -> context (* raises Argo_Proof.UNSAT *) 31 32 (* model *) 33 val model_of: context -> string * Argo_Expr.typ -> bool option 34end 35 36structure Argo_Core: ARGO_CORE = 37struct 38 39(* context *) 40 41type context = { 42 terms: Argo_Term.context, (* the term context to identify equal expressions *) 43 iter: int, (* the current iteration of the search *) 44 cdcl: Argo_Cdcl.context, (* the context of the propositional solver *) 45 thy: Argo_Thy.context} (* the context of the theory solver *) 46 47fun mk_context terms iter cdcl thy: context = {terms=terms, iter=iter, cdcl=cdcl, thy=thy} 48 49val context = mk_context Argo_Term.context 1 Argo_Cdcl.context Argo_Thy.context 50 51fun backjump levels = funpow levels Argo_Thy.backtrack 52 53 54(* enriching the context *) 55 56fun identify i ({terms, iter, cdcl, thy}: context) = 57 let val (identified, terms) = Argo_Term.identify_item i terms 58 in (identified, mk_context terms iter cdcl thy) end 59 60fun add_atom i cx = 61 (case identify i cx of 62 known as (Argo_Term.Known _, _) => known 63 | (atom as Argo_Term.New t, {terms, iter, cdcl, thy}: context) => 64 (case (Argo_Cdcl.add_atom t cdcl, Argo_Thy.add_atom t thy) of 65 (cdcl, (NONE, thy)) => (atom, mk_context terms iter cdcl thy) 66 | (cdcl, (SOME lit, thy)) => 67 (case Argo_Cdcl.assume Argo_Thy.explain lit cdcl thy of 68 (NONE, cdcl, thy) => (atom, mk_context terms iter cdcl thy) 69 | (SOME _, _, _) => raise Fail "bad conflict with new atom"))) 70 71fun add_axiom cls ({terms, iter, cdcl, thy}: context) = 72 let val (levels, cdcl) = Argo_Cdcl.add_axiom cls cdcl 73 in mk_context terms iter cdcl (backjump levels thy) end 74 75 76(* DPLL(T) loop: CDCL with theories *) 77 78datatype implications = None | Implications | Conflict of Argo_Cls.clause 79 80fun cdcl_assume [] cdcl thy = (NONE, cdcl, thy) 81 | cdcl_assume (lit :: lits) cdcl thy = 82 (* assume an assignment deduced by the theory solver *) 83 (case Argo_Cdcl.assume Argo_Thy.explain lit cdcl thy of 84 (NONE, cdcl, thy) => cdcl_assume lits cdcl thy 85 | (SOME cls, cdcl, thy) => (SOME cls, cdcl, thy)) 86 87fun theory_deduce _ (conflict as (Conflict _, _, _)) = conflict 88 | theory_deduce f (result, cdcl, thy) = 89 (case f thy of 90 (Argo_Common.Implied [], thy) => (result, cdcl, thy) 91 | (Argo_Common.Implied lits, thy) => 92 (* turn all implications of the theory solver into propositional assignments *) 93 (case cdcl_assume lits cdcl thy of 94 (NONE, cdcl, thy) => (Implications, cdcl, thy) 95 | (SOME cls, cdcl, thy) => (Conflict cls, cdcl, thy)) 96 | (Argo_Common.Conflict cls, thy) => (Conflict cls, cdcl, thy)) 97 98fun theory_assume [] cdcl thy = (None, cdcl, thy) 99 | theory_assume lps cdcl thy = 100 (None, cdcl, thy) 101 (* propagate all propositional implications to the theory solver *) 102 |> fold (theory_deduce o Argo_Thy.assume) lps 103 (* check the consistency of the theory model *) 104 |> theory_deduce Argo_Thy.check 105 106fun search limit cdcl thy = 107 (* collect all propositional implications of the last assignments *) 108 (case Argo_Cdcl.propagate cdcl of 109 (Argo_Common.Implied lps, cdcl) => 110 (* propagate all propositional implications to the theory solver *) 111 (case theory_assume lps cdcl thy of 112 (None, cdcl, thy) => 113 (* stop searching if the conflict limit has been exceeded *) 114 if limit <= 0 then (false, cdcl, thy) 115 else 116 (* no further propositional assignments, choose a value for the next unassigned atom *) 117 (case Argo_Cdcl.decide cdcl of 118 NONE => (true, cdcl, thy) (* the context is satisfiable *) 119 | SOME cdcl => search limit cdcl (Argo_Thy.add_level thy)) 120 | (Implications, cdcl, thy) => search limit cdcl thy 121 | (Conflict ([], p), _, _) => Argo_Proof.unsat p 122 | (Conflict cls, cdcl, thy) => analyze cls limit cdcl thy) 123 | (Argo_Common.Conflict cls, cdcl) => analyze cls limit cdcl thy) 124 125and analyze cls limit cdcl thy = 126 (* analyze the conflict, probably using lazy explanations from the theory solver *) 127 let val (levels, cdcl, thy) = Argo_Cdcl.analyze Argo_Thy.explain cls cdcl thy 128 in search (limit - 1) cdcl (backjump levels thy) end 129 130fun luby_number i = 131 let 132 fun mult p = if p < i + 1 then mult (2 * p) else p 133 val p = mult 2 134 in if i = p - 1 then p div 2 else luby_number (i - (p div 2) + 1) end 135 136fun next_restart_limit iter = 100 * luby_number iter 137 138fun loop iter cdcl thy = 139 (* perform a limited search that is stopped after a certain number of conflicts *) 140 (case search (next_restart_limit iter) cdcl thy of 141 (true, cdcl, thy) => (iter + 1, cdcl, thy) 142 | (false, cdcl, thy) => 143 (* restart the solvers to avoid that they get stuck in a fruitless search *) 144 let val (levels, cdcl) = Argo_Cdcl.restart cdcl 145 in loop (iter + 1) cdcl (backjump levels thy) end) 146 147fun run ({terms, iter, cdcl, thy}: context) = 148 let val (iter, cdcl, thy) = loop iter cdcl (Argo_Thy.prepare thy) 149 in mk_context terms iter cdcl thy end 150 151 152(* model *) 153 154fun model_of ({terms, cdcl, ...}: context) c = 155 (case Argo_Term.identify_item (Argo_Term.Expr (Argo_Expr.E (Argo_Expr.Con c, []))) terms of 156 (Argo_Term.Known t, _) => Argo_Cdcl.assignment_of cdcl (Argo_Lit.Pos t) 157 | (Argo_Term.New _, _) => NONE) 158 159end 160