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