From ce65f10f9cbb349f6188a70b60313b2f99b99ba9 Mon Sep 17 00:00:00 2001 From: Guillaume Bury Date: Sun, 31 Jan 2016 02:09:16 +0100 Subject: [PATCH] Big cleanup of interfaces. Breaks retro-compat ! --- main.ml | 2 + msat.mlpack | 1 + sat/sat.ml | 79 +++----------------- sat/sat.mli | 107 ++++++++++----------------- smt/mcsat.ml | 4 ++ smt/smt.ml | 43 ++--------- smt/smt.mli | 34 +-------- solver/solver.ml | 163 +++++++++++++++++++++++++++--------------- solver/solver.mli | 71 ++---------------- solver/solver_intf.ml | 84 ++++++++++++++++++++++ 10 files changed, 257 insertions(+), 331 deletions(-) create mode 100644 solver/solver_intf.ml diff --git a/main.ml b/main.ml index 9aedda8e..f5061db9 100644 --- a/main.ml +++ b/main.ml @@ -236,6 +236,7 @@ let main () = print "Unsat (%f)" (Sys.time ()); if !p_check then begin let p = Smt.get_proof () in + Smt.Proof.check p; print_proof p; if !p_unsat_core then print_unsat_core (Smt.unsat_core p) @@ -255,6 +256,7 @@ let main () = print "Unsat (%f)" (Sys.time ()); if !p_check then begin let p = Mcsat.get_proof () in + Mcsat.Proof.check p; print_mcproof p; if !p_unsat_core then print_mc_unsat_core (Mcsat.unsat_core p) diff --git a/msat.mlpack b/msat.mlpack index e53a1fc2..dde93da5 100644 --- a/msat.mlpack +++ b/msat.mlpack @@ -8,6 +8,7 @@ Plugin_intf Expr_intf Tseitin_intf Res_intf +Solver_intf Solver_types_intf # Solver Modules diff --git a/sat/sat.ml b/sat/sat.ml index a8da48ad..9ef90445 100644 --- a/sat/sat.ml +++ b/sat/sat.ml @@ -5,7 +5,8 @@ Copyright 2014 Simon Cruanes *) module Fsat = struct - exception Dummy of int + + exception Bad_atom type t = int type proof = unit @@ -19,8 +20,7 @@ module Fsat = struct max_index := max !max_index (abs i); i end else - (Format.printf "Warning : %d/%d@." i max_lit; - raise (Dummy i)) + raise Bad_atom let dummy = 0 @@ -40,6 +40,7 @@ module Fsat = struct let add_label _ _ = () let make i = _make (2 * i) + let fresh, iter = let create () = incr max_fresh; @@ -62,77 +63,19 @@ end module Tseitin = Tseitin.Make(Fsat) module Make(Dummy : sig end) = struct + module Tsat = Solver.DummyTheory(Fsat) - module SatSolver = Solver.Make(Fsat)(Tsat) - - exception Bad_atom - exception UndecidedLit = SatSolver.UndecidedLit - - type atom = Fsat.t - type clause = SatSolver.St.clause - type proof = SatSolver.Proof.proof - - let tag_clause = SatSolver.tag_clause - - type res = - | Sat - | Unsat - - let new_atom () = - try - Fsat.fresh () - with Fsat.Dummy _ -> - raise Bad_atom - - let make i = - try - Fsat.make i - with Fsat.Dummy _ -> - raise Bad_atom - - - let abs = Fsat.abs - let neg = Fsat.neg - let sign = Fsat.sign - let apply_sign = Fsat.apply_sign - let set_sign = Fsat.set_sign - - let hash = Fsat.hash - let equal = Fsat.equal - let compare = Fsat.compare - - let iter_atoms = Fsat.iter - - let solve () = - try - SatSolver.solve (); - Sat - with SatSolver.Unsat -> Unsat - - let assume ?tag l = - try - SatSolver.assume ?tag l - with SatSolver.Unsat -> () - - let eval = SatSolver.eval - let eval_level = SatSolver.eval_level - - let get_proof () = - (* SatSolver.Proof.learn (SatSolver.history ()); *) - match SatSolver.unsat_conflict () with - | None -> assert false - | Some c -> SatSolver.Proof.prove_unsat c - - let unsat_core = SatSolver.Proof.unsat_core + include Solver.Make(Fsat)(Tsat) let print_atom = Fsat.print - let print_clause = SatSolver.St.print_clause + let print_clause = St.print_clause let print_proof out p = - let module Dot = Dot.Make(SatSolver.Proof)(struct - let clause_name c = SatSolver.St.(c.name) - let print_atom = SatSolver.St.print_atom + let module Dot = Dot.Make(Proof)(struct + let clause_name c = St.(c.name) + let print_atom = St.print_atom let lemma_info () = "()", None, [] end) in Dot.print out p + end diff --git a/sat/sat.mli b/sat/sat.mli index d766a9cc..d830b3cd 100644 --- a/sat/sat.mli +++ b/sat/sat.mli @@ -4,88 +4,55 @@ Copyright 2014 Guillaume Bury Copyright 2014 Simon Cruanes *) -module Fsat : Formula_intf.S with type t = private int +module Fsat : sig + + include Formula_intf.S with type t = private int + + exception Bad_atom + (** Exception raised when a problem with atomic formula encoding is detected. *) + + val make : int -> t + (** Returns the literal corresponding to the integer. + @raise Bad_atom if given [0] as argument.*) + + val fresh : unit -> t + (** [new_atom ()] returns a fresh literal. + @raise Bad_atom if there are no more integer available to represent new atoms. *) + + val neg : t -> t + (** [neg a] returns the negation of a literal. Involutive, i.e [neg (neg a) = a]. *) + + val abs : t -> t + val sign : t -> bool + val apply_sign : bool -> t -> t + val set_sign : bool -> t -> t + (** Convenienc functions for manipulating literals. *) + + val hash : t -> int + val equal : t -> t -> bool + val compare : t -> t -> int + (** Usual hash and comparison functions. For now, directly uses + [Pervasives] and [Hashtbl] builtins. *) + + val iter : (t -> unit) -> unit + (** Allows iteration over all atoms created (even if unused). *) + +end module Tseitin : Tseitin.S with type atom = Fsat.t module Make(Dummy : sig end) : sig (** Fonctor to make a pure SAT Solver module with built-in literals. *) - exception UndecidedLit - - exception Bad_atom - (** Exception raised when a problem with atomic formula encoding is detected. *) - - type atom = Fsat.t - (** Type for atoms, i.e boolean literals. *) - - type clause - (** Abstract type for clauses *) - - type proof - (** Abstract type for resolution proofs *) - - type res = Sat | Unsat - (** Type of results returned by the solve function. *) - - val new_atom : unit -> atom - (** [new_atom ()] returns a fresh literal. - @raise Bad_atom if there are no more integer available to represent new atoms. *) - - val make : int -> atom - (** Returns the literal corresponding to the integer. - @raise Bad_atom if given [0] as argument.*) - - val neg : atom -> atom - (** [neg a] returns the negation of a literal. Involutive, i.e [neg (neg a) = a]. *) - - val abs : atom -> atom - val sign : atom -> bool - val apply_sign : bool -> atom -> atom - val set_sign : bool -> atom -> atom - - val hash : atom -> int - val equal : atom -> atom -> bool - val compare : atom -> atom -> int - (** Usual hash and comparison functions. For now, directly uses - [Pervasives] and [Hashtbl] builtins. *) - - val iter_atoms : (atom -> unit) -> unit - (** Allows iteration over all atoms created (even if unused). *) - - val solve : unit -> res - (** Returns the satisfiability status of the current set of assumptions. *) - - val eval : atom -> bool - (** Return the current assignement of the literal. - @raise UndecidedLit if the literal is not decided *) - - val eval_level : atom -> bool * int - (** Return the current assignement of the literals, as well as its - decision level. If the level is 0, then it is necessary for - the atom to have this value; otherwise it is due to choices - that can potentially be backtracked. - @raise UndecidedLit if the literal is not decided *) - - val assume : ?tag:int -> atom list list -> unit - (** Add a list of clauses to the set of assumptions. *) - - val tag_clause : clause -> int option - (** Returns the tag associated with the clause. *) - - val get_proof : unit -> proof - (** Returns the resolution proof found, if [solve] returned [Unsat]. *) - - val unsat_core : proof -> clause list - (** Returns the unsat-core of the proof. *) + include Solver.S with type St.formula = Fsat.t val print_atom : Format.formatter -> atom -> unit (** Print the atom on the given formatter. *) - val print_clause : Format.formatter -> clause -> unit + val print_clause : Format.formatter -> St.clause -> unit (** Print the clause on the given formatter. *) - val print_proof : Format.formatter -> proof -> unit + val print_proof : Format.formatter -> Proof.proof -> unit (** Print the given proof in dot format. *) end diff --git a/smt/mcsat.ml b/smt/mcsat.ml index 911b4dba..254f32e6 100644 --- a/smt/mcsat.ml +++ b/smt/mcsat.ml @@ -112,11 +112,15 @@ end module Make(Dummy:sig end) = struct module SmtSolver = Mcsolver.Make(Fsmt)(Tsmt) + + module Proof = SmtSolver.Proof + module Dot = Dot.Make(SmtSolver.Proof)(struct let print_atom = SmtSolver.St.print_atom let lemma_info () = "Proof", Some "PURPLE", [] end) + type atom = Fsmt.t type clause = SmtSolver.St.clause type proof = SmtSolver.Proof.proof diff --git a/smt/smt.ml b/smt/smt.ml index 8658ceed..1248fd57 100644 --- a/smt/smt.ml +++ b/smt/smt.ml @@ -61,45 +61,14 @@ end module Make(Dummy:sig end) = struct - module SmtSolver = Solver.Make(Fsmt)(Tsmt) - module Dot = Dot.Make(SmtSolver.Proof)(struct - let clause_name c = SmtSolver.St.(c.name) - let print_atom = SmtSolver.St.print_atom + include Solver.Make(Fsmt)(Tsmt) + module Dot = Dot.Make(Proof)(struct + let clause_name c = St.(c.name) + let print_atom = St.print_atom let lemma_info () = "Proof", Some "PURPLE", [] end) - type atom = Fsmt.t - type clause = SmtSolver.St.clause - type proof = SmtSolver.Proof.proof - - type res = - | Sat - | Unsat - - let solve () = - try - SmtSolver.solve (); - Sat - with SmtSolver.Unsat -> Unsat - - let assume l = - try - SmtSolver.assume l - with SmtSolver.Unsat -> () - - let get_proof () = - match SmtSolver.unsat_conflict () with - | None -> assert false - | Some c -> - let p = SmtSolver.Proof.prove_unsat c in - SmtSolver.Proof.check p; - p - - let eval = SmtSolver.eval - - let unsat_core = SmtSolver.Proof.unsat_core - - let print_atom = Fsmt.print - let print_clause = SmtSolver.St.print_clause + let print_clause = St.print_clause let print_proof = Dot.print + end diff --git a/smt/smt.mli b/smt/smt.mli index bbc9a05b..f11e3865 100644 --- a/smt/smt.mli +++ b/smt/smt.mli @@ -7,40 +7,12 @@ Copyright 2014 Simon Cruanes module Make(Dummy: sig end) : sig (** Fonctor to make a SMT Solver module with built-in literals. *) - type atom = Expr.Formula.t - (** Type for atoms, i.e boolean literals. *) + include Solver.S with type St.formula = Expr.t - type clause - (** Abstract type for clauses *) - - type proof - (** Abstract type for resolution proofs *) - - type res = Sat | Unsat - (** Type of results returned by the solve function. *) - - val solve : unit -> res - (** Returns the satisfiability status of the current set of assumptions. *) - - val assume : atom list list -> unit - (** Add a list of clauses to the set of assumptions. *) - - val eval : atom -> bool - (** Returns the valuation of the given atom in the current state of the prover *) - - val get_proof : unit -> proof - (** Returns the resolution proof found, if [solve] returned [Unsat]. *) - - val unsat_core : proof -> clause list - (** Returns the unsat-core of the proof. *) - - val print_atom : Format.formatter -> atom -> unit - (** Print the atom on the given formatter. *) - - val print_clause : Format.formatter -> clause -> unit + val print_clause : Format.formatter -> St.clause -> unit (** Print the clause on the given formatter. *) - val print_proof : Format.formatter -> proof -> unit + val print_proof : Format.formatter -> Proof.proof -> unit (** Print the given proof in dot format. *) end diff --git a/solver/solver.ml b/solver/solver.ml index 0915797d..c4207662 100644 --- a/solver/solver.ml +++ b/solver/solver.ml @@ -10,6 +10,8 @@ (* *) (**************************************************************************) +module type S = Solver_intf.S + module DummyTheory(F : Formula_intf.S with type proof = unit) = struct (* We don't have anything to do since the SAT Solver already * does propagation and conflict detection *) @@ -35,72 +37,115 @@ module DummyTheory(F : Formula_intf.S with type proof = unit) = struct let backtrack _ = () end +module Plugin(E : Formula_intf.S) + (Th : Theory_intf.S with type formula = E.t and type proof = E.proof) = struct + + type term = E.t + type formula = E.t + type proof = Th.proof + + type assumption = + | Lit of formula + | Assign of term * term + + type slice = { + start : int; + length : int; + get : int -> assumption * int; + push : formula list -> proof -> unit; + propagate : formula -> int -> unit; + } + + type level = Th.level + + type res = + | Sat + | Unsat of formula list * proof + + type eval_res = + | Valued of bool * int + | Unknown + + let dummy = Th.dummy + + let current_level = Th.current_level + + let assume_get s i = match s.get i with + | Lit f, _ -> f | _ -> assert false + + let assume s = + match Th.assume { + Th.start = s.start; + Th.length = s.length; + Th.get = assume_get s; + Th.push = s.push; + } with + | Th.Sat _ -> Sat + | Th.Unsat (l, p) -> Unsat (l, p) + + let backtrack = Th.backtrack + + let assign _ = assert false + + let iter_assignable _ _ = () + + let eval _ = Unknown + + let if_sat _ = () + + let proof_debug _ = assert false + +end + + module Make (E : Formula_intf.S) (Th : Theory_intf.S with type formula = E.t and type proof = E.proof) = struct - module Plugin = struct - type term = E.t - type formula = E.t - type proof = Th.proof - - type assumption = - | Lit of formula - | Assign of term * term - - type slice = { - start : int; - length : int; - get : int -> assumption * int; - push : formula list -> proof -> unit; - propagate : formula -> int -> unit; - } - - type level = Th.level - - type res = - | Sat - | Unsat of formula list * proof - - type eval_res = - | Valued of bool * int - | Unknown - - let dummy = Th.dummy - - let current_level = Th.current_level - - let assume_get s i = match s.get i with - | Lit f, _ -> f | _ -> assert false - - let assume s = - match Th.assume { - Th.start = s.start; - Th.length = s.length; - Th.get = assume_get s; - Th.push = s.push; - } with - | Th.Sat _ -> Sat - | Th.Unsat (l, p) -> Unsat (l, p) - - let backtrack = Th.backtrack - - let assign _ = assert false - - let iter_assignable _ _ = () - - let eval _ = Unknown - - let if_sat _ = () - - let proof_debug _ = assert false - end + module P = Plugin(E)(Th) module St = Solver_types.SatMake(E) - module S = Internal.Make(St)(Plugin) + module S = Internal.Make(St)(P) - include S + module Proof = S.Proof + + exception UndecidedLit = S.UndecidedLit + + type atom = E.t + type clause = St.clause + type proof = Proof.proof + + type res = Sat | Unsat + + let assume ?tag l = + try S.assume ?tag l + with S.Unsat -> () + + let solve () = + try + S.solve (); + Sat + with S.Unsat -> Unsat + + let eval = S.eval + let eval_level = S.eval_level + + let get_proof () = + match S.unsat_conflict () with + | None -> assert false + | Some c -> S.Proof.prove_unsat c + + let unsat_core = S.Proof.unsat_core + + let get_tag cl = St.(cl.tag) + + (* Push/pop operations *) + type level = S.level + let base_level = S.base_level + let current_level = S.current_level + let push = S.push + let pop = S.pop + let reset = S.reset - let tag_clause cl = St.(cl.tag) end diff --git a/solver/solver.mli b/solver/solver.mli index 6594ad63..8d705aa9 100644 --- a/solver/solver.mli +++ b/solver/solver.mli @@ -11,77 +11,16 @@ (* *) (**************************************************************************) +module type S = Solver_intf.S + (** Simple case where the proof type is [unit] and the theory is empty *) module DummyTheory(F : Formula_intf.S with type proof = unit) : Theory_intf.S with type formula = F.t and type proof = unit module Make (F : Formula_intf.S) - (Th : Theory_intf.S with type formula = F.t and type proof = F.proof) : sig + (Th : Theory_intf.S with type formula = F.t and type proof = F.proof) : + S with type St.formula = F.t + and type St.proof = F.proof (** Functor to create a SMT Solver parametrised by the atomic formulas and a theory. *) - exception Unsat - exception UndecidedLit - - module St : Solver_types.S - with type formula = F.t - and type proof = F.proof - - module Proof : Res.S with module St = St - - val solve : unit -> unit - (** Try and solves the current set of assumptions. - @return () if the current set of clauses is satisfiable - @raise Unsat if a toplevel conflict is found *) - - val assume : ?tag:int -> F.t list list -> unit - (** Add the list of clauses to the current set of assumptions. - Modifies the sat solver state in place. - @raise Unsat if a conflict is detect when adding the clauses *) - - val tag_clause : St.clause -> int option - (** Recover tag from a clause, if any *) - - val eval : F.t -> bool - (** Returns the valuation of a formula in the current state - of the sat solver. - @raise UndecidedLit if the literal is not decided *) - - val eval_level : F.t -> bool * int - (** Return the current assignement of the literals, as well as its - decision level. If the level is 0, then it is necessary for - the atom to have this value; otherwise it is due to choices - that can potentially be backtracked. - @raise UndecidedLit if the literal is not decided *) - - val hyps : unit -> St.clause Vec.t - (** Returns the vector of assumptions used by the solver. May be slightly different - from the clauses assumed because of top-level simplification of clauses. *) - - val history : unit -> St.clause Vec.t - (** Returns the history of learnt clauses, in the right order. *) - - val unsat_conflict : unit -> St.clause option - (** Returns the unsat clause found at the toplevel, if it exists (i.e if - [solve] has raised [Unsat]) *) - - type level - (** Abstract notion of assumption level. *) - - val base_level : level - (** Level with no assumption at all, corresponding to the empty solver *) - - val current_level : unit -> level - (** The current level *) - - val push : unit -> level - (** Create a new level that extends the previous one. *) - - val pop : level -> unit - (** Go back to the given level, forgetting every assumption added since. - @raise Invalid_argument if the current level is below the argument *) - - val reset : unit -> unit - (** Return to level {!base_level} *) -end - diff --git a/solver/solver_intf.ml b/solver/solver_intf.ml new file mode 100644 index 00000000..3b9ede7a --- /dev/null +++ b/solver/solver_intf.ml @@ -0,0 +1,84 @@ +(* +MSAT is free software, using the Apache license, see file LICENSE +Copyright 2016 Guillaume Bury +Copyright 2016 Simon Cruanes +*) + +module type S = sig + + (** {2 Internal modules} + These are the internal modules used, you should probablynot use them + if you're not familiar with the internals of mSAT. *) + + module St : Solver_types.S + + module Proof : Res.S with module St = St + + (** {2 Types} *) + + type atom = St.formula + (** The type of atoms given by the module argument for formulas *) + + type res = Sat | Unsat + (** Result type for the solver *) + + exception UndecidedLit + (** Exception raised by the evaluating functions when a literal + has not yet been assigned a value. *) + + (** {2 Base operations} *) + + val assume : ?tag:int -> atom list list -> unit + (** Add the list of clauses to the current set of assumptions. + Modifies the sat solver state in place. *) + + val solve : unit -> res + (** Try and solves the current set of assumptions. + @return () if the current set of clauses is satisfiable + @raise Unsat if a toplevel conflict is found *) + + val eval : atom -> bool + (** Returns the valuation of a formula in the current state + of the sat solver. + @raise UndecidedLit if the literal is not decided *) + + val eval_level : atom -> bool * int + (** Return the current assignement of the literals, as well as its + decision level. If the level is 0, then it is necessary for + the atom to have this value; otherwise it is due to choices + that can potentially be backtracked. + @raise UndecidedLit if the literal is not decided *) + + val get_proof : unit -> Proof.proof + (** If the last call to [solve] returned [Unsat], then returns a persistent + proof of the empty clause. *) + + val unsat_core : Proof.proof -> St.clause list + (** Returns the unsat core of a given proof. *) + + val get_tag : St.clause -> int option + (** Recover tag from a clause, if any *) + + (** {2 Push/Pop operations} *) + + type level + (** Abstract notion of assumption level. *) + + val base_level : level + (** Level with no assumption at all, corresponding to the empty solver *) + + val current_level : unit -> level + (** The current level *) + + val push : unit -> level + (** Create a new level that extends the previous one. *) + + val pop : level -> unit + (** Go back to the given level, forgetting every assumption added since. + @raise Invalid_argument if the current level is below the argument *) + + val reset : unit -> unit + (** Rest the state of the solver, i.e return to level {!base_level} *) + +end +