From 1aa160fe56a20b1ae09e63f324f271c71e769aa2 Mon Sep 17 00:00:00 2001 From: Simon Cruanes Date: Sun, 18 Jul 2021 02:46:04 -0400 Subject: [PATCH] use a pure sat solver for cnf files --- sidekick.opam | 1 - src/backend/Dot.ml | 8 ++-- src/main/dune | 2 +- src/main/main.ml | 88 +++++++++++++++---------------------- src/main/pure_sat_solver.ml | 58 ++++++++++++++++++++++++ src/sat/Sidekick_sat.ml | 2 + src/sat/Solver.ml | 38 +++++++++------- src/sat/Solver_intf.ml | 2 +- src/smtlib/dune | 2 +- src/util/dune | 2 +- 10 files changed, 124 insertions(+), 79 deletions(-) create mode 100644 src/main/pure_sat_solver.ml diff --git a/sidekick.opam b/sidekick.opam index 7f27208f..03a6a890 100644 --- a/sidekick.opam +++ b/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} diff --git a/src/backend/Dot.ml b/src/backend/Dot.ml index 632f39a7..7085fc86 100644 --- a/src/backend/Dot.ml +++ b/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" diff --git a/src/main/dune b/src/main/dune index 621bc88c..e17a42e6 100644 --- a/src/main/dune +++ b/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)) diff --git a/src/main/main.ml b/src/main/main.ml index 6651aca3..b407d696 100644 --- a/src/main/main.ml +++ b/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, " 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 () = - 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 main_smt ~dot_proof () : _ result = 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 - else Sidekick_smtlib.parse tst !file + 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; ); diff --git a/src/main/pure_sat_solver.ml b/src/main/pure_sat_solver.ml new file mode 100644 index 00000000..14f79638 --- /dev/null +++ b/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 () diff --git a/src/sat/Sidekick_sat.ml b/src/sat/Sidekick_sat.ml index a618d8a7..9ffa03ad 100644 --- a/src/sat/Sidekick_sat.ml +++ b/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 diff --git a/src/sat/Solver.ml b/src/sat/Solver.ml index bb827f8f..07609129 100644 --- a/src/sat/Solver.ml +++ b/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? - i.e does it have theories *) + (** [true] iff the solver is parametrized by a theory, not just + 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 - | Hyp _ -> "H" ^ string_of_int c.cid - | Lemma _ -> "T" ^ string_of_int c.cid - | Local -> "L" ^ string_of_int c.cid - | History _ -> "C" ^ string_of_int c.cid - | Empty_premise -> string_of_int c.cid + let kind_of_clause c = match c.cpremise with + | Hyp _ -> "H" + | Lemma _ -> "T" + | Local -> "L" + | History _ -> "C" + | 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/" 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 - | Empty_premise -> Format.fprintf out "" + Format.fprintf out "(@[res"; + 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@[{@[%a@]}@ cpremise={@[%a@]}@]" - (name c) Atom.debug_a arr debug_premise cp + Format.fprintf out + "(@[cl[%s%d]@ {@[%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 diff --git a/src/sat/Solver_intf.ml b/src/sat/Solver_intf.ml index 0abbbff8..69a2b911 100644 --- a/src/sat/Solver_intf.ml +++ b/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 diff --git a/src/smtlib/dune b/src/smtlib/dune index 318b0cda..0ab68eb4 100644 --- a/src/smtlib/dune +++ b/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) diff --git a/src/util/dune b/src/util/dune index 93411a31..584dcca7 100644 --- a/src/util/dune +++ b/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))