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

refactor(sat): simplify interface a lot

Browse source 
- pure_sat is not a functor anymore
- make_cdcl_t is only functorized over theory
- both use standard `Lit.t` and proofs
This commit is contained in:
Simon Cruanes 2022-07-29 22:28:21 -04:00
parent c09650db51
commit d4ba4602a4
No known key found for this signature in database
GPG key ID: EBFFF6F283F3A2B4
6 changed files with 111 additions and 242 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

31
src/sat/Proof_dummy.ml
View file

@ -1,31 +0,0 @@
(** Dummy proof module using rule=[unit].
These proof traces will not record anything. *)
module Make (Lit : sig
type t
end) : sig
module Proof_trace :
Sidekick_sigs_proof_trace.S
with type A.rule = unit
and type A.step_id = unit
and type t = unit
module Proof_rules :
Solver_intf.PROOF_RULES
with type lit = Lit.t
and type rule = unit
and type step_id = unit
end = struct
module Proof_trace = Sidekick_proof_trace_dummy.Unit
module Proof_rules = struct
type lit = Lit.t
type rule = unit
type step_id = unit
let sat_input_clause _ = ()
let sat_redundant_clause _ ~hyps:_ = ()
let sat_unsat_core _ = ()
end
end

19
src/sat/Sidekick_sat.ml
View file

@ -1,29 +1,25 @@
(** Main API *) (** Main API *)
open Sidekick_core
module Solver_intf = Solver_intf module Solver_intf = Solver_intf
module type S = Solver_intf.S module type S = Solver_intf.S
module type LIT = Solver_intf.LIT module type LIT = Solver_intf.LIT
module type PLUGIN_CDCL_T = Solver_intf.PLUGIN_CDCL_T module type PLUGIN_CDCL_T = Solver_intf.PLUGIN_CDCL_T
module type PLUGIN_SAT = Solver_intf.PLUGIN_SAT
module type PROOF_RULES = Solver_intf.PROOF_RULES
type lbool = Solver_intf.lbool = L_true | L_false | L_undefined type lbool = Solver_intf.lbool = L_true | L_false | L_undefined
module type SAT_STATE = Solver_intf.SAT_STATE module type SAT_STATE = Solver_intf.SAT_STATE
type 'form sat_state = 'form Solver_intf.sat_state type sat_state = Solver_intf.sat_state
type ('lit, 'proof) reason = ('lit, 'proof) Solver_intf.reason = type reason = Solver_intf.reason =
| Consequence of (unit -> 'lit list * 'proof) | Consequence of (unit -> Lit.t list * Proof_step.id)
[@@unboxed] [@@unboxed]
module type ACTS = Solver_intf.ACTS module type ACTS = Solver_intf.ACTS
type ('lit, 'proof, 'proof_step) acts = type acts = (module ACTS)
('lit, 'proof, 'proof_step) Solver_intf.acts
type negated = bool
(** Print {!lbool} values *) (** Print {!lbool} values *)
let pp_lbool out = function let pp_lbool out = function
@ -36,7 +32,4 @@ exception Resource_exhausted = Solver_intf.Resource_exhausted
module Solver = Solver module Solver = Solver
module Make_cdcl_t = Solver.Make_cdcl_t module Make_cdcl_t = Solver.Make_cdcl_t
module Make_pure_sat = Solver.Make_pure_sat module Pure_sat = Solver.Pure_sat
module Proof_dummy = Proof_dummy
(** Module for dummy proofs based on unit *)

135
src/sat/Solver.ml
View file

@ -1,3 +1,5 @@
open Sidekick_core
module type PLUGIN = sig module type PLUGIN = sig
val has_theory : bool val has_theory : bool
(** [true] iff the solver is parametrized by a theory, not just (** [true] iff the solver is parametrized by a theory, not just
@ -13,16 +15,9 @@ let invalid_argf fmt =
Format.kasprintf (fun msg -> invalid_arg ("sidekick.sat: " ^ msg)) fmt Format.kasprintf (fun msg -> invalid_arg ("sidekick.sat: " ^ msg)) fmt
module Make (Plugin : PLUGIN) = struct module Make (Plugin : PLUGIN) = struct
module Lit = Plugin.Lit module Step_vec = Proof_trace.Step_vec
module Proof_trace = Plugin.Proof_trace
module Proof_rules = Plugin.Proof_rules
module Step_vec = Proof_trace.A.Step_vec
type lit = Plugin.Lit.t
type theory = Plugin.t type theory = Plugin.t
type proof_rule = Proof_trace.A.rule
type proof_step = Proof_trace.A.step_id
type proof_trace = Proof_trace.t
module Clause_pool_id : sig module Clause_pool_id : sig
type t = private int type t = private int
@ -128,10 +123,10 @@ module Make (Plugin : PLUGIN) = struct
(* atoms *) (* atoms *)
a_is_true: Bitvec.t; a_is_true: Bitvec.t;
a_seen: Bitvec.t; a_seen: Bitvec.t;
a_form: lit Vec.t; a_form: Lit.t Vec.t;
(* TODO: store watches in clauses instead *) (* TODO: store watches in clauses instead *)
a_watched: Clause0.CVec.t Vec.t; a_watched: Clause0.CVec.t Vec.t;
a_proof_lvl0: proof_step ATbl.t; a_proof_lvl0: Proof_step.id ATbl.t;
(* atom -> proof for it to be true at level 0 *) (* atom -> proof for it to be true at level 0 *)
stat_n_atoms: int Stat.counter; stat_n_atoms: int Stat.counter;
(* clauses *) (* clauses *)
@ -296,9 +291,9 @@ module Make (Plugin : PLUGIN) = struct
(** Make a clause with the given atoms *) (** Make a clause with the given atoms *)
val make_a : store -> removable:bool -> atom array -> proof_step -> t val make_a : store -> removable:bool -> atom array -> Proof_step.id -> t
val make_l : store -> removable:bool -> atom list -> proof_step -> t val make_l : store -> removable:bool -> atom list -> Proof_step.id -> t
val make_vec : store -> removable:bool -> atom Vec.t -> proof_step -> t val make_vec : store -> removable:bool -> atom Vec.t -> Proof_step.id -> t
val n_atoms : store -> t -> int val n_atoms : store -> t -> int
val marked : store -> t -> bool val marked : store -> t -> bool
val set_marked : store -> t -> bool -> unit val set_marked : store -> t -> bool -> unit
@ -312,8 +307,8 @@ module Make (Plugin : PLUGIN) = struct
val dealloc : store -> t -> unit val dealloc : store -> t -> unit
(** Delete the clause *) (** Delete the clause *)
val set_proof_step : store -> t -> proof_step -> unit val set_proof_step : store -> t -> Proof_step.id -> unit
val proof_step : store -> t -> proof_step val proof_step : store -> t -> Proof_step.id
val activity : store -> t -> float val activity : store -> t -> float
val set_activity : store -> t -> float -> unit val set_activity : store -> t -> float -> unit
val iter : store -> f:(atom -> unit) -> t -> unit val iter : store -> f:(atom -> unit) -> t -> unit
@ -321,9 +316,9 @@ module Make (Plugin : PLUGIN) = struct
val for_all : store -> f:(atom -> bool) -> t -> bool val for_all : store -> f:(atom -> bool) -> t -> bool
val exists : store -> f:(atom -> bool) -> t -> bool val exists : store -> f:(atom -> bool) -> t -> bool
val atoms_a : store -> t -> atom array val atoms_a : store -> t -> atom array
val lits_l : store -> t -> lit list val lits_l : store -> t -> Lit.t list
val lits_a : store -> t -> lit array val lits_a : store -> t -> Lit.t array
val lits_iter : store -> t -> lit Iter.t val lits_iter : store -> t -> Lit.t Iter.t
val short_name : store -> t -> string val short_name : store -> t -> string
val pp : store -> Format.formatter -> t -> unit val pp : store -> Format.formatter -> t -> unit
val debug : store -> Format.formatter -> t -> unit val debug : store -> Format.formatter -> t -> unit
@ -485,15 +480,15 @@ module Make (Plugin : PLUGIN) = struct
let[@inline] atoms_a store c : atom array = let[@inline] atoms_a store c : atom array =
Vec.get store.c_store.c_lits (c : t :> int) Vec.get store.c_store.c_lits (c : t :> int)
let lits_l store c : lit list = let lits_l store c : Lit.t list =
let arr = atoms_a store c in let arr = atoms_a store c in
Util.array_to_list_map (Atom.lit store) arr Util.array_to_list_map (Atom.lit store) arr
let lits_a store c : lit array = let lits_a store c : Lit.t array =
let arr = atoms_a store c in let arr = atoms_a store c in
Array.map (Atom.lit store) arr Array.map (Atom.lit store) arr
let lits_iter store c : lit Iter.t = let lits_iter store c : Lit.t Iter.t =
let arr = atoms_a store c in let arr = atoms_a store c in
Iter.of_array arr |> Iter.map (Atom.lit store) Iter.of_array arr |> Iter.map (Atom.lit store)
@ -512,7 +507,8 @@ module Make (Plugin : PLUGIN) = struct
end end
(* allocate new variable *) (* allocate new variable *)
let alloc_var_uncached_ ?default_pol:(pol = true) self (form : lit) : var = let alloc_var_uncached_ ?default_pol:(pol = true) self (form : Lit.t) : var
=
let { let {
v_count; v_count;
v_of_lit; v_of_lit;
@ -560,7 +556,7 @@ module Make (Plugin : PLUGIN) = struct
v v
(* create new variable *) (* create new variable *)
let alloc_var (self : t) ?default_pol (lit : lit) : let alloc_var (self : t) ?default_pol (lit : Lit.t) :
var * Solver_intf.same_sign = var * Solver_intf.same_sign =
let lit, same_sign = Lit.norm_sign lit in let lit, same_sign = Lit.norm_sign lit in
try Lit_tbl.find self.v_of_lit lit, same_sign try Lit_tbl.find self.v_of_lit lit, same_sign
@ -882,9 +878,9 @@ module Make (Plugin : PLUGIN) = struct
mutable clause_incr: float; (* increment for clauses' activity *) mutable clause_incr: float; (* increment for clauses' activity *)
(* FIXME: use event *) (* FIXME: use event *)
on_conflict: (Clause.t, unit) Event.Emitter.t; on_conflict: (Clause.t, unit) Event.Emitter.t;
on_decision: (lit, unit) Event.Emitter.t; on_decision: (Lit.t, unit) Event.Emitter.t;
on_learnt: (Clause.t, unit) Event.Emitter.t; on_learnt: (Clause.t, unit) Event.Emitter.t;
on_gc: (lit array, unit) Event.Emitter.t; on_gc: (Lit.t array, unit) Event.Emitter.t;
stat: Stat.t; stat: Stat.t;
n_conflicts: int Stat.counter; n_conflicts: int Stat.counter;
n_propagations: int Stat.counter; n_propagations: int Stat.counter;
@ -975,11 +971,11 @@ module Make (Plugin : PLUGIN) = struct
let[@inline] insert_var_order st (v : var) : unit = H.insert st.order v let[@inline] insert_var_order st (v : var) : unit = H.insert st.order v
(* find atom for the lit, if any *) (* find atom for the lit, if any *)
let[@inline] find_atom_ (self : t) (p : lit) : atom option = let[@inline] find_atom_ (self : t) (p : Lit.t) : atom option =
Store.find_atom self.store p Store.find_atom self.store p
(* create a new atom, pushing it into the decision queue if needed *) (* create a new atom, pushing it into the decision queue if needed *)
let make_atom_ (self : t) ?default_pol (p : lit) : atom = let make_atom_ (self : t) ?default_pol (p : Lit.t) : atom =
let a = Store.alloc_atom self.store ?default_pol p in let a = Store.alloc_atom self.store ?default_pol p in
if Atom.level self.store a < 0 then if Atom.level self.store a < 0 then
insert_var_order self (Atom.var a) insert_var_order self (Atom.var a)
@ -1041,7 +1037,7 @@ module Make (Plugin : PLUGIN) = struct
(* get/build the proof for [a], which must be an atom true at level 0. (* get/build the proof for [a], which must be an atom true at level 0.
This uses a global cache to avoid repeated computations, as many clauses This uses a global cache to avoid repeated computations, as many clauses
might resolve against a given 0-level atom. *) might resolve against a given 0-level atom. *)
let rec proof_of_atom_lvl0_ (self : t) (a : atom) : proof_step = let rec proof_of_atom_lvl0_ (self : t) (a : atom) : Proof_step.id =
assert (Atom.is_true self.store a && Atom.level self.store a = 0); assert (Atom.is_true self.store a && Atom.level self.store a = 0);
match Atom.proof_lvl0 self.store a with match Atom.proof_lvl0 self.store a with
@ -1075,7 +1071,7 @@ module Make (Plugin : PLUGIN) = struct
proof_c2 proof_c2
else else
Proof_trace.add_step self.proof Proof_trace.add_step self.proof
@@ Proof_rules.sat_redundant_clause @@ Proof_sat.sat_redundant_clause
(Iter.return (Atom.lit self.store a)) (Iter.return (Atom.lit self.store a))
~hyps:Iter.(cons proof_c2 (of_list !steps)) ~hyps:Iter.(cons proof_c2 (of_list !steps))
in in
@ -1168,7 +1164,7 @@ module Make (Plugin : PLUGIN) = struct
let proof = let proof =
let lits = Iter.of_array atoms |> Iter.map (Atom.lit store) in let lits = Iter.of_array atoms |> Iter.map (Atom.lit store) in
Proof_trace.add_step self.proof Proof_trace.add_step self.proof
@@ Proof_rules.sat_redundant_clause lits @@ Proof_sat.sat_redundant_clause lits
~hyps: ~hyps:
Iter.( Iter.(
cons (Clause.proof_step self.store c) (of_list !res0_proofs)) cons (Clause.proof_step self.store c) (of_list !res0_proofs))
@ -1282,7 +1278,7 @@ module Make (Plugin : PLUGIN) = struct
let p_empty = let p_empty =
Proof_trace.add_step self.proof Proof_trace.add_step self.proof
@@ Proof_rules.sat_redundant_clause Iter.empty @@ Proof_sat.sat_redundant_clause Iter.empty
~hyps:(Step_vec.to_iter pvec) ~hyps:(Step_vec.to_iter pvec)
in in
Step_vec.clear pvec; Step_vec.clear pvec;
@ -1643,7 +1639,7 @@ module Make (Plugin : PLUGIN) = struct
let p = let p =
Proof_trace.add_step self.proof Proof_trace.add_step self.proof
@@ Proof_rules.sat_redundant_clause @@ Proof_sat.sat_redundant_clause
(Iter.of_array cr.cr_learnt |> Iter.map (Atom.lit self.store)) (Iter.of_array cr.cr_learnt |> Iter.map (Atom.lit self.store))
~hyps:(Step_vec.to_iter cr.cr_steps) ~hyps:(Step_vec.to_iter cr.cr_steps)
in in
@ -1660,7 +1656,7 @@ module Make (Plugin : PLUGIN) = struct
let fuip = cr.cr_learnt.(0) in let fuip = cr.cr_learnt.(0) in
let p = let p =
Proof_trace.add_step self.proof Proof_trace.add_step self.proof
@@ Proof_rules.sat_redundant_clause @@ Proof_sat.sat_redundant_clause
(Iter.of_array cr.cr_learnt |> Iter.map (Atom.lit self.store)) (Iter.of_array cr.cr_learnt |> Iter.map (Atom.lit self.store))
~hyps:(Step_vec.to_iter cr.cr_steps) ~hyps:(Step_vec.to_iter cr.cr_steps)
in in
@ -1842,8 +1838,8 @@ module Make (Plugin : PLUGIN) = struct
let[@inline] slice_get st i = AVec.get st.trail i let[@inline] slice_get st i = AVec.get st.trail i
let acts_add_clause self ?(keep = false) (l : lit list) (p : proof_step) : let acts_add_clause self ?(keep = false) (l : Lit.t list) (p : Proof_step.id)
unit = : unit =
let atoms = List.rev_map (make_atom_ self) l in let atoms = List.rev_map (make_atom_ self) l in
let removable = not keep in let removable = not keep in
let c = Clause.make_l self.store ~removable atoms p in let c = Clause.make_l self.store ~removable atoms p in
@ -1852,8 +1848,8 @@ module Make (Plugin : PLUGIN) = struct
(* will be added later, even if we backtrack *) (* will be added later, even if we backtrack *)
Delayed_actions.add_clause_learnt self.delayed_actions c Delayed_actions.add_clause_learnt self.delayed_actions c
let acts_add_clause_in_pool self ~pool (l : lit list) (p : proof_step) : unit let acts_add_clause_in_pool self ~pool (l : Lit.t list) (p : Proof_step.id) :
= unit =
let atoms = List.rev_map (make_atom_ self) l in let atoms = List.rev_map (make_atom_ self) l in
let removable = true in let removable = true in
let c = Clause.make_l self.store ~removable atoms p in let c = Clause.make_l self.store ~removable atoms p in
@ -1864,7 +1860,7 @@ module Make (Plugin : PLUGIN) = struct
(* will be added later, even if we backtrack *) (* will be added later, even if we backtrack *)
Delayed_actions.add_clause_pool self.delayed_actions c pool Delayed_actions.add_clause_pool self.delayed_actions c pool
let acts_add_decision_lit (self : t) (f : lit) (sign : bool) : unit = let acts_add_decision_lit (self : t) (f : Lit.t) (sign : bool) : unit =
let store = self.store in let store = self.store in
let a = make_atom_ self f in let a = make_atom_ self f in
let a = let a =
@ -1879,7 +1875,7 @@ module Make (Plugin : PLUGIN) = struct
Delayed_actions.add_decision self.delayed_actions a Delayed_actions.add_decision self.delayed_actions a
) )
let acts_raise self (l : lit list) (p : proof_step) : 'a = let acts_raise self (l : Lit.t list) (p : Proof_step.id) : 'a =
let atoms = List.rev_map (make_atom_ self) l in let atoms = List.rev_map (make_atom_ self) l in
(* conflicts can be removed *) (* conflicts can be removed *)
let c = Clause.make_l self.store ~removable:true atoms p in let c = Clause.make_l self.store ~removable:true atoms p in
@ -1903,7 +1899,7 @@ module Make (Plugin : PLUGIN) = struct
(Atom.debug store) (Atom.neg a) (Atom.debug store) (Atom.neg a)
| exception Not_found -> () | exception Not_found -> ()
let acts_propagate (self : t) f (expl : (_, proof_step) Solver_intf.reason) = let acts_propagate (self : t) f (expl : Solver_intf.reason) =
let store = self.store in let store = self.store in
match expl with match expl with
| Solver_intf.Consequence mk_expl -> | Solver_intf.Consequence mk_expl ->
@ -1994,19 +1990,15 @@ module Make (Plugin : PLUGIN) = struct
else else
Solver_intf.L_undefined Solver_intf.L_undefined
let[@inline] acts_eval_lit self (f : lit) : Solver_intf.lbool = let[@inline] acts_eval_lit self (f : Lit.t) : Solver_intf.lbool =
let a = make_atom_ self f in let a = make_atom_ self f in
eval_atom_ self a eval_atom_ self a
let[@inline] acts_add_lit self ?default_pol f : unit = let[@inline] acts_add_lit self ?default_pol f : unit =
ignore (make_atom_ ?default_pol self f : atom) ignore (make_atom_ ?default_pol self f : atom)
let[@inline] current_slice st : _ Solver_intf.acts = let[@inline] current_slice st : Solver_intf.acts =
let module M = struct let module M = struct
type nonrec proof = Proof_trace.t
type nonrec proof_step = proof_step
type nonrec lit = lit
let proof = st.proof let proof = st.proof
let iter_assumptions = acts_iter st ~full:false st.th_head let iter_assumptions = acts_iter st ~full:false st.th_head
let eval_lit = acts_eval_lit st let eval_lit = acts_eval_lit st
@ -2019,12 +2011,8 @@ module Make (Plugin : PLUGIN) = struct
(module M) (module M)
(* full slice, for [if_sat] final check *) (* full slice, for [if_sat] final check *)
let[@inline] full_slice st : _ Solver_intf.acts = let[@inline] full_slice st : Solver_intf.acts =
let module M = struct let module M = struct
type nonrec proof = Proof_trace.t
type nonrec proof_step = proof_step
type nonrec lit = lit
let proof = st.proof let proof = st.proof
let iter_assumptions = acts_iter st ~full:true st.th_head let iter_assumptions = acts_iter st ~full:true st.th_head
let eval_lit = acts_eval_lit st let eval_lit = acts_eval_lit st
@ -2403,7 +2391,7 @@ module Make (Plugin : PLUGIN) = struct
let atoms = Util.array_of_list_map (make_atom_ self) l in let atoms = Util.array_of_list_map (make_atom_ self) l in
let proof = let proof =
Proof_trace.add_step self.proof Proof_trace.add_step self.proof
@@ Proof_rules.sat_input_clause (Iter.of_list l) @@ Proof_sat.sat_input_clause (Iter.of_list l)
in in
let c = Clause.make_a self.store ~removable:false atoms proof in let c = Clause.make_a self.store ~removable:false atoms proof in
Log.debugf 10 (fun k -> Log.debugf 10 (fun k ->
@ -2419,14 +2407,14 @@ module Make (Plugin : PLUGIN) = struct
let[@inline] add_lit self ?default_pol lit = let[@inline] add_lit self ?default_pol lit =
ignore (make_atom_ self lit ?default_pol : atom) ignore (make_atom_ self lit ?default_pol : atom)
let[@inline] set_default_pol (self : t) (lit : lit) (pol : bool) : unit = let[@inline] set_default_pol (self : t) (lit : Lit.t) (pol : bool) : unit =
let a = make_atom_ self lit ~default_pol:pol in let a = make_atom_ self lit ~default_pol:pol in
Var.set_default_pol self.store (Atom.var a) pol Var.set_default_pol self.store (Atom.var a) pol
(* Result type *) (* Result type *)
type res = type res =
| Sat of Lit.t Solver_intf.sat_state | Sat of Solver_intf.sat_state
| Unsat of (lit, clause, proof_step) Solver_intf.unsat_state | Unsat of clause Solver_intf.unsat_state
let pp_all self lvl status = let pp_all self lvl status =
Log.debugf lvl (fun k -> Log.debugf lvl (fun k ->
@ -2447,7 +2435,7 @@ module Make (Plugin : PLUGIN) = struct
(Util.pp_iter @@ Clause.debug self.store) (Util.pp_iter @@ Clause.debug self.store)
(cp_to_iter_ self.clauses_learnt)) (cp_to_iter_ self.clauses_learnt))
let mk_sat (self : t) : Lit.t Solver_intf.sat_state = let mk_sat (self : t) : Solver_intf.sat_state =
pp_all self 99 "SAT"; pp_all self 99 "SAT";
let t = self.trail in let t = self.trail in
let module M = struct let module M = struct
@ -2495,7 +2483,7 @@ module Make (Plugin : PLUGIN) = struct
let lits = Iter.of_list !res |> Iter.map (Atom.lit self.store) in let lits = Iter.of_list !res |> Iter.map (Atom.lit self.store) in
let hyps = Iter.of_list (Clause.proof_step self.store c :: !lvl0) in let hyps = Iter.of_list (Clause.proof_step self.store c :: !lvl0) in
Proof_trace.add_step self.proof Proof_trace.add_step self.proof
@@ Proof_rules.sat_redundant_clause lits ~hyps @@ Proof_sat.sat_redundant_clause lits ~hyps
in in
Clause.make_l self.store ~removable:false !res proof Clause.make_l self.store ~removable:false !res proof
) )
@ -2530,16 +2518,13 @@ module Make (Plugin : PLUGIN) = struct
assert (Atom.equal first @@ List.hd core); assert (Atom.equal first @@ List.hd core);
let proof = let proof =
let lits = Iter.of_list core |> Iter.map (Atom.lit self.store) in let lits = Iter.of_list core |> Iter.map (Atom.lit self.store) in
Proof_trace.add_step self.proof Proof_trace.add_step self.proof @@ Proof_sat.sat_unsat_core lits
@@ Proof_rules.sat_unsat_core lits
in in
Clause.make_l self.store ~removable:false [] proof) Clause.make_l self.store ~removable:false [] proof)
in in
fun () -> Lazy.force c fun () -> Lazy.force c
in in
let module M = struct let module M = struct
type nonrec lit = lit
type nonrec proof_step = proof_step
type clause = Clause.t type clause = Clause.t
let unsat_conflict = unsat_conflict let unsat_conflict = unsat_conflict
@ -2554,7 +2539,7 @@ module Make (Plugin : PLUGIN) = struct
type propagation_result = type propagation_result =
| PR_sat | PR_sat
| PR_conflict of { backtracked: int } | PR_conflict of { backtracked: int }
| PR_unsat of (lit, clause, proof_step) Solver_intf.unsat_state | PR_unsat of clause Solver_intf.unsat_state
(* decide on assumptions, and do propagations, but no other kind of decision *) (* decide on assumptions, and do propagations, but no other kind of decision *)
let propagate_under_assumptions (self : t) : propagation_result = let propagate_under_assumptions (self : t) : propagation_result =
@ -2591,8 +2576,8 @@ module Make (Plugin : PLUGIN) = struct
assert false assert false
with Exit -> !result with Exit -> !result
let add_clause_atoms_ self ~pool ~removable (c : atom array) (pr : proof_step) let add_clause_atoms_ self ~pool ~removable (c : atom array)
: unit = (pr : Proof_step.id) : unit =
try try
let c = Clause.make_a self.store ~removable c pr in let c = Clause.make_a self.store ~removable c pr in
add_clause_ ~pool self c add_clause_ ~pool self c
@ -2602,26 +2587,26 @@ module Make (Plugin : PLUGIN) = struct
let c = Array.map (make_atom_ self) c in let c = Array.map (make_atom_ self) c in
add_clause_atoms_ ~pool:self.clauses_learnt ~removable:false self c pr add_clause_atoms_ ~pool:self.clauses_learnt ~removable:false self c pr
let add_clause self (c : lit list) (pr : proof_step) : unit = let add_clause self (c : Lit.t list) (pr : Proof_step.id) : unit =
let c = Util.array_of_list_map (make_atom_ self) c in let c = Util.array_of_list_map (make_atom_ self) c in
add_clause_atoms_ ~pool:self.clauses_learnt ~removable:false self c pr add_clause_atoms_ ~pool:self.clauses_learnt ~removable:false self c pr
let add_input_clause self (c : lit list) = let add_input_clause self (c : Lit.t list) =
let pr = let pr =
Proof_trace.add_step self.proof Proof_trace.add_step self.proof
@@ Proof_rules.sat_input_clause (Iter.of_list c) @@ Proof_sat.sat_input_clause (Iter.of_list c)
in in
add_clause self c pr add_clause self c pr
let add_input_clause_a self c = let add_input_clause_a self c =
let pr = let pr =
Proof_trace.add_step self.proof Proof_trace.add_step self.proof
@@ Proof_rules.sat_input_clause (Iter.of_array c) @@ Proof_sat.sat_input_clause (Iter.of_array c)
in in
add_clause_a self c pr add_clause_a self c pr
(* run [f()] with additional assumptions *) (* run [f()] with additional assumptions *)
let with_local_assumptions_ (self : t) (assumptions : lit list) f = let with_local_assumptions_ (self : t) (assumptions : Lit.t list) f =
let old_assm_lvl = AVec.size self.assumptions in let old_assm_lvl = AVec.size self.assumptions in
List.iter List.iter
(fun lit -> (fun lit ->
@ -2645,7 +2630,7 @@ module Make (Plugin : PLUGIN) = struct
Sat (mk_sat self) Sat (mk_sat self)
with E_unsat us -> Unsat (mk_unsat self us) with E_unsat us -> Unsat (mk_unsat self us)
let push_assumption (self : t) (lit : lit) : unit = let push_assumption (self : t) (lit : Lit.t) : unit =
let a = make_atom_ self lit in let a = make_atom_ self lit in
AVec.push self.assumptions a AVec.push self.assumptions a
@ -2667,7 +2652,7 @@ module Make (Plugin : PLUGIN) = struct
let us = mk_unsat self us in let us = mk_unsat self us in
PR_unsat us PR_unsat us
let true_at_level0 (self : t) (lit : lit) : bool = let true_at_level0 (self : t) (lit : Lit.t) : bool =
match find_atom_ self lit with match find_atom_ self lit with
| None -> false | None -> false
| Some a -> | Some a ->
@ -2676,7 +2661,7 @@ module Make (Plugin : PLUGIN) = struct
b && lev = 0 b && lev = 0
with UndecidedLit -> false) with UndecidedLit -> false)
let[@inline] eval_lit self (lit : lit) : Solver_intf.lbool = let[@inline] eval_lit self (lit : Lit.t) : Solver_intf.lbool =
match find_atom_ self lit with match find_atom_ self lit with
| Some a -> eval_atom_ self a | Some a -> eval_atom_ self a
| None -> Solver_intf.L_undefined | None -> Solver_intf.L_undefined
@ -2690,11 +2675,7 @@ module Make_cdcl_t (Plugin : Solver_intf.PLUGIN_CDCL_T) = Make (struct
end) end)
[@@inline] [@@specialise] [@@inline] [@@specialise]
module Make_pure_sat (Plugin : Solver_intf.PLUGIN_SAT) = Make (struct module Pure_sat = Make (struct
module Lit = Plugin.Lit
module Proof_trace = Plugin.Proof_trace
module Proof_rules = Plugin.Proof_rules
type t = unit type t = unit
let push_level () = () let push_level () = ()

15
src/sat/Solver.mli
View file

@ -1,16 +1,5 @@
module type S = Solver_intf.S module type S = Solver_intf.S
(** Safe external interface of solvers. *) (** Safe external interface of solvers. *)
module Make_pure_sat (Th : Solver_intf.PLUGIN_SAT) : module Pure_sat : S with type theory = unit
S module Make_cdcl_t (Th : Solver_intf.PLUGIN_CDCL_T) : S with type theory = Th.t
with module Lit = Th.Lit
and module Proof_trace = Th.Proof_trace
and module Proof_rules = Th.Proof_rules
and type theory = unit
module Make_cdcl_t (Th : Solver_intf.PLUGIN_CDCL_T) :
S
with module Lit = Th.Lit
and module Proof_trace = Th.Proof_trace
and module Proof_rules = Th.Proof_rules
and type theory = Th.t

148
src/sat/Solver_intf.ml
View file

@ -11,53 +11,46 @@ Copyright 2016 Guillaume Bury
Copyright 2016 Simon Cruanes Copyright 2016 Simon Cruanes
*) *)
open Sidekick_core
type 'a printer = Format.formatter -> 'a -> unit type 'a printer = Format.formatter -> 'a -> unit
(** Solver in a "SATISFIABLE" state *) (** Solver in a "SATISFIABLE" state *)
module type SAT_STATE = sig module type SAT_STATE = sig
type lit val eval : Lit.t -> bool
(** Literals (signed boolean atoms) *)
val eval : lit -> bool
(** Returns the valuation of a lit in the current state (** Returns the valuation of a lit in the current state
of the sat solver. of the sat solver.
@raise UndecidedLit if the literal is not decided *) @raise UndecidedLit if the literal is not decided *)
val eval_level : lit -> bool * int val eval_level : Lit.t -> bool * int
(** Return the current assignement of the literals, as well as its (** Return the current assignement of the literals, as well as its
decision level. If the level is 0, then it is necessary for decision level. If the level is 0, then it is necessary for
the literal to have this value; otherwise it is due to choices the literal to have this value; otherwise it is due to choices
that can potentially be backtracked. that can potentially be backtracked.
@raise UndecidedLit if the literal is not decided *) @raise UndecidedLit if the literal is not decided *)
val iter_trail : (lit -> unit) -> unit val iter_trail : (Lit.t -> unit) -> unit
(** Iter through the lits in order of decision/propagation (** Iter through the lits in order of decision/propagation
(starting from the first propagation, to the last propagation). *) (starting from the first propagation, to the last propagation). *)
end end
type 'form sat_state = (module SAT_STATE with type lit = 'form) type sat_state = (module SAT_STATE)
(** The type of values returned when the solver reaches a SAT state. *) (** The type of values returned when the solver reaches a SAT state. *)
(** Solver in an "UNSATISFIABLE" state *) (** Solver in an "UNSATISFIABLE" state *)
module type UNSAT_STATE = sig module type UNSAT_STATE = sig
type lit
type clause type clause
type proof_step
val unsat_conflict : unit -> clause val unsat_conflict : unit -> clause
(** Returns the unsat clause found at the toplevel *) (** Returns the unsat clause found at the toplevel *)
val unsat_assumptions : unit -> lit Iter.t val unsat_assumptions : unit -> Lit.t Iter.t
(** Subset of assumptions responsible for "unsat" *) (** Subset of assumptions responsible for "unsat" *)
val unsat_proof : unit -> proof_step val unsat_proof : unit -> Proof_term.step_id
end end
type ('lit, 'clause, 'proof_step) unsat_state = type 'clause unsat_state = (module UNSAT_STATE with type clause = 'clause)
(module UNSAT_STATE
with type lit = 'lit
and type clause = 'clause
and type proof_step = 'proof_step)
(** The type of values returned when the solver reaches an UNSAT state. *) (** The type of values returned when the solver reaches an UNSAT state. *)
type same_sign = bool type same_sign = bool
@ -65,9 +58,7 @@ type same_sign = bool
[true] means the literal stayed the same, [false] that its sign was flipped. *) [true] means the literal stayed the same, [false] that its sign was flipped. *)
(** The type of reasons for propagations of a lit [f]. *) (** The type of reasons for propagations of a lit [f]. *)
type ('lit, 'proof_step) reason = type reason = Consequence of (unit -> Lit.t list * Proof_step.id) [@@unboxed]
| Consequence of (unit -> 'lit list * 'proof_step)
[@@unboxed]
(** [Consequence (l, p)] means that the lits in [l] imply the propagated (** [Consequence (l, p)] means that the lits in [l] imply the propagated
lit [f]. The proof should be a proof of the clause "[l] implies [f]". lit [f]. The proof should be a proof of the clause "[l] implies [f]".
@ -95,23 +86,19 @@ type lbool = L_true | L_false | L_undefined (** Valuation of an atom *)
are provided with a [(module ACTS)] so they can modify the SAT solver are provided with a [(module ACTS)] so they can modify the SAT solver
by adding new lemmas, raise conflicts, etc. *) by adding new lemmas, raise conflicts, etc. *)
module type ACTS = sig module type ACTS = sig
type lit val proof : Proof_trace.t
type proof
type proof_step
val proof : proof val iter_assumptions : (Lit.t -> unit) -> unit
val iter_assumptions : (lit -> unit) -> unit
(** Traverse the new assumptions on the boolean trail. *) (** Traverse the new assumptions on the boolean trail. *)
val eval_lit : lit -> lbool val eval_lit : Lit.t -> lbool
(** Obtain current value of the given literal *) (** Obtain current value of the given literal *)
val add_lit : ?default_pol:bool -> lit -> unit val add_lit : ?default_pol:bool -> Lit.t -> unit
(** Map the given lit to an internal atom, which will be decided by the (** Map the given lit to an internal atom, which will be decided by the
SAT solver. *) SAT solver. *)
val add_clause : ?keep:bool -> lit list -> proof_step -> unit val add_clause : ?keep:bool -> Lit.t list -> Proof_step.id -> unit
(** Add a clause to the solver. (** Add a clause to the solver.
@param keep if true, the clause will be kept by 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 Otherwise the solver is allowed to GC the clause and propose this
@ -119,26 +106,22 @@ module type ACTS = sig
- [C_use_allocator alloc] puts the clause in the given allocator. - [C_use_allocator alloc] puts the clause in the given allocator.
*) *)
val raise_conflict : lit list -> proof_step -> 'b val raise_conflict : Lit.t list -> Proof_step.id -> 'b
(** Raise a conflict, yielding control back to the solver. (** Raise a conflict, yielding control back to the solver.
The list of atoms must be a valid theory lemma that is false in the The list of atoms must be a valid theory lemma that is false in the
current trail. *) current trail. *)
val propagate : lit -> (lit, proof_step) reason -> unit val propagate : Lit.t -> reason -> unit
(** Propagate a lit, i.e. the theory can evaluate the lit to be true (** Propagate a lit, i.e. the theory can evaluate the lit to be true
(see the definition of {!type:eval_res} *) (see the definition of {!type:eval_res} *)
val add_decision_lit : lit -> bool -> unit val add_decision_lit : Lit.t -> bool -> unit
(** Ask the SAT solver to decide on the given lit with given sign (** Ask the SAT solver to decide on the given lit with given sign
before it can answer [SAT]. The order of decisions is still unspecified. before it can answer [SAT]. The order of decisions is still unspecified.
Useful for theory combination. This will be undone on backtracking. *) Useful for theory combination. This will be undone on backtracking. *)
end end
type ('lit, 'proof, 'proof_step) acts = type acts = (module ACTS)
(module ACTS
with type lit = 'lit
and type proof = 'proof
and type proof_step = 'proof_step)
(** The type for a slice of assertions to assume/propagate in the theory. *) (** The type for a slice of assertions to assume/propagate in the theory. *)
exception No_proof exception No_proof
@ -169,77 +152,39 @@ module type LIT = sig
but one returns [false] and the other [true]. *) but one returns [false] and the other [true]. *)
end end
module type PROOF_RULES = Sidekick_sigs_proof_sat.S
(** Signature for theories to be given to the CDCL(T) solver *) (** Signature for theories to be given to the CDCL(T) solver *)
module type PLUGIN_CDCL_T = sig module type PLUGIN_CDCL_T = sig
type t type t
(** The plugin state itself *) (** The plugin state itself *)
module Lit : LIT
module Proof_trace : Sidekick_sigs_proof_trace.S
module Proof_rules :
PROOF_RULES
with type lit = Lit.t
and type rule = Proof_trace.A.rule
and type step_id = Proof_trace.A.step_id
val push_level : t -> unit val push_level : t -> unit
(** Create a new backtrack level *) (** Create a new backtrack level *)
val pop_levels : t -> int -> unit val pop_levels : t -> int -> unit
(** Pop [n] levels of the theory *) (** Pop [n] levels of the theory *)
val partial_check : val partial_check : t -> acts -> unit
t -> (Lit.t, Proof_trace.t, Proof_trace.A.step_id) acts -> unit
(** Assume the lits in the slice, possibly using the [slice] (** Assume the lits in the slice, possibly using the [slice]
to push new lits to be propagated or to raising a conflict or to add to push new lits to be propagated or to raising a conflict or to add
new lemmas. *) new lemmas. *)
val final_check : val final_check : t -> acts -> unit
t -> (Lit.t, Proof_trace.t, Proof_trace.A.step_id) acts -> unit
(** Called at the end of the search in case a model has been found. (** 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 no new clause is pushed, then proof search ends and "sat" is returned;
if lemmas are added, search is resumed; if lemmas are added, search is resumed;
if a conflict clause is added, search backtracks and then resumes. *) if a conflict clause is added, search backtracks and then resumes. *)
end end
(** Signature for pure SAT solvers *)
module type PLUGIN_SAT = sig
module Lit : LIT
module Proof_trace : Sidekick_sigs_proof_trace.S
module Proof_rules :
PROOF_RULES
with type lit = Lit.t
and type rule = Proof_trace.A.rule
and type step_id = Proof_trace.A.step_id
end
exception Resource_exhausted exception Resource_exhausted
(** Can be raised in a progress handler *) (** Can be raised in a progress handler *)
(** The external interface implemented by safe solvers, such as the one (** The external interface implemented by safe solvers, such as the one
created by the {!Solver.Make} and {!Mcsolver.Make} functors. *) created by the {!Solver.Make} and {!Mcsolver.Make} functors. *)
module type S = sig module type S = sig
(** {2 Internal modules}
These are the internal modules used, you should probably not use them
if you're not familiar with the internals of mSAT. *)
module Lit : LIT
module Proof_trace : Sidekick_sigs_proof_trace.S
type lit = Lit.t
(** literals *) (** literals *)
type clause type clause
type theory type theory
type proof_rule = Proof_trace.A.rule
type proof_step = Proof_trace.A.step_id
type proof_trace = Proof_trace.t
(** A representation of a full proof *)
type solver type solver
(** The main solver type. *) (** The main solver type. *)
@ -262,23 +207,16 @@ module type S = sig
val n_atoms : store -> t -> int val n_atoms : store -> t -> int
val lits_iter : store -> t -> lit Iter.t val lits_iter : store -> t -> Lit.t Iter.t
(** Literals of a clause *) (** Literals of a clause *)
val lits_a : store -> t -> lit array val lits_a : store -> t -> Lit.t array
(** Atoms of a clause *) (** Atoms of a clause *)
val lits_l : store -> t -> lit list val lits_l : store -> t -> Lit.t list
(** List of atoms of a clause *) (** List of atoms of a clause *)
end end
(** Proof rules for SAT solving *)
module Proof_rules :
PROOF_RULES
with type lit = lit
and type rule = proof_rule
and type step_id = proof_step
(** {2 Main Solver Type} *) (** {2 Main Solver Type} *)
type t = solver type t = solver
@ -287,7 +225,7 @@ module type S = sig
val create : val create :
?stat:Stat.t -> ?stat:Stat.t ->
?size:[ `Tiny | `Small | `Big ] -> ?size:[ `Tiny | `Small | `Big ] ->
proof:proof_trace -> proof:Proof_trace.t ->
theory -> theory ->
t t
(** Create new solver (** Create new solver
@ -305,21 +243,21 @@ module type S = sig
val stat : t -> Stat.t val stat : t -> Stat.t
(** Statistics *) (** Statistics *)
val proof : t -> proof_trace val proof : t -> Proof_trace.t
(** Access the inner proof *) (** Access the inner proof *)
val on_conflict : t -> (Clause.t, unit) Event.t val on_conflict : t -> (Clause.t, unit) Event.t
val on_decision : t -> (lit, unit) Event.t val on_decision : t -> (Lit.t, unit) Event.t
val on_learnt : t -> (Clause.t, unit) Event.t val on_learnt : t -> (Clause.t, unit) Event.t
val on_gc : t -> (lit array, unit) Event.t val on_gc : t -> (Lit.t array, unit) Event.t
(** {2 Types} *) (** {2 Types} *)
(** Result type for the solver *) (** Result type for the solver *)
type res = type res =
| Sat of lit sat_state | Sat of sat_state
(** Returned when the solver reaches SAT, with a model *) (** Returned when the solver reaches SAT, with a model *)
| Unsat of (lit, clause, proof_step) unsat_state | Unsat of clause unsat_state
(** Returned when the solver reaches UNSAT, with a proof *) (** Returned when the solver reaches UNSAT, with a proof *)
exception UndecidedLit exception UndecidedLit
@ -328,25 +266,25 @@ module type S = sig
(** {2 Base operations} *) (** {2 Base operations} *)
val assume : t -> lit list list -> unit val assume : t -> Lit.t list list -> unit
(** Add the list of clauses to the current set of assumptions. (** Add the list of clauses to the current set of assumptions.
Modifies the sat solver state in place. *) Modifies the sat solver state in place. *)
val add_clause : t -> lit list -> proof_step -> unit val add_clause : t -> Lit.t list -> Proof_step.id -> unit
(** Lower level addition of clauses *) (** Lower level addition of clauses *)
val add_clause_a : t -> lit array -> proof_step -> unit val add_clause_a : t -> Lit.t array -> Proof_step.id -> unit
(** Lower level addition of clauses *) (** Lower level addition of clauses *)
val add_input_clause : t -> lit list -> unit val add_input_clause : t -> Lit.t list -> unit
(** Like {!add_clause} but with the justification of being an input clause *) (** Like {!add_clause} but with the justification of being an input clause *)
val add_input_clause_a : t -> lit array -> unit val add_input_clause_a : t -> Lit.t array -> unit
(** Like {!add_clause_a} but with justification of being an input clause *) (** Like {!add_clause_a} but with justification of being an input clause *)
(** {2 Solving} *) (** {2 Solving} *)
val solve : ?on_progress:(unit -> unit) -> ?assumptions:lit list -> t -> res val solve : ?on_progress:(unit -> unit) -> ?assumptions:Lit.t list -> t -> res
(** Try and solves the current set of clauses. (** Try and solves the current set of clauses.
@param assumptions additional atomic assumptions to be temporarily added. @param assumptions additional atomic assumptions to be temporarily added.
The assumptions are just used for this call to [solve], they are The assumptions are just used for this call to [solve], they are
@ -360,24 +298,24 @@ module type S = sig
(** {2 Evaluating and adding literals} *) (** {2 Evaluating and adding literals} *)
val add_lit : t -> ?default_pol:bool -> lit -> unit val add_lit : t -> ?default_pol:bool -> Lit.t -> unit
(** Ensure the SAT solver handles this particular literal, ie add (** Ensure the SAT solver handles this particular literal, ie add
a boolean variable for it if it's not already there. *) a boolean variable for it if it's not already there. *)
val set_default_pol : t -> lit -> bool -> unit val set_default_pol : t -> Lit.t -> bool -> unit
(** Set default polarity for the given boolean variable. (** Set default polarity for the given boolean variable.
Sign of the literal is ignored. *) Sign of the literal is ignored. *)
val true_at_level0 : t -> lit -> bool val true_at_level0 : t -> Lit.t -> bool
(** [true_at_level0 a] returns [true] if [a] was proved at level0, i.e. (** [true_at_level0 a] returns [true] if [a] was proved at level0, i.e.
it must hold in all models *) it must hold in all models *)
val eval_lit : t -> lit -> lbool val eval_lit : t -> Lit.t -> lbool
(** Evaluate atom in current state *) (** Evaluate atom in current state *)
(** {2 Assumption stack} *) (** {2 Assumption stack} *)
val push_assumption : t -> lit -> unit val push_assumption : t -> Lit.t -> unit
(** Pushes an assumption onto the assumption stack. It will remain (** Pushes an assumption onto the assumption stack. It will remain
there until it's pop'd by {!pop_assumptions}. *) there until it's pop'd by {!pop_assumptions}. *)
@ -390,10 +328,10 @@ module type S = sig
type propagation_result = type propagation_result =
| PR_sat | PR_sat
| PR_conflict of { backtracked: int } | PR_conflict of { backtracked: int }
| PR_unsat of (lit, clause, proof_step) unsat_state | PR_unsat of clause unsat_state
val check_sat_propagations_only : val check_sat_propagations_only :
?assumptions:lit list -> t -> propagation_result ?assumptions:Lit.t list -> t -> propagation_result
(** [check_sat_propagations_only solver] uses the added clauses (** [check_sat_propagations_only solver] uses the added clauses
and local assumptions (using {!push_assumptions} and [assumptions]) and local assumptions (using {!push_assumptions} and [assumptions])
to quickly assess whether the context is satisfiable. to quickly assess whether the context is satisfiable.

5
src/sat/dune
View file

@ -1,7 +1,6 @@
(library (library
(name sidekick_sat) (name sidekick_sat)
(public_name sidekick.sat) (public_name sidekick.sat)
(libraries iter sidekick.util sidekick.core sidekick.sigs.proof-trace
sidekick.proof-trace.dummy)
(synopsis "Pure OCaml SAT solver implementation for sidekick") (synopsis "Pure OCaml SAT solver implementation for sidekick")
(flags :standard -open Sidekick_util)) (libraries iter sidekick.util sidekick.core)
(flags :standard -w +32 -open Sidekick_util))