Quellcode-Bibliothek argo_core.ML Sprache: SML

(*  Title:      Tools/Argo/argo_core.ML
    Author:     Sascha Boehme

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

  (* DPLL(T) loop *)
  val run: context -> context (* raises Argo_Proof.UNSAT *)

  (* model *)
  val model_of: context -> string * Argo_Expr.typ -> bool option
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) =
  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

(* 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 *)
  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 =
  (* 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 *)
      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

(* model *)

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

quality100%

¤ 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.0.11Bemerkung: (vorverarbeitet) ¤

*Bot Zugriff

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

Haftungshinweis

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.