mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-14 04:48:45 +00:00
Code Activity

fix

Browse source
This commit is contained in:
Nikolaj Bjorner 2022-01-24 15:11:24 +01:00
parent 20f9814939
commit 3b8c0b7ae6
2 changed files with 11 additions and 9 deletions

13
src/ast/datatype_decl_plugin.cpp
View file

@ -580,7 +580,7 @@ namespace datatype {
m_defs.remove(s);
}
bool plugin::is_value_visit(expr * arg, ptr_buffer<app> & todo) const {
bool plugin::is_value_visit(bool unique, expr * arg, ptr_buffer<app> & todo) const {
if (!is_app(arg))
return false;
family_id fid = to_app(arg)->get_family_id();
@ -592,12 +592,13 @@ namespace datatype {
todo.push_back(to_app(arg));
return true;
}
else {
else if (unique)
return m_manager->is_unique_value(arg);
else
return m_manager->is_value(arg);
}
}
bool plugin::is_value(app * e) const {
bool plugin::is_value_aux(bool unique, app * e) const {
TRACE("dt_is_value", tout << "checking\n" << mk_ismt2_pp(e, *m_manager) << "\n";);
if (!u().is_constructor(e))
return false;
@ -608,7 +609,7 @@ namespace datatype {
ptr_buffer<app> todo;
// potentially expensive check for common sub-expressions.
for (expr* arg : *e) {
if (!is_value_visit(arg, todo)) {
if (!is_value_visit(unique, arg, todo)) {
TRACE("dt_is_value", tout << "not-value:\n" << mk_ismt2_pp(arg, *m_manager) << "\n";);
return false;
}
@ -618,7 +619,7 @@ namespace datatype {
SASSERT(u().is_constructor(curr));
todo.pop_back();
for (expr* arg : *curr) {
if (!is_value_visit(arg, todo)) {
if (!is_value_visit(unique, arg, todo)) {
TRACE("dt_is_value", tout << "not-value:\n" << mk_ismt2_pp(arg, *m_manager) << "\n";);
return false;
}

7
src/ast/datatype_decl_plugin.h
View file

@ -230,9 +230,9 @@ namespace datatype {
bool is_fully_interp(sort * s) const override;
bool is_value(app* e) const override;
bool is_value(app* e) const override { return is_value_aux(false, e); }
bool is_unique_value(app * e) const override { return is_value(e); }
bool is_unique_value(app * e) const override { return is_value_aux(true, e); }
void get_op_names(svector<builtin_name> & op_names, symbol const & logic) override;
@ -257,7 +257,8 @@ namespace datatype {
bool has_nested_arrays() const { return m_has_nested_arrays; }
private:
bool is_value_visit(expr * arg, ptr_buffer<app> & todo) const;
bool is_value_visit(bool unique, expr * arg, ptr_buffer<app> & todo) const;
bool is_value_aux(bool unique, app * arg) const;
func_decl * mk_update_field(
unsigned num_parameters, parameter const * parameters,