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

fixing bugs in model evaluator. remove wrong assertions

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2012-11-17 22:09:15 +01:00
parent 50385e7e29
commit 29a45e34a2
3 changed files with 23 additions and 5 deletions
Download patch file Download diff file Expand all files Collapse all files

13
src/muz_qe/dl_context.cpp
View file

@ -1608,12 +1608,14 @@ namespace datalog {
expr* const* axioms = m_background.c_ptr();
expr_ref fml(m);
expr_ref_vector rules(m);
svector<symbol> names;
bool use_fixedpoint_extensions = m_params.get_bool(":print-with-fixedpoint-extensions", true);
{
rule_set::iterator it = m_rule_set.begin(), end = m_rule_set.end();
for (; it != end; ++it) {
(*it)->to_formula(fml);
rules.push_back(fml);
names.push_back((*it)->name());
}
}
@ -1680,11 +1682,18 @@ namespace datalog {
}
for (unsigned i = 0; i < rules.size(); ++i) {
out << (use_fixedpoint_extensions?"(rule ":"(assert ");
expr* r = rules[i].get();
if (symbol::null != names[i]) {
out << "(! ";
}
if (use_fixedpoint_extensions) {
ast_smt2_pp(out, rules[i].get(), env, params);
ast_smt2_pp(out, r, env, params);
}
else {
out << mk_smt_pp(rules[i].get(), m);
out << mk_smt_pp(r, m);
}
if (symbol::null != names[i]) {
out << " :named " << names[i] << ")";
}
out << ")\n";
}

11
src/muz_qe/pdr_util.cpp
View file

@ -466,6 +466,7 @@ void model_evaluator::eval_arith(app* e) {
}
void model_evaluator::inherit_value(expr* e, expr* v) {
expr* w;
SASSERT(!is_unknown(v));
SASSERT(m.get_sort(e) == m.get_sort(v));
if (is_x(v)) {
@ -475,7 +476,10 @@ void model_evaluator::inherit_value(expr* e, expr* v) {
SASSERT(m.is_bool(v));
if (is_true(v)) set_true(e);
else if (is_false(v)) set_false(e);
else set_x(e);
else {
TRACE("pdr", tout << "not inherited:\n" << mk_pp(e, m) << "\n" << mk_pp(v, m) << "\n";);
set_x(e);
}
}
else if (m_arith.is_int_real(e)) {
set_number(e, get_number(v));
@ -483,7 +487,11 @@ void model_evaluator::inherit_value(expr* e, expr* v) {
else if (m.is_value(v)) {
set_value(e, v);
}
else if (m_values.find(v, w)) {
set_value(e, w);
}
else {
TRACE("pdr", tout << "not inherited:\n" << mk_pp(e, m) << "\n" << mk_pp(v, m) << "\n";);
set_x(e);
}
}
@ -642,6 +650,7 @@ void model_evaluator::eval_basic(app* e) {
set_bool(e, e1 == e2);
}
else {
TRACE("pdr", tout << "not value equal:\n" << mk_pp(e1, m) << "\n" << mk_pp(e2, m) << "\n";);
set_x(e);
}
}

4
src/muz_qe/proof_utils.cpp
View file

@ -223,7 +223,7 @@ public:
found_false = true;
break;
}
SASSERT(m.get_fact(tmp) == m.get_fact(m.get_parent(p, i)));
// SASSERT(m.get_fact(tmp) == m.get_fact(m.get_parent(p, i)));
parents.push_back(tmp);
if (is_closed(tmp) && !m_units.contains(m.get_fact(tmp))) {
m_units.insert(m.get_fact(tmp), tmp);
@ -283,7 +283,7 @@ public:
found_false = true;
break;
}
SASSERT(m.get_fact(tmp) == m.get_fact(m.get_parent(p, i)));
// SASSERT(m.get_fact(tmp) == m.get_fact(m.get_parent(p, i)));
change = change || (tmp != m.get_parent(p, i));
args.push_back(tmp);
}