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

wip missing updates

Browse source
This commit is contained in:
Nikolaj Bjorner 2022-11-13 12:10:43 -08:00
parent 196788a091
commit 38cde14e08
1 changed files with 7 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

9
src/ast/converters/expr_inverter.cpp
View file

@ -40,7 +40,7 @@ class basic_expr_inverter : public iexpr_inverter {
mk_fresh_uncnstr_var_for(f, r); mk_fresh_uncnstr_var_for(f, r);
if (m_mc) if (m_mc)
add_def(v, m.mk_ite(t, t, d)); add_def(v, m.mk_ite(r, t, d));
return true; return true;
} }
@ -352,8 +352,11 @@ class bv_expr_inverter : public iexpr_inverter {
// parity can be defined using a "giant" ite expression. // parity can be defined using a "giant" ite expression.
// //
#if 0
for (unsigned i = 0; i < num; ++i)
if (uncnstr(args[i])) if (uncnstr(args[i]))
IF_VERBOSE(11, verbose_stream() << "MISSED mult-unconstrained " << mk_bounded_pp(args[i], m) << "\n"); IF_VERBOSE(11, verbose_stream() << "MISSED mult-unconstrained " << mk_bounded_pp(args[i], m) << "\n");
#endif
return false; return false;
} }
@ -550,6 +553,7 @@ class bv_expr_inverter : public iexpr_inverter {
} }
bool mk_diff(expr* t, expr_ref& r) override { bool mk_diff(expr* t, expr_ref& r) override {
SASSERT(bv.is_bv(t));
r = bv.mk_bv_not(t); r = bv.mk_bv_not(t);
return true; return true;
} }
@ -806,7 +810,8 @@ void expr_inverter::set_is_var(std::function<bool(expr*)>& is_var) {
} }
void expr_inverter::set_model_converter(generic_model_converter* mc) { void expr_inverter::set_model_converter(generic_model_converter* mc) {
m_mc = mc;
for (auto* p : m_inverters) for (auto* p : m_inverters)
if (p) if (p)
p->set_model_converter(mc); p->set_model_converter(mc);
} }