From 3968688a3525d4e60531c099b785b8805da31adc Mon Sep 17 00:00:00 2001 From: Simon Cruanes Date: Wed, 9 May 2018 22:47:21 -0500 Subject: [PATCH] large refactor of SAT solver, all internal code in Internal now --- src/backend/Coq.ml | 191 ---------- src/backend/Coq.mli | 46 --- src/backend/Dedukti.ml | 61 ---- src/backend/Dedukti.mli | 32 -- src/backend/Dimacs.ml | 28 +- src/backend/Dimacs.mli | 4 +- src/backend/Dot.ml | 75 ++-- src/backend/Dot.mli | 10 +- src/backend/jbuild | 3 +- src/main/main.ml | 2 +- src/sat/Internal.ml | 668 ++++++++++++++++++++++++++++++++--- src/sat/Res.ml | 302 ---------------- src/sat/Res.mli | 19 - src/sat/Res_intf.ml | 136 ------- src/sat/Sidekick_sat.ml | 5 +- src/sat/Solver.ml | 64 ++-- src/sat/Solver.mli | 10 +- src/sat/Solver_intf.ml | 167 +++++++-- src/sat/Solver_types.ml | 345 ------------------ src/sat/Solver_types.mli | 18 - src/sat/Solver_types_intf.ml | 208 ----------- src/smt/Solver.ml | 6 +- src/smt/Solver.mli | 4 +- 23 files changed, 861 insertions(+), 1543 deletions(-) delete mode 100644 src/backend/Coq.ml delete mode 100644 src/backend/Coq.mli delete mode 100644 src/backend/Dedukti.ml delete mode 100644 src/backend/Dedukti.mli delete mode 100644 src/sat/Res.ml delete mode 100644 src/sat/Res.mli delete mode 100644 src/sat/Res_intf.ml delete mode 100644 src/sat/Solver_types.ml delete mode 100644 src/sat/Solver_types.mli delete mode 100644 src/sat/Solver_types_intf.ml diff --git a/src/backend/Coq.ml b/src/backend/Coq.ml deleted file mode 100644 index aefcfa6f..00000000 --- a/src/backend/Coq.ml +++ /dev/null @@ -1,191 +0,0 @@ -(* -MSAT is free software, using the Apache license, see file LICENSE -Copyright 2015 Guillaume Bury -*) - -module type S = Backend_intf.S - -module type Arg = sig - - type hyp - type lemma - type assumption - - val prove_hyp : Format.formatter -> string -> hyp -> unit - val prove_lemma : Format.formatter -> string -> lemma -> unit - val prove_assumption : Format.formatter -> string -> assumption -> unit - -end - -module Make(S : Res.S)(A : Arg with type hyp := S.clause - and type lemma := S.clause - and type assumption := S.clause) = struct - - module Atom = S.Atom - module Clause = S.Clause - module M = Map.Make(S.Atom) - module C_tbl = S.Clause.Tbl - - let name = Clause.name - - let clause_map c = - let rec aux acc a i = - if i >= Array.length a then acc - else begin - let name = Format.sprintf "A%d" i in - aux (M.add a.(i) name acc) a (i + 1) - end - in - aux M.empty (Clause.atoms c) 0 - - let clause_iter m format fmt clause = - let aux atom = Format.fprintf fmt format (M.find atom m) in - Array.iter aux (Clause.atoms clause) - - let elim_duplicate fmt goal hyp _ = - (** Printing info comment in coq *) - Format.fprintf fmt - "(* Eliminating doublons. Goal : %s ; Hyp : %s *)@\n" - (name goal) (name hyp); - (** Prove the goal: intro the atoms, then use them with the hyp *) - let m = clause_map goal in - Format.fprintf fmt "pose proof @[(fun %a=>@ %s%a) as %s@].@\n" - (clause_iter m "%s@ ") goal (name hyp) - (clause_iter m "@ %s") hyp (name goal) - - let resolution_aux m a h1 h2 fmt () = - Format.fprintf fmt "%s%a" (name h1) - (fun fmt -> Array.iter (fun b -> - if b == a then begin - Format.fprintf fmt "@ (fun p =>@ %s%a)" - (name h2) (fun fmt -> (Array.iter (fun c -> - if Atom.equal c (Atom.neg a) then - Format.fprintf fmt "@ (fun np => np p)" - else - Format.fprintf fmt "@ %s" (M.find c m))) - ) (Clause.atoms h2) - end else - Format.fprintf fmt "@ %s" (M.find b m) - )) (Clause.atoms h1) - - let resolution fmt goal hyp1 hyp2 atom = - let a = Atom.abs atom in - let h1, h2 = - if Array.exists (Atom.equal a) (Clause.atoms hyp1) then hyp1, hyp2 - else ( - assert (Array.exists (Atom.equal a) (Clause.atoms hyp2)); - hyp2, hyp1 - ) - in - (** Print some debug info *) - Format.fprintf fmt - "(* Clausal resolution. Goal : %s ; Hyps : %s, %s *)@\n" - (name goal) (name h1) (name h2); - (** Prove the goal: intro the axioms, then perform resolution *) - if Array.length (Clause.atoms goal) = 0 then ( - let m = M.empty in - Format.fprintf fmt "exact @[(%a)@].@\n" (resolution_aux m a h1 h2) (); - false - ) else ( - let m = clause_map goal in - Format.fprintf fmt "pose proof @[(fun %a=>@ %a)@ as %s.@]@\n" - (clause_iter m "%s@ ") goal (resolution_aux m a h1 h2) () (name goal); - true - ) - - (* Count uses of hypotheses *) - let incr_use h c = - let i = try C_tbl.find h c with Not_found -> 0 in - C_tbl.add h c (i + 1) - - let decr_use h c = - let i = C_tbl.find h c - 1 in - assert (i >= 0); - let () = C_tbl.add h c i in - i <= 0 - - let clear fmt c = - Format.fprintf fmt "clear %s." (name c) - - let rec clean_aux fmt = function - | [] -> () - | [x] -> - Format.fprintf fmt "%a@\n" clear x - | x :: ((_ :: _) as r) -> - Format.fprintf fmt "%a@ %a" clear x clean_aux r - - let clean h fmt l = - match List.filter (decr_use h) l with - | [] -> () - | l' -> - Format.fprintf fmt "(* Clearing unused clauses *)@\n%a" clean_aux l' - - let prove_node t fmt node = - let clause = node.S.conclusion in - match node.S.step with - | S.Hypothesis -> - A.prove_hyp fmt (name clause) clause - | S.Assumption -> - A.prove_assumption fmt (name clause) clause - | S.Lemma _ -> - A.prove_lemma fmt (name clause) clause - | S.Duplicate (p, l) -> - let c = S.conclusion p in - let () = elim_duplicate fmt clause c l in - clean t fmt [c] - | S.Resolution (p1, p2, a) -> - let c1 = S.conclusion p1 in - let c2 = S.conclusion p2 in - if resolution fmt clause c1 c2 a then clean t fmt [c1; c2] - - let count_uses p = - let h = C_tbl.create 128 in - let aux () node = - List.iter (fun p' -> incr_use h S.(conclusion p')) (S.parents node.S.step) - in - let () = S.fold aux () p in - h - - (* Here the main idea is to always try and have exactly - one goal to prove, i.e False. So each *) - let print fmt p = - let h = count_uses p in - let aux () node = - Format.fprintf fmt "%a" (prove_node h) node - in - Format.fprintf fmt "(* Coq proof generated by mSAT*)@\n"; - S.fold aux () p - -end - - -module Simple(S : Res.S) - (A : Arg with type hyp = S.formula list - and type lemma := S.lemma - and type assumption := S.formula) = - Make(S)(struct - - (* Some helpers *) - let lit = S.Atom.lit - - let get_assumption c = - match S.Clause.atoms_l c with - | [ x ] -> x - | _ -> assert false - - let get_lemma c = - match S.expand (S.prove c) with - | {S.step=S.Lemma p; _} -> p - | _ -> assert false - - let prove_hyp fmt name c = - A.prove_hyp fmt name (List.map lit (S.Clause.atoms_l c)) - - let prove_lemma fmt name c = - A.prove_lemma fmt name (get_lemma c) - - let prove_assumption fmt name c = - A.prove_assumption fmt name (lit (get_assumption c)) - - end) - diff --git a/src/backend/Coq.mli b/src/backend/Coq.mli deleted file mode 100644 index 4e4828dc..00000000 --- a/src/backend/Coq.mli +++ /dev/null @@ -1,46 +0,0 @@ -(* -MSAT is free software, using the Apache license, see file LICENSE -Copyright 2015 Guillaume Bury -*) - -(** Coq Backend - - This module provides an easy way to produce coq scripts - corresponding to the resolution proofs output by the - sat solver. *) - -module type S = Backend_intf.S -(** Interface for exporting proofs. *) - -module type Arg = sig - (** Term printing for Coq *) - - type hyp - type lemma - type assumption - (** The types of hypotheses, lemmas, and assumptions *) - - val prove_hyp : Format.formatter -> string -> hyp -> unit - val prove_lemma : Format.formatter -> string -> lemma -> unit - val prove_assumption : Format.formatter -> string -> assumption -> unit - (** Proving function for hypotheses, lemmas and assumptions. - [prove_x fmt name x] should prove [x], and be such that after - executing it, [x] is among the coq hypotheses under the name [name]. - The hypothesis should be the encoding of the given clause, i.e - for a clause [a \/ not b \/ c], the proved hypothesis should be: - [ ~ a -> ~ ~ b -> ~ c -> False ], keeping the same order as the - one in the atoms array of the clause. *) - -end - -module Make(S : Res.S)(A : Arg with type hyp := S.clause - and type lemma := S.clause - and type assumption := S.clause) : S with type t := S.proof -(** Base functor to output Coq proofs *) - - -module Simple(S : Res.S)(A : Arg with type hyp = S.formula list - and type lemma := S.lemma - and type assumption := S.formula) : S with type t := S.proof -(** Simple functo to output Coq proofs *) - diff --git a/src/backend/Dedukti.ml b/src/backend/Dedukti.ml deleted file mode 100644 index 742f5886..00000000 --- a/src/backend/Dedukti.ml +++ /dev/null @@ -1,61 +0,0 @@ -(* -MSAT is free software, using the Apache license, see file LICENSE -Copyright 2015 Guillaume Bury -*) - -module type S = Backend_intf.S - -module type Arg = sig - - type proof - type lemma - type formula - - val print : Format.formatter -> formula -> unit - val prove : Format.formatter -> lemma -> unit - val context : Format.formatter -> proof -> unit -end - -module Make(S : Res.S)(A : Arg with type formula := S.formula - and type lemma := S.lemma - and type proof := S.proof) = struct - - let pp_nl fmt = Format.fprintf fmt "@\n" - let fprintf fmt format = Format.kfprintf pp_nl fmt format - - let _clause_name = S.Clause.name - - let _pp_clause fmt c = - let rec aux fmt = function - | [] -> () - | a :: r -> - let f, pos = - if S.Atom.is_pos a then - S.Atom.lit a, true - else - S.Atom.lit (S.Atom.neg a), false - in - fprintf fmt "%s _b %a ->@ %a" - (if pos then "_pos" else "_neg") A.print f aux r - in - fprintf fmt "_b : Prop ->@ %a ->@ _proof _b" aux (S.Clause.atoms_l c) - - let context fmt p = - fprintf fmt "(; Embedding ;)"; - fprintf fmt "Prop : Type."; - fprintf fmt "_proof : Prop -> Type."; - fprintf fmt "(; Notations for clauses ;)"; - fprintf fmt "_pos : Prop -> Prop -> Type."; - fprintf fmt "_neg : Prop -> Prop -> Type."; - fprintf fmt "[b: Prop, p: Prop] _pos b p --> _proof p -> _proof b."; - fprintf fmt "[b: Prop, p: Prop] _neg b p --> _pos b p -> _proof b."; - A.context fmt p - - let print fmt p = - fprintf fmt "#NAME Proof."; - fprintf fmt "(; Dedukti file automatically generated by mSAT ;)"; - context fmt p; - () - -end - diff --git a/src/backend/Dedukti.mli b/src/backend/Dedukti.mli deleted file mode 100644 index 5e14c075..00000000 --- a/src/backend/Dedukti.mli +++ /dev/null @@ -1,32 +0,0 @@ -(* -MSAT is free software, using the Apache license, see file LICENSE -Copyright 2014 Guillaume Bury -Copyright 2014 Simon Cruanes -*) - -(** Deduki backend for proofs - - Work in progress... -*) - -module type S = Backend_intf.S - -module type Arg = sig - - type lemma - type proof - type formula - - val print : Format.formatter -> formula -> unit - val prove : Format.formatter -> lemma -> unit - val context : Format.formatter -> proof -> unit -end - -module Make : - functor(S : Res.S) -> - functor(A : Arg - with type formula := S.formula - and type lemma := S.lemma - and type proof := S.proof) -> - S with type t := S.proof -(** Functor to generate a backend to output proofs for the dedukti type checker. *) diff --git a/src/backend/Dimacs.ml b/src/backend/Dimacs.ml index 8a03a05b..53123c29 100644 --- a/src/backend/Dimacs.ml +++ b/src/backend/Dimacs.ml @@ -15,19 +15,17 @@ module type S = sig Format.formatter -> hyps:clause Vec.t -> history:clause Vec.t -> - local:clause Vec.t -> unit val export_icnf : Format.formatter -> hyps:clause Vec.t -> history:clause Vec.t -> - local:clause Vec.t -> unit end -module Make(St : Solver_types_intf.S) = struct +module Make(St : Sidekick_sat.S) = struct type st = St.t (* Dimacs & iCNF export *) @@ -72,20 +70,17 @@ module Make(St : Solver_types_intf.S) = struct ) learnt; lemmas - let export st fmt ~hyps ~history ~local = + let export st fmt ~hyps ~history : unit = assert (Vec.for_all (fun c -> St.Clause.premise c = St.Hyp) hyps); (* Learnt clauses, then filtered to only keep only the theory lemmas; all other learnt clauses should be logical consequences of the rest. *) let lemmas = filter_vec history in - (* Local assertions *) - assert (Vec.for_all (fun c -> St.Local = St.Clause.premise c) local); (* Number of atoms and clauses *) - let n = St.nb_elt st in - let m = Vec.size local + Vec.size hyps + Vec.size lemmas in + let n = St.n_vars st in + let m = Vec.size hyps + Vec.size lemmas in Format.fprintf fmt - "@[p cnf %d %d@,%a%a%a@]@." n m - (export_vec "Local assumptions") local + "@[p cnf %d %d@,%a%a@]@." n m (export_vec "Hypotheses") hyps (export_vec "Lemmas") lemmas @@ -93,24 +88,15 @@ module Make(St : Solver_types_intf.S) = struct let icnf_hyp = ref 0 let icnf_lemmas = ref 0 - let export_icnf fmt ~hyps ~history ~local = + let export_icnf fmt ~hyps ~history = assert (Vec.for_all (fun c -> St.Clause.premise c = St.Hyp) hyps); let lemmas = history in - (* Local assertions *) - let l = List.map - (fun c -> match St.Clause.premise c, St.Clause.atoms c with - | St.Local, [| a |] -> a - | _ -> assert false) - (Vec.to_list local) - in - let local = St.Clause.make_l l St.Local in (* Number of atoms and clauses *) Format.fprintf fmt - "@[%s@,%a%a%a@]@." + "@[%s@,%a%a@]@." (if !icnf_hyp = 0 && !icnf_lemmas = 0 then "p inccnf" else "") (export_icnf_aux icnf_hyp "Hypotheses" (fun x -> Some x)) hyps (export_icnf_aux icnf_lemmas "Lemmas" map_filter_learnt) lemmas - export_assumption local end diff --git a/src/backend/Dimacs.mli b/src/backend/Dimacs.mli index 927f88a9..1686034d 100644 --- a/src/backend/Dimacs.mli +++ b/src/backend/Dimacs.mli @@ -21,7 +21,6 @@ module type S = sig Format.formatter -> hyps:clause Vec.t -> history:clause Vec.t -> - local:clause Vec.t -> unit (** Export the given clause vectors to the dimacs format. The arguments should be transmitted directly from the corresponding @@ -31,7 +30,6 @@ module type S = sig Format.formatter -> hyps:clause Vec.t -> history:clause Vec.t -> - local:clause Vec.t -> unit (** Export the given clause vectors to the dimacs format. The arguments should be transmitted directly from the corresponding @@ -42,6 +40,6 @@ module type S = sig end -module Make(St: Solver_types_intf.S) : S with type clause := St.clause and type st = St.t +module Make(St: Sidekick_sat.S) : S with type clause := St.clause and type st = St.t (** Functor to create a module for exporting probems to the dimacs (& iCNF) formats. *) diff --git a/src/backend/Dot.ml b/src/backend/Dot.ml index 1087f084..2796fa64 100644 --- a/src/backend/Dot.ml +++ b/src/backend/Dot.ml @@ -11,7 +11,6 @@ module type S = Backend_intf.S module type Arg = sig type atom - (* Type of atoms *) type hyp type lemma @@ -28,9 +27,10 @@ module type Arg = sig end -module Default(S : Res.S) = struct +module Default(S : Sidekick_sat.S) = struct module Atom = S.Atom module Clause = S.Clause + module P = S.Proof let print_atom = Atom.pp @@ -49,37 +49,39 @@ module Default(S : Res.S) = struct end (** Functor to provide dot printing *) -module Make(S : Res.S)(A : Arg with type atom := S.atom +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.name n.S.conclusion + let node_id n = Clause.name n.P.conclusion let res_node_id n = (node_id n) ^ "_res" - let proof_id p = node_id (S.expand p) + let proof_id p = node_id (P.expand p) let print_clause fmt c = let v = Clause.atoms c in if Array.length v = 0 then Format.fprintf fmt "⊥" - else + else ( let n = Array.length v in for i = 0 to n - 1 do - Format.fprintf fmt "%a" A.print_atom v.(i); + Format.fprintf fmt "%a" A.print_atom (Array.get 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 S.(n.step) with - | S.Resolution (p1, p2, _) -> + match n.P.step with + | P.Resolution (p1, p2, _) -> print_edge fmt (res_node_id n) (proof_id p1); print_edge fmt (res_node_id n) (proof_id p2) | _ -> () @@ -107,29 +109,29 @@ module Make(S : Res.S)(A : Arg with type atom := S.atom let ttify f c = fun fmt () -> f fmt c let print_contents fmt n = - match S.(n.step) with + match n.P.step with (* Leafs of the proof tree *) - | S.Hypothesis -> - let rule, color, l = A.hyp_info S.(n.conclusion) in + | 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" S.(n.conclusion) rule color l - | S.Assumption -> - let rule, color, l = A.assumption_info S.(n.conclusion) 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" S.(n.conclusion) rule color l - | S.Lemma _ -> - let rule, color, l = A.lemma_info S.(n.conclusion) 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" S.(n.conclusion) rule color l + print_dot_node fmt (node_id n) "LIGHTBLUE" P.(n.conclusion) rule color l (* Tree nodes *) - | S.Duplicate (p, l) -> - print_dot_node fmt (node_id n) "GREY" S.(n.conclusion) "Duplicate" "GREY" + | 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 (S.expand p)) - | S.Resolution (_, _, a) -> - print_dot_node fmt (node_id n) "GREY" S.(n.conclusion) "Resolution" "GREY" + print_edge fmt (node_id n) (node_id (P.expand p)) + | P.Resolution (_, _, a) -> + print_dot_node fmt (node_id n) "GREY" P.(n.conclusion) "Resolution" "GREY" [(fun fmt () -> (Format.fprintf fmt "%s" (node_id n)))]; print_dot_res_node fmt (res_node_id n) a; print_edge fmt (node_id n) (res_node_id n) @@ -140,45 +142,46 @@ module Make(S : Res.S)(A : Arg with type atom := S.atom let print fmt p = Format.fprintf fmt "digraph proof {@\n"; - S.fold (fun () -> print_node fmt) () p; + P.fold (fun () -> print_node fmt) () p; Format.fprintf fmt "}@." end -module Simple(S : Res.S) - (A : Arg with type atom := S.formula - and type hyp = S.formula list +module Simple(S : Sidekick_sat.S) + (A : Arg with type atom := S.atom + and type hyp = S.atom list and type lemma := S.lemma - and type assumption = S.formula) = + and type assumption = S.atom) = Make(S)(struct module Atom = S.Atom module Clause = S.Clause + module P = S.Proof (* Some helpers *) - let lit = Atom.lit + let get_form = Atom.get_formula let get_assumption c = - match S.Clause.atoms_l c with + match Clause.atoms_l c with | [ x ] -> x | _ -> assert false let get_lemma c = - match S.expand (S.prove c) with - | {S.step=S.Lemma p;_} -> p + 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 (Atom.lit a) + A.print_atom fmt a let hyp_info c = - A.hyp_info (List.map lit (S.Clause.atoms_l c)) + A.hyp_info (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)) + A.assumption_info (get_assumption c) end) diff --git a/src/backend/Dot.mli b/src/backend/Dot.mli index 5e76cc33..85313dba 100644 --- a/src/backend/Dot.mli +++ b/src/backend/Dot.mli @@ -47,23 +47,23 @@ module type Arg = sig end -module Default(S : Res.S) : Arg with type atom := S.atom +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 : Res.S)(A : Arg with type atom := S.atom +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 (** Functor for making a module to export proofs to the DOT format. *) -module Simple(S : Res.S)(A : Arg with type atom := S.formula - and type hyp = S.formula list +module Simple(S : Sidekick_sat.S)(A : Arg with type atom := S.atom + and type hyp = S.atom list and type lemma := S.lemma - and type assumption = S.formula) : S with type t := S.proof + and type assumption = S.atom) : S with type t := S.proof (** 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/jbuild b/src/backend/jbuild index 172bb385..6c703b90 100644 --- a/src/backend/jbuild +++ b/src/backend/jbuild @@ -6,7 +6,8 @@ (public_name sidekick.backend) (synopsis "proof backends for Sidekick") (libraries (sidekick.sat)) - (flags (:standard -w +a-4-42-44-48-50-58-32-60@8 -color always -safe-string -open Sidekick_sat)) + (flags (:standard -w +a-4-42-44-48-50-58-32-60@8 -color always -safe-string + -open Sidekick_sat -open Sidekick_util)) (ocamlopt_flags (:standard -O3 -bin-annot -unbox-closures -unbox-closures-factor 20)) )) diff --git a/src/main/main.ml b/src/main/main.ml index a5a8bd07..0b431522 100644 --- a/src/main/main.ml +++ b/src/main/main.ml @@ -34,7 +34,7 @@ let p_progress = ref false let hyps : Ast.term list ref = ref [] -module Dot = Sidekick_backend.Dot.Make(Solver.Sat_solver.Proof)(Sidekick_backend.Dot.Default(Solver.Sat_solver.Proof)) +module Dot = Sidekick_backend.Dot.Make(Solver.Sat_solver) let check_model _state = let check_clause _c = diff --git a/src/sat/Internal.ml b/src/sat/Internal.ml index fb92c14a..6c679daa 100644 --- a/src/sat/Internal.ml +++ b/src/sat/Internal.ml @@ -4,21 +4,109 @@ Copyright 2014 Guillaume Bury Copyright 2014 Simon Cruanes *) -module Make - (St : Solver_types.S) - (Th : Theory_intf.S with type formula = St.formula - and type proof = St.proof) -= struct - module Proof = Res.Make(St) - open St +module Var_fields = Solver_intf.Var_fields + +let v_field_seen_neg = Var_fields.mk_field() +let v_field_seen_pos = Var_fields.mk_field() +let () = Var_fields.freeze() + +module C_fields = Solver_intf.C_fields + +let c_field_attached = C_fields.mk_field () (* watching literals? *) +let c_field_visited = C_fields.mk_field () (* used during propagation and proof generation. *) + +module Make (Th : Theory_intf.S) = struct + type formula = Th.Form.t + type lemma = Th.proof + + type var = { + vid : int; + pa : atom; + na : atom; + mutable v_fields : Var_fields.t; + 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; + mutable watched : clause Vec.t; + } + + and clause = { + name : int; + tag : int option; + atoms : atom array; + mutable cpremise : premise; + mutable activity : float; + mutable c_flags : C_fields.t + } + + and reason = + | Decision + | Bcp of clause + + and premise = + | Hyp + | Local + | Lemma of lemma + | History of clause list + + type proof = clause + + let rec dummy_var = + { vid = -101; + pa = dummy_atom; + na = dummy_atom; + v_fields = Var_fields.empty; + v_level = -1; + v_weight = -1.; + v_idx= -1; + reason = None; + } + and dummy_atom = + { var = dummy_var; + lit = Th.Form.dummy; + watched = Obj.magic 0; + (* should be [Vec.make_empty dummy_clause] + but we have to break the cycle *) + neg = dummy_atom; + is_true = false; + aid = -102; + } + let dummy_clause = + { name = -1; + tag = None; + atoms = [| |]; + activity = -1.; + c_flags = C_fields.empty; + cpremise = History []; + } + + let () = dummy_atom.watched <- Vec.make_empty dummy_clause + + (* Constructors *) + module MF = Hashtbl.Make(Th.Form) + + let name_of_clause c = match c.cpremise with + | Hyp -> "H" ^ string_of_int c.name + | Local -> "L" ^ string_of_int c.name + | Lemma _ -> "T" ^ string_of_int c.name + | History _ -> "C" ^ string_of_int c.name module H = Heap.Make(struct - type t = St.var - let[@inline] cmp i j = Var.weight j < Var.weight i (* comparison by weight *) - let dummy = St.Var.dummy - let idx = St.Var.idx - let set_idx = St.Var.set_idx + type t = var + let[@inline] cmp i j = j.v_weight < i.v_weight (* comparison by weight *) + let dummy = dummy_var + let[@inline] idx v = v.v_idx + let[@inline] set_idx v i = v.v_idx <- i end) exception Sat @@ -48,7 +136,10 @@ module Make (* Singleton type containing the current state *) type t = { - st : St.t; + f_map: var MF.t; + vars: var Vec.t; + mutable cpt_mk_var: int; + mutable cpt_mk_clause: int; th: Th.t lazy_t; @@ -123,20 +214,23 @@ module Make } (* Starting environment. *) - let create_ ~st ~size_trail ~size_lvl th : t = { - st; + let create_ ~size_map ~size_vars ~size_trail ~size_lvl th : t = { + f_map = MF.create size_map; + vars = Vec.make size_vars dummy_var; + cpt_mk_var = 0; + cpt_mk_clause = 0; th; unsat_conflict = None; next_decision = None; - clauses_hyps = Vec.make 0 Clause.dummy; - clauses_learnt = Vec.make 0 Clause.dummy; - clauses_temp = Vec.make 0 Clause.dummy; + clauses_hyps = Vec.make 0 dummy_clause; + clauses_learnt = Vec.make 0 dummy_clause; + clauses_temp = Vec.make 0 dummy_clause; th_head = 0; elt_head = 0; - trail = Vec.make size_trail Atom.dummy; + trail = Vec.make size_trail dummy_atom; elt_levels = Vec.make size_lvl (-1); backtrack_levels = Vec.make size_lvl (-1); backtrack = Vec.make size_lvl (fun () -> ()); @@ -151,6 +245,497 @@ module Make dirty=false; } + type state = t + + let[@inline] n_vars st = Vec.size st.vars + let[@inline] get_var st i = Vec.get st.vars i + + module Var = struct + type t = var + let dummy = dummy_var + 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] id v = v.vid + let[@inline] level v = v.v_level + let[@inline] idx v = v.v_idx + + let[@inline] set_level v lvl = v.v_level <- lvl + let[@inline] set_idx v i = v.v_idx <- i + let[@inline] set_weight v w = v.v_weight <- w + + let[@inline] in_heap v = v.v_idx >= 0 + + let make (st:state) (t:formula) : var * Theory_intf.negated = + let lit, negated = Th.Form.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 = Var_fields.empty; + v_level = -1; + v_idx= -1; + v_weight = 0.; + reason = None; + } + and pa = + { var = var; + lit = lit; + watched = Vec.make 10 dummy_clause; + neg = na; + is_true = false; + aid = cpt_double (* aid = vid*2 *) } + and na = + { var = var; + lit = Th.Form.neg lit; + watched = Vec.make 10 dummy_clause; + 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; + Vec.push st.vars var; + var, negated + + (* Marking helpers *) + let[@inline] clear v = + v.v_fields <- Var_fields.empty + + let[@inline] seen_both v = + Var_fields.get v_field_seen_pos v.v_fields && + Var_fields.get v_field_seen_neg v.v_fields + end + + module Atom = struct + type t = atom + let dummy = dummy_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] get_formula a = a.lit + let[@inline] equal a b = a == b + let[@inline] is_pos a = a == abs a + let[@inline] compare a b = Pervasives.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[@inline] seen a = + let pos = equal a (abs a) in + if pos + then Var_fields.get v_field_seen_pos a.var.v_fields + else Var_fields.get v_field_seen_neg a.var.v_fields + + let[@inline] mark a = + let pos = equal a (abs a) in + if pos + then a.var.v_fields <- Var_fields.set v_field_seen_pos true a.var.v_fields + else a.var.v_fields <- Var_fields.set v_field_seen_neg true a.var.v_fields + + let[@inline] make st lit = + let var, negated = Var.make st lit in + match negated with + | Theory_intf.Negated -> var.na + | Theory_intf.Same_sign -> var.pa + + let pp fmt a = Th.Form.print 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 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" n (name_of_clause c) + + 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][@[%a@]]" + (sign a) (a.var.vid+1) debug_value a Th.Form.print a.lit + + let debug_a out vec = + Array.iteri (fun i a -> if i>0 then Format.fprintf out "@ "; debug out a) vec + end + + module Clause = struct + type t = clause + let dummy = dummy_clause + + let make = + let n = ref 0 in + fun ?tag atoms premise -> + let name = !n in + incr n; + { name; + tag = tag; + atoms = atoms; + c_flags = C_fields.empty; + activity = 0.; + cpremise = premise; + } + + let make_l ?tag l pr = make ?tag (Array.of_list l) pr + + let empty = make [| |] (History []) + let name = name_of_clause + let[@inline] equal c1 c2 = c1==c2 + let[@inline] atoms c = c.atoms + let[@inline] atoms_l c = Array.to_list c.atoms + let[@inline] tag c = c.tag + let hash cl = Array.fold_left (fun i a -> Hashtbl.hash (a.aid, i)) 0 cl.atoms + + let[@inline] premise c = c.cpremise + let[@inline] set_premise c p = c.cpremise <- p + + let[@inline] visited c = C_fields.get c_field_visited c.c_flags + let[@inline] set_visited c b = c.c_flags <- C_fields.set c_field_visited b c.c_flags + + let[@inline] attached c = C_fields.get c_field_attached c.c_flags + let[@inline] set_attached c b = c.c_flags <- C_fields.set c_field_attached b c.c_flags + + 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 pp fmt c = + Format.fprintf fmt "%s : %a" (name c) Atom.pp_a c.atoms + + let debug_premise out = function + | Hyp -> Format.fprintf out "hyp" + | Local -> Format.fprintf out "local" + | Lemma _ -> Format.fprintf out "th_lemma" + | History v -> Util.pp_list (CCFormat.of_to_string name_of_clause) out v + + let debug out ({atoms=arr; cpremise=cp;_}as c) = + Format.fprintf out "%s@[{@[%a@]}@ cpremise={@[%a@]}@]" + (name c) Atom.debug_a arr debug_premise cp + + let pp_dimacs fmt {atoms;_} = + let aux fmt a = + Array.iter (fun p -> + Format.fprintf fmt "%s%d " + (if p == p.var.pa then "-" else "") + (p.var.vid+1) + ) a + in + Format.fprintf fmt "%a0" aux atoms + end + + module Formula = struct + include Th.Form + let pp = print + end + + module Proof = struct + type t = proof + + exception Resolution_error of string + exception Insufficient_hyps + (** Raised when a complete resolution derivation cannot be found using the current hypotheses. *) + + let equal_atoms = Atom.equal + let compare_atoms = Atom.compare + + let merge = List.merge compare_atoms + + let _c = ref 0 + let fresh_pcl_name () = incr _c; "R" ^ (string_of_int !_c) + + (* Compute resolution of 2 clauses *) + let resolve l = + let rec aux resolved acc = function + | [] -> resolved, acc + | [a] -> resolved, a :: acc + | a :: b :: r -> + if equal_atoms a b then + aux resolved (a :: acc) r + else if equal_atoms (a.neg) b then + aux ((a.var.pa) :: resolved) acc r + else + aux resolved (a :: acc) (b :: r) + in + let resolved, new_clause = aux [] [] l in + resolved, List.rev new_clause + + (* Compute the set of doublons of a clause *) + let list c = List.sort Atom.compare (Array.to_list (c.atoms)) + + let analyze cl = + let rec aux duplicates free = function + | [] -> duplicates, free + | [ x ] -> duplicates, x :: free + | x :: ((y :: r) as l) -> + if x == y then + count duplicates (x :: free) x [y] r + else + aux duplicates (x :: free) l + and count duplicates free x acc = function + | (y :: r) when x == y -> + count duplicates free x (y :: acc) r + | l -> + aux (acc :: duplicates) free l + in + let doublons, acc = aux [] [] cl in + doublons, List.rev acc + + let to_list c = + let cl = list c in + let doublons, l = analyze cl in + let conflicts, _ = resolve l in + if doublons <> [] then + Log.debug 5 "Input clause has redundancies"; + if conflicts <> [] then + Log.debug 5 "Input clause is a tautology"; + cl + + (* Comparison of clauses *) + let cmp_cl c d = + let rec aux = function + | [], [] -> 0 + | a :: r, a' :: r' -> + begin match compare_atoms a a' with + | 0 -> aux (r, r') + | x -> x + end + | _ :: _ , [] -> -1 + | [], _ :: _ -> 1 + in + aux (c, d) + + let[@inline] prove conclusion = + assert (conclusion.cpremise <> History []); + conclusion + + let rec set_atom_proof a = + let aux acc b = + if equal_atoms 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 -> + Log.debugf 5 (fun k->k "Analysing: @[%a@ %a@]" Atom.debug a Clause.debug c); + if Array.length c.atoms = 1 then ( + Log.debugf 5 (fun k -> k "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 [| a.neg |] r in + a.var.reason <- Some (Bcp c'); + Log.debugf 5 + (fun k -> k "New reason: @[%a@ %a@]" Atom.debug a Clause.debug c'); + c' + ) + | _ -> + Log.debugf 1 (fun k -> k "Error while proving atom %a" Atom.debug a); + raise (Resolution_error "Cannot prove atom") + + let prove_unsat conflict = + if Array.length conflict.atoms = 0 then conflict + else ( + Log.debugf 2 (fun k -> k "Proving 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 [| |] (History (conflict :: l)) in + Log.debugf 2 (fun k -> k "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 + + (* Interface exposed *) + type node = { + conclusion : clause; + step : step; + } + and step = + | Hypothesis + | Assumption + | Lemma of lemma + | Duplicate of proof * atom list + | Resolution of proof * proof * atom + + let rec chain_res (c, cl) = function + | d :: r -> + Log.debugf 5 + (fun k -> k " Resolving clauses : @[%a@\n%a@]" Clause.debug c Clause.debug d); + let dl = to_list d in + begin match resolve (merge cl dl) with + | [ a ], l -> + begin match r with + | [] -> (l, c, d, a) + | _ -> + let new_clause = Clause.make_l l (History [c; d]) in + chain_res (new_clause, l) r + end + | _ -> + Log.debugf 1 + (fun k -> k "While resolving clauses:@[%a@\n%a@]" + Clause.debug c Clause.debug d); + raise (Resolution_error "Clause mismatch") + end + | _ -> + raise (Resolution_error "Bad history") + + let[@inline] conclusion (p:proof) : clause = p + + let expand conclusion = + Log.debugf 5 (fun k -> k "Expanding : @[%a@]" Clause.debug conclusion); + match conclusion.cpremise with + | Lemma l -> + {conclusion; step = Lemma l; } + | Hyp -> + { conclusion; step = Hypothesis; } + | Local -> + { conclusion; step = Assumption; } + | History [] -> + Log.debugf 1 (fun k -> k "Empty history for clause: %a" Clause.debug conclusion); + raise (Resolution_error "Empty history") + | History [ c ] -> + let duplicates, res = analyze (list c) in + assert (cmp_cl res (list conclusion) = 0); + { conclusion; step = Duplicate (c, List.concat duplicates) } + | History ( c :: ([_] as r)) -> + let (l, c', d', a) = chain_res (c, to_list c) r in + assert (cmp_cl l (to_list conclusion) = 0); + { conclusion; step = Resolution (c', d', a); } + | History ( c :: r ) -> + let (l, c', d', a) = chain_res (c, to_list c) r in + conclusion.cpremise <- History [c'; d']; + assert (cmp_cl l (to_list conclusion) = 0); + { conclusion; step = Resolution (c', d', a); } + + let[@inline] step p = (expand p).step + + (* Proof nodes manipulation *) + let is_leaf = function + | Hypothesis + | Assumption + | Lemma _ -> true + | Duplicate _ + | Resolution _ -> false + + let parents = function + | Hypothesis + | Assumption + | Lemma _ -> [] + | Duplicate (p, _) -> [p] + | Resolution (p, p', _) -> [p; p'] + + let expl = function + | Hypothesis -> "hypothesis" + | Assumption -> "assumption" + | Lemma _ -> "lemma" + | Duplicate _ -> "duplicate" + | Resolution _ -> "resolution" + + (* Compute unsat-core + TODO: replace visited bool by a int unique to each call + of unsat_core, so that the cleanup can be removed ? *) + 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 + | Hyp | Local | Lemma _ -> 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 proof + | Leaving of proof + + 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 + | Resolution (p1, p2, _) -> + Stack.push (Enter p2) s; + 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 p = fold (fun () _ -> ()) () p + end + let[@inline] theory st = Lazy.force st.th let[@inline] at_level_0 st : bool = Vec.is_empty st.backtrack_levels let[@inline] on_backtrack st f : unit = @@ -158,7 +743,6 @@ module Make Vec.push st.backtrack f ) - let[@inline] st t = t.st let[@inline] nb_clauses st = Vec.size st.clauses_hyps let[@inline] decision_level st = Vec.size st.elt_levels let[@inline] base_level st = Vec.size st.user_levels @@ -202,8 +786,8 @@ module Make H.insert st.order v; ) - let new_atom ~permanent st (p:formula) : St.atom = - let a = Atom.make st.st p in + let new_atom ~permanent st (p:formula) : atom = + let a = Atom.make st p in if permanent then ( redo_down_to_level_0 st (fun () -> insert_var_order st a.var) @@ -225,8 +809,8 @@ module Make 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 St.nb_elt st.st - 1 do - Var.set_weight (St.get_elt st.st i) ((Var.weight (St.get_elt st.st i)) *. 1e-100) + for i = 0 to n_vars st - 1 do + Var.set_weight (get_var st i) ((Var.weight (get_var st i)) *. 1e-100) done; st.var_incr <- st.var_incr *. 1e-100; ); @@ -474,7 +1058,7 @@ module Make Wrapper function for adding a new propagated formula. *) let enqueue_bool st a reason : unit = if a.neg.is_true then ( - Util.errorf "(@[sat.enqueue_bool.error@ :false-literal %a@])" Atom.debug a + Util.errorf "(@[sat.enqueue_bool.1@ :false-literal %a@])" Atom.debug a ); let level = decision_level st in Log.debugf 5 @@ -539,7 +1123,7 @@ module Make ) (* result of conflict analysis, containing the learnt clause and some - additional info. + additional 2. invariant: cr_history's order matters, as its head is later used during pop operations to determine the origin of a clause/conflict @@ -609,7 +1193,7 @@ module Make (* look for the next node to expand *) while let a = Vec.get st.trail !tr_ind in - Log.debugf 5 (fun k -> k "(@[sat.conflict.looking-at@ %a@])" St.Atom.debug a); + Log.debugf 5 (fun k -> k "(@[sat.conflict.looking-at@ %a@])" Atom.debug a); (not (Var.seen_both a.var)) || (a.var.v_level < conflict_level) do decr tr_ind; @@ -906,7 +1490,7 @@ module Make f a.lit done - let act_push_ ~permanent st (l:formula IArray.t) (lemma:proof): unit = + let act_push_ ~permanent st (l:formula IArray.t) (lemma:lemma): unit = let atoms = IArray.to_array_map (new_atom ~permanent st) l in let c = Clause.make atoms (Lemma lemma) in Log.debugf 3 @@ -933,7 +1517,7 @@ module Make ) ) else ( Util.errorf "(@[sat.act_propagate.invalid_guard@ :guard %a@ \ - :error all lits are not true@])" + :1 all lits are not true@])" (Util.pp_list Atom.debug) l ) @@ -955,15 +1539,14 @@ module Make propagate = act_propagate st; } - let create ?(size=`Big) ?st () : t = - let st = match st with Some s -> s | None -> St.create ~size () in - let size_trail, size_lvl = match size with - | `Tiny -> 0, 0 - | `Small -> 32, 16 - | `Big -> 600, 50 + let create ?(size=`Big) () : t = + let size_map, size_vars, size_trail, size_lvl = match size with + | `Tiny -> 8, 0, 0, 0 + | `Small -> 16, 0, 32, 16 + | `Big -> 4096, 128, 600, 50 in let rec solver = lazy ( - create_ ~st ~size_trail ~size_lvl th + create_ ~size_map ~size_vars ~size_trail ~size_lvl th ) and th = lazy ( Th.create (actions (Lazy.force solver)) ) in @@ -991,7 +1574,7 @@ module Make (* conflict *) let l = List.rev_map (new_atom ~permanent:false st) l in List.iter (fun a -> insert_var_order st a.var) l; - let c = St.Clause.make_l l (Lemma p) in + let c = Clause.make_l l (Lemma p) in Some c ) @@ -1057,8 +1640,7 @@ module Make | None -> (* No Conflict *) assert (st.elt_head = Vec.size st.trail); assert (st.elt_head = st.th_head); - if Vec.size st.trail = St.nb_elt st.st - then raise Sat; + if Vec.size st.trail = n_vars st then raise Sat; if n_of_conflicts > 0 && !conflictC >= n_of_conflicts then ( Log.debug 3 "(sat.restarting)"; cancel_until st (base_level st); @@ -1074,7 +1656,7 @@ module Make done let eval_level (st:t) lit = - let var, negated = Var.make st.st lit in + let var, negated = Var.make st lit in if not var.pa.is_true && not var.na.is_true then raise UndecidedLit else assert (var.v_level >= 0); @@ -1172,7 +1754,7 @@ module Make (* pop the last factice decision level *) let pop st : unit = if base_level st = 0 then ( - Log.debug 2 "(sat.error: cannot pop (already at level 0))" + Log.debug 2 "(sat.1: cannot pop (already at level 0))" ) else ( Log.debug 3 "(sat.pop-user-level)"; assert (base_level st > 0); @@ -1212,7 +1794,7 @@ module Make cancel_until st (base_level st); List.iter add_lit assumptions | Some _ -> - Log.debug 2 "(sat.local_assumptions.error: already unsat)" + Log.debug 2 "(sat.local_assumptions.1: already unsat)" (* Check satisfiability *) let check_clause c = @@ -1223,7 +1805,7 @@ module Make let res = Array.exists (fun x -> x) tmp in if not res then ( Log.debugf 5 - (fun k -> k "(@[sat.check-clause.error@ :not-satisfied %a@])" Clause.debug c); + (fun k -> k "(@[sat.check-clause.1@ :not-satisfied %a@])" Clause.debug c); false ) else true diff --git a/src/sat/Res.ml b/src/sat/Res.ml deleted file mode 100644 index ae07761e..00000000 --- a/src/sat/Res.ml +++ /dev/null @@ -1,302 +0,0 @@ -(* -MSAT is free software, using the Apache license, see file LICENSE -Copyright 2014 Guillaume Bury -Copyright 2014 Simon Cruanes -*) - -module type S = Res_intf.S -module type FULL = Res_intf.FULL - -module Make(St : Solver_types.S) = struct - - module St = St - - type formula = St.formula - type lemma = St.proof - type clause = St.clause - type atom = St.atom - - exception Insufficient_hyps - exception Resolution_error of string - - (* Log levels *) - let error = 1 - let warn = 3 - let info = 10 - let debug = 80 - - let equal_atoms a b = St.(a.aid) = St.(b.aid) - let compare_atoms a b = Pervasives.compare St.(a.aid) St.(b.aid) - - module Clause = St.Clause - module Atom = St.Atom - - let merge = List.merge compare_atoms - - let _c = ref 0 - let fresh_pcl_name () = incr _c; "R" ^ (string_of_int !_c) - - (* Compute resolution of 2 clauses *) - let resolve l = - let rec aux resolved acc = function - | [] -> resolved, acc - | [a] -> resolved, a :: acc - | a :: b :: r -> - if equal_atoms a b then - aux resolved (a :: acc) r - else if equal_atoms St.(a.neg) b then - aux (St.(a.var.pa) :: resolved) acc r - else - aux resolved (a :: acc) (b :: r) - in - let resolved, new_clause = aux [] [] l in - resolved, List.rev new_clause - - (* Compute the set of doublons of a clause *) - let list c = List.sort St.Atom.compare (Array.to_list St.(c.atoms)) - - let analyze cl = - let rec aux duplicates free = function - | [] -> duplicates, free - | [ x ] -> duplicates, x :: free - | x :: ((y :: r) as l) -> - if x == y then - count duplicates (x :: free) x [y] r - else - aux duplicates (x :: free) l - and count duplicates free x acc = function - | (y :: r) when x == y -> - count duplicates free x (y :: acc) r - | l -> - aux (acc :: duplicates) free l - in - let doublons, acc = aux [] [] cl in - doublons, List.rev acc - - let to_list c = - let cl = list c in - let doublons, l = analyze cl in - let conflicts, _ = resolve l in - if doublons <> [] then - Log.debug warn "Input clause has redundancies"; - if conflicts <> [] then - Log.debug warn "Input clause is a tautology"; - cl - - (* - let pp_cl fmt l = - let rec aux fmt = function - | [] -> () - | a :: r -> - Format.fprintf fmt "%a@,%a" St.pp_atom a aux r - in - Format.fprintf fmt "@[%a@]" aux l - *) - - (* Comparison of clauses *) - let cmp_cl c d = - let rec aux = function - | [], [] -> 0 - | a :: r, a' :: r' -> - begin match compare_atoms a a' with - | 0 -> aux (r, r') - | x -> x - end - | _ :: _ , [] -> -1 - | [], _ :: _ -> 1 - in - aux (c, d) - - let[@inline] prove conclusion = - assert St.(conclusion.cpremise <> History []); - conclusion - - let rec set_atom_proof a = - let aux acc b = - if equal_atoms a.St.neg b then acc - else set_atom_proof b :: acc - in - assert St.(a.var.v_level >= 0); - match St.(a.var.reason) with - | Some St.Bcp c -> - Log.debugf debug (fun k->k "Analysing: @[%a@ %a@]" St.Atom.debug a St.Clause.debug c); - if Array.length c.St.atoms = 1 then ( - Log.debugf debug (fun k -> k "Old reason: @[%a@]" St.Atom.debug a); - c - ) else ( - assert (a.St.neg.St.is_true); - let r = St.History (c :: (Array.fold_left aux [] c.St.atoms)) in - let c' = St.Clause.make [| a.St.neg |] r in - a.St.var.St.reason <- Some St.(Bcp c'); - Log.debugf debug - (fun k -> k "New reason: @[%a@ %a@]" St.Atom.debug a St.Clause.debug c'); - c' - ) - | _ -> - Log.debugf error (fun k -> k "Error while proving atom %a" St.Atom.debug a); - raise (Resolution_error "Cannot prove atom") - - let prove_unsat conflict = - if Array.length conflict.St.atoms = 0 then conflict - else ( - Log.debugf info (fun k -> k "Proving unsat from: @[%a@]" St.Clause.debug conflict); - let l = Array.fold_left (fun acc a -> set_atom_proof a :: acc) [] conflict.St.atoms in - let res = St.Clause.make [| |] (St.History (conflict :: l)) in - Log.debugf info (fun k -> k "Proof found: @[%a@]" St.Clause.debug res); - res - ) - - let prove_atom a = - if St.(a.is_true && a.var.v_level = 0) then - Some (set_atom_proof a) - else - None - - (* Interface exposed *) - type proof = clause - and proof_node = { - conclusion : clause; - step : step; - } - and step = - | Hypothesis - | Assumption - | Lemma of lemma - | Duplicate of proof * atom list - | Resolution of proof * proof * atom - - let rec chain_res (c, cl) = function - | d :: r -> - Log.debugf debug - (fun k -> k " Resolving clauses : @[%a@\n%a@]" St.Clause.debug c St.Clause.debug d); - let dl = to_list d in - begin match resolve (merge cl dl) with - | [ a ], l -> - begin match r with - | [] -> (l, c, d, a) - | _ -> - let new_clause = St.Clause.make_l l (St.History [c; d]) in - chain_res (new_clause, l) r - end - | _ -> - Log.debugf error - (fun k -> k "While resolving clauses:@[%a@\n%a@]" - St.Clause.debug c St.Clause.debug d); - raise (Resolution_error "Clause mismatch") - end - | _ -> - raise (Resolution_error "Bad history") - - let[@inline] conclusion (p:proof) : clause = p - - let expand conclusion = - Log.debugf debug (fun k -> k "Expanding : @[%a@]" St.Clause.debug conclusion); - match conclusion.St.cpremise with - | St.Lemma l -> - {conclusion; step = Lemma l; } - | St.Hyp -> - { conclusion; step = Hypothesis; } - | St.Local -> - { conclusion; step = Assumption; } - | St.History [] -> - Log.debugf error (fun k -> k "Empty history for clause: %a" St.Clause.debug conclusion); - raise (Resolution_error "Empty history") - | St.History [ c ] -> - let duplicates, res = analyze (list c) in - assert (cmp_cl res (list conclusion) = 0); - { conclusion; step = Duplicate (c, List.concat duplicates) } - | St.History ( c :: ([_] as r)) -> - let (l, c', d', a) = chain_res (c, to_list c) r in - assert (cmp_cl l (to_list conclusion) = 0); - { conclusion; step = Resolution (c', d', a); } - | St.History ( c :: r ) -> - let (l, c', d', a) = chain_res (c, to_list c) r in - conclusion.St.cpremise <- St.History [c'; d']; - assert (cmp_cl l (to_list conclusion) = 0); - { conclusion; step = Resolution (c', d', a); } - - (* Proof nodes manipulation *) - let is_leaf = function - | Hypothesis - | Assumption - | Lemma _ -> true - | Duplicate _ - | Resolution _ -> false - - let parents = function - | Hypothesis - | Assumption - | Lemma _ -> [] - | Duplicate (p, _) -> [p] - | Resolution (p, p', _) -> [p; p'] - - let expl = function - | Hypothesis -> "hypothesis" - | Assumption -> "assumption" - | Lemma _ -> "lemma" - | Duplicate _ -> "duplicate" - | Resolution _ -> "resolution" - - (* Compute unsat-core - TODO: replace visited bool by a int unique to each call - of unsat_core, so that the cleanup can be removed ? *) - 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.St.cpremise with - | St.Hyp | St.Local | St.Lemma _ -> aux (c :: res) acc r - | St.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 proof - | Leaving of proof - - 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 - | Resolution (p1, p2, _) -> - Stack.push (Enter p2) s; - 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 p = fold (fun () _ -> ()) () p - -end - diff --git a/src/sat/Res.mli b/src/sat/Res.mli deleted file mode 100644 index 06b9c647..00000000 --- a/src/sat/Res.mli +++ /dev/null @@ -1,19 +0,0 @@ -(* -MSAT is free software, using the Apache license, see file LICENSE -Copyright 2014 Guillaume Bury -Copyright 2014 Simon Cruanes -*) - -(** Resolution proofs - - This modules defines functions to create and manipulate resolution proofs. -*) - -module type S = Res_intf.S -(** Interface for a module manipulating resolution proofs. *) - -module type FULL = Res_intf.FULL - -module Make : functor (St : Solver_types.S) -> FULL with module St = St -(** Functor to create a module building proofs from a sat-solver unsat trace. *) - diff --git a/src/sat/Res_intf.ml b/src/sat/Res_intf.ml deleted file mode 100644 index f88035c5..00000000 --- a/src/sat/Res_intf.ml +++ /dev/null @@ -1,136 +0,0 @@ -(* -MSAT is free software, using the Apache license, see file LICENSE -Copyright 2014 Guillaume Bury -Copyright 2014 Simon Cruanes -*) - -(** Interface for proofs *) - -type 'a printer = Format.formatter -> 'a -> unit - -module type S = sig - (** Signature for a module handling proof by resolution from sat solving traces *) - - (** {3 Type declarations} *) - - exception Insufficient_hyps - (** Raised when a complete resolution derivation cannot be found using the current hypotheses. *) - - type formula - type atom - type lemma - type clause - (** Abstract types for atoms, clauses and theory-specific lemmas *) - - type proof - (** 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 - (** 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 proof * atom list - (** The conclusion is obtained by eliminating multiple occurences of the atom in - the conclusion of the provided proof. *) - | Resolution of proof * proof * atom - (** 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 building functions} *) - - val prove : clause -> proof - (** Given a clause, return a proof of that clause. - @raise Insuficient_hyps if it does not succeed. *) - - val prove_unsat : clause -> proof - (** Given a conflict clause [c], returns a proof of the empty clause. - @raise Insuficient_hyps if it does not succeed. *) - - val prove_atom : atom -> proof option - (** Given an atom [a], returns a proof of the clause [[a]] if [a] is true at level 0 *) - - (** {3 Proof Nodes} *) - - 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). *) - - val parents : step -> proof list - (** Returns the parents of a proof node. *) - - - (** {3 Proof Manipulation} *) - - val expand : proof -> proof_node - (** Return the proof step at the root of a given proof. *) - - val conclusion : proof -> clause - (** What is proved at the root of the clause *) - - val fold : ('a -> proof_node -> 'a) -> 'a -> proof -> '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 : proof -> 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 : proof -> unit - (** Check the contents of a proof. Mainly for internal use *) - - module Clause : sig - type t = clause - val name : t -> string - val atoms : t -> atom array - val atoms_l : t -> atom list - val pp : t printer - (** A nice looking printer for clauses, which sort the atoms before printing. *) - - module Tbl : Hashtbl.S with type key = t - end - - module Atom : sig - type t = atom - val is_pos : t -> bool - val neg : t -> t - val abs : t -> t - val compare : t -> t -> int - val equal : t -> t -> bool - val lit : t -> formula - val pp : t printer - end - - module Tbl : Hashtbl.S with type key = proof -end - -module type FULL = sig - module St : Solver_types.S - (** Module defining atom and clauses *) - - include S with type atom = St.atom - and type lemma = St.proof - and type clause = St.clause - and type formula = St.formula -end diff --git a/src/sat/Sidekick_sat.ml b/src/sat/Sidekick_sat.ml index 3a3c0306..d0a48442 100644 --- a/src/sat/Sidekick_sat.ml +++ b/src/sat/Sidekick_sat.ml @@ -2,9 +2,6 @@ (** Main API *) module Theory_intf = Theory_intf -module Solver_types_intf = Solver_types_intf - -module Res = Res module type S = Solver_intf.S @@ -50,7 +47,7 @@ type ('form, 'proof) slice_actions = ('form, 'proof) Theory_intf.slice_actions = slice_iter : ('form -> unit) -> unit; } -module Make(E : Theory_intf.S) = Solver.Make(Solver_types.Make(E))(E) +module Make = Solver.Make (**/**) module Vec = Vec diff --git a/src/sat/Solver.ml b/src/sat/Solver.ml index b25f2688..0b04ada8 100644 --- a/src/sat/Solver.ml +++ b/src/sat/Solver.ml @@ -8,25 +8,24 @@ module type S = Solver_intf.S open Solver_intf -module Make - (St : Solver_types.S) - (Th : Theory_intf.S with type formula = St.formula - and type proof = St.proof) -= struct - - module St = St - - module S = Internal.Make(St)(Th) +module Make (Th : Theory_intf.S) = struct + module S = Internal.Make(Th) module Proof = S.Proof exception UndecidedLit = S.UndecidedLit - type formula = St.formula - type atom = St.formula - type lit = St.atom - type clause = St.clause + type formula = S.formula + type atom = S.atom + type clause = S.clause type theory = Th.t + type proof = S.proof + type lemma = S.lemma + type premise = S.premise = + | Hyp + | Local + | Lemma of lemma + | History of clause list type t = S.t type solver = t @@ -35,8 +34,8 @@ module Make (* Result type *) type res = - | Sat of St.formula sat_state - | Unsat of (St.clause,Proof.proof) unsat_state + | Sat of formula sat_state + | Unsat of (clause,proof) unsat_state let pp_all st lvl status = Log.debugf lvl @@ -44,15 +43,15 @@ module Make "@[%s - Full resume:@,@[Trail:@\n%a@]@,\ @[Temp:@\n%a@]@,@[Hyps:@\n%a@]@,@[Lemmas:@\n%a@]@,@]@." status - (Vec.print ~sep:"" St.Atom.debug) (S.trail st) - (Vec.print ~sep:"" St.Clause.debug) (S.temp st) - (Vec.print ~sep:"" St.Clause.debug) (S.hyps st) - (Vec.print ~sep:"" St.Clause.debug) (S.history st) + (Vec.print ~sep:"" S.Atom.debug) (S.trail st) + (Vec.print ~sep:"" S.Clause.debug) (S.temp st) + (Vec.print ~sep:"" S.Clause.debug) (S.hyps st) + (Vec.print ~sep:"" S.Clause.debug) (S.history st) ) let mk_sat (st:S.t) : _ sat_state = pp_all st 99 "SAT"; - let iter f : unit = Vec.iter (fun a -> f a.St.lit) (S.trail st) in + let iter f : unit = Vec.iter (fun a -> f a.S.lit) (S.trail st) in Sat_state { eval = S.eval st; eval_level = S.eval_level st; @@ -109,6 +108,7 @@ module Make cleanup_ st; S.pop st + let n_vars = S.n_vars let unsat_core = S.Proof.unsat_core let true_at_level0 st a = @@ -117,7 +117,7 @@ module Make b && lev = 0 with S.UndecidedLit -> false - let get_tag cl = St.(cl.tag) + let[@inline] get_tag cl = S.(cl.tag) let[@inline] new_atom ~permanent st a = cleanup_ st; @@ -125,32 +125,30 @@ module Make let actions = S.actions - let export (st:t) : St.clause export = + let export (st:t) : S.clause export = let hyps = S.hyps st in let history = S.history st in let local = S.temp st in {hyps; history; local} - module Lit = struct - type t = lit - - let pp = St.Atom.pp + module Atom = struct + include S.Atom let make = S.new_atom ~permanent:false end module Clause = struct - include St.Clause + include S.Clause - let atoms c = St.Clause.atoms c |> IArray.of_array_map (fun a -> a.St.lit) - let atoms_l c = St.Clause.atoms_l c |> List.map (fun a -> a.St.lit) + let forms c = atoms c |> IArray.of_array_map Atom.get_formula + let forms_l c = atoms_l c |> List.map Atom.get_formula - let[@inline] make ?tag (a:lit array) : t = St.Clause.make ?tag a St.Hyp - let[@inline] make_l ?tag l : t = St.Clause.make_l ?tag l St.Hyp + let[@inline] make ?tag (a:atom array) : t = S.Clause.make ?tag a S.Hyp + let[@inline] make_l ?tag l : t = S.Clause.make_l ?tag l S.Hyp - let of_atoms st ?tag l = + let of_formulas st ?tag l = let l = List.map (S.new_atom ~permanent:false st) l in make_l ?tag l end - module Formula = St.Formula + module Formula = S.Formula end diff --git a/src/sat/Solver.mli b/src/sat/Solver.mli index 1a18d7cf..4176bb3b 100644 --- a/src/sat/Solver.mli +++ b/src/sat/Solver.mli @@ -13,14 +13,10 @@ Copyright 2014 Simon Cruanes module type S = Solver_intf.S (** Safe external interface of solvers. *) -module Make - (St : Solver_types.S) - (Th : Theory_intf.S with type formula = St.formula - and type proof = St.proof) - : S with type formula = St.formula - and type clause = St.clause - and type Proof.lemma = St.proof +module Make(Th : Theory_intf.S) + : S with type formula = Th.formula and type theory = Th.t + and type lemma = Th.proof (** Functor to make a safe external interface. *) diff --git a/src/sat/Solver_intf.ml b/src/sat/Solver_intf.ml index 1f7a5ca6..d6c1d846 100644 --- a/src/sat/Solver_intf.ml +++ b/src/sat/Solver_intf.ml @@ -5,6 +5,11 @@ functor in {!Solver} or {!Mcsolver}. *) +module Var_fields = BitField.Make() +module C_fields = BitField.Make() + +type 'a printer = Format.formatter -> 'a -> unit + type 'form sat_state = Sat_state of { eval: 'form -> bool; (** Returns the valuation of a formula in the current state @@ -37,8 +42,6 @@ type 'clause export = { } (** Export internal state *) -type 'a printer = Format.formatter -> 'a -> unit - (** The external interface implemented by safe solvers, such as the one created by the {!Solver.Make} and {!Mcsolver.Make} functors. *) module type S = sig @@ -46,16 +49,29 @@ module type S = sig These are the internal modules used, you should probably not use them if you're not familiar with the internals of mSAT. *) - type formula (** user formulas *) + type formula + (** 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 lit (** SAT solver literals *) + + type atom (** SAT solver literals *) type clause (** SAT solver clauses *) type theory (** user theory *) - module Proof : Res.S with type clause = clause - (** A module to manipulate proofs. *) + type proof + (** Lazy type for proof trees. Proofs are persistent objects, and can be + extended to proof nodes using functions defined later. *) + + type lemma (** A theory lemma, used to justify a theory conflict clause *) + + type premise = + | Hyp + | Local + | Lemma of lemma + | History of clause list type t (** Main solver type, containing all state for solving. *) @@ -67,15 +83,10 @@ module type S = sig (** {2 Types} *) - type atom = formula - (** 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. *) - (** Result type for the solver *) type res = | Sat of formula sat_state (** Returned when the solver reaches SAT, with a model *) - | Unsat of (clause,Proof.proof) unsat_state (** Returned when the solver reaches UNSAT, with a proof *) + | Unsat of (clause,proof) unsat_state (** Returned when the solver reaches UNSAT, with a proof *) exception UndecidedLit (** Exception raised by the evaluating functions when a literal @@ -83,9 +94,11 @@ module type S = sig (** {2 Base operations} *) + val n_vars : t -> int + val theory : t -> theory - val assume : ?permanent:bool -> t -> ?tag:int -> atom list list -> unit + val assume : ?permanent:bool -> t -> ?tag:int -> formula list list -> unit (** Add the list of clauses to the current set of assumptions. Modifies the sat solver state in place. @param permanent if true, kept after backtracking (default true) *) @@ -94,23 +107,23 @@ module type S = sig (** Lower level addition of clauses. See {!Clause} to create clauses. @param permanent if true, kept after backtracking *) - val solve : t -> ?assumptions:atom list -> unit -> res + val solve : t -> ?assumptions:formula list -> unit -> 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 new_atom : permanent:bool -> t -> atom -> unit + val new_atom : permanent:bool -> t -> formula -> unit (** Add a new atom (i.e propositional formula) to the solver. This formula will be decided on at some point during solving, whether it appears in clauses or not. @param permanent if true, kept after backtracking *) - val unsat_core : Proof.proof -> clause list + val unsat_core : proof -> clause list (** Returns the unsat core of a given proof, ie a subset of all the added clauses that is sufficient to establish unsatisfiability. *) - val true_at_level0 : t -> atom -> bool + val true_at_level0 : t -> formula -> bool (** [true_at_level0 a] returns [true] if [a] was proved at level0, i.e. it must hold in all models *) @@ -126,7 +139,7 @@ module type S = sig (** Return to last save point, discarding clauses added since last call to [push] *) - val actions : t -> (formula,Proof.lemma) Theory_intf.actions + val actions : t -> (formula,lemma) Theory_intf.actions (** Obtain actions *) val export : t -> clause export @@ -135,30 +148,132 @@ module type S = sig type solver = t - module Lit : sig - type t = lit + module Atom : sig + type t = atom + val is_pos : t -> bool + val neg : t -> t + val abs : t -> t + val compare : t -> t -> int + val equal : t -> t -> bool + val get_formula : t -> formula - val make : solver -> atom -> t - val pp : t CCFormat.printer + val make : solver -> formula -> t + + val pp : t printer end + (** A module to manipulate proofs. *) + module Proof : sig + type t = proof + + type 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 + (** 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 proof * atom list + (** The conclusion is obtained by eliminating multiple occurences of the atom in + the conclusion of the provided proof. *) + | Resolution of proof * proof * atom + (** 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. *) + + exception Insufficient_hyps + (** Raised when a complete resolution derivation cannot be found using the current hypotheses. *) + + (** {3 Proof building functions} *) + + val prove : clause -> t + (** Given a clause, return a proof of that clause. + @raise Insuficient_hyps if it does not succeed. *) + + val prove_unsat : clause -> t + (** Given a conflict clause [c], returns a proof of the empty clause. + @raise Insuficient_hyps 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 *) + + (** {3 Proof Nodes} *) + + 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). *) + + val parents : step -> t list + (** Returns the parents of a proof node. *) + + (** {3 Proof Manipulation} *) + + val expand : proof -> node + (** Return the proof step at the root of a given proof. *) + + val step : proof -> step + + val conclusion : proof -> clause + (** What is proved at the root of the clause *) + + val fold : ('a -> 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 : t -> unit + (** Check the contents of a proof. Mainly for internal use *) + + module Tbl : Hashtbl.S with type key = t + end + module Clause : sig type t = clause - val atoms : t -> atom IArray.t + val atoms : t -> atom array (** do not modify *) val atoms_l : t -> atom list + val forms : t -> formula IArray.t + val forms_l : t -> formula list val tag : t -> int option val equal : t -> t -> bool - val make : ?tag:int -> lit array -> t + val make : ?tag:int -> atom array -> t (** Make a clause from this array of SAT literals. The array's ownership is transferred to the clause, do not mutate it *) - val make_l : ?tag:int -> lit list -> t + val make_l : ?tag:int -> atom list -> t - val of_atoms : solver -> ?tag:int -> atom list -> t + val of_formulas : solver -> ?tag:int -> formula list -> t + val premise : t -> premise + + val name : t -> string val pp : t printer + val pp_dimacs : t printer + + val dummy : t + + module Tbl : Hashtbl.S with type key = t end module Formula : sig diff --git a/src/sat/Solver_types.ml b/src/sat/Solver_types.ml deleted file mode 100644 index 07d194fa..00000000 --- a/src/sat/Solver_types.ml +++ /dev/null @@ -1,345 +0,0 @@ -module type S = Solver_types_intf.S - -module Var_fields = Solver_types_intf.Var_fields - -let v_field_seen_neg = Var_fields.mk_field() -let v_field_seen_pos = Var_fields.mk_field() -let () = Var_fields.freeze() - -module C_fields = Solver_types_intf.C_fields - -let c_field_attached = C_fields.mk_field () (* watching literals? *) -let c_field_visited = C_fields.mk_field () (* used during propagation and proof generation. *) - -(* Solver types for McSat Solving *) -(* ************************************************************************ *) - -module Make (E : Theory_intf.S) = struct - - type formula = E.Form.t - type proof = E.proof - - type var = { - vid : int; - pa : atom; - na : atom; - mutable v_fields : Var_fields.t; - 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; - mutable watched : clause Vec.t; - } - - and clause = { - name : int; - tag : int option; - atoms : atom array; - mutable cpremise : premise; - mutable activity : float; - mutable c_flags : C_fields.t - } - - and reason = - | Decision - | Bcp of clause - - and premise = - | Hyp - | Local - | Lemma of proof - | History of clause list - - let rec dummy_var = - { vid = -101; - pa = dummy_atom; - na = dummy_atom; - v_fields = Var_fields.empty; - v_level = -1; - v_weight = -1.; - v_idx= -1; - reason = None; - } - and dummy_atom = - { var = dummy_var; - lit = E.Form.dummy; - watched = Obj.magic 0; - (* should be [Vec.make_empty dummy_clause] - but we have to break the cycle *) - neg = dummy_atom; - is_true = false; - aid = -102; - } - let dummy_clause = - { name = -1; - tag = None; - atoms = [| |]; - activity = -1.; - c_flags = C_fields.empty; - cpremise = History []; - } - - let () = dummy_atom.watched <- Vec.make_empty dummy_clause - - (* Constructors *) - module MF = Hashtbl.Make(E.Form) - - type t = { - f_map: var MF.t; - vars: var Vec.t; - mutable cpt_mk_var: int; - mutable cpt_mk_clause: int; - } - - type state = t - - let create_ size_map size_vars () : t = { - f_map = MF.create size_map; - vars = Vec.make size_vars dummy_var; - cpt_mk_var = 0; - cpt_mk_clause = 0; - } - - let create ?(size=`Big) () : t = - let size_map, size_vars = match size with - | `Tiny -> 8, 0 - | `Small -> 16, 10 - | `Big -> 4096, 128 - in - create_ size_map size_vars () - - 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 name_of_clause c = match c.cpremise with - | Hyp -> "H" ^ string_of_int c.name - | Local -> "L" ^ string_of_int c.name - | Lemma _ -> "T" ^ string_of_int c.name - | History _ -> "C" ^ string_of_int c.name - - module Var = struct - type t = var - let dummy = dummy_var - 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] id v = v.vid - let[@inline] level v = v.v_level - let[@inline] idx v = v.v_idx - - let[@inline] set_level v lvl = v.v_level <- lvl - let[@inline] set_idx v i = v.v_idx <- i - let[@inline] set_weight v w = v.v_weight <- w - - let[@inline] in_heap v = v.v_idx >= 0 - - let make (st:state) (t:formula) : var * Theory_intf.negated = - let lit, negated = E.Form.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 = Var_fields.empty; - v_level = -1; - v_idx= -1; - v_weight = 0.; - reason = None; - } - and pa = - { var = var; - lit = lit; - watched = Vec.make 10 dummy_clause; - neg = na; - is_true = false; - aid = cpt_double (* aid = vid*2 *) } - and na = - { var = var; - lit = E.Form.neg lit; - watched = Vec.make 10 dummy_clause; - 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; - Vec.push st.vars var; - var, negated - - (* Marking helpers *) - let[@inline] clear v = - v.v_fields <- Var_fields.empty - - let[@inline] seen_both v = - Var_fields.get v_field_seen_pos v.v_fields && - Var_fields.get v_field_seen_neg v.v_fields - end - - module Atom = struct - type t = atom - let dummy = dummy_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] lit a = a.lit - let[@inline] equal a b = a == b - let[@inline] is_pos a = a == abs a - let[@inline] compare a b = Pervasives.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[@inline] seen a = - let pos = equal a (abs a) in - if pos - then Var_fields.get v_field_seen_pos a.var.v_fields - else Var_fields.get v_field_seen_neg a.var.v_fields - - let[@inline] mark a = - let pos = equal a (abs a) in - if pos - then a.var.v_fields <- Var_fields.set v_field_seen_pos true a.var.v_fields - else a.var.v_fields <- Var_fields.set v_field_seen_neg true a.var.v_fields - - let[@inline] make st lit = - let var, negated = Var.make st lit in - match negated with - | Theory_intf.Negated -> var.na - | Theory_intf.Same_sign -> var.pa - - let pp fmt a = E.Form.print 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 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" n (name_of_clause c) - - 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][@[%a@]]" - (sign a) (a.var.vid+1) debug_value a E.Form.print a.lit - - let debug_a out vec = - Array.iteri (fun i a -> if i>0 then Format.fprintf out "@ "; debug out a) vec - end - - module Clause = struct - type t = clause - let dummy = dummy_clause - - let make = - let n = ref 0 in - fun ?tag atoms premise -> - let name = !n in - incr n; - { name; - tag = tag; - atoms = atoms; - c_flags = C_fields.empty; - activity = 0.; - cpremise = premise; - } - - let make_l ?tag l pr = make ?tag (Array.of_list l) pr - - let empty = make [| |] (History []) - let name = name_of_clause - let[@inline] equal c1 c2 = c1==c2 - let[@inline] atoms c = c.atoms - let[@inline] atoms_l c = Array.to_list c.atoms - let[@inline] tag c = c.tag - let hash cl = Array.fold_left (fun i a -> Hashtbl.hash (a.aid, i)) 0 cl.atoms - - let[@inline] premise c = c.cpremise - let[@inline] set_premise c p = c.cpremise <- p - - let[@inline] visited c = C_fields.get c_field_visited c.c_flags - let[@inline] set_visited c b = c.c_flags <- C_fields.set c_field_visited b c.c_flags - - let[@inline] attached c = C_fields.get c_field_attached c.c_flags - let[@inline] set_attached c b = c.c_flags <- C_fields.set c_field_attached b c.c_flags - - 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 pp fmt c = - Format.fprintf fmt "%s : %a" (name c) Atom.pp_a c.atoms - - let debug_premise out = function - | Hyp -> Format.fprintf out "hyp" - | Local -> Format.fprintf out "local" - | Lemma _ -> Format.fprintf out "th_lemma" - | History v -> Util.pp_list (CCFormat.of_to_string name_of_clause) out v - - let debug out ({atoms=arr; cpremise=cp;_}as c) = - Format.fprintf out "%s@[{@[%a@]}@ cpremise={@[%a@]}@]" - (name c) Atom.debug_a arr debug_premise cp - - let pp_dimacs fmt {atoms;_} = - let aux fmt a = - Array.iter (fun p -> - Format.fprintf fmt "%s%d " - (if p == p.var.pa then "-" else "") - (p.var.vid+1) - ) a - in - Format.fprintf fmt "%a0" aux atoms - end - - module Formula = struct - include E.Form - let pp = print - end -end[@@inline] diff --git a/src/sat/Solver_types.mli b/src/sat/Solver_types.mli deleted file mode 100644 index a8635834..00000000 --- a/src/sat/Solver_types.mli +++ /dev/null @@ -1,18 +0,0 @@ - -(** Internal types (implementation) - - This modules actually implements the internal types used by the solver. - Since mutation is heavily used in the solver, it is really, really, *really* - discouraged to direclty use the functions in this module if you don't know the - inner working of mSAT perfectly as even the simplest - change can have dramatic effects on the solver. -*) - -module type S = Solver_types_intf.S -(** Interface for the internal types. *) - -module Make (E : Theory_intf.S): - S with type formula = E.formula - and type proof = E.proof -(** Functor to instantiate the types of clauses for a solver. *) - diff --git a/src/sat/Solver_types_intf.ml b/src/sat/Solver_types_intf.ml deleted file mode 100644 index 557f9520..00000000 --- a/src/sat/Solver_types_intf.ml +++ /dev/null @@ -1,208 +0,0 @@ -(** Internal types (interface) - - This modules defines the interface of most of the internal types - used in the core solver. -*) - -module Var_fields = BitField.Make() -module C_fields = BitField.Make() - -type 'a printer = Format.formatter -> 'a -> unit - -module type S = sig - (** The signatures of clauses used in the Solver. *) - - type t - (** State for creating new terms, literals, clauses *) - - val create: ?size:[`Tiny|`Small|`Big] -> unit -> t - - (** {2 Type definitions} *) - - type formula - type proof - (** The types of formulas and proofs. All of these are user-provided. *) - - (* TODO: hide these types (from the outside of [Msat]); - instead, provide well defined modules [module Lit : sig type t val …] - that define their API in Msat itself (not here) *) - - type var = { - vid : int; (** Unique identifier *) - pa : atom; (** Link for the positive atom *) - na : atom; (** Link for the negative atom *) - mutable v_fields : Var_fields.t; (** bool fields *) - mutable v_level : int; (** Level of decision/propagation *) - mutable v_idx: int; (** rank in variable heap *) - mutable v_weight : float; (** Variable weight (for the heap) *) - mutable reason : reason option; - (** The reason for propagation/decision of the literal *) - } - - and atom = { - aid : int; (** Unique identifier *) - var : var; (** Link for the parent variable *) - neg : atom; (** Link for the negation of the atom *) - lit : formula; (** Wrapped formula *) - mutable is_true : bool; (** Is the atom true ? Conversely, the atom - is false iff a.neg.is_true *) - mutable watched : clause Vec.t; (** The vector of clauses that watch this atom *) - } - (** Atoms and variables wrap theory formulas. They exist in the form of - triplet: a variable and two atoms. For a formula [f] in normal form, - the variable v points to the positive atom [a] which wraps [f], while - [a.neg] wraps the theory negation of [f]. *) - - and clause = { - name : int; (** Clause name, mainly for printing, unique. *) - tag : int option; (** User-provided tag for clauses. *) - atoms : atom array; (** The atoms that constitute the clause.*) - mutable cpremise : premise; (** The premise of the clause, i.e. the justification - of why the clause must be satisfied. *) - mutable activity : float; (** Clause activity, used for the heap heuristics. *) - mutable c_flags: C_fields.t; (** Boolean flags for the clause *) - } - (** The type of clauses. Each clause generated should be true, i.e. enforced - by the current problem (for more information, see the cpremise field). *) - - and reason = - | Decision (** The atom has been decided by the sat solver *) - | Bcp of clause (** The atom has been propagated by the given clause *) - (** Reasons of propagation/decision of atoms. *) - - and premise = - | Hyp (** The clause is a hypothesis, provided by the user. *) - | Local (** The clause is a 1-atom clause, - where the atom is a local assumption*) - | Lemma of proof (** The clause is a theory-provided tautology, with - the given proof. *) - | History of clause list (** The clause can be obtained by resolution of the clauses - in the list. If the list has a single element [c] , then - the clause can be obtained by simplifying [c] (i.e - eliminating doublons in its atom list). - For a premise [History [a_1 :: ... :: a_n]] ([n > 0]) - the clause is obtained by performing resolution of - [a_1] with [a_2], and then performing a resolution step between - the result and [a_3], etc... - Of course, each of the clause [a_i] also has its own premise. *) - (** Premises for clauses. Indeed each clause generated during a run of the solver - should be satisfied, the premise is the justification of why it should be - satisfied by the solver. *) - - (** {2 Decisions and propagations} *) - - (** {2 Elements} *) - - val nb_elt : t -> int - val get_elt : t -> int -> var - val iter_elt : t -> (var -> unit) -> unit - (** Read access to the vector of variables created *) - - (** {2 Variables, Literals & Clauses } *) - - type state = t - - module Var : sig - type t = var - val dummy : t - - val pos : t -> atom - val neg : t -> atom - - val level : t -> int - val idx : t -> int - val reason : t -> reason option - val weight : t -> float - - val set_level : t -> int -> unit - val set_idx : t -> int -> unit - val set_weight : t -> float -> unit - - val in_heap : t -> bool - - val make : state -> formula -> t * Theory_intf.negated - (** Returns the variable linked with the given formula, - and whether the atom associated with the formula - is [var.pa] or [var.na] *) - - val seen_both : t -> bool - (** both atoms have been seen? *) - - val clear : t -> unit - (** Clear the 'seen' field of the variable. *) - end - - module Atom : sig - type t = atom - val dummy : t - val level : t -> int - val reason : t -> reason option - val lit : t -> formula - val equal : t -> t -> bool - val compare : t -> t -> int - val var : t -> Var.t - val abs : t -> t (** positive atom *) - val neg : t -> t - val id : t -> int - val is_pos : t -> bool (* positive atom? *) - val is_true : t -> bool - val is_false : t -> bool - - val make : state -> formula -> t - (** Returns the atom associated with the given formula *) - - val mark : t -> unit - (** Mark the atom as seen, using the 'seen' field in the variable. *) - - val seen : t -> bool - (** Returns wether the atom has been marked as seen. *) - - val pp : t printer - val pp_a : t array printer - val debug : t printer - val debug_a : t array printer - end - - module Clause : sig - type t = clause - val dummy : t - - val name : t -> string - val equal : t -> t -> bool - val hash : t -> int - val atoms : t -> Atom.t array - val atoms_l : t -> Atom.t list - val tag : t -> int option - val premise : t -> premise - - val attached : t -> bool - val set_attached : t -> bool -> unit - val visited : t -> bool - val set_visited : t -> bool -> unit - - val empty : t - (** The empty clause *) - - val make : ?tag:int -> Atom.t array -> premise -> t - (** [make_clause name atoms size premise] creates a clause with - the given attributes. - The array's ownership is transferred to the clause, do not - mutate it after that. *) - - val make_l : ?tag:int -> Atom.t list -> premise -> t - - val pp : t printer - val pp_dimacs : t printer - val debug : t printer - - module Tbl : Hashtbl.S with type key = t - end - - module Formula : sig - type t = formula - val equal : t -> t -> bool - val hash : t -> int - val pp : t printer - end -end - diff --git a/src/smt/Solver.ml b/src/smt/Solver.ml index 332a2a8b..8f05a745 100644 --- a/src/smt/Solver.ml +++ b/src/smt/Solver.ml @@ -14,10 +14,10 @@ type level = int module Sat_solver = Sidekick_sat.Make(Theory_combine) let[@inline] clause_of_mclause (c:Sat_solver.clause): Lit.t IArray.t = - Sat_solver.Clause.atoms c + Sat_solver.Clause.forms c module Proof = struct - type t = Sat_solver.Proof.proof + type t = Sat_solver.Proof.t let pp out (p:t) : unit = let pp_step_res out p = @@ -389,7 +389,7 @@ let do_on_exit ~on_exit = let assume (self:t) (c:Lit.t IArray.t) : unit = let sat = solver self in - let c = Sat_solver.Clause.make (IArray.to_array_map (Sat_solver.Lit.make sat) c) in + let c = Sat_solver.Clause.make (IArray.to_array_map (Sat_solver.Atom.make sat) c) in Sat_solver.add_clause ~permanent:false sat c let[@inline] assume_eq self t u expl : unit = diff --git a/src/smt/Solver.mli b/src/smt/Solver.mli index 39c2a66f..bb921ef7 100644 --- a/src/smt/Solver.mli +++ b/src/smt/Solver.mli @@ -8,14 +8,14 @@ module Sat_solver : Sidekick_sat.S with type formula = Lit.t and type theory = Theory_combine.t - and type Proof.lemma = Theory_combine.proof + and type lemma = Theory_combine.proof (** {2 Result} *) type model = Model.t module Proof : sig - type t = Sat_solver.Proof.proof + type t = Sat_solver.Proof.t val pp : t CCFormat.printer end