simon/sidekick
1
0
Fork 0
mirror of https://github.com/c-cube/sidekick.git synced 2025-12-06 03:05:31 -05:00
Code Issues Projects Releases Packages Wiki Activity Actions

Merge branch 'wip-data'

Browse source
This commit is contained in:
Simon Cruanes 2020-01-14 23:02:49 -06:00
commit 5bcecfd68c
38 changed files with 1708 additions and 199 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
Makefile
View file

@ -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)

127
src/base-term/Base_types.ml
View file

@ -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

1
src/base-term/Sidekick_base_term.ml
View file

@ -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

63
src/cc/Sidekick_cc.ml
View file

@ -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 "(@[<hv1>cc.push_pending@ %a@])" N.pp t);
Log.debugf 50 (fun k->k "(@[<hv1>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 "(@[<hv1>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 "(@[<hv1>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 "(@[<hv>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 =

157
src/core/Sidekick_core.ml
View file

@ -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

5
src/main/dune
View file

@ -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))

4
src/main/main.ml
View file

@ -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 ->

3
src/main/sidekick_version.ml
View file

@ -1,2 +1 @@
let version = {git|ef77e1e729f176c3db680de25df9f2f820795e47
|git}
let version = {git|dev|git}

9
src/msat-solver/Sidekick_msat_solver.ml
View file

@ -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 "(@[<hv1>@{<green>msat-solver.assume_lits@}%s@ %a@])"
(if final then "[final]" else "") (Util.pp_seq ~sep:"; " Lit.pp) lits);
(fun k->k "(@[<hv1>@{<green>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)

12
src/smtlib/Form.ml
View file

@ -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

39
src/smtlib/Process.ml
View file

@ -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

2
src/smtlib/Process.mli
View file

@ -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

11
src/smtlib/Typecheck.ml
View file

@ -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]

2
src/smtlib/dune
View file

@ -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

18
src/th-bool-static/Sidekick_th_bool_static.ml
View file

@ -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)";

105
src/th-cstor/Sidekick_th_cstor.ml
View file

@ -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 =

888
src/th-data/Sidekick_th_data.ml Normal file
View file

@ -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 "(@[<hv>%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: (@[<hv>%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
*)

60
src/th-data/Sidekick_th_data.mli Normal file
View file

@ -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

8
src/th-data/dune Normal file
View file

@ -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

2
src/th-data/types.ml
View file

@ -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)
*)

2
tests/benchpress.sexp
View file

@ -9,7 +9,7 @@
(dir
(path $cur_dir)
(pattern ".*.(smt2|cnf)")
(pattern ".*.(smt2|cnf)$")
(expect (try (run smtlib-read-status) (run z3))))
(task

40
tests/sat/typed_v5l90027.cvc.smt2 Normal file
View file

@ -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)

28
tests/sat/v1l40032.cvc.smt2 Normal file
View file

@ -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)

8
tests/unsat/data_acycl1.smt2 Normal file
View file

@ -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)

14
tests/unsat/data_acycl_if.smt2 Normal file
View file

@ -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)

11
tests/unsat/data_card1.smt2 Normal file
View file

@ -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)

22
tests/unsat/diamond2_cong_if.smt2 Normal file
View file

@ -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)

14
tests/unsat/if_ff_fg.smt2 Normal file
View file

@ -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)

17
tests/unsat/nested_if.smt2 Normal file
View file

@ -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)

14
tests/unsat/smtlib.626179.smt2 Normal file
View file

@ -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)

23
tests/unsat/t_cstor1.smt2.tmp Normal file
View file

@ -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)

12
tests/unsat/t_subform.smt2 Normal file
View file

@ -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)

8
tests/unsat/test_ite_1.smt2 Normal file
View file

@ -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)

34
tests/unsat/typed_v3l30091.cvc.smt2 Normal file
View file

@ -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)

34
tests/unsat/typed_v3l40070.cvc.smt2 Normal file
View file

@ -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)

40
tests/unsat/typed_v5l90068.cvc.smt2 Normal file
View file

@ -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)

34
tests/unsat/v3l60049.cvc.smt2 Normal file
View file

@ -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)

34
tests/unsat/v3l90003.cvc.smt2 Normal file
View file

@ -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)