diff --git a/src/backend/Backend_intf.ml b/src/backend/Backend_intf.ml
index 29900a0c..b83b5acb 100644
--- a/src/backend/Backend_intf.ml
+++ b/src/backend/Backend_intf.ml
@@ -17,10 +17,12 @@ module type S = sig
according to the conventions of a given format.
*)
+ type store
+
type t
(** The type of proofs. *)
- val pp : Format.formatter -> t -> unit
+ val pp : store -> 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
index 7085fc86..e8f2f8e1 100644
--- a/src/backend/Dot.ml
+++ b/src/backend/Dot.ml
@@ -13,17 +13,18 @@ module type Arg = sig
type atom
(* Type of atoms *)
+ type store
type hyp
type lemma
type assumption
(** Types for hypotheses, lemmas, and assumptions. *)
- val print_atom : Format.formatter -> atom -> unit
+ val print_atom : store -> 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
+ val hyp_info : store -> hyp -> string * string option * (Format.formatter -> unit -> unit) list
+ val lemma_info : store -> lemma -> string * string option * (Format.formatter -> unit -> unit) list
+ val assumption_info : store -> assumption -> string * string option * (Format.formatter -> unit -> unit) list
(** Functions to return information about hypotheses and lemmas *)
end
@@ -32,19 +33,20 @@ module Default(S : Sidekick_sat.S) = struct
module Atom = S.Atom
module Clause = S.Clause
- let print_atom = Atom.pp
+ type store = S.solver
+ let print_atom = S.Atom.pp
- let hyp_info c =
+ let hyp_info store c =
"hypothesis", Some "LIGHTBLUE",
- [ fun fmt () -> Format.fprintf fmt "%s" @@ Clause.short_name c]
+ [ fun fmt () -> Format.fprintf fmt "%s" @@ S.Clause.short_name store c]
- let lemma_info c =
+ let lemma_info store c =
"lemma", Some "BLUE",
- [ fun fmt () -> Format.fprintf fmt "%s" @@ Clause.short_name c]
+ [ fun fmt () -> Format.fprintf fmt "%s" @@ S.Clause.short_name store c]
- let assumption_info c =
+ let assumption_info store c =
"assumption", Some "PURPLE",
- [ fun fmt () -> Format.fprintf fmt "%s" @@ Clause.short_name c]
+ [ fun fmt () -> Format.fprintf fmt "%s" @@ S.Clause.short_name store c]
end
@@ -52,24 +54,25 @@ end
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 store := S.store
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 node_id store n = S.Clause.short_name store n.P.conclusion
+ let proof_id store p = node_id store (P.expand store p)
+ let res_nn_id store n1 n2 = node_id store n1 ^ "_" ^ node_id store n2 ^ "_res"
+ let res_np_id store n1 n2 = node_id store n1 ^ "_" ^ proof_id store n2 ^ "_res"
- let print_clause fmt c =
- let v = Clause.atoms c in
+ let print_clause store fmt c =
+ let v = S.Clause.atoms_a store 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);
+ Format.fprintf fmt "%a" (A.print_atom store) v.(i);
if i < n - 1 then
Format.fprintf fmt ", "
done
@@ -77,21 +80,21 @@ module Make(S : Sidekick_sat.S)(A : Arg with type atom := S.atom
let print_edge fmt i j =
Format.fprintf fmt "%s -> %s;@\n" j i
- let print_edges fmt n =
+ let print_edges store 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);
+ print_edge fmt (res_np_id store n p0) (proof_id store hr_init);
List.iter
- (fun (_,p2) -> print_edge fmt (res_np_id n p2) (proof_id p2))
+ (fun (_,p2) -> print_edge fmt (res_np_id store n p2) (proof_id store 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;
+ let table store fmt (c, rule, color, l) =
+ Format.fprintf fmt "| %a |
" (print_clause store) c;
match l with
| [] ->
Format.fprintf fmt "| %s |
" color rule
@@ -100,92 +103,54 @@ module Make(S : Sidekick_sat.S)(A : Arg with type atom := S.atom
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 =
+ let print_dot_node store fmt id color c rule rule_color l =
Format.fprintf fmt "%s [shape=plaintext, label=<>];@\n"
- id table_options color table (c, rule, rule_color, l)
+ id table_options color (table store) (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 print_dot_res_node store fmt id a =
+ Format.fprintf fmt "%s [label=<%a>];@\n" id (A.print_atom store) a
let ttify f c = fun fmt () -> f fmt c
- let print_contents fmt n =
+ let print_contents store 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 rule, color, l = A.hyp_info store 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
+ print_dot_node store fmt (node_id store n) "LIGHTBLUE" P.(n.conclusion) rule color l
| P.Assumption ->
- let rule, color, l = A.assumption_info P.(n.conclusion) in
+ let rule, color, l = A.assumption_info store 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
+ print_dot_node store fmt (node_id store n) "LIGHTBLUE" P.(n.conclusion) rule color l
| P.Lemma _ ->
- let rule, color, l = A.lemma_info P.(n.conclusion) in
+ let rule, color, l = A.lemma_info store 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
+ print_dot_node store fmt (node_id store 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))
+ print_dot_node store fmt (node_id store n) "GREY" P.(n.conclusion) "Duplicate" "GREY"
+ ((fun fmt () -> (Format.fprintf fmt "%s" (node_id store n))) ::
+ List.map (ttify @@ A.print_atom store) l);
+ print_edge fmt (node_id store n) (node_id store (P.expand store 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)))];
+ print_dot_node store fmt (node_id store n) "GREY" P.(n.conclusion) "Resolution" "GREY"
+ [(fun fmt () -> (Format.fprintf fmt "%s" (node_id store 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))
+ print_dot_res_node store fmt (res_np_id store n p2) a;
+ print_edge fmt (node_id store n) (res_np_id store n p2))
l
- let print_node fmt n =
- print_contents fmt n;
- print_edges fmt n
+ let print_node store fmt n =
+ print_contents store fmt n;
+ print_edges store fmt n
- let pp fmt p =
+ let pp store fmt p =
Format.fprintf fmt "digraph proof {@\n";
- P.fold (fun () -> print_node fmt) () p;
+ P.fold store (fun () -> print_node store 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
index eecdebaf..11bd9a7d 100644
--- a/src/backend/Dot.mli
+++ b/src/backend/Dot.mli
@@ -28,14 +28,16 @@ module type Arg = sig
type assumption
(** The type of theory-specifi proofs (also called lemmas). *)
- val print_atom : Format.formatter -> atom -> unit
+ type store
+
+ val print_atom : store -> 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
+ val hyp_info : store -> hyp -> string * string option * (Format.formatter -> unit -> unit) list
+ val lemma_info : store -> lemma -> string * string option * (Format.formatter -> unit -> unit) list
+ val assumption_info : store -> 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:
@@ -50,21 +52,16 @@ 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 store := S.store
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
+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 store := S.store
+ and type assumption := S.clause)
+ : S with type t := S.Proof.t and type store := S.store
(** 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
index 316c6d7a..93b0e234 100644
--- a/src/backend/dune
+++ b/src/backend/dune
@@ -2,5 +2,6 @@
(name sidekick_backend)
(public_name sidekick.backend)
(synopsis "Proof backends for sidekick")
+ (flags :standard -warn-error -a+8)
(libraries sidekick.sat))
diff --git a/src/core/Sidekick_core.ml b/src/core/Sidekick_core.ml
index e4642fb4..3316679d 100644
--- a/src/core/Sidekick_core.ml
+++ b/src/core/Sidekick_core.ml
@@ -948,6 +948,7 @@ module type SOLVER = sig
theory
(** Helper to create a theory. *)
+ (* TODO: remove? hide? *)
(** {3 Boolean Atoms}
Atoms are the SAT solver's version of our boolean literals
diff --git a/src/msat-solver/Sidekick_msat_solver.ml b/src/msat-solver/Sidekick_msat_solver.ml
index 03963f12..b7f51080 100644
--- a/src/msat-solver/Sidekick_msat_solver.ml
+++ b/src/msat-solver/Sidekick_msat_solver.ml
@@ -516,13 +516,12 @@ module Make(A : ARG)
(** the parametrized SAT Solver *)
module Sat_solver = Sidekick_sat.Make_cdcl_t(Solver_internal)
- module Atom = Sat_solver.Atom
-
module Pre_proof = struct
module SP = Sat_solver.Proof
module SC = Sat_solver.Clause
type t = {
+ solver: Sat_solver.t;
msat: Sat_solver.Proof.t;
tdefs: (term*term) list; (* term definitions *)
p: P.t lazy_t;
@@ -533,7 +532,7 @@ module Make(A : ARG)
let pp_dot =
let module Dot =
Sidekick_backend.Dot.Make(Sat_solver)(Sidekick_backend.Dot.Default(Sat_solver)) in
- let pp out self = Dot.pp out self.msat in
+ let pp out self = Dot.pp (Sat_solver.store self.solver) out self.msat in
Some pp
(* export to proof {!P.t}, translating Msat-level proof ising:
@@ -545,7 +544,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) (t_defs:_ list) : P.t =
+ let conv_proof (store:Sat_solver.store) (msat:Sat_solver.Proof.t) (t_defs:_ list) : P.t =
let assms = ref [] in
let steps = ref [] in
@@ -558,7 +557,7 @@ module Make(A : ARG)
with Not_found ->
Error.errorf
"msat-solver.pre-proof.to_proof: cannot find proof step with conclusion %a"
- SC.pp (SP.conclusion p)
+ (SC.pp store) (SP.conclusion p)
in
let add_step s = steps := s :: !steps in
@@ -577,10 +576,10 @@ module Make(A : ARG)
(* build conclusion of proof step *)
let tr_atom a : P.lit =
let sign = Sat_solver.Atom.sign a in
- let t = Lit.term (Sat_solver.Atom.formula a) in
+ let t = Lit.term (Sat_solver.Atom.formula store a) in
P.lit_mk sign t
in
- let concl = List.rev_map tr_atom @@ Sat_solver.Clause.atoms_l c in
+ let concl = List.rev_map tr_atom @@ Sat_solver.Clause.atoms_l store c in
(* proof for the node *)
let pr_step : P.t =
@@ -592,7 +591,7 @@ module Make(A : ARG)
let name = Printf.sprintf "a%d" !n_step in
let lit = match concl with
| [l] -> l
- | _ -> Error.errorf "assumption with non-unit clause %a" SC.pp c
+ | _ -> Error.errorf "assumption with non-unit clause %a" (SC.pp store) c
in
incr n_step;
assms := (name, lit) :: !assms;
@@ -611,12 +610,12 @@ module Make(A : ARG)
let proof_init = P.ref_by_name @@ find_proof_name init in
let tr_step (pivot,p') : P.hres_step =
(* unit resolution? *)
- let is_r1_step = Array.length (SC.atoms (SP.conclusion p')) = 1 in
+ let is_r1_step = Iter.length (SC.atoms store (SP.conclusion p')) = 1 in
let proof_p' = P.ref_by_name @@ find_proof_name p' in
if is_r1_step then (
P.r1 proof_p'
) else (
- let pivot = Lit.term (Sat_solver.Atom.formula pivot) in
+ let pivot = Lit.term (Sat_solver.Atom.formula store pivot) in
P.r proof_p' ~pivot
)
in
@@ -630,17 +629,17 @@ module Make(A : ARG)
in
(* this should traverse from the leaves, so that order of [steps] is correct *)
- Sat_solver.Proof.fold tr_node_to_step () msat;
+ Sat_solver.Proof.fold store tr_node_to_step () msat;
let assms = !assms in
(* gather all term definitions *)
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.t) (tdefs: _ list) : t =
- { msat; tdefs; p=lazy (conv_proof msat tdefs) }
+ let make solver (msat: Sat_solver.Proof.t) (tdefs: _ list) : t =
+ { solver; msat; tdefs; p=lazy (conv_proof (Sat_solver.store solver) msat tdefs) }
- let check self = SP.check self.msat
+ let check self = SP.check (Sat_solver.store self.solver) self.msat
let pp_debug out self = P.pp_debug ~sharing:false out (to_proof self)
let output oc (self:t) = P.Quip.output oc (to_proof self)
end
@@ -656,6 +655,12 @@ module Make(A : ARG)
}
type solver = t
+ module Atom = struct
+ include Sat_solver.Atom
+ let pp self out a = pp (Sat_solver.store self.solver) out a
+ let formula self a = formula (Sat_solver.store self.solver) a
+ end
+
module type THEORY = sig
type t
val name : string
@@ -741,7 +746,8 @@ module Make(A : ARG)
let atom = mk_atom_t_ self sub in
(* also map [sub] to this atom in the congruence closure, for propagation *)
let cc = cc self in
- CC.set_as_lit cc (CC.add_term cc sub ) (Sat_solver.Atom.formula atom);
+ let store = Sat_solver.store self.solver in
+ CC.set_as_lit cc (CC.add_term cc sub ) (Sat_solver.Atom.formula store atom);
())
let rec mk_atom_lit self lit : Atom.t * P.t =
@@ -833,8 +839,10 @@ module Make(A : ARG)
let add_clause (self:t) (c:Atom.t IArray.t) (proof:P.t) : unit =
Stat.incr self.count_clause;
- Log.debugf 50 (fun k->k "(@[solver.add-clause@ %a@ :proof %a@])"
- (Util.pp_iarray Atom.pp) c (P.pp_debug ~sharing:false) proof);
+ Log.debugf 50 (fun k->
+ let store = Sat_solver.store self.solver in
+ k "(@[solver.add-clause@ %a@ :proof %a@])"
+ (Util.pp_iarray (Sat_solver.Atom.pp store)) c (P.pp_debug ~sharing:false) proof);
let pb = Profile.begin_ "add-clause" in
Sat_solver.add_clause_a self.solver (c:> Atom.t array) proof;
Profile.exit pb
@@ -927,8 +935,9 @@ module Make(A : ARG)
let proof = lazy (
try
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))
+ let store = Sat_solver.store self.solver in
+ if check then Sat_solver.Proof.check store pr;
+ Some (Pre_proof.make self.solver pr (List.rev self.si.t_defs))
with Sidekick_sat.Solver_intf.No_proof -> None
) in
let unsat_core = lazy (UNSAT.unsat_assumptions ()) in
diff --git a/src/sat/Solver.ml b/src/sat/Solver.ml
index 6d8c22a3..6741fce0 100644
--- a/src/sat/Solver.ml
+++ b/src/sat/Solver.ml
@@ -42,11 +42,11 @@ module Make(Plugin : PLUGIN)
(* ### types ### *)
(* a boolean variable (positive int) *)
- module Var : INT_ID = Mk_int_id()
- type var = Var.t
+ module Var0 : INT_ID = Mk_int_id()
+ type var = Var0.t
(* a signed atom. +v is (v << 1), -v is (v<<1 | 1) *)
- module Atom : sig
+ module Atom0 : sig
include INT_ID
val neg : t -> t
val sign : t -> bool
@@ -65,11 +65,11 @@ module Make(Plugin : PLUGIN)
let[@inline] pa v = (v:var:>int) lsl 1
let of_var = pa
let[@inline] abs a = a land (lnot 1)
- let[@inline] var a = Var.of_int_unsafe (a lsr 1)
+ let[@inline] var a = Var0.of_int_unsafe (a lsr 1)
let[@inline] na v = (((v:var:>int) lsl 1) lor 1)
module Set = Util.Int_set
end
- type atom = Atom.t
+ type atom = Atom0.t
(* TODO: special clause allocator *)
type clause = {
@@ -151,9 +151,10 @@ module Make(Plugin : PLUGIN)
(** iterate on variables *)
let iter_vars self f =
- Vec.iteri (fun i _ -> f (Var.of_int_unsafe i)) self.v_level
+ Vec.iteri (fun i _ -> f (Var0.of_int_unsafe i)) self.v_level
- module Vars = struct
+ module Var = struct
+ include Var0
let[@inline] level self v = Vec.get self.v_level (v:var:>int)
let[@inline] set_level self v l = Vec.set self.v_level (v:var:>int) l
let[@inline] reason self v = Vec.get self.v_reason (v:var:>int)
@@ -169,8 +170,10 @@ module Make(Plugin : PLUGIN)
let[@inline] set_heap_idx self v i = Vec.set self.v_heap_idx (v:var:>int) i
end
- module Atoms = struct
+ module Atom = struct
+ include Atom0
let[@inline] lit self a = Vec.get self.a_form (a:atom:>int)
+ let formula = lit
let[@inline] mark self a = Bitvec.set self.a_seen (a:atom:>int) true
let[@inline] unmark self a = Bitvec.set self.a_seen (a:atom:>int) false
let[@inline] seen self a = Bitvec.get self.a_seen (a:atom:>int)
@@ -178,12 +181,12 @@ module Make(Plugin : PLUGIN)
let[@inline] is_true self a = Bitvec.get self.a_is_true (a:atom:>int)
let[@inline] set_is_true self a b = Bitvec.set self.a_is_true (a:atom:>int) b
- let[@inline] is_false self a = is_true self (Atom.neg a)
+ let[@inline] is_false self a = is_true self (neg a)
let[@inline] has_value self a = is_true self a || is_false self a
- let[@inline] reason self a = Vars.reason self (Atom.var a)
- let[@inline] level self a = Vars.level self (Atom.var a)
- let[@inline] seen_both self a = seen self a && seen self (Atom.neg a)
+ let[@inline] reason self a = Var.reason self (var a)
+ let[@inline] level self a = Var.level self (var a)
+ let[@inline] seen_both self a = seen self a && seen self (neg a)
(*
let[@inline] var a = a.var
@@ -194,7 +197,7 @@ module Make(Plugin : PLUGIN)
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] reason a = V.reason a.var
let[@inline] id a = a.aid
*)
@@ -214,7 +217,7 @@ module Make(Plugin : PLUGIN)
(* Complete debug printing *)
- let[@inline] pp_sign a = if Atom.sign a then "+" else "-"
+ let[@inline] pp_sign a = if sign a then "+" else "-"
(* print level+reason of assignment *)
let debug_reason out = function
@@ -226,8 +229,8 @@ module Make(Plugin : PLUGIN)
| n, Some (Bcp_lazy _) -> Format.fprintf out "->%d/" n
let pp_level self out a =
- let v = Atom.var a in
- debug_reason out (Vars.level self v, Vars.reason self v)
+ let v = var a in
+ debug_reason out (Var.level self v, Var.reason self v)
let debug_value self out (a:atom) =
if is_true self a then Format.fprintf out "T%a" (pp_level self) a
@@ -236,7 +239,7 @@ module Make(Plugin : PLUGIN)
let debug self out a =
Format.fprintf out "%s%d[%a][atom:@[%a@]]"
- (pp_sign a) (Atom.var a:var:>int) (debug_value self) a
+ (pp_sign a) (var a:var:>int) (debug_value self) a
Formula.pp (lit self a)
let debug_a self out vec =
@@ -285,9 +288,9 @@ module Make(Plugin : PLUGIN)
v, negated
let clear_var (self:t) (v:var) : unit =
- Vars.unmark self v;
- Atoms.unmark self (Atom.pa v);
- Atoms.unmark self (Atom.na v);
+ Var.unmark self v;
+ Atom.unmark self (Atom.pa v);
+ Atom.unmark self (Atom.na v);
()
let alloc_atom (self:t) ?default_pol lit : atom =
@@ -302,7 +305,7 @@ module Make(Plugin : PLUGIN)
let has_value a = is_true a || is_false a
let[@inline] make ?default_pol st lit =
- let var, negated = Var.make ?default_pol st lit in
+ let var, negated = V.make ?default_pol st lit in
match negated with
| Solver_intf.Negated -> var.na
| Solver_intf.Same_sign -> var.pa
@@ -323,7 +326,9 @@ module Make(Plugin : PLUGIN)
*)
end
type store = Store.t
- open Store
+
+ module Atom = Store.Atom
+ module Var = Store.Var
(* FIXME
@@ -361,9 +366,9 @@ module Make(Plugin : PLUGIN)
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[@inline] atoms _ c = Iter.of_array c.atoms
+ let[@inline] atoms_a _ c = c.atoms
+ let[@inline] atoms_l _ c = Array.to_list c.atoms
let flag_attached = 0b1
let flag_visited = 0b10
@@ -401,10 +406,10 @@ module Make(Plugin : PLUGIN)
let equal = equal
end)
- let short_name c = Printf.sprintf "%s%d" (kind_of_clause c) c.cid
+ let short_name _store c = Printf.sprintf "%s%d" (kind_of_clause c) c.cid
let pp self fmt c =
Format.fprintf fmt "(cl[%s%d] : %a" (kind_of_clause c) c.cid
- (Store.Atoms.pp_a self) c.atoms
+ (Store.Atom.pp_a self) c.atoms
let debug_premise out = function
| Hyp _ -> Format.fprintf out "hyp"
@@ -419,7 +424,7 @@ module Make(Plugin : PLUGIN)
let debug self out ({atoms=arr; cpremise=cp;_}as c) =
Format.fprintf out
"(@[cl[%s%d]@ {@[%a@]}@ :premise %a@])"
- (kind_of_clause c) c.cid (Store.Atoms.debug_a self) arr debug_premise cp
+ (kind_of_clause c) c.cid (Store.Atom.debug_a self) arr debug_premise cp
end
module Proof = struct
@@ -429,23 +434,24 @@ module Make(Plugin : PLUGIN)
type clause = Clause.t
type formula = Formula.t
type lemma = Plugin.proof
+ type nonrec store = store
let error_res_f msg = Format.kasprintf (fun s -> raise (Resolution_error s)) msg
- let[@inline] clear_var_of_ store (a:atom) = clear_var store (Atom.var a)
+ let[@inline] clear_var_of_ store (a:atom) = Store.clear_var store (Atom.var a)
(* Compute resolution of 2 clauses.
returns [pivots, resulting_atoms] *)
let resolve self (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 (Atoms.mark self) c2.atoms;
+ Array.iter (Atom.mark self) c2.atoms;
let pivots = ref [] in
let l =
Array.fold_left
(fun l a ->
- if Atoms.seen self a then l
- else if Atoms.seen self (Atom.neg a) then (
+ if Atom.seen self a then l
+ else if Atom.seen self (Atom.neg a) then (
pivots := (Atom.abs a) :: !pivots;
clear_var_of_ self a;
l
@@ -453,7 +459,7 @@ module Make(Plugin : PLUGIN)
[] c1.atoms
in
let l =
- Array.fold_left (fun l a -> if Atoms.seen self a then a::l else l) l c2.atoms
+ Array.fold_left (fun l a -> if Atom.seen self a then a::l else l) l c2.atoms
in
Array.iter (clear_var_of_ self) c2.atoms;
!pivots, l
@@ -463,10 +469,10 @@ module Make(Plugin : PLUGIN)
let res =
Array.fold_left
(fun (dups,l) a ->
- if Atoms.seen self a then (
+ if Atom.seen self a then (
a::dups, l
) else (
- Atoms.mark self a;
+ Atom.mark self a;
dups, a::l
))
([], []) c.atoms
@@ -477,14 +483,14 @@ module Make(Plugin : PLUGIN)
(* do [c1] and [c2] have the same lits, modulo reordering and duplicates? *)
let same_lits self (c1:atom Iter.t) (c2:atom Iter.t): bool =
let subset a b =
- Iter.iter (Atoms.mark self) b;
- let res = Iter.for_all (Atoms.seen self) a in
+ Iter.iter (Atom.mark self) b;
+ let res = Iter.for_all (Atom.seen self) a in
Iter.iter (clear_var_of_ self) b;
res
in
subset c1 c2 && subset c2 c1
- let prove conclusion =
+ let prove _sol conclusion =
match conclusion.cpremise with
| History [] -> assert false
| Empty_premise -> raise Solver_intf.No_proof
@@ -495,27 +501,27 @@ module Make(Plugin : PLUGIN)
if Atom.equal (Atom.neg a) b then acc
else set_atom_proof self b :: acc
in
- assert (Vars.level self (Atom.var a) >= 0);
- match Vars.reason self (Atom.var a) with
+ assert (Var.level self (Atom.var a) >= 0);
+ match Var.reason self (Atom.var a) with
| Some (Bcp c | Bcp_lazy (lazy c)) ->
Log.debugf 5 (fun k->k "(@[proof.analyze.clause@ :atom %a@ :c %a@])"
- (Atoms.debug self) a (Clause.debug self) c);
+ (Atom.debug self) a (Clause.debug self) c);
if Array.length c.atoms = 1 then (
Log.debugf 5 (fun k -> k "(@[proof.analyze.old-reason@ %a@])"
- (Atoms.debug self) a);
+ (Atom.debug self) a);
c
) else (
- assert (Atoms.is_false self a);
+ assert (Atom.is_false self a);
let r = History (c :: (Array.fold_left aux [] c.atoms)) in
let c' = Clause.make_permanent [Atom.neg a] r in
- Vars.set_reason self (Atom.var a) (Some (Bcp c'));
+ Var.set_reason self (Atom.var a) (Some (Bcp c'));
Log.debugf 5
(fun k -> k "(@[proof.analyze.new-reason@ :atom %a@ :c %a@])"
- (Atoms.debug self) a (Clause.debug self) c');
+ (Atom.debug self) a (Clause.debug self) c');
c'
)
| _ ->
- error_res_f "cannot prove atom %a" (Atoms.debug self) a
+ error_res_f "cannot prove atom %a" (Atom.debug self) a
let prove_unsat self conflict =
if Array.length conflict.atoms = 0 then (
@@ -529,8 +535,8 @@ module Make(Plugin : PLUGIN)
)
let prove_atom self a =
- if Atoms.is_true self a &&
- Vars.level self (Atom.var a) = 0 then
+ if Atom.is_true self a &&
+ Var.level self (Atom.var a) = 0 then
Some (set_atom_proof self a)
else
None
@@ -560,14 +566,14 @@ module Make(Plugin : PLUGIN)
Log.debugf 15
(fun k->k "(@[proof.find-pivots@ :init %a@ :l %a@])"
(Clause.debug self) init (Format.pp_print_list (Clause.debug self)) l);
- Array.iter (Atoms.mark self) init.atoms;
+ Array.iter (Atom.mark self) init.atoms;
let steps =
List.map
(fun c ->
let pivot =
match
Iter.of_array c.atoms
- |> Iter.filter (fun a -> Atoms.seen self (Atom.neg a))
+ |> Iter.filter (fun a -> Atom.seen self (Atom.neg a))
|> Iter.to_list
with
| [a] -> a
@@ -575,9 +581,9 @@ module Make(Plugin : PLUGIN)
error_res_f "(@[proof.expand.pivot_missing@ %a@])" (Clause.debug self) c
| pivots ->
error_res_f "(@[proof.expand.multiple_pivots@ %a@ :pivots %a@])"
- (Clause.debug self) c (Atoms.debug_l self) pivots
+ (Clause.debug self) c (Atom.debug_l self) pivots
in
- Array.iter (Atoms.mark self) c.atoms; (* add atoms to result *)
+ Array.iter (Atom.mark self) c.atoms; (* add atoms to result *)
clear_var_of_ self pivot;
Atom.abs pivot, c)
l
@@ -585,7 +591,7 @@ module Make(Plugin : PLUGIN)
(* cleanup *)
let res = ref [] in
let cleanup_a_ a =
- if Atoms.seen self a then (
+ if Atom.seen self a then (
res := a :: !res;
clear_var_of_ self a
)
@@ -594,8 +600,8 @@ module Make(Plugin : PLUGIN)
List.iter (fun c -> Array.iter cleanup_a_ c.atoms) l;
!res, steps
- let expand self conclusion =
- Log.debugf 5 (fun k -> k "(@[sat.proof.expand@ @[%a@]@])" (Clause.debug self) conclusion);
+ let expand store conclusion =
+ Log.debugf 5 (fun k -> k "(@[sat.proof.expand@ @[%a@]@])" (Clause.debug store) conclusion);
match conclusion.cpremise with
| Lemma l ->
{ conclusion; step = Lemma l; }
@@ -604,14 +610,14 @@ module Make(Plugin : PLUGIN)
| Hyp l ->
{ conclusion; step = Hypothesis l; }
| History [] ->
- error_res_f "@[empty history for clause@ %a@]" (Clause.debug self) conclusion
+ error_res_f "@[empty history for clause@ %a@]" (Clause.debug store) conclusion
| History [c] ->
- let duplicates, res = find_dups self c in
- assert (same_lits self (Iter.of_list res) (Clause.atoms_seq conclusion));
+ let duplicates, res = find_dups store c in
+ assert (same_lits store (Iter.of_list res) (Clause.atoms store conclusion));
{ conclusion; step = Duplicate (c, duplicates) }
| History (c :: r) ->
- let res, steps = find_pivots self c r in
- assert (same_lits self (Iter.of_list res) (Clause.atoms_seq conclusion));
+ let res, steps = find_pivots store c r in
+ assert (same_lits store (Iter.of_list res) (Clause.atoms store conclusion));
{ conclusion; step = Hyper_res {hr_init=c; hr_steps=steps}; }
| Empty_premise -> raise Solver_intf.No_proof
@@ -721,9 +727,9 @@ module Make(Plugin : PLUGIN)
type t = var
open Store
let[@inline] cmp store i j =
- Vars.weight store j < Vars.weight store i (* comparison by weight *)
- let heap_idx = Vars.heap_idx
- let set_heap_idx = Vars.set_heap_idx
+ Var.weight store j < Var.weight store i (* comparison by weight *)
+ let heap_idx = Var.heap_idx
+ let set_heap_idx = Var.set_heap_idx
end)
(* cause of "unsat", possibly conditional to local assumptions *)
@@ -892,11 +898,11 @@ module Make(Plugin : PLUGIN)
(* create a new atom, pushing it into the decision queue if needed *)
let make_atom (self:t) ?default_pol (p:formula) : atom =
let a = Store.alloc_atom self.store ?default_pol p in
- if Atoms.level self.store a < 0 then (
+ if Atom.level self.store a < 0 then (
insert_var_order self (Atom.var a);
(match self.on_new_atom with Some f -> f a | None -> ());
) else (
- assert (Atoms.is_true self.store a || Atoms.is_false self.store a);
+ assert (Atom.is_true self.store a || Atom.is_false self.store a);
);
a
@@ -912,11 +918,11 @@ module Make(Plugin : PLUGIN)
(* increase activity of [v] *)
let var_bump_activity self v =
let store = self.store in
- Vars.set_weight store v (Vars.weight store v +. self.var_incr);
- if Vars.weight store v > 1e100 then (
+ Var.set_weight store v (Var.weight store v +. self.var_incr);
+ if Var.weight store v > 1e100 then (
Store.iter_vars store
(fun v ->
- Vars.set_weight store v (Vars.weight store v *. 1e-100));
+ Var.set_weight store v (Var.weight store v *. 1e-100));
self.var_incr <- self.var_incr *. 1e-100;
);
if H.in_heap self.order v then (
@@ -955,15 +961,15 @@ module Make(Plugin : PLUGIN)
let duplicates = ref [] in
let res = ref [] in
Array.iter (fun a ->
- if Atoms.seen store a then duplicates := a :: !duplicates
+ if Atom.seen store a then duplicates := a :: !duplicates
else (
- Atoms.mark store a;
+ Atom.mark store a;
res := a :: !res
))
clause.atoms;
List.iter
(fun a ->
- if Atoms.seen_both store a then trivial := true;
+ if Atom.seen_both store a then trivial := true;
Store.clear_var store (Atom.var a))
!res;
if !trivial then (
@@ -987,20 +993,20 @@ module Make(Plugin : PLUGIN)
trues @ unassigned @ falses, history
) else (
let a = atoms.(i) in
- if Atoms.is_true store a then (
- let l = Atoms.level store a in
+ if Atom.is_true store a then (
+ let l = Atom.level store a in
if l = 0 then
- raise_notrace Trivial (* A var true at level 0 gives a trivially true clause *)
+ raise_notrace Trivial (* Atom var true at level 0 gives a trivially true clause *)
else
(a :: trues) @ unassigned @ falses @
(arr_to_list atoms (i + 1)), history
- ) else if Atoms.is_false store a then (
- let l = Atoms.level store a in
+ ) else if Atom.is_false store a then (
+ let l = Atom.level store a in
if l = 0 then (
- match Atoms.reason store a with
+ match Atom.reason store a 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,
+ (* Atom 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
@@ -1033,7 +1039,7 @@ module Make(Plugin : PLUGIN)
(* Attach/Detach a clause.
- A clause is attached (to its watching lits) when it is first added,
+ Atom clause is attached (to its watching lits) when it is first added,
either because it is assumed or learnt.
*)
@@ -1041,8 +1047,8 @@ module Make(Plugin : PLUGIN)
let store = self.store in
assert (not @@ Clause.attached c);
Log.debugf 20 (fun k -> k "(@[sat.attach-clause@ %a@])" (Clause.debug store) c);
- Vec.push (Atoms.watched store (Atom.neg c.atoms.(0))) c;
- Vec.push (Atoms.watched store (Atom.neg c.atoms.(1))) c;
+ Vec.push (Atom.watched store (Atom.neg c.atoms.(0))) c;
+ Vec.push (Atom.watched store (Atom.neg c.atoms.(1))) c;
Clause.set_attached c true;
()
@@ -1066,11 +1072,11 @@ module Make(Plugin : PLUGIN)
(i.e to the right of elt_head in the queue. *)
for c = self.elt_head to Vec.size self.trail - 1 do
let a = Vec.get self.trail c in
- (* A literal is unassigned, we nedd to add it back to
+ (* Atom 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 Atoms.level store a <= lvl then (
+ (* Atom variable is not true/false anymore, one of two things can happen: *)
+ if Atom.level store a <= 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. *)
@@ -1080,10 +1086,10 @@ module Make(Plugin : PLUGIN)
(* 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. *)
- Atoms.set_is_true store a false;
- Atoms.set_is_true store (Atom.neg a) false;
- Vars.set_level store (Atom.var a) (-1);
- Vars.set_reason store (Atom.var a) None;
+ Atom.set_is_true store a false;
+ Atom.set_is_true store (Atom.neg a) false;
+ Var.set_level store (Atom.var a) (-1);
+ Var.set_reason store (Atom.var a) None;
insert_var_order self (Atom.var a)
)
done;
@@ -1101,7 +1107,7 @@ module Make(Plugin : PLUGIN)
let pp_unsat_cause self out = function
| US_local {first=_; core} ->
Format.fprintf out "(@[unsat-cause@ :false-assumptions %a@])"
- (Format.pp_print_list (Atoms.pp self.store)) core
+ (Format.pp_print_list (Atom.pp self.store)) core
| US_false c ->
Format.fprintf out "(@[unsat-cause@ :false %a@])" (Clause.debug self.store) c
@@ -1149,7 +1155,7 @@ module Make(Plugin : PLUGIN)
Log.debugf 0
(fun k ->
k "(@[sat.simplify-reason.failed@ :at %a@ %a@]"
- (Vec.pp ~sep:"" (Atoms.debug self.store)) (Vec.of_list l)
+ (Vec.pp ~sep:"" (Atom.debug self.store)) (Vec.of_list l)
(Clause.debug self.store) cl);
assert false
end
@@ -1159,25 +1165,25 @@ module Make(Plugin : PLUGIN)
Wrapper function for adding a new propagated formula. *)
let enqueue_bool (self:t) a ~level:lvl reason : unit =
let store = self.store in
- if Atoms.is_false store a then (
+ if Atom.is_false store a then (
Log.debugf 0
- (fun k->k "(@[sat.error.trying to enqueue a false literal %a@])" (Atoms.debug store) a);
+ (fun k->k "(@[sat.error.trying to enqueue a false literal %a@])" (Atom.debug store) a);
assert false
);
- assert (not (Atoms.is_true store a) &&
- Atoms.level store a < 0 &&
- Atoms.reason store a == None && lvl >= 0);
+ assert (not (Atom.is_true store a) &&
+ Atom.level store a < 0 &&
+ Atom.reason store a == None && lvl >= 0);
let reason =
if lvl > 0 then reason
else simpl_reason self reason
in
- Atoms.set_is_true store a true;
- Vars.set_level store (Atom.var a) lvl;
- Vars.set_reason store (Atom.var a) (Some reason);
+ Atom.set_is_true store a true;
+ Var.set_level store (Atom.var a) lvl;
+ Var.set_reason store (Atom.var a) (Some reason);
Vec.push self.trail a;
Log.debugf 20
(fun k->k "(@[sat.enqueue[%d]@ %a@])"
- (Vec.size self.trail) (Atoms.debug store) a);
+ (Vec.size self.trail) (Atom.debug store) a);
()
(* swap elements of array *)
@@ -1192,7 +1198,7 @@ module Make(Plugin : PLUGIN)
let put_high_level_atoms_first (store:store) (arr:atom array) : unit =
Array.iteri
(fun i a ->
- if i>0 && Atoms.level store a > Atoms.level store arr.(0) then (
+ if i>0 && Atom.level store a > Atom.level store arr.(0) then (
(* move first to second, [i]-th to first, second to [i] *)
if i=1 then (
swap_arr arr 0 1;
@@ -1202,7 +1208,7 @@ module Make(Plugin : PLUGIN)
arr.(0) <- arr.(i);
arr.(i) <- tmp;
);
- ) else if i>1 && Atoms.level store a > Atoms.level store arr.(1) then (
+ ) else if i>1 && Atom.level store a > Atom.level store arr.(1) then (
swap_arr arr 1 i;
))
arr
@@ -1218,14 +1224,14 @@ module Make(Plugin : PLUGIN)
) else (
let a = arr.(0) in
let b = arr.(1) in
- assert (Atoms.level store a > 0);
- if Atoms.level store a > Atoms.level store b then (
+ assert (Atom.level store a > 0);
+ if Atom.level store a > Atom.level store b then (
(* backtrack below [a], so we can propagate [not a] *)
- Atoms.level store b, true
+ Atom.level store b, true
) else (
- assert (Atoms.level store a = Atoms.level store b);
- assert (Atoms.level store a >= 0);
- max (Atoms.level store a - 1) 0, false
+ assert (Atom.level store a = Atom.level store b);
+ assert (Atom.level store a >= 0);
+ max (Atom.level store a - 1) 0, false
)
)
@@ -1260,7 +1266,7 @@ module Make(Plugin : PLUGIN)
Vec.clear to_unmark;
let conflict_level =
if Plugin.has_theory
- then Array.fold_left (fun acc p -> max acc (Atoms.level store p)) 0 c_clause.atoms
+ then Array.fold_left (fun acc p -> max acc (Atom.level store p)) 0 c_clause.atoms
else decision_level self
in
Log.debugf 30
@@ -1281,25 +1287,25 @@ module Make(Plugin : PLUGIN)
(* visit the current predecessors *)
for j = 0 to Array.length clause.atoms - 1 do
let q = clause.atoms.(j) in
- assert (Atoms.is_true store q ||
- Atoms.is_false store q &&
- Atoms.level store q >= 0); (* unsure? *)
- if Atoms.level store q <= 0 then (
- assert (Atoms.is_false store q);
- match Atoms.reason store q with
+ assert (Atom.is_true store q ||
+ Atom.is_false store q &&
+ Atom.level store q >= 0); (* unsure? *)
+ if Atom.level store q <= 0 then (
+ assert (Atom.is_false store q);
+ match Atom.reason store q with
| Some (Bcp cl | Bcp_lazy (lazy cl)) -> history := cl :: !history
| Some Decision | None -> assert false
);
- if not (Vars.marked store (Atom.var q)) then (
- Vars.mark store (Atom.var q);
+ if not (Var.marked store (Atom.var q)) then (
+ Var.mark store (Atom.var q);
Vec.push to_unmark (Atom.var q);
- if Atoms.level store q > 0 then (
+ if Atom.level store q > 0 then (
var_bump_activity self (Atom.var q);
- if Atoms.level store q >= conflict_level then (
+ if Atom.level store q >= conflict_level then (
incr pathC;
) else (
learnt := q :: !learnt;
- blevel := max !blevel (Atoms.level store q)
+ blevel := max !blevel (Atom.level store q)
)
)
)
@@ -1310,22 +1316,22 @@ module Make(Plugin : PLUGIN)
while
let a = Vec.get self.trail !tr_ind in
Log.debugf 30
- (fun k -> k "(@[sat.analyze-conflict.at-trail-elt@ %a@])" (Atoms.debug store) a);
- (not (Vars.marked store (Atom.var a))) ||
- (Atoms.level store a < conflict_level)
+ (fun k -> k "(@[sat.analyze-conflict.at-trail-elt@ %a@])" (Atom.debug store) a);
+ (not (Var.marked store (Atom.var a))) ||
+ (Atom.level store a < conflict_level)
do
decr tr_ind;
done;
let p = Vec.get self.trail !tr_ind in
decr pathC;
decr tr_ind;
- match !pathC, Atoms.reason store p with
+ match !pathC, Atom.reason store p with
| 0, _ ->
cond := false;
learnt := Atom.neg p :: List.rev !learnt
| n, Some (Bcp cl | Bcp_lazy (lazy cl)) ->
assert (n > 0);
- assert (Atoms.level store p >= conflict_level);
+ assert (Atom.level store p >= conflict_level);
c := Some cl
| _, (None | Some Decision) -> assert false
done;
@@ -1337,7 +1343,7 @@ module Make(Plugin : PLUGIN)
let a = Array.of_list !learnt in
(* TODO: use a preallocate vec for learnt *)
(* TODO: a sort that doesn't allocate as much, on the vec *)
- Array.fast_sort (fun p q -> compare (Atoms.level store q) (Atoms.level store p)) a;
+ Array.fast_sort (fun p q -> compare (Atom.level store q) (Atom.level store p)) a;
(* put_high_level_atoms_first a; *)
let level, is_uip = backtrack_lvl self a in
{ cr_backtrack_lvl = level;
@@ -1354,7 +1360,7 @@ module Make(Plugin : PLUGIN)
| [| |] -> assert false
| [|fuip|] ->
assert (cr.cr_backtrack_lvl = 0 && decision_level self = 0);
- if Atoms.is_false store fuip then (
+ if Atom.is_false store fuip then (
(* incompatible at level 0 *)
report_unsat self (US_false confl)
) else (
@@ -1387,7 +1393,7 @@ module Make(Plugin : PLUGIN)
self.next_decisions <- [];
assert (decision_level self >= 0);
if decision_level self = 0 ||
- Array.for_all (fun a -> Atoms.level store a <= 0) confl.atoms then (
+ Array.for_all (fun a -> Atom.level store a <= 0) confl.atoms then (
(* Top-level conflict *)
report_unsat self (US_false confl);
);
@@ -1433,31 +1439,31 @@ module Make(Plugin : PLUGIN)
report_unsat self @@ US_false clause
| [a] ->
cancel_until self 0;
- if Atoms.is_false store a then (
+ if Atom.is_false store a then (
(* cannot recover from this *)
report_unsat self @@ US_false clause
- ) else if Atoms.is_true store a then (
+ ) else if Atom.is_true store a then (
() (* atom is already true, nothing to do *)
) else (
Log.debugf 40
- (fun k->k "(@[sat.add-clause.unit-clause@ :propagating %a@])" (Atoms.debug store) a);
+ (fun k->k "(@[sat.add-clause.unit-clause@ :propagating %a@])" (Atom.debug store) a);
add_clause_to_vec self clause;
enqueue_bool self a ~level:0 (Bcp clause)
)
| a::b::_ ->
add_clause_to_vec self clause;
- if Atoms.is_false store a then (
- (* Atoms need to be sorted in decreasing order of decision level,
+ if Atom.is_false store a then (
+ (* Atom need to be sorted in decreasing order of decision level,
or we might watch the wrong literals. *)
put_high_level_atoms_first store clause.atoms;
attach_clause self clause;
add_boolean_conflict self clause
) else (
attach_clause self clause;
- if Atoms.is_false store b &&
- not (Atoms.is_true store a) &&
- not (Atoms.is_false store a) then (
- let lvl = List.fold_left (fun m a -> max m (Atoms.level store a)) 0 atoms in
+ if Atom.is_false store b &&
+ not (Atom.is_true store a) &&
+ not (Atom.is_false store a) then (
+ let lvl = List.fold_left (fun m a -> max m (Atom.level store a)) 0 atoms in
cancel_until self lvl;
enqueue_bool self a ~level:lvl (Bcp clause)
)
@@ -1496,25 +1502,25 @@ module Make(Plugin : PLUGIN)
assert (Atom.neg a = atoms.(1))
);
let first = atoms.(0) in
- if Atoms.is_true store first then (
+ if Atom.is_true store first 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 (Atoms.is_false store ak) then (
+ if not (Atom.is_false store ak) then (
(* watch lit found: update and exit *)
atoms.(1) <- ak;
atoms.(k) <- Atom.neg a;
(* remove [c] from [a.watched], add it to [ak.neg.watched] *)
- Vec.push (Atoms.watched store (Atom.neg ak)) c;
- assert (Vec.get (Atoms.watched store a) i == c);
- Vec.fast_remove (Atoms.watched store a) i;
+ Vec.push (Atom.watched store (Atom.neg ak)) c;
+ assert (Vec.get (Atom.watched store a) i == c);
+ Vec.fast_remove (Atom.watched store a) i;
raise_notrace Exit
)
done;
(* no watch lit found *)
- if Atoms.is_false store first then (
+ if Atom.is_false store first then (
(* clause is false *)
self.elt_head <- Vec.size self.trail;
raise_notrace (Conflict c)
@@ -1532,7 +1538,7 @@ module Make(Plugin : PLUGIN)
@param res the optional conflict clause that the propagation might trigger *)
let propagate_atom (self:t) a : unit =
let store = self.store in
- let watched = Atoms.watched store a in
+ let watched = Atom.watched store a in
let rec aux i =
if i >= Vec.size watched then ()
else (
@@ -1568,8 +1574,8 @@ module Make(Plugin : PLUGIN)
let store = self.store in
let a = make_atom self f in
let a = if sign then a else Atom.neg a in
- if not (Atoms.has_value store a) then (
- Log.debugf 10 (fun k->k "(@[sat.th.add-decision-lit@ %a@])" (Atoms.debug store) a);
+ if not (Atom.has_value store a) then (
+ Log.debugf 10 (fun k->k "(@[sat.th.add-decision-lit@ %a@])" (Atom.debug store) a);
self.next_decisions <- a :: self.next_decisions
)
@@ -1583,11 +1589,11 @@ module Make(Plugin : PLUGIN)
let check_consequence_lits_false_ self l : unit =
let store = self.store in
- match List.find (Atoms.is_true store) l with
+ match List.find (Atom.is_true store) l with
| a ->
invalid_argf
"slice.acts_propagate:@ Consequence should contain only true literals, but %a isn't"
- (Atoms.debug store) (Atom.neg a)
+ (Atom.debug store) (Atom.neg a)
| exception Not_found -> ()
let acts_propagate (self:t) f expl =
@@ -1595,8 +1601,8 @@ module Make(Plugin : PLUGIN)
match expl with
| Solver_intf.Consequence mk_expl ->
let p = make_atom self f in
- if Atoms.is_true store p then ()
- else if Atoms.is_false store p then (
+ if Atom.is_true store p then ()
+ else if Atom.is_false store p then (
let lits, proof = mk_expl() in
let l = List.rev_map (fun f -> Atom.neg @@ make_atom self f) lits in
check_consequence_lits_false_ self l;
@@ -1623,12 +1629,12 @@ module Make(Plugin : PLUGIN)
let[@specialise] acts_iter self ~full head f : unit =
for i = (if full then 0 else head) to Vec.size self.trail-1 do
let a = Vec.get self.trail i in
- f (Atoms.lit self.store a);
+ f (Atom.lit self.store a);
done
let eval_atom_ self a =
- if Atoms.is_true self.store a then Solver_intf.L_true
- else if Atoms.is_false self.store a then Solver_intf.L_false
+ if Atom.is_true self.store a then Solver_intf.L_true
+ else if Atom.is_false self.store a then Solver_intf.L_false
else Solver_intf.L_undefined
let[@inline] acts_eval_lit self (f:formula) : Solver_intf.lbool =
@@ -1669,7 +1675,7 @@ module Make(Plugin : PLUGIN)
(* Assert that the conflict is indeeed a conflict *)
let check_is_conflict_ self (c:Clause.t) : unit =
- if not @@ Array.for_all (Atoms.is_false self.store) c.atoms then (
+ if not @@ Array.for_all (Atom.is_false self.store) c.atoms then (
invalid_argf "conflict should be false: %a" (Clause.debug self.store) c
)
@@ -1718,33 +1724,33 @@ module Make(Plugin : PLUGIN)
(* compute unsat core from assumption [a] *)
let analyze_final (self:t) (a:atom) : atom list =
let store = self.store in
- Log.debugf 5 (fun k->k "(@[sat.analyze-final@ :lit %a@])" (Atoms.debug store) a);
- assert (Atoms.is_false store a);
+ Log.debugf 5 (fun k->k "(@[sat.analyze-final@ :lit %a@])" (Atom.debug store) a);
+ assert (Atom.is_false store a);
let core = ref [a] in
let idx = ref (Vec.size self.trail - 1) in
- Vars.mark store (Atom.var a);
+ Var.mark store (Atom.var a);
let seen = ref [Atom.var a] in
while !idx >= 0 do
let a' = Vec.get self.trail !idx in
- if Vars.marked store (Atom.var a') then (
- match Atoms.reason store a' with
+ if Var.marked store (Atom.var a') then (
+ match Atom.reason store a' with
| Some Decision -> core := a' :: !core
| Some (Bcp c | Bcp_lazy (lazy c)) ->
Array.iter
(fun a ->
let v = Atom.var a in
- if not (Vars.marked store v) then (
+ if not (Var.marked store v) then (
seen := v :: !seen;
- Vars.mark store v;
+ Var.mark store v;
))
c.atoms
| None -> ()
);
decr idx
done;
- List.iter (Vars.unmark store) !seen;
+ List.iter (Var.unmark store) !seen;
Log.debugf 5 (fun k->k "(@[sat.analyze-final.done@ :core %a@])"
- (Format.pp_print_list (Atoms.debug store)) !core);
+ (Format.pp_print_list (Atom.debug store)) !core);
!core
(* remove some learnt clauses. *)
@@ -1768,9 +1774,9 @@ module Make(Plugin : PLUGIN)
(* Decide on a new literal, and enqueue it into the trail *)
let rec pick_branch_aux self atom : unit =
let v = Atom.var atom in
- if Vars.level self.store v >= 0 then (
- assert (Atoms.is_true self.store (Atom.pa v) ||
- Atoms.is_true self.store (Atom.na v));
+ if Var.level self.store v >= 0 then (
+ assert (Atom.is_true self.store (Atom.pa v) ||
+ Atom.is_true self.store (Atom.na v));
pick_branch_lit self
) else (
new_decision_level self;
@@ -1787,10 +1793,10 @@ module Make(Plugin : PLUGIN)
| [] when decision_level self < Vec.size self.assumptions ->
(* use an assumption *)
let a = Vec.get self.assumptions (decision_level self) in
- if Atoms.is_true self.store a then (
+ if Atom.is_true self.store a then (
new_decision_level self; (* pseudo decision level, [a] is already true *)
pick_branch_lit self
- ) else if Atoms.is_false self.store a then (
+ ) else if Atom.is_false self.store a then (
(* root conflict, find unsat core *)
let core = analyze_final self a in
raise (E_unsat (US_local {first=a; core}))
@@ -1801,7 +1807,7 @@ module Make(Plugin : PLUGIN)
begin match H.remove_min self.order with
| v ->
pick_branch_aux self
- (if Vars.default_pol self.store v then Atom.pa v else Atom.na v)
+ (if Var.default_pol self.store v then Atom.pa v else Atom.na v)
| exception Not_found -> raise_notrace E_sat
end
@@ -1845,11 +1851,11 @@ module Make(Plugin : PLUGIN)
done
let eval_level (self:t) (a:atom) =
- let lvl = Atoms.level self.store a in
- if Atoms.is_true self.store a then (
+ let lvl = Atom.level self.store a in
+ if Atom.is_true self.store a then (
assert (lvl >= 0);
true, lvl
- ) else if Atoms.is_false self.store a then (
+ ) else if Atom.is_false self.store a then (
false, lvl
) else (
raise UndecidedLit
@@ -1914,7 +1920,7 @@ module Make(Plugin : PLUGIN)
(* Check satisfiability *)
let check_clause self c =
- let res = Array.exists (Atoms.is_true self.store) c.atoms in
+ let res = Array.exists (Atom.is_true self.store) c.atoms in
if not res then (
Log.debugf 30
(fun k -> k "(@[sat.check-clause@ :not-satisfied @[%a@]@])"
@@ -1930,6 +1936,7 @@ module Make(Plugin : PLUGIN)
check_vec self self.clauses_learnt
let[@inline] theory st = st.th
+ let[@inline] store st = st.store
(* Unsafe access to internal data *)
@@ -1950,7 +1957,7 @@ module Make(Plugin : PLUGIN)
"(@[sat.full-state :res %s - Full summary:@,@[Trail:@\n%a@]@,\
@[Hyps:@\n%a@]@,@[Lemmas:@\n%a@]@,@]@."
status
- (Vec.pp ~sep:"" @@ Atoms.debug self.store) (trail self)
+ (Vec.pp ~sep:"" @@ Atom.debug self.store) (trail self)
(Vec.pp ~sep:"" @@ Clause.debug self.store) (hyps self)
(Vec.pp ~sep:"" @@ Clause.debug self.store) (history self)
)
@@ -1960,7 +1967,7 @@ module Make(Plugin : PLUGIN)
let t = trail self in
let module M = struct
type formula = Formula.t
- let iter_trail f = Vec.iter (fun a -> f (Atoms.lit self.store a)) t
+ let iter_trail f = Vec.iter (fun a -> f (Atom.lit self.store a)) t
let[@inline] eval f = eval self (make_atom self f)
let[@inline] eval_level f = eval_level self (make_atom self f)
end in
@@ -1979,7 +1986,7 @@ module Make(Plugin : PLUGIN)
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 Atoms.reason self.store a with
+ let proof_of (a:atom) = match Atom.reason self.store a with
| Some Decision -> Clause.make_removable [a] Local
| Some (Bcp c | Bcp_lazy (lazy c)) -> c
| None -> assert false
@@ -1993,9 +2000,9 @@ module Make(Plugin : PLUGIN)
) in
fun () -> Lazy.force c
in
- let get_proof () =
+ let get_proof () : Proof.t =
let c = unsat_conflict () in
- Proof.prove c
+ Proof.prove self.store c
in
let module M = struct
type nonrec atom = atom
@@ -2040,13 +2047,6 @@ module Make(Plugin : PLUGIN)
with UndecidedLit -> false
let[@inline] eval_atom self a : Solver_intf.lbool = eval_atom_ self a
-
-
- module Atom = struct
- include Atom
- let pp self out a = Atoms.pp self.store out a
- let formula self a = Atoms.lit self.store a
- end
end
[@@inline][@@specialise]
diff --git a/src/sat/Solver_intf.ml b/src/sat/Solver_intf.ml
index 0277b952..ca2f140c 100644
--- a/src/sat/Solver_intf.ml
+++ b/src/sat/Solver_intf.ml
@@ -63,6 +63,7 @@ type negated =
(** This type is used during the normalisation of formulas.
See {!val:Expr_intf.S.norm} for more details. *)
+(** The type of reasons for propagations of a formula [f]. *)
type ('formula, 'proof) reason =
| Consequence of (unit -> 'formula list * 'proof) [@@unboxed]
(** [Consequence (l, p)] means that the formulas in [l] imply the propagated
@@ -83,7 +84,6 @@ type ('formula, 'proof) reason =
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 *)
@@ -206,6 +206,8 @@ module type PROOF = sig
type clause
(** Abstract types for atoms, clauses and theory-specific lemmas *)
+ type store
+
type t
(** Lazy type for proof trees. Proofs are persistent objects, and can be
extended to proof nodes using functions defined later. *)
@@ -236,18 +238,18 @@ module type PROOF = sig
(** {3 Proof building functions} *)
- val prove : clause -> t
+ val prove : store -> clause -> t
(** Given a clause, return a proof of that clause.
@raise Resolution_error if it does not succeed. *)
- val prove_unsat : clause -> t
+ val prove_unsat : store -> 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
+ val prove_atom : store -> 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
+ val res_of_hyper_res : store -> 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.
@@ -271,13 +273,13 @@ module type PROOF = sig
(** {3 Proof Manipulation} *)
- val expand : t -> proof_node
+ val expand : store -> 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
+ val fold : store -> ('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. *)
@@ -290,11 +292,11 @@ module type PROOF = sig
(** {3 Misc} *)
- val check_empty_conclusion : t -> unit
+ val check_empty_conclusion : store -> t -> unit
(** Check that the proof's conclusion is the empty clause,
@raise Resolution_error otherwise *)
- val check : t -> unit
+ val check : store -> t -> unit
(** Check the contents of a proof. Mainly for internal use. *)
module Tbl : Hashtbl.S with type key = t
@@ -325,6 +327,8 @@ module type S = sig
type solver
+ type store
+
(* TODO: keep this internal *)
module Atom : sig
type t = atom
@@ -336,21 +340,32 @@ module type S = sig
val sign : t -> bool
val abs : t -> t
- val formula : solver -> t -> formula
- val pp : solver -> t printer
+ val pp : store -> t printer
+ (** Print the atom *)
+
+ val formula : store -> t -> formula
+ (** Get back the formula for this atom *)
end
module Clause : sig
type t = clause
val equal : t -> t -> bool
- val atoms : solver -> t -> atom array
- val atoms_l : solver -> t -> atom list
-
- val pp : solver -> t printer
- val short_name : t -> string
-
module Tbl : Hashtbl.S with type key = t
+
+ val pp : store -> t printer
+ (** Print the clause *)
+
+ val short_name : store -> t -> string
+ (** Short name for a clause. Unspecified *)
+
+ val atoms : store -> t -> atom Iter.t
+ (** Atoms of a clause *)
+
+ val atoms_a : store -> t -> atom array
+
+ val atoms_l : store -> t -> atom list
+ (** List of atoms of a clause *)
end
module Proof : PROOF
@@ -358,6 +373,7 @@ module type S = sig
and type atom = atom
and type formula = formula
and type lemma = lemma
+ and type store = store
(** A module to manipulate proofs. *)
type t = solver
@@ -381,6 +397,9 @@ module type S = sig
val theory : t -> theory
(** Access the theory state *)
+ val store : t -> store
+ (** Store for the solver *)
+
(** {2 Types} *)
(** Result type for the solver *)
@@ -412,10 +431,12 @@ module type S = sig
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
+ val make_atom : t -> ?default_pol:bool -> 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. *)
+ wether it appears in clauses or not.
+ @param default_pol default polarity of the boolean variable.
+ Default is [true]. *)
val true_at_level0 : t -> atom -> bool
(** [true_at_level0 a] returns [true] if [a] was proved at level0, i.e.
diff --git a/src/sat/dune b/src/sat/dune
index 25a4c2cf..8b762d67 100644
--- a/src/sat/dune
+++ b/src/sat/dune
@@ -4,7 +4,7 @@
(public_name sidekick.sat)
(libraries iter sidekick.util)
(synopsis "Pure OCaml SAT solver implementation for sidekick")
- (flags :standard -open Sidekick_util)
+ (flags :standard -warn-error -a+8 -open Sidekick_util)
(ocamlopt_flags :standard -O3 -bin-annot
-unbox-closures -unbox-closures-factor 20)
)
diff --git a/src/util/Bitvec.ml b/src/util/Bitvec.ml
index ab861ea7..0c043858 100644
--- a/src/util/Bitvec.ml
+++ b/src/util/Bitvec.ml
@@ -1,7 +1,4 @@
-module I32Vec = Vec
-type i32vec = int Vec.t
-
type t = {
mutable chunks: bytes; (* TODO: use a in32vec with bigarray *)
}
@@ -10,7 +7,6 @@ let create () : t = {
chunks = Bytes.make 32 '\x00';
}
-let n_bits_ = 8
let i2c = Char.chr
let c2i = Char.code
diff --git a/src/util/dune b/src/util/dune
index 584dcca7..800a53c7 100644
--- a/src/util/dune
+++ b/src/util/dune
@@ -1,4 +1,5 @@
(library
(name sidekick_util)
(public_name sidekick.util)
+ (flags :standard -warn-error -a+8)
(libraries containers iter sidekick.sigs))