mirror of
https://github.com/Z3Prover/z3
synced 2025-04-06 09:34:08 +00:00
parent
0499b6b64a
commit
c2e0491456
|
@ -191,6 +191,11 @@ class mbp::impl {
|
|||
vars.shrink(j);
|
||||
}
|
||||
|
||||
// over-approximation
|
||||
bool contains_uninterpreted(expr* v) {
|
||||
return true;
|
||||
}
|
||||
|
||||
bool extract_bools(model_evaluator& eval, expr_ref_vector& fmls, expr* fml) {
|
||||
TRACE("qe", tout << "extract bools: " << mk_pp(fml, m) << "\n";);
|
||||
ptr_vector<expr> todo;
|
||||
|
@ -209,10 +214,14 @@ class mbp::impl {
|
|||
m_visited.mark(e);
|
||||
if (m.is_bool(e) && !m.is_true(e) && !m.is_false(e) && m.inc()) {
|
||||
expr_ref val = eval(e);
|
||||
TRACE("qe", tout << "found: " << mk_pp(e, m) << "\n";);
|
||||
TRACE("qe", tout << "found: " << mk_pp(e, m) << " " << val << "\n";);
|
||||
if (!m.inc())
|
||||
continue;
|
||||
if (!m.is_true(val) && !m.is_false(val) && contains_uninterpreted(val)) {
|
||||
throw default_exception("could not evaluate Boolean in model");
|
||||
}
|
||||
SASSERT(m.is_true(val) || m.is_false(val));
|
||||
|
||||
if (!m_bool_visited.is_marked(e)) {
|
||||
fmls.push_back(m.is_true(val) ? e : mk_not(m, e));
|
||||
}
|
||||
|
|
|
@ -331,7 +331,7 @@ namespace qe {
|
|||
}
|
||||
if (sz == args.size()) {
|
||||
if (diff) {
|
||||
r = m.mk_app(a->get_decl(), sz, args.c_ptr());
|
||||
r = m.mk_app(a->get_decl(), args);
|
||||
trail.push_back(r);
|
||||
}
|
||||
else {
|
||||
|
@ -424,7 +424,7 @@ namespace qe {
|
|||
}
|
||||
if (args.size() == sz) {
|
||||
if (diff) {
|
||||
r = m.mk_app(a->get_decl(), sz, args.c_ptr());
|
||||
r = m.mk_app(a->get_decl(), args);
|
||||
}
|
||||
else {
|
||||
r = to_app(a);
|
||||
|
@ -456,9 +456,8 @@ namespace qe {
|
|||
|
||||
void pred_abs::display(std::ostream& out) const {
|
||||
out << "pred2lit:\n";
|
||||
obj_map<expr, expr*>::iterator it = m_pred2lit.begin(), end = m_pred2lit.end();
|
||||
for (; it != end; ++it) {
|
||||
out << mk_pp(it->m_key, m) << " |-> " << mk_pp(it->m_value, m) << "\n";
|
||||
for (auto const& kv : m_pred2lit) {
|
||||
out << mk_pp(kv.m_key, m) << " |-> " << mk_pp(kv.m_value, m) << "\n";
|
||||
}
|
||||
for (unsigned i = 0; i < m_preds.size(); ++i) {
|
||||
out << "level " << i << "\n";
|
||||
|
@ -477,10 +476,10 @@ namespace qe {
|
|||
|
||||
void pred_abs::display(std::ostream& out, expr_ref_vector const& asms) const {
|
||||
max_level lvl;
|
||||
for (unsigned i = 0; i < asms.size(); ++i) {
|
||||
expr* e = asms[i];
|
||||
bool is_not = m.is_not(asms[i], e);
|
||||
out << mk_pp(asms[i], m);
|
||||
for (expr* a : asms) {
|
||||
expr* e = a;
|
||||
bool is_not = m.is_not(a, e);
|
||||
out << mk_pp(a, m);
|
||||
if (m_elevel.find(e, lvl)) {
|
||||
lvl.display(out << " - ");
|
||||
}
|
||||
|
@ -1010,7 +1009,7 @@ namespace qe {
|
|||
}
|
||||
}
|
||||
if (all_visited) {
|
||||
r = m.mk_app(a->get_decl(), args.size(), args.c_ptr());
|
||||
r = m.mk_app(a->get_decl(), args);
|
||||
todo.pop_back();
|
||||
trail.push_back(r);
|
||||
visited.insert(e, r);
|
||||
|
|
|
@ -10,6 +10,7 @@ z3_add_component(smt
|
|||
expr_context_simplifier.cpp
|
||||
fingerprints.cpp
|
||||
mam.cpp
|
||||
model_sweeper.cpp
|
||||
old_interval.cpp
|
||||
qi_queue.cpp
|
||||
seq_axioms.cpp
|
||||
|
|
|
@ -22,6 +22,7 @@ Revision History:
|
|||
#include "ast/for_each_expr.h"
|
||||
#include "smt/theory_recfun.h"
|
||||
#include "smt/params/smt_params_helper.hpp"
|
||||
#include "smt/model_sweeper.h"
|
||||
|
||||
|
||||
#define TRACEFN(x) TRACE("recfun", tout << x << '\n';)
|
||||
|
@ -443,6 +444,7 @@ namespace smt {
|
|||
final_check_status theory_recfun::final_check_eh() {
|
||||
TRACEFN("final\n");
|
||||
if (can_propagate()) {
|
||||
generate_induction_lemmas(get_context());
|
||||
propagate();
|
||||
return FC_CONTINUE;
|
||||
}
|
||||
|
|
Loading…
Reference in a new issue