mirror of
https://github.com/Z3Prover/z3
synced 2025-04-08 18:31:49 +00:00
extend distinct check to ADT
This commit is contained in:
parent
61f7dc3513
commit
f2afb369bd
|
@ -635,6 +635,28 @@ namespace datatype {
|
|||
}
|
||||
}
|
||||
|
||||
bool plugin::are_distinct(app * a, app * b) const {
|
||||
if (a == b)
|
||||
return false;
|
||||
if (is_unique_value(a) && is_unique_value(b))
|
||||
return true;
|
||||
if (u().is_constructor(a) && u().is_constructor(b)) {
|
||||
if (a->get_decl() != b->get_decl())
|
||||
return true;
|
||||
for (unsigned i = a->get_num_args(); i-- > 0; ) {
|
||||
if (!is_app(a->get_arg(i)))
|
||||
continue;
|
||||
if (!is_app(b->get_arg(i)))
|
||||
continue;
|
||||
app* _a = to_app(a->get_arg(i));
|
||||
app* _b = to_app(b->get_arg(i));
|
||||
if (m_manager->are_distinct(_a, _b))
|
||||
return true;
|
||||
}
|
||||
}
|
||||
return false;
|
||||
}
|
||||
|
||||
expr * plugin::get_some_value(sort * s) {
|
||||
SASSERT(u().is_datatype(s));
|
||||
func_decl * c = u().get_non_rec_constructor(s);
|
||||
|
|
|
@ -233,6 +233,8 @@ namespace datatype {
|
|||
bool is_value(app* e) const override { return is_value_aux(false, e); }
|
||||
|
||||
bool is_unique_value(app * e) const override { return is_value_aux(true, e); }
|
||||
|
||||
bool are_distinct(app * a, app * b) const override;
|
||||
|
||||
void get_op_names(svector<builtin_name> & op_names, symbol const & logic) override;
|
||||
|
||||
|
|
Loading…
Reference in a new issue