Skip to content

Commit

Permalink
na
Browse files Browse the repository at this point in the history
  • Loading branch information
@NikolajBjorner
NikolajBjorner committed May 6, 2020
1 parent 93004a9 commit 1a642b4
Show file tree
Hide file tree
Showing 2 changed files with 18 additions and 18 deletions.
16 changes: 9 additions & 7 deletions src/ast/datatype_decl_plugin.h
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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)); }

This comment has been minimized.

Sign in to view

Copy link
@LeventErkok

LeventErkok May 7, 2020

This line generates a warning:

../src/ast/datatype_decl_plugin.h:348:69: warning: '&&' within '||' [-Wlogical-op-parentheses]
        bool is_recognizer(expr const * f) const { return is_app(f) && is_recognizer0(to_app(f)) || is_is(to_app(f)); }
                                                          ~~~~~~~~~~^~~~~~~~~~~~~~~~~~~~~~~~~~~~ ~~
../src/ast/datatype_decl_plugin.h:348:69: note: place parentheses around the '&&' expression to silence this warning
        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);
Expand Down
20 changes: 9 additions & 11 deletions src/smt/smt_consequences.cpp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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());
Expand All @@ -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;
Expand All @@ -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) {
Expand Down Expand Up @@ -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:
Expand Down Expand Up @@ -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);
Expand Down Expand Up @@ -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);
Expand Down

0 comments on commit 1a642b4

Please sign in to comment.