From b3f328027c949b6d737d9293d79c1d3fb697e146 Mon Sep 17 00:00:00 2001 From: Simon Cruanes Date: Wed, 5 Jun 2019 20:47:58 -0500 Subject: [PATCH] wip --- src/cc/Sidekick_cc.ml | 172 +++++++++++++++++++------------------- src/core/Sidekick_core.ml | 46 ++++------ src/smtlib/Process.mli | 7 +- src/smtlib/Typecheck.ml | 4 +- src/smtlib/Typecheck.mli | 2 +- 5 files changed, 113 insertions(+), 118 deletions(-) diff --git a/src/cc/Sidekick_cc.ml b/src/cc/Sidekick_cc.ml index aa9f2a7e..608fceff 100644 --- a/src/cc/Sidekick_cc.ml +++ b/src/cc/Sidekick_cc.ml @@ -13,19 +13,6 @@ type ('f, 't, 'ts) view = ('f, 't, 'ts) View.t = module type ARG = Sidekick_core.CC_ARG module type S = Sidekick_core.CC_S -module Bits = CCBitField.Make() - -let field_is_pending = Bits.mk_field() -(** true iff the node is in the [cc.pending] queue *) - -let field_usr1 = Bits.mk_field() -(** General purpose *) - -let field_usr2 = Bits.mk_field() -(** General purpose *) - -let () = Bits.freeze() - module Make(CC_A: ARG) = struct module A = CC_A.A module CC_A = CC_A @@ -33,13 +20,42 @@ module Make(CC_A: ARG) = struct type term_state = A.Term.state type lit = A.Lit.t type fun_ = A.Fun.t - type proof = A.Proof.t - type th_data = CC_A.Data.t + type lemma = A.Lemma.t type actions = CC_A.Actions.t module T = A.Term module Fun = A.Fun + module Bits : sig + type t = private int + type field = private int + val empty : t + val mk_field : unit -> field + val inter : t -> t -> t + val union : t -> t -> t + val get : field -> t -> bool + val set : field -> t -> t + val unset : field -> t -> t + end = struct + type t = int + type field = int + let max_width = Sys.word_size - 2 + + let mk_field = + let n_ = ref 0 in + fun () -> let x = 1 lsl !n_ in incr n_; x + + let empty = 0 + let[@inline] get f x = x land f <> 0 + let[@inline] set f x = x lor f + let[@inline] unset f x = x land (lnot f) + let[@inline] union x y = x lor y + let[@inline] inter x y = x land y + end + + let field_is_pending = Bits.mk_field() + (** true iff the node is in the [cc.pending] queue *) + (** A node of the congruence closure. An equivalence class is represented by its "root" element, the representative. *) @@ -51,9 +67,8 @@ module Make(CC_A: ARG) = struct mutable n_root: node; (* representative of congruence class (itself if a representative) *) mutable n_next: node; (* pointer to next element of congruence class *) mutable n_size: int; (* size of the class *) - mutable n_as_lit: lit option; (* TODO: put into payload? and only in root? *) + mutable n_as_lit: lit option; mutable n_expl: explanation_forest_link; (* the rooted forest for explanations *) - mutable n_th_data: th_data; (* theory data *) } and signature = (fun_, node, node list) view @@ -85,7 +100,6 @@ module Make(CC_A: ARG) = struct let[@inline] term n = n.n_term let[@inline] pp out n = T.pp out n.n_term let[@inline] as_lit n = n.n_as_lit - let[@inline] th_data n = n.n_th_data let make (t:term) : t = let rec n = { @@ -98,7 +112,6 @@ module Make(CC_A: ARG) = struct n_expl=FL_none; n_next=n; n_size=1; - n_th_data=CC_A.Data.empty; } in n @@ -122,12 +135,8 @@ module Make(CC_A: ARG) = struct Bag.to_seq n.n_parents let[@inline] get_field f t = Bits.get f t.n_bits - let[@inline] set_field f b t = t.n_bits <- Bits.set f b t.n_bits - - let[@inline] get_field_usr1 t = get_field field_usr1 t - let[@inline] set_field_usr1 t b = set_field field_usr1 b t - let[@inline] get_field_usr2 t = get_field field_usr2 t - let[@inline] set_field_usr2 t b = set_field field_usr2 b t + let[@inline] set_field f t = t.n_bits <- Bits.set f t.n_bits + let[@inline] unset_field f t = t.n_bits <- Bits.unset f t.n_bits end module N_tbl = CCHashtbl.Make(N) @@ -227,7 +236,7 @@ module Make(CC_A: ARG) = struct pending: node Vec.t; combine: combine_task Vec.t; undo: (unit -> unit) Backtrack_stack.t; - mutable on_merge: ev_on_merge list; + mutable on_merge: (Bits.field * ev_on_merge) list; mutable on_new_term: ev_on_new_term list; mutable ps_lits: lit list; (* TODO: thread it around instead? *) (* proof state *) @@ -245,8 +254,8 @@ module Make(CC_A: ARG) = struct several times. See "fast congruence closure and extensions", Nieuwenhis&al, page 14 *) - and ev_on_merge = t -> N.t -> th_data -> N.t -> th_data -> Expl.t -> unit - and ev_on_new_term = t -> N.t -> term -> th_data option + and ev_on_merge = t -> N.t -> N.t -> Expl.t -> unit + and ev_on_new_term = t -> N.t -> term -> unit let[@inline] size_ (r:repr) = r.n_size let[@inline] true_ cc = Lazy.force cc.true_ @@ -329,7 +338,7 @@ module Make(CC_A: ARG) = struct let push_pending cc t : unit = if not @@ N.get_field field_is_pending t then ( Log.debugf 5 (fun k->k "(@[cc.push_pending@ %a@])" N.pp t); - N.set_field field_is_pending true t; + N.set_field field_is_pending t; Vec.push cc.pending t ) @@ -354,11 +363,11 @@ module Make(CC_A: ARG) = struct let raise_conflict (cc:t) (acts:actions) (e:conflict) : _ = (* clear tasks queue *) - Vec.iter (N.set_field field_is_pending false) cc.pending; + Vec.iter (N.unset_field field_is_pending) cc.pending; Vec.clear cc.pending; Vec.clear cc.combine; Stat.incr cc.count_conflict; - CC_A.Actions.raise_conflict acts e A.Proof.default + CC_A.Actions.raise_conflict acts e A.Lemma.default let[@inline] all_classes cc : repr Iter.t = T_tbl.values cc.tbl @@ -502,16 +511,7 @@ module Make(CC_A: ARG) = struct (* [n] might be merged with other equiv classes *) push_pending cc n; ); - (* initial theory data *) - let th_data = - List.fold_left - (fun data f -> - match f cc n t with - | None -> data - | Some d -> CC_A.Data.merge data d) - CC_A.Data.empty cc.on_new_term - in - n.n_th_data <- th_data; + List.iter (fun f -> f cc n t) cc.on_new_term; (* notify *) n (* compute the initial signature of the given node *) @@ -572,7 +572,7 @@ module Make(CC_A: ARG) = struct done and task_pending_ cc (n:node) : unit = - N.set_field field_is_pending false n; + N.unset_field field_is_pending n; (* check if some parent collided *) begin match n.n_sig0 with | None -> () (* no-op *) @@ -654,17 +654,21 @@ module Make(CC_A: ARG) = struct Log.debugf 15 (fun k->k "(@[cc.merge@ :from %a@ :into %a@])" N.pp r_from N.pp r_into); (* call [on_merge] functions, and merge theory data items *) begin - let th_into = r_into.n_th_data in - let th_from = r_from.n_th_data in - let new_data = CC_A.Data.merge th_into th_from in + let bits_into = r_into.n_bits in + let bits_from = r_from.n_bits in + let inter = Bits.inter bits_into bits_from in + let union = Bits.union bits_into bits_from in (* restore old data, if it changed *) - if new_data != th_into then ( - on_backtrack cc (fun () -> r_into.n_th_data <- th_into); + if union != bits_into then ( + on_backtrack cc (fun () -> r_into.n_bits <- bits_into); ); - r_into.n_th_data <- new_data; - (* explanation is [a=ra & e_ab & b=rb] *) + r_into.n_bits <- union; + (* call merge handlers with explanation [a=ra & e_ab & b=rb]. + Only do so for handlers whose bit is on for both classes. *) let expl = Expl.mk_list [e_ab; Expl.mk_merge a ra; Expl.mk_merge b rb] in - List.iter (fun f -> f cc r_into th_into r_from th_from expl) cc.on_merge; + List.iter (fun (f_field,f) -> + if Bits.get f_field inter then f cc r_into r_from expl) + cc.on_merge; end; begin (* parents might have a different signature, check for collisions *) @@ -740,7 +744,7 @@ module Make(CC_A: ARG) = struct let e = explain_eq_n ~init:(Lazy.force half_expl) cc u1 t1 in List.iter yield e in - CC_A.Actions.propagate acts lit ~reason A.Proof.default + CC_A.Actions.propagate acts lit ~reason A.Lemma.default | _ -> ()) module Theory = struct @@ -760,39 +764,39 @@ module Make(CC_A: ARG) = struct let add_term = add_term end - let check_invariants_ (cc:t) = - Log.debug 5 "(cc.check-invariants)"; - Log.debugf 15 (fun k-> k "%a" pp_full cc); - assert (T.equal (T.bool cc.tst true) (true_ cc).n_term); - assert (T.equal (T.bool cc.tst false) (false_ cc).n_term); - assert (not @@ same_class (true_ cc) (false_ cc)); - assert (Vec.is_empty cc.combine); - assert (Vec.is_empty cc.pending); - (* check that subterms are internalized *) - T_tbl.iter - (fun t n -> - assert (T.equal t n.n_term); - assert (not @@ N.get_field field_is_pending n); - assert (N.equal n.n_root n.n_next.n_root); - (* check proper signature. - note that some signatures in the sig table can be obsolete (they - were not removed) but there must be a valid, up-to-date signature for - each term *) - begin match CCOpt.map update_sig n.n_sig0 with - | None -> () - | Some s -> - Log.debugf 15 (fun k->k "(@[cc.check-sig@ %a@ :sig %a@])" T.pp t Signature.pp s); - (* add, but only if not present already *) - begin match Sig_tbl.find cc.signatures_tbl s with - | exception Not_found -> assert false - | repr_s -> assert (same_class n repr_s) - end - end; - ) - cc.tbl; - () - module Debug_ = struct + let check_invariants_ (cc:t) = + Log.debug 5 "(cc.check-invariants)"; + Log.debugf 15 (fun k-> k "%a" pp_full cc); + assert (T.equal (T.bool cc.tst true) (true_ cc).n_term); + assert (T.equal (T.bool cc.tst false) (false_ cc).n_term); + assert (not @@ same_class (true_ cc) (false_ cc)); + assert (Vec.is_empty cc.combine); + assert (Vec.is_empty cc.pending); + (* check that subterms are internalized *) + T_tbl.iter + (fun t n -> + assert (T.equal t n.n_term); + assert (not @@ N.get_field field_is_pending n); + assert (N.equal n.n_root n.n_next.n_root); + (* check proper signature. + note that some signatures in the sig table can be obsolete (they + were not removed) but there must be a valid, up-to-date signature for + each term *) + begin match CCOpt.map update_sig n.n_sig0 with + | None -> () + | Some s -> + Log.debugf 15 (fun k->k "(@[cc.check-sig@ %a@ :sig %a@])" T.pp t Signature.pp s); + (* add, but only if not present already *) + begin match Sig_tbl.find cc.signatures_tbl s with + | exception Not_found -> assert false + | repr_s -> assert (same_class n repr_s) + end + end; + ) + cc.tbl; + () + let[@inline] check_invariants (cc:t) : unit = if Util._CHECK_INVARIANTS then check_invariants_ cc let pp out _ = Fmt.string out "cc" @@ -806,7 +810,7 @@ module Make(CC_A: ARG) = struct Backtrack_stack.push_level self.undo let pop_levels (self:t) n : unit = - Vec.iter (N.set_field field_is_pending false) self.pending; + Vec.iter (N.unset_field field_is_pending) self.pending; Vec.clear self.pending; Vec.clear self.combine; Log.debugf 15 diff --git a/src/core/Sidekick_core.ml b/src/core/Sidekick_core.ml index 1cc50814..7379b6f6 100644 --- a/src/core/Sidekick_core.ml +++ b/src/core/Sidekick_core.ml @@ -117,7 +117,7 @@ module type CORE_TYPES = sig val pp : t Fmt.printer end - module Proof : sig + module Lemma : sig type t val pp : t Fmt.printer @@ -136,20 +136,12 @@ module type CC_ARG = sig val cc_view : Term.t -> (Fun.t, Term.t, Term.t Iter.t) CC_view.t (** View the term through the lens of the congruence closure *) - (** Monoid embedded in every node *) - module Data : sig - type t - val merge : t -> t -> t - val pp : t Fmt.printer - val empty : t - end - module Actions : sig type t - val raise_conflict : t -> Lit.t list -> Proof.t -> 'a + val raise_conflict : t -> Lit.t list -> Lemma.t -> 'a - val propagate : t -> Lit.t -> reason:Lit.t Iter.t -> Proof.t -> unit + val propagate : t -> Lit.t -> reason:Lit.t Iter.t -> Lemma.t -> unit end end @@ -160,8 +152,7 @@ module type CC_S = sig type term = A.Term.t type fun_ = A.Fun.t type lit = A.Lit.t - type proof = A.Proof.t - type th_data = CC_A.Data.t + type lemma = A.Lemma.t type actions = CC_A.Actions.t type t @@ -197,19 +188,6 @@ module type CC_S = sig val iter_class : t -> t Iter.t (** Traverse the congruence class. Precondition: [is_root n] (see {!find} below) *) - - val iter_parents : t -> t Iter.t - (** Traverse the parents of the class. - Precondition: [is_root n] (see {!find} below) *) - - val th_data : t -> th_data - (** Access theory data for this node *) - - val get_field_usr1 : t -> bool - val set_field_usr1 : t -> bool -> unit - - val get_field_usr2 : t -> bool - val set_field_usr2 : t -> bool -> unit end module Expl : sig @@ -261,8 +239,8 @@ module type CC_S = sig To be used in theories *) end - type ev_on_merge = t -> N.t -> th_data -> N.t -> th_data -> Expl.t -> unit - type ev_on_new_term = t -> N.t -> term -> th_data option + type ev_on_merge = t -> N.t -> N.t -> Expl.t -> unit + type ev_on_new_term = t -> N.t -> term -> unit val create : ?stat:Stat.t -> @@ -351,7 +329,7 @@ module type SOLVER_INTERNAL = sig type lit = A.Lit.t type term = A.Term.t type term_state = A.Term.state - type proof = A.Proof.t + type lemma = A.Lemma.t (** {3 Main type for a solver} *) type t @@ -500,7 +478,7 @@ module type SOLVER = sig type term = A.Term.t type ty = A.Ty.t type lit = A.Lit.t - type proof = A.Proof.t + type lemma = A.Lemma.t type value = A.Value.t (** {3 A theory} @@ -582,6 +560,14 @@ module type SOLVER = sig *) end + module Proof : sig + type t + (* TODO: expose more? *) + + end + + type proof = Proof.t + (** {3 Main API} *) val stats : t -> Stat.t diff --git a/src/smtlib/Process.mli b/src/smtlib/Process.mli index 46c20333..7c585851 100644 --- a/src/smtlib/Process.mli +++ b/src/smtlib/Process.mli @@ -1,7 +1,12 @@ (** {1 Process Statements} *) -open Sidekick_smt +open Sidekick_base_term + +module Solver : Sidekick_msat_solver.S + with type A.Term.t = Term.t + and type A.Ty.t = Ty.t + and type A.Fun.t = Cst.t type 'a or_error = ('a, string) CCResult.t diff --git a/src/smtlib/Typecheck.ml b/src/smtlib/Typecheck.ml index c96bc106..2487397d 100644 --- a/src/smtlib/Typecheck.ml +++ b/src/smtlib/Typecheck.ml @@ -3,12 +3,12 @@ (** {1 Preprocessing AST} *) -module ID = Sidekick_smt.ID +module ID = Sidekick_base_term.ID module Loc = Locations module Fmt = CCFormat module Log = Msat.Log -module A = Sidekick_smt.Ast +module A = Sidekick_base_term.Ast module PA = Parse_ast type 'a or_error = ('a, string) CCResult.t diff --git a/src/smtlib/Typecheck.mli b/src/smtlib/Typecheck.mli index 9c295dfa..12d33b61 100644 --- a/src/smtlib/Typecheck.mli +++ b/src/smtlib/Typecheck.mli @@ -16,7 +16,7 @@ module Ctx : sig end module PA = Parse_ast -module A = Sidekick_smt.Ast +module A = Sidekick_base_term.Ast val conv_term : Ctx.t -> PA.term -> A.term