simon/sidekick
1
0
Fork 0
mirror of https://github.com/c-cube/sidekick.git synced 2026-01-21 16:56:41 -05:00
Code Issues Projects Releases Packages Wiki Activity Actions

refactor: internalize terms earlier

Browse source
This commit is contained in:
Simon Cruanes 2018-05-25 21:32:24 -05:00
parent ea5bce9635
commit 9b8c21513a
3 changed files with 51 additions and 70 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

3
src/sat/Theory_intf.ml
View file

@ -124,6 +124,9 @@ module type S = sig
(** Assume the formulas in the slice, possibly pushing new formulas to be propagated,
and returns the result of the new assumptions. *)
val add_formula : t -> formula -> unit
(** Internalize formula for later use *)
val if_sat : t -> formula slice_actions -> (formula, proof) res
(** Called at the end of the search in case a model has been found. If no new clause is
pushed, then 'sat' is returned, else search is resumed. *)

62
src/smt/Congruence_closure.ml
View file

@ -154,8 +154,7 @@ let add_signature cc (t:term) (r:repr): unit = match signature cc t with
(* add, but only if not present already *)
begin match Sig_tbl.get cc.signatures_tbl s with
| None ->
on_backtrack cc
(fun () -> Sig_tbl.remove cc.signatures_tbl s);
on_backtrack cc (fun () -> Sig_tbl.remove cc.signatures_tbl s);
Sig_tbl.add cc.signatures_tbl s r;
| Some r' ->
assert (Equiv_class.equal r r');
@ -381,18 +380,8 @@ and update_combine cc =
assert (is_root_ ra);
assert (is_root_ rb);
(* We will merge [r_from] into [r_into].
we try to ensure that [size ra <= size rb] in general, unless
it clashes with the invariant that the representative must
be a normal form if the class contains a normal form *)
let must_solve, r_from, r_into =
match Term.is_semantic ra.n_term, Term.is_semantic rb.n_term with
| true, true ->
if size_ ra > size_ rb then true, rb, ra else true, ra, rb
| false, false ->
if size_ ra > size_ rb then false, rb, ra else false, ra, rb
| true, false -> false, rb, ra (* semantic ==> representative *)
| false, true -> false, ra, rb
in
we try to ensure that [size ra <= size rb] in general *)
let r_from, r_into = if size_ ra > size_ rb then rb, ra else ra, rb in
let new_tags =
Util.Int_map.union
(fun _i (n1,e1) (n2,e2) ->
@ -411,28 +400,6 @@ and update_combine cc =
raise_conflict cc @@ Lit.Set.elements lits)
ra.n_tags rb.n_tags
in
(* solve the equation, if both [ra] and [rb] are semantic.
The equation is between signatures, so as to canonize w.r.t the
current congruence before solving *)
if must_solve then (
let t_a = ra.n_term and t_b = rb.n_term in
match signature cc t_a, signature cc t_b with
| Some (Custom t1), Some (Custom t2) ->
begin match t1.tc.tc_t_solve t1.view t2.view with
| Solve_ok {subst=l} ->
Log.debugf 5
(fun k->k "(@[solve@ (@[= %a %a@])@ :yields (@[%a@])@])"
Term.pp t_a Term.pp t_b
(Util.pp_list @@ Util.pp_pair Equiv_class.pp Term.pp) l);
List.iter (fun (u1,u2) -> push_combine cc u1 (add cc u2) e_ab) l
| Solve_fail {expl} ->
Log.debugf 5
(fun k->k "(@[solve-fail@ (@[= %a %a@])@ :expl %a@])"
Term.pp t_a Term.pp t_b (CCFormat.Dump.list Lit.pp) expl);
raise_conflict cc expl
end
| _ -> assert false
);
(* remove [ra.parents] from signature, put them into [st.pending] *)
begin
Bag.to_seq (r_from:>node).n_parents
@ -487,6 +454,7 @@ and notify_merge cc (ra:repr) ~into:(rb:repr) (e:explanation): unit =
(* add [t] to [cc] when not present already *)
and add_new_term cc (t:term) : node =
assert (not @@ mem cc t);
Log.debugf 20 (fun k->k "(@[cc.add_term@ %a@])" Term.pp t);
let n = Equiv_class.make t in
(* how to add a subterm *)
let add_to_parents_of_sub_node (sub:node) : unit =
@ -515,32 +483,36 @@ and add_new_term cc (t:term) : node =
tc.tc_t_relevant view add_sub_t
end;
(* remove term when we backtrack *)
on_backtrack cc (fun () -> Term.Tbl.remove cc.tbl t);
on_backtrack cc
(fun () ->
Log.debugf 20 (fun k->k "(@[cc.remove_term@ %a@])" Term.pp t);
Term.Tbl.remove cc.tbl t);
(* add term to the table *)
Term.Tbl.add cc.tbl t n;
(* [n] might be merged with other equiv classes *)
push_pending cc n;
n
(* TODO? *)
(* add [t=u] to the congruence closure, unconditionally (reduction relation) *)
and[@inline] add_eqn (cc:t) (eqn:merge_op): unit =
let t, u, expl = eqn in
push_combine cc t u expl
(* add a term *)
and[@inline] add cc t =
and[@inline] add cc t : node =
try Term.Tbl.find cc.tbl t
with Not_found -> add_new_term cc t
let[@inline] add_seq cc seq = seq (fun t -> ignore @@ add cc t)
(* before we push tasks into [pending], ensure they are removed when we backtrack *)
let reset_on_backtrack cc : unit =
if Vec.is_empty cc.pending then (
on_backtrack cc (fun () -> Vec.clear cc.pending);
)
(* assert that this boolean literal holds *)
let assert_lit cc lit : unit = match Lit.view lit with
| Lit_fresh _
| Lit_expanded _ -> ()
| Lit_atom t ->
assert (Ty.is_prop t.term_ty);
Log.debugf 5 (fun k->k "(@[cc.assert_lit@ %a@])" Lit.pp lit);
let sign = Lit.sign lit in
(* equate t and true/false *)
let rhs = if sign then true_ cc else false_ cc in
@ -549,6 +521,7 @@ let assert_lit cc lit : unit = match Lit.view lit with
basically, just have [n] point to true/false and thus acquire
the corresponding value, so its superterms (like [ite]) can evaluate
properly *)
reset_on_backtrack cc;
push_combine cc n rhs (E_lit lit);
()
@ -556,6 +529,7 @@ let assert_eq cc (t:term) (u:term) expl : unit =
let n1 = add cc t in
let n2 = add cc u in
if not (same_class cc n1 n2) then (
reset_on_backtrack cc;
union cc n1 n2 expl
)

56
src/smt/Theory_combine.ml
View file

@ -4,6 +4,7 @@
(** Combine the congruence closure with a number of plugins *)
module Sat_solver = Sidekick_sat
module C_clos = Congruence_closure
open Solver_types
module Proof = struct
@ -25,7 +26,7 @@ type t = {
(** actions provided by the SAT solver *)
tst: Term.state;
(** state for managing terms *)
cc: Congruence_closure.t lazy_t;
cc: C_clos.t lazy_t;
(** congruence closure *)
mutable theories : Theory.state list;
(** Set of theories *)
@ -43,7 +44,7 @@ let[@inline] theories (self:t) : Theory.state Sequence.t =
(* handle a literal assumed by the SAT solver *)
let assume_lit (self:t) (lit:Lit.t) : unit =
Sat_solver.Log.debugf 2
(fun k->k "(@[<1>@{<green>theory_combine.assume_lit@}@ @[%a@]@])" Lit.pp lit);
(fun k->k "(@[<1>@{<green>th_combine.assume_lit@}@ @[%a@]@])" Lit.pp lit);
(* check consistency first *)
begin match Lit.view lit with
| Lit_fresh _ -> ()
@ -52,7 +53,7 @@ let assume_lit (self:t) (lit:Lit.t) : unit =
| Lit_atom {term_cell=Bool false; _} -> ()
| Lit_atom _ ->
(* transmit to theories. *)
Congruence_closure.assert_lit (cc self) lit;
C_clos.assert_lit (cc self) lit;
theories self (fun (module Th) -> Th.on_assert Th.state lit);
end
@ -64,14 +65,15 @@ let cdcl_return_res (self:t) : _ Sat_solver.res =
| Some lit_set ->
let conflict_clause = IArray.of_list_map Lit.neg lit_set in
Sat_solver.Log.debugf 3
(fun k->k "(@[<1>conflict@ clause: %a@])"
(fun k->k "(@[<1>@{<yellow>th_combine.conflict@}@ :clause %a@])"
Theory.Clause.pp conflict_clause);
self.conflict <- None;
Sat_solver.Unsat (IArray.to_list conflict_clause, Proof.default)
end
let[@inline] check (self:t) : unit =
Congruence_closure.check (cc self)
Log.debug 5 "(th_combine.check)";
C_clos.check (cc self)
let with_conflict_catch self f =
begin
@ -95,27 +97,29 @@ let assume_real (self:t) (slice:Lit.t Sat_solver.slice_actions) =
check self
)
let add_formula (self:t) (lit:Lit.t) =
match Lit.view lit with
| Lit_atom t ->
let lazy cc = self.cc in
ignore (C_clos.add cc t : cc_node)
| Lit_expanded _ | Lit_fresh _ -> ()
(* propagation from the bool solver *)
let assume (self:t) (slice:_ Sat_solver.slice_actions) =
match self.conflict with
| Some _ -> cdcl_return_res self (* already in conflict! *)
| None -> assume_real self slice
| Some _ ->
(* already in conflict! *)
cdcl_return_res self
(* perform final check of the model *)
let if_sat (self:t) (slice:Lit.t Sat_solver.slice_actions) : _ Sat_solver.res =
Congruence_closure.final_check (cc self);
(* all formulas in the SAT solver's trail *)
let forms =
let (module SA) = slice in
SA.slice_iter
in
(* final check for each theory *)
let (module SA) = slice in
with_conflict_catch self
(fun () ->
(* final check for CC + each theory *)
C_clos.final_check (cc self);
theories self
(fun (module Th) -> Th.final_check Th.state forms))
(fun (module Th) -> Th.final_check Th.state SA.slice_iter))
(** {2 Various helpers} *)
@ -123,7 +127,7 @@ let if_sat (self:t) (slice:Lit.t Sat_solver.slice_actions) : _ Sat_solver.res =
let act_propagate (self:t) f guard : unit =
let (module A) = self.cdcl_acts in
Sat_solver.Log.debugf 2
(fun k->k "(@[@{<green>propagate@}@ %a@ :guard %a@])"
(fun k->k "(@[@{<green>th.propagate@}@ %a@ :guard %a@])"
Lit.pp f (Util.pp_list Lit.pp) guard);
A.propagate f guard Proof.default
@ -136,7 +140,7 @@ let on_merge_from_cc (self:t) r1 r2 e : unit =
theories self
(fun (module Th) -> Th.on_merge Th.state r1 r2 e)
let mk_cc_actions (self:t) : Congruence_closure.actions =
let mk_cc_actions (self:t) : C_clos.actions =
let (module A) = self.cdcl_acts in
let module R = struct
let on_backtrack = A.on_backtrack
@ -150,34 +154,34 @@ let mk_cc_actions (self:t) : Congruence_closure.actions =
(* create a new theory combination *)
let create (cdcl_acts:_ Sat_solver.actions) : t =
Sat_solver.Log.debug 5 "theory_combine.create";
Sat_solver.Log.debug 5 "th_combine.create";
let rec self = {
cdcl_acts;
tst=Term.create ~size:1024 ();
cc = lazy (
(* lazily tie the knot *)
let actions = mk_cc_actions self in
Congruence_closure.create ~size:1024 ~actions self.tst;
C_clos.create ~size:1024 ~actions self.tst;
);
theories = [];
conflict = None;
} in
ignore (Lazy.force @@ self.cc : Congruence_closure.t);
ignore (Lazy.force @@ self.cc : C_clos.t);
self
(** {2 Interface to individual theories} *)
let act_all_classes self = Congruence_closure.all_classes (cc self)
let act_all_classes self = C_clos.all_classes (cc self)
let act_propagate_eq self t u guard =
Congruence_closure.assert_eq (cc self) t u guard
C_clos.assert_eq (cc self) t u guard
let act_propagate_distinct self l ~neq guard =
Congruence_closure.assert_distinct (cc self) l ~neq guard
C_clos.assert_distinct (cc self) l ~neq guard
let act_find self t =
Congruence_closure.add (cc self) t
|> Congruence_closure.find (cc self)
C_clos.add (cc self) t
|> C_clos.find (cc self)
let act_add_local_axiom self c : unit =
Sat_solver.Log.debugf 5 (fun k->k "(@[<2>th_combine.push_local_lemma@ %a@])" Theory.Clause.pp c);
@ -208,7 +212,7 @@ let mk_theory_actions (self:t) : Theory.actions =
let add_theory (self:t) (th:Theory.t) : unit =
Sat_solver.Log.debugf 2
(fun k->k "(@[theory_combine.add_th@ :name %S@])" th.Theory.name);
(fun k->k "(@[th_combine.add_th@ :name %S@])" th.Theory.name);
let th_s = th.Theory.make self.tst (mk_theory_actions self) in
self.theories <- th_s :: self.theories