Res now includes solver type

_tags

@@ -13,5 +13,6 @@
 
 # more warnings
 <**/*.ml>: warn_K, warn_Y, warn_X
+<**/*.ml>: keep_locks, short_paths, safe_string, strict_sequence
 <**/*.cm*>: debug
 

backend/dedukti.ml

@@ -1,26 +1,44 @@
 (*
 MSAT is free software, using the Apache license, see file LICENSE
-Copyright 2014 Guillaume Bury
+Copyright 2015 Guillaume Bury
-Copyright 2014 Simon Cruanes
 *)
 
 module type S = Backend_intf.S
 
 module type Arg = sig
+
   type proof
+  type lemma
   type formula
-  val prove : Format.formatter -> formula list -> unit
+
+  val print : Format.formatter -> formula -> unit
+  val prove : Format.formatter -> lemma -> unit
   val context : Format.formatter -> proof -> unit
-  val translate : Format.formatter -> formula -> unit
 end
 
-module Make(S : Res.S)(A : Arg with type formula := S.atom and type proof := S.proof) = struct
+module Make(S : Res.S)(A : Arg with type formula := S.St.formula and type proof := S.proof) = struct
 
-  let print_aux fmt = Format.fprintf fmt "@\n"
+  let pp_nl fmt = Format.fprintf fmt "@\n"
+  let fprintf fmt format = Format.kfprintf pp_nl fmt format
 
-  let fprintf fmt format = Format.kfprintf print_aux fmt format
+  let clause_name c = S.St.(c.name)
 
-  let context fmt () =
+  let pp_clause fmt c =
+    let rec aux fmt = function
+      | [] -> ()
+      | a :: r ->
+        let f, pos =
+          if S.St.(a.var.pa == a) then
+            S.St.(a.lit), true
+          else
+            S.St.(a.neg.lit), false
+        in
+        fprintf fmt "%s _b %a ->@ %a"
+          (if pos then "_pos" else "_neg") A.print f aux r
+    in
+    fprintf fmt "_b : Prop ->@ %a ->@ _proof _b" aux (S.to_list c)
+
+  let context fmt p =
     fprintf fmt "(; Embedding ;)";
     fprintf fmt "Prop : Type.";
     fprintf fmt "_proof : Prop -> Type.";
@@ -28,10 +46,13 @@ module Make(S : Res.S)(A : Arg with type formula := S.atom and type proof := S.p
     fprintf fmt "_pos : Prop -> Prop -> Type.";
     fprintf fmt "_neg : Prop -> Prop -> Type.";
     fprintf fmt "[b: Prop, p: Prop] _pos b p --> _proof p -> _proof b.";
-    fprintf fmt "[b: Prop, p: Prop] _neg b p --> _pos b p -> _proof b."
+    fprintf fmt "[b: Prop, p: Prop] _neg b p --> _pos b p -> _proof b.";
+    A.context fmt p
 
-  let print fmt _ =
+  let print fmt p =
-    context fmt ();
+    fprintf fmt "#NAME Proof.";
+    fprintf fmt "(; Dedukti file automatically generated by mSAT ;)";
+    context fmt p;
     ()
 
 end

backend/dedukti.mli

@@ -2,15 +2,18 @@
 module type S = Backend_intf.S
 
 module type Arg = sig
+
+  type lemma
   type proof
   type formula
-  val prove : Format.formatter -> formula list -> unit
+
+  val print : Format.formatter -> formula -> unit
+  val prove : Format.formatter -> lemma -> unit
   val context : Format.formatter -> proof -> unit
-  val translate : Format.formatter -> formula -> unit
 end
 
 module Make :
   functor(S : Res.S) ->
-  functor(A : Arg with type formula := S.atom and type proof := S.proof) ->
+  functor(A : Arg with type formula := S.St.formula and type proof := S.proof) ->
     S with type t := S.proof
 (** Functor to generate a backend to output proofs for the dedukti type checker. *)

backend/dot.ml

@@ -2,18 +2,17 @@
 module type S = Backend_intf.S
 
 module type Arg = sig
+
   type atom
-  type clause
   type lemma
 
-  val clause_name : clause -> string
   val print_atom : Format.formatter -> atom -> unit
   val lemma_info : lemma -> string * string option * (Format.formatter -> unit -> unit) list
 end
 
-module Make(S : Res.S)(A : Arg with type atom := S.atom and type clause := S.clause and type lemma := S.lemma) = struct
+module Make(S : Res.S)(A : Arg with type atom := S.atom and type lemma := S.lemma) = struct
 
-  let node_id n = A.clause_name S.(n.conclusion)
+  let node_id n = n.S.conclusion.S.St.name
 
   let res_node_id n = (node_id n) ^ "_res"
 
@@ -55,14 +54,14 @@ module Make(S : Res.S)(A : Arg with type atom := S.atom and type clause := S.cla
     match S.(n.step) with
     | S.Hypothesis ->
       print_dot_node fmt (node_id n) "LIGHTBLUE" S.(n.conclusion) "Hypothesis" "LIGHTBLUE"
-        [(fun fmt () -> (Format.fprintf fmt "%s" (A.clause_name n.S.conclusion)))];
+        [(fun fmt () -> (Format.fprintf fmt "%s" (node_id n)))];
     | S.Lemma lemma ->
       let rule, color, l = A.lemma_info lemma in
       let color = match color with None -> "YELLOW" | Some c -> c in
       print_dot_node fmt (node_id n) "LIGHTBLUE" S.(n.conclusion) rule color l
     | S.Resolution (_, _, a) ->
       print_dot_node fmt (node_id n) "GREY" S.(n.conclusion) "Resolution" "GREY"
-        [(fun fmt () -> (Format.fprintf fmt "%s" (A.clause_name n.S.conclusion)))];
+        [(fun fmt () -> (Format.fprintf fmt "%s" (node_id n)))];
       print_dot_res_node fmt (res_node_id n) a;
       print_edge fmt (node_id n) (res_node_id n)
 

backend/dot.mli

@@ -3,14 +3,12 @@ module type S = Backend_intf.S
 
 module type Arg = sig
   type atom
-  type clause
   type lemma
 
-  val clause_name : clause -> string
   val print_atom : Format.formatter -> atom -> unit
   val lemma_info : lemma -> string * string option * (Format.formatter -> unit -> unit) list
 end
 
-module Make(S : Res.S)(A : Arg with type atom := S.atom and type clause := S.clause and type lemma := S.lemma) :
+module Make(S : Res.S)(A : Arg with type atom := S.atom and type lemma := S.lemma) :
   S with type t := S.proof
 

smt/mcsat.ml

@@ -112,7 +112,6 @@ module Make(Dummy:sig end) = struct
 
   module SmtSolver = Mcsolver.Make(Log)(Fsmt)(Tsmt)
   module Dot = Dot.Make(SmtSolver.Proof)(struct
-      let clause_name c = SmtSolver.St.(c.name)
       let print_atom = SmtSolver.St.print_atom
       let lemma_info () = "Proof", Some "PURPLE", []
     end)

solver/internal.mli

@@ -10,10 +10,7 @@ module Make (L : Log_intf.S)(St : Solver_types.S)
 
   exception Unsat
 
-  module Proof : Res.S
+  module Proof : Res.S with module St = St
-    with type atom = St.atom
-     and type clause = St.clause
-     and type lemma = Th.proof
 
   val solve : unit -> unit
   (** Try and solves the current set of assumptions.

solver/mcsolver.mli

@@ -13,11 +13,10 @@ module Make (L : Log_intf.S)(E : Expr_intf.S)
   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 type atom = St.atom
+    with module St = St
-     and type clause = St.clause
-     and type lemma = Th.proof
 
   val solve : unit -> unit
   (** Try and solves the current set of assumptions.

solver/res.ml

@@ -8,6 +8,8 @@ module type S = Res_intf.S
 
 module Make(L : Log_intf.S)(St : Solver_types.S) = struct
 
+  module St = St
+
   (* Type definitions *)
   type lemma = St.proof
   type clause = St.clause

solver/res.mli

@@ -8,6 +8,5 @@ module type S = Res_intf.S
 
 module Make :
   functor (L : Log_intf.S) ->
-  functor (St : Solver_types.S) ->
+  functor (St : Solver_types.S) -> S with module St = St
-    S with type atom = St.atom and type clause = St.clause and type lemma = St.proof
 (** Functor to create a module building proofs from a sat-solver unsat trace. *)

solver/res_intf.ml

@@ -7,14 +7,17 @@ Copyright 2014 Simon Cruanes
 module type S = sig
   (** Signature for a module handling proof by resolution from sat solving traces *)
 
+  module St : Solver_types.S
+  (** Module defining atom and clauses *)
+
   (** {3 Type declarations} *)
 
   exception Insuficient_hyps
   (** Raised when a complete resolution derivation cannot be found using the current hypotheses. *)
 
-  type atom
+  type atom = St.atom
-  type clause
+  type clause = St.clause
-  type lemma
+  type lemma = St.proof
   (** Abstract types for atoms, clauses and theory-specific lemmas *)
 
   type proof

solver/solver.mli

@@ -22,10 +22,7 @@ module Make (L : Log_intf.S)(F : Formula_intf.S)
     with type formula = F.t
      and type proof = F.proof
 
-  module Proof : Res.S
+  module Proof : Res.S with module St = St
-    with type atom = St.atom
-     and type clause = St.clause
-     and type lemma = Th.proof
 
   val solve : unit -> unit
   (** Try and solves the current set of assumptions.

solver/solver_types.ml

@@ -349,7 +349,6 @@ module SatMake (L : Log_intf.S)(E : Formula_intf.S) = struct
     | Lemma of proof
     | History of clause list
 
-  (* Flag for Mcsat v.s Pure Sat *)
   (* Flag for Mcsat v.s Pure Sat *)
   let mcsat = false
 

tests/run

@@ -7,7 +7,7 @@ solvertest () {
     for f in `find -L $1 -type f -name '*.cnf' -o -name '*.smt2'`
     do
         echo -ne "\r\033[KTesting $f..."
-        "$SOLVER" -s $3 -check -time 30s -size 1G $f | grep $2
+        "$SOLVER" -s $3 -time 30s -size 1G $f | grep $2
         RET=$?
         if [ $RET -ne 0 ];
         then

util/log.ml

@@ -44,5 +44,5 @@ let on_buffer pp x =
   Buffer.contents buf
 
 let on_fmt pp x =
-  pp Format.str_formatter x;
+  let _ = pp Format.str_formatter x in
   Format.flush_str_formatter ()