1263083Sjmmv(*  Title:      Tools/Argo/argo_core.ML
2263083Sjmmv    Author:     Sascha Boehme
3263083Sjmmv
4263083SjmmvCore of the Argo theorem prover implementing the DPLL(T) loop.
5263083Sjmmv
6263083SjmmvThe implementation is based on:
7263083Sjmmv
8263083Sjmmv  Harald Ganzinger, George Hagen, Robert Nieuwenhuis, Albert Oliveras,
9263083Sjmmv  Cesare Tinelli. DPLL(T): Fast decision procedures. In Lecture Notes in
10263083Sjmmv  Computer Science, volume 3114, pages 175-188. Springer, 2004.
11263083Sjmmv
12263083Sjmmv  Robert Nieuwenhuis, Albert Oliveras, Cesare Tinelli. Solving SAT and
13263083Sjmmv  SAT modulo theories: From an abstract Davis-Putnam-Logemann-Loveland
14263083Sjmmv  procedure to DPLL(T). In Journal of the ACM, volume 53(6), pages
15263083Sjmmv  937-977.  ACM, 2006.
16263083Sjmmv*)
17263083Sjmmv
18263083Sjmmvsignature ARGO_CORE =
19263083Sjmmvsig
20263083Sjmmv  (* context *)
21263083Sjmmv  type context
22263083Sjmmv  val context: context
23263083Sjmmv
24263083Sjmmv  (* enriching the context *)
25263083Sjmmv  val identify: Argo_Term.item -> context -> Argo_Term.identified * context
26263083Sjmmv  val add_atom: Argo_Term.item -> context -> Argo_Term.identified * context
27263083Sjmmv  val add_axiom: Argo_Cls.clause -> context -> context
28263083Sjmmv
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