diff --git a/.github/workflows/main.yml b/.github/workflows/main.yml index 09222c24..e4b3df6f 100644 --- a/.github/workflows/main.yml +++ b/.github/workflows/main.yml @@ -1,5 +1,11 @@ name: Build sidekick-bin -on: [push] +on: + push: + branches: + - master + pull_request: + branches: + - master jobs: run: name: Build diff --git a/.header b/.header deleted file mode 100644 index fe8863b5..00000000 --- a/.header +++ /dev/null @@ -1,5 +0,0 @@ -(* -MSAT is free software, using the Apache license, see file LICENSE -Copyright 2014 Guillaume Bury -Copyright 2014 Simon Cruanes -*) diff --git a/Makefile b/Makefile index aba219b0..2f4a1990 100644 --- a/Makefile +++ b/Makefile @@ -67,7 +67,7 @@ reindent: WATCH=@all watch: - @dune build $(WATCH) -w + @dune build $(WATCH) -w $(OPTS) --profile=release #@dune build @all -w # TODO: once tests pass .PHONY: clean doc all bench install uninstall remove reinstall bin test diff --git a/sidekick-bin.opam b/sidekick-bin.opam index 50202b34..3ebd039f 100644 --- a/sidekick-bin.opam +++ b/sidekick-bin.opam @@ -19,10 +19,13 @@ depends: [ "sidekick" { = version } "sidekick-base" { = version } "menhir" - "mtime" "ocaml" { >= "4.04" } "odoc" {with-doc} ] +depopts: [ + "memtrace" + "mtime" +] tags: [ "sat" "smt" ] homepage: "https://github.com/c-cube/sidekick" dev-repo: "git+https://github.com/c-cube/sidekick.git" 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/Backend_intf.ml b/src/backend/Backend_intf.ml new file mode 100644 index 00000000..29900a0c --- /dev/null +++ b/src/backend/Backend_intf.ml @@ -0,0 +1,27 @@ +(* +MSAT is free software, using the Apache license, see file LICENSE +Copyright 2014 Guillaume Bury +Copyright 2014 Simon Cruanes +*) + +(** Backend interface + + This modules defines the interface of the modules providing + export of proofs. +*) + +module type S = sig + (** Proof exporting + + Currently, exporting a proof means printing it into a file + according to the conventions of a given format. + *) + + type t + (** The type of proofs. *) + + val pp : Format.formatter -> t -> unit + (** A function for printing proofs in the desired format. *) + +end + diff --git a/src/backend/Dot.ml b/src/backend/Dot.ml new file mode 100644 index 00000000..7085fc86 --- /dev/null +++ b/src/backend/Dot.ml @@ -0,0 +1,191 @@ +(* +MSAT is free software, using the Apache license, see file LICENSE +Copyright 2014 Guillaume Bury +Copyright 2014 Simon Cruanes +*) + +(** Output interface for the backend *) +module type S = Backend_intf.S + +(** Input module for the backend *) +module type Arg = sig + + type atom + (* Type of atoms *) + + type hyp + type lemma + type assumption + (** Types for hypotheses, lemmas, and assumptions. *) + + val print_atom : Format.formatter -> atom -> unit + (** Printing function for atoms *) + + val hyp_info : hyp -> string * string option * (Format.formatter -> unit -> unit) list + val lemma_info : lemma -> string * string option * (Format.formatter -> unit -> unit) list + val assumption_info : assumption -> string * string option * (Format.formatter -> unit -> unit) list + (** Functions to return information about hypotheses and lemmas *) + +end + +module Default(S : Sidekick_sat.S) = struct + module Atom = S.Atom + module Clause = S.Clause + + let print_atom = Atom.pp + + let hyp_info c = + "hypothesis", Some "LIGHTBLUE", + [ fun fmt () -> Format.fprintf fmt "%s" @@ Clause.short_name c] + + let lemma_info c = + "lemma", Some "BLUE", + [ fun fmt () -> Format.fprintf fmt "%s" @@ Clause.short_name c] + + let assumption_info c = + "assumption", Some "PURPLE", + [ fun fmt () -> Format.fprintf fmt "%s" @@ Clause.short_name c] + +end + +(** Functor to provide dot printing *) +module Make(S : Sidekick_sat.S)(A : Arg with type atom := S.atom + and type hyp := S.clause + and type lemma := S.clause + and type assumption := S.clause) = struct + module Atom = S.Atom + module Clause = S.Clause + module P = S.Proof + + 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" + + let print_clause fmt c = + let v = Clause.atoms c in + if Array.length v = 0 then + Format.fprintf fmt "⊥" + else + let n = Array.length v in + for i = 0 to n - 1 do + Format.fprintf fmt "%a" A.print_atom v.(i); + if i < n - 1 then + Format.fprintf fmt ", " + done + + let print_edge fmt i j = + Format.fprintf fmt "%s -> %s;@\n" j i + + let print_edges fmt n = + match P.(n.step) with + | P.Hyper_res {P.hr_steps=[];_} -> assert false (* NOTE: should never happen *) + | P.Hyper_res {P.hr_init; hr_steps=((_,p0)::_) as l} -> + print_edge fmt (res_np_id n p0) (proof_id hr_init); + List.iter + (fun (_,p2) -> print_edge fmt (res_np_id n p2) (proof_id p2)) + l; + | _ -> () + + let table_options fmt color = + Format.fprintf fmt "BORDER=\"0\" CELLBORDER=\"1\" CELLSPACING=\"0\" BGCOLOR=\"%s\"" color + + let table fmt (c, rule, color, l) = + Format.fprintf fmt "%a" print_clause c; + match l with + | [] -> + Format.fprintf fmt "%s" color rule + | f :: r -> + Format.fprintf fmt "%s%a" + color (List.length l) rule f (); + List.iter (fun f -> Format.fprintf fmt "%a" f ()) r + + let print_dot_node fmt id color c rule rule_color l = + Format.fprintf fmt "%s [shape=plaintext, label=<%a
>];@\n" + id table_options color table (c, rule, rule_color, l) + + let print_dot_res_node fmt id a = + Format.fprintf fmt "%s [label=<%a>];@\n" id A.print_atom a + + let ttify f c = fun fmt () -> f fmt c + + let print_contents fmt n = + match P.(n.step) with + (* Leafs of the proof tree *) + | P.Hypothesis _ -> + let rule, color, l = A.hyp_info P.(n.conclusion) in + let color = match color with None -> "LIGHTBLUE" | Some c -> c in + print_dot_node fmt (node_id n) "LIGHTBLUE" P.(n.conclusion) rule color l + | P.Assumption -> + let rule, color, l = A.assumption_info P.(n.conclusion) in + let color = match color with None -> "LIGHTBLUE" | Some c -> c in + print_dot_node fmt (node_id n) "LIGHTBLUE" P.(n.conclusion) rule color l + | P.Lemma _ -> + let rule, color, l = A.lemma_info P.(n.conclusion) in + let color = match color with None -> "YELLOW" | Some c -> c in + print_dot_node fmt (node_id n) "LIGHTBLUE" P.(n.conclusion) rule color l + + (* Tree nodes *) + | P.Duplicate (p, l) -> + print_dot_node fmt (node_id n) "GREY" P.(n.conclusion) "Duplicate" "GREY" + ((fun fmt () -> (Format.fprintf fmt "%s" (node_id n))) :: + List.map (ttify A.print_atom) l); + print_edge fmt (node_id n) (node_id (P.expand p)) + | P.Hyper_res {P.hr_steps=l; _} -> + print_dot_node fmt (node_id n) "GREY" P.(n.conclusion) "Resolution" "GREY" + [(fun fmt () -> (Format.fprintf fmt "%s" (node_id n)))]; + List.iter + (fun (a,p2) -> + print_dot_res_node fmt (res_np_id n p2) a; + print_edge fmt (node_id n) (res_np_id n p2)) + l + + let print_node fmt n = + print_contents fmt n; + print_edges fmt n + + let pp fmt p = + Format.fprintf fmt "digraph proof {@\n"; + P.fold (fun () -> print_node fmt) () p; + Format.fprintf fmt "}@." + +end + +module Simple(S : Sidekick_sat.S) + (A : Arg with type atom := S.formula + and type hyp = S.formula list + and type lemma := S.lemma + and type assumption = S.formula) = + Make(S)(struct + module Atom = S.Atom + module Clause = S.Clause + module P = S.Proof + + (* Some helpers *) + let lit = Atom.formula + + let get_assumption c = + match S.Clause.atoms_l c with + | [ x ] -> x + | _ -> assert false + + let get_lemma c = + match P.expand (P.prove c) with + | {P.step=P.Lemma p;_} -> p + | _ -> assert false + + (* Actual functions *) + let print_atom fmt a = + A.print_atom fmt (lit a) + + let hyp_info c = + A.hyp_info (List.map lit (S.Clause.atoms_l c)) + + let lemma_info c = + A.lemma_info (get_lemma c) + + let assumption_info c = + A.assumption_info (lit (get_assumption c)) + + end) + diff --git a/src/backend/Dot.mli b/src/backend/Dot.mli new file mode 100644 index 00000000..eecdebaf --- /dev/null +++ b/src/backend/Dot.mli @@ -0,0 +1,70 @@ +(* +MSAT is free software, using the Apache license, see file LICENSE +Copyright 2014 Guillaume Bury +Copyright 2014 Simon Cruanes +*) + +(** Dot backend for proofs + + This module provides functions to export proofs into the dot graph format. + Graphs in dot format can be used to generates images using the graphviz tool. +*) + +module type S = Backend_intf.S +(** Interface for exporting proofs. *) + +module type Arg = sig + (** Term printing for DOT + + This module defines what functions are required in order to export + a proof to the DOT format. + *) + + type atom + (** The type of atomic formuals *) + + type hyp + type lemma + type assumption + (** The type of theory-specifi proofs (also called lemmas). *) + + val print_atom : Format.formatter -> atom -> unit + (** Print the contents of the given atomic formulas. + WARNING: this function should take care to escape and/or not output special + reserved characters for the dot format (such as quotes and so on). *) + + val hyp_info : hyp -> string * string option * (Format.formatter -> unit -> unit) list + val lemma_info : lemma -> string * string option * (Format.formatter -> unit -> unit) list + val assumption_info : assumption -> string * string option * (Format.formatter -> unit -> unit) list + (** Generate some information about the leafs of the proof tree. Currently this backend + print each lemma/assumption/hypothesis as a single leaf of the proof tree. + These function should return a triplet [(rule, color, l)], such that: + - [rule] is a name for the proof (arbitrary, does not need to be unique, but + should rather be descriptive) + - [color] is a color name (optional) understood by DOT + - [l] is a list of printers that will be called to print some additional information + *) + +end + +module Default(S : Sidekick_sat.S) : Arg with type atom := S.atom + and type hyp := S.clause + and type lemma := S.clause + and type assumption := S.clause +(** Provides a reasonnable default to instantiate the [Make] functor, assuming + the original printing functions are compatible with DOT html labels. *) + +module Make(S : Sidekick_sat.S)(A : Arg with type atom := S.atom + and type hyp := S.clause + and type lemma := S.clause + and type assumption := S.clause) : S with type t := S.Proof.t +(** Functor for making a module to export proofs to the DOT format. *) + +module Simple(S : Sidekick_sat.S)(A : Arg with type atom := S.formula + and type hyp = S.formula list + and type lemma := S.lemma + and type assumption = S.formula) : S with type t := S.Proof.t +(** Functor for making a module to export proofs to the DOT format. + The substitution of the hyp type is non-destructive due to a restriction + of destructive substitutions on earlier versions of ocaml. *) + diff --git a/src/backend/dune b/src/backend/dune new file mode 100644 index 00000000..316c6d7a --- /dev/null +++ b/src/backend/dune @@ -0,0 +1,6 @@ +(library + (name sidekick_backend) + (public_name sidekick.backend) + (synopsis "Proof backends for sidekick") + (libraries sidekick.sat)) + diff --git a/src/base/Base_types.ml b/src/base/Base_types.ml index 97fc2562..c788cf97 100644 --- a/src/base/Base_types.ml +++ b/src/base/Base_types.ml @@ -1,7 +1,7 @@ (** Basic type definitions for Sidekick_base *) -module Vec = Msat.Vec -module Log = Msat.Log +module Vec = Sidekick_util.Vec +module Log = Sidekick_util.Log module Fmt = CCFormat module CC_view = Sidekick_core.CC_view diff --git a/src/main/dune b/src/main/dune index 621bc88c..11c38908 100644 --- a/src/main/dune +++ b/src/main/dune @@ -4,8 +4,9 @@ (name main) (public_name sidekick) (package sidekick-bin) - (libraries containers iter result msat sidekick.core sidekick-base - sidekick.msat-solver sidekick-bin.smtlib sidekick.tef) + (libraries containers iter result sidekick.sat sidekick.core sidekick-base + sidekick.msat-solver sidekick-bin.smtlib sidekick.tef + sidekick.memtrace) (flags :standard -safe-string -color always -open Sidekick_util)) (rule diff --git a/src/main/main.ml b/src/main/main.ml index 8b61bb49..15a7eae7 100644 --- a/src/main/main.ml +++ b/src/main/main.ml @@ -4,14 +4,13 @@ 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 -module Vec = Msat.Vec + +open E.Infix type 'a or_error = ('a, string) E.t @@ -84,43 +83,10 @@ let argspec = Arg.align [ "--time", Arg.String (int_arg time_limit), " [smhd] sets the time limit for the sat solver"; "-t", Arg.String (int_arg time_limit), " short for --time"; "--version", Arg.Unit (fun () -> Printf.printf "version: %s\n%!" Sidekick_version.version; exit 0), " show version and exit"; - "-d", Arg.Int Msat.Log.set_debug, " sets the debug verbose level"; - "--debug", Arg.Int Msat.Log.set_debug, " sets the debug verbose level"; + "-d", Arg.Int Log.set_debug, " sets the debug verbose level"; + "--debug", Arg.Int 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 @@ -131,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; @@ -164,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 *) @@ -187,6 +139,39 @@ 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 () = + + (* instrumentation and tracing *) + Sidekick_tef.setup(); + at_exit Sidekick_tef.teardown; + Sidekick_memtrace.trace_if_requested ~context:"sidekick" (); + + 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/memtrace/dune b/src/memtrace/dune new file mode 100644 index 00000000..95085599 --- /dev/null +++ b/src/memtrace/dune @@ -0,0 +1,10 @@ + +(library + (name sidekick_memtrace) + (public_name sidekick.memtrace) + (libraries + (select sidekick_memtrace.ml from + (memtrace -> sidekick_memtrace.real.ml) + (-> sidekick_memtrace.dummy.ml))) + (flags :standard -warn-error -a+8)) + diff --git a/src/memtrace/sidekick_memtrace.dummy.ml b/src/memtrace/sidekick_memtrace.dummy.ml new file mode 100644 index 00000000..fd147541 --- /dev/null +++ b/src/memtrace/sidekick_memtrace.dummy.ml @@ -0,0 +1,2 @@ + +let trace_if_requested ?context:_ ?sampling_rate:_ () = () diff --git a/src/memtrace/sidekick_memtrace.mli b/src/memtrace/sidekick_memtrace.mli new file mode 100644 index 00000000..28211463 --- /dev/null +++ b/src/memtrace/sidekick_memtrace.mli @@ -0,0 +1,3 @@ + + +val trace_if_requested : ?context:string -> ?sampling_rate:float -> unit -> unit diff --git a/src/memtrace/sidekick_memtrace.real.ml b/src/memtrace/sidekick_memtrace.real.ml new file mode 100644 index 00000000..f2e78004 --- /dev/null +++ b/src/memtrace/sidekick_memtrace.real.ml @@ -0,0 +1 @@ +let trace_if_requested = Memtrace.trace_if_requested diff --git a/src/msat-solver/Sidekick_msat_solver.ml b/src/msat-solver/Sidekick_msat_solver.ml index 139d2694..03963f12 100644 --- a/src/msat-solver/Sidekick_msat_solver.ml +++ b/src/msat-solver/Sidekick_msat_solver.ml @@ -1,12 +1,10 @@ -(** {1 Implementation of a Solver using Msat} *) +(** Core of the SMT solver using Sidekick_sat -(** {{: https://github.com/Gbury/mSAT/} Msat} is a modular SAT solver in + Sidekick_sat (in src/sat/) is a modular SAT solver in pure OCaml. - This builds a {!Sidekick_core.SOLVER} on top of it. *) - -module Log = Msat.Log -(** A logging module *) + This builds a {!Sidekick_core.SOLVER} on top of it. +*) (** Argument to pass to the functor {!Make} in order to create a new Msat-based SMT solver. *) @@ -76,7 +74,7 @@ module Make(A : ARG) type lit = Lit_.t (* actions from msat *) - type msat_acts = (Msat.void, lit, Msat.void, P.t) Msat.acts + type msat_acts = (lit, P.t) Sidekick_sat.acts (* the full argument to the congruence closure *) module CC_actions = struct @@ -90,11 +88,13 @@ module Make(A : ARG) module P = P module Lit = Lit type t = msat_acts - let[@inline] raise_conflict a lits pr = - a.Msat.acts_raise_conflict lits pr - let[@inline] propagate a lit ~reason = - let reason = Msat.Consequence reason in - a.Msat.acts_propagate lit reason + let[@inline] raise_conflict (a:t) lits pr = + let (module A) = a in + A.raise_conflict lits pr + let[@inline] propagate (a:t) lit ~reason = + let (module A) = a in + let reason = Sidekick_sat.Consequence reason in + A.propagate lit reason end end @@ -218,7 +218,7 @@ module Make(A : ARG) include Lit let norm lit = let lit', sign = norm_sign lit in - lit', if sign then Msat.Same_sign else Msat.Negated + lit', if sign then Sidekick_sat.Same_sign else Sidekick_sat.Negated end module Eq_class = CC.N module Expl = CC.Expl @@ -243,23 +243,27 @@ module Make(A : ARG) let on_model_gen self f = self.mk_model <- f :: self.mk_model let push_decision (_self:t) (acts:actions) (lit:lit) : unit = + let (module A) = acts in let sign = Lit.sign lit in - acts.Msat.acts_add_decision_lit (Lit.abs lit) sign + A.add_decision_lit (Lit.abs lit) sign - let[@inline] raise_conflict self acts c proof : 'a = + let[@inline] raise_conflict self (acts:actions) c proof : 'a = + let (module A) = acts in Stat.incr self.count_conflict; - acts.Msat.acts_raise_conflict c proof + A.raise_conflict c proof - let[@inline] propagate self acts p ~reason : unit = + let[@inline] propagate self (acts:actions) p ~reason : unit = + let (module A) = acts in Stat.incr self.count_propagate; - acts.Msat.acts_propagate p (Msat.Consequence reason) + A.propagate p (Sidekick_sat.Consequence reason) let[@inline] propagate_l self acts p cs proof : unit = propagate self acts p ~reason:(fun()->cs,proof) - let add_sat_clause_ self acts ~keep lits (proof:P.t) : unit = + let add_sat_clause_ self (acts:actions) ~keep lits (proof:P.t) : unit = + let (module A) = acts in Stat.incr self.count_axiom; - acts.Msat.acts_add_clause ~keep lits proof + A.add_clause ~keep lits proof let preprocess_term_ (self:t) ~add_clause (t:term) : term * proof = let mk_lit t = Lit.atom self.tst t in (* no further simplification *) @@ -377,7 +381,9 @@ module Make(A : ARG) let[@inline] add_clause_permanent self acts lits (proof:P.t) : unit = add_sat_clause_ self acts ~keep:true lits proof - let add_lit _self acts lit : unit = acts.Msat.acts_mk_lit lit + let[@inline] add_lit _self (acts:actions) lit : unit = + let (module A) = acts in + A.mk_lit lit let add_lit_t self acts ?sign t = let lit = mk_lit self acts ?sign t in @@ -429,7 +435,7 @@ module Make(A : ARG) (* handle a literal assumed by the SAT solver *) let assert_lits_ ~final (self:t) (acts:actions) (lits:Lit.t Iter.t) : unit = - Msat.Log.debugf 2 + Log.debugf 2 (fun k->k "(@[@{msat-solver.assume_lits@}%s[lvl=%d]@ %a@])" (if final then "[final]" else "") self.level (Util.pp_iter ~sep:"; " Lit.pp) lits); (* transmit to CC *) @@ -456,28 +462,26 @@ module Make(A : ARG) ); () - let[@inline] iter_atoms_ acts : _ Iter.t = + let[@inline] iter_atoms_ (acts:actions) : _ Iter.t = fun f -> - acts.Msat.acts_iter_assumptions - (function - | Msat.Lit a -> f a - | Msat.Assign _ -> assert false) + let (module A) = acts in + A.iter_assumptions f (* propagation from the bool solver *) let check_ ~final (self:t) (acts: msat_acts) = let pb = if final then Profile.begin_ "solver.final-check" else Profile.null_probe in let iter = iter_atoms_ acts in - Msat.Log.debugf 5 (fun k->k "(msat-solver.assume :len %d)" (Iter.length iter)); + Log.debugf 5 (fun k->k "(msat-solver.assume :len %d)" (Iter.length iter)); self.on_progress(); assert_lits_ ~final self acts iter; Profile.exit pb (* propagation from the bool solver *) - let[@inline] partial_check (self:t) (acts:_ Msat.acts) : unit = + let[@inline] partial_check (self:t) (acts:_ Sidekick_sat.acts) : unit = check_ ~final:false self acts (* perform final check of the model *) - let[@inline] final_check (self:t) (acts:_ Msat.acts) : unit = + let[@inline] final_check (self:t) (acts:_ Sidekick_sat.acts) : unit = check_ ~final:true self acts let create ~stat (tst:Term.store) (ty_st:Ty.store) () : t = @@ -510,7 +514,7 @@ module Make(A : ARG) module Lit = Solver_internal.Lit (** the parametrized SAT Solver *) - module Sat_solver = Msat.Make_cdcl_t(Solver_internal) + module Sat_solver = Sidekick_sat.Make_cdcl_t(Solver_internal) module Atom = Sat_solver.Atom @@ -519,7 +523,7 @@ module Make(A : ARG) module SC = Sat_solver.Clause type t = { - msat: Sat_solver.proof; + msat: Sat_solver.Proof.t; tdefs: (term*term) list; (* term definitions *) p: P.t lazy_t; } @@ -528,7 +532,7 @@ module Make(A : ARG) let pp_dot = let module Dot = - Msat_backend.Dot.Make(Sat_solver)(Msat_backend.Dot.Default(Sat_solver)) in + Sidekick_backend.Dot.Make(Sat_solver)(Sidekick_backend.Dot.Default(Sat_solver)) in let pp out self = Dot.pp out self.msat in Some pp @@ -541,7 +545,7 @@ module Make(A : ARG) clause [c] under given assumptions (each assm is a lit), and return [-a1 \/ … \/ -an \/ c], discharging assumptions *) - let conv_proof (msat:Sat_solver.proof) (t_defs:_ list) : P.t = + let conv_proof (msat:Sat_solver.Proof.t) (t_defs:_ list) : P.t = let assms = ref [] in let steps = ref [] in @@ -549,7 +553,7 @@ module Make(A : ARG) let n_tbl_: string SC.Tbl.t = SC.Tbl.create 32 in (* node.concl -> unique idx *) (* name of an already processed proof node *) - let find_proof_name (p:Sat_solver.proof) : string = + let find_proof_name (p:Sat_solver.Proof.t) : string = try SC.Tbl.find n_tbl_ (SP.conclusion p) with Not_found -> Error.errorf @@ -633,7 +637,7 @@ module Make(A : ARG) let t_defs = CCList.map (fun (c,rhs) -> P.deft c rhs) t_defs in P.composite_l ~assms (CCList.append t_defs (List.rev !steps)) - let make (msat: Sat_solver.proof) (tdefs: _ list) : t = + let make (msat: Sat_solver.Proof.t) (tdefs: _ list) : t = { msat; tdefs; p=lazy (conv_proof msat tdefs) } let check self = SP.check self.msat @@ -912,22 +916,22 @@ module Make(A : ARG) let r = Sat_solver.solve ~assumptions (solver self) in Stat.incr self.count_solve; match r with - | Sat_solver.Sat st -> + | Sat_solver.Sat (module SAT) -> Log.debug 1 "sidekick.msat-solver: SAT"; - let _lits f = st.iter_trail f (fun _ -> ()) in + let _lits f = SAT.iter_trail f in (* TODO: theory combination *) let m = mk_model self _lits in do_on_exit (); Sat m - | Sat_solver.Unsat us -> + | Sat_solver.Unsat (module UNSAT) -> let proof = lazy ( try - let pr = us.get_proof () in + let pr = UNSAT.get_proof () in if check then Sat_solver.Proof.check pr; Some (Pre_proof.make pr (List.rev self.si.t_defs)) - with Msat.Solver_intf.No_proof -> None + with Sidekick_sat.Solver_intf.No_proof -> None ) in - let unsat_core = lazy (us.Msat.unsat_assumptions ()) in + let unsat_core = lazy (UNSAT.unsat_assumptions ()) in do_on_exit (); Unsat {proof; unsat_core} diff --git a/src/msat-solver/dune b/src/msat-solver/dune index 2a945b95..78d55808 100644 --- a/src/msat-solver/dune +++ b/src/msat-solver/dune @@ -2,5 +2,5 @@ (name Sidekick_msat_solver) (public_name sidekick.msat-solver) (libraries containers iter sidekick.core sidekick.util - sidekick.cc msat msat.backend) + sidekick.cc sidekick.sat sidekick.backend) (flags :standard -open Sidekick_util)) diff --git a/src/sat/.gitignore b/src/sat/.gitignore new file mode 100644 index 00000000..f07c6d70 --- /dev/null +++ b/src/sat/.gitignore @@ -0,0 +1,13 @@ +_build/ +*.annot +*.native +*.log +*.status +.*.swp +.session +*.docdir +src/util/log.ml +doc/index.html +*.exe +.merlin +*.install diff --git a/src/sat/CHANGELOG.md b/src/sat/CHANGELOG.md new file mode 100644 index 00000000..0efb4bb4 --- /dev/null +++ b/src/sat/CHANGELOG.md @@ -0,0 +1,118 @@ +# CHANGES + +## 0.9.1 + +- add `on_conflit` callback +- fix termination issue when using `push_decision_lit` from plugin + +## 0.9 + +- feat: allow the theory to ask for some literals to be decided on +- feat: allow to set the default polarity of variables at creation time + +## 0.8.3 + +- support containers 3.0 + +## 0.8.2 + +- fix opam file +- fix: allow conflicts below decision level in `Make_cdcl_t` + +## 0.8.1 + +- fixes in `Heap` +- package for `msat-bin` +- use `iter` instead of `sequence` in dune and opam files +- more docs + +## 0.8 + +big refactoring, change of API with fewer functions, etc. +see `git log` for more details. + +## 0.6.1 + +- add simple functor for DOT backend +- various bugfixes + +## 0.6 + +### Feature + +- An already instantiated sat solver in the Sat module +- A `full_slice` function for running possibly expensive satisfiability + tests (in SMT) when a propositional model has been found +- Forgetful propagations: propagations whose reason (i.e clause) is not watched + +## 0.5.1 + +### Bug + +- Removed some needless allocations + +### Breaking + +- Better interface for mcsat propagations + +### Feature + +- Allow level 0 semantic propagations + +## 0.5 + +### Bug + +- Grow heap when adding local hyps +- Avoid forgetting some one atom clauses +- Fixed a bug for propagations at level 0 +- Late propagations need to be re-propagated +- Fixed conflict at level 0 +- Avoid forgetting some theory conflict clauses + +### Breaking + +- Changed `if_sat` interface + +## 0.4.1 + +### Bug + +- fix bug in `add_clause` + +## 0.4 + +- performance improvements +- many bugfixes +- more tests + +### Breaking + +- remove push/pop (source of many bugs) +- replaced by solve : assumptions:lit list -> unit -> result + +### Features + +- Accept late conflict clauses +- cleaner API, moving some types outside the client-required interface + +## 0.3 + +### Features + +- Proofs for atoms at level 0 +- Compatibility with ocaml >= 4.00 +- Released some restrictions on dummy sat theories + +## 0.2 + +### Breaking + +- Log argument has been removed from functors +- All the functors now take a dummy last argument to ensure the solver modules are unique + +### Features + +- push/pop operations +- access to decision level when evaluating literals + diff --git a/src/sat/Heap.ml b/src/sat/Heap.ml new file mode 100644 index 00000000..ed9884bb --- /dev/null +++ b/src/sat/Heap.ml @@ -0,0 +1,145 @@ + +module type RANKED = Heap_intf.RANKED + +module type S = Heap_intf.S + +module Make(Elt : RANKED) = struct + type elt = Elt.t + + type t = { + heap : elt Vec.t; + } [@@unboxed] + + let _absent_index = -1 + + let create () = + { heap = Vec.create(); } + + let[@inline] left i = (i lsl 1) + 1 (* i*2 + 1 *) + let[@inline] right i = (i + 1) lsl 1 (* (i+1)*2 *) + let[@inline] parent i = (i - 1) asr 1 (* (i-1) / 2 *) + + (* + let rec heap_property cmp ({heap=heap} as s) i = + i >= (Vec.size heap) || + ((i = 0 || not(cmp (Vec. get heap i) (Vec.get heap (parent i)))) + && heap_property cmp s (left i) && heap_property cmp s (right i)) + + let heap_property cmp s = heap_property cmp s 1 + *) + + (* [elt] is above or at its expected position. Move it up the heap + (towards high indices) to restore the heap property *) + let percolate_up {heap} (elt:Elt.t) : unit = + let pi = ref (parent (Elt.idx elt)) in + let i = ref (Elt.idx elt) in + while !i <> 0 && Elt.cmp elt (Vec.get heap !pi) do + Vec.set heap !i (Vec.get heap !pi); + Elt.set_idx (Vec.get heap !i) !i; + i := !pi; + pi := parent !i + done; + Vec.set heap !i elt; + Elt.set_idx elt !i + + let percolate_down {heap} (elt:Elt.t): unit = + let sz = Vec.size heap in + let li = ref (left (Elt.idx elt)) in + let ri = ref (right (Elt.idx elt)) in + let i = ref (Elt.idx elt) in + begin + try + while !li < sz do + let child = + if !ri < sz && Elt.cmp (Vec.get heap !ri) (Vec.get heap !li) + then !ri + else !li + in + if not (Elt.cmp (Vec.get heap child) elt) then raise Exit; + Vec.set heap !i (Vec.get heap child); + Elt.set_idx (Vec.get heap !i) !i; + i := child; + li := left !i; + ri := right !i + done; + with Exit -> () + end; + Vec.set heap !i elt; + Elt.set_idx elt !i + + let[@inline] in_heap x = Elt.idx x >= 0 + + let[@inline] decrease s x = assert (in_heap x); percolate_up s x + + (* + let increase cmp s n = + assert (in_heap s n); percolate_down cmp s (V.get s.indices n) + *) + + let filter s filt = + let j = ref 0 in + let lim = Vec.size s.heap in + for i = 0 to lim - 1 do + if filt (Vec.get s.heap i) then ( + Vec.set s.heap !j (Vec.get s.heap i); + Elt.set_idx (Vec.get s.heap i) !j; + incr j; + ) else ( + Elt.set_idx (Vec.get s.heap i) _absent_index; + ); + done; + Vec.shrink s.heap (lim - !j); + for i = (lim / 2) - 1 downto 0 do + percolate_down s (Vec.get s.heap i) + done + + let size s = Vec.size s.heap + + let is_empty s = Vec.is_empty s.heap + + let clear {heap} = + Vec.iter (fun e -> Elt.set_idx e _absent_index) heap; + Vec.clear heap; + () + + let insert s elt = + if not (in_heap elt) then ( + Elt.set_idx elt (Vec.size s.heap); + Vec.push s.heap elt; + percolate_up s elt; + ) + + (* + let update cmp s n = + assert (heap_property cmp s); + begin + if in_heap s n then + begin + percolate_up cmp s (Vec.get s.indices n); + percolate_down cmp s (Vec.get s.indices n) + end + else insert cmp s n + end; + assert (heap_property cmp s) + *) + + let remove_min ({heap} as s) = + match Vec.size heap with + | 0 -> raise Not_found + | 1 -> + let x = Vec.pop heap in + Elt.set_idx x _absent_index; + x + | _ -> + let x = Vec.get heap 0 in + let new_hd = Vec.pop heap in (* heap.last() *) + Vec.set heap 0 new_hd; + Elt.set_idx x _absent_index; + Elt.set_idx new_hd 0; + (* enforce heap property again *) + if Vec.size heap > 1 then ( + percolate_down s new_hd; + ); + x + +end [@@inline] diff --git a/src/sat/Heap.mli b/src/sat/Heap.mli new file mode 100644 index 00000000..a621885c --- /dev/null +++ b/src/sat/Heap.mli @@ -0,0 +1,5 @@ +module type RANKED = Heap_intf.RANKED + +module type S = Heap_intf.S + +module Make(X : RANKED) : S with type elt = X.t diff --git a/src/sat/Heap_intf.ml b/src/sat/Heap_intf.ml new file mode 100644 index 00000000..e7d4aee7 --- /dev/null +++ b/src/sat/Heap_intf.ml @@ -0,0 +1,51 @@ + +module type RANKED = sig + type t + + val idx: t -> int + (** Index in heap. return -1 if never set *) + + val set_idx : t -> int -> unit + (** Update index in heap *) + + val cmp : t -> t -> bool +end + +module type S = sig + type elt + (** Type of elements *) + + type t + (** Heap of {!elt}, whose priority is increased or decreased + incrementally (see {!decrease} for instance) *) + + val create : unit -> t + (** Create a heap *) + + val decrease : t -> elt -> unit + (** [decrease h x] decreases the value associated to [x] within [h] *) + + val in_heap : elt -> bool + + (*val increase : (int -> int -> bool) -> t -> int -> unit*) + + val size : t -> int + (** Number of integers within the heap *) + + val is_empty : t -> bool + + val clear : t -> unit + (** Clear the content of the heap *) + + val insert : t -> elt -> unit + (** Insert a new element into the heap *) + + (*val update : (int -> int -> bool) -> t -> int -> unit*) + + val remove_min : t -> elt + (** Remove and return the integer that has the lowest value from the heap + @raise Not_found if the heap is empty *) + + val filter : t -> (elt -> bool) -> unit + (** Filter out values that don't satisfy the predicate *) +end diff --git a/src/sat/README.md b/src/sat/README.md new file mode 100644 index 00000000..8cf81dcc --- /dev/null +++ b/src/sat/README.md @@ -0,0 +1,188 @@ +# MSAT [![Build Status](https://travis-ci.org/Gbury/mSAT.svg?branch=master)](https://travis-ci.org/Gbury/mSAT) + +MSAT is an OCaml library that features a modular SAT-solver and some +extensions (including SMT), derived from [Alt-Ergo Zero](http://cubicle.lri.fr/alt-ergo-zero). + +It was presented at [ICFP 2017](https://icfp17.sigplan.org/event/ocaml-2017-papers-msat-an-ocaml-sat-solver), +using a [poster](https://github.com/Gbury/mSAT/blob/master/articles/icfp_2017.pdf) + + +## COPYRIGHT + +This program is distributed under the Apache Software License version +2.0. See the enclosed file `LICENSE`. + +## Documentation + +See https://gbury.github.io/mSAT/ + +## INSTALLATION + +### Via opam + +Once the package is on [opam](http://opam.ocaml.org), just `opam install msat`. +For the development version, use: + +``` +opam pin add msat https://github.com/Gbury/mSAT.git +``` + +### Manual installation + +You will need `dune` and `iter`. The command is: + +``` +$ make install +``` + +## USAGE + +### Generic SAT/SMT Solver + +A modular implementation of the SMT algorithm can be found in the `Msat.Solver` module, +as a functor which takes two modules : + + - A representation of formulas (which implements the `Formula_intf.S` signature) + + - A theory (which implements the `Theory_intf.S` signature) to check consistence of assertions. + + - A dummy empty module to ensure generativity of the solver (solver modules heavily relies on + side effects to their internal state) + +### Sat Solver + +A ready-to-use SAT solver is available in the `Msat_sat` module +using the `msat.sat` library. It can be loaded +as shown in the following code : + +```ocaml +# #require "msat";; +# #require "msat.sat";; +# #print_depth 0;; (* do not print details *) +``` + +Then we can create a solver and create some boolean variables: + +```ocaml +module Sat = Msat_sat +module E = Sat.Int_lit (* expressions *) + +let solver = Sat.create() + +(* We create here two distinct atoms *) +let a = E.fresh () (* A 'new_atom' is always distinct from any other atom *) +let b = E.make 1 (* Atoms can be created from integers *) +``` + +We can try and check the satisfiability of some clauses — here, the clause `a or b`. +`Sat.assume` adds a list of clauses to the solver. Calling `Sat.solve` +will check the satisfiability of the current set of clauses, here "Sat". + +```ocaml +# a <> b;; +- : bool = true +# Sat.assume solver [[a; b]] ();; +- : unit = () +# let res = Sat.solve solver;; +val res : Sat.res = Sat.Sat ... +``` + +The Sat solver has an incremental mutable state, so we still have +the clause `a or b` in our assumptions. +We add `not a` and `not b` to the state, and get "Unsat". + +```ocaml +# Sat.assume solver [[E.neg a]; [E.neg b]] () ;; +- : unit = () +# let res = Sat.solve solver ;; +val res : Sat.res = Sat.Unsat ... +``` + +#### Formulas API + +Writing clauses by hand can be tedious and error-prone. +The functor `Msat_tseitin.Make` in the library `msat.tseitin` +proposes a formula AST (parametrized by +atoms) and a function to convert these formulas into clauses: + +```ocaml +# #require "msat.tseitin";; +``` + +```ocaml +(* Module initialization *) +module F = Msat_tseitin.Make(E) + +let solver = Sat.create () + +(* We create here two distinct atoms *) +let a = E.fresh () (* A fresh atom is always distinct from any other atom *) +let b = E.make 1 (* Atoms can be created from integers *) + +(* Let's create some formulas *) +let p = F.make_atom a +let q = F.make_atom b +let r = F.make_and [p; q] +let s = F.make_or [F.make_not p; F.make_not q] +``` + +We can try and check the satisfiability of the given formulas, by turning +it into clauses using `make_cnf`: + +```ocaml +# Sat.assume solver (F.make_cnf r) ();; +- : unit = () +# Sat.solve solver;; +- : Sat.res = Sat.Sat ... +``` + +```ocaml +# Sat.assume solver (F.make_cnf s) ();; +- : unit = () +# Sat.solve solver ;; +- : Sat.res = Sat.Unsat ... +``` + +### CDCL(T): a Sudoku solver as an example + +The directory `src/sudoku/` contains a simple Sudoku solver that +uses the interface `Msat.Make_cdcl_t`. +In essence, it implements the logical theory `CDCL(Sudoku)`. +The script `sudoku_solve.sh` compiles and runs the solver, +as does `dune exec src/sudoku/sudoku_solve.exe`. + +It's able to parse sudoku grids denoted as 81 integers +(see `tests/sudoku/sudoku.txt` for example). + +Here is a sample grid and the output from the solver (in roughly .5s): + +```sh non-deterministic=command +$ echo '..............3.85..1.2.......5.7.....4...1...9.......5......73..2.1........4...9' > sudoku.txt +$ dune exec src/sudoku/sudoku_solve.exe -- sudoku.txt +... +######################### +solve grid: + ......... + .....3.85 + ..1.2.... + ...5.7... + ..4...1.. + .9....... + 5......73 + ..2.1.... + ....4...9 + +... + 987654321 + 246173985 + 351928746 + 128537694 + 634892157 + 795461832 + 519286473 + 472319568 + 863745219 + +################### +... +``` diff --git a/src/sat/Sidekick_sat.ml b/src/sat/Sidekick_sat.ml new file mode 100644 index 00000000..873fb9b7 --- /dev/null +++ b/src/sat/Sidekick_sat.ml @@ -0,0 +1,39 @@ +(** Main API *) + + +module Solver_intf = Solver_intf + +module type S = Solver_intf.S +module type FORMULA = Solver_intf.FORMULA +module type PLUGIN_CDCL_T = Solver_intf.PLUGIN_CDCL_T +module type PROOF = Solver_intf.PROOF + +type lbool = Solver_intf.lbool = L_true | L_false | L_undefined + +module type SAT_STATE = Solver_intf.SAT_STATE +type 'form sat_state = 'form Solver_intf.sat_state + +type ('formula, 'proof) reason = ('formula, 'proof) Solver_intf.reason = + | Consequence of (unit -> 'formula list * 'proof) [@@unboxed] + +module type ACTS = Solver_intf.ACTS +type ('formula, 'proof) acts = ('formula, 'proof) Solver_intf.acts + +type negated = Solver_intf.negated = Negated | Same_sign + +(** Print {!negated} values *) +let pp_negated out = function + | Negated -> Format.fprintf out "negated" + | Same_sign -> Format.fprintf out "same-sign" + +(** Print {!lbool} values *) +let pp_lbool out = function + | L_true -> Format.fprintf out "true" + | L_false -> Format.fprintf out "false" + | L_undefined -> Format.fprintf out "undefined" + +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 new file mode 100644 index 00000000..c341673b --- /dev/null +++ b/src/sat/Solver.ml @@ -0,0 +1,1940 @@ + +module type PLUGIN = sig + val has_theory : bool + (** [true] iff the solver is parametrized by a theory, not just + pure SAT. *) + + include Solver_intf.PLUGIN_CDCL_T +end + +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 ("sidekick.sat: " ^ msg)) fmt + +module Make(Plugin : PLUGIN) += struct + module Formula = Plugin.Formula + + type formula = Formula.t + type theory = Plugin.t + type lemma = Plugin.proof + + type var = { + vid : int; + pa : atom; + na : atom; + mutable v_fields : int; + mutable v_level : int; + mutable v_idx: int; (** position in heap *) + mutable v_weight : float; (** Weight (for the heap), tracking activity *) + mutable reason : reason option; + } + + and atom = { + aid : int; + var : var; + neg : atom; + lit : formula; + mutable is_true : bool; + watched : clause Vec.t; + } + + and clause = { + cid: int; + atoms : atom array; + mutable cpremise : premise; + mutable activity : float; + mutable flags: int; (* bitfield *) + } + + and reason = + | Decision + | Bcp of clause + | Bcp_lazy of clause lazy_t + + (* TODO: remove, replace with user-provided proof trackng device? + for pure SAT, [reason] is sufficient *) + and premise = + | Hyp of lemma + | Local + | Lemma of lemma + | History of clause list + | Empty_premise + + (* 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; + mutable cpt_mk_var: int; + mutable cpt_mk_clause: int; + } + + let create_st ?(size=`Big) () : st = + let size_map = match size with + | `Tiny -> 8 + | `Small -> 16 + | `Big -> 4096 + in + { f_map = MF.create size_map; + vars = Vec.create(); + cpt_mk_var = 0; + cpt_mk_clause = 0; + } + + let nb_elt st = Vec.size st.vars + let get_elt st i = Vec.get st.vars i + let iter_elt st f = Vec.iter f st.vars + + 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 + let seen_pos = 0b10 + let seen_neg = 0b100 + let default_pol_true = 0b1000 + + module Var = struct + let[@inline] level v = v.v_level + let[@inline] pos v = v.pa + let[@inline] neg v = v.na + let[@inline] reason v = v.reason + let[@inline] weight v = v.v_weight + let[@inline] set_weight v w = v.v_weight <- w + let[@inline] mark v = v.v_fields <- v.v_fields lor seen_var + let[@inline] unmark v = v.v_fields <- v.v_fields land (lnot seen_var) + let[@inline] marked v = (v.v_fields land seen_var) <> 0 + let[@inline] set_default_pol_true v = v.v_fields <- v.v_fields lor default_pol_true + let[@inline] set_default_pol_false v = v.v_fields <- v.v_fields land (lnot default_pol_true) + let[@inline] default_pol v = (v.v_fields land default_pol_true) <> 0 + let[@inline] idx v = v.v_idx + let[@inline] set_idx v i = v.v_idx <- i + + let make ?(default_pol=true) (st:st) (t:formula) : var * Solver_intf.negated = + let lit, negated = Formula.norm t in + try + MF.find st.f_map lit, negated + with Not_found -> + let cpt_double = st.cpt_mk_var lsl 1 in + let rec var = + { vid = st.cpt_mk_var; + pa = pa; + na = na; + v_fields = 0; + v_level = -1; + v_idx= -1; + v_weight = 0.; + reason = None; + } + and pa = + { var = var; + lit = lit; + watched = Vec.create(); + neg = na; + is_true = false; + aid = cpt_double (* aid = vid*2 *) } + and na = + { var = var; + lit = Formula.neg lit; + watched = Vec.create(); + neg = pa; + is_true = false; + aid = cpt_double + 1 (* aid = vid*2+1 *) } in + MF.add st.f_map lit var; + st.cpt_mk_var <- st.cpt_mk_var + 1; + if default_pol then set_default_pol_true var; + Vec.push st.vars var; + var, negated + + (* Marking helpers *) + let[@inline] clear v = + v.v_fields <- 0 + + let[@inline] seen_both v = + (seen_pos land v.v_fields <> 0) && + (seen_neg land v.v_fields <> 0) + end + + module Atom = struct + type t = atom + let[@inline] level a = a.var.v_level + let[@inline] var a = a.var + let[@inline] neg a = a.neg + let[@inline] abs a = a.var.pa + let[@inline] formula a = a.lit + let[@inline] equal a b = a == b + let[@inline] sign a = a == abs a + let[@inline] hash a = Hashtbl.hash a.aid + let[@inline] compare a b = compare a.aid b.aid + let[@inline] reason a = Var.reason a.var + let[@inline] id a = a.aid + let[@inline] is_true a = a.is_true + let[@inline] is_false a = a.neg.is_true + let has_value a = is_true a || is_false a + + let[@inline] seen a = + if sign a + then (seen_pos land a.var.v_fields <> 0) + else (seen_neg land a.var.v_fields <> 0) + + let[@inline] mark a = + let pos = equal a (abs a) in + if pos then ( + a.var.v_fields <- seen_pos lor a.var.v_fields + ) else ( + a.var.v_fields <- seen_neg lor a.var.v_fields + ) + + let[@inline] make ?default_pol st lit = + let var, negated = Var.make ?default_pol st lit in + match negated with + | Solver_intf.Negated -> var.na + | Solver_intf.Same_sign -> var.pa + + let pp fmt a = Formula.pp fmt a.lit + + let pp_a fmt v = + if Array.length v = 0 then ( + Format.fprintf fmt "∅" + ) else ( + pp fmt v.(0); + if (Array.length v) > 1 then begin + for i = 1 to (Array.length v) - 1 do + Format.fprintf fmt " ∨ %a" pp v.(i) + done + end + ) + + (* Complete debug printing *) + let pp_sign a = if a == a.var.pa then "+" else "-" + + let debug_reason fmt = function + | n, _ when n < 0 -> + Format.fprintf fmt "%%" + | n, None -> + Format.fprintf fmt "%d" n + | n, Some Decision -> + Format.fprintf fmt "@@%d" n + | n, Some Bcp c -> + Format.fprintf fmt "->%d/%s/%d" n (kind_of_clause c) c.cid + | n, Some (Bcp_lazy _) -> + Format.fprintf fmt "->%d/" n + + let pp_level fmt a = + debug_reason fmt (a.var.v_level, a.var.reason) + + let debug_value fmt a = + if a.is_true then + Format.fprintf fmt "T%a" pp_level a + else if a.neg.is_true then + Format.fprintf fmt "F%a" pp_level a + else + Format.fprintf fmt "" + + let debug out a = + Format.fprintf out "%s%d[%a][atom:@[%a@]]" + (pp_sign a) (a.var.vid+1) debug_value a Formula.pp a.lit + + let debug_a out vec = + Array.iter (fun a -> Format.fprintf out "%a@ " debug a) vec + let debug_l out l = + List.iter (fun a -> Format.fprintf out "%a@ " debug a) l + + module Set = Set.Make(struct type t=atom let compare=compare end) + end + + module Clause = struct + type t = clause + + let make_a = + let n = ref 0 in + fun ~flags atoms premise -> + let cid = !n in + incr n; + { cid; + atoms = atoms; + flags; + activity = 0.; + cpremise = premise} + + let make ~flags l premise = make_a ~flags (Array.of_list l) premise + + let empty = make [] (History []) + let[@inline] equal c1 c2 = c1.cid = c2.cid + let[@inline] hash c = Hashtbl.hash c.cid + let[@inline] atoms c = c.atoms + let[@inline] atoms_seq c = Iter.of_array c.atoms + let[@inline] atoms_l c = Array.to_list c.atoms + + let flag_attached = 0b1 + let flag_visited = 0b10 + let flag_removable = 0b100 + let flag_dead = 0b1000 + + let[@inline] make_removable l premise = make ~flags:flag_removable l premise + let[@inline] make_removable_a l premise = make_a ~flags:flag_removable l premise + let[@inline] make_permanent l premise = make ~flags:0 l premise + + let[@inline] visited c = (c.flags land flag_visited) <> 0 + let[@inline] set_visited c b = + if b then c.flags <- c.flags lor flag_visited + else c.flags <- c.flags land lnot flag_visited + + let[@inline] attached c = (c.flags land flag_attached) <> 0 + let[@inline] set_attached c b = + if b then c.flags <- c.flags lor flag_attached + else c.flags <- c.flags land lnot flag_attached + + let[@inline] removable c = (c.flags land flag_removable) <> 0 + let[@inline] set_removable c b = + if b then c.flags <- c.flags lor flag_removable + else c.flags <- c.flags land lnot flag_removable + + let[@inline] dead c = (c.flags land flag_dead) <> 0 + let[@inline] set_dead c = c.flags <- c.flags lor flag_dead + + let[@inline] activity c = c.activity + let[@inline] set_activity c w = c.activity <- w + + module Tbl = Hashtbl.Make(struct + type t = clause + let hash = hash + 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 "(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 -> + 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 + "(@[cl[%s%d]@ {@[%a@]}@ :premise %a@])" + (kind_of_clause c) c.cid Atom.debug_a arr debug_premise cp + end + + module Proof = struct + exception Resolution_error of string + + type atom = Atom.t + type clause = Clause.t + type formula = Formula.t + type lemma = Plugin.proof + + let error_res_f msg = Format.kasprintf (fun s -> raise (Resolution_error s)) msg + + let[@inline] clear_var_of_ (a:atom) = Var.clear a.var + + (* Compute resolution of 2 clauses. + returns [pivots, resulting_atoms] *) + let resolve (c1:clause) (c2:clause) : atom list * atom list = + (* invariants: only atoms in [c2] are marked, and the pivot is + cleared when traversing [c1] *) + Array.iter Atom.mark c2.atoms; + let pivots = ref [] in + let l = + Array.fold_left + (fun l a -> + if Atom.seen a then l + else if Atom.seen a.neg then ( + pivots := a.var.pa :: !pivots; + clear_var_of_ a; + l + ) else a::l) + [] c1.atoms + in + let l = + Array.fold_left (fun l a -> if Atom.seen a then a::l else l) l c2.atoms + in + Array.iter clear_var_of_ c2.atoms; + !pivots, l + + (* [find_dups c] returns a list of duplicate atoms, and the deduplicated list *) + let find_dups (c:clause) : atom list * atom list = + let res = + Array.fold_left + (fun (dups,l) a -> + if Atom.seen a then ( + a::dups, l + ) else ( + Atom.mark a; + dups, a::l + )) + ([], []) c.atoms + in + Array.iter clear_var_of_ c.atoms; + res + + (* do [c1] and [c2] have the same lits, modulo reordering and duplicates? *) + let same_lits (c1:atom Iter.t) (c2:atom Iter.t): bool = + let subset a b = + Iter.iter Atom.mark b; + let res = Iter.for_all Atom.seen a in + Iter.iter clear_var_of_ b; + res + in + subset c1 c2 && subset c2 c1 + + let prove conclusion = + match conclusion.cpremise with + | History [] -> assert false + | Empty_premise -> raise Solver_intf.No_proof + | _ -> conclusion + + let rec set_atom_proof a = + let aux acc b = + if Atom.equal a.neg b then acc + else set_atom_proof b :: acc + in + assert (a.var.v_level >= 0); + match (a.var.reason) with + | Some (Bcp c | Bcp_lazy (lazy c)) -> + Log.debugf 5 (fun k->k "(@[proof.analyze.clause@ :atom %a@ :c %a@])" Atom.debug a Clause.debug c); + if Array.length c.atoms = 1 then ( + Log.debugf 5 (fun k -> k "(@[proof.analyze.old-reason@ %a@])" Atom.debug a); + c + ) else ( + assert (a.neg.is_true); + let r = History (c :: (Array.fold_left aux [] c.atoms)) in + let c' = Clause.make_permanent [a.neg] r in + a.var.reason <- Some (Bcp c'); + Log.debugf 5 + (fun k -> k "(@[proof.analyze.new-reason@ :atom %a@ :c %a@])" Atom.debug a Clause.debug c'); + c' + ) + | _ -> + error_res_f "cannot prove atom %a" Atom.debug a + + let prove_unsat conflict = + if Array.length conflict.atoms = 0 then ( + conflict + ) else ( + Log.debugf 1 (fun k -> k "(@[sat.prove-unsat@ :from %a@])" Clause.debug conflict); + let l = Array.fold_left (fun acc a -> set_atom_proof a :: acc) [] conflict.atoms in + let res = Clause.make_permanent [] (History (conflict :: l)) in + Log.debugf 1 (fun k -> k "(@[sat.proof-found@ %a@])" Clause.debug res); + res + ) + + let prove_atom a = + if a.is_true && a.var.v_level = 0 then + Some (set_atom_proof a) + else + None + + type t = clause + and proof_node = { + conclusion : clause; + step : step; + } + and step = + | Hypothesis of lemma + | Assumption + | Lemma of lemma + | Duplicate of t * atom list + | Hyper_res of hyper_res_step + + and hyper_res_step = { + hr_init: t; + hr_steps: (atom * t) list; (* list of pivot+clause to resolve against [init] *) + } + + let[@inline] conclusion (p:t) : clause = p + + (* find pivots for resolving [l] with [init], and also return + the atoms of the conclusion *) + let find_pivots (init:clause) (l:clause list) : _ * (atom * t) list = + Log.debugf 15 + (fun k->k "(@[proof.find-pivots@ :init %a@ :l %a@])" + Clause.debug init (Format.pp_print_list Clause.debug) l); + Array.iter Atom.mark init.atoms; + let steps = + List.map + (fun c -> + let pivot = + match + Iter.of_array c.atoms + |> Iter.filter (fun a -> Atom.seen (Atom.neg a)) + |> Iter.to_list + with + | [a] -> a + | [] -> + error_res_f "(@[proof.expand.pivot_missing@ %a@])" Clause.debug c + | pivots -> + error_res_f "(@[proof.expand.multiple_pivots@ %a@ :pivots %a@])" + Clause.debug c Atom.debug_l pivots + in + Array.iter Atom.mark c.atoms; (* add atoms to result *) + clear_var_of_ pivot; + Atom.abs pivot, c) + l + in + (* cleanup *) + let res = ref [] in + let cleanup_a_ a = + if Atom.seen a then ( + res := a :: !res; + clear_var_of_ a + ) + in + Array.iter cleanup_a_ init.atoms; + List.iter (fun c -> Array.iter cleanup_a_ c.atoms) l; + !res, steps + + let expand conclusion = + Log.debugf 5 (fun k -> k "(@[sat.proof.expand@ @[%a@]@])" Clause.debug conclusion); + match conclusion.cpremise with + | Lemma l -> + { conclusion; step = Lemma l; } + | Local -> + { conclusion; step = Assumption; } + | Hyp l -> + { conclusion; step = Hypothesis l; } + | History [] -> + error_res_f "@[empty history for clause@ %a@]" Clause.debug conclusion + | History [c] -> + let duplicates, res = find_dups c in + assert (same_lits (Iter.of_list res) (Clause.atoms_seq conclusion)); + { conclusion; step = Duplicate (c, duplicates) } + | History (c :: r) -> + let res, steps = find_pivots c r in + assert (same_lits (Iter.of_list res) (Clause.atoms_seq conclusion)); + { conclusion; step = Hyper_res {hr_init=c; hr_steps=steps}; } + | Empty_premise -> raise Solver_intf.No_proof + + let rec res_of_hyper_res (hr: hyper_res_step) : _ * _ * atom = + let {hr_init=c1; hr_steps=l} = hr in + match l with + | [] -> assert false + | [a, c2] -> c1, c2, a (* done *) + | (a,c2) :: steps' -> + (* resolve [c1] with [c2], then resolve that against [steps] *) + let pivots, l = resolve c1 c2 in + assert (match pivots with [a'] -> Atom.equal a a' | _ -> false); + let c_1_2 = Clause.make_removable l (History [c1; c2]) in + res_of_hyper_res {hr_init=c_1_2; hr_steps=steps'} + + (* Proof nodes manipulation *) + let is_leaf = function + | Hypothesis _ + | Assumption + | Lemma _ -> true + | Duplicate _ + | Hyper_res _ -> false + + let parents = function + | Hypothesis _ + | Assumption + | Lemma _ -> [] + | Duplicate (p, _) -> [p] + | Hyper_res {hr_init; hr_steps} -> hr_init :: List.map snd hr_steps + + let expl = function + | Hypothesis _ -> "hypothesis" + | Assumption -> "assumption" + | Lemma _ -> "lemma" + | Duplicate _ -> "duplicate" + | Hyper_res _ -> "hyper-resolution" + + (* Compute unsat-core by accumulating the leaves *) + let unsat_core proof = + let rec aux res acc = function + | [] -> res, acc + | c :: r -> + if not @@ Clause.visited c then ( + Clause.set_visited c true; + match c.cpremise with + | Empty_premise -> raise Solver_intf.No_proof + | Hyp _ | Lemma _ | Local -> aux (c :: res) acc r + | History h -> + let l = List.fold_left (fun acc c -> + if not @@ Clause.visited c then c :: acc else acc) r h in + aux res (c :: acc) l + ) else ( + aux res acc r + ) + in + let res, tmp = aux [] [] [proof] in + List.iter (fun c -> Clause.set_visited c false) res; + List.iter (fun c -> Clause.set_visited c false) tmp; + res + + module Tbl = Clause.Tbl + + type task = + | Enter of t + | Leaving of t + + let spop s = try Some (Stack.pop s) with Stack.Empty -> None + + let rec fold_aux s h f acc = + match spop s with + | None -> acc + | Some (Leaving c) -> + Tbl.add h c true; + fold_aux s h f (f acc (expand c)) + | Some (Enter c) -> + if not (Tbl.mem h c) then begin + Stack.push (Leaving c) s; + let node = expand c in + begin match node.step with + | Duplicate (p1, _) -> + Stack.push (Enter p1) s + | Hyper_res {hr_init=p1; hr_steps=l} -> + List.iter (fun (_,p2) -> Stack.push (Enter p2) s) l; + Stack.push (Enter p1) s; + | Hypothesis _ | Assumption | Lemma _ -> () + end + end; + fold_aux s h f acc + + let fold f acc p = + let h = Tbl.create 42 in + let s = Stack.create () in + Stack.push (Enter p) s; + fold_aux s h f acc + + let check_empty_conclusion (p:t) = + if Array.length p.atoms > 0 then ( + error_res_f "@[<2>Proof.check: non empty conclusion for clause@ %a@]" Clause.debug p; + ) + + let check (p:t) = fold (fun () _ -> ()) () p + end + + module H = (Heap.Make [@specialise]) (struct + type t = var + let[@inline] cmp i j = Var.weight j < Var.weight i (* comparison by weight *) + let idx = Var.idx + let set_idx = Var.set_idx + end) + + (* cause of "unsat", possibly conditional to local assumptions *) + type unsat_cause = + | US_local of { + first: atom; (* assumption which was found to be proved false *) + core: atom list; (* the set of assumptions *) + } + | US_false of clause (* true unsat *) + + exception E_sat + exception E_unsat of unsat_cause + exception UndecidedLit + exception Restart + exception Conflict of clause + + (* Log levels *) + let error = 1 + let warn = 3 + let info = 5 + let debug = 50 + + let var_decay : float = 1. /. 0.95 + (* inverse of the activity factor for variables. Default 1/0.95 *) + + let clause_decay : float = 1. /. 0.999 + (* inverse of the activity factor for clauses. Default 1/0.999 *) + + let restart_inc : float = 1.5 + (* multiplicative factor for restart limit, default 1.5 *) + + let learntsize_inc : float = 1.1 + (* multiplicative factor for [learntsize_factor] at each restart, default 1.1 *) + + (* Singleton type containing the current state *) + type t = { + st : st; + th: theory; + + store_proof: bool; (* do we store proofs? *) + + (* Clauses are simplified for eficiency purposes. In the following + vectors, the comments actually refer to the original non-simplified + clause. *) + + clauses_hyps : clause Vec.t; + (* clauses added by the user *) + clauses_learnt : clause Vec.t; + (* learnt clauses (tautologies true at any time, whatever the user level) *) + + clauses_to_add : clause Vec.t; + (* Clauses either assumed or pushed by the theory, waiting to be added. *) + + mutable unsat_at_0: clause option; + (* conflict at level 0, if any *) + + mutable next_decisions : atom list; + (* When the last conflict was a semantic one (mcsat), + this stores the next decision to make; + if some theory wants atoms to be decided on (for theory combination), + store them here. *) + + trail : atom Vec.t; + (* decision stack + propagated elements (atoms or assignments). *) + + var_levels : int Vec.t; + (* decision levels in [trail] *) + + mutable assumptions: atom Vec.t; + (* current assumptions *) + + mutable th_head : int; + (* Start offset in the queue {!trail} of + unit facts not yet seen by the theory. *) + mutable elt_head : int; + (* Start offset in the queue {!trail} of + unit facts to propagate, within the trail *) + + (* invariant: + - during propagation, th_head <= elt_head + - then, once elt_head reaches length trail, Th.assume is + called so that th_head can catch up with elt_head + - this is repeated until a fixpoint is reached; + - before a decision (and after the fixpoint), + th_head = elt_head = length trail + *) + + order : H.t; + (* Heap ordered by variable activity *) + + to_clear: var Vec.t; + (* variables to unmark *) + + mutable var_incr : float; + (* increment for variables' activity *) + + mutable clause_incr : float; + (* increment for clauses' activity *) + + mutable on_conflict : (atom array -> unit) option; + mutable on_decision : (atom -> unit) option; + mutable on_new_atom: (atom -> unit) option; + } + type solver = t + + (* intial restart limit *) + let restart_first = 100 + + (* initial limit for the number of learnt clauses, 1/3 of initial + number of clauses by default *) + let learntsize_factor = 1. /. 3. + + let _nop_on_conflict (_:atom array) = () + + (* Starting environment. *) + let create_ ~st ~store_proof (th:theory) : t = { + st; th; + unsat_at_0=None; + next_decisions = []; + + clauses_hyps = Vec.create(); + clauses_learnt = Vec.create(); + + clauses_to_add = Vec.create (); + to_clear=Vec.create(); + + th_head = 0; + elt_head = 0; + + trail = Vec.create (); + var_levels = Vec.create(); + assumptions= Vec.create(); + + order = H.create(); + + var_incr = 1.; + clause_incr = 1.; + store_proof; + on_conflict = None; + on_decision= None; + on_new_atom = None; + } + + let create + ?on_conflict ?on_decision ?on_new_atom + ?(store_proof=true) ?(size=`Big) (th:theory) : t = + let st = create_st ~size () in + let st = create_ ~st ~store_proof th in + st.on_new_atom <- on_new_atom; + st.on_decision <- on_decision; + st.on_conflict <- on_conflict; + st + + let[@inline] nb_clauses st = Vec.size st.clauses_hyps + let[@inline] decision_level st = Vec.size st.var_levels + + (* Do we have a level-0 empty clause? *) + let[@inline] check_unsat_ st = + match st.unsat_at_0 with + | Some c -> raise (E_unsat (US_false c)) + | None -> () + + let mk_atom ?default_pol st (f:formula) : atom = + let res = Atom.make ?default_pol st.st f in + res + + (* Variable and literal activity. + Activity is used to decide on which variable to decide when propagation + is done. Uses a heap (implemented in Iheap), to keep track of variable activity. + To be more general, the heap only stores the variable/literal id (i.e an int). + *) + let insert_var_order st (v:var) : unit = + H.insert st.order v + + let make_atom st (p:formula) : atom = + let a = mk_atom st p in + if a.var.v_level < 0 then ( + insert_var_order st a.var; + (match st.on_new_atom with Some f -> f a | None -> ()); + ) else ( + assert (a.is_true || a.neg.is_true); + ); + a + + (* Rather than iterate over all the heap when we want to decrease all the + variables/literals activity, we instead increase the value by which + we increase the activity of 'interesting' var/lits. *) + let[@inline] var_decay_activity st = + st.var_incr <- st.var_incr *. var_decay + + let[@inline] clause_decay_activity st = + st.clause_incr <- st.clause_incr *. clause_decay + + (* increase activity of [v] *) + let var_bump_activity st v = + v.v_weight <- v.v_weight +. st.var_incr; + if v.v_weight > 1e100 then ( + for i = 0 to nb_elt st.st - 1 do + Var.set_weight (get_elt st.st i) ((Var.weight (get_elt st.st i)) *. 1e-100) + done; + st.var_incr <- st.var_incr *. 1e-100; + ); + if H.in_heap v then ( + H.decrease st.order v + ) + + (* increase activity of clause [c] *) + let clause_bump_activity st (c:clause) : unit = + c.activity <- c.activity +. st.clause_incr; + if c.activity > 1e20 then ( + Vec.iter (fun c -> c.activity <- c.activity *. 1e-20) st.clauses_learnt; + st.clause_incr <- st.clause_incr *. 1e-20 + ) + + (* Simplification of clauses. + + When adding new clauses, it is desirable to 'simplify' them, i.e + minimize the amount of literals in it, because it greatly reduces + the search space for new watched literals during propagation. + Additionally, we have to partition the lits, to ensure the watched + literals (which are the first two lits of the clause) are appropriate. + Indeed, it is better to watch true literals, and then unassigned literals. + Watching false literals should be a last resort, and come with constraints + (see {!add_clause}). + *) + exception Trivial + + (* [arr_to_list a i] converts [a.(i), ... a.(length a-1)] into a list *) + let arr_to_list arr i : _ list = + if i >= Array.length arr then [] + else Array.to_list (Array.sub arr i (Array.length arr - i)) + + (* Eliminates atom duplicates in clauses *) + let eliminate_duplicates clause : clause = + let trivial = ref false in + let duplicates = ref [] in + let res = ref [] in + Array.iter (fun a -> + if Atom.seen a then duplicates := a :: !duplicates + else ( + Atom.mark a; + res := a :: !res + )) + clause.atoms; + List.iter + (fun a -> + if Var.seen_both a.var then trivial := true; + Var.clear a.var) + !res; + if !trivial then ( + raise Trivial + ) else if !duplicates = [] then ( + clause + ) else ( + Clause.make ~flags:clause.flags !res (History [clause]) + ) + + (* Partition literals for new clauses, into: + - true literals (maybe makes the clause trivial if the lit is proved true at level 0) + - unassigned literals, yet to be decided + - false literals (not suitable to watch, those at level 0 can be removed from the clause) + + Clauses that propagated false lits are remembered to reconstruct resolution proofs. + *) + let partition atoms : atom list * clause list = + let rec partition_aux trues unassigned falses history i = + if i >= Array.length atoms then ( + trues @ unassigned @ falses, history + ) else ( + let a = atoms.(i) in + if a.is_true then ( + let l = a.var.v_level in + if l = 0 then + raise Trivial (* A var true at level 0 gives a trivially true clause *) + else + (a :: trues) @ unassigned @ falses @ + (arr_to_list atoms (i + 1)), history + ) else if a.neg.is_true then ( + let l = a.var.v_level in + if l = 0 then ( + match a.var.reason with + | Some (Bcp cl | Bcp_lazy (lazy cl)) -> + partition_aux trues unassigned falses (cl :: history) (i + 1) + (* A var false at level 0 can be eliminated from the clause, + but we need to kepp in mind that we used another clause to simplify it. *) + (* TODO: get a proof of the propagation. *) + | None | Some Decision -> assert false + (* The var must have a reason, and it cannot be a decision/assumption, + since its level is 0. *) + ) else ( + partition_aux trues unassigned (a::falses) history (i + 1) + ) + ) else ( + partition_aux trues (a::unassigned) falses history (i + 1) + ) + ) + in + partition_aux [] [] [] [] 0 + + + (* Making a decision. + Before actually creatig a new decision level, we check that + all propagations have been done and propagated to the theory, + i.e that the theoriy state indeed takes into account the whole + stack of literals + i.e we have indeed reached a propagation fixpoint before making + a new decision *) + let new_decision_level st = + assert (st.th_head = Vec.size st.trail); + assert (st.elt_head = Vec.size st.trail); + Vec.push st.var_levels (Vec.size st.trail); + Plugin.push_level st.th; + () + + (* Attach/Detach a clause. + + A clause is attached (to its watching lits) when it is first added, + either because it is assumed or learnt. + + *) + let attach_clause c = + assert (not @@ Clause.attached c); + Log.debugf debug (fun k -> k "(@[sat.attach-clause@ %a@])" Clause.debug c); + Vec.push c.atoms.(0).neg.watched c; + Vec.push c.atoms.(1).neg.watched c; + Clause.set_attached c true; + () + + (* Backtracking. + Used to backtrack, i.e cancel down to [lvl] excluded, + i.e we want to go back to the state the solver was in + when decision level [lvl] was created. *) + let cancel_until st lvl = + assert (lvl >= 0); + (* Nothing to do if we try to backtrack to a non-existent level. *) + if decision_level st <= lvl then ( + Log.debugf debug (fun k -> k "(@[sat.cancel-until.nop@ :already-at-level <= %d@])" lvl) + ) else ( + Log.debugf info (fun k -> k "(@[sat.cancel-until %d@])" lvl); + (* We set the head of the solver and theory queue to what it was. *) + let head = ref (Vec.get st.var_levels lvl) in + st.elt_head <- !head; + st.th_head <- !head; + (* Now we need to cleanup the vars that are not valid anymore + (i.e to the right of elt_head in the queue. *) + for c = st.elt_head to Vec.size st.trail - 1 do + let a = Vec.get st.trail c in + (* A literal is unassigned, we nedd to add it back to + the heap of potentially assignable literals, unless it has + a level lower than [lvl], in which case we just move it back. *) + (* A variable is not true/false anymore, one of two things can happen: *) + if a.var.v_level <= lvl then ( + (* It is a late propagation, which has a level + lower than where we backtrack, so we just move it to the head + of the queue, to be propagated again. *) + Vec.set st.trail !head a; + head := !head + 1 + ) else ( + (* it is a result of bolean propagation, or a semantic propagation + with a level higher than the level to which we backtrack, + in that case, we simply unset its value and reinsert it into the heap. *) + a.is_true <- false; + a.neg.is_true <- false; + a.var.v_level <- -1; + a.var.reason <- None; + insert_var_order st a.var + ) + done; + (* Recover the right theory state. *) + let n = decision_level st - lvl in + assert (n>0); + (* Resize the vectors according to their new size. *) + Vec.shrink st.trail !head; + Vec.shrink st.var_levels lvl; + Plugin.pop_levels st.th n; + st.next_decisions <- []; + ); + () + + let pp_unsat_cause out = function + | US_local {first=_; core} -> + Format.fprintf out "(@[unsat-cause@ :false-assumptions %a@])" + (Format.pp_print_list Atom.pp) core + | US_false c -> + Format.fprintf out "(@[unsat-cause@ :false %a@])" Clause.debug c + + (* Unsatisfiability is signaled through an exception, since it can happen + in multiple places (adding new clauses, or solving for instance). *) + let report_unsat st (us:unsat_cause) : _ = + Log.debugf info (fun k -> k "(@[sat.unsat-conflict@ %a@])" pp_unsat_cause us); + let us = match us with + | US_false c -> + let c = if st.store_proof then Proof.prove_unsat c else c in + st.unsat_at_0 <- Some c; + US_false c + | _ -> us + in + raise (E_unsat us) + + (* Simplification of boolean propagation reasons. + When doing boolean propagation *at level 0*, it can happen + that the clause cl, which propagates a formula, also contains + other formulas, but has been simplified. in which case, we + need to rebuild a clause with correct history, in order to + be able to build a correct proof at the end of proof search. *) + let simpl_reason : reason -> reason = function + | (Bcp cl | Bcp_lazy (lazy cl)) as r -> + let l, history = partition cl.atoms in + begin match l with + | [_] -> + if history = [] then ( + (* no simplification has been done, so [cl] is actually a clause with only + [a], so it is a valid reason for propagating [a]. *) + r + ) else ( + (* Clauses in [history] have been used to simplify [cl] into a clause [tmp_cl] + with only one formula (which is [a]). So we explicitly create that clause + and set it as the cause for the propagation of [a], that way we can + rebuild the whole resolution tree when we want to prove [a]. *) + let c' = Clause.make ~flags:cl.flags l (History (cl :: history)) in + Log.debugf debug + (fun k -> k "(@[sat.simplified-reason@ %a@ %a@])" Clause.debug cl Clause.debug c'); + Bcp c' + ) + | _ -> + Log.debugf error + (fun k -> + k "(@[sat.simplify-reason.failed@ :at %a@ %a@]" + (Vec.pp ~sep:"" Atom.debug) (Vec.of_list l) + Clause.debug cl); + assert false + end + | Decision as r -> r + + (* Boolean propagation. + Wrapper function for adding a new propagated formula. *) + let enqueue_bool st a ~level:lvl reason : unit = + if a.neg.is_true then ( + Log.debugf error + (fun k->k "(@[sat.error.trying to enqueue a false literal %a@])" Atom.debug a); + assert false + ); + assert (not a.is_true && a.var.v_level < 0 && + a.var.reason = None && lvl >= 0); + let reason = + if lvl > 0 then reason + else simpl_reason reason + in + a.is_true <- true; + a.var.v_level <- lvl; + a.var.reason <- Some reason; + Vec.push st.trail a; + Log.debugf debug + (fun k->k "(@[sat.enqueue[%d]@ %a@])" (Vec.size st.trail) Atom.debug a); + () + + (* swap elements of array *) + let[@inline] swap_arr a i j = + if i<>j then ( + let tmp = a.(i) in + a.(i) <- a.(j); + a.(j) <- tmp; + ) + + (* move atoms assigned at high levels first *) + let put_high_level_atoms_first (arr:atom array) : unit = + Array.iteri + (fun i a -> + if i>0 && Atom.level a > Atom.level arr.(0) then ( + (* move first to second, [i]-th to first, second to [i] *) + if i=1 then ( + swap_arr arr 0 1; + ) else ( + let tmp = arr.(1) in + arr.(1) <- arr.(0); + arr.(0) <- arr.(i); + arr.(i) <- tmp; + ); + ) else if i>1 && Atom.level a > Atom.level arr.(1) then ( + swap_arr arr 1 i; + )) + arr + + (* find which level to backtrack to, given a conflict clause + and a boolean stating whether it is + a UIP ("Unique Implication Point") + precond: the atom list is sorted by decreasing decision level *) + let backtrack_lvl _st (arr: atom array) : int * bool = + if Array.length arr <= 1 then ( + 0, true + ) else ( + let a = arr.(0) in + let b = arr.(1) in + assert(a.var.v_level > 0); + if a.var.v_level > b.var.v_level then ( + (* backtrack below [a], so we can propagate [not a] *) + b.var.v_level, true + ) else ( + assert (a.var.v_level = b.var.v_level); + assert (a.var.v_level >= 0); + max (a.var.v_level - 1) 0, false + ) + ) + + (* result of conflict analysis, containing the learnt clause and some + additional info. + + invariant: cr_history's order matters, as its head is later used + during pop operations to determine the origin of a clause/conflict + (boolean conflict i.e hypothesis, or theory lemma) *) + type conflict_res = { + cr_backtrack_lvl : int; (* level to backtrack to *) + cr_learnt: atom array; (* lemma learnt from conflict *) + cr_history: clause list; (* justification *) + cr_is_uip: bool; (* conflict is UIP? *) + } + + (* conflict analysis for SAT + Same idea as the mcsat analyze function (without semantic propagations), + except we look the the Last UIP (TODO: check ?), and do it in an imperative + and efficient manner. *) + let analyze st c_clause : conflict_res = + let pathC = ref 0 in + let learnt = ref [] in + let cond = ref true in + let blevel = ref 0 in + let to_unmark = st.to_clear in (* for cleanup *) + let c = ref (Some c_clause) in + let tr_ind = ref (Vec.size st.trail - 1) in + let history = ref [] in + assert (decision_level st > 0); + Vec.clear to_unmark; + let conflict_level = + if Plugin.has_theory + then Array.fold_left (fun acc p -> max acc p.var.v_level) 0 c_clause.atoms + else decision_level st + in + Log.debugf debug + (fun k -> k "(@[sat.analyze-conflict@ :c-level %d@ :clause %a@])" conflict_level Clause.debug c_clause); + while !cond do + begin match !c with + | None -> + Log.debug debug "(@[sat.analyze-conflict: skipping resolution for semantic propagation@])" + | Some clause -> + Log.debugf debug (fun k->k"(@[sat.analyze-conflict.resolve@ %a@])" Clause.debug clause); + if Clause.removable clause then ( + clause_bump_activity st clause; + ); + history := clause :: !history; + (* visit the current predecessors *) + for j = 0 to Array.length clause.atoms - 1 do + let q = clause.atoms.(j) in + assert (q.is_true || q.neg.is_true && q.var.v_level >= 0); (* unsure? *) + if q.var.v_level <= 0 then ( + assert (q.neg.is_true); + match q.var.reason with + | Some (Bcp cl | Bcp_lazy (lazy cl)) -> history := cl :: !history + | Some Decision | None -> assert false + ); + if not (Var.marked q.var) then ( + Var.mark q.var; + Vec.push to_unmark q.var; + if q.var.v_level > 0 then ( + var_bump_activity st q.var; + if q.var.v_level >= conflict_level then ( + incr pathC; + ) else ( + learnt := q :: !learnt; + blevel := max !blevel q.var.v_level + ) + ) + ) + done + end; + + (* look for the next node to expand *) + while + let a = Vec.get st.trail !tr_ind in + Log.debugf debug + (fun k -> k "(@[sat.analyze-conflict.at-trail-elt@ %a@])" Atom.debug a); + (not (Var.marked a.var)) || + (a.var.v_level < conflict_level) + do + decr tr_ind; + done; + let p = Vec.get st.trail !tr_ind in + decr pathC; + decr tr_ind; + match !pathC, p.var.reason with + | 0, _ -> + cond := false; + learnt := p.neg :: List.rev !learnt + | n, Some (Bcp cl | Bcp_lazy (lazy cl)) -> + assert (n > 0); + assert (p.var.v_level >= conflict_level); + c := Some cl + | _, (None | Some Decision) -> assert false + done; + Vec.iter Var.clear to_unmark; + Vec.clear to_unmark; + (* put high-level literals first, so that: + - they make adequate watch lits + - the first literal is the UIP, if any *) + let a = Array.of_list !learnt in + Array.fast_sort (fun p q -> compare q.var.v_level p.var.v_level) a; + (* put_high_level_atoms_first a; *) + let level, is_uip = backtrack_lvl st a in + { cr_backtrack_lvl = level; + cr_learnt = a; + cr_history = List.rev !history; + cr_is_uip = is_uip; + } + + (* add the learnt clause to the clause database, propagate, etc. *) + let record_learnt_clause st (confl:clause) (cr:conflict_res): unit = + let proof = if st.store_proof then History cr.cr_history else Empty_premise in + begin match cr.cr_learnt with + | [| |] -> assert false + | [|fuip|] -> + assert (cr.cr_backtrack_lvl = 0 && decision_level st = 0); + if fuip.neg.is_true then ( + (* incompatible at level 0 *) + report_unsat st (US_false confl) + ) else ( + let uclause = Clause.make_removable_a cr.cr_learnt proof in + (* no need to attach [uclause], it is true at level 0 *) + enqueue_bool st fuip ~level:0 (Bcp uclause) + ) + | _ -> + let fuip = cr.cr_learnt.(0) in + let lclause = Clause.make_removable_a cr.cr_learnt proof in + if Array.length lclause.atoms > 2 then ( + Vec.push st.clauses_learnt lclause; (* potentially gc'able *) + ); + attach_clause lclause; + clause_bump_activity st lclause; + assert (cr.cr_is_uip); + enqueue_bool st fuip ~level:cr.cr_backtrack_lvl (Bcp lclause) + end; + var_decay_activity st; + clause_decay_activity st + + (* process a conflict: + - learn clause + - backtrack + - report unsat if conflict at level 0 + *) + let add_boolean_conflict st (confl:clause): unit = + Log.debugf info (fun k -> k "(@[sat.add-bool-conflict@ %a@])" Clause.debug confl); + st.next_decisions <- []; + assert (decision_level st >= 0); + if decision_level st = 0 || + Array.for_all (fun a -> a.var.v_level <= 0) confl.atoms then ( + (* Top-level conflict *) + report_unsat st (US_false confl); + ); + let cr = analyze st confl in + cancel_until st (max cr.cr_backtrack_lvl 0); + record_learnt_clause st confl cr + + (* Get the correct vector to insert a clause in. *) + let[@inline] add_clause_to_vec st c = + if Clause.removable c then ( + Vec.push st.clauses_learnt c + ) else ( + Vec.push st.clauses_hyps c + ) + + (* Add a new clause, simplifying, propagating, and backtracking if + the clause is false in the current trail *) + let add_clause_ st (init:clause) : unit = + Log.debugf debug (fun k -> k "(@[sat.add-clause@ @[%a@]@])" Clause.debug init); + (* Insertion of new lits is done before simplification. Indeed, else a lit in a + trivial clause could end up being not decided on, which is a bug. *) + Array.iter (fun x -> insert_var_order st x.var) init.atoms; + try + let c = eliminate_duplicates init in + assert (c.flags = init.flags); + Log.debugf debug (fun k -> k "(@[sat.dups-removed@ %a@])" Clause.debug c); + let atoms, history = partition c.atoms in + let clause = + if history = [] then ( + (* just update order of atoms *) + List.iteri (fun i a -> c.atoms.(i) <- a) atoms; + c + ) else ( + let proof = if st.store_proof then History (c::history) else Empty_premise in + Clause.make ~flags:c.flags atoms proof + ) + in + assert (clause.flags = init.flags); + Log.debugf info (fun k->k "(@[sat.new-clause@ @[%a@]@])" Clause.debug clause); + match atoms with + | [] -> + report_unsat st @@ US_false clause + | [a] -> + cancel_until st 0; + if a.neg.is_true then ( + (* cannot recover from this *) + report_unsat st @@ US_false clause + ) else if a.is_true then ( + () (* atom is already true, nothing to do *) + ) else ( + Log.debugf debug + (fun k->k "(@[sat.add-clause.unit-clause@ :propagating %a@])" Atom.debug a); + add_clause_to_vec st clause; + enqueue_bool st a ~level:0 (Bcp clause) + ) + | a::b::_ -> + add_clause_to_vec st clause; + if a.neg.is_true then ( + (* Atoms need to be sorted in decreasing order of decision level, + or we might watch the wrong literals. *) + put_high_level_atoms_first clause.atoms; + attach_clause clause; + add_boolean_conflict st clause + ) else ( + attach_clause clause; + if b.neg.is_true && not a.is_true && not a.neg.is_true then ( + let lvl = List.fold_left (fun m a -> max m a.var.v_level) 0 atoms in + cancel_until st lvl; + enqueue_bool st a ~level:lvl (Bcp clause) + ) + ) + with Trivial -> + Log.debugf info + (fun k->k "(@[sat.add-clause@ :ignore-trivial @[%a@]@])" Clause.debug init) + + let[@inline never] flush_clauses_ st = + while not @@ Vec.is_empty st.clauses_to_add do + let c = Vec.pop st.clauses_to_add in + add_clause_ st c + done + + let[@inline] flush_clauses st = + if not @@ Vec.is_empty st.clauses_to_add then flush_clauses_ st + + type watch_res = + | Watch_kept + | Watch_removed + + (* boolean propagation. + [a] is the false atom, one of [c]'s two watch literals + [i] is the index of [c] in [a.watched] + @return whether [c] was removed from [a.watched] + *) + let propagate_in_clause st (a:atom) (c:clause) (i:int): watch_res = + let atoms = c.atoms in + let first = atoms.(0) in + if first == a.neg then ( + (* false lit must be at index 1 *) + atoms.(0) <- atoms.(1); + atoms.(1) <- first + ) else ( + assert (a.neg == atoms.(1)) + ); + let first = atoms.(0) in + if first.is_true + then Watch_kept (* true clause, keep it in watched *) + else ( + try (* look for another watch lit *) + for k = 2 to Array.length atoms - 1 do + let ak = atoms.(k) in + if not (ak.neg.is_true) then ( + (* watch lit found: update and exit *) + atoms.(1) <- ak; + atoms.(k) <- a.neg; + (* remove [c] from [a.watched], add it to [ak.neg.watched] *) + Vec.push ak.neg.watched c; + assert (Vec.get a.watched i == c); + Vec.fast_remove a.watched i; + raise_notrace Exit + ) + done; + (* no watch lit found *) + if first.neg.is_true then ( + (* clause is false *) + st.elt_head <- Vec.size st.trail; + raise_notrace (Conflict c) + ) else ( + enqueue_bool st first ~level:(decision_level st) (Bcp c) + ); + Watch_kept + with Exit -> + Watch_removed + ) + + (* propagate atom [a], which was just decided. This checks every + clause watching [a] to see if the clause is false, unit, or has + other possible watches + @param res the optional conflict clause that the propagation might trigger *) + let propagate_atom st a : unit = + let watched = a.watched in + let rec aux i = + if i >= Vec.size watched then () + else ( + let c = Vec.get watched i in + assert (Clause.attached c); + let j = + if Clause.dead c then ( + Vec.fast_remove watched i; + i + ) else ( + match propagate_in_clause st a c i with + | Watch_kept -> i+1 + | Watch_removed -> i (* clause at this index changed *) + ) + in + aux j + ) + in + aux 0 + + exception Th_conflict of Clause.t + + let[@inline] slice_get st i = Vec.get st.trail i + + let acts_add_clause st ?(keep=false) (l:formula list) (lemma:lemma): unit = + let atoms = List.rev_map (mk_atom st) l in + let flags = if keep then 0 else Clause.flag_removable in + let c = Clause.make ~flags atoms (Lemma lemma) in + Log.debugf info (fun k->k "(@[sat.th.add-clause@ %a@])" Clause.debug c); + Vec.push st.clauses_to_add c + + let acts_add_decision_lit (st:t) (f:formula) (sign:bool) : unit = + let a = mk_atom st f in + let a = if sign then a else Atom.neg a in + if not (Atom.has_value a) then ( + Log.debugf 10 (fun k->k "(@[sat.th.add-decision-lit@ %a@])" Atom.debug a); + st.next_decisions <- a :: st.next_decisions + ) + + let acts_raise st (l:formula list) proof : 'a = + let atoms = List.rev_map (mk_atom st) l in + (* conflicts can be removed *) + let c = Clause.make_removable atoms (Lemma proof) in + Log.debugf 5 (fun k->k "(@[@{sat.th.raise-conflict@}@ %a@])" Clause.debug c); + raise_notrace (Th_conflict c) + + let check_consequence_lits_false_ l : unit = + match List.find Atom.is_true l with + | a -> + invalid_argf + "slice.acts_propagate:@ Consequence should contain only true literals, but %a isn't" + Atom.debug (Atom.neg a) + | exception Not_found -> () + + let acts_propagate (st:t) f = function + | Solver_intf.Consequence mk_expl -> + let p = mk_atom st f in + if Atom.is_true p then () + else if Atom.is_false p then ( + let lits, proof = mk_expl() in + let l = List.rev_map (fun f -> Atom.neg @@ mk_atom st f) lits in + check_consequence_lits_false_ l; + let c = Clause.make_removable (p :: l) (Lemma proof) in + raise_notrace (Th_conflict c) + ) else ( + insert_var_order st p.var; + let c = lazy ( + let lits, proof = mk_expl () in + let l = List.rev_map (fun f -> Atom.neg @@ mk_atom st f) lits in + (* note: we can check that invariant here in the [lazy] block, + as conflict analysis will run in an environment where + the literals should be true anyway, since it's an extension of the + current trail + (otherwise the propagated lit would have been backtracked and + discarded already.) *) + check_consequence_lits_false_ l; + Clause.make_removable (p :: l) (Lemma proof) + ) in + let level = decision_level st in + enqueue_bool st p ~level (Bcp_lazy c) + ) + + let[@specialise] acts_iter st ~full head f : unit = + for i = (if full then 0 else head) to Vec.size st.trail-1 do + let a = Vec.get st.trail i in + f a.lit + done + + let eval_atom_ a = + if Atom.is_true a then Solver_intf.L_true + else if Atom.is_false a then Solver_intf.L_false + else Solver_intf.L_undefined + + let[@inline] acts_eval_lit st (f:formula) : Solver_intf.lbool = + let a = mk_atom st f in + eval_atom_ a + + let[@inline] acts_mk_lit st ?default_pol f : unit = + ignore (mk_atom ?default_pol st f : atom) + + let[@inline] current_slice st : _ Solver_intf.acts = + let module M = struct + type nonrec proof = lemma + type nonrec formula = formula + let iter_assumptions=acts_iter st ~full:false st.th_head + let eval_lit= acts_eval_lit st + let mk_lit=acts_mk_lit st + let add_clause = acts_add_clause st + let propagate = acts_propagate st + let raise_conflict c pr=acts_raise st c pr + let add_decision_lit=acts_add_decision_lit st + end in + (module M) + + (* full slice, for [if_sat] final check *) + let[@inline] full_slice st : _ Solver_intf.acts = + let module M = struct + type nonrec proof = lemma + type nonrec formula = formula + let iter_assumptions=acts_iter st ~full:true st.th_head + let eval_lit= acts_eval_lit st + let mk_lit=acts_mk_lit st + let add_clause = acts_add_clause st + let propagate = acts_propagate st + let raise_conflict c pr=acts_raise st c pr + let add_decision_lit=acts_add_decision_lit st + end in + (module M) + + (* Assert that the conflict is indeeed a conflict *) + let check_is_conflict_ (c:Clause.t) : unit = + if not @@ Array.for_all (Atom.is_false) c.atoms then ( + invalid_argf "conflict should be false: %a" Clause.debug c + ) + + (* some boolean literals were decided/propagated within Msat. Now we + need to inform the theory of those assumptions, so it can do its job. + @return the conflict clause, if the theory detects unsatisfiability *) + let rec theory_propagate st : clause option = + assert (st.elt_head = Vec.size st.trail); + assert (st.th_head <= st.elt_head); + if st.th_head = st.elt_head then ( + None (* fixpoint/no propagation *) + ) else ( + let slice = current_slice st in + st.th_head <- st.elt_head; (* catch up *) + match Plugin.partial_check st.th slice with + | () -> + flush_clauses st; + propagate st + | exception Th_conflict c -> + check_is_conflict_ c; + Array.iter (fun a -> insert_var_order st a.var) c.atoms; + Some c + ) + + (* fixpoint between boolean propagation and theory propagation + @return a conflict clause, if any *) + and propagate (st:t) : clause option = + (* First, treat the stack of lemmas added by the theory, if any *) + flush_clauses st; + (* Now, check that the situation is sane *) + assert (st.elt_head <= Vec.size st.trail); + if st.elt_head = Vec.size st.trail then ( + theory_propagate st + ) else ( + match + while st.elt_head < Vec.size st.trail do + let a = Vec.get st.trail st.elt_head in + propagate_atom st a; + st.elt_head <- st.elt_head + 1; + done; + with + | () -> theory_propagate st + | exception Conflict c -> Some c + ) + + (* compute unsat core from assumption [a] *) + let analyze_final (self:t) (a:atom) : atom list = + Log.debugf 5 (fun k->k "(@[sat.analyze-final@ :lit %a@])" Atom.debug a); + assert (Atom.is_false a); + let core = ref [a] in + let idx = ref (Vec.size self.trail - 1) in + Var.mark a.var; + let seen = ref [a.var] in + while !idx >= 0 do + let a' = Vec.get self.trail !idx in + if Var.marked a'.var then ( + match Atom.reason a' with + | Some Decision -> core := a' :: !core + | Some (Bcp c | Bcp_lazy (lazy c)) -> + Array.iter + (fun a -> + let v = a.var in + if not @@ Var.marked v then ( + seen := v :: !seen; + Var.mark v; + )) + c.atoms + | None -> () + ); + decr idx + done; + List.iter Var.unmark !seen; + Log.debugf 5 (fun k->k "(@[sat.analyze-final.done@ :core %a@])" (Format.pp_print_list Atom.debug) !core); + !core + + (* remove some learnt clauses. *) + let reduce_db (st:t) (n_of_learnts: int) : unit = + let v = st.clauses_learnt in + Log.debugf 3 (fun k->k "(@[sat.gc.start :keep %d :out-of %d@])" n_of_learnts (Vec.size v)); + assert (Vec.size v > n_of_learnts); + (* sort by decreasing activity *) + Vec.sort v (fun c1 c2 -> compare c2.activity c1.activity); + let n_collected = ref 0 in + while Vec.size v > n_of_learnts do + let c = Vec.pop v in + assert (Clause.removable c); + Clause.set_dead c; + assert (Clause.dead c); + incr n_collected; + done; + Log.debugf 3 (fun k->k "(@[sat.gc.done :collected %d@])" !n_collected); + () + + (* Decide on a new literal, and enqueue it into the trail *) + let rec pick_branch_aux st atom : unit = + let v = atom.var in + if v.v_level >= 0 then ( + assert (v.pa.is_true || v.na.is_true); + pick_branch_lit st + ) else ( + new_decision_level st; + let current_level = decision_level st in + enqueue_bool st atom ~level:current_level Decision; + (match st.on_decision with Some f -> f atom | None -> ()); + ) + + and pick_branch_lit st = + match st.next_decisions with + | atom :: tl -> + st.next_decisions <- tl; + pick_branch_aux st atom + | [] when decision_level st < Vec.size st.assumptions -> + (* use an assumption *) + let a = Vec.get st.assumptions (decision_level st) in + if Atom.is_true a then ( + new_decision_level st; (* pseudo decision level, [a] is already true *) + pick_branch_lit st + ) else if Atom.is_false a then ( + (* root conflict, find unsat core *) + let core = analyze_final st a in + raise (E_unsat (US_local {first=a; core})) + ) else ( + pick_branch_aux st a + ) + | [] -> + begin match H.remove_min st.order with + | v -> + pick_branch_aux st (if Var.default_pol v then v.pa else v.na) + | exception Not_found -> raise_notrace E_sat + end + + (* do some amount of search, until the number of conflicts or clause learnt + reaches the given parameters *) + let search (st:t) n_of_conflicts n_of_learnts : unit = + Log.debugf 3 + (fun k->k "(@[sat.search@ :n-conflicts %d@ :n-learnt %d@])" n_of_conflicts n_of_learnts); + let conflictC = ref 0 in + while true do + match propagate st with + | Some confl -> (* Conflict *) + incr conflictC; + (* When the theory has raised Unsat, add_boolean_conflict + might 'forget' the initial conflict clause, and only add the + analyzed backtrack clause. So in those case, we use add_clause + to make sure the initial conflict clause is also added. *) + if Clause.attached confl then ( + add_boolean_conflict st confl + ) else ( + add_clause_ st confl + ); + (match st.on_conflict with Some f -> f confl.atoms | None -> ()); + + | None -> (* No Conflict *) + assert (st.elt_head = Vec.size st.trail); + assert (st.elt_head = st.th_head); + if n_of_conflicts > 0 && !conflictC >= n_of_conflicts then ( + Log.debug info "(sat.restarting)"; + cancel_until st 0; + raise_notrace Restart + ); + (* if decision_level() = 0 then simplify (); *) + + if n_of_learnts > 0 && + Vec.size st.clauses_learnt - Vec.size st.trail > n_of_learnts then ( + reduce_db st n_of_learnts; + ); + + pick_branch_lit st + done + + let eval_level (_st:t) (a:atom) = + let lvl = a.var.v_level in + if Atom.is_true a then ( + assert (lvl >= 0); + true, lvl + ) else if Atom.is_false a then ( + false, lvl + ) else ( + raise UndecidedLit + ) + + let[@inline] eval st lit = fst @@ eval_level st lit + + let[@inline] unsat_conflict st = st.unsat_at_0 + + (* fixpoint of propagation and decisions until a model is found, or a + conflict is reached *) + let solve_ (st:t) : unit = + Log.debugf 5 (fun k->k "(@[sat.solve :assms %d@])" (Vec.size st.assumptions)); + check_unsat_ st; + try + flush_clauses st; (* add initial clauses *) + let n_of_conflicts = ref (float_of_int restart_first) in + let n_of_learnts = ref ((float_of_int (nb_clauses st)) *. learntsize_factor) in + while true do + begin try + search st (int_of_float !n_of_conflicts) (int_of_float !n_of_learnts) + with + | Restart -> + n_of_conflicts := !n_of_conflicts *. restart_inc; + n_of_learnts := !n_of_learnts *. learntsize_inc + | E_sat -> + assert (st.elt_head = Vec.size st.trail && + Vec.is_empty st.clauses_to_add && + st.next_decisions=[]); + begin match Plugin.final_check st.th (full_slice st) with + | () -> + if st.elt_head = Vec.size st.trail && + Vec.is_empty st.clauses_to_add && + st.next_decisions = [] + then ( + raise_notrace E_sat + ); + (* otherwise, keep on *) + flush_clauses st; + | exception Th_conflict c -> + check_is_conflict_ c; + Array.iter (fun a -> insert_var_order st a.var) c.atoms; + Log.debugf info (fun k -> k "(@[sat.theory-conflict-clause@ %a@])" Clause.debug c); + (match st.on_conflict with Some f -> f c.atoms | None -> ()); + Vec.push st.clauses_to_add c; + flush_clauses st; + end; + end + done + with E_sat -> () + + let assume st cnf lemma = + List.iter + (fun l -> + let atoms = List.rev_map (mk_atom st) l in + let c = Clause.make_permanent atoms (Hyp lemma) in + Log.debugf debug (fun k -> k "(@[sat.assume-clause@ @[%a@]@])" Clause.debug c); + Vec.push st.clauses_to_add c) + cnf + + (* Check satisfiability *) + let check_clause c = + let res = Array.exists (fun a -> a.is_true) c.atoms in + if not res then ( + Log.debugf debug + (fun k -> k "(@[sat.check-clause@ :not-satisfied @[%a@]@])" Clause.debug c); + false + ) else + true + + let check_vec v = Vec.for_all check_clause v + let check st : bool = + Vec.is_empty st.clauses_to_add && + check_vec st.clauses_hyps && + check_vec st.clauses_learnt + + let[@inline] theory st = st.th + + (* Unsafe access to internal data *) + + let hyps env = env.clauses_hyps + + let history env = env.clauses_learnt + + let trail env = env.trail + + (* Result type *) + type res = + | Sat of Formula.t Solver_intf.sat_state + | Unsat of (atom,clause,Proof.t) Solver_intf.unsat_state + + let pp_all st lvl status = + Log.debugf lvl + (fun k -> k + "(@[sat.full-state :res %s - Full summary:@,@[Trail:@\n%a@]@,\ + @[Hyps:@\n%a@]@,@[Lemmas:@\n%a@]@,@]@." + status + (Vec.pp ~sep:"" Atom.debug) (trail st) + (Vec.pp ~sep:"" Clause.debug) (hyps st) + (Vec.pp ~sep:"" Clause.debug) (history st) + ) + + let mk_sat (st:t) : Formula.t Solver_intf.sat_state = + pp_all st 99 "SAT"; + let t = trail st in + let module M = struct + type formula = Formula.t + let iter_trail f = Vec.iter (fun a -> f (Atom.formula a)) t + let[@inline] eval f = eval st (mk_atom st f) + let[@inline] eval_level f = eval_level st (mk_atom st f) + end in + (module M) + + let mk_unsat (st:t) (us: unsat_cause) : _ Solver_intf.unsat_state = + pp_all st 99 "UNSAT"; + let unsat_assumptions () = match us with + | US_local {first=_; core} -> core + | _ -> [] + in + let unsat_conflict = match us with + | US_false c -> fun() -> c + | US_local {core=[]; _} -> assert false + | US_local {first; core} -> + let c = lazy ( + let core = List.rev core in (* increasing trail order *) + assert (Atom.equal first @@ List.hd core); + let proof_of (a:atom) = match Atom.reason a with + | Some Decision -> Clause.make_removable [a] Local + | Some (Bcp c | Bcp_lazy (lazy c)) -> c + | None -> assert false + in + let other_lits = List.filter (fun a -> not (Atom.equal a first)) core in + let hist = + Clause.make_permanent [first] Local :: + proof_of first :: + List.map proof_of other_lits in + Clause.make_permanent [] (History hist) + ) in + fun () -> Lazy.force c + in + let get_proof () = + let c = unsat_conflict () in + Proof.prove c + in + let module M = struct + type nonrec atom = atom + type clause = Clause.t + type proof = Proof.t + let get_proof = get_proof + let unsat_conflict = unsat_conflict + let unsat_assumptions = unsat_assumptions + end in + (module M) + + let add_clause_a st c lemma : unit = + try + let c = Clause.make_a ~flags:0 c (Hyp lemma) in + add_clause_ st c + with + | E_unsat (US_false c) -> + st.unsat_at_0 <- Some c + + let add_clause st c lemma : unit = + try + let c = Clause.make_permanent c (Hyp lemma) in + add_clause_ st c + with + | E_unsat (US_false c) -> + st.unsat_at_0 <- Some c + + let solve ?(assumptions=[]) (st:t) : res = + cancel_until st 0; + Vec.clear st.assumptions; + List.iter (Vec.push st.assumptions) assumptions; + try + solve_ st; + Sat (mk_sat st) + with E_unsat us -> + Unsat (mk_unsat st us) + + let true_at_level0 st a = + try + let b, lev = eval_level st a in + b && lev = 0 + with UndecidedLit -> false + + let[@inline] eval_atom _st a : Solver_intf.lbool = eval_atom_ a +end +[@@inline][@@specialise] + + +module Make_cdcl_t(Plugin : Solver_intf.PLUGIN_CDCL_T) = + Make(struct + include Plugin + let has_theory = true + end) +[@@inline][@@specialise] + +module Make_pure_sat(Plugin : Solver_intf.PLUGIN_SAT) = + Make(struct + module Formula = Plugin.Formula + type t = unit + type proof = Plugin.proof + let push_level () = () + let pop_levels _ _ = () + let partial_check () _ = () + let final_check () _ = () + let has_theory = false +end) +[@@inline][@@specialise] + diff --git a/src/sat/Solver_intf.ml b/src/sat/Solver_intf.ml new file mode 100644 index 00000000..afe2dfc6 --- /dev/null +++ b/src/sat/Solver_intf.ml @@ -0,0 +1,426 @@ +(* +MSAT is free software, using the Apache license, see file LICENSE +Copyright 2016 Guillaume Bury +Copyright 2016 Simon Cruanes +*) + +(** Interface for Solvers + + This modules defines the safe external interface for solvers. + Solvers that implements this interface can be obtained using the [Make] + functor in {!Solver} or {!Mcsolver}. +*) + +type 'a printer = Format.formatter -> 'a -> unit + +module type SAT_STATE = sig + type formula + + val eval : formula -> bool + (** Returns the valuation of a formula in the current state + of the sat solver. + @raise UndecidedLit if the literal is not decided *) + + val eval_level : formula -> bool * int + (** Return the current assignement of the literals, as well as its + decision level. If the level is 0, then it is necessary for + the atom to have this value; otherwise it is due to choices + that can potentially be backtracked. + @raise UndecidedLit if the literal is not decided *) + + val iter_trail : (formula -> unit) -> unit + (** Iter through the formulas in order of decision/propagation + (starting from the first propagation, to the last propagation). *) +end + +type 'form sat_state = (module SAT_STATE with type formula = 'form) +(** The type of values returned when the solver reaches a SAT state. *) + +module type UNSAT_STATE = sig + type atom + type clause + type proof + + val unsat_conflict : unit -> clause + (** Returns the unsat clause found at the toplevel *) + + val get_proof : unit -> proof + (** returns a persistent proof of the empty clause from the Unsat result. *) + + val unsat_assumptions: unit -> atom list + (** Subset of assumptions responsible for "unsat" *) +end + +type ('atom, 'clause, 'proof) unsat_state = + (module UNSAT_STATE with type atom = 'atom + and type clause = 'clause + and type proof = 'proof) +(** The type of values returned when the solver reaches an UNSAT state. *) + +type negated = + | Negated (** changed sign *) + | Same_sign (** kept sign *) +(** This type is used during the normalisation of formulas. + See {!val:Expr_intf.S.norm} for more details. *) + +type ('formula, 'proof) reason = + | Consequence of (unit -> 'formula list * 'proof) [@@unboxed] + (** [Consequence (l, p)] means that the formulas in [l] imply the propagated + formula [f]. The proof should be a proof of the clause "[l] implies [f]". + + invariant: in [Consequence (fun () -> l,p)], all elements of [l] must be true in + the current trail. + + {b note} on lazyiness: the justification is suspended (using [unit -> …]) + to avoid potentially costly computations that might never be used + if this literal is backtracked without participating in a conflict. + Therefore the function that produces [(l,p)] needs only be safe in + trails (partial models) that are conservative extensions of the current + trail. + If the theory isn't robust w.r.t. extensions of the trail (e.g. if + its internal state undergoes significant changes), + it can be easier to produce the explanation eagerly when + propagating, and then use [Consequence (fun () -> expl, proof)] with + the already produced [(expl,proof)] tuple. + *) +(** The type of reasons for propagations of a formula [f]. *) + +type lbool = L_true | L_false | L_undefined +(** Valuation of an atom *) + +module type ACTS = sig + type formula + type proof + + val iter_assumptions: (formula -> unit) -> unit + (** Traverse the new assumptions on the boolean trail. *) + + val eval_lit: formula -> lbool + (** Obtain current value of the given literal *) + + val mk_lit: ?default_pol:bool -> formula -> unit + (** Map the given formula to a literal, which will be decided by the + SAT solver. *) + + val add_clause: ?keep:bool -> formula list -> proof -> unit + (** Add a clause to the solver. + @param keep if true, the clause will be kept by the solver. + Otherwise the solver is allowed to GC the clause and propose this + partial model again. + *) + + val raise_conflict: formula list -> proof -> 'b + (** Raise a conflict, yielding control back to the solver. + The list of atoms must be a valid theory lemma that is false in the + current trail. *) + + val propagate: formula -> (formula, proof) reason -> unit + (** Propagate a formula, i.e. the theory can evaluate the formula to be true + (see the definition of {!type:eval_res} *) + + val add_decision_lit: formula -> bool -> unit + (** Ask the SAT solver to decide on the given formula with given sign + before it can answer [SAT]. The order of decisions is still unspecified. + Useful for theory combination. This will be undone on backtracking. *) +end + +(* TODO: find a way to use atoms instead of formulas here *) +type ('formula, 'proof) acts = + (module ACTS with type formula = 'formula + and type proof = 'proof) +(** The type for a slice of assertions to assume/propagate in the theory. *) + +exception No_proof + +module type FORMULA = sig + (** formulas *) + + type t + (** The type of atomic formulas over terms. *) + + val equal : t -> t -> bool + (** Equality over formulas. *) + + val hash : t -> int + (** Hashing function for formulas. Should be such that two formulas equal according + to {!val:Expr_intf.S.equal} have the same hash. *) + + val pp : t printer + (** Printing function used among other thing for debugging. *) + + val neg : t -> t + (** Formula negation *) + + val norm : t -> t * negated + (** Returns a 'normalized' form of the formula, possibly negated + (in which case return [Negated]). + [norm] must be so that [a] and [neg a] normalise to the same formula, + but one returns [Negated] and the other [Same_sign]. *) +end + +(** Signature for theories to be given to the CDCL(T) solver *) +module type PLUGIN_CDCL_T = sig + type t + (** The plugin state itself *) + + module Formula : FORMULA + + type proof + + val push_level : t -> unit + (** Create a new backtrack level *) + + val pop_levels : t -> int -> unit + (** Pop [n] levels of the theory *) + + val partial_check : t -> (Formula.t, proof) acts -> unit + (** Assume the formulas in the slice, possibly using the [slice] + to push new formulas to be propagated or to raising a conflict or to add + new lemmas. *) + + val final_check : t -> (Formula.t, proof) acts -> unit + (** Called at the end of the search in case a model has been found. + If no new clause is pushed, then proof search ends and "sat" is returned; + if lemmas are added, search is resumed; + if a conflict clause is added, search backtracks and then resumes. *) +end + +(** Signature for pure SAT solvers *) +module type PLUGIN_SAT = sig + module Formula : FORMULA + + type proof +end + +module type PROOF = sig + (** Signature for a module handling proof by resolution from sat solving traces *) + + (** {3 Type declarations} *) + + exception Resolution_error of string + (** Raised when resolution failed. *) + + type formula + type atom + type lemma + type clause + (** Abstract types for atoms, clauses and theory-specific lemmas *) + + type t + (** Lazy type for proof trees. Proofs are persistent objects, and can be + extended to proof nodes using functions defined later. *) + + and proof_node = { + conclusion : clause; (** The conclusion of the proof *) + step : step; (** The reasoning step used to prove the conclusion *) + } + (** A proof can be expanded into a proof node, which show the first step of the proof. *) + + (** The type of reasoning steps allowed in a proof. *) + and step = + | Hypothesis of lemma + (** The conclusion is a user-provided hypothesis *) + | Assumption + (** The conclusion has been locally assumed by the user *) + | Lemma of lemma + (** The conclusion is a tautology provided by the theory, with associated proof *) + | Duplicate of t * atom list + (** The conclusion is obtained by eliminating multiple occurences of the atom in + the conclusion of the provided proof. *) + | Hyper_res of hyper_res_step + + and hyper_res_step = { + hr_init: t; + hr_steps: (atom * t) list; (* list of pivot+clause to resolve against [init] *) + } + + (** {3 Proof building functions} *) + + val prove : clause -> t + (** Given a clause, return a proof of that clause. + @raise Resolution_error if it does not succeed. *) + + val prove_unsat : clause -> t + (** Given a conflict clause [c], returns a proof of the empty clause. + @raise Resolution_error if it does not succeed. *) + + val prove_atom : atom -> t option + (** Given an atom [a], returns a proof of the clause [[a]] if [a] is true at level 0 *) + + val res_of_hyper_res : hyper_res_step -> t * t * atom + (** Turn an hyper resolution step into a resolution step. + The conclusion can be deduced by performing a resolution between the conclusions + of the two given proofs. + The atom on which to perform the resolution is also given. *) + + (** {3 Proof Nodes} *) + + val parents : step -> t list + (** Returns the parents of a proof node. *) + + val is_leaf : step -> bool + (** Returns wether the the proof node is a leaf, i.e. an hypothesis, + an assumption, or a lemma. + [true] if and only if {!parents} returns the empty list. *) + + val expl : step -> string + (** Returns a short string description for the proof step; for instance + ["hypothesis"] for a [Hypothesis] + (it currently returns the variant name in lowercase). *) + + + (** {3 Proof Manipulation} *) + + val expand : t -> proof_node + (** Return the proof step at the root of a given proof. *) + + val conclusion : t -> clause + (** What is proved at the root of the clause *) + + val fold : ('a -> proof_node -> 'a) -> 'a -> t -> 'a + (** [fold f acc p], fold [f] over the proof [p] and all its node. It is guaranteed that + [f] is executed exactly once on each proof node in the tree, and that the execution of + [f] on a proof node happens after the execution on the parents of the nodes. *) + + val unsat_core : t -> clause list + (** Returns the unsat_core of the given proof, i.e the lists of conclusions + of all leafs of the proof. + More efficient than using the [fold] function since it has + access to the internal representation of proofs *) + + (** {3 Misc} *) + + val check_empty_conclusion : t -> unit + (** Check that the proof's conclusion is the empty clause, + @raise Resolution_error otherwise *) + + val check : t -> unit + (** Check the contents of a proof. Mainly for internal use. *) + + module Tbl : Hashtbl.S with type key = t +end + +(** The external interface implemented by safe solvers, such as the one + created by the {!Solver.Make} and {!Mcsolver.Make} functors. *) +module type S = sig + (** {2 Internal modules} + These are the internal modules used, you should probably not use them + if you're not familiar with the internals of mSAT. *) + + module Formula : FORMULA + + type formula = Formula.t (** user formulas *) + + type atom + (** The type of atoms given by the module argument for formulas. + An atom is a user-defined atomic formula whose truth value is + picked by Msat. *) + + type clause + + type theory + + type lemma + (** A theory lemma or an input axiom *) + + type solver + + (* TODO: keep this internal *) + module Atom : sig + type t = atom + + val equal : t -> t -> bool + val compare : t -> t -> int + val hash : t -> int + val neg : t -> t + val sign : t -> bool + val abs : t -> t + val formula : t -> formula + val pp : t printer + end + + module Clause : sig + type t = clause + + val atoms : t -> atom array + val atoms_l : t -> atom list + val equal : t -> t -> bool + + val short_name : t -> string + val pp : t printer + + module Tbl : Hashtbl.S with type key = t + end + + module Proof : PROOF + with type clause = clause + and type atom = atom + and type formula = formula + and type lemma = lemma + (** A module to manipulate proofs. *) + + type t = solver + (** Main solver type, containing all state for solving. *) + + val create : + ?on_conflict:(atom array -> unit) -> + ?on_decision:(atom -> unit) -> + ?on_new_atom:(atom -> unit) -> + ?store_proof:bool -> + ?size:[`Tiny|`Small|`Big] -> + theory -> + t + (** Create new solver + @param theory the theory + @param store_proof if true, stores proof (default [true]). Otherwise + the functions that return proofs will fail with [No_proof] + @param size the initial size of internal data structures. The bigger, + the faster, but also the more RAM it uses. *) + + val theory : t -> theory + (** Access the theory state *) + + (** {2 Types} *) + + (** Result type for the solver *) + type res = + | Sat of formula sat_state (** Returned when the solver reaches SAT, with a model *) + | Unsat of (atom,clause,Proof.t) unsat_state (** Returned when the solver reaches UNSAT, with a proof *) + + exception UndecidedLit + (** Exception raised by the evaluating functions when a literal + has not yet been assigned a value. *) + + (** {2 Base operations} *) + + val assume : t -> formula list list -> lemma -> unit + (** Add the list of clauses to the current set of assumptions. + Modifies the sat solver state in place. *) + + val add_clause : t -> atom list -> lemma -> unit + (** Lower level addition of clauses *) + + val add_clause_a : t -> atom array -> lemma -> unit + (** Lower level addition of clauses *) + + val solve : + ?assumptions:atom list -> + t -> res + (** Try and solves the current set of clauses. + @param assumptions additional atomic assumptions to be temporarily added. + The assumptions are just used for this call to [solve], they are + not saved in the solver's state. *) + + val make_atom : t -> formula -> atom + (** Add a new atom (i.e propositional formula) to the solver. + This formula will be decided on at some point during solving, + wether it appears in clauses or not. *) + + val true_at_level0 : t -> atom -> bool + (** [true_at_level0 a] returns [true] if [a] was proved at level0, i.e. + it must hold in all models *) + + val eval_atom : t -> atom -> lbool + (** Evaluate atom in current state *) +end + diff --git a/src/sat/dune b/src/sat/dune new file mode 100644 index 00000000..25a4c2cf --- /dev/null +++ b/src/sat/dune @@ -0,0 +1,10 @@ + +(library + (name sidekick_sat) + (public_name sidekick.sat) + (libraries iter sidekick.util) + (synopsis "Pure OCaml SAT solver implementation for sidekick") + (flags :standard -open Sidekick_util) + (ocamlopt_flags :standard -O3 -bin-annot + -unbox-closures -unbox-closures-factor 20) + ) diff --git a/src/smtlib/Typecheck.ml b/src/smtlib/Typecheck.ml index 703912fc..1faed13b 100644 --- a/src/smtlib/Typecheck.ml +++ b/src/smtlib/Typecheck.ml @@ -5,7 +5,6 @@ open Sidekick_base module Loc = Smtlib_utils.V_2_6.Loc module Fmt = CCFormat -module Log = Msat.Log module PA = Smtlib_utils.V_2_6.Ast module BT = Sidekick_base diff --git a/src/smtlib/dune b/src/smtlib/dune index 318b0cda..4476ec7a 100644 --- a/src/smtlib/dune +++ b/src/smtlib/dune @@ -1,8 +1,8 @@ (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.backend smtlib-utils sidekick.tef) (flags :standard -warn-error -a+8 -open Sidekick_util)) diff --git a/src/tef/Sidekick_tef.dummy.ml b/src/tef/Sidekick_tef.dummy.ml new file mode 100644 index 00000000..994edeb7 --- /dev/null +++ b/src/tef/Sidekick_tef.dummy.ml @@ -0,0 +1,3 @@ + +let setup() = () +let teardown() = () diff --git a/src/tef/Sidekick_tef.ml b/src/tef/Sidekick_tef.real.ml similarity index 100% rename from src/tef/Sidekick_tef.ml rename to src/tef/Sidekick_tef.real.ml diff --git a/src/tef/dune b/src/tef/dune index db8f8b5e..a529f1cf 100644 --- a/src/tef/dune +++ b/src/tef/dune @@ -3,6 +3,10 @@ (name sidekick_tef) (public_name sidekick.tef) (synopsis "profiling backend based on TEF") - (optional) (flags :standard -warn-error -a+8) - (libraries sidekick.util unix threads mtime mtime.clock.os)) + (libraries + sidekick.util unix threads + (select Sidekick_tef.ml from + (mtime mtime.clock.os -> Sidekick_tef.real.ml) + (-> Sidekick_tef.dummy.ml))) + (optional)) diff --git a/src/util/Backtrack_stack.ml b/src/util/Backtrack_stack.ml index 890be02f..81b78f37 100644 --- a/src/util/Backtrack_stack.ml +++ b/src/util/Backtrack_stack.ml @@ -1,6 +1,4 @@ -module Vec = Msat.Vec - type 'a t = { vec: 'a Vec.t; lvls: int Vec.t; diff --git a/src/util/Log.ml b/src/util/Log.ml new file mode 100644 index 00000000..b93d4a7f --- /dev/null +++ b/src/util/Log.ml @@ -0,0 +1,28 @@ + +(** {1 Logging functions, real version} *) + +let enabled = true (* NOTE: change here for 0-overhead *) + +let debug_level_ = ref 0 +let set_debug l = debug_level_ := l +let get_debug () = !debug_level_ + +let debug_fmt_ = ref Format.err_formatter + +let set_debug_out f = debug_fmt_ := f + +(* does the printing, inconditionally *) +let debug_real_ l k = + k (fun fmt -> + Format.fprintf !debug_fmt_ "@[<2>@{[%d|%.3f]@}@ " + l (Sys.time()); + Format.kfprintf + (fun fmt -> Format.fprintf fmt "@]@.") + !debug_fmt_ fmt) + +let[@inline] debugf l k = + if enabled && l <= !debug_level_ then ( + debug_real_ l k; + ) + +let[@inline] debug l msg = debugf l (fun k->k "%s" msg) diff --git a/src/util/Log.mli b/src/util/Log.mli new file mode 100644 index 00000000..f6b7f435 --- /dev/null +++ b/src/util/Log.mli @@ -0,0 +1,24 @@ + +(** Logging function, for debugging *) + +val enabled : bool + +val set_debug : int -> unit +(** Set debug level *) + +val get_debug : unit -> int +(** Current debug level *) + +val debugf : + int -> + ((('a, Format.formatter, unit, unit) format4 -> 'a) -> unit) -> + unit +(** Emit a debug message at the given level. If the level is lower + than [get_debug ()], the message will indeed be emitted *) + +val debug : int -> string -> unit +(** Simpler version of {!debug}, without formatting *) + +val set_debug_out : Format.formatter -> unit +(** Change the output formatter. *) + diff --git a/src/util/Sidekick_util.ml b/src/util/Sidekick_util.ml index 01ae1f46..09b56058 100644 --- a/src/util/Sidekick_util.ml +++ b/src/util/Sidekick_util.ml @@ -1,9 +1,10 @@ (* re-exports *) module Fmt = CCFormat -module Vec = Msat.Vec -module Log = Msat.Log + module Util = Util +module Vec = Vec +module Log = Log module Backtrack_stack = Backtrack_stack module Backtrackable_tbl = Backtrackable_tbl module Error = Error diff --git a/src/util/Vec.ml b/src/util/Vec.ml new file mode 100644 index 00000000..782a8b6a --- /dev/null +++ b/src/util/Vec.ml @@ -0,0 +1,113 @@ + +type 'a t = { + mutable data : 'a array; + mutable sz : int; +} + +let make n x = {data=Array.make n x; sz=0} + +let[@inline] create () = {data = [||]; sz = 0} + +let[@inline] clear s = s.sz <- 0 + +let[@inline] shrink t i = + assert (i >= 0); + assert (i<=t.sz); + t.sz <- i + +let[@inline] pop t = + if t.sz = 0 then invalid_arg "vec.pop"; + let x = Array.unsafe_get t.data (t.sz - 1) in + t.sz <- t.sz - 1; + x + +let[@inline] size t = t.sz + +let[@inline] is_empty t = t.sz = 0 + +let[@inline] is_full t = Array.length t.data = t.sz + +let[@inline] copy t : _ t = + let data = Array.copy t.data in + {t with data} + +(* grow the array *) +let[@inline never] grow_to_double_size t x : unit = + if Array.length t.data = Sys.max_array_length then ( + failwith "vec: cannot resize"; + ); + let size = + min Sys.max_array_length (max 4 (2 * Array.length t.data)) + in + let arr' = Array.make size x in + Array.blit t.data 0 arr' 0 (Array.length t.data); + t.data <- arr'; + assert (Array.length t.data > t.sz); + () + +let[@inline] push t x : unit = + if is_full t then grow_to_double_size t x; + Array.unsafe_set t.data t.sz x; + t.sz <- t.sz + 1 + +let[@inline] get t i = + if i < 0 || i >= t.sz then invalid_arg "vec.get"; + Array.unsafe_get t.data i + +let[@inline] set t i v = + if i < 0 || i > t.sz then invalid_arg "vec.set"; + if i = t.sz then ( + push t v + ) else ( + Array.unsafe_set t.data i v + ) + +let[@inline] fast_remove t i = + assert (i>= 0 && i < t.sz); + Array.unsafe_set t.data i @@ Array.unsafe_get t.data (t.sz - 1); + t.sz <- t.sz - 1 + +let filter_in_place f vec = + let i = ref 0 in + while !i < size vec do + if f (Array.unsafe_get vec.data !i) then incr i else fast_remove vec !i + done + +let sort t f : unit = + let sub_arr = if is_full t then t.data else Array.sub t.data 0 t.sz in + Array.fast_sort f sub_arr; + t.data <- sub_arr + +let[@inline] iter f t = + for i = 0 to size t - 1 do + f (Array.unsafe_get t.data i) + done + +let[@inline] iteri f t = + for i = 0 to size t - 1 do + f i (Array.unsafe_get t.data i) + done + +let[@inline] to_seq a k = iter k a + +let exists p t = Iter.exists p @@ to_seq t +let for_all p t = Iter.for_all p @@ to_seq t +let fold f acc a = Iter.fold f acc @@ to_seq a +let to_list a = Iter.to_list @@ to_seq a +let to_array a = Array.sub a.data 0 a.sz + +let of_list l : _ t = + match l with + | [] -> create() + | x :: tl -> + let v = make (List.length tl+1) x in + List.iter (push v) l; + v + +let pp ?(sep=", ") pp out v = + let first = ref true in + iter + (fun x -> + if !first then first := false else Format.fprintf out "%s@," sep; + pp out x) + v diff --git a/src/util/Vec.mli b/src/util/Vec.mli new file mode 100644 index 00000000..b4994de4 --- /dev/null +++ b/src/util/Vec.mli @@ -0,0 +1,90 @@ + +(** Vectors + + A resizable array, workhorse of imperative programming :-). + This implementation originated in alt-ergo-zero but has been basically rewritten + from scratch several times since. +*) + +type 'a t +(** Abstract type of vectors of 'a *) + +val make : int -> 'a -> 'a t +(** [make cap dummy] creates a new vector filled with [dummy]. The vector + is initially empty but its underlying array has capacity [cap]. + [dummy] will stay alive as long as the vector *) + +val create : unit -> 'a t + +val to_list : 'a t -> 'a list +(** Returns the list of elements of the vector *) + +val to_array : 'a t -> 'a array + +val of_list : 'a list -> 'a t + +val to_seq : 'a t -> 'a Iter.t + +val clear : 'a t -> unit +(** Set size to 0, doesn't free elements *) + +val shrink : 'a t -> int -> unit +(** [shrink vec sz] resets size of [vec] to [sz]. + Assumes [sz >=0 && sz <= size vec] *) + +val pop : 'a t -> 'a +(** Pop last element and return it. + @raise Invalid_argument if the vector is empty *) + +val size : 'a t -> int + +val is_empty : 'a t -> bool + +val is_full : 'a t -> bool +(** Is the capacity of the vector equal to the number of its elements? *) + +val push : 'a t -> 'a -> unit +(** Push element into the vector *) + +val get : 'a t -> int -> 'a +(** get the element at the given index, or + @raise Invalid_argument if the index is not valid *) + +val set : 'a t -> int -> 'a -> unit +(** set the element at the given index, either already set or the first + free slot if [not (is_full vec)], or + @raise Invalid_argument if the index is not valid *) + +val copy : 'a t -> 'a t +(** Fresh copy *) + +val fast_remove : 'a t -> int -> unit +(** Remove element at index [i] without preserving order + (swap with last element) *) + +val filter_in_place : ('a -> bool) -> 'a t -> unit +(** [filter_in_place f v] removes from [v] the elements that do + not satisfy [f] *) + +val sort : 'a t -> ('a -> 'a -> int) -> unit +(** Sort in place the array *) + +val iter : ('a -> unit) -> 'a t -> unit +(** Iterate on elements *) + +val iteri : (int -> 'a -> unit) -> 'a t -> unit +(** Iterate on elements with their index *) + +val fold : ('b -> 'a -> 'b) -> 'b -> 'a t -> 'b +(** Fold over elements *) + +val exists : ('a -> bool) -> 'a t -> bool +(** Does there exist an element that satisfies the predicate? *) + +val for_all : ('a -> bool) -> 'a t -> bool +(** Do all elements satisfy the predicate? *) + +val pp : + ?sep:string -> + (Format.formatter -> 'a -> unit) -> + Format.formatter -> 'a t -> unit 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))