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) diff --git a/src/base-term/Base_types.ml b/src/base-term/Base_types.ml index fa3449ef..e719aac5 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 = { @@ -85,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; @@ -97,10 +99,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 +183,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 +210,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 +217,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 +239,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 +271,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 +294,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 +314,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 +328,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) [] @@ -438,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 @@ -488,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 @@ -585,6 +556,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 @@ -968,17 +941,6 @@ module Data = struct let pp out d = ID.pp out d.data_id end -module Cstor = struct - type t = cstor = { - cstor_id: ID.t; - cstor_is_a: ID.t; - cstor_args: select list lazy_t; - cstor_ty_as_data: data; - cstor_ty: ty lazy_t; - } - let equal = eq_cstor -end - module Select = struct type t = select = { select_id: ID.t; @@ -986,6 +948,23 @@ module Select = struct 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; + 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; + } + 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 Proof = struct 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/cc/Sidekick_cc.ml b/src/cc/Sidekick_cc.ml index f6ad319a..a64b2454 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 @@ -281,14 +279,24 @@ 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[@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 + 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 @@ -330,20 +338,22 @@ 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@])" - 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]. @@ -550,7 +560,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 *) @@ -574,17 +584,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 *) @@ -615,8 +625,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@])" @@ -637,9 +647,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 @@ -771,7 +781,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 -> @@ -781,7 +791,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 @@ -805,6 +815,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 = diff --git a/src/core/Sidekick_core.ml b/src/core/Sidekick_core.ml index 6be110ba..0f554612 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 @@ -232,10 +231,14 @@ 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}. *) + 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 *) @@ -279,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]. @@ -359,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. *) @@ -658,3 +664,146 @@ 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 * (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 -> + SI.CC.Expl.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 + 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 + val iter_all : t -> (M.SI.CC.repr * M.t) Iter.t +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 = + 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 + 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' (Expl.mk_list []) 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 + + let on_pre_merge (self:t) cc acts n1 n2 e_n1_n2 : unit = + 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@ :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 e_n1_n2 with + | Ok v' -> + N_tbl.remove self.values n2; (* only keep repr *) + N_tbl.add self.values n1 v'; + | 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; + 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 + + let create_and_setup ?size (solver:SI.t) : t = + 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); + self +end 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/main.ml b/src/main/main.ml index f22e3185..12b57e49 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 () @@ -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/main/sidekick_version.ml b/src/main/sidekick_version.ml index bcefbe83..fa6207d0 100644 --- a/src/main/sidekick_version.ml +++ b/src/main/sidekick_version.ml @@ -1,2 +1 @@ -let version = {git|ef77e1e729f176c3db680de25df9f2f820795e47 -|git} \ No newline at end of file +let version = {git|dev|git} \ No newline at end of file diff --git a/src/msat-solver/Sidekick_msat_solver.ml b/src/msat-solver/Sidekick_msat_solver.ml index fc3de178..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 @@ -558,6 +562,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/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/Process.ml b/src/smtlib/Process.ml index 90efbed7..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 -> @@ -200,7 +199,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? *) @@ -258,14 +257,40 @@ 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 + module Cstor = Cstor - 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 as_datatype ty = match Ty.view ty with + | Ty_atomic {def=Ty_data data;_} -> + 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} + + 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_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)) + ) 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 end) module Th_bool = Sidekick_th_bool_static.Make(struct @@ -275,4 +300,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/Typecheck.ml b/src/smtlib/Typecheck.ml index fa616caa..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) -> @@ -390,8 +390,9 @@ 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_arity=0; cstor_ty_as_data=data; cstor_ty=data.data_as_ty; } in @@ -416,19 +417,19 @@ 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 (* 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/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-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)"; diff --git a/src/th-cstor/Sidekick_th_cstor.ml b/src/th-cstor/Sidekick_th_cstor.ml index 1d5b666b..279d4ac9 100644 --- a/src/th-cstor/Sidekick_th_cstor.ml +++ b/src/th-cstor/Sidekick_th_cstor.ml @@ -24,71 +24,62 @@ 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 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; + ] + 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 new file mode 100644 index 00000000..e023ed6e --- /dev/null +++ b/src/th-data/Sidekick_th_data.ml @@ -0,0 +1,888 @@ + +(** {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; + } + | Ty_other + +let name = "th-data" + +(** An abtract representation of a datatype *) +module type DATA_TY = sig + type t + type cstor + + 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 + + (** A table indexed by types. *) + module Tbl : Hashtbl.S with type key = t +end + +(** {2 Cardinality of types} *) + +module C = 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 sum = Iter.fold (+) Finite + let product = Iter.fold ( * ) Finite +end + +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 + 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 + +(** 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 + 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 Ty = A.S.T.Ty + module Fun = A.S.T.Fun + module Expl = SI.CC.Expl + + 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 = { + c_n: N.t; + c_cstor: A.Cstor.t; + c_args: T.t IArray.t; + } + + let pp out (v:t) = + 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 = + match A.view_as_data t with + | T_cstor (cstor,args) -> + Some {c_n=n;c_cstor=cstor; c_args=args}, [] + | _ -> None, [] + + 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@])@])" + 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; + ] + in + if A.Cstor.equal c1.c_cstor c2.c_cstor then ( + (* same function: injectivity *) + assert (IArray.length c1.c_args = IArray.length c2.c_args); + IArray.iter2 + (fun u1 u2 -> SI.CC.merge_t cc u1 u2 expl) + 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; + 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) *) + 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@ :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@]]@]@])" + 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; 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; is_a_arg=u;}]; + parent_select=[]; + } in + None, [u, m_sel] + | T_cstor _ | T_other _ -> None, [] + + 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); + 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: 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: 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 + | T_cstor (cstor,args) -> + Log.debugf 20 + (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-finite-ty@ %a@])" name T.pp t); + N_tbl.add self.to_decide n (); + ) + | _ -> () + + 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 -> + 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 + (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) -> + 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) + | Some _ -> () + | None -> + N_tbl.add self.to_decide repr_u (); (* needs to be decided *) + 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-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; + 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@ :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; + mk_merge_t (N.term n2) sel2.sel_arg]); + ) + 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; + 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.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.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.Monoid_cstor.c_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 + + (* 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. *) + 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) + |> Iter.filter + (fun n -> + not (ST_cstors.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.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 -> + let t = N.term n in + (* [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; + () + + let create_and_setup (solver:SI.t) : t = + 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(); + } 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_partial_check solver (on_partial_check self); + SI.on_final_check solver (on_final_check 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/Sidekick_th_data.mli b/src/th-data/Sidekick_th_data.mli new file mode 100644 index 00000000..5ab39727 --- /dev/null +++ b/src/th-data/Sidekick_th_data.mli @@ -0,0 +1,60 @@ + +(** 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 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? *) + + 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 diff --git a/src/th-data/dune b/src/th-data/dune new file mode 100644 index 00000000..f1dfcd0f --- /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 -w -27-32)) ; TODO get warning back + 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) + *) diff --git a/tests/benchpress.sexp b/tests/benchpress.sexp index 20006d15..42c06d62 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/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) + + 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/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) 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_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/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) 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/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) + + 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) + +