From d6c84b93bf85950c4b2f2e403fe4e411b16af095 Mon Sep 17 00:00:00 2001 From: Simon Cruanes Date: Thu, 28 Dec 2017 19:23:36 +0100 Subject: [PATCH] restrict what Msat core lib exposes, provide shortcuts --- src/backend/Dimacs.ml | 2 +- src/backend/Dimacs.mli | 2 +- src/core/Msat.ml | 39 +++++++++++++++++++++++++++ src/core/{External.ml => Solver.ml} | 0 src/core/{External.mli => Solver.mli} | 0 src/main/main.ml | 6 ++--- src/solver/mcsolver.ml | 6 ++--- src/solver/mcsolver.mli | 2 +- src/solver/solver.ml | 6 ++--- src/solver/solver.mli | 2 +- tests/test_api.ml | 2 +- 11 files changed, 53 insertions(+), 14 deletions(-) create mode 100644 src/core/Msat.ml rename src/core/{External.ml => Solver.ml} (100%) rename src/core/{External.mli => Solver.mli} (100%) diff --git a/src/backend/Dimacs.ml b/src/backend/Dimacs.ml index cbec4c32..f2445d9f 100644 --- a/src/backend/Dimacs.ml +++ b/src/backend/Dimacs.ml @@ -32,7 +32,7 @@ module type S = sig end -module Make(St : Solver_types.S)(Dummy: sig end) = struct +module Make(St : Solver_types_intf.S)(Dummy: sig end) = struct (* Dimacs & iCNF export *) let export_vec name fmt vec = diff --git a/src/backend/Dimacs.mli b/src/backend/Dimacs.mli index dcd11b47..0ad94e63 100644 --- a/src/backend/Dimacs.mli +++ b/src/backend/Dimacs.mli @@ -42,6 +42,6 @@ module type S = sig end -module Make(St: Solver_types.S)(Dummy: sig end) : S with type clause := St.clause +module Make(St: Solver_types_intf.S)(Dummy: sig end) : S with type clause := St.clause (** Functor to create a module for exporting probems to the dimacs (& iCNF) formats. *) diff --git a/src/core/Msat.ml b/src/core/Msat.ml new file mode 100644 index 00000000..daa470c2 --- /dev/null +++ b/src/core/Msat.ml @@ -0,0 +1,39 @@ + +(** Main API *) + +module Formula_intf = Formula_intf +module Plugin_intf = Plugin_intf +module Theory_intf = Theory_intf +module Expr_intf = Expr_intf +module Solver_types_intf = Solver_types_intf + +module Res = Res + +module type S = Solver_intf.S + +type ('term, 'form) sat_state = ('term, 'form) Solver_intf.sat_state = { + eval : 'form -> bool; + eval_level : 'form -> bool * int; + iter_trail : ('form -> unit) -> ('term -> unit) -> unit; + model : unit -> ('term * 'term) list; +} + +type ('clause, 'proof) unsat_state = ('clause, 'proof) Solver_intf.unsat_state = { + unsat_conflict : unit -> 'clause; + get_proof : unit -> 'proof; +} +type 'clause export = 'clause Solver_intf.export = { + hyps : 'clause Vec.t; + history : 'clause Vec.t; + local : 'clause Vec.t; +} + +module Make_smt_expr(E : Formula_intf.S) = Solver_types.SatMake(E) +module Make_mcsat_expr(E : Expr_intf.S) = Solver_types.McMake(E) + +module Make = Solver.Make + +(**/**) +module Vec = Vec +module Log = Log +(**/**) diff --git a/src/core/External.ml b/src/core/Solver.ml similarity index 100% rename from src/core/External.ml rename to src/core/Solver.ml diff --git a/src/core/External.mli b/src/core/Solver.mli similarity index 100% rename from src/core/External.mli rename to src/core/Solver.mli diff --git a/src/main/main.ml b/src/main/main.ml index 9ca05d85..c1df4484 100644 --- a/src/main/main.ml +++ b/src/main/main.ml @@ -27,7 +27,7 @@ module type S = sig end module Make - (S : External.S) + (S : Msat.S) (T : Msat_solver.Type.S with type atom := S.atom) : sig val do_task : Dolmen.Statement.t -> unit @@ -42,7 +42,7 @@ module Make let l = List.map (function a -> Log.debugf 99 (fun k -> k "Checking value of %a" S.St.pp_atom (S.St.add_atom a)); - state.Solver_intf.eval a) c in + state.Msat.eval a) c in List.exists (fun x -> x) l in let l = List.map check_clause !hyps in @@ -60,7 +60,7 @@ module Make Format.printf "Sat (%f/%f)@." t t' | S.Unsat state -> if !p_check then begin - let p = state.Solver_intf.get_proof () in + let p = state.Msat.get_proof () in S.Proof.check p; if !p_dot_proof <> "" then begin let fmt = Format.formatter_of_out_channel (open_out !p_dot_proof) in diff --git a/src/solver/mcsolver.ml b/src/solver/mcsolver.ml index 4c68e07c..a81bf7ae 100644 --- a/src/solver/mcsolver.ml +++ b/src/solver/mcsolver.ml @@ -4,15 +4,15 @@ Copyright 2014 Guillaume Bury Copyright 2014 Simon Cruanes *) -module type S = Solver_intf.S +module type S = Msat.S module Make (E : Expr_intf.S) (Th : Plugin_intf.S with type term = E.Term.t and type formula = E.Formula.t and type proof = E.proof) () = - External.Make - (Solver_types.McMake(E)(struct end)) + Msat.Make + (Make_mcsat_expr(E)()) (Th) () diff --git a/src/solver/mcsolver.mli b/src/solver/mcsolver.mli index 383fcc8f..7ae92fad 100644 --- a/src/solver/mcsolver.mli +++ b/src/solver/mcsolver.mli @@ -9,7 +9,7 @@ Copyright 2014 Simon Cruanes This module provides a functor to create an McSAt solver. *) -module type S = Solver_intf.S +module type S = Msat.S (** The interface exposed by the solver. *) module Make (E : Expr_intf.S) diff --git a/src/solver/solver.ml b/src/solver/solver.ml index 8f86a1f1..8ad787c5 100644 --- a/src/solver/solver.ml +++ b/src/solver/solver.ml @@ -10,7 +10,7 @@ (* *) (**************************************************************************) -module type S = Solver_intf.S +module type S = Msat.S module DummyTheory(F : Formula_intf.S) = struct (* We don't have anything to do since the SAT Solver already @@ -77,8 +77,8 @@ end module Make (E : Formula_intf.S) (Th : Theory_intf.S with type formula = E.t and type proof = E.proof) () = - External.Make - (Solver_types.SatMake(E)(struct end)) + Msat.Make + (Make_smt_expr(E)(struct end)) (Plugin(E)(Th)) () diff --git a/src/solver/solver.mli b/src/solver/solver.mli index 2480e453..37840eb7 100644 --- a/src/solver/solver.mli +++ b/src/solver/solver.mli @@ -11,7 +11,7 @@ Copyright 2014 Simon Cruanes functor in order to create a pure SAT solver. *) -module type S = Solver_intf.S +module type S = Msat.S (** The interface of instantiated solvers. *) module DummyTheory(F : Formula_intf.S) : diff --git a/tests/test_api.ml b/tests/test_api.ml index fc41286e..2d9aa422 100644 --- a/tests/test_api.ml +++ b/tests/test_api.ml @@ -51,7 +51,7 @@ let mk_solver (): (module BASIC_SOLVER) = | Sat _ -> R_sat | Unsat us -> - let p = us.Solver_intf.get_proof () in + let p = us.Msat.get_proof () in Proof.check p; R_unsat end