Mcsat now works

Makefile

@@ -5,7 +5,7 @@ COMP=ocamlbuild -log $(LOG) -use-ocamlfind -classic-display
 FLAGS=
 DIRS=-Is solver,sat,smt,util,util/smtlib
 DOC=msat.docdir/index.html
-TEST=sat_solve.native bench_stats.native
+TEST=sat_solve.native mcsat_solve.native
 
 NAME=msat
 

msat.mlpack

@@ -3,8 +3,6 @@ Formula_intf
 Solver
 Solver_types
 Theory_intf
-
-# Mcsat Solver modules
 Expr_intf
 Mcsolver
 Mcsolver_types
@@ -16,10 +14,11 @@ Mcproof
 Tseitin
 Tseitin_intf
 
-# Sat modules
+# Sat/Smt modules
+Expr
+Cnf
 Sat
-
-# Smt Modules
+Mcsat
 Cc
 Sig
 Smt

smt/.merlin

@@ -1,8 +1,10 @@
 S ./
 S ../sat/
 S ../util/
+S ../solver/
 
 B ../_build/
 B ../_build/sat/
 B ../_build/smt/
 B ../_build/util/
+B ../_build/solver/

smt/cc.ml

@@ -23,6 +23,8 @@ module Make(T : Sig.OrderedType) = struct
         size = M.empty;
     }
 
+    let repr t a = U.find t.repr a
+
     let map_find m v default = try M.find v m with Not_found -> default
     let find_parent v m = map_find m v v
 
@@ -87,5 +89,11 @@ module Make(T : Sig.OrderedType) = struct
         with U.Unsat (a, b) ->
             raise (Unsat (a, b, expl t a b))
 
+    let are_neq t a b =
+        try
+            ignore (U.union t.repr a b);
+            false
+        with U.Unsat _ ->
+            true
 
 end

smt/cc.mli

@@ -12,4 +12,7 @@ module Make(T : Sig.OrderedType) : sig
     val empty : t
     val add_eq : t -> T.t -> T.t -> t
     val add_neq : t -> T.t -> T.t -> t
+
+    val repr : t -> T.t -> T.t
+    val are_neq : t -> T.t -> T.t -> bool
 end

smt/cnf.ml

@@ -0,0 +1,7 @@
+(*
+MSAT is free software, using the Apache license, see file LICENSE
+Copyright 2014 Guillaume Bury
+Copyright 2014 Simon Cruanes
+*)
+
+module S = Tseitin.Make(Expr)

smt/cnf.mli

@@ -0,0 +1,7 @@
+(*
+MSAT is free software, using the Apache license, see file LICENSE
+Copyright 2014 Guillaume Bury
+Copyright 2014 Simon Cruanes
+*)
+
+module S : Tseitin.S with type atom = Expr.Formula.t

smt/expr.ml

@@ -0,0 +1,73 @@
+(*
+MSAT is free software, using the Apache license, see file LICENSE
+Copyright 2014 Guillaume Bury
+Copyright 2014 Simon Cruanes
+*)
+
+exception Invalid_var
+
+type var = string
+type formula =
+    | Prop of int
+    | Equal of var * var
+    | Distinct of var * var
+type t = formula
+
+let dummy = Prop 0
+
+let max_fresh = ref 0
+let fresh () =
+    incr max_fresh;
+  Prop (2 * !max_fresh + 1)
+
+let mk_prop i =
+    if i <> 0 && i < max_int / 2 then Prop (2 * i)
+    else raise Invalid_var
+
+let mk_var i =
+    if i <> "" then i
+    else raise Invalid_var
+
+let mk_eq i j = Equal (mk_var (min i j), mk_var (max i j))
+let mk_neq i j = Distinct (mk_var (min i j), mk_var (max i j))
+
+let neg = function
+  | Prop i -> Prop (-i)
+  | Equal (a, b) -> Distinct (a, b)
+  | Distinct (a, b) -> Equal (a, b)
+
+let norm = function
+  | Prop i -> Prop (abs i), i < 0
+  | Equal (a, b) -> Equal (a, b), false
+  | Distinct (a, b) -> Equal (a, b), true
+
+  (* Only used after normalisation, so usual functions should work *)
+let hash = Hashtbl.hash
+let equal = (=)
+let compare = Pervasives.compare
+
+let s = Hstring.make ""
+let label _ = s
+let add_label _ _ = ()
+
+let print fmt = function
+  | Prop i -> Format.fprintf fmt "%s%s%d" (if i < 0 then "¬ " else "") (if i mod 2 = 0 then "v" else "f") ((abs i) / 2)
+  | Equal (a, b) -> Format.fprintf fmt "%s = %s" a b
+  | Distinct (a, b) -> Format.fprintf fmt "%s ≠ %s" a b
+
+module Term = struct
+  type t = var
+  let hash = Hashtbl.hash
+  let equal = (=)
+  let compare = Pervasives.compare
+  let print fmt t = Format.fprintf fmt "%s" t
+end
+
+module Formula = struct
+  type t = formula
+  let hash = Hashtbl.hash
+  let equal = (=)
+  let compare = Pervasives.compare
+  let print = print
+end
+

smt/mcsat.ml

@@ -0,0 +1,145 @@
+(*
+MSAT is free software, using the Apache license, see file LICENSE
+Copyright 2014 Guillaume Bury
+Copyright 2014 Simon Cruanes
+*)
+
+module Fsmt = Expr
+
+module Tsmt = struct
+
+  module M = Map.Make(Fsmt.Term)
+  module CC = Cc.Make(String)
+
+  (* Type definitions *)
+  type term = Fsmt.var
+  type formula = Fsmt.t
+
+  type proof = unit
+
+  type assumption =
+    | Lit of formula
+    | Assign of term * term
+
+  type slice = {
+    start : int;
+    length : int;
+    get : int -> assumption * int;
+    push : formula list -> proof -> unit;
+  }
+
+  type level = {
+      cc : CC.t;
+      assign : (term * int) M.t;
+  }
+
+  type res =
+    | Sat of level
+    | Unsat of formula list * proof
+
+  type eval_res =
+    | Valued of bool * int
+    | Unknown
+
+  (* Functions *)
+  let dummy = { cc = CC.empty; assign = M.empty; }
+
+  let env = ref dummy
+
+  let current_level () = !env
+
+  let to_clause (a, b, l) =
+      Log.debug 10 "Expl : %s; %s" a b;
+      List.iter (fun s -> Log.debug 10 " |- %s" s) l;
+      let rec aux acc = function
+          | [] | [_] -> acc
+          | x :: ((y :: _) as r) ->
+                  aux (Fsmt.mk_eq x y :: acc) r
+      in
+      (Fsmt.mk_eq a b) :: (List.rev_map Fsmt.neg (aux [] l))
+
+  let assume s =
+      try
+          for i = s.start to s.start + s.length - 1 do
+              match s.get i with
+              | (Assign (x, v)), lvl ->
+                      env := { !env with assign = M.add x (v, lvl) !env.assign }
+              | Lit f, _ ->
+                Log.debug 10 "Propagating in th : %s" (Log.on_fmt Fsmt.print f);
+                match f with
+                | Fsmt.Prop _ -> ()
+                | Fsmt.Equal (i, j) ->
+                  env := { !env with cc = CC.add_eq !env.cc i j }
+                | Fsmt.Distinct (i, j) ->
+                  env := { !env with cc = CC.add_neq !env.cc i j }
+                | _ -> assert false
+          done;
+          Sat (current_level ())
+      with CC.Unsat x ->
+        Log.debug 8 "Making explanation clause...";
+        Unsat (to_clause x, ())
+
+  let backtrack l = env := l
+
+  let assign t = CC.repr !env.cc t
+
+  let iter_assignable f = function
+      | Fsmt.Prop _ -> ()
+      | Fsmt.Equal(a, b)
+      | Fsmt.Distinct (a, b) -> f a; f b
+
+  let eval = function
+      | Fsmt.Prop _ -> Unknown
+      | Fsmt.Equal (a, b) ->
+              begin try
+                  let a', lvl_a = M.find a !env.assign in
+                  let b', lvl_b = M.find b !env.assign in
+                  Valued (Fsmt.Term.equal a' b', max lvl_a lvl_b)
+              with Not_found -> Unknown end
+      | Fsmt.Distinct (a, b) ->
+              begin try
+                  let a', lvl_a = M.find a !env.assign in
+                  let b', lvl_b = M.find b !env.assign in
+                  Valued (not (Fsmt.Term.equal a' b'), max lvl_a lvl_b)
+              with Not_found -> Unknown end
+
+end
+
+module Make(Dummy:sig end) = struct
+  module SmtSolver = Mcsolver.Make(Fsmt)(Tsmt)
+
+  type atom = Fsmt.t
+  type clause = SmtSolver.St.clause
+  type proof = SmtSolver.Proof.proof
+
+  type res =
+    | Sat
+    | Unsat
+
+  let _i = ref 0
+  let solve () =
+    try
+      SmtSolver.solve ();
+      Sat
+    with SmtSolver.Unsat -> Unsat
+
+  let assume l =
+    incr _i;
+    try
+      SmtSolver.assume l !_i
+    with SmtSolver.Unsat -> ()
+
+  let get_proof () =
+    SmtSolver.Proof.learn (SmtSolver.history ());
+    match SmtSolver.unsat_conflict () with
+    | None -> assert false
+    | Some c -> SmtSolver.Proof.prove_unsat c
+
+  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 = SmtSolver.Proof.print_dot
+end

smt/smt.ml

@@ -4,61 +4,7 @@ Copyright 2014 Guillaume Bury
 Copyright 2014 Simon Cruanes
 *)
 
-module Fsmt = struct
-
-  exception Invalid_var
-
-  type var = string
-  type t =
-    | Prop of int
-    | Equal of var * var
-    | Distinct of var * var
-
-  let dummy = Prop 0
-
-  let max_fresh = ref 0
-  let fresh () =
-    incr max_fresh;
-    Prop (2 * !max_fresh + 1)
-
-  let mk_prop i =
-      if i <> 0 && i < max_int / 2 then Prop (2 * i)
-      else raise Invalid_var
-
-  let mk_var i =
-    if i <> "" then i
-    else raise Invalid_var
-
-  let mk_eq i j = Equal (mk_var (min i j), mk_var (max i j))
-  let mk_neq i j = Distinct (mk_var (min i j), mk_var (max i j))
-
-  let neg = function
-    | Prop i -> Prop (-i)
-    | Equal (a, b) -> Distinct (a, b)
-    | Distinct (a, b) -> Equal (a, b)
-
-  let norm = function
-    | Prop i -> Prop (abs i), i < 0
-    | Equal (a, b) -> Equal (a, b), false
-    | Distinct (a, b) -> Equal (a, b), true
-
-  (* Only used after normalisation, so usual functions should work *)
-  let hash = Hashtbl.hash
-  let equal = (=)
-  let compare = Pervasives.compare
-
-  let s = Hstring.make ""
-  let label _ = s
-  let add_label _ _ = ()
-
-  let print fmt = function
-    | Prop i -> Format.fprintf fmt "%s%s%d" (if i < 0 then "¬ " else "") (if i mod 2 = 0 then "v" else "f") ((abs i) / 2)
-    | Equal (a, b) -> Format.fprintf fmt "%s = %s" a b
-    | Distinct (a, b) -> Format.fprintf fmt "%s ≠ %s" a b
-
-end
-
-module Tseitin = Tseitin.Make(Fsmt)
+module Fsmt = Expr
 
 module Tsmt = struct
 

smt/smt.mli

@@ -4,19 +4,10 @@ Copyright 2014 Guillaume Bury
 Copyright 2014 Simon Cruanes
 *)
 
-module Fsmt : sig
-    include Formula_intf.S
-    val mk_prop : int -> t
-    val mk_eq : string -> string -> t
-    val mk_neq : string -> string -> t
-end
-
-module Tseitin : Tseitin.S with type atom = Fsmt.t
-
 module Make(Dummy: sig end) : sig
   (** Fonctor to make a pure SAT Solver module with built-in literals. *)
 
-  type atom = Fsmt.t
+  type atom = Expr.Formula.t
   (** Type for atoms, i.e boolean literals. *)
 
   type clause

solver/mcsolver.ml

@@ -178,12 +178,12 @@ module Make (E : Expr_intf.S)
     get_elt_level (St.get_var i) < 0
 
   (* Var/clause activity *)
-  let rec insert_var_order e = Either.destruct e
+  let insert_var_order e = Either.destruct e
       (fun v -> Iheap.insert f_weight env.order v.vid)
       (fun v ->
           Iheap.insert f_weight env.order v.vid;
-          Th.iter_assignable (fun t ->
-              insert_var_order (Either.mk_left (St.add_term t))) v.tag.pa.lit)
+          Th.iter_assignable (fun t -> Iheap.insert f_weight env.order (St.add_term t).vid) v.tag.pa.lit
+      )
 
   let var_decay_activity () =
     env.var_inc <- env.var_inc *. env.var_decay
@@ -191,7 +191,7 @@ module Make (E : Expr_intf.S)
   let clause_decay_activity () =
     env.clause_inc <- env.clause_inc *. env.clause_decay
 
-  let var_bump_activity v =
+  let var_bump_activity_aux v =
     v.weight <- v.weight +. env.var_inc;
     if v.weight > 1e100 then begin
       for i = 0 to (St.nb_vars ()) - 1 do
@@ -202,6 +202,10 @@ module Make (E : Expr_intf.S)
     if Iheap.in_heap env.order v.vid then
       Iheap.decrease f_weight env.order v.vid
 
+  let var_bump_activity v =
+      var_bump_activity_aux v;
+      Th.iter_assignable (fun t -> var_bump_activity_aux (St.add_term t)) v.tag.pa.lit
+
   let clause_bump_activity c =
     c.activity <- c.activity +. env.clause_inc;
     if c.activity > 1e20 then begin
@@ -259,16 +263,21 @@ module Make (E : Expr_intf.S)
     if decision_level () > lvl then begin
       env.qhead <- Vec.get env.trail_lim lvl;
       env.tatoms_qhead <- env.qhead;
-      for c = Vec.size env.trail - 1 downto env.qhead do
+      for c = env.qhead to Vec.size env.trail - 1 do
         Either.destruct (Vec.get env.trail c)
         (fun a -> ())
         (fun a ->
-          a.is_true <- false;
-          a.neg.is_true <- false;
-          a.var.level <- -1;
-          a.var.tag.reason <- Bcp None;
-          a.var.tag.vpremise <- History [];
-          insert_var_order (Either.mk_right a.var))
+            if a.var.level <= lvl then begin
+              Vec.set env.trail env.qhead (Either.mk_right a);
+              env.qhead <- env.qhead + 1
+            end else begin
+              a.is_true <- false;
+              a.neg.is_true <- false;
+              a.var.level <- -1;
+              a.var.tag.reason <- Bcp None;
+              a.var.tag.vpremise <- History [];
+              insert_var_order (Either.mk_right a.var)
+            end)
       done;
       Th.backtrack (Vec.get env.tenv_queue lvl); (* recover the right tenv *)
       Vec.shrink env.trail ((Vec.size env.trail) - env.qhead);
@@ -286,9 +295,6 @@ module Make (E : Expr_intf.S)
   let enqueue_bool a lvl reason =
     assert (not a.is_true && not a.neg.is_true && a.var.level < 0
             && a.var.tag.reason = Bcp None && lvl >= 0);
-    assert (lvl = decision_level ());
-    (* keep the reason for proof/unsat-core *)
-    (*let reason = if lvl = 0 then None else reason in*)
     a.is_true <- true;
     a.var.level <- lvl;
     a.var.tag.reason <- reason;
@@ -299,7 +305,8 @@ module Make (E : Expr_intf.S)
     v.tag.assigned <- Some value;
     v.level <- lvl;
     Log.debug 5 "Enqueue: %a" St.pp_semantic_var v;
-    Vec.push env.trail (Either.mk_left v)
+    Vec.push env.trail (Either.mk_left v);
+    Log.debug 15 "Done."
 
   (* conflict analysis *)
   let max_lvl_atoms l =
@@ -308,42 +315,65 @@ module Make (E : Expr_intf.S)
           else if a.var.level > max_lvl then (a.var.level, [a])
           else (max_lvl, acc)) (0, []) l
 
+  let backtrack_lvl is_uip = function
+    | [] -> 0
+    | a :: r when not is_uip -> a.var.level - 1
+    | a :: r ->
+            let rec aux = function
+                | [] -> 0
+                | b :: r when b.var.level <> a.var.level -> b.var.level
+                | _ :: r -> aux r
+            in
+            aux r
+
   let analyze c_clause =
     let tr_ind  = ref (Vec.size env.trail) in
-    let blevel  = ref 0 in
     let is_uip  = ref false in
     let c       = ref (Proof.to_list c_clause) in
-    let history = ref [] in
-
+    let history = ref [c_clause] in
+    clause_bump_activity c_clause;
     let is_semantic a = match a.var.tag.reason with
         | Semantic _ -> true
         | _ -> false
     in
-
     try while true do
         let l, atoms = max_lvl_atoms !c in
+        Log.debug 15 "Current conflict clause :";
+        List.iter (fun a -> Log.debug 15 " |- %a" St.pp_atom a) !c;
         match atoms with
         | [] |  _ :: [] ->
-                blevel := -1;
+                Log.debug 15 "Found UIP clause";
+                is_uip := true;
                 raise Exit
         | _ when List.for_all is_semantic atoms ->
-                blevel := l - 1;
+                Log.debug 15 "Found Semantic backtrack clause";
                 raise Exit
         | _ ->
                 decr tr_ind;
+                Log.debug 20 "Looking at trail element %d" !tr_ind;
                 Either.destruct (Vec.get env.trail !tr_ind)
-                (fun v -> ())
+                (fun v -> Log.debug 15 "%a" St.pp_semantic_var v)
                 (fun a -> match a.var.tag.reason with
                     | Bcp (Some d) ->
+                            Log.debug 15 "Propagation : %a" St.pp_atom a;
+                            Log.debug 15 " |- %a" St.pp_clause d;
                             let tmp, res = Proof.resolve (Proof.merge !c (Proof.to_list d)) in
                             begin match tmp with
-                            | [b] when b == a.neg -> c := !c
-                            | _ -> ()
+                            | [] -> Log.debug 15 "No lit to resolve over."
+                            | [b] when b == a.var.tag.pa ->
+                                    clause_bump_activity d;
+                                    var_bump_activity a.var;
+                                    history := d :: !history;
+                                    c := res
+                            | _ -> assert false
                             end
-                    | _ -> ())
+                    | _ -> Log.debug 15 "Decision : %a" St.pp_atom a)
     done; assert false
     with Exit ->
-      !blevel, !c, !history, !is_uip
+      let learnt = List.sort (fun a b -> Pervasives.compare b.var.level a.var.level) !c in
+      let blevel = backtrack_lvl !is_uip learnt in
+      blevel, learnt, !history, !is_uip
+
     (*
     while !cond do
       if !c.learnt then clause_bump_activity !c;
@@ -439,7 +469,7 @@ module Make (E : Expr_intf.S)
   let partition atoms init0 =
     let rec partition_aux trues unassigned falses init = function
       | [] -> trues @ unassigned @ falses, init
-      | a::r ->
+      | a :: r ->
         if a.is_true then
           if a.var.level = 0 then raise Trivial
           else (a::trues) @ unassigned @ falses @ r, init
@@ -574,8 +604,8 @@ module Make (E : Expr_intf.S)
   (* Propagation (boolean and theory *)
   let _th_cnumber = ref 0
   let slice_get i = Either.destruct (Vec.get env.trail i)
-    (function {tag={term; assigned = Some v}} -> Th.Assign (term, v) | _ -> assert false)
-    (fun a -> Th.Lit a.lit)
+      (function {level; tag={term; assigned = Some v}} -> Th.Assign (term, v), level | _ -> assert false)
+      (fun a -> Th.Lit a.lit, a.var.level)
 
   let slice_push l lemma =
     decr _th_cnumber;
@@ -612,9 +642,9 @@ module Make (E : Expr_intf.S)
         Either.destruct (Vec.get env.trail env.qhead)
         (fun a -> ())
         (fun a ->
-          env.qhead <- env.qhead + 1;
           incr num_props;
-          propagate_atom a res)
+          propagate_atom a res);
+        env.qhead <- env.qhead + 1
       done;
       env.propagations <- env.propagations + !num_props;
       env.simpDB_props <- env.simpDB_props - !num_props;
@@ -797,9 +827,12 @@ module Make (E : Expr_intf.S)
     Vec.grow_to_by_double env.clauses nbc;
     Vec.grow_to_by_double env.learnts nbc;
     env.nb_init_clauses <- nbc;
+    St.iter_vars (fun e -> Either.destruct e
+        (fun v -> Log.debug 50 " -- %a" St.pp_semantic_var v)
+        (fun a -> Log.debug 50 " -- %a" St.pp_atom a.tag.pa)
+    );
     add_clauses cnf ~cnumber
 
-
   let assume cnf ~cnumber =
     let cnf = List.rev_map (List.rev_map St.add_atom) cnf in
     init_solver cnf ~cnumber

solver/mcsolver.mli

@@ -20,12 +20,10 @@ module Make (E : Expr_intf.S)
   module St : Mcsolver_types.S
     with type formula = E.Formula.t
 
-  (*
   module Proof : Res.S
     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_types.ml

@@ -15,7 +15,8 @@ open Printf
 
 module type S = Mcsolver_types_intf.S
 
-module Make (E : Expr_intf.S)(Th : Plugin_intf.S) = struct
+module Make (E : Expr_intf.S)(Th : Plugin_intf.S with
+    type formula = E.Formula.t and type term = E.Term.t) = struct
 
   (* Types declarations *)
 
@@ -115,6 +116,22 @@ module Make (E : Expr_intf.S)(Th : Plugin_intf.S) = struct
 
   let cpt_mk_var = ref 0
 
+  let make_semantic_var t =
+      try MT.find t !t_map
+      with Not_found ->
+        let res = {
+          vid = !cpt_mk_var;
+          weight = 1.;
+          level = -1;
+          tag = {
+            term = t;
+            assigned = None; };
+        } in
+        incr cpt_mk_var;
+        t_map := MT.add t res !t_map;
+        Vec.push vars (Either.mk_left res);
+        res
+
   let make_boolean_var =
     fun lit ->
       let lit, negated = E.norm lit in
@@ -149,24 +166,9 @@ module Make (E : Expr_intf.S)(Th : Plugin_intf.S) = struct
         f_map := MF.add lit var !f_map;
         incr cpt_mk_var;
         Vec.push vars (Either.mk_right var);
+        Th.iter_assignable (fun t -> ignore (make_semantic_var t)) lit;
         var, negated
 
-  let make_semantic_var t =
-      try MT.find t !t_map
-      with Not_found ->
-        let res = {
-          vid = !cpt_mk_var;
-          weight = 0.;
-          level = -1;
-          tag = {
-            term = t;
-            assigned = None; };
-        } in
-        incr cpt_mk_var;
-        t_map := MT.add t res !t_map;
-        Vec.push vars (Either.mk_left res);
-        res
-
   let add_term t = make_semantic_var t
 
   let add_atom lit =

solver/mcsolver_types.mli

@@ -13,6 +13,7 @@
 
 module type S = Mcsolver_types_intf.S
 
-module Make : functor (E : Expr_intf.S)(Th : Plugin_intf.S)
+module Make : functor (E : Expr_intf.S)(Th : Plugin_intf.S with
+    type term = E.Term.t and type formula = E.Formula.t)
   -> S with type term = E.Term.t and type formula = E.Formula.t and type proof = Th.proof
 (** Functor to instantiate the types of clauses for the Solver. *)

solver/plugin_intf.ml

@@ -31,7 +31,7 @@ module type S = sig
   type slice = {
     start : int;
     length : int;
-    get : int -> assumption;
+    get : int -> assumption * int;
     push : formula list -> proof -> unit;
   }
   (** The type for a slice of litterals to assume/propagate in the theory.

tests/sat/test-010.smt2

@@ -0,0 +1,2 @@
+(assert (and (= a b) (= b c) (or (not (= a c)) (= a d))))
+(check-sat)

tests/unsat/test-011.smt2

@@ -0,0 +1,2 @@
+(assert (and (= a b) (= b c) (= c d) (or (not (= a c)) (not (= a a)))))
+(check-sat)

util/mcsat_solve.ml

@@ -0,0 +1,222 @@
+
+module F = Expr
+module T = Cnf.S
+module S = Mcsat.Make(struct end)
+
+exception Incorrect_model
+exception Out_of_time
+exception Out_of_space
+
+(* IO wrappers *)
+(* Types for input/output languages *)
+type sat_input =
+  | Auto
+  | Dimacs
+  | Smtlib
+
+type sat_output =
+  | Standard (* Only output problem status *)
+  | Dot
+
+let input = ref Auto
+let output = ref Standard
+
+let input_list = [
+  "auto", Auto;
+  "dimacs", Dimacs;
+  "smtlib", Smtlib;
+]
+let output_list = [
+  "dot", Dot;
+]
+
+let error_msg opt arg l =
+  Format.fprintf Format.str_formatter "'%s' is not a valid argument for '%s', valid arguments are : %a"
+    arg opt (fun fmt -> List.iter (fun (s, _) -> Format.fprintf fmt "%s, " s)) l;
+  Format.flush_str_formatter ()
+
+let set_io opt arg flag l =
+  try
+    flag := List.assoc arg l
+  with Not_found ->
+    invalid_arg (error_msg opt arg l)
+
+let set_input s = set_io "Input" s input input_list
+let set_output s = set_io "Output" s output output_list
+
+(* Input Parsing *)
+let rec rev_flat_map f acc = function
+  | [] -> acc
+  | a :: r -> rev_flat_map f (List.rev_append (f a) acc) r
+
+let format_of_filename s =
+  let last n =
+    try String.sub s (String.length s - n) n
+    with Invalid_argument _ -> ""
+  in
+  if last 4 = ".cnf" then
+    Dimacs
+  else if last 5 = ".smt2" then
+    Smtlib
+  else (* Default choice *)
+    Dimacs
+
+let parse_with_input file = function
+  | Auto -> assert false
+  | Dimacs -> List.rev_map (List.rev_map F.mk_prop) (Parsedimacs.parse file)
+  | Smtlib -> rev_flat_map T.make_cnf [] (Smtlib.parse file)
+
+let parse_input file =
+  parse_with_input file (match !input with
+      | Auto -> format_of_filename file
+      | f -> f)
+
+(* Printing wrappers *)
+let std = Format.std_formatter
+
+let print format = match !output with
+  | Standard -> Format.fprintf std "%( fmt %)@." format
+  | Dot -> Format.fprintf std "/* %( fmt %) */@." format
+
+let print_proof proof = match !output with
+  | Standard -> ()
+  | Dot -> S.print_proof std proof
+
+let rec print_cl fmt = function
+  | [] -> Format.fprintf fmt "[]"
+  | [a] -> F.print fmt a
+  | a :: ((_ :: _) as r) -> Format.fprintf fmt "%a ∨ %a" F.print a print_cl r
+
+let print_lcl l =
+  List.iter (fun c -> Format.fprintf std "%a@\n" print_cl c) l
+
+let print_lclause l =
+  List.iter (fun c -> Format.fprintf std "%a@\n" S.print_clause c) l
+
+let print_cnf cnf = match !output with
+  | Standard -> print_lcl cnf
+  | Dot -> ()
+
+let print_unsat_core u = match !output with
+  | Standard -> print_lclause u
+  | Dot -> ()
+
+(* Arguments parsing *)
+let file = ref ""
+let p_cnf = ref false
+let p_check = ref false
+let p_proof_print = ref false
+let p_unsat_core = ref false
+let time_limit = ref 300.
+let size_limit = ref 1000_000_000.
+
+let int_arg r arg =
+  let l = String.length arg in
+  let multiplier m =
+    let arg1 = String.sub arg 0 (l-1) in
+    r := m *. (float_of_string arg1)
+  in
+  if l = 0 then raise (Arg.Bad "bad numeric argument")
+  else
+    try
+      match arg.[l-1] with
+      | 'k' -> multiplier 1e3
+      | 'M' -> multiplier 1e6
+      | 'G' -> multiplier 1e9
+      | 'T' -> multiplier 1e12
+      | 's' -> multiplier 1.
+      | 'm' -> multiplier 60.
+      | 'h' -> multiplier 3600.
+      | 'd' -> multiplier 86400.
+      | '0'..'9' -> r := float_of_string arg
+      | _ -> raise (Arg.Bad "bad numeric argument")
+    with Failure "float_of_string" -> raise (Arg.Bad "bad numeric argument")
+
+let setup_gc_stat () =
+  at_exit (fun () ->
+      Gc.print_stat stdout;
+    )
+
+let input_file = fun s -> file := s
+
+let usage = "Usage : main [options] <file>"
+let argspec = Arg.align [
+    "-bt", Arg.Unit (fun () -> Printexc.record_backtrace true),
+    " Enable stack traces";
+    "-cnf", Arg.Set p_cnf,
+    " Prints the cnf used.";
+    "-check", Arg.Set p_check,
+    " Build, check and print the proof (if output is set), if unsat";
+    "-gc", Arg.Unit setup_gc_stat,
+    " Outputs statistics about the GC";
+    "-i", Arg.String set_input,
+    " Sets the input format (default auto)";
+    "-o", Arg.String set_output,
+    " Sets the output format (default none)";
+    "-size", Arg.String (int_arg size_limit),
+    "<s>[kMGT] Sets the size limit for the sat solver";
+    "-time", Arg.String (int_arg time_limit),
+    "<t>[smhd] Sets the time limit for the sat solver";
+    "-u", Arg.Set p_unsat_core,
+    " Prints the unsat-core explanation of the unsat proof (if used with -check)";
+    "-v", Arg.Int (fun i -> Log.set_debug i),
+    "<lvl> Sets the debug verbose level";
+  ]
+
+(* Limits alarm *)
+let check () =
+  let t = Sys.time () in
+  let heap_size = (Gc.quick_stat ()).Gc.heap_words in
+  let s = float heap_size *. float Sys.word_size /. 8. in
+  if t > !time_limit then
+    raise Out_of_time
+  else if s > !size_limit then
+    raise Out_of_space
+
+(* Entry file parsing *)
+let get_cnf () = parse_input !file
+
+let main () =
+  (* Administrative duties *)
+  Arg.parse argspec input_file usage;
+  if !file = "" then begin
+    Arg.usage argspec usage;
+    exit 2
+  end;
+  let al = Gc.create_alarm check in
+
+  (* Interesting stuff happening *)
+  let cnf = get_cnf () in
+  if !p_cnf then
+    print_cnf cnf;
+  S.assume cnf;
+  let res = S.solve () in
+  Gc.delete_alarm al;
+  match res with
+  | S.Sat ->
+    print "Sat";
+    if !p_check then
+      if not (List.for_all (List.exists S.eval) cnf) then
+          raise Incorrect_model
+  | S.Unsat ->
+    print "Unsat";
+    if !p_check then begin
+      let p = S.get_proof () in
+      print_proof p;
+      if !p_unsat_core then
+        print_unsat_core (S.unsat_core p)
+    end
+
+let () =
+  try
+    main ()
+  with
+  | Incorrect_model ->
+    print "Internal error : incorrect *sat* model";
+    exit 4
+  | Out_of_time ->
+    print "Time limit exceeded";
+    exit 2
+  | Out_of_space ->
+    print "Size limit exceeded";
+    exit 3

util/sat_solve.ml

@@ -1,6 +1,6 @@
 
-module F = Smt.Fsmt
-module T = Smt.Tseitin
+module F = Expr
+module T = Cnf.S
 module S = Smt.Make(struct end)
 
 exception Incorrect_model

util/smtlib/smtlib.ml

@@ -2,8 +2,8 @@
 
 open Smtlib_syntax
 
-module F = Smt.Fsmt
-module T = Smt.Tseitin
+module F = Expr
+module T = Cnf.S
 
 exception Bad_arity of string
 exception Unknown_command

util/smtlib/smtlib.mli

@@ -1,3 +1,3 @@
 (* Copyright 2014 INRIA *)
 
-val parse : string -> Smt.Tseitin.t list
+val parse : string -> Cnf.S.t list