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

refactor: move SAT_PROOF into sidekick.core

Browse source 
SAT proofs are part of bigger proofs, now. And we expect them to work on
the literals of CDCL(T) directly, bypassing the low level boolean atoms
This commit is contained in:
Simon Cruanes 2021-08-17 23:59:02 -04:00
parent cc1a93fa74
commit 7bead748a6
5 changed files with 169 additions and 249 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

95
src/core/Sidekick_core.ml
View file

@ -155,6 +155,35 @@ module type CC_PROOF = sig
of uninterpreted functions. *)
end
(** Signature for SAT-solver proof emission, using DRUP.
We do not store the resolution steps, just the stream of clauses deduced.
See {!Sidekick_drup} for checking these proofs. *)
module type SAT_PROOF = sig
type t
(** The stored proof (possibly nil, possibly on disk, possibly in memory) *)
type lit
(** A boolean literal for the proof trace *)
type dproof = t -> unit
(** A delayed proof, used to produce proofs on demand from theories. *)
val enabled : t -> bool
(** Do we emit proofs at all? *)
val emit_input_clause : t -> lit Iter.t -> unit
(** Emit an input clause. *)
val emit_redundant_clause : t -> lit Iter.t -> unit
(** Emit a clause deduced by the SAT solver, redundant wrt axioms.
The clause must be RUP wrt previous clauses. *)
val del_clause : t -> lit Iter.t -> unit
(** Forget a clause. Only useful for performance considerations. *)
(* TODO: replace with something index-based? *)
end
(** Proofs of unsatisfiability.
We use DRUP(T)-style traces where we simply emit clauses as we go,
@ -173,19 +202,26 @@ module type PROOF = sig
with type t := t
and type lit := lit
include SAT_PROOF
with type t := t
and type lit := lit
val begin_subproof : t -> unit
(** Begins a subproof. The result of this will only be the
clause with which {!end_subproof} is called; all other intermediate
steps will be discarded. *)
val end_subproof : t -> lit Iter.t -> unit
(** [end_subproof p lits] ends the current active subproof, which {b must}
prove the clause [lits] by RUP. *)
val end_subproof : t -> unit
(** [end_subproof p] ends the current active subproof, the last result
of which is kept. *)
val define_term : t -> term -> term -> unit
(** [define_term p cst u] defines the new constant [cst] as being equal
to [u]. *)
val lemma_true : t -> term -> unit
(** [lemma_true p (true)] asserts the clause [(true)] *)
val lemma_preprocess : t -> term -> term -> unit
(** [lemma_preprocess p t u] asserts that [t = u] is a tautology
and that [t] has been preprocessed into [u].
@ -223,6 +259,17 @@ module type LIT = sig
(** [abs lit] is like [lit] but always positive, i.e. [sign (abs lit) = true] *)
val signed_term : t -> T.Term.t * bool
(** Return the atom and the sign *)
val atom : T.Term.store -> ?sign:bool -> T.Term.t -> t
(** [atom store t] makes a literal out of a term, possibly normalizing
its sign in the process.
@param sign if provided, and [sign=false], negate the resulting lit. *)
val norm_sign : t -> t * bool
(** [norm_sign (+t)] is [+t, true],
and [norm_sign (-t)] is [+t, false].
In both cases the term is positive, and the boolean reflects the initial sign. *)
val equal : t -> t -> bool
val hash : t -> int
@ -594,6 +641,7 @@ end
new lemmas, propagate literals, access the congruence closure, etc. *)
module type SOLVER_INTERNAL = sig
module T : TERM
module Lit : LIT with module T = T
type ty = T.Ty.t
type term = T.Term.t
@ -603,13 +651,6 @@ module type SOLVER_INTERNAL = sig
type dproof = proof -> unit
(** Delayed proof. This is used to build a proof step on demand. *)
(** {3 Literals}
A literal is a (preprocessed) term along with its sign.
It is directly manipulated by the SAT solver.
*)
module Lit : LIT with module T = T
(** {3 Proofs} *)
module P : PROOF with type lit = Lit.t and type term = term and type t = proof
@ -726,7 +767,7 @@ module type SOLVER_INTERNAL = sig
(** Create a literal. This automatically preprocesses the term. *)
val preprocess_term :
t -> add_clause:(Lit.t list -> proof -> unit) -> term -> term * dproof
t -> add_clause:(Lit.t list -> dproof -> unit) -> term -> term * dproof
(** Preprocess a term. *)
val add_lit : t -> actions -> lit -> unit
@ -989,7 +1030,7 @@ module type SOLVER = sig
?stat:Stat.t ->
?size:[`Big | `Tiny | `Small] ->
(* TODO? ?config:Config.t -> *)
?store_proof:bool ->
proof:proof ->
theories:theory list ->
T.Term.store ->
T.Ty.store ->
@ -1018,7 +1059,7 @@ module type SOLVER = sig
val add_theory_l : t -> theory list -> unit
val mk_atom_lit : t -> lit -> Atom.t
val mk_atom_lit : t -> lit -> Atom.t * dproof
(** [mk_atom_lit _ lit] returns [atom, pr]
where [atom] is an internal atom for the solver,
and [pr] is a proof of [|- lit = atom] *)
@ -1026,7 +1067,7 @@ module type SOLVER = sig
val mk_atom_lit' : t -> lit -> Atom.t
(** Like {!mk_atom_t} but skips the proof *)
val mk_atom_t : t -> ?sign:bool -> term -> Atom.t
val mk_atom_t : t -> ?sign:bool -> term -> Atom.t * dproof
(** [mk_atom_t _ ~sign t] returns [atom, pr]
where [atom] is an internal representation of [± t],
and [pr] is a proof of [|- atom = (± t)] *)
@ -1034,11 +1075,11 @@ module type SOLVER = sig
val mk_atom_t' : t -> ?sign:bool -> term -> Atom.t
(** Like {!mk_atom_t} but skips the proof *)
val add_clause : t -> Atom.t IArray.t -> P.t -> unit
val add_clause : t -> Atom.t IArray.t -> dproof -> unit
(** [add_clause solver cs] adds a boolean clause to the solver.
Subsequent calls to {!solve} will need to satisfy this clause. *)
val add_clause_l : t -> Atom.t list -> P.t -> unit
val add_clause_l : t -> Atom.t list -> dproof -> unit
(** Add a clause to the solver, given as a list. *)
val assert_terms : t -> term list -> unit
@ -1049,32 +1090,10 @@ module type SOLVER = sig
(** Helper that turns the term into an atom, before adding the result
to the solver as a unit clause assertion *)
(** {2 Internal representation of proofs}
A type or state convertible into {!P.t} *)
module Pre_proof : sig
type t
val output : out_channel -> t -> unit
(** Output onto a channel, efficiently *)
val pp_debug : t Fmt.printer
val pp_dot : t Fmt.printer option
(** Optional printer into DOT/graphviz *)
val check : t -> unit
(** Check the proof (to an unspecified level of confidence;
this can be a no-op). May fail. *)
val to_proof : t -> P.t
end
(** Result of solving for the current set of clauses *)
type res =
| Sat of Model.t (** Satisfiable *)
| Unsat of {
proof: Pre_proof.t option lazy_t; (** proof of unsat *)
unsat_core: Atom.t list lazy_t; (** subset of assumptions responsible for unsat *)
} (** Unsatisfiable *)
| Unknown of Unknown.t

200
src/sat/Solver.ml
View file

@ -33,14 +33,14 @@ end
module Make(Plugin : PLUGIN)
= struct
type formula = Plugin.formula
type theory = Plugin.t
type proof = Plugin.proof
type dproof = proof -> unit
module Formula = Plugin.Formula
module Proof = Plugin.Proof
type formula = Formula.t
type theory = Plugin.t
type lemma = Plugin.lemma
type proof = Plugin.proof
(* ### types ### *)
(* a boolean variable (positive int) *)
@ -88,27 +88,11 @@ module Make(Plugin : PLUGIN)
end
type clause = Clause0.t
(* TODO: remove, replace with user-provided proof trackng device?
for pure SAT, [reason] is sufficient *)
type premise =
| Hyp of lemma
| Local
| Lemma of lemma
| History of clause list
| Empty_premise
and reason =
| Decision
| Bcp of clause
| Bcp_lazy of clause lazy_t
let kind_of_premise p = match p with
| Hyp _ -> "H"
| Lemma _ -> "T"
| Local -> "L"
| History _ -> "C"
| Empty_premise -> ""
(* ### stores ### *)
module Form_tbl = Hashtbl.Make(Formula)
@ -118,7 +102,6 @@ module Make(Plugin : PLUGIN)
type cstore = {
c_lits: atom array Vec.t; (* storage for clause content *)
c_activity: Vec_float.t;
c_premise: premise Vec.t;
c_recycle_idx: VecI32.t; (* recycle clause numbers that were GC'd *)
c_attached: Bitvec.t;
c_marked: Bitvec.t; (* TODO : remove *)
@ -170,7 +153,6 @@ module Make(Plugin : PLUGIN)
c_store={
c_lits=Vec.create();
c_activity=Vec_float.create();
c_premise=Vec.create();
c_recycle_idx=VecI32.create ~cap:0 ();
c_dead=Bitvec.create();
c_attached=Bitvec.create();
@ -245,8 +227,7 @@ module Make(Plugin : PLUGIN)
| n, None -> Format.fprintf out "%d" n
| n, Some Decision -> Format.fprintf out "@@%d" n
| n, Some Bcp c ->
let premise = Vec.get self.c_store.c_premise (c:>int) in
Format.fprintf out "->%d/%s/%d" n (kind_of_premise premise) (c:>int)
Format.fprintf out "->%d/%d" n (c:>int)
| n, Some (Bcp_lazy _) -> Format.fprintf out "->%d/<lazy>" n
let pp_level self out a =
@ -274,11 +255,9 @@ module Make(Plugin : PLUGIN)
(** Make a clause with the given atoms *)
val make_a : store -> removable:bool -> atom array -> premise -> t
val make_l : store -> removable:bool -> atom list -> premise -> t
val make_vec : store -> removable:bool -> atom Vec.t -> premise -> t
val premise : store -> t -> premise
val make_a : store -> removable:bool -> atom array -> t
val make_l : store -> removable:bool -> atom list -> t
val make_vec : store -> removable:bool -> atom Vec.t -> t
val n_atoms : store -> t -> int
@ -314,9 +293,9 @@ module Make(Plugin : PLUGIN)
(* TODO: store watch lists inside clauses *)
let make_a (store:store) ~removable (atoms:atom array) premise : t =
let make_a (store:store) ~removable (atoms:atom array) : t =
let {
c_recycle_idx; c_lits; c_activity; c_premise;
c_recycle_idx; c_lits; c_activity;
c_attached; c_dead; c_removable; c_marked;
} = store.c_store in
(* allocate new ID *)
@ -330,7 +309,6 @@ module Make(Plugin : PLUGIN)
begin
let new_len = cid + 1 in
Vec.ensure_size c_lits [||] new_len;
Vec.ensure_size c_premise Empty_premise new_len;
Vec_float.ensure_size c_activity new_len;
Bitvec.ensure_size c_attached new_len;
Bitvec.ensure_size c_dead new_len;
@ -341,16 +319,15 @@ module Make(Plugin : PLUGIN)
end;
Vec.set c_lits cid atoms;
Vec.set c_premise cid premise;
let c = of_int_unsafe cid in
c
let make_l store ~removable atoms premise : t =
make_a store ~removable (Array.of_list atoms) premise
let make_l store ~removable atoms : t =
make_a store ~removable (Array.of_list atoms)
let make_vec store ~removable atoms premise : t =
make_a store ~removable (Vec.to_array atoms) premise
let make_vec store ~removable atoms : t =
make_a store ~removable (Vec.to_array atoms)
let[@inline] n_atoms (store:store) (c:t) : int =
Array.length (Vec.get store.c_store.c_lits (c:t:>int))
@ -377,7 +354,6 @@ module Make(Plugin : PLUGIN)
let {c_lits; _} = store.c_store in
Array.fold_left f acc (Vec.get c_lits (c:t:>int))
let[@inline] premise store c = Vec.get store.c_store.c_premise (c:t:>int)
let[@inline] marked store c = Bitvec.get store.c_store.c_marked (c:t:>int)
let[@inline] set_marked store c b = Bitvec.set store.c_store.c_marked (c:t:>int) b
let[@inline] attached store c = Bitvec.get store.c_store.c_attached (c:t:>int)
@ -389,7 +365,7 @@ module Make(Plugin : PLUGIN)
let dealloc store c : unit =
assert (dead store c);
let {c_lits; c_premise; c_recycle_idx; c_activity;
let {c_lits; c_recycle_idx; c_activity;
c_dead; c_removable; c_attached; c_marked; } = store.c_store in
(* clear data *)
@ -399,7 +375,6 @@ module Make(Plugin : PLUGIN)
Bitvec.set c_removable cid false;
Bitvec.set c_marked cid false;
Vec.set c_lits cid [||];
Vec.set c_premise cid Empty_premise;
Vec_float.set c_activity cid 0.;
VecI32.push c_recycle_idx cid; (* recycle idx *)
@ -412,14 +387,14 @@ module Make(Plugin : PLUGIN)
let[@inline] activity store c = Vec_float.get store.c_store.c_activity (c:t:>int)
let[@inline] set_activity store c f = Vec_float.set store.c_store.c_activity (c:t:>int) f
let[@inline] make_removable store l premise =
make_l store ~removable:true l premise
let[@inline] make_removable store l =
make_l store ~removable:true l
let[@inline] make_removable_a store a premise =
make_a store ~removable:true a premise
let[@inline] make_removable_a store a =
make_a store ~removable:true a
let[@inline] make_permanent store l premise =
let c = make_l store ~removable:false l premise in
let[@inline] make_permanent store l =
let c = make_l store ~removable:false l in
assert (not (removable store c)); (* permanent by default *)
c
@ -428,32 +403,18 @@ module Make(Plugin : PLUGIN)
let atoms_l store c : _ list = Array.to_list (atoms_a store c)
let atoms_iter store c = fun k -> iter store c ~f:k
let short_name store c =
let p = premise store c in
Printf.sprintf "%s%d" (kind_of_premise p) (c:t:>int)
let short_name _store c = Printf.sprintf "cl[%d]" (c:t:>int)
let pp store fmt c =
let p = premise store c in
Format.fprintf fmt "(cl[%s%d] : %a" (kind_of_premise p) (c:t:>int)
Format.fprintf fmt "(cl[%d] : %a" (c:t:>int)
(Atom.pp_a store) (atoms_a store c)
let debug_premise out = function
| Hyp _ -> Format.fprintf out "hyp"
| Lemma _ -> Format.fprintf out "th_lemma"
| Local -> Format.fprintf out "local"
| History v as p ->
Format.fprintf out "(@[res";
List.iter (fun c -> Format.fprintf out "@ %s%d," (kind_of_premise p) (c:t:>int)) v;
Format.fprintf out "@])"
| Empty_premise -> Format.fprintf out "none"
let debug store out c =
let atoms = atoms_a store c in
let p = premise store c in
Format.fprintf out
"(@[cl[%s%d]@ {@[<hov>%a@]}@ :premise %a@])"
(kind_of_premise p) (c:t:>int)
(Atom.debug_a store) atoms debug_premise p
"(@[cl[%d]@ {@[<hov>%a@]}@])"
(c:t:>int)
(Atom.debug_a store) atoms
end
(* allocate new variable *)
@ -557,7 +518,7 @@ module Make(Plugin : PLUGIN)
th: theory;
(* user defined theory *)
store_proof: bool; (* do we store proofs? *)
proof: Proof.t; (* the proof object *)
(* Clauses are simplified for efficiency purposes. In the following
vectors, the comments actually refer to the original non-simplified
@ -647,7 +608,7 @@ module Make(Plugin : PLUGIN)
let _nop_on_conflict (_:atom array) = ()
(* Starting environment. *)
let create_ ~store ~store_proof (th:theory) : t = {
let create_ ~store ~proof (th:theory) : t = {
store; th;
unsat_at_0=None;
next_decisions = [];
@ -671,7 +632,8 @@ module Make(Plugin : PLUGIN)
var_incr = 1.;
clause_incr = 1.;
store_proof;
proof;
n_conflicts = 0;
n_decisions = 0;
@ -687,10 +649,10 @@ module Make(Plugin : PLUGIN)
let create
?on_conflict ?on_decision ?on_new_atom ?on_learnt ?on_gc
?(store_proof=true) ?(size=`Big)
?(size=`Big) ~proof
(th:theory) : t =
let store = Store.create ~size () in
let self = create_ ~store ~store_proof th in
let self = create_ ~store ~proof th in
self.on_new_atom <- on_new_atom;
self.on_decision <- on_decision;
self.on_conflict <- on_conflict;
@ -806,7 +768,7 @@ module Make(Plugin : PLUGIN)
clause
) else (
let removable = Clause.removable store clause in
Clause.make_l store ~removable !res (History [clause])
Clause.make_l store ~removable !res
)
(* TODO: do it in place in a vec? *)
@ -948,7 +910,6 @@ module Make(Plugin : PLUGIN)
Log.debugf 3 (fun k -> k "(@[sat.unsat-conflict@ %a@])" (pp_unsat_cause self) us);
let us = match us with
| US_false c ->
let c = if self.store_proof then Proof.prove_unsat self.store c else c in
self.unsat_at_0 <- Some c;
(match self.on_learnt with Some f -> f self (Clause.atoms_a self.store c) | None -> ());
US_false c
@ -979,9 +940,7 @@ module Make(Plugin : PLUGIN)
and set it as the cause for the propagation of [a], that way we can
rebuild the whole resolution tree when we want to prove [a]. *)
let removable = Clause.removable self.store cl in
let c' =
Clause.make_l self.store ~removable l (History (cl :: history))
in
let c' = Clause.make_l self.store ~removable l in
Log.debugf 3
(fun k -> k "(@[<hv>sat.simplified-reason@ %a@ %a@])"
(Clause.debug self.store) cl (Clause.debug self.store) c');
@ -1208,10 +1167,6 @@ module Make(Plugin : PLUGIN)
(* add the learnt clause to the clause database, propagate, etc. *)
let record_learnt_clause (self:t) (confl:clause) (cr:conflict_res): unit =
let store = self.store in
let proof =
if self.store_proof
then History (Array.to_list cr.cr_history)
else Empty_premise in
begin match cr.cr_learnt with
| [| |] -> assert false
| [|fuip|] ->
@ -1221,14 +1176,14 @@ module Make(Plugin : PLUGIN)
report_unsat self (US_false confl)
) else (
let uclause =
Clause.make_a store ~removable:true cr.cr_learnt proof in
Clause.make_a store ~removable:true cr.cr_learnt in
(match self.on_learnt with Some f -> f self cr.cr_learnt | None -> ());
(* no need to attach [uclause], it is true at level 0 *)
enqueue_bool self fuip ~level:0 (Bcp uclause)
)
| _ ->
let fuip = cr.cr_learnt.(0) in
let lclause = Clause.make_a store ~removable:true cr.cr_learnt proof in
let lclause = Clause.make_a store ~removable:true cr.cr_learnt in
if Clause.n_atoms store lclause > 2 then (
Vec.push self.clauses_learnt lclause; (* potentially gc'able *)
);
@ -1287,9 +1242,8 @@ module Make(Plugin : PLUGIN)
List.iteri (fun i a -> c_atoms.(i) <- a) atoms;
c
) else (
let proof = if self.store_proof then History (c::history) else Empty_premise in
let removable = Clause.removable store c in
Clause.make_l store ~removable atoms proof
Clause.make_l store ~removable atoms
)
in
assert (Clause.removable store clause = Clause.removable store init);
@ -1420,10 +1374,11 @@ module Make(Plugin : PLUGIN)
let[@inline] slice_get st i = Vec.get st.trail i
let acts_add_clause self ?(keep=false) (l:formula list) (lemma:lemma): unit =
let acts_add_clause self ?(keep=false) (l:formula list) (dp:dproof): unit =
let atoms = List.rev_map (make_atom self) l in
let removable = not keep in
let c = Clause.make_l self.store ~removable atoms (Lemma lemma) in
let c = Clause.make_l self.store ~removable atoms in
if Proof.enabled self.proof then dp self.proof;
Log.debugf 5 (fun k->k "(@[sat.th.add-clause@ %a@])" (Clause.debug self.store) c);
Vec.push self.clauses_to_add c
@ -1436,10 +1391,11 @@ module Make(Plugin : PLUGIN)
self.next_decisions <- a :: self.next_decisions
)
let acts_raise self (l:formula list) proof : 'a =
let acts_raise self (l:formula list) (pr:dproof) : 'a =
let atoms = List.rev_map (make_atom self) l in
(* conflicts can be removed *)
let c = Clause.make_l self.store ~removable:true atoms (Lemma proof) in
let c = Clause.make_l self.store ~removable:true atoms in
if Proof.enabled self.proof then pr self.proof;
Log.debugf 5 (fun k->k "(@[@{<yellow>sat.th.raise-conflict@}@ %a@])"
(Clause.debug self.store) c);
raise_notrace (Th_conflict c)
@ -1460,15 +1416,16 @@ module Make(Plugin : PLUGIN)
let p = make_atom self f in
if Atom.is_true store p then ()
else if Atom.is_false store p then (
let lits, proof = mk_expl() in
let lits, dp = mk_expl() in
let l = List.rev_map (fun f -> Atom.neg @@ make_atom self f) lits in
check_consequence_lits_false_ self l;
let c = Clause.make_l store ~removable:true (p :: l) (Lemma proof) in
let c = Clause.make_l store ~removable:true (p :: l) in
if Proof.enabled self.proof then dp self.proof;
raise_notrace (Th_conflict c)
) else (
insert_var_order self (Atom.var p);
let c = lazy (
let lits, proof = mk_expl () in
let lits, dp = mk_expl () in
let l = List.rev_map (fun f -> Atom.neg @@ make_atom self f) lits in
(* note: we can check that invariant here in the [lazy] block,
as conflict analysis will run in an environment where
@ -1477,7 +1434,8 @@ module Make(Plugin : PLUGIN)
(otherwise the propagated lit would have been backtracked and
discarded already.) *)
check_consequence_lits_false_ self l;
Clause.make_l store ~removable:true (p :: l) (Lemma proof)
if Proof.enabled self.proof then dp self.proof;
Clause.make_l store ~removable:true (p :: l)
) in
let level = decision_level self in
self.n_propagations <- 1 + self.n_propagations;
@ -1505,7 +1463,7 @@ module Make(Plugin : PLUGIN)
let[@inline] current_slice st : _ Solver_intf.acts =
let module M = struct
type nonrec proof = proof
type nonrec lemma = lemma
type dproof = proof -> unit
type nonrec formula = formula
let iter_assumptions=acts_iter st ~full:false st.th_head
let eval_lit= acts_eval_lit st
@ -1521,7 +1479,7 @@ module Make(Plugin : PLUGIN)
let[@inline] full_slice st : _ Solver_intf.acts =
let module M = struct
type nonrec proof = proof
type nonrec lemma = lemma
type dproof = proof -> unit
type nonrec formula = formula
let iter_assumptions=acts_iter st ~full:true st.th_head
let eval_lit= acts_eval_lit st
@ -1842,11 +1800,12 @@ module Make(Plugin : PLUGIN)
done
with E_sat -> ()
let assume self cnf lemma : unit =
let assume self cnf dp : unit =
List.iter
(fun l ->
let atoms = List.rev_map (make_atom self) l in
let c = Clause.make_l self.store ~removable:false atoms (Hyp lemma) in
let c = Clause.make_l self.store ~removable:false atoms in
if Proof.enabled self.proof then dp self.proof;
Log.debugf 10 (fun k -> k "(@[sat.assume-clause@ @[<hov 2>%a@]@])"
(Clause.debug self.store) c);
Vec.push self.clauses_to_add c)
@ -1875,7 +1834,7 @@ module Make(Plugin : PLUGIN)
(* Result type *)
type res =
| Sat of Formula.t Solver_intf.sat_state
| Unsat of (atom,clause,Proof.t) Solver_intf.unsat_state
| Unsat of (atom,clause) Solver_intf.unsat_state
let pp_all self lvl status =
Log.debugf lvl
@ -1911,45 +1870,32 @@ 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 Atom.reason self.store a with
| Some Decision -> Clause.make_l self.store ~removable:true [a] Local
| Some (Bcp c | Bcp_lazy (lazy c)) -> c
| None -> assert false
in
let other_lits = List.filter (fun a -> not (Atom.equal a first)) core in
let hist =
Clause.make_l self.store ~removable:false [first] Local ::
proof_of first ::
List.map proof_of other_lits in
Clause.make_l self.store ~removable:false [] (History hist)
Clause.make_l self.store ~removable:false []
) in
fun () -> Lazy.force c
in
let get_proof () : Proof.t =
let c = unsat_conflict () in
Proof.prove self.store c
in
let module M = struct
type nonrec atom = atom
type clause = Clause.t
type proof = Proof.t
let get_proof = get_proof
let unsat_conflict = unsat_conflict
let unsat_assumptions = unsat_assumptions
end in
(module M)
let add_clause_a self c lemma : unit =
let add_clause_a self c dp : unit =
try
let c = Clause.make_a self.store ~removable:false c (Hyp lemma) in
let c = Clause.make_a self.store ~removable:false c in
if Proof.enabled self.proof then dp self.proof;
add_clause_ self c
with
| E_unsat (US_false c) ->
self.unsat_at_0 <- Some c
let add_clause self c lemma : unit =
let add_clause self c dp : unit =
try
let c = Clause.make_l self.store ~removable:false c (Hyp lemma) in
let c = Clause.make_l self.store ~removable:false c in
if Proof.enabled self.proof then dp self.proof;
add_clause_ self c
with
| E_unsat (US_false c) ->
@ -1985,14 +1931,16 @@ module Make_cdcl_t(Plugin : Solver_intf.PLUGIN_CDCL_T) =
module Make_pure_sat(Plugin : Solver_intf.PLUGIN_SAT) =
Make(struct
module Formula = Plugin.Formula
type t = unit
type proof = Plugin.proof
let push_level () = ()
let pop_levels _ _ = ()
let partial_check () _ = ()
let final_check () _ = ()
let has_theory = false
end)
type formula = Plugin.formula
type proof = Plugin.proof
module Formula = Plugin.Formula
module Proof = Plugin.Proof
type t = unit
let push_level () = ()
let pop_levels _ _ = ()
let partial_check () _ = ()
let final_check () _ = ()
let has_theory = false
end)
[@@inline][@@specialise]

10
src/sat/Solver.mli
View file

@ -3,13 +3,15 @@ module type S = Solver_intf.S
(** Safe external interface of solvers. *)
module Make_pure_sat(Th: Solver_intf.PLUGIN_SAT)
: S with module Formula = Th.Formula
and type lemma = Th.lemma
: S with type formula = Th.formula
and module Formula = Th.Formula
and type proof = Th.proof
and module Proof = Th.Proof
and type theory = unit
module Make_cdcl_t(Th : Solver_intf.PLUGIN_CDCL_T)
: S with module Formula = Th.Formula
and type lemma = Th.lemma
: S with type formula = Th.formula
and module Formula = Th.Formula
and type proof = Th.proof
and module Proof = Th.Proof
and type theory = Th.t

111
src/sat/Solver_intf.ml
View file

@ -39,22 +39,17 @@ type 'form sat_state = (module SAT_STATE with type formula = 'form)
module type UNSAT_STATE = sig
type atom
type clause
type proof
val unsat_conflict : unit -> clause
(** Returns the unsat clause found at the toplevel *)
val get_proof : unit -> proof
(** returns a persistent proof of the empty clause from the Unsat result. *)
val unsat_assumptions: unit -> atom list
(** Subset of assumptions responsible for "unsat" *)
end
type ('atom, 'clause, 'proof) unsat_state =
type ('atom, 'clause) unsat_state =
(module UNSAT_STATE with type atom = 'atom
and type clause = 'clause
and type proof = 'proof)
and type clause = 'clause)
(** The type of values returned when the solver reaches an UNSAT state. *)
type negated =
@ -64,8 +59,8 @@ type negated =
See {!val:Expr_intf.S.norm} for more details. *)
(** The type of reasons for propagations of a formula [f]. *)
type ('formula, 'lemma) reason =
| Consequence of (unit -> 'formula list * 'lemma) [@@unboxed]
type ('formula, 'proof) reason =
| Consequence of (unit -> 'formula list * 'proof) [@@unboxed]
(** [Consequence (l, p)] means that the formulas in [l] imply the propagated
formula [f]. The proof should be a proof of the clause "[l] implies [f]".
@ -90,7 +85,8 @@ type lbool = L_true | L_false | L_undefined
module type ACTS = sig
type formula
type lemma
type proof
type dproof = proof -> unit
val iter_assumptions: (formula -> unit) -> unit
(** Traverse the new assumptions on the boolean trail. *)
@ -102,19 +98,19 @@ module type ACTS = sig
(** Map the given formula to a literal, which will be decided by the
SAT solver. *)
val add_clause: ?keep:bool -> formula list -> lemma -> unit
val add_clause: ?keep:bool -> formula list -> dproof -> unit
(** Add a clause to the solver.
@param keep if true, the clause will be kept by the solver.
Otherwise the solver is allowed to GC the clause and propose this
partial model again.
*)
val raise_conflict: formula list -> lemma -> 'b
val raise_conflict: formula list -> dproof -> 'b
(** Raise a conflict, yielding control back to the solver.
The list of atoms must be a valid theory lemma that is false in the
current trail. *)
val propagate: formula -> (formula, lemma) reason -> unit
val propagate: formula -> (formula, dproof) reason -> unit
(** Propagate a formula, i.e. the theory can evaluate the formula to be true
(see the definition of {!type:eval_res} *)
@ -124,9 +120,9 @@ module type ACTS = sig
Useful for theory combination. This will be undone on backtracking. *)
end
type ('formula, 'lemma) acts =
type ('formula, 'proof) acts =
(module ACTS with type formula = 'formula
and type lemma = 'lemma)
and type proof = 'proof)
(** The type for a slice of assertions to assume/propagate in the theory. *)
exception No_proof
@ -157,61 +153,22 @@ module type FORMULA = sig
but one returns [Negated] and the other [Same_sign]. *)
end
(** Signature for proof emission, using DRUP.
We do not store the resolution steps, just the stream of clauses deduced.
See {!Sidekick_drup} for checking these proofs. *)
module type PROOF = sig
type t
(** The stored proof (possibly nil, possibly on disk, possibly in memory) *)
type atom
(** A boolean atom for the proof trace *)
type lemma
(** A theory lemma *)
module Atom : sig
type t = atom
val sign : t -> bool
val var_int : t -> int
val make : sign:bool -> int -> t
val pp : t Fmt.printer
end
val enabled : t -> bool
(** Do we emit proofs at all? *)
val emit_input_clause : t -> atom Iter.t -> unit
(** Emit an input clause. *)
val emit_lemma : t -> atom Iter.t -> lemma -> unit
(** Emit a theory lemma *)
val emit_redundant_clause : t -> atom Iter.t -> unit
(** Emit a clause deduced by the SAT solver, redundant wrt axioms.
The clause must be RUP wrt previous clauses. *)
val del_clause : t -> atom Iter.t -> unit
(** Forget a clause. Only useful for performance considerations. *)
end
module type PROOF = Sidekick_core.SAT_PROOF
(** Signature for theories to be given to the CDCL(T) solver *)
module type PLUGIN_CDCL_T = sig
type t
(** The plugin state itself *)
module Formula : FORMULA
type formula
module Formula : FORMULA with type t = formula
type proof
(** Proof storage/recording *)
type lemma
(* Theory lemmas *)
module Proof : PROOF
with type t = proof
and type lemma = lemma
and type lit = formula
val push_level : t -> unit
(** Create a new backtrack level *)
@ -219,12 +176,12 @@ module type PLUGIN_CDCL_T = sig
val pop_levels : t -> int -> unit
(** Pop [n] levels of the theory *)
val partial_check : t -> (Formula.t, lemma) acts -> unit
val partial_check : t -> (Formula.t, proof) acts -> unit
(** Assume the formulas in the slice, possibly using the [slice]
to push new formulas to be propagated or to raising a conflict or to add
new lemmas. *)
val final_check : t -> (Formula.t, lemma) acts -> unit
val final_check : t -> (Formula.t, proof) acts -> unit
(** Called at the end of the search in case a model has been found.
If no new clause is pushed, then proof search ends and "sat" is returned;
if lemmas are added, search is resumed;
@ -233,14 +190,11 @@ end
(** Signature for pure SAT solvers *)
module type PLUGIN_SAT = sig
module Formula : FORMULA
type formula
module Formula : FORMULA with type t = formula
type lemma = unit
type proof
module Proof : PROOF
with type t = proof
and type lemma = lemma
module Proof : PROOF with type t = proof and type lit = formula
end
(** The external interface implemented by safe solvers, such as the one
@ -250,9 +204,9 @@ module type S = sig
These are the internal modules used, you should probably not use them
if you're not familiar with the internals of mSAT. *)
module Formula : FORMULA
type formula (** user formulas *)
type formula = Formula.t (** user formulas *)
module Formula : FORMULA with type t = formula
type atom
(** The type of atoms given by the module argument for formulas.
@ -263,12 +217,11 @@ module type S = sig
type theory
type lemma
(** A theory lemma or an input axiom. *)
type proof
(** A representation of a full proof *)
type dproof = proof -> unit
type solver
(** The main solver type. *)
@ -317,8 +270,7 @@ module type S = sig
end
module Proof : PROOF
with type atom = atom
and type lemma = lemma
with type lit = formula
and type t = proof
(** A module to manipulate proofs. *)
@ -331,14 +283,13 @@ module type S = sig
?on_new_atom:(t -> atom -> unit) ->
?on_learnt:(t -> atom array -> unit) ->
?on_gc:(t -> atom array -> unit) ->
?store_proof:bool ->
?size:[`Tiny|`Small|`Big] ->
proof:Proof.t ->
theory ->
t
(** Create new solver
@param theory the theory
@param store_proof if true, stores proof (default [true]). Otherwise
the functions that return proofs will fail with [No_proof]
@param the proof
@param size the initial size of internal data structures. The bigger,
the faster, but also the more RAM it uses. *)
@ -353,7 +304,7 @@ module type S = sig
(** Result type for the solver *)
type res =
| Sat of formula sat_state (** Returned when the solver reaches SAT, with a model *)
| Unsat of (atom,clause,Proof.t) unsat_state (** Returned when the solver reaches UNSAT, with a proof *)
| Unsat of (atom,clause) unsat_state (** Returned when the solver reaches UNSAT, with a proof *)
exception UndecidedLit
(** Exception raised by the evaluating functions when a literal
@ -361,14 +312,14 @@ module type S = sig
(** {2 Base operations} *)
val assume : t -> formula list list -> lemma -> unit
val assume : t -> formula list list -> dproof -> unit
(** Add the list of clauses to the current set of assumptions.
Modifies the sat solver state in place. *)
val add_clause : t -> atom list -> lemma -> unit
val add_clause : t -> atom list -> dproof -> unit
(** Lower level addition of clauses *)
val add_clause_a : t -> atom array -> lemma -> unit
val add_clause_a : t -> atom array -> dproof -> unit
(** Lower level addition of clauses *)
val solve :

2
src/sat/dune
View file

@ -2,7 +2,7 @@
(library
(name sidekick_sat)
(public_name sidekick.sat)
(libraries iter sidekick.util)
(libraries iter sidekick.util sidekick.core)
(synopsis "Pure OCaml SAT solver implementation for sidekick")
(flags :standard -warn-error -a+8 -open Sidekick_util)
(ocamlopt_flags :standard -O3 -bin-annot