use a pure sat solver for cnf files

sidekick.opam

@@ -14,7 +14,6 @@ depends: [
   "dune" { >= "1.1" }
   "containers" { >= "3.0" & < "4.0" }
   "iter" { >= "1.0" & < "2.0" }
-  "msat" { >= "0.9" < "0.10" }
   "ocaml" { >= "4.04" }
   "alcotest" {with-test}
   "odoc" {with-doc}

src/backend/Dot.ml

@@ -36,15 +36,15 @@ module Default(S : Sidekick_sat.S) = struct
 
   let hyp_info c =
     "hypothesis", Some "LIGHTBLUE",
-    [ fun fmt () -> Format.fprintf fmt "%s" @@ Clause.name c]
+    [ fun fmt () -> Format.fprintf fmt "%s" @@ Clause.short_name c]
 
   let lemma_info c =
     "lemma", Some "BLUE",
-    [ fun fmt () -> Format.fprintf fmt "%s" @@ Clause.name c]
+    [ fun fmt () -> Format.fprintf fmt "%s" @@ Clause.short_name c]
 
   let assumption_info c =
     "assumption", Some "PURPLE",
-    [ fun fmt () -> Format.fprintf fmt "%s" @@ Clause.name c]
+    [ fun fmt () -> Format.fprintf fmt "%s" @@ Clause.short_name c]
 
 end
 
@@ -57,7 +57,7 @@ module Make(S : Sidekick_sat.S)(A : Arg with type atom := S.atom
   module Clause = S.Clause
   module P = S.Proof
 
-  let node_id n = Clause.name n.P.conclusion
+  let node_id n = Clause.short_name n.P.conclusion
   let proof_id p = node_id (P.expand p)
   let res_nn_id n1 n2 = node_id n1 ^ "_" ^ node_id n2 ^ "_res"
   let res_np_id n1 n2 = node_id n1 ^ "_" ^ proof_id n2 ^ "_res"

src/main/dune

@@ -4,7 +4,7 @@
  (name main)
  (public_name sidekick)
  (package sidekick-bin)
- (libraries containers iter result msat sidekick.core sidekick-base
+ (libraries containers iter result sidekick.sat sidekick.core sidekick-base
             sidekick.msat-solver sidekick-bin.smtlib sidekick.tef)
  (flags :standard -safe-string -color always -open Sidekick_util))
 

src/main/main.ml

@@ -4,14 +4,14 @@ Copyright 2014 Guillaume Bury
 Copyright 2014 Simon Cruanes
 *)
 
-open CCResult.Infix
-
 module E = CCResult
 module Fmt = CCFormat
 module Term = Sidekick_base.Term
 module Solver = Sidekick_smtlib.Solver
 module Process = Sidekick_smtlib.Process
 
+open E.Infix
+
 type 'a or_error = ('a, string) E.t
 
 exception Out_of_time
@@ -87,39 +87,6 @@ let argspec = Arg.align [
     "--debug", Arg.Int Msat.Log.set_debug, "<lvl> sets the debug verbose level";
   ] |> List.sort compare
 
-module Dimacs = struct
-  open Sidekick_base
-  module T = Term
-
-  let parse_file tst (file:string) : Statement.t list or_error =
-    let atoms = Util.Int_tbl.create 32 in
-    let get_lit i =
-      let v =
-        match Util.Int_tbl.find atoms (abs i) with
-        | x -> Term.const tst x
-        | exception Not_found ->
-          let f = Sidekick_base.Fun.mk_undef_const
-              (ID.makef "%d" (abs i)) (Ty.bool()) in
-          Util.Int_tbl.add atoms (abs i) f;
-          Term.const tst f
-      in
-      if i<0 then Term.not_ tst v else v
-    in
-    try
-      CCIO.with_in file
-        (fun ic ->
-           let p = Dimacs_parser.create ic in
-           let stmts = ref [] in
-           Dimacs_parser.iter p
-             (fun c ->
-                let lits = List.rev_map get_lit c in
-                stmts := Statement.Stmt_assert_clause lits :: !stmts);
-           stmts := Statement.Stmt_check_sat [] :: !stmts;
-           Ok (List.rev !stmts))
-    with e ->
-      E.of_exn_trace e
-end
-
 (* Limits alarm *)
 let check_limits () =
   let t = Sys.time () in
@@ -130,25 +97,12 @@ let check_limits () =
   else if s > !size_limit then
     raise Out_of_space
 
-let main () =
+let main_smt ~dot_proof () : _ result =
-  Sidekick_tef.setup();
-  at_exit Sidekick_tef.teardown;
-  CCFormat.set_color_default true;
-  (* Administrative duties *)
-  Arg.parse argspec input_file usage;
-  if !file = "" then (
-    Arg.usage argspec usage;
-    exit 2
-  );
-  let dot_proof = if !p_dot_proof = "" then None else Some !p_dot_proof in
-  check := !check || CCOpt.is_some dot_proof; (* dot requires a proof *)
-  let al = Gc.create_alarm check_limits in
-  Util.setup_gc();
   let tst = Term.create ~size:4_096 () in
-  let is_cnf = Filename.check_suffix !file ".cnf" in
   let solver =
     let theories =
-      if is_cnf then [] else [
+      (* TODO: probes, to load only required theories *)
+      [
         Process.th_bool;
         Process.th_data;
         Process.th_lra;
@@ -163,8 +117,7 @@ let main () =
     Solver.add_theory solver Process.Check_cc.theory;
   );
   begin
-    if is_cnf then Dimacs.parse_file tst !file
+    Sidekick_smtlib.parse tst !file
-    else Sidekick_smtlib.parse tst !file
   end
   >>= fun input ->
   (* process statements *)
@@ -186,6 +139,35 @@ let main () =
   if !p_stat then (
     Format.printf "%a@." Solver.pp_stats solver;
   );
+  res
+
+let main_cnf () : _ result =
+  let solver = Pure_sat_solver.SAT.create ~size:`Big () in
+  Pure_sat_solver.Dimacs.parse_file solver !file >>= fun () ->
+  Pure_sat_solver.solve solver
+
+let main () =
+  Sidekick_tef.setup();
+  at_exit Sidekick_tef.teardown;
+  CCFormat.set_color_default true;
+  (* Administrative duties *)
+  Arg.parse argspec input_file usage;
+  if !file = "" then (
+    Arg.usage argspec usage;
+    exit 2
+  );
+  let dot_proof = if !p_dot_proof = "" then None else Some !p_dot_proof in
+  check := !check || CCOpt.is_some dot_proof; (* dot requires a proof *)
+  let al = Gc.create_alarm check_limits in
+  Util.setup_gc();
+  let is_cnf = Filename.check_suffix !file ".cnf" in
+  let res =
+    if is_cnf then (
+      main_cnf ()
+    ) else (
+      main_smt ~dot_proof ()
+    )
+  in
   if !p_gc_stat then (
     Printf.printf "(gc_stats\n%t)\n" Gc.print_stat;
   );

src/main/pure_sat_solver.ml

@@ -0,0 +1,58 @@
+
+(* pure SAT solver *)
+
+module E = CCResult
+module SS = Sidekick_sat
+
+module Arg = struct
+  module Formula = struct
+    type t = int
+    let norm t = if t>0 then t, SS.Same_sign else -t, SS.Negated
+    let abs = abs
+    let sign t = t>0
+    let equal = CCInt.equal
+    let hash = CCHash.int
+    let neg x = -x
+    let pp = Fmt.int
+  end
+  type proof=unit
+end
+
+module SAT = Sidekick_sat.Make_pure_sat(Arg)
+
+module Dimacs = struct
+  open Sidekick_base
+  module T = Term
+
+  let parse_file (solver:SAT.t) (file:string) : (unit, string) result =
+    let get_lit i : SAT.atom = SAT.make_atom solver i in
+
+    try
+      CCIO.with_in file
+        (fun ic ->
+           let p = Dimacs_parser.create ic in
+           Dimacs_parser.iter p
+             (fun c ->
+                let atoms = List.rev_map get_lit c in
+                SAT.add_clause solver atoms ());
+           Ok ())
+    with e ->
+      E.of_exn_trace e
+end
+
+let solve (solver:SAT.t) : (unit, string) result =
+  let res =
+    Profile.with_ "solve" (fun () -> SAT.solve solver)
+  in
+  let t2 = Sys.time () in
+  Printf.printf "\r"; flush stdout;
+  begin match res with
+    | SAT.Sat _ ->
+      let t3 = Sys.time () -. t2 in
+      Format.printf "Sat (%.3f/%.3f)@." t2 t3;
+    | SAT.Unsat _ ->
+
+      let t3 = Sys.time () -. t2 in
+      Format.printf "Unsat (%.3f/%.3f)@." t2 t3;
+  end;
+  Ok ()

src/sat/Sidekick_sat.ml

@@ -54,4 +54,6 @@ let pp_lbool out = function
 
 exception No_proof = Solver_intf.No_proof
 
+module Solver = Solver
 module Make_cdcl_t = Solver.Make_cdcl_t
+module Make_pure_sat = Solver.Make_pure_sat

src/sat/Solver.ml

@@ -1,8 +1,8 @@
 
 module type PLUGIN = sig
   val has_theory : bool
-  (** Is this a CDCL(T) plugin or mcsat plugin?
+  (** [true] iff the solver is parametrized by a theory, not just
-      i.e does it have theories *)
+      pure SAT. *)
 
   include Solver_intf.PLUGIN_CDCL_T
 end
@@ -11,7 +11,7 @@ module type S = Solver_intf.S
 module type PLUGIN_CDCL_T = Solver_intf.PLUGIN_CDCL_T
 
 let invalid_argf fmt =
-  Format.kasprintf (fun msg -> invalid_arg ("msat: " ^ msg)) fmt
+  Format.kasprintf (fun msg -> invalid_arg ("sidekick.sat: " ^ msg)) fmt
 
 module Make(Plugin : PLUGIN)
 = struct
@@ -66,6 +66,8 @@ module Make(Plugin : PLUGIN)
   (* Constructors *)
   module MF = Hashtbl.Make(Formula)
 
+  (* state for variables. declared separately because it simplifies our
+     life below, as it's required to construct new atoms/variables *)
   type st = {
     f_map: var MF.t;
     vars: var Vec.t;
@@ -89,12 +91,12 @@ module Make(Plugin : PLUGIN)
   let get_elt st i = Vec.get st.vars i
   let iter_elt st f = Vec.iter f st.vars
 
-  let name_of_clause c = match c.cpremise with
+  let kind_of_clause c = match c.cpremise with
-    | Hyp _ -> "H" ^ string_of_int c.cid
+    | Hyp _ -> "H"
-    | Lemma _ -> "T" ^ string_of_int c.cid
+    | Lemma _ -> "T"
-    | Local -> "L" ^ string_of_int c.cid
+    | Local -> "L"
-    | History _ -> "C" ^ string_of_int c.cid
+    | History _ -> "C"
-    | Empty_premise -> string_of_int c.cid
+    | Empty_premise -> ""
 
   (* some boolean flags for variables, used as masks *)
   let seen_var = 0b1
@@ -224,7 +226,7 @@ module Make(Plugin : PLUGIN)
       | n, Some Decision ->
         Format.fprintf fmt "@@%d" n
       | n, Some Bcp c ->
-        Format.fprintf fmt "->%d/%s" n (name_of_clause c)
+        Format.fprintf fmt "->%d/%s/%d" n (kind_of_clause c) c.cid
       | n, Some (Bcp_lazy _) ->
         Format.fprintf fmt "->%d/<lazy>" n
 
@@ -268,7 +270,6 @@ module Make(Plugin : PLUGIN)
     let make ~flags l premise = make_a ~flags (Array.of_list l) premise
 
     let empty = make [] (History [])
-    let name = name_of_clause
     let[@inline] equal c1 c2 = c1.cid = c2.cid
     let[@inline] hash c = Hashtbl.hash c.cid
     let[@inline] atoms c = c.atoms
@@ -311,20 +312,24 @@ module Make(Plugin : PLUGIN)
         let equal = equal
       end)
 
+    let short_name c = Printf.sprintf "%s%d" (kind_of_clause c) c.cid
     let pp fmt c =
-      Format.fprintf fmt "%s : %a" (name c) Atom.pp_a c.atoms
+      Format.fprintf fmt "(cl[%s%d] : %a" (kind_of_clause c) c.cid Atom.pp_a c.atoms
 
     let debug_premise out = function
       | Hyp _ -> Format.fprintf out "hyp"
       | Lemma _ -> Format.fprintf out "th_lemma"
       | Local -> Format.fprintf out "local"
       | History v ->
-        List.iter (fun c -> Format.fprintf out "%s,@ " (name_of_clause c)) v
+        Format.fprintf out "(@[res";
-      | Empty_premise -> Format.fprintf out "<no premise>"
+        List.iter (fun c -> Format.fprintf out "@ %s%d," (kind_of_clause c) c.cid) v;
+        Format.fprintf out "@])"
+      | Empty_premise -> Format.fprintf out "none"
 
     let debug out ({atoms=arr; cpremise=cp;_}as c) =
-      Format.fprintf out "%s@[<hov>{@[<hov>%a@]}@ cpremise={@[<hov>%a@]}@]"
+      Format.fprintf out
-        (name c) Atom.debug_a arr debug_premise cp
+        "(@[cl[%s%d]@ {@[<hov>%a@]}@ :premise %a@])"
+        (kind_of_clause c) c.cid Atom.debug_a arr debug_premise cp
   end
 
   module Proof =  struct
@@ -774,7 +779,6 @@ module Make(Plugin : PLUGIN)
     st.on_conflict <- on_conflict;
     st
 
-  let[@inline] st t = t.st
   let[@inline] nb_clauses st = Vec.size st.clauses_hyps
   let[@inline] decision_level st = Vec.size st.var_levels
 

src/sat/Solver_intf.ml

@@ -341,8 +341,8 @@ module type S = sig
     val atoms : t -> atom array
     val atoms_l : t -> atom list
     val equal : t -> t -> bool
-    val name : t -> string
 
+    val short_name : t -> string
     val pp : t printer
 
     module Tbl : Hashtbl.S with type key = t

src/smtlib/dune

@@ -1,7 +1,7 @@
 (library
  (name sidekick_smtlib)
  (public_name sidekick-bin.smtlib)
- (libraries containers zarith msat sidekick.core sidekick.util
+ (libraries containers zarith sidekick.core sidekick.util
             sidekick-base sidekick-base.solver
             msat.backend smtlib-utils
             sidekick.tef)

src/util/dune

@@ -1,4 +1,4 @@
 (library
   (name sidekick_util)
   (public_name sidekick.util)
-  (libraries containers iter msat sidekick.sigs))
+  (libraries containers iter sidekick.sigs))