1(*  Title:      Tools/Argo/argo_solver.ML
2    Author:     Sascha Boehme
3
4The main interface to the Argo solver.
5
6The solver performs satisfiability checking for a given set of assertions. If these assertions
7are unsatisfiable, a proof trace is returned. If these assertions are satisfiable, the computed
8model can be queried or further assertions may be added.
9*)
10
11signature ARGO_SOLVER =
12sig
13  type context
14  val context: context
15  val assert: Argo_Expr.expr list -> context -> context (* raises Argo_Expr.TYPE, Argo_Expr.EXPR
16    and Argo_Proof.UNSAT *)
17  val model_of: context -> string * Argo_Expr.typ -> bool option
18end
19
20structure Argo_Solver: ARGO_SOLVER =
21struct
22
23(* context *)
24
25type context = {
26  next_axiom: int,
27  prf: Argo_Proof.context,
28  core: Argo_Core.context}
29
30fun mk_context next_axiom prf core: context = {next_axiom=next_axiom, prf=prf, core=core}
31
32val context = mk_context 0 Argo_Proof.solver_context Argo_Core.context
33
34
35(* rewriting and normalizing axioms *)
36
37val simp_context =
38  Argo_Rewr.context
39  |> Argo_Rewr.nnf
40  |> Argo_Rewr.norm_prop
41  |> Argo_Rewr.norm_ite
42  |> Argo_Rewr.norm_eq
43  |> Argo_Rewr.norm_arith
44
45val simp_axiom = Argo_Rewr.with_proof (Argo_Rewr.rewrite simp_context)
46
47
48(* asserting axioms *)
49
50fun add_axiom e ({next_axiom, prf, core}: context) =
51  let
52    val _ = Argo_Expr.check e
53    val (p, prf) = Argo_Proof.mk_axiom next_axiom prf
54    val (ep, prf) = simp_axiom (e, p) prf 
55    val (prf, core) = Argo_Clausify.clausify simp_context ep (prf, core)
56  in mk_context (next_axiom + 1) prf core end
57
58fun assert es cx =
59  let val {next_axiom, prf, core}: context = fold add_axiom es cx
60  in mk_context next_axiom prf (Argo_Core.run core) end
61
62
63(* models *)
64
65fun model_of ({core, ...}: context) = Argo_Core.model_of core
66
67end
68