mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-12 12:08:18 +00:00
Code Activity

#5528

Browse source
This commit is contained in:
Nikolaj Bjorner 2021-09-02 11:21:57 -07:00
parent 55285b2193
commit af5c6e43b9
2 changed files with 10 additions and 4 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/sat/sat_solver/inc_sat_solver.cpp
View file

@ -1050,6 +1050,8 @@ private:
eval.set_model_completion(true); eval.set_model_completion(true);
bool all_true = true; bool all_true = true;
for (expr * f : m_fmls) { for (expr * f : m_fmls) {
if (has_quantifiers(f))
continue;
expr_ref tmp(m); expr_ref tmp(m);
eval(f, tmp); eval(f, tmp);
if (m.limit().is_canceled()) if (m.limit().is_canceled())

12
src/sat/smt/q_ematch.cpp
View file

@ -359,17 +359,21 @@ namespace q {
for (unsigned i = 0; i < c.num_decls(); ++i) for (unsigned i = 0; i < c.num_decls(); ++i)
_binding.push_back(binding[i]->get_expr()); _binding.push_back(binding[i]->get_expr());
var_subst subst(m); var_subst subst(m);
auto sub = [&](expr* e) {
expr_ref r = subst(e, _binding);
//ctx.rewrite(r);
return l.sign ? ~ctx.mk_literal(r) : ctx.mk_literal(r);
};
if (m.is_true(l.rhs)) { if (m.is_true(l.rhs)) {
SASSERT(!l.sign); SASSERT(!l.sign);
return ctx.mk_literal(subst(l.lhs, _binding)); return sub(l.lhs);
} }
else if (m.is_false(l.rhs)) { else if (m.is_false(l.rhs)) {
SASSERT(!l.sign); SASSERT(!l.sign);
return ~ctx.mk_literal(subst(l.lhs, _binding)); return ~sub(l.lhs);
} }
expr_ref fml(m.mk_eq(l.lhs, l.rhs), m); expr_ref fml(m.mk_eq(l.lhs, l.rhs), m);
fml = subst(fml, _binding); return sub(fml);
return l.sign ? ~ctx.mk_literal(fml) : ctx.mk_literal(fml);
} }
struct ematch::reset_in_queue : public trail { struct ematch::reset_in_queue : public trail {