From 431988d5e4382c3421bac8502444b859358f1732 Mon Sep 17 00:00:00 2001 From: Simon Cruanes Date: Sat, 9 Mar 2019 16:15:24 -0600 Subject: [PATCH] feat: more expressive theories, also plug `distinct` in --- src/cc/Congruence_closure.ml | 8 +++++++- src/cc/Congruence_closure_intf.ml | 4 ++++ src/main/main.ml | 4 +++- src/smt/Term.ml | 1 + src/smt/Term.mli | 1 + src/smt/Theory.ml | 11 +++++++++-- src/smt/Theory_combine.ml | 1 + src/smtlib/Process.ml | 4 ++-- 8 files changed, 28 insertions(+), 6 deletions(-) diff --git a/src/cc/Congruence_closure.ml b/src/cc/Congruence_closure.ml index 92ca628b..86e5ba77 100644 --- a/src/cc/Congruence_closure.ml +++ b/src/cc/Congruence_closure.ml @@ -324,6 +324,7 @@ module Make(A: ARG) = struct combine: combine_task Vec.t; undo: (unit -> unit) Backtrack_stack.t; mutable theories: theory IM.t; + mutable on_merge: (t -> N.t -> N.t -> Expl.t -> unit) list; mutable ps_lits: lit list; (* TODO: thread it around instead? *) (* proof state *) ps_queue: (node*node) Vec.t; @@ -734,6 +735,8 @@ module Make(A: ARG) = struct merge_bool rb b ra a; (* perform [union r_from r_into] *) Log.debugf 15 (fun k->k "(@[cc.merge@ :from %a@ :into %a@])" N.pp r_from N.pp r_into); + (* call [on_merge] functions *) + List.iter (fun f -> f cc r_into r_from e_ab) cc.on_merge; (* call micro theories *) begin let th_into = r_into.n_th_data in @@ -986,13 +989,16 @@ module Make(A: ARG) = struct Log.debugf 3 (fun k->k "(@[@{cc.add-theory@} %a@])" Key.pp Th.key); self.theories <- IM.add Th.key_id th self.theories - let create ?th:(theories=[]) ?(size=`Big) (tst:term_state) : t = + let on_merge cc f = cc.on_merge <- f :: cc.on_merge + + let create ?th:(theories=[]) ?(on_merge=[]) ?(size=`Big) (tst:term_state) : t = let size = match size with `Small -> 128 | `Big -> 2048 in let rec cc = { tst; tbl = T_tbl.create size; signatures_tbl = Sig_tbl.create size; theories=IM.empty; + on_merge; pending=Vec.create(); combine=Vec.create(); ps_lits=[]; diff --git a/src/cc/Congruence_closure_intf.ml b/src/cc/Congruence_closure_intf.ml index f9105d75..410370d6 100644 --- a/src/cc/Congruence_closure_intf.ml +++ b/src/cc/Congruence_closure_intf.ml @@ -152,6 +152,7 @@ module type S = sig val create : ?th:Theory.t list -> + ?on_merge:(t -> N.t -> N.t -> Expl.t -> unit) list -> ?size:[`Small | `Big] -> term_state -> t @@ -162,6 +163,9 @@ module type S = sig @raise Error.Error if there is already a theory with the same key. *) + val on_merge : t -> (t -> N.t -> N.t -> Expl.t -> unit) -> unit + (** Add a function to be called when two classes are merged *) + val set_as_lit : t -> N.t -> lit -> unit (** map the given node to a literal. *) diff --git a/src/main/main.ml b/src/main/main.ml index d64dbf9d..edb43c35 100644 --- a/src/main/main.ml +++ b/src/main/main.ml @@ -117,7 +117,9 @@ let main () = (* TODO: eager CNF conversion *) [Sidekick_th_bool.th_dynamic_tseitin] | Smtlib -> - [Sidekick_th_bool.th_dynamic_tseitin] (* TODO: more theories *) + [ Sidekick_th_bool.th_dynamic_tseitin; + Sidekick_th_distinct.th; + ] (* TODO: more theories *) in Sidekick_smt.Solver.create ~store_proof:!check ~theories () in diff --git a/src/smt/Term.ml b/src/smt/Term.ml index 9690c02e..10f3adcd 100644 --- a/src/smt/Term.ml +++ b/src/smt/Term.ml @@ -102,6 +102,7 @@ module As_key = struct end module Map = CCMap.Make(As_key) +module Set = CCSet.Make(As_key) module Tbl = CCHashtbl.Make(As_key) let to_seq t yield = diff --git a/src/smt/Term.mli b/src/smt/Term.mli index 3978d383..b7e751be 100644 --- a/src/smt/Term.mli +++ b/src/smt/Term.mli @@ -56,3 +56,4 @@ val as_cst_undef : t -> (cst * Ty.Fun.t) option module Tbl : CCHashtbl.S with type key = t module Map : CCMap.S with type key = t +module Set : CCSet.S with type elt = t diff --git a/src/smt/Theory.ml b/src/smt/Theory.ml index 149529e5..99c9ca89 100644 --- a/src/smt/Theory.ml +++ b/src/smt/Theory.ml @@ -36,6 +36,10 @@ module type ACTIONS = sig (** Propagate a boolean using a unit clause. [expl => lit] must be a theory lemma, that is, a T-tautology *) + val add_lit : Lit.t -> unit + (** Add the given literal to the SAT solver, so it gets assigned + a boolean value *) + val add_local_axiom: Lit.t list -> unit (** Add local clause to the SAT solver. This clause will be removed when the solver backtracks. *) @@ -56,10 +60,11 @@ module type S = sig val create : Term.state -> t (** Instantiate the theory's state *) - (* TODO: instead pass Congruence_closure.theory to [create] + val on_new_term : t -> actions -> Term.t -> unit + (** Called when a new term is added *) + val on_merge: t -> actions -> CC_eq_class.t -> CC_eq_class.t -> CC_expl.t -> unit (** Called when two classes are merged *) - *) val partial_check : t -> actions -> Lit.t Sequence.t -> unit (** Called when a literal becomes true *) @@ -87,6 +92,7 @@ type 'a t1 = (module S with type t = 'a) let make (type st) ?(check_invariants=fun _ -> ()) + ?(on_new_term=fun _ _ _ -> ()) ?(on_merge=fun _ _ _ _ _ -> ()) ?(partial_check=fun _ _ _ -> ()) ?(mk_model=fun _ _ m -> m) @@ -100,6 +106,7 @@ let make type nonrec t = st let name = name let create = create + let on_new_term = on_new_term let on_merge = on_merge let partial_check = partial_check let final_check = final_check diff --git a/src/smt/Theory_combine.ml b/src/smt/Theory_combine.ml index 42d08f44..fa7692c4 100644 --- a/src/smt/Theory_combine.ml +++ b/src/smt/Theory_combine.ml @@ -60,6 +60,7 @@ let assert_lits_ ~final (self:t) acts (lits:Lit.t Sequence.t) : unit = acts.Msat.acts_add_clause ~keep:false lits Proof_default let[@inline] add_persistent_axiom lits : unit = acts.Msat.acts_add_clause ~keep:true lits Proof_default + let[@inline] add_lit lit : unit = acts.Msat.acts_mk_lit lit end in let acts = (module A : Theory.ACTIONS) in theories self diff --git a/src/smtlib/Process.ml b/src/smtlib/Process.ml index 1f95c73b..8f474c88 100644 --- a/src/smtlib/Process.ml +++ b/src/smtlib/Process.ml @@ -8,7 +8,7 @@ type 'a or_error = ('a, string) CCResult.t module E = CCResult module A = Ast module Form = Sidekick_th_bool.Bool_term -module Distinct = Sidekick_th_distinct +module Th_distinct = Sidekick_th_distinct module Fmt = CCFormat module Dot = Msat_backend.Dot.Make(Solver.Sat_solver)(Msat_backend.Dot.Default(Solver.Sat_solver)) @@ -138,7 +138,7 @@ module Conv = struct in Form.and_l tst (curry_eq l) | A.Op (A.Distinct, l) -> - Distinct.distinct_l tst @@ List.map (aux subst) l + Th_distinct.distinct_l tst @@ List.map (aux subst) l | A.Not f -> Form.not_ tst (aux subst f) | A.Bool true -> Term.true_ tst | A.Bool false -> Term.false_ tst