From 553d3203685be82073bb97a73fcc11858e5b1899 Mon Sep 17 00:00:00 2001 From: Guillaume Bury Date: Thu, 30 Jun 2016 09:54:21 +0200 Subject: [PATCH] Fixed compilation. Refactored some code in external --- main.ml | 4 +-- msat.mlpack | 1 + msat.odocl | 1 + smt/mcsat.ml | 52 +++++++-------------------------- smt/smt.ml | 3 +- solver/external.ml | 60 ++++++++++++++++++++++++++++++++++++++ solver/external.mli | 17 +++++++++++ solver/internal.ml | 5 ++-- solver/mcsolver.ml | 21 +++++++------- solver/mcsolver.mli | 71 +++++++-------------------------------------- solver/solver.ml | 53 ++++----------------------------- solver/solver.mli | 6 ++-- 12 files changed, 125 insertions(+), 169 deletions(-) create mode 100644 solver/external.ml create mode 100644 solver/external.mli diff --git a/main.ml b/main.ml index 2a879b0d..04e1c9c2 100644 --- a/main.ml +++ b/main.ml @@ -105,12 +105,12 @@ let print format = match !output with let print_proof proof = match !output with | Standard -> () | Dot -> Smt.print_dot std proof - | Dedulti -> Smt.print_dedukti std proof + | Dedukti -> Smt.print_dedukti std proof let print_mcproof proof = match !output with | Standard -> () | Dot -> Mcsat.print_dot std proof - | Dedulti -> Mcsat.print_dedukti std proof + | Dedukti -> Mcsat.print_dedukti std proof let rec print_cl fmt = function | [] -> Format.fprintf fmt "[]" diff --git a/msat.mlpack b/msat.mlpack index dde93da5..bf7c053c 100644 --- a/msat.mlpack +++ b/msat.mlpack @@ -13,6 +13,7 @@ Solver_types_intf # Solver Modules Internal +External Solver Mcsolver Solver_types diff --git a/msat.odocl b/msat.odocl index 9ccb844e..b7562e25 100644 --- a/msat.odocl +++ b/msat.odocl @@ -10,6 +10,7 @@ solver/Solver_types_intf solver/Solver_intf solver/Internal +solver/External solver/Solver solver/Mcsolver solver/Solver_types diff --git a/smt/mcsat.ml b/smt/mcsat.ml index 1888097f..daa16547 100644 --- a/smt/mcsat.ml +++ b/smt/mcsat.ml @@ -111,49 +111,19 @@ end module Make(Dummy:sig end) = struct - module SmtSolver = Mcsolver.Make(Fsmt)(Tsmt)(struct end) - - module Proof = SmtSolver.Proof - - module Dot = Dot.Make(SmtSolver.Proof)(struct - let print_atom = SmtSolver.St.print_atom + include Mcsolver.Make(Fsmt)(Tsmt)(struct end) + module Dot = Dot.Make(Proof)(struct + let print_atom = St.print_atom let lemma_info () = "Proof", Some "PURPLE", [] end) + module Dedukti = Dedukti.Make(Proof)(struct + let print _ _ = () + let prove _ _ = () + let context _ _ = () + end) + let print_clause = St.print_clause + let print_dot = Dot.print + let print_dedukti = Dedukti.print - 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 () = - (* SmtSolver.Proof.learn (SmtSolver.history ()); *) - 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_proof = Dot.print end diff --git a/smt/smt.ml b/smt/smt.ml index 27bbe374..873cfcf4 100644 --- a/smt/smt.ml +++ b/smt/smt.ml @@ -63,7 +63,6 @@ module Make(Dummy:sig end) = struct include Solver.Make(Fsmt)(Tsmt)(struct end) 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) @@ -75,6 +74,6 @@ module Make(Dummy:sig end) = struct let print_clause = St.print_clause let print_dot = Dot.print - let print_dedulti = Dedukti.print + let print_dedukti = Dedukti.print end diff --git a/solver/external.ml b/solver/external.ml new file mode 100644 index 00000000..c5c49729 --- /dev/null +++ b/solver/external.ml @@ -0,0 +1,60 @@ +(* +MSAT is free software, using the Apache license, see file LICENSE +Copyright 2016 Guillaume Bury +Copyright 2016 Simon Cruanes +*) + +module type S = Solver_intf.S + +module Make + (St : Solver_types.S) + (Th : Plugin_intf.S with type term = St.term + and type formula = St.formula + and type proof = St.proof) + (Dummy : sig end) = struct + + module St = St + + module S = Internal.Make(St)(Th)(struct end) + + module Proof = S.Proof + + exception UndecidedLit = S.UndecidedLit + + type atom = St.formula + 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 + +end diff --git a/solver/external.mli b/solver/external.mli new file mode 100644 index 00000000..7edc9f9c --- /dev/null +++ b/solver/external.mli @@ -0,0 +1,17 @@ +(* +MSAT is free software, using the Apache license, see file LICENSE +Copyright 2014 Guillaume Bury +Copyright 2014 Simon Cruanes +*) + +module type S = Solver_intf.S + +module Make + (St : Solver_types.S) + (Th : Plugin_intf.S with type term = St.term + and type formula = St.formula + and type proof = St.proof) + (Dummy : sig end) : + S with module St = St + + diff --git a/solver/internal.ml b/solver/internal.ml index 9a98b2bb..74b42d89 100644 --- a/solver/internal.ml +++ b/solver/internal.ml @@ -219,8 +219,10 @@ module Make let f_weight i j = get_elt_weight (St.get_elt j) < get_elt_weight (St.get_elt i) + (* let f_filter i = get_elt_level (St.get_elt i) < 0 + *) (* Var/clause activity *) let insert_var_order = function @@ -275,7 +277,6 @@ module Make let decision_level () = Vec.size env.elt_levels let nb_clauses () = Vec.size env.clauses_hyps - let nb_learnts () = Vec.size env.clauses_learnt let nb_vars () = St.nb_elt () (* Simplify clauses *) @@ -851,6 +852,7 @@ module Make Vec.shrink env.learnts (lim2 - !j) *) +(* (* remove from [vec] the clauses that are satisfied in the current trail *) let remove_satisfied vec = for i = 0 to Vec.size vec - 1 do @@ -858,7 +860,6 @@ module Make if satisfied c then remove_clause c done -(* let simplify () = assert (decision_level () = 0); if is_unsat () then raise Unsat; diff --git a/solver/mcsolver.ml b/solver/mcsolver.ml index fd1bcb45..a0d7f62a 100644 --- a/solver/mcsolver.ml +++ b/solver/mcsolver.ml @@ -4,17 +4,16 @@ Copyright 2014 Guillaume Bury Copyright 2014 Simon Cruanes *) +module type S = Solver_intf.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) - (Dummy: sig end) = struct + (Th : Plugin_intf.S with type term = E.Term.t + and type formula = E.Formula.t + and type proof = E.proof) + (Dummy: sig end) = + External.Make + (Solver_types.McMake(E)(struct end)) + (Th) + (struct end) - module St = Solver_types.McMake(E)(struct end) - - module M = Internal.Make(St)(Th)(struct end) - - include St - - include M - -end diff --git a/solver/mcsolver.mli b/solver/mcsolver.mli index 1bcc48d0..8e16f22b 100644 --- a/solver/mcsolver.mli +++ b/solver/mcsolver.mli @@ -4,66 +4,15 @@ Copyright 2014 Guillaume Bury Copyright 2014 Simon Cruanes *) +module type S = Solver_intf.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) - (Dummy: sig end) : sig - (** Functor to create a solver parametrised by the atomic formulas and a theory. *) - - exception Unsat - - module St : Solver_types.S - with type term = E.Term.t - and type formula = E.Formula.t - and type proof = E.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 -> E.Formula.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 eval : E.Formula.t -> bool - (** Returns the valuation of a formula in the current state - of the sat solver. *) - - 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]) *) - - val model : unit -> (St.term * St.term) list - (** Returns the model found if the formula is satisfiable. *) - - 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 + (Th : Plugin_intf.S with type term = E.Term.t + and type formula = E.Formula.t + and type proof = E.proof) + (Dummy: sig end) : + S with type St.term = E.Term.t + and type St.formula = E.Formula.t + and type St.proof = E.proof +(** Functor to create a solver parametrised by the atomic formulas and a theory. *) diff --git a/solver/solver.ml b/solver/solver.ml index 30bb8b1a..3a34f089 100644 --- a/solver/solver.ml +++ b/solver/solver.ml @@ -100,53 +100,10 @@ end module Make (E : Formula_intf.S) (Th : Theory_intf.S with type formula = E.t and type proof = E.proof) - (Dummy: sig end) = struct + (Dummy: sig end) = + External.Make + (Solver_types.SatMake(E)(struct end)) + (Plugin(E)(Th)) + (struct end) - module P = Plugin(E)(Th) - - module St = Solver_types.SatMake(E)(struct end) - - module S = Internal.Make(St)(P)(struct end) - - 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 - -end diff --git a/solver/solver.mli b/solver/solver.mli index e9e1ab7f..17a25f31 100644 --- a/solver/solver.mli +++ b/solver/solver.mli @@ -8,10 +8,12 @@ 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) : - Theory_intf.S with type formula = F.t and type proof = F.proof + Theory_intf.S with type formula = F.t + and type proof = F.proof module Make (F : Formula_intf.S) - (Th : Theory_intf.S with type formula = F.t and type proof = F.proof) + (Th : Theory_intf.S with type formula = F.t + and type proof = F.proof) (Dummy: sig end) : S with type St.formula = F.t and type St.proof = F.proof