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

refactor(sat): hide atoms, API now talks only about literals

Browse source
This commit is contained in:
Simon Cruanes 2021-08-19 09:35:54 -04:00
parent 8bc1f1c864
commit 3fbb9af664
6 changed files with 238 additions and 231 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

8
src/sat/Sidekick_sat.ml
View file

@ -4,7 +4,7 @@
module Solver_intf = Solver_intf
module type S = Solver_intf.S
module type FORMULA = Solver_intf.FORMULA
module type LIT = Solver_intf.LIT
module type PLUGIN_CDCL_T = Solver_intf.PLUGIN_CDCL_T
module type PROOF = Solver_intf.PROOF
@ -13,11 +13,11 @@ type lbool = Solver_intf.lbool = L_true | L_false | L_undefined
module type SAT_STATE = Solver_intf.SAT_STATE
type 'form sat_state = 'form Solver_intf.sat_state
type ('formula, 'proof) reason = ('formula, 'proof) Solver_intf.reason =
| Consequence of (unit -> 'formula list * 'proof) [@@unboxed]
type ('lit, 'proof) reason = ('lit, 'proof) Solver_intf.reason =
| Consequence of (unit -> 'lit list * 'proof) [@@unboxed]
module type ACTS = Solver_intf.ACTS
type ('formula, 'proof) acts = ('formula, 'proof) Solver_intf.acts
type ('lit, 'proof) acts = ('lit, 'proof) Solver_intf.acts
type negated = Solver_intf.negated = Negated | Same_sign

264
src/sat/Solver.ml
View file

@ -33,12 +33,12 @@ end
module Make(Plugin : PLUGIN)
= struct
type formula = Plugin.formula
type lit = Plugin.lit
type theory = Plugin.t
type proof = Plugin.proof
type dproof = proof -> unit
module Formula = Plugin.Formula
module Lit = Plugin.Lit
module Proof = Plugin.Proof
(* ### types ### *)
@ -95,7 +95,7 @@ module Make(Plugin : PLUGIN)
(* ### stores ### *)
module Form_tbl = Hashtbl.Make(Formula)
module Lit_tbl = Hashtbl.Make(Lit)
(* variable/atom store *)
module Store = struct
@ -111,7 +111,7 @@ module Make(Plugin : PLUGIN)
type t = {
(* variables *)
v_of_form: var Form_tbl.t;
v_of_lit: var Lit_tbl.t;
v_level: int Vec.t;
v_heap_idx: int Vec.t;
v_weight: Vec_float.t;
@ -123,7 +123,7 @@ module Make(Plugin : PLUGIN)
(* atoms *)
a_is_true: Bitvec.t;
a_seen: Bitvec.t;
a_form: formula Vec.t;
a_form: lit Vec.t;
(* TODO: store watches in clauses instead *)
a_watched: clause Vec.t Vec.t;
@ -138,7 +138,7 @@ module Make(Plugin : PLUGIN)
| `Small -> 16
| `Big -> 4096
in
{ v_of_form = Form_tbl.create size_map;
{ v_of_lit = Lit_tbl.create size_map;
v_level = Vec.create();
v_heap_idx = Vec.create();
v_weight = Vec_float.create();
@ -188,7 +188,7 @@ module Make(Plugin : PLUGIN)
module Atom = struct
include Atom0
let[@inline] lit self a = Vec.get self.a_form (a:atom:>int)
let formula = lit
let lit = 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] marked self a = Bitvec.get self.a_seen (a:atom:>int)
@ -203,7 +203,7 @@ module Make(Plugin : PLUGIN)
let[@inline] level self a = Var.level self (var a)
let[@inline] marked_both self a = marked self a && marked self (neg a)
let pp self fmt a = Formula.pp fmt (lit self a)
let pp self fmt a = Lit.pp fmt (lit self a)
let pp_a self fmt v =
if Array.length v = 0 then (
@ -242,7 +242,7 @@ module Make(Plugin : PLUGIN)
let debug self out a =
Format.fprintf out "%s%d[%a][atom:@[<hov>%a@]]"
(pp_sign a) (var a:var:>int) (debug_value self) a
Formula.pp (lit self a)
Lit.pp (lit self a)
let debug_a self out vec =
Array.iter (fun a -> Format.fprintf out "@[%a@]@ " (debug self) a) vec
@ -282,8 +282,10 @@ module Make(Plugin : PLUGIN)
val exists : store -> f:(atom -> bool) -> t -> bool
val atoms_a : store -> t -> atom array
val atoms_l : store -> t -> atom list (* allocates *)
val atoms_iter : store -> t -> atom Iter.t
val lits_l : store -> t -> lit list
val lits_a : store -> t -> lit array
val lits_iter : store -> t -> lit Iter.t
val short_name : store -> t -> string
val pp : store -> Format.formatter -> t -> unit
@ -400,8 +402,18 @@ module Make(Plugin : PLUGIN)
let[@inline] atoms_a store c : atom array =
Vec.get store.c_store.c_lits (c:t:>int)
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 lits_l store c : lit list =
let arr = atoms_a store c in
Util.array_to_list_map (Atom.lit store) arr
let lits_a store c : lit array =
let arr = atoms_a store c in
Array.map (Atom.lit store) arr
let lits_iter store c : lit Iter.t =
let arr = atoms_a store c in
Iter.of_array arr |> Iter.map (Atom.lit store)
let short_name _store c = Printf.sprintf "cl[%d]" (c:t:>int)
@ -418,8 +430,8 @@ module Make(Plugin : PLUGIN)
end
(* allocate new variable *)
let alloc_var_uncached_ ?default_pol:(pol=true) self (form:formula) : var =
let {v_count; v_of_form; v_level; v_heap_idx; v_weight;
let alloc_var_uncached_ ?default_pol:(pol=true) self (form:lit) : var =
let {v_count; v_of_lit; v_level; v_heap_idx; v_weight;
v_reason; v_seen; v_default_polarity;
a_is_true; a_seen; a_watched; a_form; c_store=_;
} = self in
@ -428,7 +440,7 @@ module Make(Plugin : PLUGIN)
let v = Var.of_int_unsafe v_idx in
self.v_count <- 1 + v_idx;
Form_tbl.add v_of_form form v;
Lit_tbl.add v_of_lit form v;
Vec.push v_level (-1);
Vec.push v_heap_idx (-1);
Vec.push v_reason None;
@ -442,18 +454,18 @@ module Make(Plugin : PLUGIN)
Bitvec.ensure_size a_seen (2*(v:var:>int));
Vec.push a_form form;
Vec.push a_watched (Vec.create());
Vec.push a_form (Formula.neg form);
Vec.push a_form (Lit.neg form);
Vec.push a_watched (Vec.create());
assert (Vec.get a_form (Atom.of_var v:atom:>int) == form);
v
(* create new variable *)
let alloc_var (self:t) ?default_pol (t:formula) : var * Solver_intf.negated =
let form, negated = Formula.norm t in
try Form_tbl.find self.v_of_form form, negated
let alloc_var (self:t) ?default_pol (lit:lit) : var * Solver_intf.negated =
let lit, negated = Lit.norm lit in
try Lit_tbl.find self.v_of_lit lit, negated
with Not_found ->
let v = alloc_var_uncached_ ?default_pol self form in
let v = alloc_var_uncached_ ?default_pol self lit in
v, negated
let clear_var (self:t) (v:var) : unit =
@ -462,11 +474,20 @@ module Make(Plugin : PLUGIN)
Atom.unmark self (Atom.na v);
()
let atom_of_var_ v negated : atom =
match negated with
| Solver_intf.Same_sign -> Atom.pa v
| Solver_intf.Negated -> Atom.na v
let alloc_atom (self:t) ?default_pol lit : atom =
let var, negated = alloc_var self ?default_pol lit in
match negated with
| Solver_intf.Same_sign -> Atom.pa var
| Solver_intf.Negated -> Atom.na var
atom_of_var_ var negated
let find_atom (self:t) lit : atom option =
let lit, negated = Lit.norm lit in
match Lit_tbl.find self.v_of_lit lit with
| v -> Some (atom_of_var_ v negated)
| exception Not_found -> None
end
type store = Store.t
@ -585,11 +606,10 @@ module Make(Plugin : PLUGIN)
mutable clause_incr : float;
(* increment for clauses' activity *)
mutable on_conflict : (t -> atom array -> unit) option;
mutable on_decision : (t -> atom -> unit) option;
mutable on_new_atom: (t -> atom -> unit) option;
mutable on_learnt : (t -> atom array -> unit) option;
mutable on_gc : (t -> atom array -> unit) option;
mutable on_conflict : (t -> Clause.t -> unit) option;
mutable on_decision : (t -> lit -> unit) option;
mutable on_learnt : (t -> Clause.t -> unit) option;
mutable on_gc : (t -> lit array -> unit) option;
mutable n_conflicts : int;
mutable n_propagations : int;
@ -642,18 +662,16 @@ module Make(Plugin : PLUGIN)
on_conflict = None;
on_decision= None;
on_new_atom = None;
on_learnt = None;
on_gc = None;
}
let create
?on_conflict ?on_decision ?on_new_atom ?on_learnt ?on_gc
?on_conflict ?on_decision ?on_learnt ?on_gc
?(size=`Big) ~proof
(th:theory) : t =
let store = Store.create ~size () 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;
self.on_learnt <- on_learnt;
@ -682,12 +700,15 @@ module Make(Plugin : PLUGIN)
let[@inline] insert_var_order st (v:var) : unit =
H.insert st.order v
(* find atom for the lit, if any *)
let[@inline] find_atom_ (self:t) (p:lit) : atom option =
Store.find_atom self.store p
(* create a new atom, pushing it into the decision queue if needed *)
let make_atom (self:t) ?default_pol (p:formula) : atom =
let make_atom_ (self:t) ?default_pol (p:lit) : atom =
let a = Store.alloc_atom self.store ?default_pol p in
if Atom.level self.store a < 0 then (
insert_var_order self (Atom.var a);
(match self.on_new_atom with Some f -> f self a | None -> ());
) else (
assert (Atom.is_true self.store a || Atom.is_false self.store a);
);
@ -911,7 +932,7 @@ module Make(Plugin : PLUGIN)
let us = match us with
| US_false c ->
self.unsat_at_0 <- Some c;
(match self.on_learnt with Some f -> f self (Clause.atoms_a self.store c) | None -> ());
(match self.on_learnt with Some f -> f self c | None -> ());
US_false c
| _ -> us
in
@ -920,8 +941,8 @@ module Make(Plugin : PLUGIN)
(* TODO: remove when we use DRUP *)
(* Simplification of boolean propagation reasons.
When doing boolean propagation *at level 0*, it can happen
that the clause cl, which propagates a formula, also contains
other formulas, but has been simplified. in which case, we
that the clause cl, which propagates a lit, also contains
other lits, but has been simplified. in which case, we
need to rebuild a clause with correct history, in order to
be able to build a correct proof at the end of proof search. *)
let simpl_reason (self:t) (r:reason) : reason =
@ -936,7 +957,7 @@ module Make(Plugin : PLUGIN)
r
) else (
(* Clauses in [history] have been used to simplify [cl] into a clause [tmp_cl]
with only one formula (which is [a]). So we explicitly create that clause
with only one lit (which is [a]). So we explicitly create that clause
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
@ -957,7 +978,7 @@ module Make(Plugin : PLUGIN)
| Decision as r -> r
(* Boolean propagation.
Wrapper function for adding a new propagated formula. *)
Wrapper function for adding a new propagated lit. *)
let enqueue_bool (self:t) a ~level:lvl reason : unit =
let store = self.store in
if Atom.is_false store a then (
@ -1177,7 +1198,7 @@ module Make(Plugin : PLUGIN)
) else (
let uclause =
Clause.make_a store ~removable:true cr.cr_learnt in
(match self.on_learnt with Some f -> f self cr.cr_learnt | None -> ());
(match self.on_learnt with Some f -> f self uclause | None -> ());
(* no need to attach [uclause], it is true at level 0 *)
enqueue_bool self fuip ~level:0 (Bcp uclause)
)
@ -1189,7 +1210,7 @@ module Make(Plugin : PLUGIN)
);
attach_clause self lclause;
clause_bump_activity self lclause;
(match self.on_learnt with Some f -> f self cr.cr_learnt | None -> ());
(match self.on_learnt with Some f -> f self lclause | None -> ());
assert (cr.cr_is_uip);
enqueue_bool self fuip ~level:cr.cr_backtrack_lvl (Bcp lclause)
end;
@ -1374,25 +1395,25 @@ 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) (dp:dproof): unit =
let atoms = List.rev_map (make_atom self) l in
let acts_add_clause self ?(keep=false) (l:lit 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 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
let acts_add_decision_lit (self:t) (f:formula) (sign:bool) : unit =
let acts_add_decision_lit (self:t) (f:lit) (sign:bool) : unit =
let store = self.store in
let a = make_atom self f in
let a = make_atom_ self f in
let a = if sign then a else Atom.neg a in
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
)
let acts_raise self (l:formula list) (pr:dproof) : 'a =
let atoms = List.rev_map (make_atom self) l in
let acts_raise self (l:lit 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 in
if Proof.enabled self.proof then pr self.proof;
@ -1413,11 +1434,11 @@ module Make(Plugin : PLUGIN)
let store = self.store in
match expl with
| Solver_intf.Consequence mk_expl ->
let p = make_atom self f in
let p = make_atom_ self f in
if Atom.is_true store p then ()
else if Atom.is_false store p then (
let lits, dp = mk_expl() in
let l = List.rev_map (fun f -> Atom.neg @@ make_atom self f) lits 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) in
if Proof.enabled self.proof then dp self.proof;
@ -1426,7 +1447,7 @@ module Make(Plugin : PLUGIN)
insert_var_order self (Atom.var p);
let c = lazy (
let lits, dp = mk_expl () in
let l = List.rev_map (fun f -> Atom.neg @@ make_atom self f) lits 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
the literals should be true anyway, since it's an extension of the
@ -1453,18 +1474,18 @@ module Make(Plugin : PLUGIN)
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 =
let a = make_atom self f in
let[@inline] acts_eval_lit self (f:lit) : Solver_intf.lbool =
let a = make_atom_ self f in
eval_atom_ self a
let[@inline] acts_mk_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 module M = struct
type nonrec proof = proof
type dproof = proof -> unit
type nonrec formula = formula
type nonrec lit = lit
let iter_assumptions=acts_iter st ~full:false st.th_head
let eval_lit= acts_eval_lit st
let mk_lit=acts_mk_lit st
@ -1480,7 +1501,7 @@ module Make(Plugin : PLUGIN)
let module M = struct
type nonrec proof = proof
type dproof = proof -> unit
type nonrec formula = formula
type nonrec lit = lit
let iter_assumptions=acts_iter st ~full:true st.th_head
let eval_lit= acts_eval_lit st
let mk_lit=acts_mk_lit st
@ -1619,7 +1640,9 @@ module Make(Plugin : PLUGIN)
let atoms = Clause.atoms_a store c in
mark_dirty_atom (Atom.neg atoms.(0)); (* need to remove from watchlists *)
mark_dirty_atom (Atom.neg atoms.(1));
(match self.on_gc with Some f -> f self atoms | None -> ());
(match self.on_gc with
| Some f -> let lits = Clause.lits_a store c in f self lits
| None -> ());
in
(* find clauses to GC *)
@ -1669,7 +1692,7 @@ module Make(Plugin : PLUGIN)
let current_level = decision_level self in
enqueue_bool self atom ~level:current_level Decision;
self.n_decisions <- 1 + self.n_decisions;
(match self.on_decision with Some f -> f self atom | None -> ());
(match self.on_decision with Some f -> f self (Atom.lit self.store atom) | None -> ());
)
and pick_branch_lit self : unit =
@ -1718,7 +1741,7 @@ module Make(Plugin : PLUGIN)
add_clause_ st confl
);
st.n_conflicts <- 1 + st.n_conflicts;
(match st.on_conflict with Some f -> f st (Clause.atoms_a st.store confl) | None -> ());
(match st.on_conflict with Some f -> f st confl | None -> ());
| None -> (* No Conflict *)
assert (st.elt_head = Vec.size st.trail);
@ -1791,8 +1814,7 @@ module Make(Plugin : PLUGIN)
Log.debugf 5 (fun k -> k "(@[sat.theory-conflict-clause@ %a@])"
(Clause.debug self.store) c);
self.n_conflicts <- 1 + self.n_conflicts;
(match self.on_conflict with
Some f -> f self (Clause.atoms_a self.store c) | None -> ());
(match self.on_conflict with Some f -> f self c | None -> ());
Vec.push self.clauses_to_add c;
flush_clauses self;
end;
@ -1800,42 +1822,31 @@ module Make(Plugin : PLUGIN)
done
with E_sat -> ()
let assume self cnf dp : unit =
let assume self cnf : 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 in
if Proof.enabled self.proof then dp self.proof;
let atoms = Util.array_of_list_map (make_atom_ self) l in
let c = Clause.make_a self.store ~removable:false atoms in
if Proof.enabled self.proof then (
Proof.emit_input_clause self.proof (Iter.of_list l)
);
Log.debugf 10 (fun k -> k "(@[sat.assume-clause@ @[<hov 2>%a@]@])"
(Clause.debug self.store) c);
Vec.push self.clauses_to_add c)
cnf
(* Check satisfiability *)
let check_clause self c =
let res = Clause.exists self.store c ~f:(Atom.is_true self.store) in
if not res then (
Log.debugf 30
(fun k -> k "(@[sat.check-clause@ :not-satisfied @[<hov>%a@]@])"
(Clause.debug self.store) c);
false
) else
true
let check_vec self v = Vec.for_all (check_clause self) v
let check self : bool =
Vec.is_empty self.clauses_to_add &&
check_vec self self.clauses_hyps &&
check_vec self self.clauses_learnt
let[@inline] theory st = st.th
let[@inline] store st = st.store
let[@inline] proof st = st.proof
let[@inline] set_default_pol (self:t) (lit:lit) (pol:bool) : unit =
let a = make_atom_ self lit ~default_pol:pol in
Var.set_default_pol self.store (Atom.var a) pol
(* Result type *)
type res =
| Sat of Formula.t Solver_intf.sat_state
| Unsat of (atom,clause) Solver_intf.unsat_state
| Sat of Lit.t Solver_intf.sat_state
| Unsat of (lit,clause) Solver_intf.unsat_state
let pp_all self lvl status =
Log.debugf lvl
@ -1847,22 +1858,25 @@ module Make(Plugin : PLUGIN)
(Vec.pp ~sep:"" @@ Clause.debug self.store) self.clauses_hyps
(Vec.pp ~sep:"" @@ Clause.debug self.store) self.clauses_learnt)
let mk_sat (self:t) : Formula.t Solver_intf.sat_state =
let mk_sat (self:t) : Lit.t Solver_intf.sat_state =
pp_all self 99 "SAT";
let t = self.trail in
let module M = struct
type formula = Formula.t
type lit = Lit.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)
let[@inline] eval f = eval self (make_atom_ self f)
let[@inline] eval_level f = eval_level self (make_atom_ self f)
end in
(module M)
let mk_unsat (self:t) (us: unsat_cause) : _ Solver_intf.unsat_state =
pp_all self 99 "UNSAT";
let unsat_assumptions () = match us with
| US_local {first=_; core} -> core
| _ -> []
| US_local {first=_; core} ->
let store = store self in
let lits = Iter.of_list core |> Iter.map (Atom.lit store) in
lits
| _ -> Iter.empty
in
let unsat_conflict = match us with
| US_false c -> fun() -> c
@ -1876,7 +1890,7 @@ module Make(Plugin : PLUGIN)
fun () -> Lazy.force c
in
let module M = struct
type nonrec atom = atom
type nonrec lit = lit
type clause = Clause.t
type proof = Proof.t
let unsat_conflict = unsat_conflict
@ -1884,7 +1898,7 @@ module Make(Plugin : PLUGIN)
end in
(module M)
let add_clause_a self c dp : unit =
let add_clause_atoms_ self (c:atom array) dp : unit =
try
let c = Clause.make_a self.store ~removable:false c in
if Proof.enabled self.proof then dp self.proof;
@ -1893,47 +1907,49 @@ module Make(Plugin : PLUGIN)
| E_unsat (US_false c) ->
self.unsat_at_0 <- Some c
let add_clause self c dp : unit =
try
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) ->
self.unsat_at_0 <- Some c
let add_clause_a self c dp : unit =
let c = Array.map (make_atom_ self) c in
add_clause_atoms_ self c dp
(* FIXME: take lits, not atoms *)
let add_input_clause self c =
let emit_proof p =
let lits = Iter.of_list c |> Iter.map (Atom.formula (store self)) in
Proof.emit_input_clause p lits
in
let add_clause self (c:lit list) dp : unit =
let c = Util.array_of_list_map (make_atom_ self) c in
add_clause_atoms_ self c dp
let add_input_clause self (c:lit list) =
let emit_proof p = Proof.emit_input_clause p (Iter.of_list c) in
add_clause self c emit_proof
let add_input_clause_a self c =
let emit_proof p =
let lits = Iter.of_array c |> Iter.map (Atom.formula (store self)) in
Proof.emit_input_clause p lits
in
let emit_proof p = Proof.emit_input_clause p (Iter.of_array c) in
add_clause_a self c emit_proof
let solve ?(assumptions=[]) (st:t) : res =
cancel_until st 0;
Vec.clear st.assumptions;
List.iter (Vec.push st.assumptions) assumptions;
let solve ?(assumptions=[]) (self:t) : res =
cancel_until self 0;
Vec.clear self.assumptions;
List.iter
(fun lit ->
let a = make_atom_ self lit in
Vec.push self.assumptions a)
assumptions;
try
solve_ st;
Sat (mk_sat st)
solve_ self;
Sat (mk_sat self)
with E_unsat us ->
Unsat (mk_unsat st us)
Unsat (mk_unsat self us)
let true_at_level0 st a =
try
let b, lev = eval_level st a in
b && lev = 0
with UndecidedLit -> false
let true_at_level0 (self:t) (lit:lit) : bool =
match find_atom_ self lit with
| None -> false
| Some a ->
try
let b, lev = eval_level self a in
b && lev = 0
with UndecidedLit -> false
let[@inline] eval_atom self a : Solver_intf.lbool = eval_atom_ self a
let[@inline] eval_lit self (lit:lit) : Solver_intf.lbool =
match find_atom_ self lit with
| Some a -> eval_atom_ self a
| None -> Solver_intf.L_undefined
end
[@@inline][@@specialise]
@ -1947,9 +1963,9 @@ module Make_cdcl_t(Plugin : Solver_intf.PLUGIN_CDCL_T) =
module Make_pure_sat(Plugin : Solver_intf.PLUGIN_SAT) =
Make(struct
type formula = Plugin.formula
type lit = Plugin.lit
type proof = Plugin.proof
module Formula = Plugin.Formula
module Lit = Plugin.Lit
module Proof = Plugin.Proof
type t = unit
let push_level () = ()

8
src/sat/Solver.mli
View file

@ -3,15 +3,15 @@ module type S = Solver_intf.S
(** Safe external interface of solvers. *)
module Make_pure_sat(Th: Solver_intf.PLUGIN_SAT)
: S with type formula = Th.formula
and module Formula = Th.Formula
: S with type lit = Th.lit
and module Lit = Th.Lit
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 type formula = Th.formula
and module Formula = Th.Formula
: S with type lit = Th.lit
and module Lit = Th.Lit
and type proof = Th.proof
and module Proof = Th.Proof
and type theory = Th.t

173
src/sat/Solver_intf.ml
View file

@ -14,55 +14,56 @@ Copyright 2016 Simon Cruanes
type 'a printer = Format.formatter -> 'a -> unit
module type SAT_STATE = sig
type formula
type lit
(** Literals (signed boolean atoms) *)
val eval : formula -> bool
(** Returns the valuation of a formula in the current state
val eval : lit -> bool
(** Returns the valuation of a lit in the current state
of the sat solver.
@raise UndecidedLit if the literal is not decided *)
val eval_level : formula -> bool * int
val eval_level : lit -> bool * int
(** Return the current assignement of the literals, as well as its
decision level. If the level is 0, then it is necessary for
the atom 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.
@raise UndecidedLit if the literal is not decided *)
val iter_trail : (formula -> unit) -> unit
(** Iter through the formulas in order of decision/propagation
val iter_trail : (lit -> unit) -> unit
(** Iter through the lits in order of decision/propagation
(starting from the first propagation, to the last propagation). *)
end
type 'form sat_state = (module SAT_STATE with type formula = 'form)
type 'form sat_state = (module SAT_STATE with type lit = 'form)
(** The type of values returned when the solver reaches a SAT state. *)
module type UNSAT_STATE = sig
type atom
type lit
type clause
val unsat_conflict : unit -> clause
(** Returns the unsat clause found at the toplevel *)
val unsat_assumptions: unit -> atom list
val unsat_assumptions : unit -> lit Iter.t
(** Subset of assumptions responsible for "unsat" *)
end
type ('atom, 'clause) unsat_state =
(module UNSAT_STATE with type atom = 'atom
type ('lit, 'clause) unsat_state =
(module UNSAT_STATE with type lit = 'lit
and type clause = 'clause)
(** The type of values returned when the solver reaches an UNSAT state. *)
type negated =
| Negated (** changed sign *)
| Same_sign (** kept sign *)
(** This type is used during the normalisation of formulas.
(** This type is used during the normalisation of lits.
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
formula [f]. The proof should be a proof of the clause "[l] implies [f]".
(** The type of reasons for propagations of a lit [f]. *)
type ('lit, 'proof) reason =
| Consequence of (unit -> 'lit list * 'proof) [@@unboxed]
(** [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]".
invariant: in [Consequence (fun () -> l,p)], all elements of [l] must be true in
the current trail.
@ -84,60 +85,60 @@ type lbool = L_true | L_false | L_undefined
(** Valuation of an atom *)
module type ACTS = sig
type formula
type lit
type proof
type dproof = proof -> unit
val iter_assumptions: (formula -> unit) -> unit
val iter_assumptions: (lit -> unit) -> unit
(** Traverse the new assumptions on the boolean trail. *)
val eval_lit: formula -> lbool
val eval_lit: lit -> lbool
(** Obtain current value of the given literal *)
val mk_lit: ?default_pol:bool -> formula -> unit
(** Map the given formula to a literal, which will be decided by the
val mk_lit: ?default_pol:bool -> lit -> unit
(** Map the given lit to a literal, which will be decided by the
SAT solver. *)
val add_clause: ?keep:bool -> formula list -> dproof -> unit
val add_clause: ?keep:bool -> lit 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 -> dproof -> 'b
val raise_conflict: lit 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, dproof) reason -> unit
(** Propagate a formula, i.e. the theory can evaluate the formula to be true
val propagate: lit -> (lit, dproof) reason -> unit
(** Propagate a lit, i.e. the theory can evaluate the lit to be true
(see the definition of {!type:eval_res} *)
val add_decision_lit: formula -> bool -> unit
(** Ask the SAT solver to decide on the given formula with given sign
val add_decision_lit: lit -> bool -> unit
(** 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.
Useful for theory combination. This will be undone on backtracking. *)
end
type ('formula, 'proof) acts =
(module ACTS with type formula = 'formula
type ('lit, 'proof) acts =
(module ACTS with type lit = 'lit
and type proof = 'proof)
(** The type for a slice of assertions to assume/propagate in the theory. *)
exception No_proof
module type FORMULA = sig
(** formulas *)
module type LIT = sig
(** lits *)
type t
(** The type of atomic formulas over terms. *)
(** The type of atomic lits over terms. *)
val equal : t -> t -> bool
(** Equality over formulas. *)
(** Equality over lits. *)
val hash : t -> int
(** Hashing function for formulas. Should be such that two formulas equal according
(** Hashing function for lits. Should be such that two lits equal according
to {!val:Expr_intf.S.equal} have the same hash. *)
val pp : t printer
@ -147,9 +148,9 @@ module type FORMULA = sig
(** Formula negation *)
val norm : t -> t * negated
(** Returns a 'normalized' form of the formula, possibly negated
(** Returns a 'normalized' form of the lit, possibly negated
(in which case return [Negated]).
[norm] must be so that [a] and [neg a] normalise to the same formula,
[norm] must be so that [a] and [neg a] normalise to the same lit,
but one returns [Negated] and the other [Same_sign]. *)
end
@ -160,15 +161,15 @@ module type PLUGIN_CDCL_T = sig
type t
(** The plugin state itself *)
type formula
module Formula : FORMULA with type t = formula
type lit
module Lit : LIT with type t = lit
type proof
(** Proof storage/recording *)
module Proof : PROOF
with type t = proof
and type lit = formula
and type lit = lit
val push_level : t -> unit
(** Create a new backtrack level *)
@ -176,12 +177,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, 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
val partial_check : t -> (lit, proof) acts -> unit
(** 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
new lemmas. *)
val final_check : t -> (Formula.t, proof) acts -> unit
val final_check : t -> (lit, 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;
@ -190,11 +191,11 @@ end
(** Signature for pure SAT solvers *)
module type PLUGIN_SAT = sig
type formula
module Formula : FORMULA with type t = formula
type lit
module Lit : LIT with type t = lit
type proof
module Proof : PROOF with type t = proof and type lit = formula
module Proof : PROOF with type t = proof and type lit = lit
end
(** The external interface implemented by safe solvers, such as the one
@ -204,14 +205,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. *)
type formula (** user formulas *)
type lit (** literals *)
module Formula : FORMULA with type t = formula
type atom
(** The type of atoms given by the module argument for formulas.
An atom is a user-defined atomic formula whose truth value is
picked by Msat. *)
module Lit : LIT with type t = lit
type clause
@ -228,24 +224,6 @@ module type S = sig
type store
(** Stores atoms, clauses, etc. *)
(* TODO: keep this internal *)
module Atom : sig
type t = atom
val equal : t -> t -> bool
val compare : t -> t -> int
val hash : t -> int
val neg : t -> t
val sign : t -> bool
val abs : t -> t
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
@ -260,17 +238,18 @@ module type S = sig
val n_atoms : store -> t -> int
val atoms_iter : store -> t -> atom Iter.t
val lits_iter : store -> t -> lit Iter.t
(** Literals of a clause *)
val lits_a : store -> t -> lit array
(** Atoms of a clause *)
val atoms_a : store -> t -> atom array
val atoms_l : store -> t -> atom list
val lits_l : store -> t -> lit list
(** List of atoms of a clause *)
end
module Proof : PROOF
with type lit = formula
with type lit = lit
and type t = proof
(** A module to manipulate proofs. *)
@ -278,11 +257,10 @@ module type S = sig
(** Main solver type, containing all state for solving. *)
val create :
?on_conflict:(t -> atom array -> unit) ->
?on_decision:(t -> atom -> unit) ->
?on_new_atom:(t -> atom -> unit) ->
?on_learnt:(t -> atom array -> unit) ->
?on_gc:(t -> atom array -> unit) ->
?on_conflict:(t -> Clause.t -> unit) ->
?on_decision:(t -> lit -> unit) ->
?on_learnt:(t -> Clause.t -> unit) ->
?on_gc:(t -> lit array -> unit) ->
?size:[`Tiny|`Small|`Big] ->
proof:Proof.t ->
theory ->
@ -306,8 +284,8 @@ 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) unsat_state (** Returned when the solver reaches UNSAT, with a proof *)
| Sat of lit sat_state (** Returned when the solver reaches SAT, with a model *)
| Unsat of (lit,clause) unsat_state (** Returned when the solver reaches UNSAT, with a proof *)
exception UndecidedLit
(** Exception raised by the evaluating functions when a literal
@ -315,44 +293,41 @@ module type S = sig
(** {2 Base operations} *)
val assume : t -> formula list list -> unit
val assume : t -> lit list list -> 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 -> dproof -> unit
val add_clause : t -> lit list -> dproof -> unit
(** Lower level addition of clauses *)
val add_input_clause : t -> atom list -> unit
val add_input_clause : t -> lit list -> unit
(** Like {!add_clause} but with the justification of being an input clause *)
val add_clause_a : t -> atom array -> dproof -> unit
val add_clause_a : t -> lit array -> dproof -> unit
(** Lower level addition of clauses *)
val add_input_clause_a : t -> atom array -> unit
val add_input_clause_a : t -> lit array -> unit
(** Like {!add_clause_a} but with justification of being an input clause *)
(* TODO: API to push/pop/clear assumptions from an inner vector *)
val solve :
?assumptions:atom list ->
?assumptions:lit list ->
t -> res
(** Try and solves the current set of clauses.
@param assumptions additional atomic assumptions to be temporarily added.
The assumptions are just used for this call to [solve], they are
not saved in the solver's state. *)
val 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.
@param default_pol default polarity of the boolean variable.
Default is [true]. *)
val set_default_pol : t -> lit -> bool -> unit
(** Set default polarity for the given boolean variable.
Sign of the literal is ignored. *)
val true_at_level0 : t -> atom -> bool
val true_at_level0 : t -> lit -> bool
(** [true_at_level0 a] returns [true] if [a] was proved at level0, i.e.
it must hold in all models *)
val eval_atom : t -> atom -> lbool
val eval_lit : t -> lit -> lbool
(** Evaluate atom in current state *)
val n_propagations : t -> int

11
src/util/Util.ml
View file

@ -26,6 +26,17 @@ let pp_iarray ?(sep=" ") pp out a =
let flat_map_l_ia f l =
CCList.flat_map (fun x -> IArray.to_list @@ f x) l
let array_of_list_map f l =
match l with
| [] -> [| |]
| x :: tl ->
let arr = Array.make (List.length tl+1) (f x) in
List.iteri (fun i y -> arr.(i+1) <- f y) tl;
arr
let array_to_list_map f arr =
List.init (Array.length arr) (fun i -> f arr.(i))
let setup_gc () =
let g = Gc.get () in
Gc.set {

5
src/util/Util.mli
View file

@ -16,6 +16,11 @@ val pp_iarray : ?sep:string -> 'a CCFormat.printer -> 'a IArray.t CCFormat.print
val flat_map_l_ia : ('a -> 'b IArray.t) -> 'a list -> 'b list
val array_of_list_map : ('a -> 'b) -> 'a list -> 'b array
(** [array_of_list_map f l] is the same as [Array.of_list @@ List.map f l] *)
val array_to_list_map : ('a -> 'b) -> 'a array -> 'b list
val setup_gc : unit -> unit
(** Change parameters of the GC *)