From 949e0798670d1d45b5ead5d3a1c5cb832c06b46a Mon Sep 17 00:00:00 2001 From: Simon Cruanes Date: Sat, 23 Nov 2019 10:51:04 -0600 Subject: [PATCH 01/29] wip: add datatypes --- src/smtlib/Process.ml | 5 +- src/th-data/Sidekick_th_data.ml | 513 ++++++++++++++++++++++++++++++++ src/th-data/dune | 8 + 3 files changed, 524 insertions(+), 2 deletions(-) create mode 100644 src/th-data/Sidekick_th_data.ml create mode 100644 src/th-data/dune diff --git a/src/smtlib/Process.ml b/src/smtlib/Process.ml index 90efbed7..4852eb81 100644 --- a/src/smtlib/Process.ml +++ b/src/smtlib/Process.ml @@ -258,11 +258,12 @@ let process_stmt Error.errorf "cannot deal with definitions yet" end -module Th_cstor = Sidekick_th_cstor.Make(struct +module Th_data = Sidekick_th_data.Make(struct module S = Solver open Base_types - open Sidekick_th_cstor + open Sidekick_th_data + (* TODO*) let view_as_cstor t = match Term.view t with | Term.App_fun ({fun_view=Fun.Fun_cstor _;_} as f, args) -> T_cstor (f, args) | _ -> T_other t diff --git a/src/th-data/Sidekick_th_data.ml b/src/th-data/Sidekick_th_data.ml new file mode 100644 index 00000000..397eda23 --- /dev/null +++ b/src/th-data/Sidekick_th_data.ml @@ -0,0 +1,513 @@ + +(** {1 Theory for datatypes} *) + +(** {2 Views} *) + +(** Datatype-oriented view of terms. + ['c] is the representation of constructors + ['t] is the representation of terms +*) +type ('c,'t) data_view = + | T_cstor of 'c * 't IArray.t + | T_select of 'c * int * 't + | T_is_a of 'c * 't + | T_other of 't + +(** View of types in a way that is directly useful for the theory of datatypes *) +type ('c, 'ty) data_ty_view = + | Ty_arrow of 'ty Iter.t * 'ty + | Ty_app of { + args: 'ty Iter.t; + } + | Ty_data of { + cstors: 'c list; + } + | Ty_other + +let name = "th-data" + +(** {2 Cardinality of types} *) + +module Ty_card = struct + type t = + | Finite + | Infinite + + let (+) a b = match a, b with Finite, Finite -> Finite | _ -> Infinite + let ( * ) a b = match a, b with Finite, Finite -> Finite | _ -> Infinite + let ( ^ ) a b = match a, b with Finite, Finite -> Finite | _ -> Infinite + let finite = Finite + let infinite = Infinite + + let sum = Iter.fold (+) Finite + let product = Iter.fold ( * ) Finite + + let equal : t -> t -> bool = (=) + let compare : t -> t -> int = Pervasives.compare + let pp out = function + | Finite -> Fmt.string out "finite" + | Infinite -> Fmt.string out "infinite" +end + +(** An abtract representation of a datatype *) +module type DATA_TY = sig + type t + type cstor + + val equal : t -> t -> bool + + val view : t -> (cstor, t) data_ty_view + + val cstor_args : cstor -> t Iter.t + + (** A table indexed by types. *) + module Tbl : Hashtbl.S with type key = t +end + +(** Helper to compute the cardinality of types *) +module Compute_card(Ty : DATA_TY) : sig + type t + val create : unit -> t + val card : t -> Ty.t -> Ty_card.t +end = struct + module Card = Ty_card + type t = { + cards: Card.t Ty.Tbl.t; + } + + let create() : t = { cards=Ty.Tbl.create 16} + + let card (self:t) (ty:Ty.t) : Card.t = + let rec aux (ty:Ty.t) : Card.t = + match Ty.Tbl.find self.cards ty with + | c -> c + | exception Not_found -> + Ty.Tbl.add self.cards ty Card.infinite; (* temp value, for fixpoint computation *) + let c = match Ty.view ty with + | Ty_other -> Card.finite + | Ty_app {args} -> Iter.map aux args |> Card.product + | Ty_arrow (args,ret) -> + Card.( (aux ret) ^ (Card.product @@ Iter.map aux args)) + | Ty_data { cstors; } -> + cstors + |> Iter.of_list + |> Iter.map (fun c -> Card.product (Iter.map aux @@ Ty.cstor_args c)) + |> Card.sum + in + Ty.Tbl.replace self.cards ty c; + c + in + aux ty +end + +module type ARG = sig + module S : Sidekick_core.SOLVER + val view_as_cstor : S.T.Term.t -> (S.T.Fun.t, S.T.Term.t) cstor_view + val mk_cstor : S.T.Term.state -> S.T.Fun.t -> S.T.Term.t IArray.t -> S.T.Term.t + val as_datatype : S.T.Ty.t -> S.T.Fun.t list option +end + +module type S = sig + module A : ARG + val theory : A.S.theory +end + +module Make(A : ARG) : S with module A = A = struct + module A = A + module SI = A.S.Solver_internal + module T = A.S.T.Term + module N = SI.CC.N + module Fun = A.S.T.Fun + module Expl = SI.CC.Expl + + type cstor_repr = { + t: T.t; + n: N.t; + cstor: Fun.t; + args: T.t IArray.t; + } + (* associate to each class a unique constructor term in the class (if any) *) + + module N_tbl = Backtrackable_tbl.Make(N) + + type t = { + cstors: cstor_repr N_tbl.t; (* repr -> cstor for the class *) + (* TODO: also allocate a bit in CC to filter out quickly classes without cstors? *) + } + + let push_level self = N_tbl.push_level self.cstors + let pop_levels self n = N_tbl.pop_levels self.cstors n + + (* attach data to constructor terms *) + let on_new_term self _solver n (t:T.t) = + match A.view_as_cstor t with + | T_cstor (cstor,args) -> + Log.debugf 20 + (fun k->k "(@[th-cstor.on-new-term@ %a@ :cstor %a@ @[:args@ (@[%a@])@]@]@])" + T.pp t Fun.pp cstor (Util.pp_iarray T.pp) args); + N_tbl.add self.cstors n {n; t; cstor; args}; + | _ -> () + + let on_pre_merge (self:t) cc acts n1 n2 e_n1_n2 : unit = + begin match N_tbl.get self.cstors n1, N_tbl.get self.cstors n2 with + | Some cr1, Some cr2 -> + Log.debugf 5 + (fun k->k "(@[th-cstor.on_pre_merge@ @[:c1 %a@ (term %a)@]@ @[:c2 %a@ (term %a)@]@])" + N.pp n1 T.pp cr1.t N.pp n2 T.pp cr2.t); + (* build full explanation of why the constructor terms are equal *) + let expl = + Expl.mk_list [ + e_n1_n2; + Expl.mk_merge n1 cr1.n; + Expl.mk_merge n2 cr2.n; + ] + in + if Fun.equal cr1.cstor cr2.cstor then ( + (* same function: injectivity *) + assert (IArray.length cr1.args = IArray.length cr2.args); + IArray.iter2 + (fun u1 u2 -> SI.CC.merge_t cc u1 u2 expl) + cr1.args cr2.args + ) else ( + (* different function: disjointness *) + SI.CC.raise_conflict_from_expl cc acts expl + ) + | None, Some cr -> + N_tbl.add self.cstors n1 cr + | Some _, None -> () (* already there on the left *) + | None, None -> () + end + + let create_and_setup (solver:SI.t) : t = + let self = { + cstors=N_tbl.create ~size:32 (); + } in + Log.debug 1 "(setup :th-cstor)"; + SI.on_cc_new_term solver (on_new_term self); + SI.on_cc_pre_merge solver (on_pre_merge self); + self + + let theory = + A.S.mk_theory ~name ~push_level ~pop_levels ~create_and_setup () +end + +(* +module Datatype(A : Congruence_closure.THEORY_ACTION) + : Congruence_closure.THEORY with module A=A = struct + module A = A + + (* merge equiv classes: + - injectivity rule on normal forms + - check consistency of normal forms + - intersection of label sets *) + let merge (ra:A.repr) (rb:A.repr) expls = + begin match A.nf ra, A.nf rb with + | Some (NF_cstor (c1, args1)), Some (NF_cstor (c2, args2)) -> + if Cst.equal c1.cstor_cst c2.cstor_cst then ( + (* unify arguments recursively, by injectivity *) + assert (IArray.length args1 = IArray.length args2); + IArray.iter2 + (fun sub1 sub2 -> + A.add_eqn sub1 sub2 + (CC_injectivity (A.term_of_repr ra, A.term_of_repr rb))) + args1 args2; + ) else ( + A.unsat expls + ) + | _ -> () + end; + (* TODO: intersect label sets *) + (* TODO: check if Split2 applies *) + () + + type map_status = + | Map_empty + | Map_single of data_cstor + | Map_other + + type labels = data_cstor ID.Map.t + + (* check if set of cstors is empty or unary *) + let map_status (m: labels): map_status = + if ID.Map.is_empty m then Map_empty + else ( + let c, cstor = ID.Map.choose m in + let m' = ID.Map.remove c m in + if ID.Map.is_empty m' + then Map_single cstor + else Map_other + ) + + (* propagate [r = cstor], using Instantiation rules *) + let propagate_cstor (r:A.repr) (cstor:data_cstor) (expl:cc_explanation list): unit = + Log.debugf 5 + (fun k->k "(@[propagate_cstor@ %a@ %a: expl: (@[%a@])@])" + Term.pp (A.term_of_repr r) Cst.pp cstor.cstor_cst + (Util.pp_list pp_cc_explanation) expl); + (* TODO: propagate, add_eqn with cstor term, but only + if either: + - cstor is finite + - or some parent term of [r_u] is a selector. + + We need to create new constants for the arguments *) + assert false + + (* perform (Split 2) if all the cstors of [m] (labels of [r]) are finite + and (Split 1) was not applied on [r] *) + let maybe_split (r:A.repr) (m: labels) (expl:cc_explanation list): unit = + assert (ID.Map.cardinal m >= 2); + if ID.Map.for_all (fun _ cstor -> Cst.is_finite_cstor cstor.cstor_cst) m + && not (Term_bits.get Term.field_is_split (A.term_of_repr r).term_bits) + then ( + Log.debugf 5 + (fun k->k "(@[split_finite@ %a@ cstors: (@[%a@])@ expl: (@[%a@])@])" + Term.pp (A.term_of_repr r) (Util.pp_list Cst.pp) + (ID.Map.values m |> Sequence.map (fun c->c.cstor_cst) |> Sequence.to_list) + (Util.pp_list pp_cc_explanation) expl); + let lits = + ID.Map.values m + |> Sequence.map + (fun cstor -> Lit.cstor_test cstor (A.term_of_repr r)) + |> Sequence.to_list + in + A.split lits expl + ) + + let set_nf t nf (e:cc_explanation): unit = match nf, t.term_cell with + | NF_bool sign, App_cst ({cst_kind=Cst_test (_, lazy cstor); _}, args) -> + (* update set of possible cstors for [A.find args.(0)] + if [t = is-cstor args] is true/false *) + assert (IArray.length args = 1); + let u = IArray.get args 1 in + let r_u = A.find u in + let cstor_set, expl = match (A.term_of_repr r_u).term_cases_set with + | TC_cstors (m,e') -> m,e' + | _ -> assert false + in + let new_expl = e::expl in + let cstor_id = cstor.cstor_cst.cst_id in + if sign then ( + if ID.Map.mem cstor_id cstor_set then ( + (* unit propagate now *) + propagate_cstor r_u cstor new_expl + ) else ( + A.unsat new_expl (* conflict: *) + ) + ) else ( + (* remove [cstor] from the set *) + if ID.Map.mem cstor_id cstor_set then ( + Log.debugf 5 + (fun k->k "(@[remove_cstor@ %a@ from %a@])" ID.pp cstor_id Term.pp u); + let new_set = ID.Map.remove cstor_id cstor_set in + begin match map_status new_set with + | Map_empty -> + A.unsat new_expl (* conflict *) + | Map_single cstor' -> + propagate_cstor r_u cstor' new_expl; + | Map_other -> + (* just update set of labels *) + if Backtrack.not_at_level_0 () then ( + let old_cases = (A.term_of_repr r_u).term_cases_set in + Backtrack.push_undo (fun () -> (A.term_of_repr r_u).term_cases_set <- old_cases); + ); + (A.term_of_repr r_u).term_cases_set <- TC_cstors (new_set, new_expl); + maybe_split r_u new_set new_expl + end + ) + ) + | _ -> () + + let eval t = match t.term_cell with + | Case (u, m) -> + let r_u = A.find u in + begin match A.nf r_u with + | Some (NF_cstor (c, _)) -> + (* reduce to the proper branch *) + let rhs = + try ID.Map.find c.cstor_cst.cst_id m + with Not_found -> assert false + in + A.add_eqn t rhs (CC_reduce_nf u); + | Some (NF_bool _) -> assert false + | None -> () + end + | App_cst ({cst_kind=Cst_test(_,lazy cstor); _}, a) when IArray.length a=1 -> + (* check if [a.(0)] has a constructor *) + let arg = IArray.get a 0 in + let r_a = A.find arg in + begin match A.nf r_a with + | None -> () + | Some (NF_cstor (cstor', _)) -> + (* reduce to true/false depending on whether [cstor=cstor'] *) + if Cst.equal cstor.cstor_cst cstor'.cstor_cst then ( + A.add_eqn t Term.true_ (CC_reduce_nf arg) + ) else ( + A.add_eqn t Term.true_ (CC_reduce_nf arg) + ) + | Some (NF_bool _) -> assert false + end + | App_cst ({cst_kind=Cst_proj(_,lazy cstor,i); _}, a) when IArray.length a=1 -> + (* reduce if [a.(0)] has the proper constructor *) + let arg = IArray.get a 0 in + let r_a = A.find arg in + begin match A.nf r_a with + | None -> () + | Some (NF_cstor (cstor', nf_cstor_args)) -> + (* [proj-C-i (C t1...tn) = ti] *) + if Cst.equal cstor.cstor_cst cstor'.cstor_cst then ( + A.add_eqn t (IArray.get nf_cstor_args i) (CC_reduce_nf arg) + ) + | Some (NF_bool _) -> assert false + end + | _ -> () + + let is_evaluable t = match t.term_cell with + | Case _ -> true + | App_cst ({cst_kind=Cst_test(_,_); _}, a) + | App_cst ({cst_kind=Cst_proj(_,_,_); _}, a) -> + IArray.length a=1 + | _ -> false + + (* split every term that is not split yet, and to which some selectors + are applied *) + let split_rule () = + let is_in_proj (r:A.repr): bool = + Bag.to_seq (A.term_of_repr r).term_parents + |> Sequence.exists + (fun parent -> match parent.term_cell with + | App_cst ({cst_kind=Cst_proj _; _}, a) -> + let res = IArray.length a = 1 in + (* invariant: a.(0) == r should hold *) + if res then assert(A.equal_repr r (IArray.get a 1 |> A.find)); + res + | _ -> false) + in + begin + Log.debug 3 "(data.split1)"; + A.all_classes + |> Sequence.filter + (fun (r:A.repr) -> + (* keep only terms of data-type, never split, with at least + two possible cases in their label, and that occur in + at least one selector *) + Format.printf "check %a@." Term.pp (A.term_of_repr r); + Ty.is_data (A.term_of_repr r).term_ty + && + begin match (A.term_of_repr r).term_cases_set with + | TC_cstors (m, _) -> ID.Map.cardinal m >= 2 + | _ -> assert false + end + && + not (Term_bits.get Term.field_is_split (A.term_of_repr r).term_bits) + && + is_in_proj r) + |> Sequence.iter + (fun r -> + let r = A.term_of_repr r in + Log.debugf 5 (fun k->k "(@[split_1@ term: %a@])" Term.pp r); + (* unconditional split: consider all cstors *) + let cstors = match r.term_ty.ty_cell with + | Atomic (_, Data {data_cstors=lazy cstors;_}) -> cstors + | _ -> assert false + in + let lits = + ID.Map.values cstors + |> Sequence.map (fun cstor -> Lit.cstor_test cstor r) + |> Sequence.to_list + in + r.term_bits <- Term_bits.set Term.field_is_split true r.term_bits; + A.split lits []) + end + + (* TODO acyclicity rule + could be done by traversing the set of terms, assigning a "level" to + each equiv class. If level clash, find why, return conflict. + *) + + let final_check (): unit = + split_rule (); + (* TODO: acyclicity *) + () +end + + + + | Ast.Data l -> + (* the datatypes in [l]. Used for computing cardinalities *) + let in_same_block : ID.Set.t = + List.map (fun {Ast.Ty.data_id; _} -> data_id) l |> ID.Set.of_list + in + (* declare the type, and all the constructors *) + List.iter + (fun {Ast.Ty.data_id; data_cstors} -> + let ty = lazy ( + let card_ : ty_card ref = ref Finite in + let cstors = lazy ( + data_cstors + |> ID.Map.map + (fun c -> + let c_id = c.Ast.Ty.cstor_id in + let ty_c = conv_ty c.Ast.Ty.cstor_ty in + let ty_args, ty_ret = Ty.unfold ty_c in + (* add cardinality of [c] to the cardinality of [data_id]. + (product of cardinalities of args) *) + let cstor_card = + ty_args + |> List.map + (fun ty_arg -> match ty_arg.ty_cell with + | Atomic (id, _) when ID.Set.mem id in_same_block -> + Infinite + | _ -> Lazy.force ty_arg.ty_card) + |> Ty_card.product + in + card_ := Ty_card.( !card_ + cstor_card ); + let rec cst = lazy ( + Cst.make_cstor c_id ty_c cstor + ) and cstor = lazy ( + let cstor_proj = lazy ( + let n = ref 0 in + List.map2 + (fun id ty_arg -> + let ty_proj = Ty.arrow ty_ret ty_arg in + let i = !n in + incr n; + Cst.make_proj id ty_proj cstor i) + c.Ast.Ty.cstor_proj ty_args + |> IArray.of_list + ) in + let cstor_test = lazy ( + let ty_test = Ty.arrow ty_ret Ty.prop in + Cst.make_tester c.Ast.Ty.cstor_test ty_test cstor + ) in + { cstor_ty=ty_c; cstor_cst=Lazy.force cst; + cstor_args=IArray.of_list ty_args; + cstor_proj; cstor_test; cstor_card; } + ) in + ID.Tbl.add decl_ty_ c_id cst; (* declare *) + Lazy.force cstor) + ) + in + let data = { data_cstors=cstors; } in + let card = lazy ( + ignore (Lazy.force cstors); + let r = !card_ in + Log.debugf 5 + (fun k->k "(@[card_of@ %a@ %a@])" ID.pp data_id Ty_card.pp r); + r + ) in + Ty.atomic data_id (Data data) ~card + ) in + ID.Tbl.add ty_tbl_ data_id ty; + ) + l; + (* force evaluation *) + List.iter + (fun {Ast.Ty.data_id; _} -> + let lazy ty = ID.Tbl.find ty_tbl_ data_id in + ignore (Lazy.force ty.ty_card); + begin match ty.ty_cell with + | Atomic (_, Data {data_cstors=lazy _; _}) -> () + | _ -> assert false + end) + l + *) diff --git a/src/th-data/dune b/src/th-data/dune new file mode 100644 index 00000000..35e07fee --- /dev/null +++ b/src/th-data/dune @@ -0,0 +1,8 @@ + + +(library + (name Sidekick_th_data) + (public_name sidekick.th-data) + (libraries containers sidekick.core sidekick.util) + (flags :standard -open Sidekick_util)) + From 8c5e28da2878cf3b2c10d025e756f7df8867bb8b Mon Sep 17 00:00:00 2001 From: Simon Cruanes Date: Sat, 23 Nov 2019 16:20:53 -0600 Subject: [PATCH 02/29] wip: theory of datatypes --- src/base-term/Base_types.ml | 1 + src/main/main.ml | 2 +- src/smtlib/Process.ml | 14 +++++++++++--- src/smtlib/Process.mli | 2 +- src/smtlib/dune | 2 +- src/th-data/Sidekick_th_data.ml | 25 +++++++++++++++++-------- src/th-data/types.ml | 2 ++ 7 files changed, 34 insertions(+), 14 deletions(-) diff --git a/src/base-term/Base_types.ml b/src/base-term/Base_types.ml index fa3449ef..e9ed2637 100644 --- a/src/base-term/Base_types.ml +++ b/src/base-term/Base_types.ml @@ -977,6 +977,7 @@ module Cstor = struct cstor_ty: ty lazy_t; } let equal = eq_cstor + let pp out c = ID.pp out c.cstor_id end module Select = struct diff --git a/src/main/main.ml b/src/main/main.ml index f22e3185..5f4adf3d 100644 --- a/src/main/main.ml +++ b/src/main/main.ml @@ -143,7 +143,7 @@ let main () = let theories = if is_cnf then [] else [ Process.th_bool ; - Process.th_cstor; + Process.th_data; ] in Process.Solver.create ~store_proof:!check ~theories tst () diff --git a/src/smtlib/Process.ml b/src/smtlib/Process.ml index 4852eb81..98c7890b 100644 --- a/src/smtlib/Process.ml +++ b/src/smtlib/Process.ml @@ -262,11 +262,19 @@ module Th_data = Sidekick_th_data.Make(struct module S = Solver open Base_types open Sidekick_th_data + module Cstor = Cstor + + let as_datatype ty = match Ty.view ty with + | Ty_atomic {def=Ty_data data;_} -> + Some (Lazy.force data.data_cstors |> ID.Map.values) + | _ -> None (* TODO*) - let view_as_cstor t = match Term.view t with - | Term.App_fun ({fun_view=Fun.Fun_cstor _;_} as f, args) -> T_cstor (f, args) + let view_as_data t = match Term.view t with + | Term.App_fun ({fun_view=Fun.Fun_cstor c;_}, args) -> T_cstor (c, args) | _ -> T_other t + + let mk_cstor tst c args : Term.t = Term.app_fun tst (Fun.cstor c) args end) module Th_bool = Sidekick_th_bool_static.Make(struct @@ -276,4 +284,4 @@ module Th_bool = Sidekick_th_bool_static.Make(struct end) let th_bool : Solver.theory = Th_bool.theory -let th_cstor : Solver.theory = Th_cstor.theory +let th_data : Solver.theory = Th_data.theory diff --git a/src/smtlib/Process.mli b/src/smtlib/Process.mli index 8b8f5972..ec8a2084 100644 --- a/src/smtlib/Process.mli +++ b/src/smtlib/Process.mli @@ -8,7 +8,7 @@ module Solver and type T.Ty.t = Ty.t val th_bool : Solver.theory -val th_cstor : Solver.theory +val th_data : Solver.theory type 'a or_error = ('a, string) CCResult.t diff --git a/src/smtlib/dune b/src/smtlib/dune index 36d4e020..9809d72a 100644 --- a/src/smtlib/dune +++ b/src/smtlib/dune @@ -3,7 +3,7 @@ (public_name sidekick-bin.smtlib) (libraries containers zarith msat sidekick.core sidekick.util sidekick.msat-solver sidekick.base-term sidekick.th-bool-static - sidekick.mini-cc sidekick.th-cstor msat.backend smtlib-utils) + sidekick.mini-cc sidekick.th-data msat.backend smtlib-utils) (flags :standard -warn-error -27-37 -open Sidekick_util)) ; TODO: enable warn-error again diff --git a/src/th-data/Sidekick_th_data.ml b/src/th-data/Sidekick_th_data.ml index 397eda23..8e539fb8 100644 --- a/src/th-data/Sidekick_th_data.ml +++ b/src/th-data/Sidekick_th_data.ml @@ -102,9 +102,15 @@ end module type ARG = sig module S : Sidekick_core.SOLVER - val view_as_cstor : S.T.Term.t -> (S.T.Fun.t, S.T.Term.t) cstor_view - val mk_cstor : S.T.Term.state -> S.T.Fun.t -> S.T.Term.t IArray.t -> S.T.Term.t - val as_datatype : S.T.Ty.t -> S.T.Fun.t list option + + module Cstor : sig + type t + val pp : t Fmt.printer + val equal : t -> t -> bool + end + val view_as_data : S.T.Term.t -> (Cstor.t, S.T.Term.t) data_view + val mk_cstor : S.T.Term.state -> Cstor.t -> S.T.Term.t IArray.t -> S.T.Term.t + val as_datatype : S.T.Ty.t -> Cstor.t Iter.t option end module type S = sig @@ -123,7 +129,7 @@ module Make(A : ARG) : S with module A = A = struct type cstor_repr = { t: T.t; n: N.t; - cstor: Fun.t; + cstor: A.Cstor.t; args: T.t IArray.t; } (* associate to each class a unique constructor term in the class (if any) *) @@ -135,16 +141,19 @@ module Make(A : ARG) : S with module A = A = struct (* TODO: also allocate a bit in CC to filter out quickly classes without cstors? *) } + (* TODO: select/is-a, with exhaustivity rule *) + (* TODO: acyclicity *) + let push_level self = N_tbl.push_level self.cstors let pop_levels self n = N_tbl.pop_levels self.cstors n (* attach data to constructor terms *) let on_new_term self _solver n (t:T.t) = - match A.view_as_cstor t with + match A.view_as_data t with | T_cstor (cstor,args) -> Log.debugf 20 (fun k->k "(@[th-cstor.on-new-term@ %a@ :cstor %a@ @[:args@ (@[%a@])@]@]@])" - T.pp t Fun.pp cstor (Util.pp_iarray T.pp) args); + T.pp t A.Cstor.pp cstor (Util.pp_iarray T.pp) args); N_tbl.add self.cstors n {n; t; cstor; args}; | _ -> () @@ -162,7 +171,7 @@ module Make(A : ARG) : S with module A = A = struct Expl.mk_merge n2 cr2.n; ] in - if Fun.equal cr1.cstor cr2.cstor then ( + if A.Cstor.equal cr1.cstor cr2.cstor then ( (* same function: injectivity *) assert (IArray.length cr1.args = IArray.length cr2.args); IArray.iter2 @@ -182,7 +191,7 @@ module Make(A : ARG) : S with module A = A = struct let self = { cstors=N_tbl.create ~size:32 (); } in - Log.debug 1 "(setup :th-cstor)"; + Log.debugf 1 (fun k->k "(setup :%s)" name); SI.on_cc_new_term solver (on_new_term self); SI.on_cc_pre_merge solver (on_pre_merge self); self diff --git a/src/th-data/types.ml b/src/th-data/types.ml index ba4085e3..bcb52385 100644 --- a/src/th-data/types.ml +++ b/src/th-data/types.ml @@ -1,3 +1,4 @@ +(* and datatype = { data_cstors: data_cstor ID.Map.t lazy_t; @@ -48,3 +49,4 @@ let cstor_proj cstor i t = let p = IArray.get (Lazy.force cstor.cstor_proj) i in app_cst p (IArray.singleton t) + *) From 444a0b9f8583ea9378a93a309b29ac58f502f39f Mon Sep 17 00:00:00 2001 From: Simon Cruanes Date: Sun, 1 Dec 2019 17:17:37 -0600 Subject: [PATCH 03/29] wip: theory of datatypes --- src/base-term/Base_types.ml | 111 +++++--------- src/base-term/Sidekick_base_term.ml | 1 - src/main/main.ml | 2 +- src/smtlib/Process.ml | 17 ++- src/smtlib/Typecheck.ml | 6 +- src/th-data/Sidekick_th_data.ml | 229 ++++++++++++++++++++-------- 6 files changed, 222 insertions(+), 144 deletions(-) diff --git a/src/base-term/Base_types.ml b/src/base-term/Base_types.ml index e9ed2637..d1803cd5 100644 --- a/src/base-term/Base_types.ml +++ b/src/base-term/Base_types.ml @@ -63,17 +63,18 @@ and ty_view = | Ty_atomic of { def: ty_def; args: ty list; - card: ty_card lazy_t; + mutable finite: bool; } and ty_def = | Ty_uninterpreted of ID.t - | Ty_data of data + | Ty_data of { + data: data; + } | Ty_def of { id: ID.t; pp: ty Fmt.printer -> ty list Fmt.printer; default_val: value list -> value; (* default value of this type *) - card: ty list -> ty_card; } and data = { @@ -97,10 +98,6 @@ and select = { select_i: int; } -and ty_card = - | Finite - | Infinite - (** Semantic values, used for models (and possibly model-constructing calculi) *) and value = | V_bool of bool @@ -185,9 +182,9 @@ let rec pp_ty out t = match t.ty_view with | Ty_atomic {def=Ty_uninterpreted id; args; _} -> Fmt.fprintf out "(@[%a@ %a@])" ID.pp id (Util.pp_list pp_ty) args | Ty_atomic {def=Ty_def def; args; _} -> def.pp pp_ty out args - | Ty_atomic {def=Ty_data d; args=[];_} -> ID.pp out d.data_id + | Ty_atomic {def=Ty_data d; args=[];_} -> ID.pp out d.data.data_id | Ty_atomic {def=Ty_data d; args;_} -> - Fmt.fprintf out "(@[%a@ %a@])" ID.pp d.data_id (Util.pp_list pp_ty) args + Fmt.fprintf out "(@[%a@ %a@])" ID.pp d.data.data_id (Util.pp_list pp_ty) args let pp_term_view_gen ~pp_id ~pp_t out = function | Bool true -> Fmt.string out "true" @@ -212,40 +209,6 @@ let pp_term_top ~ids out t = let pp_term = pp_term_top ~ids:false let pp_term_view = pp_term_view_gen ~pp_id:ID.pp_name ~pp_t:pp_term -module Ty_card : sig - type t = ty_card = Finite | Infinite - - val (+) : t -> t -> t - val ( * ) : t -> t -> t - val ( ^ ) : t -> t -> t - val finite : t - val infinite : t - - val sum : t list -> t - val product : t list -> t - - val equal : t -> t -> bool - val compare : t -> t -> int - val pp : t CCFormat.printer -end = struct - type t = ty_card = Finite | Infinite - - let (+) a b = match a, b with Finite, Finite -> Finite | _ -> Infinite - let ( * ) a b = match a, b with Finite, Finite -> Finite | _ -> Infinite - let ( ^ ) a b = match a, b with Finite, Finite -> Finite | _ -> Infinite - let finite = Finite - let infinite = Infinite - - let sum = List.fold_left (+) Finite - let product = List.fold_left ( * ) Finite - - let equal = (=) - let compare = Pervasives.compare - let pp out = function - | Finite -> CCFormat.string out "finite" - | Infinite -> CCFormat.string out "infinite" -end - module Ty : sig type t = ty type view = ty_view = @@ -253,17 +216,18 @@ module Ty : sig | Ty_atomic of { def: ty_def; args: ty list; - card: ty_card lazy_t; + mutable finite: bool; } type def = ty_def = | Ty_uninterpreted of ID.t - | Ty_data of data + | Ty_data of { + data: data; + } | Ty_def of { id: ID.t; pp: ty Fmt.printer -> ty list Fmt.printer; default_val: value list -> value; (* default value of this type *) - card: ty list -> ty_card; } val id : t -> int @@ -274,7 +238,8 @@ module Ty : sig val atomic_uninterpreted : ID.t -> t - val card : t -> ty_card + val finite : t -> bool + val set_finite : t -> bool -> unit val is_bool : t -> bool val is_uninterpreted : t -> bool @@ -305,16 +270,17 @@ end = struct | Ty_atomic of { def: ty_def; args: ty list; - card: ty_card lazy_t; + mutable finite: bool; } type def = ty_def = | Ty_uninterpreted of ID.t - | Ty_data of data + | Ty_data of { + data: data; + } | Ty_def of { id: ID.t; pp: ty Fmt.printer -> ty list Fmt.printer; default_val: value list -> value; (* default value of this type *) - card: ty list -> ty_card; } let[@inline] id t = t.ty_id @@ -327,7 +293,7 @@ end = struct let equal_def d1 d2 = match d1, d2 with | Ty_uninterpreted id1, Ty_uninterpreted id2 -> ID.equal id1 id2 | Ty_def d1, Ty_def d2 -> ID.equal d1.id d2.id - | Ty_data d1, Ty_data d2 -> ID.equal d1.data_id d2.data_id + | Ty_data d1, Ty_data d2 -> ID.equal d1.data.data_id d2.data.data_id | (Ty_uninterpreted _ | Ty_def _ | Ty_data _), _ -> false @@ -347,7 +313,7 @@ end = struct | Ty_atomic {def=Ty_def d; args; _} -> Hash.combine3 20 (ID.hash d.id) (Hash.list hash args) | Ty_atomic {def=Ty_data d; args; _} -> - Hash.combine3 30 (ID.hash d.data_id) (Hash.list hash args) + Hash.combine3 30 (ID.hash d.data.data_id) (Hash.list hash args) let set_id ty id = assert (ty.ty_id < 0); @@ -361,21 +327,18 @@ end = struct let ty = {ty_id= -1; ty_view=c; } in H.hashcons tbl ty - let card t = match view t with - | Ty_bool -> Finite - | Ty_atomic {card=lazy c; _} -> c + let finite t = match view t with + | Ty_bool -> true + | Ty_atomic {finite=f; _} -> f + + let set_finite t b = match view t with + | Ty_bool -> assert false + | Ty_atomic r -> r.finite <- b let bool = make_ Ty_bool let atomic def args : t = - let card = lazy ( - match def with - | Ty_uninterpreted _ -> - if List.for_all (fun sub -> card sub = Finite) args then Finite else Infinite - | Ty_def d -> d.card args - | Ty_data _ -> assert false (* TODO *) - ) in - make_ (Ty_atomic {def; args; card}) + make_ (Ty_atomic {def; args; finite=true;}) let atomic_uninterpreted id = atomic (Ty_uninterpreted id) [] @@ -968,6 +931,17 @@ module Data = struct let pp out d = ID.pp out d.data_id end +module Select = struct + type t = select = { + select_id: ID.t; + select_cstor: cstor; + select_ty: ty lazy_t; + select_i: int; + } + + let ty sel = Lazy.force sel.select_ty +end + module Cstor = struct type t = cstor = { cstor_id: ID.t; @@ -976,19 +950,12 @@ module Cstor = struct cstor_ty_as_data: data; cstor_ty: ty lazy_t; } + let ty_args c = + Lazy.force c.cstor_args |> Iter.of_list |> Iter.map Select.ty let equal = eq_cstor let pp out c = ID.pp out c.cstor_id end -module Select = struct - type t = select = { - select_id: ID.t; - select_cstor: cstor; - select_ty: ty lazy_t; - select_i: int; - } -end - module Proof = struct type t = Default let default = Default diff --git a/src/base-term/Sidekick_base_term.ml b/src/base-term/Sidekick_base_term.ml index cc936713..46477741 100644 --- a/src/base-term/Sidekick_base_term.ml +++ b/src/base-term/Sidekick_base_term.ml @@ -1,6 +1,5 @@ module Base_types = Base_types module ID = ID -module Ty_card = Base_types.Ty_card module Fun = Base_types.Fun module Stat = Stat module Model = Model diff --git a/src/main/main.ml b/src/main/main.ml index 5f4adf3d..12b57e49 100644 --- a/src/main/main.ml +++ b/src/main/main.ml @@ -192,7 +192,7 @@ let () = match main() with if Printexc.backtrace_status () then ( Format.fprintf Format.std_formatter "%s@." b ); - Pervasives.exit n + CCShims_.Stdlib.exit n in begin match e with | Error.Error msg -> diff --git a/src/smtlib/Process.ml b/src/smtlib/Process.ml index 98c7890b..b07da7a6 100644 --- a/src/smtlib/Process.ml +++ b/src/smtlib/Process.ml @@ -266,15 +266,26 @@ module Th_data = Sidekick_th_data.Make(struct let as_datatype ty = match Ty.view ty with | Ty_atomic {def=Ty_data data;_} -> - Some (Lazy.force data.data_cstors |> ID.Map.values) - | _ -> None + Ty_data {cstors=Lazy.force data.data.data_cstors |> ID.Map.values} + | Ty_atomic {def=_;args;finite=_} -> + Ty_app{args=Iter.of_list args} + | Ty_bool -> Ty_app {args=Iter.empty} - (* TODO*) let view_as_data t = match Term.view t with | Term.App_fun ({fun_view=Fun.Fun_cstor c;_}, args) -> T_cstor (c, args) + | Term.App_fun ({fun_view=Fun.Fun_select sel;_}, args) -> + assert (IArray.length args=1); + T_select (sel.select_cstor, sel.select_i, IArray.get args 0) + | Term.App_fun ({fun_view=Fun.Fun_is_a c;_}, args) -> + assert (IArray.length args=1); + T_is_a (c, IArray.get args 0) | _ -> T_other t let mk_cstor tst c args : Term.t = Term.app_fun tst (Fun.cstor c) args + let mk_is_a tst c u : Term.t = Term.app_fun tst (Fun.is_a c) (IArray.singleton u) + + let ty_is_finite = Ty.finite + let ty_set_is_finite = Ty.set_finite end) module Th_bool = Sidekick_th_bool_static.Make(struct diff --git a/src/smtlib/Typecheck.ml b/src/smtlib/Typecheck.ml index fa616caa..92887633 100644 --- a/src/smtlib/Typecheck.ml +++ b/src/smtlib/Typecheck.ml @@ -390,7 +390,7 @@ and conv_statement_aux ctx (stmt:PA.statement) : Stmt.t list = let rec cstor = { Cstor. cstor_id; - cstor_is_a = ID.makef "is-a.%s" cstor_name; (* every fun needs a name *) + cstor_is_a = ID.makef "(is _ %s)" cstor_name; (* every fun needs a name *) cstor_args=lazy (mk_selectors cstor); cstor_ty_as_data=data; cstor_ty=data.data_as_ty; @@ -416,12 +416,12 @@ and conv_statement_aux ctx (stmt:PA.statement) : Stmt.t list = data_id; data_cstors=lazy (cstors_of_data data cstors); data_as_ty=lazy ( - let def = Ty.Ty_data data in + let def = Ty.Ty_data { data; } in Ty.atomic def [] ); } in Ctx.add_id_ ctx data_name data_id - (Ctx.K_ty (Ctx.K_atomic (Ty.Ty_data data))); + (Ctx.K_ty (Ctx.K_atomic (Ty.Ty_data {data}))); data) l in diff --git a/src/th-data/Sidekick_th_data.ml b/src/th-data/Sidekick_th_data.ml index 8e539fb8..1a5ce551 100644 --- a/src/th-data/Sidekick_th_data.ml +++ b/src/th-data/Sidekick_th_data.ml @@ -20,35 +20,12 @@ type ('c, 'ty) data_ty_view = args: 'ty Iter.t; } | Ty_data of { - cstors: 'c list; - } + cstors: 'c; + } | Ty_other let name = "th-data" -(** {2 Cardinality of types} *) - -module Ty_card = struct - type t = - | Finite - | Infinite - - let (+) a b = match a, b with Finite, Finite -> Finite | _ -> Infinite - let ( * ) a b = match a, b with Finite, Finite -> Finite | _ -> Infinite - let ( ^ ) a b = match a, b with Finite, Finite -> Finite | _ -> Infinite - let finite = Finite - let infinite = Infinite - - let sum = Iter.fold (+) Finite - let product = Iter.fold ( * ) Finite - - let equal : t -> t -> bool = (=) - let compare : t -> t -> int = Pervasives.compare - let pp out = function - | Finite -> Fmt.string out "finite" - | Infinite -> Fmt.string out "infinite" -end - (** An abtract representation of a datatype *) module type DATA_TY = sig type t @@ -56,6 +33,10 @@ module type DATA_TY = sig val equal : t -> t -> bool + val finite : t -> bool + + val set_finite : t -> bool -> unit + val view : t -> (cstor, t) data_ty_view val cstor_args : cstor -> t Iter.t @@ -64,40 +45,18 @@ module type DATA_TY = sig module Tbl : Hashtbl.S with type key = t end -(** Helper to compute the cardinality of types *) -module Compute_card(Ty : DATA_TY) : sig - type t - val create : unit -> t - val card : t -> Ty.t -> Ty_card.t -end = struct - module Card = Ty_card - type t = { - cards: Card.t Ty.Tbl.t; - } +(** {2 Cardinality of types} *) - let create() : t = { cards=Ty.Tbl.create 16} +module C = struct + type t = + | Finite + | Infinite - let card (self:t) (ty:Ty.t) : Card.t = - let rec aux (ty:Ty.t) : Card.t = - match Ty.Tbl.find self.cards ty with - | c -> c - | exception Not_found -> - Ty.Tbl.add self.cards ty Card.infinite; (* temp value, for fixpoint computation *) - let c = match Ty.view ty with - | Ty_other -> Card.finite - | Ty_app {args} -> Iter.map aux args |> Card.product - | Ty_arrow (args,ret) -> - Card.( (aux ret) ^ (Card.product @@ Iter.map aux args)) - | Ty_data { cstors; } -> - cstors - |> Iter.of_list - |> Iter.map (fun c -> Card.product (Iter.map aux @@ Ty.cstor_args c)) - |> Card.sum - in - Ty.Tbl.replace self.cards ty c; - c - in - aux ty + let (+) a b = match a, b with Finite, Finite -> Finite | _ -> Infinite + let ( * ) a b = match a, b with Finite, Finite -> Finite | _ -> Infinite + let ( ^ ) a b = match a, b with Finite, Finite -> Finite | _ -> Infinite + let sum = Iter.fold (+) Finite + let product = Iter.fold ( * ) Finite end module type ARG = sig @@ -105,12 +64,62 @@ module type ARG = sig module Cstor : sig type t + val ty_args : t -> S.T.Ty.t Iter.t val pp : t Fmt.printer val equal : t -> t -> bool end + + val as_datatype : S.T.Ty.t -> (Cstor.t Iter.t, S.T.Ty.t) data_ty_view val view_as_data : S.T.Term.t -> (Cstor.t, S.T.Term.t) data_view val mk_cstor : S.T.Term.state -> Cstor.t -> S.T.Term.t IArray.t -> S.T.Term.t - val as_datatype : S.T.Ty.t -> Cstor.t Iter.t option + val mk_is_a: S.T.Term.state -> Cstor.t -> S.T.Term.t -> S.T.Term.t + val ty_is_finite : S.T.Ty.t -> bool + val ty_set_is_finite : S.T.Ty.t -> bool -> unit +end + +(** Helper to compute the cardinality of types *) +module Compute_card(A : ARG) : sig + type t + val create : unit -> t + val is_finite : t -> A.S.T.Ty.t -> bool +end = struct + module Ty = A.S.T.Ty + module Ty_tbl = CCHashtbl.Make(Ty) + type t = { + cards: C.t Ty_tbl.t; + } + + let create() : t = { cards=Ty_tbl.create 16} + + let card (self:t) (ty:Ty.t) : C.t = + let rec aux (ty:Ty.t) : C.t = + match Ty_tbl.find self.cards ty with + | c -> c + | exception Not_found -> + Ty_tbl.add self.cards ty C.Infinite; (* temp value, for fixpoint computation *) + let c = match A.as_datatype ty with + | Ty_other -> if A.ty_is_finite ty then C.Finite else C.Infinite + | Ty_app {args} -> Iter.map aux args |> C.product + | Ty_arrow (args,ret) -> + C.( (aux ret) ^ (C.product @@ Iter.map aux args)) + | Ty_data { cstors; } -> + let c = + cstors + |> Iter.map (fun c -> C.product (Iter.map aux @@ A.Cstor.ty_args c)) + |> C.sum + in + A.ty_set_is_finite ty (c=Finite); + c + in + Ty_tbl.replace self.cards ty c; + c + in + aux ty + + let is_finite self ty : bool = + match card self ty with + | C.Finite -> true + | C.Infinite -> false end module type S = sig @@ -123,9 +132,12 @@ module Make(A : ARG) : S with module A = A = struct module SI = A.S.Solver_internal module T = A.S.T.Term module N = SI.CC.N + module Ty = A.S.T.Ty module Fun = A.S.T.Fun module Expl = SI.CC.Expl + module Card = Compute_card(A) + type cstor_repr = { t: T.t; n: N.t; @@ -137,26 +149,71 @@ module Make(A : ARG) : S with module A = A = struct module N_tbl = Backtrackable_tbl.Make(N) type t = { + tst: T.state; cstors: cstor_repr N_tbl.t; (* repr -> cstor for the class *) + cards: Card.t; (* remember finiteness *) + to_decide: bool ref N_tbl.t; (* set of terms to decide. true means already clausified *) (* TODO: also allocate a bit in CC to filter out quickly classes without cstors? *) + (* TODO: bitfield for types with less than 62 cstors, to quickly detect conflict? *) } + let push_level self = + N_tbl.push_level self.cstors; + N_tbl.push_level self.to_decide; + () + + let pop_levels self n = + N_tbl.pop_levels self.cstors n; + N_tbl.pop_levels self.to_decide n; + () + (* TODO: select/is-a, with exhaustivity rule *) (* TODO: acyclicity *) - let push_level self = N_tbl.push_level self.cstors - let pop_levels self n = N_tbl.pop_levels self.cstors n - (* attach data to constructor terms *) - let on_new_term self _solver n (t:T.t) = + let on_new_term_look_at_shape self n (t:T.t) = match A.view_as_data t with | T_cstor (cstor,args) -> Log.debugf 20 - (fun k->k "(@[th-cstor.on-new-term@ %a@ :cstor %a@ @[:args@ (@[%a@])@]@]@])" - T.pp t A.Cstor.pp cstor (Util.pp_iarray T.pp) args); + (fun k->k "(@[%s.on-new-term@ %a@ :cstor %a@ @[:args@ (@[%a@])@]@]@])" + name T.pp t A.Cstor.pp cstor (Util.pp_iarray T.pp) args); N_tbl.add self.cstors n {n; t; cstor; args}; + | T_select (cstor,i,u) -> + Log.debugf 20 + (fun k->k "(@[%s.on-new-term.select[%d]@ %a@ :cstor %a@ :in %a@])" + name i T.pp t A.Cstor.pp cstor T.pp u); + (* TODO: remember that [u] must be decided *) + () + (* N_tbl.add self.cstors n {n; t; cstor; args}; *) + | T_is_a (cstor,u) -> + Log.debugf 20 + (fun k->k "(@[%s.on-new-term.is-a@ %a@ :cstor %a@ :in %a@])" + name T.pp t A.Cstor.pp cstor T.pp u); + () + (* N_tbl.add self.cstors n {n; t; cstor; args}; *) + | T_other _ -> () + + (* remember terms of a datatype *) + let on_new_term_look_at_ty (self:t) n (t:T.t) : unit = + let ty = T.ty t in + match A.as_datatype ty with + | Ty_data _ -> + Log.debugf 20 + (fun k->k "(@[%s.on-new-term.has-data-ty@ %a@ :ty %a@])" + name T.pp t Ty.pp ty); + if Card.is_finite self.cards ty && not (N_tbl.mem self.to_decide n) then ( + (* must decide this term *) + Log.debugf 20 + (fun k->k "(@[%s.on-new-term.must-decide-finitey@ %a@])" name T.pp t); + N_tbl.add self.to_decide n (ref false); + ) | _ -> () + let on_new_term self _solver n t = + on_new_term_look_at_shape self n t; + on_new_term_look_at_ty self n t; + () + let on_pre_merge (self:t) cc acts n1 n2 e_n1_n2 : unit = begin match N_tbl.get self.cstors n1, N_tbl.get self.cstors n2 with | Some cr1, Some cr2 -> @@ -187,13 +244,57 @@ module Make(A : ARG) : S with module A = A = struct | None, None -> () end + let cstors_of_ty (ty:Ty.t) : A.Cstor.t Iter.t = + match A.as_datatype ty with + | Ty_data {cstors} -> cstors + | _ -> assert false + + let on_final_check (self:t) (solver:SI.t) (acts:SI.actions) _trail = + let remaining_to_decide = + N_tbl.to_iter self.to_decide + |> Iter.map (fun (n,r) -> SI.cc_find solver n, r) + |> Iter.filter (fun (n,r) -> not !r && not (N_tbl.mem self.cstors n)) + |> Iter.to_rev_list + in + begin match remaining_to_decide with + | [] -> () + | l -> + Log.debugf 10 + (fun k->k "(@[%s.must-decide@ %a@])" name + (Util.pp_list (Fmt.map fst N.pp)) l); + (* add clauses [∨_c is-c(t)] and [¬(is-a t) ∨ ¬(is-b t)] *) + List.iter + (fun (n,r) -> + assert (not !r); + let t = N.term n in + let c = + cstors_of_ty (T.ty t) + |> Iter.map (fun c -> A.mk_is_a self.tst c t) + |> Iter.map (SI.mk_lit solver acts) + |> Iter.to_rev_list + in + r := true; + SI.add_clause_permanent solver acts c; + Iter.diagonal_l c + (fun (c1,c2) -> + SI.add_clause_permanent solver acts + [SI.Lit.neg c1; SI.Lit.neg c2]); + ()) + l + end; + () + let create_and_setup (solver:SI.t) : t = let self = { + tst=SI.tst solver; cstors=N_tbl.create ~size:32 (); + to_decide=N_tbl.create ~size:16 (); + cards=Card.create(); } in Log.debugf 1 (fun k->k "(setup :%s)" name); SI.on_cc_new_term solver (on_new_term self); SI.on_cc_pre_merge solver (on_pre_merge self); + SI.on_final_check solver (on_final_check self); self let theory = From c55e7a613b26c7cb136912c01af04c8fc1b16f11 Mon Sep 17 00:00:00 2001 From: Simon Cruanes Date: Sun, 1 Dec 2019 17:38:24 -0600 Subject: [PATCH 04/29] test: add some basic datatype tests --- tests/unsat/data_acycl1.smt2 | 8 ++++++++ tests/unsat/data_acycl_if.smt2 | 14 ++++++++++++++ tests/unsat/data_card1.smt2 | 11 +++++++++++ 3 files changed, 33 insertions(+) create mode 100644 tests/unsat/data_acycl1.smt2 create mode 100644 tests/unsat/data_acycl_if.smt2 create mode 100644 tests/unsat/data_card1.smt2 diff --git a/tests/unsat/data_acycl1.smt2 b/tests/unsat/data_acycl1.smt2 new file mode 100644 index 00000000..f5505cc7 --- /dev/null +++ b/tests/unsat/data_acycl1.smt2 @@ -0,0 +1,8 @@ + +(set-info :status unsat) +(declare-datatypes ((nat 0)) (((Z) (S (pred nat))))) +(declare-const n nat) + +(assert (= n (S (S n)))) + +(check-sat) diff --git a/tests/unsat/data_acycl_if.smt2 b/tests/unsat/data_acycl_if.smt2 new file mode 100644 index 00000000..2d25a0d5 --- /dev/null +++ b/tests/unsat/data_acycl_if.smt2 @@ -0,0 +1,14 @@ + +(set-info :status unsat) +(declare-datatypes ((nat 0)) (((Z) (S (pred nat))))) +(declare-const p Bool) +(declare-const n nat) +(declare-const n_t nat) +(declare-const n_f nat) + +(assert (= n_t (S n))) +(assert (= n_f (S (S n)))) +(assert (=> p (= n (S n_t)))) +(assert (=> (not p) (= n (S n_f)))) + +(check-sat) diff --git a/tests/unsat/data_card1.smt2 b/tests/unsat/data_card1.smt2 new file mode 100644 index 00000000..758891ef --- /dev/null +++ b/tests/unsat/data_card1.smt2 @@ -0,0 +1,11 @@ + +(set-info :status unsat) +(declare-datatypes ((three 0)) (((A) (B) (C)))) +(declare-const t1 three) +(declare-const t2 three) +(declare-const t3 three) +(declare-const t4 three) + +(assert (distinct t1 t2 t3 t4)) + +(check-sat) From 7c951c08ff1808f3c2c9b3c8a891c172cf12a4e3 Mon Sep 17 00:00:00 2001 From: Simon Cruanes Date: Sun, 1 Dec 2019 18:14:20 -0600 Subject: [PATCH 05/29] wip: use `t=c` instead of `(is _ c) t` for nullary constructors --- src/base-term/Base_types.ml | 2 ++ src/smtlib/Process.ml | 7 +++- src/smtlib/Typecheck.ml | 3 +- src/th-data/Sidekick_th_data.ml | 57 ++++++++++++++++++++------------- src/th-data/dune | 2 +- 5 files changed, 45 insertions(+), 26 deletions(-) diff --git a/src/base-term/Base_types.ml b/src/base-term/Base_types.ml index d1803cd5..c139a3db 100644 --- a/src/base-term/Base_types.ml +++ b/src/base-term/Base_types.ml @@ -86,6 +86,7 @@ and data = { and cstor = { cstor_id: ID.t; cstor_is_a: ID.t; + mutable cstor_arity: int; cstor_args: select list lazy_t; cstor_ty_as_data: data; cstor_ty: ty lazy_t; @@ -946,6 +947,7 @@ module Cstor = struct type t = cstor = { cstor_id: ID.t; cstor_is_a: ID.t; + mutable cstor_arity: int; cstor_args: select list lazy_t; cstor_ty_as_data: data; cstor_ty: ty lazy_t; diff --git a/src/smtlib/Process.ml b/src/smtlib/Process.ml index b07da7a6..00899d0b 100644 --- a/src/smtlib/Process.ml +++ b/src/smtlib/Process.ml @@ -282,7 +282,12 @@ module Th_data = Sidekick_th_data.Make(struct | _ -> T_other t let mk_cstor tst c args : Term.t = Term.app_fun tst (Fun.cstor c) args - let mk_is_a tst c u : Term.t = Term.app_fun tst (Fun.is_a c) (IArray.singleton u) + let mk_is_a tst c u : Term.t = + if c.cstor_arity=0 then ( + Term.eq tst u (Term.const tst (Fun.cstor c)) + ) else ( + Term.app_fun tst (Fun.is_a c) (IArray.singleton u) + ) let ty_is_finite = Ty.finite let ty_set_is_finite = Ty.set_finite diff --git a/src/smtlib/Typecheck.ml b/src/smtlib/Typecheck.ml index 92887633..e5a565fc 100644 --- a/src/smtlib/Typecheck.ml +++ b/src/smtlib/Typecheck.ml @@ -392,6 +392,7 @@ and conv_statement_aux ctx (stmt:PA.statement) : Stmt.t list = cstor_id; cstor_is_a = ID.makef "(is _ %s)" cstor_name; (* every fun needs a name *) cstor_args=lazy (mk_selectors cstor); + cstor_arity=0; cstor_ty_as_data=data; cstor_ty=data.data_as_ty; } in @@ -428,7 +429,7 @@ and conv_statement_aux ctx (stmt:PA.statement) : Stmt.t list = (* now force definitions *) List.iter (fun {Data.data_cstors=lazy m;data_as_ty=lazy _;_} -> - ID.Map.iter (fun _ {Cstor.cstor_args=lazy _;_} -> ()) m; + ID.Map.iter (fun _ ({Cstor.cstor_args=lazy l;_} as r) -> r.cstor_arity <- List.length l) m; ()) l; [Stmt.Stmt_data l] diff --git a/src/th-data/Sidekick_th_data.ml b/src/th-data/Sidekick_th_data.ml index 1a5ce551..2e080b32 100644 --- a/src/th-data/Sidekick_th_data.ml +++ b/src/th-data/Sidekick_th_data.ml @@ -152,7 +152,8 @@ module Make(A : ARG) : S with module A = A = struct tst: T.state; cstors: cstor_repr N_tbl.t; (* repr -> cstor for the class *) cards: Card.t; (* remember finiteness *) - to_decide: bool ref N_tbl.t; (* set of terms to decide. true means already clausified *) + to_decide: unit N_tbl.t; (* set of terms to decide. *) + case_split_done: unit T.Tbl.t; (* set of terms for which case split is done *) (* TODO: also allocate a bit in CC to filter out quickly classes without cstors? *) (* TODO: bitfield for types with less than 62 cstors, to quickly detect conflict? *) } @@ -167,7 +168,7 @@ module Make(A : ARG) : S with module A = A = struct N_tbl.pop_levels self.to_decide n; () - (* TODO: select/is-a, with exhaustivity rule *) + (* TODO: select/is-a *) (* TODO: acyclicity *) (* attach data to constructor terms *) @@ -204,8 +205,8 @@ module Make(A : ARG) : S with module A = A = struct if Card.is_finite self.cards ty && not (N_tbl.mem self.to_decide n) then ( (* must decide this term *) Log.debugf 20 - (fun k->k "(@[%s.on-new-term.must-decide-finitey@ %a@])" name T.pp t); - N_tbl.add self.to_decide n (ref false); + (fun k->k "(@[%s.on-new-term.must-decide-finite-ty@ %a@])" name T.pp t); + N_tbl.add self.to_decide n (); ) | _ -> () @@ -249,37 +250,46 @@ module Make(A : ARG) : S with module A = A = struct | Ty_data {cstors} -> cstors | _ -> assert false + (* on final check, make sure we have done case split on all terms that + need it. *) let on_final_check (self:t) (solver:SI.t) (acts:SI.actions) _trail = let remaining_to_decide = N_tbl.to_iter self.to_decide - |> Iter.map (fun (n,r) -> SI.cc_find solver n, r) - |> Iter.filter (fun (n,r) -> not !r && not (N_tbl.mem self.cstors n)) + |> Iter.map (fun (n,_) -> SI.cc_find solver n) + |> Iter.filter + (fun n -> + not (N_tbl.mem self.cstors n) && + not (T.Tbl.mem self.case_split_done (N.term n))) |> Iter.to_rev_list in begin match remaining_to_decide with | [] -> () | l -> Log.debugf 10 - (fun k->k "(@[%s.must-decide@ %a@])" name - (Util.pp_list (Fmt.map fst N.pp)) l); + (fun k->k "(@[%s.final-check.must-decide@ %a@])" name (Util.pp_list N.pp) l); (* add clauses [∨_c is-c(t)] and [¬(is-a t) ∨ ¬(is-b t)] *) List.iter - (fun (n,r) -> - assert (not !r); + (fun n -> let t = N.term n in - let c = - cstors_of_ty (T.ty t) - |> Iter.map (fun c -> A.mk_is_a self.tst c t) - |> Iter.map (SI.mk_lit solver acts) - |> Iter.to_rev_list - in - r := true; - SI.add_clause_permanent solver acts c; - Iter.diagonal_l c - (fun (c1,c2) -> - SI.add_clause_permanent solver acts - [SI.Lit.neg c1; SI.Lit.neg c2]); - ()) + (* [t] might have been expanded already, in case of duplicates in [l] *) + if not @@ T.Tbl.mem self.case_split_done t then ( + T.Tbl.add self.case_split_done t (); + let c = + cstors_of_ty (T.ty t) + |> Iter.map (fun c -> A.mk_is_a self.tst c t) + |> Iter.map + (fun t -> + let lit = SI.mk_lit solver acts t in + (* TODO: set default polarity, depending on n° of args? *) + lit) + |> Iter.to_rev_list + in + SI.add_clause_permanent solver acts c; + Iter.diagonal_l c + (fun (c1,c2) -> + SI.add_clause_permanent solver acts + [SI.Lit.neg c1; SI.Lit.neg c2]); + )) l end; () @@ -289,6 +299,7 @@ module Make(A : ARG) : S with module A = A = struct tst=SI.tst solver; cstors=N_tbl.create ~size:32 (); to_decide=N_tbl.create ~size:16 (); + case_split_done=T.Tbl.create 16; cards=Card.create(); } in Log.debugf 1 (fun k->k "(setup :%s)" name); diff --git a/src/th-data/dune b/src/th-data/dune index 35e07fee..9dd86c15 100644 --- a/src/th-data/dune +++ b/src/th-data/dune @@ -4,5 +4,5 @@ (name Sidekick_th_data) (public_name sidekick.th-data) (libraries containers sidekick.core sidekick.util) - (flags :standard -open Sidekick_util)) + (flags :standard -open Sidekick_util -w -32)) ; TODO get warning back From a4e3fd5a69d7cf7a6840e9254d826ee847665ddd Mon Sep 17 00:00:00 2001 From: Simon Cruanes Date: Sun, 1 Dec 2019 19:26:12 -0600 Subject: [PATCH 06/29] feat: provide simple `repr->monoid` mapping in core --- src/cc/Sidekick_cc.ml | 7 ++ src/core/Sidekick_core.ml | 100 +++++++++++++++++++++++++++- src/th-cstor/Sidekick_th_cstor.ml | 104 ++++++++++++++---------------- src/th-data/Sidekick_th_data.ml | 96 ++++++++++++++------------- src/th-data/Sidekick_th_data.mli | 57 ++++++++++++++++ 5 files changed, 262 insertions(+), 102 deletions(-) create mode 100644 src/th-data/Sidekick_th_data.mli diff --git a/src/cc/Sidekick_cc.ml b/src/cc/Sidekick_cc.ml index f6ad319a..5b234a02 100644 --- a/src/cc/Sidekick_cc.ml +++ b/src/cc/Sidekick_cc.ml @@ -289,6 +289,13 @@ module Make (A: CC_ARG) let[@inline] on_backtrack cc f : unit = Backtrack_stack.push_if_nonzero_level cc.undo f + let set_bitfield cc field b n = + let old = N.get_field field n in + if old <> b then ( + on_backtrack cc (fun () -> N.set_field field old n); + N.set_field field b n; + ) + (* check if [t] is in the congruence closure. Invariant: [in_cc t ∧ do_cc t => forall u subterm t, in_cc u] *) let[@inline] mem (cc:t) (t:term): bool = T_tbl.mem cc.tbl t diff --git a/src/core/Sidekick_core.ml b/src/core/Sidekick_core.ml index 6be110ba..1af55db0 100644 --- a/src/core/Sidekick_core.ml +++ b/src/core/Sidekick_core.ml @@ -182,7 +182,6 @@ module type CC_S = sig and are merged automatically when classes are merged. *) val get_field : bitfield -> t -> bool - val set_field : bitfield -> bool -> t -> unit end module Expl : sig @@ -236,6 +235,10 @@ module type CC_S = sig (** Allocate a new bitfield for the nodes. See {!N.bitfield}. *) + val set_bitfield : t -> N.bitfield -> bool -> N.t -> unit + (** Set the bitfield for the node. This will be backtracked. + See {!N.bitfield}. *) + (* TODO: remove? this is managed by the solver anyway? *) val on_pre_merge : t -> ev_on_pre_merge -> unit (** Add a function to be called when two classes are merged *) @@ -658,3 +661,98 @@ module type SOLVER = sig val pp_stats : t CCFormat.printer end + +(** Helper for keeping track of state for each class *) + +module type MONOID_ARG = sig + module SI : SOLVER_INTERNAL + type t + val pp : t Fmt.printer + val name : string (* name of the monoid's value (short) *) + val of_term : SI.CC.N.t -> SI.T.Term.t -> t option + val merge : SI.CC.t -> SI.CC.N.t -> t -> SI.CC.N.t -> t -> (t, SI.CC.Expl.t) result +end + +module Monoid_of_repr(M : MONOID_ARG) : sig + type t + val create_and_setup : ?size:int -> M.SI.t -> t + val push_level : t -> unit + val pop_levels : t -> int -> unit + val mem : t -> M.SI.CC.N.t -> bool + val get : t -> M.SI.CC.N.t -> M.t option +end = struct + module SI = M.SI + module T = SI.T.Term + module N = SI.CC.N + module CC = SI.CC + module N_tbl = Backtrackable_tbl.Make(N) + module Expl = SI.CC.Expl + + type t = { + values: M.t N_tbl.t; (* repr -> value for the class *) + field_has_value: N.bitfield; (* bit in CC to filter out quickly classes without value *) + } + + let push_level self = N_tbl.push_level self.values + let pop_levels self n = N_tbl.pop_levels self.values n + + let mem self n = + let res = N.get_field self.field_has_value n in + assert (if res then N_tbl.mem self.values n else true); + res + + let get self n = N_tbl.get self.values n + + let on_new_term self cc n (t:T.t) = + match M.of_term n t with + | Some v -> + Log.debugf 20 + (fun k->k "(@[monoid[%s].on-new-term@ :n %a@ :value %a@])" + M.name N.pp n M.pp v); + SI.CC.set_bitfield cc self.field_has_value true n; + N_tbl.add self.values n v + | None -> () + + (* find cell for [n] *) + let get_cell (self:t) (n:N.t) : M.t option = + N_tbl.get self.values n + (* TODO + if N.get_field self.field_has_value n then ( + try Some (N_tbl.find self.values n) + with Not_found -> + Error.errorf "repr %a has value-field bit for %s set, but is not in table" + N.pp n M.name + ) else ( + None + ) + *) + + let on_pre_merge (self:t) cc acts n1 n2 e_n1_n2 : unit = + begin match get_cell self n1, get_cell self n2 with + | Some v1, Some v2 -> + Log.debugf 5 + (fun k->k + "(@[monoid[%s].on_pre_merge@ @[:n1 %a@ :val %a@]@ @[:n2 %a@ :val %a@]@])" + M.name N.pp n1 M.pp v1 N.pp n2 M.pp v2); + begin match M.merge cc n1 v1 n2 v2 with + | Ok v' -> + N_tbl.add self.values n1 v'; + | Error expl -> + (* add [n1=n2] to the conflict *) + let expl = Expl.mk_list [ e_n1_n2; expl; ] in + SI.CC.raise_conflict_from_expl cc acts expl + end + | None, Some cr -> + SI.CC.set_bitfield cc self.field_has_value true n1; + N_tbl.add self.values n1 cr + | Some _, None -> () (* already there on the left *) + | None, None -> () + end + + let create_and_setup ?size (solver:SI.t) : t = + let field_has_value = SI.CC.allocate_bitfield (SI.cc solver) in + let self = { values=N_tbl.create ?size (); field_has_value; } in + SI.on_cc_new_term solver (on_new_term self); + SI.on_cc_pre_merge solver (on_pre_merge self); + self +end diff --git a/src/th-cstor/Sidekick_th_cstor.ml b/src/th-cstor/Sidekick_th_cstor.ml index 1d5b666b..688e5cbd 100644 --- a/src/th-cstor/Sidekick_th_cstor.ml +++ b/src/th-cstor/Sidekick_th_cstor.ml @@ -24,71 +24,61 @@ module Make(A : ARG) : S with module A = A = struct module Fun = A.S.T.Fun module Expl = SI.CC.Expl - type cstor_repr = { - t: T.t; - n: N.t; - cstor: Fun.t; - args: T.t IArray.t; - } - (* associate to each class a unique constructor term in the class (if any) *) + module Monoid = struct + module SI = SI - module N_tbl = Backtrackable_tbl.Make(N) + (* associate to each class a unique constructor term in the class (if any) *) + type t = { + t: T.t; + n: N.t; + cstor: Fun.t; + args: T.t IArray.t; + } - type t = { - cstors: cstor_repr N_tbl.t; (* repr -> cstor for the class *) - (* TODO: also allocate a bit in CC to filter out quickly classes without cstors? *) - } + let name = name + let pp out (v:t) = + Fmt.fprintf out "(@[cstor %a@ :term %a@])" Fun.pp v.cstor T.pp v.t - let push_level self = N_tbl.push_level self.cstors - let pop_levels self n = N_tbl.pop_levels self.cstors n + (* attach data to constructor terms *) + let of_term n (t:T.t) : _ option = + match A.view_as_cstor t with + | T_cstor (cstor,args) -> Some {n; t; cstor; args} + | _ -> None - (* attach data to constructor terms *) - let on_new_term self _solver n (t:T.t) = - match A.view_as_cstor t with - | T_cstor (cstor,args) -> - Log.debugf 20 - (fun k->k "(@[th-cstor.on-new-term@ %a@ :cstor %a@ @[:args@ (@[%a@])@]@]@])" - T.pp t Fun.pp cstor (Util.pp_iarray T.pp) args); - N_tbl.add self.cstors n {n; t; cstor; args}; - | _ -> () - - let on_pre_merge (self:t) cc acts n1 n2 e_n1_n2 : unit = - begin match N_tbl.get self.cstors n1, N_tbl.get self.cstors n2 with - | Some cr1, Some cr2 -> - Log.debugf 5 - (fun k->k "(@[th-cstor.on_pre_merge@ @[:c1 %a@ (term %a)@]@ @[:c2 %a@ (term %a)@]@])" - N.pp n1 T.pp cr1.t N.pp n2 T.pp cr2.t); - (* build full explanation of why the constructor terms are equal *) - let expl = - Expl.mk_list [ - e_n1_n2; - Expl.mk_merge n1 cr1.n; - Expl.mk_merge n2 cr2.n; - ] - in - if Fun.equal cr1.cstor cr2.cstor then ( - (* same function: injectivity *) - assert (IArray.length cr1.args = IArray.length cr2.args); - IArray.iter2 - (fun u1 u2 -> SI.CC.merge_t cc u1 u2 expl) - cr1.args cr2.args - ) else ( - (* different function: disjointness *) - SI.CC.raise_conflict_from_expl cc acts expl + let merge cc n1 v1 n2 v2 : _ result = + Log.debugf 5 + (fun k->k "(@[%s.merge@ @[:c1 %a (t %a)@]@ @[:c2 %a (t %a)@]@])" + name N.pp n1 T.pp v1.t N.pp n2 T.pp v2.t); + (* build full explanation of why the constructor terms are equal *) + let expl = + Expl.mk_list [ + Expl.mk_merge n1 v1.n; + Expl.mk_merge n2 v2.n; + ] + in + if Fun.equal v1.cstor v2.cstor then ( + (* same function: injectivity *) + assert (IArray.length v1.args = IArray.length v2.args); + IArray.iter2 + (fun u1 u2 -> SI.CC.merge_t cc u1 u2 expl) + v1.args v2.args; + Ok v1 + ) else ( + (* different function: disjointness *) + Error expl ) - | None, Some cr -> - N_tbl.add self.cstors n1 cr - | Some _, None -> () (* already there on the left *) - | None, None -> () - end + end + + module ST = Sidekick_core.Monoid_of_repr(Monoid) + + type t = ST.t + + let push_level = ST.push_level + let pop_levels = ST.pop_levels let create_and_setup (solver:SI.t) : t = - let self = { - cstors=N_tbl.create ~size:32 (); - } in Log.debug 1 "(setup :th-cstor)"; - SI.on_cc_new_term solver (on_new_term self); - SI.on_cc_pre_merge solver (on_pre_merge self); + let self = ST.create_and_setup ~size:32 solver in self let theory = diff --git a/src/th-data/Sidekick_th_data.ml b/src/th-data/Sidekick_th_data.ml index 2e080b32..c3c2ce06 100644 --- a/src/th-data/Sidekick_th_data.ml +++ b/src/th-data/Sidekick_th_data.ml @@ -138,19 +138,57 @@ module Make(A : ARG) : S with module A = A = struct module Card = Compute_card(A) - type cstor_repr = { - t: T.t; - n: N.t; - cstor: A.Cstor.t; - args: T.t IArray.t; - } - (* associate to each class a unique constructor term in the class (if any) *) + module Monoid_cstor = struct + module SI = SI + (* associate to each class a unique constructor term in the class (if any) *) + type t = { + t: T.t; + n: N.t; + cstor: A.Cstor.t; + args: T.t IArray.t; + } + + let name = "th-data.cstor" + let pp out (v:t) = + Fmt.fprintf out "(@[cstor %a@ :term %a@])" A.Cstor.pp v.cstor T.pp v.t + + (* attach data to constructor terms *) + let of_term n (t:T.t) : _ option = + match A.view_as_data t with + | T_cstor (cstor,args) -> Some {n; t; cstor; args} + | _ -> None + + let merge cc n1 v1 n2 v2 : _ result = + Log.debugf 5 + (fun k->k "(@[%s.merge@ @[:c1 %a (t %a)@]@ @[:c2 %a (t %a)@]@])" + name N.pp n1 T.pp v1.t N.pp n2 T.pp v2.t); + (* build full explanation of why the constructor terms are equal *) + let expl = + Expl.mk_list [ + Expl.mk_merge n1 v1.n; + Expl.mk_merge n2 v2.n; + ] + in + if A.Cstor.equal v1.cstor v2.cstor then ( + (* same function: injectivity *) + assert (IArray.length v1.args = IArray.length v2.args); + IArray.iter2 + (fun u1 u2 -> SI.CC.merge_t cc u1 u2 expl) + v1.args v2.args; + Ok v1 + ) else ( + (* different function: disjointness *) + Error expl + ) + end + + module ST_cstors = Sidekick_core.Monoid_of_repr(Monoid_cstor) module N_tbl = Backtrackable_tbl.Make(N) type t = { tst: T.state; - cstors: cstor_repr N_tbl.t; (* repr -> cstor for the class *) + cstors: ST_cstors.t; (* repr -> cstor for the class *) cards: Card.t; (* remember finiteness *) to_decide: unit N_tbl.t; (* set of terms to decide. *) case_split_done: unit T.Tbl.t; (* set of terms for which case split is done *) @@ -159,18 +197,19 @@ module Make(A : ARG) : S with module A = A = struct } let push_level self = - N_tbl.push_level self.cstors; + ST_cstors.push_level self.cstors; N_tbl.push_level self.to_decide; () let pop_levels self n = - N_tbl.pop_levels self.cstors n; + ST_cstors.pop_levels self.cstors n; N_tbl.pop_levels self.to_decide n; () (* TODO: select/is-a *) (* TODO: acyclicity *) + (* TODO: remove (* attach data to constructor terms *) let on_new_term_look_at_shape self n (t:T.t) = match A.view_as_data t with @@ -193,6 +232,7 @@ module Make(A : ARG) : S with module A = A = struct () (* N_tbl.add self.cstors n {n; t; cstor; args}; *) | T_other _ -> () + *) (* remember terms of a datatype *) let on_new_term_look_at_ty (self:t) n (t:T.t) : unit = @@ -211,40 +251,9 @@ module Make(A : ARG) : S with module A = A = struct | _ -> () let on_new_term self _solver n t = - on_new_term_look_at_shape self n t; on_new_term_look_at_ty self n t; () - let on_pre_merge (self:t) cc acts n1 n2 e_n1_n2 : unit = - begin match N_tbl.get self.cstors n1, N_tbl.get self.cstors n2 with - | Some cr1, Some cr2 -> - Log.debugf 5 - (fun k->k "(@[th-cstor.on_pre_merge@ @[:c1 %a@ (term %a)@]@ @[:c2 %a@ (term %a)@]@])" - N.pp n1 T.pp cr1.t N.pp n2 T.pp cr2.t); - (* build full explanation of why the constructor terms are equal *) - let expl = - Expl.mk_list [ - e_n1_n2; - Expl.mk_merge n1 cr1.n; - Expl.mk_merge n2 cr2.n; - ] - in - if A.Cstor.equal cr1.cstor cr2.cstor then ( - (* same function: injectivity *) - assert (IArray.length cr1.args = IArray.length cr2.args); - IArray.iter2 - (fun u1 u2 -> SI.CC.merge_t cc u1 u2 expl) - cr1.args cr2.args - ) else ( - (* different function: disjointness *) - SI.CC.raise_conflict_from_expl cc acts expl - ) - | None, Some cr -> - N_tbl.add self.cstors n1 cr - | Some _, None -> () (* already there on the left *) - | None, None -> () - end - let cstors_of_ty (ty:Ty.t) : A.Cstor.t Iter.t = match A.as_datatype ty with | Ty_data {cstors} -> cstors @@ -258,7 +267,7 @@ module Make(A : ARG) : S with module A = A = struct |> Iter.map (fun (n,_) -> SI.cc_find solver n) |> Iter.filter (fun n -> - not (N_tbl.mem self.cstors n) && + not (ST_cstors.mem self.cstors n) && not (T.Tbl.mem self.case_split_done (N.term n))) |> Iter.to_rev_list in @@ -297,14 +306,13 @@ module Make(A : ARG) : S with module A = A = struct let create_and_setup (solver:SI.t) : t = let self = { tst=SI.tst solver; - cstors=N_tbl.create ~size:32 (); + cstors=ST_cstors.create_and_setup ~size:32 solver; to_decide=N_tbl.create ~size:16 (); case_split_done=T.Tbl.create 16; cards=Card.create(); } in Log.debugf 1 (fun k->k "(setup :%s)" name); SI.on_cc_new_term solver (on_new_term self); - SI.on_cc_pre_merge solver (on_pre_merge self); SI.on_final_check solver (on_final_check self); self diff --git a/src/th-data/Sidekick_th_data.mli b/src/th-data/Sidekick_th_data.mli new file mode 100644 index 00000000..dd731307 --- /dev/null +++ b/src/th-data/Sidekick_th_data.mli @@ -0,0 +1,57 @@ + +(** Datatype-oriented view of terms. + ['c] is the representation of constructors + ['t] is the representation of terms +*) +type ('c,'t) data_view = + | T_cstor of 'c * 't IArray.t + | T_select of 'c * int * 't + | T_is_a of 'c * 't + | T_other of 't + +(** View of types in a way that is directly useful for the theory of datatypes *) +type ('c, 'ty) data_ty_view = + | Ty_arrow of 'ty Iter.t * 'ty + | Ty_app of { + args: 'ty Iter.t; + } + | Ty_data of { + cstors: 'c; + } + | Ty_other + +module type ARG = sig + module S : Sidekick_core.SOLVER + + module Cstor : sig + type t + val ty_args : t -> S.T.Ty.t Iter.t + val pp : t Fmt.printer + val equal : t -> t -> bool + end + + val as_datatype : S.T.Ty.t -> (Cstor.t Iter.t, S.T.Ty.t) data_ty_view + (** Try to view type as a datatype (with its constructors) *) + + val view_as_data : S.T.Term.t -> (Cstor.t, S.T.Term.t) data_view + (** Try to view term as a datatype term *) + + val mk_cstor : S.T.Term.state -> Cstor.t -> S.T.Term.t IArray.t -> S.T.Term.t + (** Make a constructor application term *) + + val mk_is_a: S.T.Term.state -> Cstor.t -> S.T.Term.t -> S.T.Term.t + (** Make a [is-a] term *) + + val ty_is_finite : S.T.Ty.t -> bool + (** Is the given type known to be finite? *) + + val ty_set_is_finite : S.T.Ty.t -> bool -> unit + (** Modify the "finite" field (see {!ty_is_finite}) *) +end + +module type S = sig + module A : ARG + val theory : A.S.theory +end + +module Make(A : ARG) : S with module A = A From 787b9404afd2feab21598132c5a1d73a95218836 Mon Sep 17 00:00:00 2001 From: Simon Cruanes Date: Sun, 1 Dec 2019 19:40:31 -0600 Subject: [PATCH 07/29] refactor: change debug levels --- src/cc/Sidekick_cc.ml | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) diff --git a/src/cc/Sidekick_cc.ml b/src/cc/Sidekick_cc.ml index 5b234a02..87f20ea6 100644 --- a/src/cc/Sidekick_cc.ml +++ b/src/cc/Sidekick_cc.ml @@ -337,18 +337,18 @@ module Make (A: CC_ARG) (* add to signature table. Assume it's not present already *) let add_signature cc (s:signature) (n:node) : unit = assert (not @@ Sig_tbl.mem cc.signatures_tbl s); - Log.debugf 15 + Log.debugf 50 (fun k->k "(@[cc.add-sig@ %a@ ~~> %a@])" Signature.pp s N.pp n); on_backtrack cc (fun () -> Sig_tbl.remove cc.signatures_tbl s); Sig_tbl.add cc.signatures_tbl s n let push_pending cc t : unit = - Log.debugf 5 (fun k->k "(@[cc.push_pending@ %a@])" N.pp t); + Log.debugf 50 (fun k->k "(@[cc.push-pending@ %a@])" N.pp t); Vec.push cc.pending t let merge_classes cc t u e : unit = - Log.debugf 5 - (fun k->k "(@[cc.push_combine@ %a ~@ %a@ :expl %a@])" + Log.debugf 50 + (fun k->k "(@[cc.push-combine@ %a ~@ %a@ :expl %a@])" N.pp t N.pp u Expl.pp e); Vec.push cc.combine @@ CT_merge (t,u,e) @@ -778,7 +778,7 @@ module Make (A: CC_ARG) otherwise merge the atom with true/false *) let assert_lit cc lit : unit = let t = Lit.term lit in - Log.debugf 5 (fun k->k "(@[cc.assert_lit@ %a@])" Lit.pp lit); + Log.debugf 15 (fun k->k "(@[cc.assert-lit@ %a@])" Lit.pp lit); let sign = Lit.sign lit in begin match A.cc_view t with | Eq (a,b) when sign -> From 0ec9c1683f5f1a6577a7905cc4e2f7deb9014c2b Mon Sep 17 00:00:00 2001 From: Simon Cruanes Date: Sat, 7 Dec 2019 18:03:31 -0600 Subject: [PATCH 08/29] test: modify logitest config file --- tests/logitest.sexp | 24 ++++++++++++++++++++++++ 1 file changed, 24 insertions(+) create mode 100644 tests/logitest.sexp diff --git a/tests/logitest.sexp b/tests/logitest.sexp new file mode 100644 index 00000000..e8b3b921 --- /dev/null +++ b/tests/logitest.sexp @@ -0,0 +1,24 @@ + +(prover + (name sidekick-dev) + (binary "./sidekick") + (cmd "./sidekick --no-check --time $timeout $file") + (unsat "Unsat") + (sat "Sat") + (unknown "Timeout|Unknown") + (version "git:.")) + +(dir + (path tests) + (pattern ".*.(smt2|cnf)") + (expect (run z3))) + +(task + (name sidekick-local-test) + (action + (run_provers + (provers sidekick) + (timeout 10) + (dirs tests)))) + + From c4d2a800ab5776561a9a0f81f3b585493aa83768 Mon Sep 17 00:00:00 2001 From: Simon Cruanes Date: Sat, 7 Dec 2019 18:53:46 -0600 Subject: [PATCH 09/29] test: update test config to use `$cur_dir` --- tests/logitest.sexp | 8 +++----- 1 file changed, 3 insertions(+), 5 deletions(-) diff --git a/tests/logitest.sexp b/tests/logitest.sexp index e8b3b921..74466163 100644 --- a/tests/logitest.sexp +++ b/tests/logitest.sexp @@ -1,17 +1,16 @@ (prover (name sidekick-dev) - (binary "./sidekick") - (cmd "./sidekick --no-check --time $timeout $file") + (cmd "${cur_dir}/../sidekick --no-check --time $timeout $file") (unsat "Unsat") (sat "Sat") (unknown "Timeout|Unknown") (version "git:.")) (dir - (path tests) + (path $cur_dir) (pattern ".*.(smt2|cnf)") - (expect (run z3))) + (expect (try (run smtlib-read-status) (run z3)))) (task (name sidekick-local-test) @@ -21,4 +20,3 @@ (timeout 10) (dirs tests)))) - From c54ee2310ee54df0ce671c2f77558215a0a42163 Mon Sep 17 00:00:00 2001 From: Simon Cruanes Date: Mon, 9 Dec 2019 19:11:29 -0600 Subject: [PATCH 10/29] test: better conf for sidekick --- tests/logitest.sexp | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/tests/logitest.sexp b/tests/logitest.sexp index 74466163..22a421f9 100644 --- a/tests/logitest.sexp +++ b/tests/logitest.sexp @@ -16,7 +16,7 @@ (name sidekick-local-test) (action (run_provers - (provers sidekick) + (provers sidekick-dev) (timeout 10) - (dirs tests)))) + (dirs)))) From bf23f7c82661c8ca9d2f59eaac2edfd770f3a833 Mon Sep 17 00:00:00 2001 From: Simon Cruanes Date: Mon, 9 Dec 2019 21:49:29 -0600 Subject: [PATCH 11/29] fix(cc): remove too powerful assertion in CC --- src/cc/Sidekick_cc.ml | 4 +--- 1 file changed, 1 insertion(+), 3 deletions(-) diff --git a/src/cc/Sidekick_cc.ml b/src/cc/Sidekick_cc.ml index 87f20ea6..d5946010 100644 --- a/src/cc/Sidekick_cc.ml +++ b/src/cc/Sidekick_cc.ml @@ -171,9 +171,7 @@ module Make (A: CC_ARG) let mk_reduction : t = E_reduction let[@inline] mk_congruence n1 n2 : t = E_congruence (n1,n2) - let[@inline] mk_merge a b : t = - assert (same_class a b); - if N.equal a b then mk_reduction else E_merge (a,b) + let[@inline] mk_merge a b : t = if N.equal a b then mk_reduction else E_merge (a,b) let[@inline] mk_merge_t a b : t = if Term.equal a b then mk_reduction else E_merge_t (a,b) let[@inline] mk_lit l : t = E_lit l From d52fb1e5fd54a5041fba6aac21bb3dbd8fa19a6b Mon Sep 17 00:00:00 2001 From: Simon Cruanes Date: Mon, 9 Dec 2019 21:49:48 -0600 Subject: [PATCH 12/29] core: add `iter_all` in monoid class --- src/core/Sidekick_core.ml | 8 +++++++- 1 file changed, 7 insertions(+), 1 deletion(-) diff --git a/src/core/Sidekick_core.ml b/src/core/Sidekick_core.ml index 1af55db0..c782138b 100644 --- a/src/core/Sidekick_core.ml +++ b/src/core/Sidekick_core.ml @@ -680,6 +680,7 @@ module Monoid_of_repr(M : MONOID_ARG) : sig val pop_levels : t -> int -> unit val mem : t -> M.SI.CC.N.t -> bool val get : t -> M.SI.CC.N.t -> M.t option + val iter_all : t -> (M.SI.CC.N.t * M.t) Iter.t end = struct module SI = M.SI module T = SI.T.Term @@ -713,6 +714,9 @@ end = struct N_tbl.add self.values n v | None -> () + let iter_all (self:t) : _ Iter.t = + N_tbl.to_iter self.values + (* find cell for [n] *) let get_cell (self:t) (n:N.t) : M.t option = N_tbl.get self.values n @@ -736,6 +740,7 @@ end = struct M.name N.pp n1 M.pp v1 N.pp n2 M.pp v2); begin match M.merge cc n1 v1 n2 v2 with | Ok v' -> + N_tbl.remove self.values n2; (* only keep repr *) N_tbl.add self.values n1 v'; | Error expl -> (* add [n1=n2] to the conflict *) @@ -744,7 +749,8 @@ end = struct end | None, Some cr -> SI.CC.set_bitfield cc self.field_has_value true n1; - N_tbl.add self.values n1 cr + N_tbl.add self.values n1 cr; + N_tbl.remove self.values n2; (* only keep reprs *) | Some _, None -> () (* already there on the left *) | None, None -> () end From 6061b5843e8e573f47e4a675ffc8c79500ca1b99 Mon Sep 17 00:00:00 2001 From: Simon Cruanes Date: Mon, 9 Dec 2019 21:50:09 -0600 Subject: [PATCH 13/29] fix(th-data): fix merge explanation in cstor monoid --- src/th-data/Sidekick_th_data.ml | 1 + 1 file changed, 1 insertion(+) diff --git a/src/th-data/Sidekick_th_data.ml b/src/th-data/Sidekick_th_data.ml index c3c2ce06..a193eeb1 100644 --- a/src/th-data/Sidekick_th_data.ml +++ b/src/th-data/Sidekick_th_data.ml @@ -168,6 +168,7 @@ module Make(A : ARG) : S with module A = A = struct Expl.mk_list [ Expl.mk_merge n1 v1.n; Expl.mk_merge n2 v2.n; + Expl.mk_merge n1 n2; ] in if A.Cstor.equal v1.cstor v2.cstor then ( From 92935539254f031858b0fd0e12646c5292919af9 Mon Sep 17 00:00:00 2001 From: Simon Cruanes Date: Mon, 9 Dec 2019 21:50:22 -0600 Subject: [PATCH 14/29] feat(th-data): first draft of acyclicity --- src/th-data/Sidekick_th_data.ml | 87 ++++++++++++++++++++++++++++++++- src/th-data/dune | 2 +- 2 files changed, 87 insertions(+), 2 deletions(-) diff --git a/src/th-data/Sidekick_th_data.ml b/src/th-data/Sidekick_th_data.ml index a193eeb1..ebc4dc43 100644 --- a/src/th-data/Sidekick_th_data.ml +++ b/src/th-data/Sidekick_th_data.ml @@ -260,9 +260,94 @@ module Make(A : ARG) : S with module A = A = struct | Ty_data {cstors} -> cstors | _ -> assert false - (* on final check, make sure we have done case split on all terms that + module Acyclicity_ = struct + type st = { + n: N.t; + mutable flag: flag; + cstor: Monoid_cstor.t; + } + and parent_uplink = { + parent: st; + t_eq_n: T.t; + } + and flag = + | New | Done + | Current of parent_uplink option + + let pp_st out st = + Fmt.fprintf out "(@[st :cstor %a@ :flag %s@])" + Monoid_cstor.pp st.cstor + (match st.flag with + | New -> "new" | Done -> "done" + | Current None -> "current-top" | Current _ -> "current(_)") + + let pp_parent out {parent; t_eq_n} = + Fmt.fprintf out "(@[parent@ :n %a@ :by-eq-t %a@])" + N.pp parent.n T.pp t_eq_n + + let check (self:t) (solver:SI.t) (acts:SI.actions) : unit = + let module Tbl = CCHashtbl.Make(N) in + let cc = SI.cc solver in + let tbl : st Tbl.t = Tbl.create 32 in + (* traverse [n] with state [st], possibly from an equality [n=t_eq_n] *) + let rec traverse ?parent (n:N.t) (st:st) : unit = + Log.debugf 50 + (fun k->k "(@[data.acycl.traverse %a@ :st %a@ :parent %a@])" + N.pp n pp_st st (Fmt.Dump.option pp_parent) parent); + match st.flag with + | Done -> () + | New -> + st.flag <- Current parent; + traverse_sub n st; + st.flag <- Done + | Current _parent -> + let parent = CCOpt.or_ ~else_:_parent parent in + Log.debugf 20 + (fun k->k "(@[data.acycl.found-loop@ %a@ :st %a@ :parent %a@])" + N.pp n pp_st st (Fmt.Dump.option pp_parent) parent); + (* conflict, we found a loop! *) + let rec mk_path acc n parent = + Log.debugf 100 + (fun k->k "(@[data.acycl.mk-path %a %a@])" N.pp n pp_parent parent); + let acc = Expl.mk_merge_t (N.term n) parent.t_eq_n :: acc in + let acc = Expl.mk_merge parent.parent.n parent.parent.cstor.n :: acc in + match parent.parent.flag with + | Current (Some p') -> mk_path acc parent.parent.n p' + | _ -> acc + in + let c0 = [Expl.mk_merge n st.cstor.n;] in + let c = match parent with + | None -> c0 + | Some parent -> mk_path c0 n parent + in + SI.CC.raise_conflict_from_expl cc acts (Expl.mk_list c) + (* traverse constructor arguments *) + and traverse_sub n st: unit = + IArray.iter + (fun sub_t -> + let sub = SI.CC.find_t cc sub_t in + match Tbl.get tbl sub with + | None -> () + | Some st' -> + let parent = {parent=st; t_eq_n=sub_t} in + traverse ~parent sub st') + st.cstor.args; + in + begin + (* populate tbl with [repr->cstor] *) + ST_cstors.iter_all self.cstors + (fun (n, cstor) -> + assert (not @@ Tbl.mem tbl n); + Tbl.add tbl n {cstor; n; flag=New}); + Tbl.iter (fun n st -> traverse n st) tbl; + end + end + + (* on final check, check acyclicity, + then make sure we have done case split on all terms that need it. *) let on_final_check (self:t) (solver:SI.t) (acts:SI.actions) _trail = + Acyclicity_.check self solver acts; let remaining_to_decide = N_tbl.to_iter self.to_decide |> Iter.map (fun (n,_) -> SI.cc_find solver n) diff --git a/src/th-data/dune b/src/th-data/dune index 9dd86c15..f1dfcd0f 100644 --- a/src/th-data/dune +++ b/src/th-data/dune @@ -4,5 +4,5 @@ (name Sidekick_th_data) (public_name sidekick.th-data) (libraries containers sidekick.core sidekick.util) - (flags :standard -open Sidekick_util -w -32)) ; TODO get warning back + (flags :standard -open Sidekick_util -w -27-32)) ; TODO get warning back From 858ffb6f2587ca5593417be1c9f95fe727390e9e Mon Sep 17 00:00:00 2001 From: Simon Cruanes Date: Mon, 9 Dec 2019 22:38:26 -0600 Subject: [PATCH 15/29] chore: add `--progress` in makefile --- Makefile | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Makefile b/Makefile index dd8be457..0e835d01 100644 --- a/Makefile +++ b/Makefile @@ -26,7 +26,7 @@ clean: test: @dune runtest --force --no-buffer -TESTOPTS ?= -j $(J) -c tests/benchpress.sexp +TESTOPTS ?= -j $(J) -c tests/benchpress.sexp --progress TESTTOOL=benchpress DATE=$(shell date +%FT%H:%M) From 6aafaad48f3f58db2eec039347a42ba1c4511a6c Mon Sep 17 00:00:00 2001 From: Simon Cruanes Date: Sat, 28 Dec 2019 06:15:50 -0600 Subject: [PATCH 16/29] feat(data): store is-a/select parents in a monoid --- src/cc/Sidekick_cc.ml | 4 +- src/core/Sidekick_core.ml | 80 ++++++++++++++++++---- src/main/sidekick_version.ml | 2 +- src/th-cstor/Sidekick_th_cstor.ml | 6 +- src/th-data/Sidekick_th_data.ml | 109 +++++++++++++++++++++++------- 5 files changed, 159 insertions(+), 42 deletions(-) diff --git a/src/cc/Sidekick_cc.ml b/src/cc/Sidekick_cc.ml index d5946010..64b587c5 100644 --- a/src/cc/Sidekick_cc.ml +++ b/src/cc/Sidekick_cc.ml @@ -282,7 +282,9 @@ module Make (A: CC_ARG) let[@inline] true_ cc = Lazy.force cc.true_ let[@inline] false_ cc = Lazy.force cc.false_ let[@inline] term_state cc = cc.tst - let[@inline] allocate_bitfield cc = Bits.mk_field cc.bitgen + let allocate_bitfield ~descr cc = + Log.debugf 5 (fun k->k "(@[cc.allocate-bit-field@ :descr %s@])" descr); + Bits.mk_field cc.bitgen let[@inline] on_backtrack cc f : unit = Backtrack_stack.push_if_nonzero_level cc.undo f diff --git a/src/core/Sidekick_core.ml b/src/core/Sidekick_core.ml index c782138b..2688a5db 100644 --- a/src/core/Sidekick_core.ml +++ b/src/core/Sidekick_core.ml @@ -231,7 +231,7 @@ module type CC_S = sig t (** Create a new congruence closure. *) - val allocate_bitfield : t -> N.bitfield + val allocate_bitfield : descr:string -> t -> N.bitfield (** Allocate a new bitfield for the nodes. See {!N.bitfield}. *) @@ -668,11 +668,24 @@ module type MONOID_ARG = sig module SI : SOLVER_INTERNAL type t val pp : t Fmt.printer - val name : string (* name of the monoid's value (short) *) - val of_term : SI.CC.N.t -> SI.T.Term.t -> t option + val name : string + (** name of the monoid's value (short) *) + + val of_term : + SI.CC.N.t -> SI.T.Term.t -> + (t option * (SI.T.Term.t * t) list) + (** [of_term n t], where [t] is the term annotating node [n], + returns [maybe_m, l], where: + - [maybe_m = Some m] if [t] has monoid value [m]; + otherwise [maybe_m=None] + - [l] is a list of [(u, m_u)] where each [u] is a direct subterm of [t] + and [m_u] is the monoid value attached to [u]. + *) + val merge : SI.CC.t -> SI.CC.N.t -> t -> SI.CC.N.t -> t -> (t, SI.CC.Expl.t) result end +(** Keep track of monoid state per equivalence class *) module Monoid_of_repr(M : MONOID_ARG) : sig type t val create_and_setup : ?size:int -> M.SI.t -> t @@ -680,7 +693,7 @@ module Monoid_of_repr(M : MONOID_ARG) : sig val pop_levels : t -> int -> unit val mem : t -> M.SI.CC.N.t -> bool val get : t -> M.SI.CC.N.t -> M.t option - val iter_all : t -> (M.SI.CC.N.t * M.t) Iter.t + val iter_all : t -> (M.SI.CC.repr * M.t) Iter.t end = struct module SI = M.SI module T = SI.T.Term @@ -704,15 +717,52 @@ end = struct let get self n = N_tbl.get self.values n - let on_new_term self cc n (t:T.t) = - match M.of_term n t with - | Some v -> - Log.debugf 20 - (fun k->k "(@[monoid[%s].on-new-term@ :n %a@ :value %a@])" - M.name N.pp n M.pp v); - SI.CC.set_bitfield cc self.field_has_value true n; - N_tbl.add self.values n v - | None -> () + let on_new_term self cc n (t:T.t) : unit = + let maybe_m, l = M.of_term n t in + begin match maybe_m with + | Some v -> + Log.debugf 20 + (fun k->k "(@[monoid[%s].on-new-term@ :n %a@ :value %a@])" + M.name N.pp n M.pp v); + SI.CC.set_bitfield cc self.field_has_value true n; + N_tbl.add self.values n v + | None -> () + end; + List.iter + (fun (u,m_u) -> + Log.debugf 20 + (fun k->k "(@[monoid[%s].on-new-term.sub@ :n %a@ :sub-t %a@ :value %a@])" + M.name N.pp n T.pp u M.pp m_u); + let n_u = + try CC.find_t cc u + with Not_found -> Error.errorf "subterm %a does not have a repr" T.pp u + in + if N.get_field self.field_has_value n_u then ( + let m_u' = + try N_tbl.find self.values n_u + with Not_found -> + Error.errorf "node %a has bitfield but no value" N.pp n_u + in + match M.merge cc n_u m_u n_u m_u' with + | Error expl -> + Error.errorf + "when merging@ @[for node %a@],@ \ + values %a and %a:@ conflict %a" + N.pp n_u M.pp m_u M.pp m_u' CC.Expl.pp expl + | Ok m_u_merged -> + Log.debugf 20 + (fun k->k "(@[monoid[%s].on-new-term.sub.merged@ \ + :n %a@ :sub-t %a@ :value %a@])" + M.name N.pp n T.pp u M.pp m_u_merged); + N_tbl.add self.values n_u m_u_merged; + ) else ( + (* just add to [n_u] *) + SI.CC.set_bitfield cc self.field_has_value true n_u; + N_tbl.add self.values n_u m_u; + ) + ) + l; + () let iter_all (self:t) : _ Iter.t = N_tbl.to_iter self.values @@ -756,7 +806,9 @@ end = struct end let create_and_setup ?size (solver:SI.t) : t = - let field_has_value = SI.CC.allocate_bitfield (SI.cc solver) in + let field_has_value = + SI.CC.allocate_bitfield ~descr:("monoid."^M.name^".has-value") + (SI.cc solver) in let self = { values=N_tbl.create ?size (); field_has_value; } in SI.on_cc_new_term solver (on_new_term self); SI.on_cc_pre_merge solver (on_pre_merge self); diff --git a/src/main/sidekick_version.ml b/src/main/sidekick_version.ml index bcefbe83..2c10c6ef 100644 --- a/src/main/sidekick_version.ml +++ b/src/main/sidekick_version.ml @@ -1,2 +1,2 @@ -let version = {git|ef77e1e729f176c3db680de25df9f2f820795e47 +let version = {git|858ffb6f2587ca5593417be1c9f95fe727390e9e |git} \ No newline at end of file diff --git a/src/th-cstor/Sidekick_th_cstor.ml b/src/th-cstor/Sidekick_th_cstor.ml index 688e5cbd..0c8f7a60 100644 --- a/src/th-cstor/Sidekick_th_cstor.ml +++ b/src/th-cstor/Sidekick_th_cstor.ml @@ -40,10 +40,10 @@ module Make(A : ARG) : S with module A = A = struct Fmt.fprintf out "(@[cstor %a@ :term %a@])" Fun.pp v.cstor T.pp v.t (* attach data to constructor terms *) - let of_term n (t:T.t) : _ option = + let of_term n (t:T.t) : _ option * _ = match A.view_as_cstor t with - | T_cstor (cstor,args) -> Some {n; t; cstor; args} - | _ -> None + | T_cstor (cstor,args) -> Some {n; t; cstor; args}, [] + | _ -> None, [] let merge cc n1 v1 n2 v2 : _ result = Log.debugf 5 diff --git a/src/th-data/Sidekick_th_data.ml b/src/th-data/Sidekick_th_data.ml index ebc4dc43..1ede288c 100644 --- a/src/th-data/Sidekick_th_data.ml +++ b/src/th-data/Sidekick_th_data.ml @@ -138,77 +138,139 @@ module Make(A : ARG) : S with module A = A = struct module Card = Compute_card(A) + (** Monoid mapping each class to the (unique) constructor it contains, + if any *) module Monoid_cstor = struct module SI = SI + let name = "th-data.cstor" (* associate to each class a unique constructor term in the class (if any) *) type t = { - t: T.t; - n: N.t; - cstor: A.Cstor.t; - args: T.t IArray.t; + c_n: N.t; + c_cstor: A.Cstor.t; + c_args: T.t IArray.t; } - let name = "th-data.cstor" let pp out (v:t) = - Fmt.fprintf out "(@[cstor %a@ :term %a@])" A.Cstor.pp v.cstor T.pp v.t + Fmt.fprintf out "(@[%s@ :cstor %a@])" name A.Cstor.pp v.c_cstor (* attach data to constructor terms *) - let of_term n (t:T.t) : _ option = + let of_term n (t:T.t) : _ option * _ list = match A.view_as_data t with - | T_cstor (cstor,args) -> Some {n; t; cstor; args} - | _ -> None + | T_cstor (cstor,args) -> + Some {c_n=n;c_cstor=cstor; c_args=args}, [] + | _ -> None, [] - let merge cc n1 v1 n2 v2 : _ result = + let merge cc n1 c1 n2 c2 : _ result = Log.debugf 5 - (fun k->k "(@[%s.merge@ @[:c1 %a (t %a)@]@ @[:c2 %a (t %a)@]@])" - name N.pp n1 T.pp v1.t N.pp n2 T.pp v2.t); + (fun k->k "(@[%s.merge@ @[:c1 %a %a@]@ @[:c2 %a %a@]@])" + name N.pp n1 pp c1 N.pp n2 pp c2); (* build full explanation of why the constructor terms are equal *) let expl = Expl.mk_list [ - Expl.mk_merge n1 v1.n; - Expl.mk_merge n2 v2.n; + Expl.mk_merge n1 c1.c_n; + Expl.mk_merge n2 c2.c_n; Expl.mk_merge n1 n2; ] in - if A.Cstor.equal v1.cstor v2.cstor then ( + if A.Cstor.equal c1.c_cstor c2.c_cstor then ( (* same function: injectivity *) - assert (IArray.length v1.args = IArray.length v2.args); + assert (IArray.length c1.c_args = IArray.length c2.c_args); IArray.iter2 (fun u1 u2 -> SI.CC.merge_t cc u1 u2 expl) - v1.args v2.args; - Ok v1 + c1.c_args c2.c_args; + Ok c1 ) else ( (* different function: disjointness *) Error expl ) end + (** Monoid mapping each class to the set of is-a/select of which it + is the argument *) + module Monoid_parents = struct + module SI = SI + let name = "th-data.parents" + + type select = { + sel_n: N.t; + sel_cstor: A.Cstor.t; + sel_idx: int; + } + + type is_a = { + is_a_n: N.t; + is_a_cstor: A.Cstor.t; + } + + (* associate to each class a unique constructor term in the class (if any) *) + type t = { + parent_is_a: is_a list;(* parents that are [is-a] *) + parent_select: select list; (* parents that are [select] *) + } + + let pp_select out s = Fmt.fprintf out "sel[%d]-%a" s.sel_idx A.Cstor.pp s.sel_cstor + let pp_is_a out s = Fmt.fprintf out "is-%a" A.Cstor.pp s.is_a_cstor + let pp out (v:t) = + Fmt.fprintf out + "(@[%s@ @[:sel [@[%a@]]@]@ @[:is-a [@[%a@]]@]@])" + name + (Util.pp_list pp_select) v.parent_select + (Util.pp_list pp_is_a) v.parent_is_a + + (* attach data to constructor terms *) + let of_term n (t:T.t) : _ option * _ list = + match A.view_as_data t with + | T_select (c, i, u) -> + let m_sel = { + parent_select=[{sel_n=n; sel_idx=i; sel_cstor=c}]; + parent_is_a=[]; + } in + None, [u, m_sel] + | T_is_a (c, u) -> + let m_sel = { + parent_is_a=[{is_a_n=n; is_a_cstor=c}]; + parent_select=[]; + } in + None, [u, m_sel] + | T_cstor _ | T_other _ -> None, [] + + let merge cc n1 v1 n2 v2 : _ result = + Log.debugf 5 + (fun k->k "(@[%s.merge@ @[:c1 %a %a@]@ @[:c2 %a %a@]@])" + name N.pp n1 pp v1 N.pp n2 pp v2); + let parent_is_a = v1.parent_is_a @ v2.parent_is_a in + let parent_select = v1.parent_select @ v2.parent_select in + Ok {parent_is_a; parent_select;} + end + module ST_cstors = Sidekick_core.Monoid_of_repr(Monoid_cstor) + module ST_parents = Sidekick_core.Monoid_of_repr(Monoid_parents) module N_tbl = Backtrackable_tbl.Make(N) type t = { tst: T.state; cstors: ST_cstors.t; (* repr -> cstor for the class *) + parents: ST_parents.t; (* repr -> parents for the class *) cards: Card.t; (* remember finiteness *) to_decide: unit N_tbl.t; (* set of terms to decide. *) case_split_done: unit T.Tbl.t; (* set of terms for which case split is done *) - (* TODO: also allocate a bit in CC to filter out quickly classes without cstors? *) (* TODO: bitfield for types with less than 62 cstors, to quickly detect conflict? *) } let push_level self = ST_cstors.push_level self.cstors; + ST_parents.push_level self.parents; N_tbl.push_level self.to_decide; () let pop_levels self n = ST_cstors.pop_levels self.cstors n; + ST_parents.pop_levels self.parents n; N_tbl.pop_levels self.to_decide n; () (* TODO: select/is-a *) - (* TODO: acyclicity *) (* TODO: remove (* attach data to constructor terms *) @@ -310,12 +372,12 @@ module Make(A : ARG) : S with module A = A = struct Log.debugf 100 (fun k->k "(@[data.acycl.mk-path %a %a@])" N.pp n pp_parent parent); let acc = Expl.mk_merge_t (N.term n) parent.t_eq_n :: acc in - let acc = Expl.mk_merge parent.parent.n parent.parent.cstor.n :: acc in + let acc = Expl.mk_merge parent.parent.n parent.parent.n :: acc in match parent.parent.flag with | Current (Some p') -> mk_path acc parent.parent.n p' | _ -> acc in - let c0 = [Expl.mk_merge n st.cstor.n;] in + let c0 = [Expl.mk_merge n st.n;] in let c = match parent with | None -> c0 | Some parent -> mk_path c0 n parent @@ -331,7 +393,7 @@ module Make(A : ARG) : S with module A = A = struct | Some st' -> let parent = {parent=st; t_eq_n=sub_t} in traverse ~parent sub st') - st.cstor.args; + st.cstor.Monoid_cstor.c_args; in begin (* populate tbl with [repr->cstor] *) @@ -393,6 +455,7 @@ module Make(A : ARG) : S with module A = A = struct let self = { tst=SI.tst solver; cstors=ST_cstors.create_and_setup ~size:32 solver; + parents=ST_parents.create_and_setup ~size:32 solver; to_decide=N_tbl.create ~size:16 (); case_split_done=T.Tbl.create 16; cards=Card.create(); From 91e9b6cc2c4319c5f35d998ec00a1dde9fb62ca1 Mon Sep 17 00:00:00 2001 From: Simon Cruanes Date: Sat, 28 Dec 2019 07:08:23 -0600 Subject: [PATCH 17/29] feat: initial support for is-a/select --- src/cc/Sidekick_cc.ml | 31 ++++++++------- src/core/Sidekick_core.ml | 9 ++++- src/main/sidekick_version.ml | 2 +- src/th-data/Sidekick_th_data.ml | 70 +++++++++++++++++++++++++++++++-- 4 files changed, 92 insertions(+), 20 deletions(-) diff --git a/src/cc/Sidekick_cc.ml b/src/cc/Sidekick_cc.ml index 64b587c5..43cacb61 100644 --- a/src/cc/Sidekick_cc.ml +++ b/src/cc/Sidekick_cc.ml @@ -279,8 +279,9 @@ module Make (A: CC_ARG) and ev_on_propagate = t -> lit -> (unit -> lit list) -> unit let[@inline] size_ (r:repr) = r.n_size - let[@inline] true_ cc = Lazy.force cc.true_ - let[@inline] false_ cc = Lazy.force cc.false_ + let[@inline] n_true cc = Lazy.force cc.true_ + let[@inline] n_false cc = Lazy.force cc.false_ + let n_bool cc b = if b then n_true cc else n_false cc let[@inline] term_state cc = cc.tst let allocate_bitfield ~descr cc = Log.debugf 5 (fun k->k "(@[cc.allocate-bit-field@ :descr %s@])" descr); @@ -557,7 +558,7 @@ module Make (A: CC_ARG) n.n_as_lit <- Some lit let n_is_bool (self:t) n : bool = - N.equal n (true_ self) || N.equal n (false_ self) + N.equal n (n_true self) || N.equal n (n_false self) (* main CC algo: add terms from [pending] to the signature table, check for collisions *) @@ -581,17 +582,17 @@ module Make (A: CC_ARG) let expl = Expl.mk_merge a b in Log.debugf 5 (fun k->k "(pending.eq@ %a@ :r1 %a@ :r2 %a@])" N.pp n N.pp a N.pp b); - merge_classes cc n (true_ cc) expl + merge_classes cc n (n_true cc) expl ) | Some (Not u) -> (* [u = bool ==> not u = not bool] *) let r_u = find_ u in - if N.equal r_u (true_ cc) then ( - let expl = Expl.mk_merge u (true_ cc) in - merge_classes cc n (false_ cc) expl - ) else if N.equal r_u (false_ cc) then ( - let expl = Expl.mk_merge u (false_ cc) in - merge_classes cc n (true_ cc) expl + if N.equal r_u (n_true cc) then ( + let expl = Expl.mk_merge u (n_true cc) in + merge_classes cc n (n_false cc) expl + ) else if N.equal r_u (n_false cc) then ( + let expl = Expl.mk_merge u (n_false cc) in + merge_classes cc n (n_true cc) expl ) | Some s0 -> (* update the signature by using [find] on each sub-node *) @@ -622,8 +623,8 @@ module Make (A: CC_ARG) assert (N.is_root rb); Stat.incr cc.count_merge; (* check we're not merging [true] and [false] *) - if (N.equal ra (true_ cc) && N.equal rb (false_ cc)) || - (N.equal rb (true_ cc) && N.equal ra (false_ cc)) then ( + if (N.equal ra (n_true cc) && N.equal rb (n_false cc)) || + (N.equal rb (n_true cc) && N.equal ra (n_false cc)) then ( Log.debugf 5 (fun k->k "(@[cc.merge.true_false_conflict@ \ @[:r1 %a@ :t1 %a@]@ @[:r2 %a@ :t2 %a@]@ :e_ab %a@])" @@ -644,9 +645,9 @@ module Make (A: CC_ARG) in (* when merging terms with [true] or [false], possibly propagate them to SAT *) let merge_bool r1 t1 r2 t2 = - if N.equal r1 (true_ cc) then ( + if N.equal r1 (n_true cc) then ( propagate_bools cc acts r2 t2 r1 t1 e_ab true - ) else if N.equal r1 (false_ cc) then ( + ) else if N.equal r1 (n_false cc) then ( propagate_bools cc acts r2 t2 r1 t1 e_ab false ) in @@ -788,7 +789,7 @@ module Make (A: CC_ARG) merge_classes cc a b (Expl.mk_lit lit) | _ -> (* equate t and true/false *) - let rhs = if sign then true_ cc else false_ cc in + let rhs = if sign then n_true cc else n_false cc in let n = add_term cc t in (* TODO: ensure that this is O(1). basically, just have [n] point to true/false and thus acquire diff --git a/src/core/Sidekick_core.ml b/src/core/Sidekick_core.ml index 2688a5db..165f025f 100644 --- a/src/core/Sidekick_core.ml +++ b/src/core/Sidekick_core.ml @@ -282,6 +282,10 @@ module type CC_S = sig it must be a theory tautology that [expl ==> absurd]. To be used in theories. *) + val n_true : t -> N.t + val n_false : t -> N.t + val n_bool : t -> bool -> N.t + val merge : t -> N.t -> N.t -> Expl.t -> unit (** Merge these two nodes given this explanation. It must be a theory tautology that [expl ==> n1 = n2]. @@ -715,7 +719,10 @@ end = struct assert (if res then N_tbl.mem self.values n else true); res - let get self n = N_tbl.get self.values n + let get self n = + if N.get_field self.field_has_value n + then N_tbl.get self.values n + else None let on_new_term self cc n (t:T.t) : unit = let maybe_m, l = M.of_term n t in diff --git a/src/main/sidekick_version.ml b/src/main/sidekick_version.ml index 2c10c6ef..068fdc87 100644 --- a/src/main/sidekick_version.ml +++ b/src/main/sidekick_version.ml @@ -1,2 +1,2 @@ -let version = {git|858ffb6f2587ca5593417be1c9f95fe727390e9e +let version = {git|6aafaad48f3f58db2eec039347a42ba1c4511a6c |git} \ No newline at end of file diff --git a/src/th-data/Sidekick_th_data.ml b/src/th-data/Sidekick_th_data.ml index 1ede288c..f7f0ac78 100644 --- a/src/th-data/Sidekick_th_data.ml +++ b/src/th-data/Sidekick_th_data.ml @@ -313,15 +313,78 @@ module Make(A : ARG) : S with module A = A = struct ) | _ -> () - let on_new_term self _solver n t = - on_new_term_look_at_ty self n t; - () + let on_new_term (self:t) cc (n:N.t) (t:T.t) : unit = + on_new_term_look_at_ty self n t; (* might have to decide [t] *) + match A.view_as_data t with + | T_is_a (c_t, u) -> + let n_u = SI.CC.add_term cc u in + let repr_u = SI.CC.find cc n_u in + begin match ST_cstors.get self.cstors repr_u with + | None -> () + | Some cstor -> + let is_true = A.Cstor.equal cstor.c_cstor c_t in + Log.debugf 5 + (fun k->k "(@[%s.on-new-term.is-a.reduce@ :to %B@ :n %a@ :sub-cstor %a@])" + name is_true N.pp n Monoid_cstor.pp cstor); + SI.CC.merge cc n (SI.CC.n_bool cc is_true) (Expl.mk_merge n_u repr_u) + end + | T_select (c_t, i, u) -> + let n_u = SI.CC.add_term cc u in + let repr_u = SI.CC.find cc n_u in + begin match ST_cstors.get self.cstors repr_u with + | Some cstor when A.Cstor.equal cstor.c_cstor c_t -> + Log.debugf 5 + (fun k->k "(@[%s.on-new-term.select.reduce@ :n %a@ :sel get[%d]-%a@])" + name N.pp n i A.Cstor.pp c_t); + assert (i < IArray.length cstor.c_args); + let u_i = IArray.get cstor.c_args i in + let n_u_i = SI.CC.add_term cc u_i in + SI.CC.merge cc n n_u_i (Expl.mk_merge n_u repr_u) + | _ -> () + end + | T_cstor _ | T_other _ -> () let cstors_of_ty (ty:Ty.t) : A.Cstor.t Iter.t = match A.as_datatype ty with | Ty_data {cstors} -> cstors | _ -> assert false + let on_pre_merge (self:t) (cc:SI.CC.t) acts n1 n2 expl : unit = + let merge_is_a n1 (c1:Monoid_cstor.t) n2 (is_a2:Monoid_parents.is_a) = + let is_true = A.Cstor.equal c1.c_cstor is_a2.is_a_cstor in + Log.debugf 50 + (fun k->k "(@[%s.on-new-term.is-a.reduce@ :to %B@ :n %a@ :sub-cstor %a@])" + name is_true N.pp n2 Monoid_cstor.pp c1); + SI.CC.merge cc n2 (SI.CC.n_bool cc is_true) + Expl.(mk_list [mk_merge n1 c1.c_n; mk_merge n2 is_a2.is_a_n]) + in + let merge_select n1 (c1:Monoid_cstor.t) n2 (sel2:Monoid_parents.select) = + if A.Cstor.equal c1.c_cstor sel2.sel_cstor then ( + Log.debugf 5 + (fun k->k "(@[%s.on-new-term.select.reduce@ :n %a@ :sel get[%d]-%a@])" + name N.pp n2 sel2.sel_idx Monoid_cstor.pp c1); + assert (sel2.sel_idx < IArray.length c1.c_args); + let u_i = IArray.get c1.c_args sel2.sel_idx in + let n_u_i = SI.CC.add_term cc u_i in + SI.CC.merge cc n2 n_u_i + Expl.(mk_list [mk_merge n1 c1.c_n; mk_merge n2 sel2.sel_n]); + ) + in + let merge_c_p n1 n2 = + match ST_cstors.get self.cstors n1, ST_parents.get self.parents n2 with + | None, _ + | _, None -> () + | Some c1, Some p2 -> + Log.debugf 50 + (fun k->k "(@[%s.pre-merge@ @[:n1 %a@ :c1 %a@]@ @[:n2 %a@ :p2 %a@]@])" + name N.pp n1 Monoid_cstor.pp c1 N.pp n2 Monoid_parents.pp p2); + List.iter (fun is_a2 -> merge_is_a n1 c1 n2 is_a2) p2.parent_is_a; + List.iter (fun s2 -> merge_select n1 c1 n2 s2) p2.parent_select; + in + merge_c_p n1 n2; + merge_c_p n2 n1; + () + module Acyclicity_ = struct type st = { n: N.t; @@ -462,6 +525,7 @@ module Make(A : ARG) : S with module A = A = struct } in Log.debugf 1 (fun k->k "(setup :%s)" name); SI.on_cc_new_term solver (on_new_term self); + SI.on_cc_pre_merge solver (on_pre_merge self); SI.on_final_check solver (on_final_check self); self From 62b1d83cd665ebbcba04805d0a5e01d44603f3f5 Mon Sep 17 00:00:00 2001 From: Simon Cruanes Date: Sat, 28 Dec 2019 08:19:59 -0600 Subject: [PATCH 18/29] debug: add type checking in `CC.merge` --- src/cc/Sidekick_cc.ml | 1 + 1 file changed, 1 insertion(+) diff --git a/src/cc/Sidekick_cc.ml b/src/cc/Sidekick_cc.ml index 43cacb61..eb05fb64 100644 --- a/src/cc/Sidekick_cc.ml +++ b/src/cc/Sidekick_cc.ml @@ -813,6 +813,7 @@ module Make (A: CC_ARG) let merge cc n1 n2 expl = Log.debugf 5 (fun k->k "(@[cc.theory.merge@ :n1 %a@ :n2 %a@ :expl %a@])" N.pp n1 N.pp n2 Expl.pp expl); + assert (T.Ty.equal (T.Term.ty n1.n_term) (T.Term.ty n2.n_term)); merge_classes cc n1 n2 expl let[@inline] merge_t cc t1 t2 expl = From 9ba5f508cebb82e98f6b4ad3e052bb5fb7ad4775 Mon Sep 17 00:00:00 2001 From: Simon Cruanes Date: Sat, 28 Dec 2019 08:31:41 -0600 Subject: [PATCH 19/29] feat(main): simpler computation of version --- src/main/dune | 5 +---- src/main/sidekick_version.ml | 3 +-- 2 files changed, 2 insertions(+), 6 deletions(-) diff --git a/src/main/dune b/src/main/dune index 689f2e91..188312bd 100644 --- a/src/main/dune +++ b/src/main/dune @@ -14,9 +14,6 @@ (mode promote) (action (with-stdout-to %{targets} - (progn - (echo "let version = {git|") - (run git rev-parse HEAD) - (echo "|git}"))))) + (echo "let version = {git|%{version:sidekick}|git}")))) (ocamllex (modules Dimacs_lexer)) diff --git a/src/main/sidekick_version.ml b/src/main/sidekick_version.ml index 068fdc87..fa6207d0 100644 --- a/src/main/sidekick_version.ml +++ b/src/main/sidekick_version.ml @@ -1,2 +1 @@ -let version = {git|6aafaad48f3f58db2eec039347a42ba1c4511a6c -|git} \ No newline at end of file +let version = {git|dev|git} \ No newline at end of file From 6f67593be13ca43c8600f1dd51653d45b4e8c44e Mon Sep 17 00:00:00 2001 From: Simon Cruanes Date: Sat, 28 Dec 2019 08:31:52 -0600 Subject: [PATCH 20/29] feat(data): fixes (decide args of is-a/select; rearrange reduction rules) --- src/th-data/Sidekick_th_data.ml | 25 +++++++++++++++---------- 1 file changed, 15 insertions(+), 10 deletions(-) diff --git a/src/th-data/Sidekick_th_data.ml b/src/th-data/Sidekick_th_data.ml index f7f0ac78..900d1bef 100644 --- a/src/th-data/Sidekick_th_data.ml +++ b/src/th-data/Sidekick_th_data.ml @@ -209,8 +209,8 @@ module Make(A : ARG) : S with module A = A = struct parent_select: select list; (* parents that are [select] *) } - let pp_select out s = Fmt.fprintf out "sel[%d]-%a" s.sel_idx A.Cstor.pp s.sel_cstor - let pp_is_a out s = Fmt.fprintf out "is-%a" A.Cstor.pp s.is_a_cstor + let pp_select out s = Fmt.fprintf out "(@[sel[%d]-%a@ :n %a@])" s.sel_idx A.Cstor.pp s.sel_cstor N.pp s.sel_n + let pp_is_a out s = Fmt.fprintf out "(@[is-%a@ :n %a@])" A.Cstor.pp s.is_a_cstor N.pp s.is_a_n let pp out (v:t) = Fmt.fprintf out "(@[%s@ @[:sel [@[%a@]]@]@ @[:is-a [@[%a@]]@]@])" @@ -320,7 +320,8 @@ module Make(A : ARG) : S with module A = A = struct let n_u = SI.CC.add_term cc u in let repr_u = SI.CC.find cc n_u in begin match ST_cstors.get self.cstors repr_u with - | None -> () + | None -> + N_tbl.add self.to_decide repr_u (); (* needs to be decided *) | Some cstor -> let is_true = A.Cstor.equal cstor.c_cstor c_t in Log.debugf 5 @@ -340,7 +341,9 @@ module Make(A : ARG) : S with module A = A = struct let u_i = IArray.get cstor.c_args i in let n_u_i = SI.CC.add_term cc u_i in SI.CC.merge cc n n_u_i (Expl.mk_merge n_u repr_u) - | _ -> () + | Some _ -> () + | None -> + N_tbl.add self.to_decide repr_u (); (* needs to be decided *) end | T_cstor _ | T_other _ -> () @@ -349,25 +352,27 @@ module Make(A : ARG) : S with module A = A = struct | Ty_data {cstors} -> cstors | _ -> assert false + (* FIXME: when merging [(is _ C) t] with true, propagate [t=C(sel[1]-c(t),…)] *) + (* FIXME: when merging [(is _ C) t] with false, remove [C] from the available list *) let on_pre_merge (self:t) (cc:SI.CC.t) acts n1 n2 expl : unit = let merge_is_a n1 (c1:Monoid_cstor.t) n2 (is_a2:Monoid_parents.is_a) = let is_true = A.Cstor.equal c1.c_cstor is_a2.is_a_cstor in Log.debugf 50 - (fun k->k "(@[%s.on-new-term.is-a.reduce@ :to %B@ :n %a@ :sub-cstor %a@])" + (fun k->k "(@[%s.on-merge.is-a.reduce@ :to %B@ :n %a@ :sub-cstor %a@])" name is_true N.pp n2 Monoid_cstor.pp c1); - SI.CC.merge cc n2 (SI.CC.n_bool cc is_true) - Expl.(mk_list [mk_merge n1 c1.c_n; mk_merge n2 is_a2.is_a_n]) + SI.CC.merge cc is_a2.is_a_n (SI.CC.n_bool cc is_true) + Expl.(mk_list [mk_merge n1 c1.c_n; mk_merge n1 n2]) in let merge_select n1 (c1:Monoid_cstor.t) n2 (sel2:Monoid_parents.select) = if A.Cstor.equal c1.c_cstor sel2.sel_cstor then ( Log.debugf 5 - (fun k->k "(@[%s.on-new-term.select.reduce@ :n %a@ :sel get[%d]-%a@])" + (fun k->k "(@[%s.on-merge.select.reduce@ :n %a@ :sel get[%d]-%a@])" name N.pp n2 sel2.sel_idx Monoid_cstor.pp c1); assert (sel2.sel_idx < IArray.length c1.c_args); let u_i = IArray.get c1.c_args sel2.sel_idx in let n_u_i = SI.CC.add_term cc u_i in - SI.CC.merge cc n2 n_u_i - Expl.(mk_list [mk_merge n1 c1.c_n; mk_merge n2 sel2.sel_n]); + SI.CC.merge cc sel2.sel_n n_u_i + Expl.(mk_list [mk_merge n1 c1.c_n; mk_merge n1 n2]); ) in let merge_c_p n1 n2 = From b250587a5f509913fd401f2a63ae6ee306f82acb Mon Sep 17 00:00:00 2001 From: Simon Cruanes Date: Sat, 28 Dec 2019 08:34:20 -0600 Subject: [PATCH 21/29] tst: add some regression tests; remove dead file --- tests/logitest.sexp | 22 ------------------- tests/sat/v1l40032.cvc.smt2 | 28 ++++++++++++++++++++++++ tests/unsat/t_cstor1.smt2.tmp | 23 +++++++++++++++++++ tests/unsat/typed_v3l30091.cvc.smt2 | 34 +++++++++++++++++++++++++++++ tests/unsat/v3l60049.cvc.smt2 | 34 +++++++++++++++++++++++++++++ tests/unsat/v3l90003.cvc.smt2 | 34 +++++++++++++++++++++++++++++ 6 files changed, 153 insertions(+), 22 deletions(-) delete mode 100644 tests/logitest.sexp create mode 100644 tests/sat/v1l40032.cvc.smt2 create mode 100644 tests/unsat/t_cstor1.smt2.tmp create mode 100644 tests/unsat/typed_v3l30091.cvc.smt2 create mode 100644 tests/unsat/v3l60049.cvc.smt2 create mode 100644 tests/unsat/v3l90003.cvc.smt2 diff --git a/tests/logitest.sexp b/tests/logitest.sexp deleted file mode 100644 index 22a421f9..00000000 --- a/tests/logitest.sexp +++ /dev/null @@ -1,22 +0,0 @@ - -(prover - (name sidekick-dev) - (cmd "${cur_dir}/../sidekick --no-check --time $timeout $file") - (unsat "Unsat") - (sat "Sat") - (unknown "Timeout|Unknown") - (version "git:.")) - -(dir - (path $cur_dir) - (pattern ".*.(smt2|cnf)") - (expect (try (run smtlib-read-status) (run z3)))) - -(task - (name sidekick-local-test) - (action - (run_provers - (provers sidekick-dev) - (timeout 10) - (dirs)))) - diff --git a/tests/sat/v1l40032.cvc.smt2 b/tests/sat/v1l40032.cvc.smt2 new file mode 100644 index 00000000..8cec8d85 --- /dev/null +++ b/tests/sat/v1l40032.cvc.smt2 @@ -0,0 +1,28 @@ +(set-info :smt-lib-version 2.6) +(set-logic QF_DT) +(set-info :source | +Generated by: Andrew Reynolds +Generated on: 2017-04-28 +Generator: Random, converted to v2.6 by CVC4 +Application: Regressions for datatypes decision procedure. +Target solver: CVC3 +Publications: "An Abstract Decision Procedure for Satisfiability in the Theory of Inductive Data Types" by Clark Barrett, Igor Shikanian, and Cesare Tinelli, Journal on Satisfiability, Boolean Modeling and Computation 2007. +|) +(set-info :license "https://creativecommons.org/licenses/by/4.0/") +(set-info :category "random") +(set-info :status sat) + + +(declare-datatypes ((nat 0)(list 0)(tree 0)) (((succ (pred nat)) (zero)) +((cons (car tree) (cdr list)) (null)) +((node (children list)) (leaf (data nat))) +)) +(declare-fun x1 () nat) +(declare-fun x2 () list) +(declare-fun x3 () tree) + +(assert (and (and (and ((_ is zero) (pred (succ (data (node x2))))) (not (= (node (children x3)) x3))) ((_ is cons) (cdr (cons (leaf (succ (succ (pred (succ (data (car null))))))) (children (car null)))))) ((_ is zero) zero))) +(check-sat) +(exit) + + diff --git a/tests/unsat/t_cstor1.smt2.tmp b/tests/unsat/t_cstor1.smt2.tmp new file mode 100644 index 00000000..8feb2b79 --- /dev/null +++ b/tests/unsat/t_cstor1.smt2.tmp @@ -0,0 +1,23 @@ + +; test for constructors +; :status unsat + +(declare-sort nat 0) +(declare-cstor zero () nat) +(declare-cstor succ (nat) nat) + +(declare-fun n0 () nat) +(declare-fun n1 () nat) +(declare-fun n2 () nat) + +(assert (= n0 (succ (succ (succ (succ zero)))))) +(assert (= n1 (succ (succ n2)))) +(assert (not (= n1 (succ (succ (succ (succ zero))))))) + +; (check-sat) ; sat + +(assert (= n2 (succ (succ zero)))) + +(check-sat) ; unsat + +(exit) diff --git a/tests/unsat/typed_v3l30091.cvc.smt2 b/tests/unsat/typed_v3l30091.cvc.smt2 new file mode 100644 index 00000000..e558b837 --- /dev/null +++ b/tests/unsat/typed_v3l30091.cvc.smt2 @@ -0,0 +1,34 @@ +(set-info :smt-lib-version 2.6) +(set-logic QF_DT) +(set-info :source | +Generated by: Andrew Reynolds +Generated on: 2017-04-28 +Generator: Random, converted to v2.6 by CVC4 +Application: Regressions for datatypes decision procedure. +Target solver: CVC3 +Publications: "An Abstract Decision Procedure for Satisfiability in the Theory of Inductive Data Types" by Clark Barrett, Igor Shikanian, and Cesare Tinelli, Journal on Satisfiability, Boolean Modeling and Computation 2007. +|) +(set-info :license "https://creativecommons.org/licenses/by/4.0/") +(set-info :category "random") +(set-info :status unsat) + + +(declare-datatypes ((nat 0)(list 0)(tree 0)) (((succ (pred nat)) (zero)) +((cons (car tree) (cdr list)) (null)) +((node (children list)) (leaf (data nat))) +)) +(declare-fun x1 () nat) +(declare-fun x2 () nat) +(declare-fun x3 () nat) +(declare-fun x4 () list) +(declare-fun x5 () list) +(declare-fun x6 () list) +(declare-fun x7 () tree) +(declare-fun x8 () tree) +(declare-fun x9 () tree) + +(assert (and (and ((_ is null) x4) (not ((_ is zero) zero))) (not (= x3 x1)))) +(check-sat) +(exit) + + diff --git a/tests/unsat/v3l60049.cvc.smt2 b/tests/unsat/v3l60049.cvc.smt2 new file mode 100644 index 00000000..b459b190 --- /dev/null +++ b/tests/unsat/v3l60049.cvc.smt2 @@ -0,0 +1,34 @@ +(set-info :smt-lib-version 2.6) +(set-logic QF_DT) +(set-info :source | +Generated by: Andrew Reynolds +Generated on: 2017-04-28 +Generator: Random, converted to v2.6 by CVC4 +Application: Regressions for datatypes decision procedure. +Target solver: CVC3 +Publications: "An Abstract Decision Procedure for Satisfiability in the Theory of Inductive Data Types" by Clark Barrett, Igor Shikanian, and Cesare Tinelli, Journal on Satisfiability, Boolean Modeling and Computation 2007. +|) +(set-info :license "https://creativecommons.org/licenses/by/4.0/") +(set-info :category "random") +(set-info :status unsat) + + +(declare-datatypes ((nat 0)(list 0)(tree 0)) (((succ (pred nat)) (zero)) +((cons (car tree) (cdr list)) (null)) +((node (children list)) (leaf (data nat))) +)) +(declare-fun x1 () nat) +(declare-fun x2 () nat) +(declare-fun x3 () nat) +(declare-fun x4 () list) +(declare-fun x5 () list) +(declare-fun x6 () list) +(declare-fun x7 () tree) +(declare-fun x8 () tree) +(declare-fun x9 () tree) + +(assert (and (and (and (and (and (not ((_ is leaf) x7)) ((_ is zero) x3)) (not ((_ is cons) x6))) (not ((_ is succ) zero))) (not (= x6 x5))) (not ((_ is cons) x5)))) +(check-sat) +(exit) + + diff --git a/tests/unsat/v3l90003.cvc.smt2 b/tests/unsat/v3l90003.cvc.smt2 new file mode 100644 index 00000000..9bbbc730 --- /dev/null +++ b/tests/unsat/v3l90003.cvc.smt2 @@ -0,0 +1,34 @@ +(set-info :smt-lib-version 2.6) +(set-logic QF_DT) +(set-info :source | +Generated by: Andrew Reynolds +Generated on: 2017-04-28 +Generator: Random, converted to v2.6 by CVC4 +Application: Regressions for datatypes decision procedure. +Target solver: CVC3 +Publications: "An Abstract Decision Procedure for Satisfiability in the Theory of Inductive Data Types" by Clark Barrett, Igor Shikanian, and Cesare Tinelli, Journal on Satisfiability, Boolean Modeling and Computation 2007. +|) +(set-info :license "https://creativecommons.org/licenses/by/4.0/") +(set-info :category "random") +(set-info :status unsat) + + +(declare-datatypes ((nat 0)(list 0)(tree 0)) (((succ (pred nat)) (zero)) +((cons (car tree) (cdr list)) (null)) +((node (children list)) (leaf (data nat))) +)) +(declare-fun x1 () nat) +(declare-fun x2 () nat) +(declare-fun x3 () nat) +(declare-fun x4 () list) +(declare-fun x5 () list) +(declare-fun x6 () list) +(declare-fun x7 () tree) +(declare-fun x8 () tree) +(declare-fun x9 () tree) + +(assert (and (and (and (and (and (and (and (and (= x4 null) (not (= x5 (children x7)))) (not ((_ is leaf) (car null)))) (not ((_ is node) x8))) (= (data (leaf zero)) x3)) (not (= x9 x7))) (not (= (pred x2) (data x9)))) ((_ is null) (cdr x6))) (= (car null) (leaf (succ x1))))) +(check-sat) +(exit) + + From 8749cfff0a2f47ee30a2cad26c7dbe27ea1fdc1f Mon Sep 17 00:00:00 2001 From: Simon Cruanes Date: Sat, 28 Dec 2019 08:49:04 -0600 Subject: [PATCH 22/29] test: add reg test --- tests/sat/typed_v5l90027.cvc.smt2 | 40 +++++++++++++++++++++++++++++++ 1 file changed, 40 insertions(+) create mode 100644 tests/sat/typed_v5l90027.cvc.smt2 diff --git a/tests/sat/typed_v5l90027.cvc.smt2 b/tests/sat/typed_v5l90027.cvc.smt2 new file mode 100644 index 00000000..870e6e3d --- /dev/null +++ b/tests/sat/typed_v5l90027.cvc.smt2 @@ -0,0 +1,40 @@ +(set-info :smt-lib-version 2.6) +(set-logic QF_DT) +(set-info :source | +Generated by: Andrew Reynolds +Generated on: 2017-04-28 +Generator: Random, converted to v2.6 by CVC4 +Application: Regressions for datatypes decision procedure. +Target solver: CVC3 +Publications: "An Abstract Decision Procedure for Satisfiability in the Theory of Inductive Data Types" by Clark Barrett, Igor Shikanian, and Cesare Tinelli, Journal on Satisfiability, Boolean Modeling and Computation 2007. +|) +(set-info :license "https://creativecommons.org/licenses/by/4.0/") +(set-info :category "random") +(set-info :status sat) + + +(declare-datatypes ((nat 0)(list 0)(tree 0)) (((succ (pred nat)) (zero)) +((cons (car tree) (cdr list)) (null)) +((node (children list)) (leaf (data nat))) +)) +(declare-fun x1 () nat) +(declare-fun x2 () nat) +(declare-fun x3 () nat) +(declare-fun x4 () nat) +(declare-fun x5 () nat) +(declare-fun x6 () list) +(declare-fun x7 () list) +(declare-fun x8 () list) +(declare-fun x9 () list) +(declare-fun x10 () list) +(declare-fun x11 () tree) +(declare-fun x12 () tree) +(declare-fun x13 () tree) +(declare-fun x14 () tree) +(declare-fun x15 () tree) + +(assert (and (and (and (and (and (and (and (and (not ((_ is null) (ite ((_ is node) x14) (children x14) null))) (not (= (ite ((_ is cons) (ite ((_ is node) x14) (children x14) null)) (car (ite ((_ is node) x14) (children x14) null)) (leaf zero)) x13))) (not (= (ite ((_ is node) x14) (children x14) null) (ite ((_ is cons) (ite ((_ is node) x15) (children x15) null)) (cdr (ite ((_ is node) x15) (children x15) null)) null)))) ((_ is zero) x2)) (not ((_ is node) x11))) ((_ is leaf) x12)) (= x6 (ite ((_ is cons) x9) (cdr x9) null))) (not ((_ is zero) x3))) (= x15 x12))) +(check-sat) +(exit) + + From e58b29da02cd2ed769c3ff808afe24ccda340796 Mon Sep 17 00:00:00 2001 From: Simon Cruanes Date: Sat, 28 Dec 2019 08:49:14 -0600 Subject: [PATCH 23/29] fix(term): hashconsing error leading to non termination --- src/base-term/Base_types.ml | 2 ++ src/msat-solver/Sidekick_msat_solver.ml | 1 + src/smtlib/Process.ml | 2 +- 3 files changed, 4 insertions(+), 1 deletion(-) diff --git a/src/base-term/Base_types.ml b/src/base-term/Base_types.ml index c139a3db..2e745b5b 100644 --- a/src/base-term/Base_types.ml +++ b/src/base-term/Base_types.ml @@ -549,6 +549,8 @@ end = struct Fun.equal f1 f2 && IArray.equal sub_eq a1 a2 | Eq(a1,b1), Eq(a2,b2) -> sub_eq a1 a2 && sub_eq b1 b2 | Not a, Not b -> sub_eq a b + | Ite (a1,b1,c1), Ite (a2,b2,c2) -> + sub_eq a1 a2 && sub_eq b1 b2 && sub_eq c1 c2 | (Bool _ | App_fun _ | Eq _ | Not _ | Ite _), _ -> false diff --git a/src/msat-solver/Sidekick_msat_solver.ml b/src/msat-solver/Sidekick_msat_solver.ml index fc3de178..ce2fdc6f 100644 --- a/src/msat-solver/Sidekick_msat_solver.ml +++ b/src/msat-solver/Sidekick_msat_solver.ml @@ -558,6 +558,7 @@ module Make(A : ARG) let add_clause (self:t) (c:Atom.t IArray.t) : unit = Stat.incr self.count_clause; + Log.debugf 50 (fun k->k "add clause %a@." (Util.pp_iarray Atom.pp) c); Sat_solver.add_clause_a self.solver (c:> Atom.t array) P.default let add_clause_l self c = add_clause self (IArray.of_list c) diff --git a/src/smtlib/Process.ml b/src/smtlib/Process.ml index 00899d0b..8765976f 100644 --- a/src/smtlib/Process.ml +++ b/src/smtlib/Process.ml @@ -200,7 +200,7 @@ let process_stmt (solver:Solver.t) (stmt:Statement.t) : unit or_error = Log.debugf 5 - (fun k->k "(@[<2>process statement@ %a@])" Statement.pp stmt); + (fun k->k "(@[smtlib.process-statement@ %a@])" Statement.pp stmt); let decl_sort c n : unit = Log.debugf 1 (fun k->k "(@[declare-sort %a@ :arity %d@])" ID.pp c n); (* TODO: more? *) From 10b9febe9dbc67cb5b8cd0b98a948dfb1d8b5098 Mon Sep 17 00:00:00 2001 From: Simon Cruanes Date: Sat, 28 Dec 2019 09:00:59 -0600 Subject: [PATCH 24/29] fix(th-data): avoid redundant explanations --- src/th-data/Sidekick_th_data.ml | 1 - 1 file changed, 1 deletion(-) diff --git a/src/th-data/Sidekick_th_data.ml b/src/th-data/Sidekick_th_data.ml index 900d1bef..d92a6d44 100644 --- a/src/th-data/Sidekick_th_data.ml +++ b/src/th-data/Sidekick_th_data.ml @@ -170,7 +170,6 @@ module Make(A : ARG) : S with module A = A = struct Expl.mk_list [ Expl.mk_merge n1 c1.c_n; Expl.mk_merge n2 c2.c_n; - Expl.mk_merge n1 n2; ] in if A.Cstor.equal c1.c_cstor c2.c_cstor then ( From dbf88279a10ba391fc8784e4a699d8814e37416c Mon Sep 17 00:00:00 2001 From: Simon Cruanes Date: Sat, 28 Dec 2019 09:19:17 -0600 Subject: [PATCH 25/29] test: more reg tests --- tests/benchpress.sexp | 2 +- tests/unsat/typed_v3l40070.cvc.smt2 | 34 ++++++++++++++++++++++++ tests/unsat/typed_v5l90068.cvc.smt2 | 40 +++++++++++++++++++++++++++++ 3 files changed, 75 insertions(+), 1 deletion(-) create mode 100644 tests/unsat/typed_v3l40070.cvc.smt2 create mode 100644 tests/unsat/typed_v5l90068.cvc.smt2 diff --git a/tests/benchpress.sexp b/tests/benchpress.sexp index 9a347b4f..67b891aa 100644 --- a/tests/benchpress.sexp +++ b/tests/benchpress.sexp @@ -9,7 +9,7 @@ (dir (path $cur_dir) - (pattern ".*.(smt2|cnf)") + (pattern ".*.(smt2|cnf)$") (expect (try (run smtlib-read-status) (run z3)))) (task diff --git a/tests/unsat/typed_v3l40070.cvc.smt2 b/tests/unsat/typed_v3l40070.cvc.smt2 new file mode 100644 index 00000000..76f8e35e --- /dev/null +++ b/tests/unsat/typed_v3l40070.cvc.smt2 @@ -0,0 +1,34 @@ +(set-info :smt-lib-version 2.6) +(set-logic QF_DT) +(set-info :source | +Generated by: Andrew Reynolds +Generated on: 2017-04-28 +Generator: Random, converted to v2.6 by CVC4 +Application: Regressions for datatypes decision procedure. +Target solver: CVC3 +Publications: "An Abstract Decision Procedure for Satisfiability in the Theory of Inductive Data Types" by Clark Barrett, Igor Shikanian, and Cesare Tinelli, Journal on Satisfiability, Boolean Modeling and Computation 2007. +|) +(set-info :license "https://creativecommons.org/licenses/by/4.0/") +(set-info :category "random") +(set-info :status unsat) + + +(declare-datatypes ((nat 0)(list 0)(tree 0)) (((succ (pred nat)) (zero)) +((cons (car tree) (cdr list)) (null)) +((node (children list)) (leaf (data nat))) +)) +(declare-fun x1 () nat) +(declare-fun x2 () nat) +(declare-fun x3 () nat) +(declare-fun x4 () list) +(declare-fun x5 () list) +(declare-fun x6 () list) +(declare-fun x7 () tree) +(declare-fun x8 () tree) +(declare-fun x9 () tree) + +(assert (and (and (and (not (= zero (ite ((_ is leaf) (node x4)) (data (node x4)) zero))) ((_ is node) x7)) (= x9 x8)) (not (= (ite ((_ is cons) (ite ((_ is cons) x4) (cdr x4) null)) (cdr (ite ((_ is cons) x4) (cdr x4) null)) null) null)))) +(check-sat) +(exit) + + diff --git a/tests/unsat/typed_v5l90068.cvc.smt2 b/tests/unsat/typed_v5l90068.cvc.smt2 new file mode 100644 index 00000000..4157b5f6 --- /dev/null +++ b/tests/unsat/typed_v5l90068.cvc.smt2 @@ -0,0 +1,40 @@ +(set-info :smt-lib-version 2.6) +(set-logic QF_DT) +(set-info :source | +Generated by: Andrew Reynolds +Generated on: 2017-04-28 +Generator: Random, converted to v2.6 by CVC4 +Application: Regressions for datatypes decision procedure. +Target solver: CVC3 +Publications: "An Abstract Decision Procedure for Satisfiability in the Theory of Inductive Data Types" by Clark Barrett, Igor Shikanian, and Cesare Tinelli, Journal on Satisfiability, Boolean Modeling and Computation 2007. +|) +(set-info :license "https://creativecommons.org/licenses/by/4.0/") +(set-info :category "random") +(set-info :status unsat) + + +(declare-datatypes ((nat 0)(list 0)(tree 0)) (((succ (pred nat)) (zero)) +((cons (car tree) (cdr list)) (null)) +((node (children list)) (leaf (data nat))) +)) +(declare-fun x1 () nat) +(declare-fun x2 () nat) +(declare-fun x3 () nat) +(declare-fun x4 () nat) +(declare-fun x5 () nat) +(declare-fun x6 () list) +(declare-fun x7 () list) +(declare-fun x8 () list) +(declare-fun x9 () list) +(declare-fun x10 () list) +(declare-fun x11 () tree) +(declare-fun x12 () tree) +(declare-fun x13 () tree) +(declare-fun x14 () tree) +(declare-fun x15 () tree) + +(assert (and (and (and (and (and (and (and (and ((_ is node) x13) (not ((_ is succ) x1))) (= zero (succ x5))) ((_ is null) x8)) ((_ is zero) x1)) (= x11 x15)) (not (= x10 x9))) (not (= (leaf x2) x13))) (= x15 (leaf x5)))) +(check-sat) +(exit) + + From 17a09f2cbc7411f38269871e9cdac1569a4b3314 Mon Sep 17 00:00:00 2001 From: Simon Cruanes Date: Tue, 14 Jan 2020 20:23:14 -0600 Subject: [PATCH 26/29] test: add some regression tests --- tests/unsat/diamond2_cong_if.smt2 | 22 ++++++++++++++++++++++ tests/unsat/if_ff_fg.smt2 | 14 ++++++++++++++ tests/unsat/nested_if.smt2 | 17 +++++++++++++++++ tests/unsat/smtlib.626179.smt2 | 14 ++++++++++++++ tests/unsat/t_subform.smt2 | 12 ++++++++++++ tests/unsat/test_ite_1.smt2 | 8 ++++++++ 6 files changed, 87 insertions(+) create mode 100644 tests/unsat/diamond2_cong_if.smt2 create mode 100644 tests/unsat/if_ff_fg.smt2 create mode 100644 tests/unsat/nested_if.smt2 create mode 100644 tests/unsat/smtlib.626179.smt2 create mode 100644 tests/unsat/t_subform.smt2 create mode 100644 tests/unsat/test_ite_1.smt2 diff --git a/tests/unsat/diamond2_cong_if.smt2 b/tests/unsat/diamond2_cong_if.smt2 new file mode 100644 index 00000000..f5149fd1 --- /dev/null +++ b/tests/unsat/diamond2_cong_if.smt2 @@ -0,0 +1,22 @@ + +; see diamond2_cong, but using "if" +; diamond based on congruence, not just transitivity +(declare-sort a 0) +(declare-fun x0 () a) +(declare-fun y0 () a) +(declare-fun z0 () a) +(declare-fun p0 () Bool) +(declare-fun x1 () a) +(declare-fun y1 () a) +(declare-fun z1 () a) +(declare-fun p1 () Bool) +(declare-fun x2 () a) +(declare-fun f (a) a) +(assert (not (= x2 (f (f x0))))) +(assert (= x1 (f y0))) +(assert (= x1 (f z0))) +(assert (= x0 (ite p0 y0 z0))) +(assert (= x2 (f y1))) +(assert (= x2 (f z1))) +(assert (= x1 (ite p1 y1 z1))) +(check-sat) diff --git a/tests/unsat/if_ff_fg.smt2 b/tests/unsat/if_ff_fg.smt2 new file mode 100644 index 00000000..6cc85d1c --- /dev/null +++ b/tests/unsat/if_ff_fg.smt2 @@ -0,0 +1,14 @@ + +; if + congruence +(declare-sort u 0) +(declare-fun p0 () Bool) +(declare-fun a () u) +(declare-fun b1 () u) +(declare-fun b2 () u) +(declare-fun c () u) +(declare-fun f (u) u) +(assert (= a (ite p0 b1 b2))) +(assert (= (f b1) c)) +(assert (= (f b2) c)) +(assert (not (= (f a) c))) +(check-sat) diff --git a/tests/unsat/nested_if.smt2 b/tests/unsat/nested_if.smt2 new file mode 100644 index 00000000..299d9cd7 --- /dev/null +++ b/tests/unsat/nested_if.smt2 @@ -0,0 +1,17 @@ + +; nested ifs +(declare-sort u 0) +(declare-fun a () u) +(declare-fun b () u) +(declare-fun c () u) +(declare-fun d () u) +(declare-fun q0 () Bool) +(declare-fun q1 () Bool) +(declare-fun q2 () Bool) +(declare-fun p (u) Bool) +(assert (p a)) +(assert (p b)) +(assert (p c)) +(assert (p d)) +(assert (not (p (ite q0 (ite q1 a b) (ite q2 c d))))) +(check-sat) diff --git a/tests/unsat/smtlib.626179.smt2 b/tests/unsat/smtlib.626179.smt2 new file mode 100644 index 00000000..95e130c4 --- /dev/null +++ b/tests/unsat/smtlib.626179.smt2 @@ -0,0 +1,14 @@ +(set-info :smt-lib-version 2.6) +(set-logic QF_UFLRA) +(set-info :source |Benchmarks from the paper: "Extending Sledgehammer with SMT Solvers" by Jasmin Blanchette, Sascha Bohme, and Lawrence C. Paulson, CADE 2011. Translated to SMT2 by Andrew Reynolds and Morgan Deters.|) +(set-info :category "industrial") +(set-info :status unsat) +(declare-sort S1 0) +(declare-fun f1 () S1) +(declare-fun f2 () S1) +(declare-fun f3 () Real) +(declare-fun f4 () Real) +(assert (not (= f1 f2))) +(assert (not (=> (< f3 f4) (=> (< f4 (* 2.0 f3)) (< 0.0 (- f4 f3)))))) +(check-sat) +(exit) diff --git a/tests/unsat/t_subform.smt2 b/tests/unsat/t_subform.smt2 new file mode 100644 index 00000000..d21144ea --- /dev/null +++ b/tests/unsat/t_subform.smt2 @@ -0,0 +1,12 @@ + +(set-info :status "unsat") +(declare-fun p () Bool) +(declare-sort u 0) +(declare-fun f (Bool) u) +(declare-const a u) +(declare-const b u) +(assert (distinct a b)) + +(assert (= (f p) a)) +(assert (= (f (and p (or p p))) b)) +(check-sat) diff --git a/tests/unsat/test_ite_1.smt2 b/tests/unsat/test_ite_1.smt2 new file mode 100644 index 00000000..3decfd60 --- /dev/null +++ b/tests/unsat/test_ite_1.smt2 @@ -0,0 +1,8 @@ + +(declare-sort U 0) +(declare-fun a () U) +(declare-fun b () U) +(declare-fun cond () Bool) +(declare-fun p (U) Bool) +(assert (and (= a b) (p a) (not (p (ite cond a b))))) +(check-sat) From b332e8ceb09e9ee154108bf532e3e281b6bb44d2 Mon Sep 17 00:00:00 2001 From: Simon Cruanes Date: Tue, 14 Jan 2020 20:23:23 -0600 Subject: [PATCH 27/29] fix: preprocess away "ite" --- src/core/Sidekick_core.ml | 3 +-- src/smtlib/Form.ml | 12 ++++-------- src/smtlib/Typecheck.ml | 2 +- src/th-bool-static/Sidekick_th_bool_static.ml | 18 +++++++++++++++--- 4 files changed, 21 insertions(+), 14 deletions(-) diff --git a/src/core/Sidekick_core.ml b/src/core/Sidekick_core.ml index 165f025f..af28909e 100644 --- a/src/core/Sidekick_core.ml +++ b/src/core/Sidekick_core.ml @@ -366,8 +366,7 @@ module type SOLVER_INTERNAL = sig (** Reset internal cache, etc. *) type hook = t -> term -> term option - (** Given a term, try to simplify it. Return [None] if it didn't change. - Can also add clauses to the simplifier. *) + (** Given a term, try to simplify it. Return [None] if it didn't change. *) val normalize : t -> term -> term (** Normalize a term using all the hooks. *) diff --git a/src/smtlib/Form.ml b/src/smtlib/Form.ml index e819171d..417fd943 100644 --- a/src/smtlib/Form.ml +++ b/src/smtlib/Form.ml @@ -7,7 +7,6 @@ exception Not_a_th_term let id_and = ID.make "and" let id_or = ID.make "or" let id_imply = ID.make "=>" -let id_ite = ID.make "ite" let view_id fid args = if ID.equal fid id_and then ( @@ -18,8 +17,6 @@ let view_id fid args = (* conclusion is stored first *) let len = IArray.length args in B_imply (IArray.sub args 1 (len-1), IArray.get args 0) - ) else if ID.equal fid id_ite && IArray.length args = 3 then ( - B_ite (IArray.get args 0, IArray.get args 1, IArray.get args 2) ) else ( raise_notrace Not_a_th_term ) @@ -29,14 +26,13 @@ let view_as_bool (t:T.t) : T.t bool_view = | Bool b -> B_bool b | Not u -> B_not u | Eq (a, b) when Ty.is_bool (T.ty a) -> B_equiv (a,b) + | Ite (a,b,c) -> B_ite(a,b,c) | App_fun ({fun_id; _}, args) -> (try view_id fun_id args with Not_a_th_term -> B_atom t) | _ -> B_atom t module Funs = struct - let get_ty id args = - if ID.equal id id_ite then T.ty (IArray.get args 1) - else Ty.bool + let get_ty _ _ = Ty.bool let abs ~self _a = match T.view self with @@ -76,7 +72,7 @@ module Funs = struct let and_ = mk_fun id_and let or_ = mk_fun id_or let imply = mk_fun id_imply - let ite = mk_fun id_ite + let ite = Term.ite end let as_id id (t:T.t) : T.t IArray.t option = @@ -117,7 +113,7 @@ let not_ = T.not_ let ite st a b c = match T.view a with | T.Bool ba -> if ba then b else c - | _ -> T.app_fun st Funs.ite (IArray.of_array_unsafe [| a;b;c |]) + | _ -> T.ite st a b c let equiv st a b = if T.equal a b then T.true_ st diff --git a/src/smtlib/Typecheck.ml b/src/smtlib/Typecheck.ml index e5a565fc..4bc8b228 100644 --- a/src/smtlib/Typecheck.ml +++ b/src/smtlib/Typecheck.ml @@ -144,7 +144,7 @@ let rec conv_term (ctx:Ctx.t) (t:PA.term) : T.t = let a = conv_term ctx a in let b = conv_term ctx b in let c = conv_term ctx c in - T.ite tst a b c + Form.ite tst a b c | PA.Fun _ | PA.Forall _ | PA.Exists _ -> errorf_ctx ctx "cannot process lambda/quantifiers in %a" PA.pp_term t | PA.Let (vbs, body) -> diff --git a/src/th-bool-static/Sidekick_th_bool_static.ml b/src/th-bool-static/Sidekick_th_bool_static.ml index 8bff46fb..7f729e11 100644 --- a/src/th-bool-static/Sidekick_th_bool_static.ml +++ b/src/th-bool-static/Sidekick_th_bool_static.ml @@ -115,7 +115,8 @@ module Make(A : ARG) : S with module A = A = struct begin match A.view_as_bool a with | B_bool true -> Some b | B_bool false -> Some c - | _ -> None + | _ -> + None end | B_equiv (a,b) when is_true a -> Some b | B_equiv (a,b) when is_false a -> Some (not_ tst b) @@ -131,6 +132,17 @@ module Make(A : ARG) : S with module A = A = struct let t = fresh_term ~pre self Ty.bool in mk_lit t + (* preprocess "ite" away *) + let preproc_ite self _si ~mk_lit ~add_clause (t:T.t) : T.t option = + match A.view_as_bool t with + | B_ite (a,b,c) -> + let t_a = fresh_term self ~pre:"ite" (T.ty b) in + let lit_a = mk_lit a in + add_clause [Lit.neg lit_a; mk_lit (eq self.tst t_a b)]; + add_clause [lit_a; mk_lit (eq self.tst t_a c)]; + Some t_a + | _ -> None + (* TODO: polarity? *) let cnf (self:state) (_si:SI.t) ~mk_lit ~add_clause (t:T.t) : T.t option = let rec get_lit (t:T.t) : Lit.t = @@ -173,8 +185,7 @@ module Make(A : ARG) : S with module A = A = struct or_a self.tst @@ IArray.append (IArray.map (not_ self.tst) args) (IArray.singleton u) in get_lit t' - | B_ite _ | B_eq _ -> - mk_lit t + | B_ite _ | B_eq _ -> mk_lit t | B_equiv (a,b) -> let a = get_lit a in let b = get_lit b in @@ -225,6 +236,7 @@ module Make(A : ARG) : S with module A = A = struct Log.debug 2 "(th-bool.setup)"; let st = create (SI.tst si) in SI.add_simplifier si (simplify st); + SI.add_preprocess si (preproc_ite st); SI.add_preprocess si (cnf st); if A.check_congruence_classes then ( Log.debug 5 "(th-bool.add-final-check)"; From ef60d1466fdce8405810c80551c1e7a05fa36aea Mon Sep 17 00:00:00 2001 From: Simon Cruanes Date: Tue, 14 Jan 2020 21:23:02 -0600 Subject: [PATCH 28/29] feat: better debug message --- src/msat-solver/Sidekick_msat_solver.ml | 8 ++++++-- 1 file changed, 6 insertions(+), 2 deletions(-) diff --git a/src/msat-solver/Sidekick_msat_solver.ml b/src/msat-solver/Sidekick_msat_solver.ml index ce2fdc6f..be1a4be8 100644 --- a/src/msat-solver/Sidekick_msat_solver.ml +++ b/src/msat-solver/Sidekick_msat_solver.ml @@ -168,6 +168,7 @@ module Make(A : ARG) mutable th_states : th_states; (** Set of theories *) mutable on_partial_check: (t -> actions -> lit Iter.t -> unit) list; mutable on_final_check: (t -> actions -> lit Iter.t -> unit) list; + mutable level: int; } and preprocess_hook = @@ -289,18 +290,20 @@ module Make(A : ARG) | Ths_cons r -> r.pop_levels r.st n; pop_lvls_ n r.next let push_level (self:t) : unit = + self.level <- 1 + self.level; CC.push_level (cc self); push_lvl_ self.th_states let pop_levels (self:t) n : unit = + self.level <- self.level - n; CC.pop_levels (cc self) n; pop_lvls_ n self.th_states (* handle a literal assumed by the SAT solver *) let assert_lits_ ~final (self:t) (acts:actions) (lits:Lit.t Iter.t) : unit = Msat.Log.debugf 2 - (fun k->k "(@[@{msat-solver.assume_lits@}%s@ %a@])" - (if final then "[final]" else "") (Util.pp_seq ~sep:"; " Lit.pp) lits); + (fun k->k "(@[@{msat-solver.assume_lits@}%s[lvl=%d]@ %a@])" + (if final then "[final]" else "") self.level (Util.pp_seq ~sep:"; " Lit.pp) lits); (* transmit to CC *) let cc = cc self in if not final then ( @@ -369,6 +372,7 @@ module Make(A : ARG) count_conflict = Stat.mk_int stat "solver.th-conflicts"; on_partial_check=[]; on_final_check=[]; + level=0; } in ignore (Lazy.force @@ self.cc : CC.t); self From a31b2b36eff7fa238beb99496d25711df1b244ec Mon Sep 17 00:00:00 2001 From: Simon Cruanes Date: Tue, 14 Jan 2020 22:41:33 -0600 Subject: [PATCH 29/29] fixes: add missing expl in monoids; handle `is-c t` --- src/base-term/Base_types.ml | 7 ++++ src/cc/Sidekick_cc.ml | 10 +++-- src/core/Sidekick_core.ml | 33 +++++------------ src/smtlib/Process.ml | 2 +- src/th-cstor/Sidekick_th_cstor.ml | 3 +- src/th-data/Sidekick_th_data.ml | 61 +++++++++++++++++++++++-------- src/th-data/Sidekick_th_data.mli | 3 ++ 7 files changed, 74 insertions(+), 45 deletions(-) diff --git a/src/base-term/Base_types.ml b/src/base-term/Base_types.ml index 2e745b5b..e719aac5 100644 --- a/src/base-term/Base_types.ml +++ b/src/base-term/Base_types.ml @@ -402,6 +402,7 @@ module Fun : sig val as_undefined_exn : t -> t * Ty.Fun.t val is_undefined : t -> bool val select : select -> t + val select_idx : cstor -> int -> t val cstor : cstor -> t val is_a : cstor -> t @@ -452,6 +453,12 @@ end = struct let is_a c : t = make c.cstor_is_a (Fun_is_a c) let cstor c : t = make c.cstor_id (Fun_cstor c) let select sel : t = make sel.select_id (Fun_select sel) + let select_idx c i : t = + let lazy l = c.cstor_args in + match List.nth l i with + | sel -> select sel + | exception Not_found -> + Error.errorf "invalid selector %d for cstor %a" i ID.pp c.cstor_id let[@inline] do_cc (c:t) : bool = match view c with | Fun_cstor _ | Fun_select _ | Fun_undef _ | Fun_is_a _ -> true diff --git a/src/cc/Sidekick_cc.ml b/src/cc/Sidekick_cc.ml index eb05fb64..a64b2454 100644 --- a/src/cc/Sidekick_cc.ml +++ b/src/cc/Sidekick_cc.ml @@ -348,10 +348,12 @@ module Make (A: CC_ARG) Vec.push cc.pending t let merge_classes cc t u e : unit = - Log.debugf 50 - (fun k->k "(@[cc.push-combine@ %a ~@ %a@ :expl %a@])" - N.pp t N.pp u Expl.pp e); - Vec.push cc.combine @@ CT_merge (t,u,e) + if t != u && not (same_class t u) then ( + Log.debugf 50 + (fun k->k "(@[cc.push-combine@ %a ~@ %a@ :expl %a@])" + N.pp t N.pp u Expl.pp e); + Vec.push cc.combine @@ CT_merge (t,u,e) + ) (* re-root the explanation tree of the equivalence class of [n] so that it points to [n]. diff --git a/src/core/Sidekick_core.ml b/src/core/Sidekick_core.ml index af28909e..0f554612 100644 --- a/src/core/Sidekick_core.ml +++ b/src/core/Sidekick_core.ml @@ -685,7 +685,11 @@ module type MONOID_ARG = sig and [m_u] is the monoid value attached to [u]. *) - val merge : SI.CC.t -> SI.CC.N.t -> t -> SI.CC.N.t -> t -> (t, SI.CC.Expl.t) result + val merge : + SI.CC.t -> + SI.CC.N.t -> t -> SI.CC.N.t -> t -> + SI.CC.Expl.t -> + (t, SI.CC.Expl.t) result end (** Keep track of monoid state per equivalence class *) @@ -749,7 +753,7 @@ end = struct with Not_found -> Error.errorf "node %a has bitfield but no value" N.pp n_u in - match M.merge cc n_u m_u n_u m_u' with + match M.merge cc n_u m_u n_u m_u' (Expl.mk_list []) with | Error expl -> Error.errorf "when merging@ @[for node %a@],@ \ @@ -773,35 +777,18 @@ end = struct let iter_all (self:t) : _ Iter.t = N_tbl.to_iter self.values - (* find cell for [n] *) - let get_cell (self:t) (n:N.t) : M.t option = - N_tbl.get self.values n - (* TODO - if N.get_field self.field_has_value n then ( - try Some (N_tbl.find self.values n) - with Not_found -> - Error.errorf "repr %a has value-field bit for %s set, but is not in table" - N.pp n M.name - ) else ( - None - ) - *) - let on_pre_merge (self:t) cc acts n1 n2 e_n1_n2 : unit = - begin match get_cell self n1, get_cell self n2 with + begin match get self n1, get self n2 with | Some v1, Some v2 -> Log.debugf 5 (fun k->k - "(@[monoid[%s].on_pre_merge@ @[:n1 %a@ :val %a@]@ @[:n2 %a@ :val %a@]@])" + "(@[monoid[%s].on_pre_merge@ (@[:n1 %a@ :val1 %a@])@ (@[:n2 %a@ :val2 %a@])@])" M.name N.pp n1 M.pp v1 N.pp n2 M.pp v2); - begin match M.merge cc n1 v1 n2 v2 with + begin match M.merge cc n1 v1 n2 v2 e_n1_n2 with | Ok v' -> N_tbl.remove self.values n2; (* only keep repr *) N_tbl.add self.values n1 v'; - | Error expl -> - (* add [n1=n2] to the conflict *) - let expl = Expl.mk_list [ e_n1_n2; expl; ] in - SI.CC.raise_conflict_from_expl cc acts expl + | Error expl -> SI.CC.raise_conflict_from_expl cc acts expl end | None, Some cr -> SI.CC.set_bitfield cc self.field_has_value true n1; diff --git a/src/smtlib/Process.ml b/src/smtlib/Process.ml index 8765976f..1a8b9e18 100644 --- a/src/smtlib/Process.ml +++ b/src/smtlib/Process.ml @@ -66,7 +66,6 @@ module Check_cc = struct (fun k->k "(@[check-cc-prop.ok@ @[%a => %a@]@])" pp_and reason Lit.pp p); ) - let theory = Solver.mk_theory ~name:"cc-check" ~create_and_setup:(fun si -> @@ -282,6 +281,7 @@ module Th_data = Sidekick_th_data.Make(struct | _ -> T_other t let mk_cstor tst c args : Term.t = Term.app_fun tst (Fun.cstor c) args + let mk_sel tst c i u = Term.app_fun tst (Fun.select_idx c i) (IArray.singleton u) let mk_is_a tst c u : Term.t = if c.cstor_arity=0 then ( Term.eq tst u (Term.const tst (Fun.cstor c)) diff --git a/src/th-cstor/Sidekick_th_cstor.ml b/src/th-cstor/Sidekick_th_cstor.ml index 0c8f7a60..279d4ac9 100644 --- a/src/th-cstor/Sidekick_th_cstor.ml +++ b/src/th-cstor/Sidekick_th_cstor.ml @@ -45,13 +45,14 @@ module Make(A : ARG) : S with module A = A = struct | T_cstor (cstor,args) -> Some {n; t; cstor; args}, [] | _ -> None, [] - let merge cc n1 v1 n2 v2 : _ result = + let merge cc n1 v1 n2 v2 e_n1_n2 : _ result = Log.debugf 5 (fun k->k "(@[%s.merge@ @[:c1 %a (t %a)@]@ @[:c2 %a (t %a)@]@])" name N.pp n1 T.pp v1.t N.pp n2 T.pp v2.t); (* build full explanation of why the constructor terms are equal *) let expl = Expl.mk_list [ + e_n1_n2; Expl.mk_merge n1 v1.n; Expl.mk_merge n2 v2.n; ] diff --git a/src/th-data/Sidekick_th_data.ml b/src/th-data/Sidekick_th_data.ml index d92a6d44..e023ed6e 100644 --- a/src/th-data/Sidekick_th_data.ml +++ b/src/th-data/Sidekick_th_data.ml @@ -73,6 +73,7 @@ module type ARG = sig val view_as_data : S.T.Term.t -> (Cstor.t, S.T.Term.t) data_view val mk_cstor : S.T.Term.state -> Cstor.t -> S.T.Term.t IArray.t -> S.T.Term.t val mk_is_a: S.T.Term.state -> Cstor.t -> S.T.Term.t -> S.T.Term.t + val mk_sel : S.T.Term.state -> Cstor.t -> int -> S.T.Term.t -> S.T.Term.t val ty_is_finite : S.T.Ty.t -> bool val ty_set_is_finite : S.T.Ty.t -> bool -> unit end @@ -152,7 +153,7 @@ module Make(A : ARG) : S with module A = A = struct } let pp out (v:t) = - Fmt.fprintf out "(@[%s@ :cstor %a@])" name A.Cstor.pp v.c_cstor + Fmt.fprintf out "(@[%s@ :cstor %a@ :n %a@])" name A.Cstor.pp v.c_cstor N.pp v.c_n (* attach data to constructor terms *) let of_term n (t:T.t) : _ option * _ list = @@ -161,13 +162,15 @@ module Make(A : ARG) : S with module A = A = struct Some {c_n=n;c_cstor=cstor; c_args=args}, [] | _ -> None, [] - let merge cc n1 c1 n2 c2 : _ result = + let merge cc n1 c1 n2 c2 e_n1_n2 : _ result = Log.debugf 5 - (fun k->k "(@[%s.merge@ @[:c1 %a %a@]@ @[:c2 %a %a@]@])" + (fun k->k "(@[%s.merge@ (@[:c1 %a %a@])@ (@[:c2 %a %a@])@])" name N.pp n1 pp c1 N.pp n2 pp c2); (* build full explanation of why the constructor terms are equal *) + (* TODO: have a sort of lemma (injectivity) here to justify this in the proof *) let expl = Expl.mk_list [ + e_n1_n2; Expl.mk_merge n1 c1.c_n; Expl.mk_merge n2 c2.c_n; ] @@ -195,11 +198,13 @@ module Make(A : ARG) : S with module A = A = struct sel_n: N.t; sel_cstor: A.Cstor.t; sel_idx: int; + sel_arg: T.t; } type is_a = { is_a_n: N.t; is_a_cstor: A.Cstor.t; + is_a_arg: T.t; } (* associate to each class a unique constructor term in the class (if any) *) @@ -222,19 +227,19 @@ module Make(A : ARG) : S with module A = A = struct match A.view_as_data t with | T_select (c, i, u) -> let m_sel = { - parent_select=[{sel_n=n; sel_idx=i; sel_cstor=c}]; + parent_select=[{sel_n=n; sel_idx=i; sel_cstor=c; sel_arg=u}]; parent_is_a=[]; } in None, [u, m_sel] | T_is_a (c, u) -> let m_sel = { - parent_is_a=[{is_a_n=n; is_a_cstor=c}]; + parent_is_a=[{is_a_n=n; is_a_cstor=c; is_a_arg=u;}]; parent_select=[]; } in None, [u, m_sel] | T_cstor _ | T_other _ -> None, [] - let merge cc n1 v1 n2 v2 : _ result = + let merge cc n1 v1 n2 v2 _e : _ result = Log.debugf 5 (fun k->k "(@[%s.merge@ @[:c1 %a %a@]@ @[:c2 %a %a@]@])" name N.pp n1 pp v1 N.pp n2 pp v2); @@ -324,8 +329,8 @@ module Make(A : ARG) : S with module A = A = struct | Some cstor -> let is_true = A.Cstor.equal cstor.c_cstor c_t in Log.debugf 5 - (fun k->k "(@[%s.on-new-term.is-a.reduce@ :to %B@ :n %a@ :sub-cstor %a@])" - name is_true N.pp n Monoid_cstor.pp cstor); + (fun k->k "(@[%s.on-new-term.is-a.reduce@ :t %a@ :to %B@ :n %a@ :sub-cstor %a@])" + name T.pp t is_true N.pp n Monoid_cstor.pp cstor); SI.CC.merge cc n (SI.CC.n_bool cc is_true) (Expl.mk_merge n_u repr_u) end | T_select (c_t, i, u) -> @@ -351,27 +356,27 @@ module Make(A : ARG) : S with module A = A = struct | Ty_data {cstors} -> cstors | _ -> assert false - (* FIXME: when merging [(is _ C) t] with true, propagate [t=C(sel[1]-c(t),…)] *) - (* FIXME: when merging [(is _ C) t] with false, remove [C] from the available list *) let on_pre_merge (self:t) (cc:SI.CC.t) acts n1 n2 expl : unit = let merge_is_a n1 (c1:Monoid_cstor.t) n2 (is_a2:Monoid_parents.is_a) = let is_true = A.Cstor.equal c1.c_cstor is_a2.is_a_cstor in Log.debugf 50 - (fun k->k "(@[%s.on-merge.is-a.reduce@ :to %B@ :n %a@ :sub-cstor %a@])" - name is_true N.pp n2 Monoid_cstor.pp c1); + (fun k->k "(@[%s.on-merge.is-a.reduce@ %a@ :to %B@ :n1 %a@ :n2 %a@ :sub-cstor %a@])" + name Monoid_parents.pp_is_a is_a2 is_true N.pp n1 N.pp n2 Monoid_cstor.pp c1); SI.CC.merge cc is_a2.is_a_n (SI.CC.n_bool cc is_true) - Expl.(mk_list [mk_merge n1 c1.c_n; mk_merge n1 n2]) + Expl.(mk_list [mk_merge n1 c1.c_n; mk_merge n1 n2; + mk_merge_t (N.term n2) is_a2.is_a_arg]) in let merge_select n1 (c1:Monoid_cstor.t) n2 (sel2:Monoid_parents.select) = if A.Cstor.equal c1.c_cstor sel2.sel_cstor then ( Log.debugf 5 - (fun k->k "(@[%s.on-merge.select.reduce@ :n %a@ :sel get[%d]-%a@])" + (fun k->k "(@[%s.on-merge.select.reduce@ :n2 %a@ :sel get[%d]-%a@])" name N.pp n2 sel2.sel_idx Monoid_cstor.pp c1); assert (sel2.sel_idx < IArray.length c1.c_args); let u_i = IArray.get c1.c_args sel2.sel_idx in let n_u_i = SI.CC.add_term cc u_i in SI.CC.merge cc sel2.sel_n n_u_i - Expl.(mk_list [mk_merge n1 c1.c_n; mk_merge n1 n2]); + Expl.(mk_list [mk_merge n1 c1.c_n; mk_merge n1 n2; + mk_merge_t (N.term n2) sel2.sel_arg]); ) in let merge_c_p n1 n2 = @@ -380,7 +385,7 @@ module Make(A : ARG) : S with module A = A = struct | _, None -> () | Some c1, Some p2 -> Log.debugf 50 - (fun k->k "(@[%s.pre-merge@ @[:n1 %a@ :c1 %a@]@ @[:n2 %a@ :p2 %a@]@])" + (fun k->k "(@[%s.pre-merge@ (@[:n1 %a@ :c1 %a@])@ (@[:n2 %a@ :p2 %a@])@])" name N.pp n1 Monoid_cstor.pp c1 N.pp n2 Monoid_parents.pp p2); List.iter (fun is_a2 -> merge_is_a n1 c1 n2 is_a2) p2.parent_is_a; List.iter (fun s2 -> merge_select n1 c1 n2 s2) p2.parent_select; @@ -472,6 +477,29 @@ module Make(A : ARG) : S with module A = A = struct end end + (* FIXME: when merging [(is _ C) t] with false, remove [C] from the available list *) + let on_partial_check (self:t) (solver:SI.t) (acts:SI.actions) trail = + let check_lit lit = + let t = SI.Lit.term lit in + match A.view_as_data t with + | T_is_a (c, u) when SI.Lit.sign lit -> + (* add [((_ is C) u) ==> u = C(sel-c-0 u, …, sel-c-k u)] *) + let rhs = + let args = + A.Cstor.ty_args c + |> Iter.mapi (fun i _ty -> A.mk_sel self.tst c i u) + |> Iter.to_list |> IArray.of_list + in + A.mk_cstor self.tst c args + in + Log.debugf 50 + (fun k->k"(@[%s.assign-is-a@ :lhs %a@ :rhs %a@ :lit %a@])" + name T.pp u T.pp rhs SI.Lit.pp lit); + SI.cc_merge_t solver acts u rhs (Expl.mk_lit lit) + | _ -> () + in + Iter.iter check_lit trail + (* on final check, check acyclicity, then make sure we have done case split on all terms that need it. *) @@ -530,6 +558,7 @@ module Make(A : ARG) : S with module A = A = struct Log.debugf 1 (fun k->k "(setup :%s)" name); SI.on_cc_new_term solver (on_new_term self); SI.on_cc_pre_merge solver (on_pre_merge self); + SI.on_partial_check solver (on_partial_check self); SI.on_final_check solver (on_final_check self); self diff --git a/src/th-data/Sidekick_th_data.mli b/src/th-data/Sidekick_th_data.mli index dd731307..5ab39727 100644 --- a/src/th-data/Sidekick_th_data.mli +++ b/src/th-data/Sidekick_th_data.mli @@ -42,6 +42,9 @@ module type ARG = sig val mk_is_a: S.T.Term.state -> Cstor.t -> S.T.Term.t -> S.T.Term.t (** Make a [is-a] term *) + val mk_sel : S.T.Term.state -> Cstor.t -> int -> S.T.Term.t -> S.T.Term.t + (** Make a selector term *) + val ty_is_finite : S.T.Ty.t -> bool (** Is the given type known to be finite? *)