simon/sidekick
1
0
Fork 0
mirror of https://github.com/c-cube/sidekick.git synced 2025-12-08 04:05:43 -05:00
Code Issues Projects Releases Packages Wiki Activity Actions

wip: refactor SAT solver

Browse source
This commit is contained in:
Simon Cruanes 2021-07-19 00:23:17 -04:00
parent b85c47ece1
commit 47bb521158
11 changed files with 323 additions and 330 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
src/backend/Backend_intf.ml
View file

@ -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

135
src/backend/Dot.ml
View file

@ -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 "<TR><TD colspan=\"2\">%a</TD></TR>" print_clause c;
let table store fmt (c, rule, color, l) =
Format.fprintf fmt "<TR><TD colspan=\"2\">%a</TD></TR>" (print_clause store) c;
match l with
| [] ->
Format.fprintf fmt "<TR><TD BGCOLOR=\"%s\" colspan=\"2\">%s</TD></TR>" 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 "<TR><TD>%a</TD></TR>" 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=<<TABLE %a>%a</TABLE>>];@\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)

31
src/backend/Dot.mli
View file

@ -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. *)

1
src/backend/dune
View file

@ -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))

1
src/core/Sidekick_core.ml
View file

@ -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

47
src/msat-solver/Sidekick_msat_solver.ml
View file

@ -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

368
src/sat/Solver.ml
View file

@ -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/<lazy>" 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:@[<hov>%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]@ {@[<hov>%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 "(@[<v2>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 @[<hov>%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)
"(@[<v>sat.full-state :res %s - Full summary:@,@[<hov 2>Trail:@\n%a@]@,\
@[<hov 2>Hyps:@\n%a@]@,@[<hov 2>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]

59
src/sat/Solver_intf.ml
View file

@ -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.

2
src/sat/dune
View file

@ -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)
)

4
src/util/Bitvec.ml
View file

@ -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

1
src/util/dune
View file

@ -1,4 +1,5 @@
(library
(name sidekick_util)
(public_name sidekick.util)
(flags :standard -warn-error -a+8)
(libraries containers iter sidekick.sigs))