mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-03 21:01:22 +00:00
Code Activity

fix model completion bug in PDR, addhoc handling of reals for arithmetic realizers

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2012-11-06 15:38:07 +02:00
parent 2c66afadd6
commit cec851440e
2 changed files with 12 additions and 3 deletions
Download patch file Download diff file Expand all files Collapse all files

6
src/muz_qe/pdr_context.cpp
View file

@ -1705,6 +1705,7 @@ namespace pdr {
void context::create_children(model_node& n) { void context::create_children(model_node& n) {
SASSERT(n.level() > 0); SASSERT(n.level() > 0);
bool use_model_generalizer = m_params.get_bool(":use-model-generalizer", false); bool use_model_generalizer = m_params.get_bool(":use-model-generalizer", false);
datalog::scoped_no_proof _sc(m);
pred_transformer& pt = n.pt(); pred_transformer& pt = n.pt();
model_ref M = n.get_model_ptr(); model_ref M = n.get_model_ptr();
@ -1764,12 +1765,13 @@ namespace pdr {
if (!vars.empty()) { if (!vars.empty()) {
// also fresh names for auxiliary variables in body? // also fresh names for auxiliary variables in body?
expr_substitution sub(m); expr_substitution sub(m);
expr_ref_vector refs(m);
expr_ref tmp(m); expr_ref tmp(m);
proof_ref pr(m); proof_ref pr(m);
pr = m.mk_asserted(m.mk_true()); pr = m.mk_asserted(m.mk_true());
for (unsigned i = 0; i < vars.size(); ++i) { for (unsigned i = 0; i < vars.size(); ++i) {
M->eval(vars[i]->get_decl(), tmp); VERIFY (M->eval(vars[i].get(), tmp, true));
refs.push_back(tmp);
sub.insert(vars[i].get(), tmp, pr); sub.insert(vars[i].get(), tmp, pr);
} }
if (!rep) rep = mk_expr_simp_replacer(m); if (!rep) rep = mk_expr_simp_replacer(m);

9
src/muz_qe/qe_arith_plugin.cpp
View file

@ -1863,11 +1863,18 @@ public:
// x := coeff * x + s // x := coeff * x + s
def = m_util.mk_add(m_util.mk_mul(x_t.get_coeff(), def), x_t.get_term()); def = m_util.mk_add(m_util.mk_mul(x_t.get_coeff(), def), x_t.get_term());
} }
if (is_strict) {
SASSERT(m_util.m_arith.is_real(x));
// We actually want a supremum, such that dual inequalities are satisfied.
// i.e. for every dual inequality , if the dual bound is feasible, make sure to
// choose a value in the feasible range.
def = m_util.mk_sub(def, m_util.mk_one(x));
}
m_util.simplify(def); m_util.simplify(def);
TRACE("qe", tout << "TBD: " << a << " " << mk_pp(def, m) << "\n";); TRACE("qe", tout << "TBD (for Real): " << a << " " << mk_pp(def, m) << "\n";);
} }
expr_ref mk_not(expr* e) { expr_ref mk_not(expr* e) {