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

na

Browse source
This commit is contained in:
Nikolaj Bjorner 2020-05-06 10:36:03 -07:00
parent 93004a9d49
commit 1a642b4311
2 changed files with 18 additions and 18 deletions
Download patch file Download diff file Expand all files Collapse all files

16
src/ast/datatype_decl_plugin.h
View file

@ -340,13 +340,15 @@ namespace datatype {
bool is_is(func_decl * f) const { return is_decl_of(f, fid(), OP_DT_IS); }
bool is_accessor(func_decl * f) const { return is_decl_of(f, fid(), OP_DT_ACCESSOR); }
bool is_update_field(func_decl * f) const { return is_decl_of(f, fid(), OP_DT_UPDATE_FIELD); }
bool is_constructor(app * f) const { return is_app_of(f, fid(), OP_DT_CONSTRUCTOR); }
bool is_constructor(expr* e) const { return is_app(e) && is_constructor(to_app(e)); }
bool is_recognizer0(app * f) const { return is_app_of(f, fid(), OP_DT_RECOGNISER);}
bool is_is(app * f) const { return is_app_of(f, fid(), OP_DT_IS);}
bool is_is(expr * e) const { return is_app(e) && is_is(to_app(e)); }
bool is_recognizer(app * f) const { return is_recognizer0(f) || is_is(f); }
bool is_accessor(expr * e) const { return is_app(e) && is_app_of(to_app(e), fid(), OP_DT_ACCESSOR); }
bool is_constructor(app const * f) const { return is_app_of(f, fid(), OP_DT_CONSTRUCTOR); }
bool is_constructor(expr const * e) const { return is_app(e) && is_constructor(to_app(e)); }
bool is_recognizer0(app const* f) const { return is_app_of(f, fid(), OP_DT_RECOGNISER);}
bool is_is(app const * f) const { return is_app_of(f, fid(), OP_DT_IS);}
bool is_is(expr const * e) const { return is_app(e) && is_is(to_app(e)); }
bool is_recognizer(expr const * f) const { return is_app(f) && is_recognizer0(to_app(f)) || is_is(to_app(f)); }
MATCH_UNARY(is_recognizer);
bool is_accessor(expr const* e) const { return is_app(e) && is_app_of(to_app(e), fid(), OP_DT_ACCESSOR); }
MATCH_UNARY(is_accessor);
bool is_update_field(app * f) const { return is_app_of(f, fid(), OP_DT_UPDATE_FIELD); }
app* mk_is(func_decl * c, expr *f);
ptr_vector<func_decl> const * get_datatype_constructors(sort * ty);

20
src/smt/smt_consequences.cpp
View file

@ -47,11 +47,11 @@ namespace smt {
//
void context::extract_fixed_consequences(literal lit, index_set const& assumptions, expr_ref_vector& conseq) {
datatype_util dt(m);
expr* e1, *e2;
expr* e1, *e2, *arg;
expr_ref fml(m);
if (lit == true_literal) return;
expr* e = bool_var2expr(lit.var());
TRACE("context", display(tout << mk_pp(e, m) << "\n"););
TRACE("context", tout << mk_pp(e, m) << "\n";);
index_set s;
if (assumptions.contains(lit.var())) {
s.insert(lit.var());
@ -60,9 +60,6 @@ namespace smt {
justify(lit, s);
}
m_antecedents.insert(lit.var(), s);
TRACE("context", display_literal_verbose(tout, lit);
for (auto v : s) tout << " " << v;
tout << "\n";);
bool found = false;
if (m_var2val.contains(e)) {
found = true;
@ -85,11 +82,11 @@ namespace smt {
fml = m.mk_eq(e1, e2);
}
}
else if (!lit.sign() && is_app(e) && dt.is_recognizer(to_app(e)->get_decl())) {
if (m_var2val.contains(to_app(e)->get_arg(0))) {
else if (!lit.sign() && dt.is_recognizer(e, arg)) {
if (m_var2val.contains(arg)) {
found = true;
fml = m.mk_eq(to_app(e)->get_arg(0), m.mk_const(dt.get_recognizer_constructor(to_app(e)->get_decl())));
m_var2val.erase(to_app(e)->get_arg(0));
fml = m.mk_eq(arg, m.mk_const(dt.get_recognizer_constructor(to_app(e)->get_decl())));
m_var2val.erase(arg);
}
}
if (found) {
@ -172,7 +169,7 @@ namespace smt {
TRACE("context",
tout << "checking " << mk_pp(k, m) << " "
<< mk_pp(v, m) << " " << get_assignment(lit) << "\n";
display(tout);
//display(tout);
);
switch (get_assignment(lit)) {
case l_true:
@ -424,6 +421,7 @@ namespace smt {
m_not_l = null_literal;
}
if (is_sat == l_true) {
TRACE("context", display(tout););
delete_unfixed(unfixed);
}
extract_fixed_consequences(num_units, _assumptions, conseq);
@ -639,7 +637,7 @@ namespace smt {
for (expr* a : assumptions) {
assert_expr(a);
}
TRACE("context", tout << "checking: " << mk_pp(c, m) << "\n";);
TRACE("context", tout << "checking fixed: " << mk_pp(c, m) << "\n";);
tmp = m.mk_not(c);
assert_expr(tmp);
VERIFY(check() != l_true);