Core of the Argo theorem prover implementing the DPLL(T) loop.
The implementation is based on:
Harald Ganzinger, George Hagen, Robert Nieuwenhuis, Albert Oliveras, Cesare Tinelli. DPLL(T): Fast decision procedures. In Lecture Notes in Computer Science, volume 3114, pages 175-188. Springer, 2004.
Robert Nieuwenhuis, Albert Oliveras, Cesare Tinelli. Solving SAT and SAT modulo theories: From an abstract Davis-Putnam-Logemann-Loveland procedure to DPLL(T). In Journal of the ACM, volume 53(6), pages 937-977. ACM, 2006.
*)
signature ARGO_CORE = sig (* context *) type context val context: context
(* enriching the context *) val identify: Argo_Term.item -> context -> Argo_Term.identified * context val add_atom: Argo_Term.item -> context -> Argo_Term.identified * context val add_axiom: Argo_Cls.clause -> context -> context
(* model *) val model_of: context -> string * Argo_Expr.typ -> booloption end
structure Argo_Core: ARGO_CORE = struct
(* context *)
type context = {
terms: Argo_Term.context, (* the term context to identify equal expressions *)
iter: int, (* the current iteration of the search *)
cdcl: Argo_Cdcl.context, (* the context of the propositional solver *)
thy: Argo_Thy.context} (* the context of the theory solver *)
fun mk_context terms iter cdcl thy: context = {terms=terms, iter=iter, cdcl=cdcl, thy=thy}
val context = mk_context Argo_Term.context 1 Argo_Cdcl.context Argo_Thy.context
fun backjump levels = funpow levels Argo_Thy.backtrack
(* enriching the context *)
fun identify i ({terms, iter, cdcl, thy}: context) = letval (identified, terms) = Argo_Term.identify_item i terms in (identified, mk_context terms iter cdcl thy) end
fun add_atom i cx =
(case identify i cx of
known as (Argo_Term.Known _, _) => known
| (atom as Argo_Term.New t, {terms, iter, cdcl, thy}: context) =>
(case (Argo_Cdcl.add_atom t cdcl, Argo_Thy.add_atom t thy) of
(cdcl, (NONE, thy)) => (atom, mk_context terms iter cdcl thy)
| (cdcl, (SOME lit, thy)) =>
(case Argo_Cdcl.assume Argo_Thy.explain lit cdcl thy of
(NONE, cdcl, thy) => (atom, mk_context terms iter cdcl thy)
| (SOME _, _, _) => raise Fail "bad conflict with new atom")))
fun add_axiom cls ({terms, iter, cdcl, thy}: context) = letval (levels, cdcl) = Argo_Cdcl.add_axiom cls cdcl in mk_context terms iter cdcl (backjump levels thy) end
(* DPLL(T) loop: CDCL with theories *)
datatype implications = None | Implications | Conflict of Argo_Cls.clause
fun cdcl_assume [] cdcl thy = (NONE, cdcl, thy)
| cdcl_assume (lit :: lits) cdcl thy = (* assume an assignment deduced by the theory solver *)
(case Argo_Cdcl.assume Argo_Thy.explain lit cdcl thy of
(NONE, cdcl, thy) => cdcl_assume lits cdcl thy
| (SOME cls, cdcl, thy) => (SOME cls, cdcl, thy))
fun theory_deduce _ (conflict as (Conflict _, _, _)) = conflict
| theory_deduce f (result, cdcl, thy) =
(case f thy of
(Argo_Common.Implied [], thy) => (result, cdcl, thy)
| (Argo_Common.Implied lits, thy) => (* turn all implications of the theory solver into propositional assignments *)
(case cdcl_assume lits cdcl thy of
(NONE, cdcl, thy) => (Implications, cdcl, thy)
| (SOME cls, cdcl, thy) => (Conflict cls, cdcl, thy))
| (Argo_Common.Conflict cls, thy) => (Conflict cls, cdcl, thy))
fun theory_assume [] cdcl thy = (None, cdcl, thy)
| theory_assume lps cdcl thy =
(None, cdcl, thy) (* propagate all propositional implications to the theory solver *)
|> fold (theory_deduce o Argo_Thy.assume) lps (* check the consistency of the theory model *)
|> theory_deduce Argo_Thy.check
fun search limit cdcl thy = (* collect all propositional implications of the last assignments *)
(case Argo_Cdcl.propagate cdcl of
(Argo_Common.Implied lps, cdcl) => (* propagate all propositional implications to the theory solver *)
(case theory_assume lps cdcl thy of
(None, cdcl, thy) => (* stop searching if the conflict limit has been exceeded *) if limit <= 0 then (false, cdcl, thy) else (* no further propositional assignments, choose a value for the next unassigned atom *)
(case Argo_Cdcl.decide cdcl of
NONE => (true, cdcl, thy) (* the context is satisfiable *)
| SOME cdcl => search limit cdcl (Argo_Thy.add_level thy))
| (Implications, cdcl, thy) => search limit cdcl thy
| (Conflict ([], p), _, _) => Argo_Proof.unsat p
| (Conflict cls, cdcl, thy) => analyze cls limit cdcl thy)
| (Argo_Common.Conflict cls, cdcl) => analyze cls limit cdcl thy)
and analyze cls limit cdcl thy = (* analyze the conflict, probably using lazy explanations from the theory solver *) letval (levels, cdcl, thy) = Argo_Cdcl.analyze Argo_Thy.explain cls cdcl thy in search (limit - 1) cdcl (backjump levels thy) end
fun luby_number i = let fun mult p = if p < i + 1 then mult (2 * p) else p val p = mult 2 inif i = p - 1 then p div 2 else luby_number (i - (p div 2) + 1) end
fun next_restart_limit iter = 100 * luby_number iter
fun loop iter cdcl thy = (* perform a limited search that is stopped after a certain number of conflicts *)
(case search (next_restart_limit iter) cdcl thy of
(true, cdcl, thy) => (iter + 1, cdcl, thy)
| (false, cdcl, thy) => (* restart the solvers to avoid that they get stuck in a fruitless search *) letval (levels, cdcl) = Argo_Cdcl.restart cdcl in loop (iter + 1) cdcl (backjump levels thy) end)
fun run ({terms, iter, cdcl, thy}: context) = letval (iter, cdcl, thy) = loop iter cdcl (Argo_Thy.prepare thy) in mk_context terms iter cdcl thy end
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung ist noch experimentell.
