Quellcode-Bibliothek argo_solver.ML Sprache: SML

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

The main interface to the Argo solver.

The solver performs satisfiability checking for a given set of assertions. If these assertions
are unsatisfiable, a proof trace is returned. If these assertions are satisfiable, the computed
model can be queried or further assertions may be added.
*)

signature ARGO_SOLVER =
sig
  type context
  val context: context
  val assert: Argo_Expr.expr list -> context -> context (* raises Argo_Expr.TYPE, Argo_Expr.EXPR
    and Argo_Proof.UNSAT *)
  val model_of: context -> string * Argo_Expr.typ -> bool option
end

structure Argo_Solver: ARGO_SOLVER =
struct

(* context *)

type context = {
  next_axiom: int,
  prf: Argo_Proof.context,
  core: Argo_Core.context}

fun mk_context next_axiom prf core: context = {next_axiom=next_axiom, prf=prf, core=core}

val context = mk_context 0 Argo_Proof.solver_context Argo_Core.context

(* rewriting and normalizing axioms *)

val simp_context =
  Argo_Rewr.context
  |> Argo_Rewr.nnf
  |> Argo_Rewr.norm_prop
  |> Argo_Rewr.norm_ite
  |> Argo_Rewr.norm_eq
  |> Argo_Rewr.norm_arith

val simp_axiom = Argo_Rewr.with_proof (Argo_Rewr.rewrite simp_context)

(* asserting axioms *)

fun add_axiom e ({next_axiom, prf, core}: context) =
  let
    val _ = Argo_Expr.check e
    val (p, prf) = Argo_Proof.mk_axiom next_axiom prf
    val (ep, prf) = simp_axiom (e, p) prf
    val (prf, core) = Argo_Clausify.clausify simp_context ep (prf, core)
  in mk_context (next_axiom + 1) prf core end

fun assert es cx =
  let val {next_axiom, prf, core}: context = fold add_axiom es cx
  in mk_context next_axiom prf (Argo_Core.run core) end

(* models *)

fun model_of ({core, ...}: context) = Argo_Core.model_of core

end

quality99%

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

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.