File ‹~~/src/Tools/Argo/argo_core.ML›
signature ARGO_CORE =
sig
type context
val context: 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
val run: context -> context
val model_of: context -> string * Argo_Expr.typ -> bool option
end
structure Argo_Core: ARGO_CORE =
struct
type context = {
terms: Argo_Term.context,
iter: int,
cdcl: Argo_Cdcl.context,
thy: Argo_Thy.context}
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
fun identify i ({terms, iter, cdcl, thy}: context) =
let val (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) =
let val (levels, cdcl) = Argo_Cdcl.add_axiom cls cdcl
in mk_context terms iter cdcl (backjump levels thy) end
datatype implications = None | Implications | Conflict of Argo_Cls.clause
fun cdcl_assume [] cdcl thy = (NONE, cdcl, thy)
| cdcl_assume (lit :: lits) cdcl thy =
(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) =>
(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)
|> fold (theory_deduce o Argo_Thy.assume) lps
|> theory_deduce Argo_Thy.check
fun search limit cdcl thy =
(case Argo_Cdcl.propagate cdcl of
(Argo_Common.Implied lps, cdcl) =>
(case theory_assume lps cdcl thy of
(None, cdcl, thy) =>
if limit <= 0 then (false, cdcl, thy)
else
(case Argo_Cdcl.decide cdcl of
NONE => (true, cdcl, thy)
| 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 =
let val (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
in if 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 =
(case search (next_restart_limit iter) cdcl thy of
(true, cdcl, thy) => (iter + 1, cdcl, thy)
| (false, cdcl, thy) =>
let val (levels, cdcl) = Argo_Cdcl.restart cdcl
in loop (iter + 1) cdcl (backjump levels thy) end)
fun run ({terms, iter, cdcl, thy}: context) =
let val (iter, cdcl, thy) = loop iter cdcl (Argo_Thy.prepare thy)
in mk_context terms iter cdcl thy end
fun model_of ({terms, cdcl, ...}: context) c =
(case Argo_Term.identify_item (Argo_Term.Expr (Argo_Expr.E (Argo_Expr.Con c, []))) terms of
(Argo_Term.Known t, _) => Argo_Cdcl.assignment_of cdcl (Argo_Lit.Pos t)
| (Argo_Term.New _, _) => NONE)
end