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

wip: use Lit.Set.t for explanations

Browse source
This commit is contained in:
Simon Cruanes 2018-05-23 22:24:35 -05:00
parent d1c88e73f7
commit 6302d13fe8
5 changed files with 13 additions and 18 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/smt/Congruence_closure.ml
View file

@ -28,7 +28,7 @@ type actions = {
raise_conflict: 'a. Lit.Set.t -> 'a;
(** Report a conflict *)
propagate: Lit.t -> Explanation.t Bag.t -> unit;
propagate: Lit.t -> Lit.t list -> unit;
(** Propagate a literal *)
}

3
src/smt/Congruence_closure.mli
View file

@ -21,8 +21,7 @@ type actions = {
raise_conflict: 'a. Lit.Set.t -> 'a;
(** Report a conflict *)
(* FIXME: take a delayed Lit.Set.t? *)
propagate: Lit.t -> Explanation.t Bag.t -> unit;
propagate: Lit.t -> Lit.t list -> unit;
(** Propagate a literal *)
}

8
src/smt/Theory.ml
View file

@ -41,13 +41,13 @@ type actions = {
raise_conflict: 'a. conflict -> 'a;
(** Give a conflict clause to the solver *)
propagate_eq: Term.t -> Term.t -> Explanation.t -> unit;
propagate_eq: Term.t -> Term.t -> Lit.Set.t -> unit;
(** Propagate an equality [t = u] because [e] *)
propagate_distinct: Term.t list -> neq:Term.t -> Explanation.t -> unit;
(** Propagate a [distinct l] because [e] (where [e = atom neq] *)
propagate_distinct: Term.t list -> neq:Term.t -> Lit.t -> unit;
(** Propagate a [distinct l] because [e] (where [e = neq] *)
propagate: Lit.t -> Explanation.t Bag.t -> unit;
propagate: Lit.t -> Lit.Set.t -> unit;
(** Propagate a boolean using a unit clause.
[expl => lit] must be a theory lemma, that is, a T-tautology *)

4
src/smt/Theory_combine.ml
View file

@ -126,10 +126,6 @@ let if_sat (self:t) (slice:_) : _ Sat_solver.res =
(* forward propagations from CC or theories directly to the SMT core *)
let act_propagate (self:t) f guard : unit =
let Sat_solver.Actions r = self.cdcl_acts in
let guard =
Congruence_closure.explain_unfold_bag (cc self) guard
|> Lit.Set.to_list
in
Sat_solver.Log.debugf 2
(fun k->k "(@[@{<green>propagate@}@ %a@ :guard %a@])"
Lit.pp f (Util.pp_list Lit.pp) guard);

14
src/smt/th_bool/Sidekick_th_bool.ml
View file

@ -255,13 +255,13 @@ let tseitin (self:t) (lit:Lit.t) (lit_t:term) (b:term builtin) : unit =
| B_not _ -> assert false (* normalized *)
| B_eq (t,u) ->
if Lit.sign lit then (
self.acts.Theory.propagate_eq t u (Explanation.lit lit)
self.acts.Theory.propagate_eq t u (Lit.Set.singleton lit)
) else (
self.acts.Theory.propagate_distinct [t;u] ~neq:lit_t (Explanation.lit lit)
self.acts.Theory.propagate_distinct [t;u] ~neq:lit_t lit
)
| B_distinct l ->
if Lit.sign lit then (
self.acts.Theory.propagate_distinct l ~neq:lit_t (Explanation.lit lit)
self.acts.Theory.propagate_distinct l ~neq:lit_t lit
) else (
(* TODO: propagate pairwise equalities? *)
Error.errorf "cannot process negative distinct lit %a" Lit.pp lit;
@ -269,7 +269,7 @@ let tseitin (self:t) (lit:Lit.t) (lit_t:term) (b:term builtin) : unit =
| B_and subs ->
if Lit.sign lit then (
(* propagate [lit => subs_i] *)
let expl = Bag.return (Explanation.lit lit) in
let expl = Lit.Set.singleton lit in
List.iter
(fun sub ->
let sublit = Lit.atom sub in
@ -277,7 +277,7 @@ let tseitin (self:t) (lit:Lit.t) (lit_t:term) (b:term builtin) : unit =
subs
) else (
(* propagate [¬lit => ∨_i ¬ subs_i] *)
let c = lit :: List.map (Lit.atom ~sign:false) subs in
let c = Lit.neg lit :: List.map (Lit.atom ~sign:false) subs in
self.acts.Theory.add_local_axiom (IArray.of_list c)
)
| B_or subs ->
@ -287,7 +287,7 @@ let tseitin (self:t) (lit:Lit.t) (lit_t:term) (b:term builtin) : unit =
self.acts.Theory.add_local_axiom (IArray.of_list c)
) else (
(* propagate [¬lit => ¬subs_i] *)
let expl = Bag.return (Explanation.lit lit) in
let expl = Lit.Set.singleton lit in
List.iter
(fun sub ->
let sublit = Lit.atom ~sign:false sub in
@ -300,7 +300,7 @@ let tseitin (self:t) (lit:Lit.t) (lit_t:term) (b:term builtin) : unit =
let c = Lit.atom concl :: Lit.neg lit :: List.map (Lit.atom ~sign:false) guard in
self.acts.Theory.add_local_axiom (IArray.of_list c)
) else (
let expl = Bag.return (Explanation.lit lit) in
let expl = Lit.Set.singleton lit in
(* propagate [¬lit => ¬concl] *)
self.acts.Theory.propagate (Lit.atom ~sign:false concl) expl;
(* propagate [¬lit => ∧_i guard_i] *)