Fixed compilation. Refactored some code in external

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 "[]"

msat.mlpack

@@ -13,6 +13,7 @@ Solver_types_intf
 
 # Solver Modules
 Internal
+External
 Solver
 Mcsolver
 Solver_types

msat.odocl

@@ -10,6 +10,7 @@ solver/Solver_types_intf
 solver/Solver_intf
 
 solver/Internal
+solver/External
 solver/Solver
 solver/Mcsolver
 solver/Solver_types

smt/mcsat.ml

@@ -111,49 +111,19 @@ end
 
 module Make(Dummy:sig end) = struct
 
-  module SmtSolver = Mcsolver.Make(Fsmt)(Tsmt)(struct end)
+  include Mcsolver.Make(Fsmt)(Tsmt)(struct end)
-
+  module Dot = Dot.Make(Proof)(struct
-  module Proof = SmtSolver.Proof
+      let print_atom = St.print_atom
-
-  module Dot = Dot.Make(SmtSolver.Proof)(struct
-      let print_atom = SmtSolver.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

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

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

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
+
+

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;

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)
+    (Th : Plugin_intf.S with type term = E.Term.t
-    (Dummy: sig end) = struct
+                         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
 

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)
+    (Th : Plugin_intf.S with type term = E.Term.t
-    (Dummy: sig end) : sig
+                         and type formula = E.Formula.t
-  (** Functor to create a solver parametrised by the atomic formulas and a theory. *)
+                         and type proof = E.proof)
-
+    (Dummy: sig end) :
-  exception Unsat
+  S with type St.term = E.Term.t
-
+     and type St.formula = E.Formula.t
-  module St : Solver_types.S
+     and type St.proof = E.proof
-    with type term = E.Term.t
+(** Functor to create a solver parametrised by the atomic formulas and a theory. *)
-     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
 

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
 

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