mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-20 12:53:38 +00:00
Code Activity

In lazy ackermannization, collect all conflicting terms in one iteration.

Browse source
This commit is contained in:
mikolas 2016-02-26 13:02:59 +00:00 • committed by Mikolas Janota
parent 2f8465552c
commit a2140085d6
1 changed files with 22 additions and 13 deletions
Download patch file Download diff file Expand all files Collapse all files

35
src/ackermannization/lackr_model_constructor.cpp
View file

@ -60,15 +60,17 @@ struct lackr_model_constructor::imp {
// //
// Returns true iff model was successfully constructed. // Returns true iff model was successfully constructed.
// Conflicts are saved as a side effect.
// //
bool check() { bool check() {
bool retv = true;
for (unsigned i = 0; i < m_abstr_model->get_num_constants(); i++) { for (unsigned i = 0; i < m_abstr_model->get_num_constants(); i++) {
func_decl * const c = m_abstr_model->get_constant(i); func_decl * const c = m_abstr_model->get_constant(i);
app * const term = m_info->find_term(c); app * const _term = m_info->find_term(c);
if (term) m_stack.push_back(term); expr * const term = _term ? _term : m_m.mk_const(c);
else m_stack.push_back(m_m.mk_const(c)); if (!check_term(term)) retv = false;
} }
return run(); return retv;
} }
@ -144,6 +146,7 @@ struct lackr_model_constructor::imp {
app2val_t m_app2val; app2val_t m_app2val;
ptr_vector<expr> m_stack; ptr_vector<expr> m_stack;
ackr_helper m_ackr_helper; ackr_helper m_ackr_helper;
expr_mark m_visited;
static inline val_info mk_val_info(expr* value, app* source_term) { static inline val_info mk_val_info(expr* value, app* source_term) {
val_info rv; val_info rv;
@ -152,17 +155,23 @@ struct lackr_model_constructor::imp {
return rv; return rv;
} }
// // Performs congruence check on a given term.
bool check_term(expr * term) {
m_stack.push_back(term);
const bool rv = _check_stack();
m_stack.reset();
return rv;
}
// Performs congruence check on terms on the stack. // Performs congruence check on terms on the stack.
// (Currently stops upon the first failure). // Stops upon the first failure.
// Returns true if and only if congruence check succeeded. // Returns true if and only if all congruence checks succeeded.
bool run() { bool _check_stack() {
m_evaluator = alloc(model_evaluator, m_empty_model); if (m_evaluator == NULL) m_evaluator = alloc(model_evaluator, m_empty_model);
expr_mark visited;
expr * curr; expr * curr;
while (!m_stack.empty()) { while (!m_stack.empty()) {
curr = m_stack.back(); curr = m_stack.back();
if (visited.is_marked(curr)) { if (m_visited.is_marked(curr)) {
m_stack.pop_back(); m_stack.pop_back();
continue; continue;
} }
@ -173,8 +182,8 @@ struct lackr_model_constructor::imp {
return false; return false;
case AST_APP: { case AST_APP: {
app * a = to_app(curr); app * a = to_app(curr);
if (for_each_expr_args(m_stack, visited, a->get_num_args(), a->get_args())) { if (for_each_expr_args(m_stack, m_visited, a->get_num_args(), a->get_args())) {
visited.mark(a, true); m_visited.mark(a, true);
m_stack.pop_back(); m_stack.pop_back();
if (!mk_value(a)) return false; if (!mk_value(a)) return false;
} }