diff --git a/lib/pdr_context.cpp b/lib/pdr_context.cpp index dac877d02..8dbb766a9 100644 --- a/lib/pdr_context.cpp +++ b/lib/pdr_context.cpp @@ -1245,56 +1245,24 @@ namespace pdr { pt->add_cover(lvl, property); } - - class context::is_propositional_proc { - ast_manager& m; - arith_util a; - bool m_is_propositional; - public: - is_propositional_proc(ast_manager& m):m(m), a(m), m_is_propositional(true) {} - void operator()(expr* e) { - if (m_is_propositional) { - - if (!m.is_bool(e) && !a.is_int_real(e)) { - m_is_propositional = false; - } - else if (!is_app(e)) { - m_is_propositional = false; - } - else if (to_app(e)->get_num_args() > 0 && - to_app(e)->get_family_id() != m.get_basic_family_id() && - to_app(e)->get_family_id() != a.get_family_id()) { - m_is_propositional = false; - } - } - } - bool is_propositional() { return m_is_propositional; } - }; - - bool context::is_propositional(datalog::rule_set& rules) { - expr_fast_mark1 mark; - is_propositional_proc proc(m); - datalog::rule_set::iterator it = rules.begin(), end = rules.end(); - for (; proc.is_propositional() && it != end; ++it) { - quick_for_each_expr(proc, mark, (*it)->get_head()); - for (unsigned i = 0; i < (*it)->get_tail_size(); ++i) { - quick_for_each_expr(proc, mark, (*it)->get_tail(i)); - } - } - return proc.is_propositional(); - } - - class context::is_bool_proc { + class context::classifier_proc { ast_manager& m; + arith_util a; bool m_is_bool; + bool m_is_bool_arith; public: - is_bool_proc(ast_manager& m):m(m), m_is_bool(true) {} + classifier_proc(ast_manager& m, datalog::rule_set& rules): + m(m), a(m), m_is_bool(true), m_is_bool_arith(true) { + classify(rules); + } void operator()(expr* e) { - if (m_is_bool) { - + if (m_is_bool) { if (!m.is_bool(e)) { m_is_bool = false; } + else if (is_var(e)) { + // no-op. + } else if (!is_app(e)) { m_is_bool = false; } @@ -1303,22 +1271,54 @@ namespace pdr { m_is_bool = false; } } - } - bool is_bool() { return m_is_bool; } - }; - - bool context::is_bool(datalog::rule_set& rules) { - expr_fast_mark1 mark; - is_bool_proc proc(m); - datalog::rule_set::iterator it = rules.begin(), end = rules.end(); - for (; proc.is_bool() && it != end; ++it) { - quick_for_each_expr(proc, mark, (*it)->get_head()); - for (unsigned i = 0; i < (*it)->get_tail_size(); ++i) { - quick_for_each_expr(proc, mark, (*it)->get_tail(i)); + if (m_is_bool_arith) { + if (!m.is_bool(e) && !a.is_int_real(e)) { + m_is_bool_arith = false; + } + else if (is_var(e)) { + // no-op + } + else if (!is_app(e)) { + m_is_bool_arith = false; + } + else if (to_app(e)->get_num_args() > 0 && + to_app(e)->get_family_id() != m.get_basic_family_id() && + to_app(e)->get_family_id() != a.get_family_id()) { + m_is_bool_arith = false; + } } } - return proc.is_bool(); - } + + bool is_bool() const { return m_is_bool; } + + bool is_bool_arith() const { return m_is_bool_arith; } + + + private: + + void classify(datalog::rule_set& rules) { + expr_fast_mark1 mark; + datalog::rule_set::iterator it = rules.begin(), end = rules.end(); + for (; it != end; ++it) { + datalog::rule& r = *(*it); + classify_pred(mark, r.get_head()); + unsigned utsz = r.get_uninterpreted_tail_size(); + for (unsigned i = 0; i < utsz; ++i) { + classify_pred(mark, r.get_tail(i)); + } + for (unsigned i = utsz; i < r.get_tail_size(); ++i) { + quick_for_each_expr(*this, mark, r.get_tail(i)); + } + } + } + + void classify_pred(expr_fast_mark1& mark, app* pred) { + for (unsigned i = 0; i < pred->get_num_args(); ++i) { + quick_for_each_expr(*this, mark, pred->get_arg(i)); + } + } + }; + void context::reset_model_generalizers() { std::for_each(m_model_generalizers.begin(), m_model_generalizers.end(), delete_proc()); @@ -1327,17 +1327,16 @@ namespace pdr { void context::init_model_generalizers(datalog::rule_set& rules) { reset_model_generalizers(); - if (is_propositional(rules)) { + classifier_proc classify(m, rules); + if (classify.is_bool_arith()) { m_model_generalizers.push_back(alloc(bool_model_evaluation_generalizer, *this, m)); } else { m_model_generalizers.push_back(alloc(model_evaluation_generalizer, *this, m)); } - if (m_params.get_bool(":use-farkas-model", false)) { m_model_generalizers.push_back(alloc(model_farkas_generalizer, *this)); } - if (m_params.get_bool(":use-precondition-generalizer", false)) { m_model_generalizers.push_back(alloc(model_precond_generalizer, *this)); } @@ -1350,11 +1349,12 @@ namespace pdr { void context::init_core_generalizers(datalog::rule_set& rules) { reset_core_generalizers(); + classifier_proc classify(m, rules); if (m_params.get_bool(":use-multicore-generalizer", false)) { m_core_generalizers.push_back(alloc(core_multi_generalizer, *this)); } - if (m_params.get_bool(":use-farkas", true) && !is_bool(rules)) { - if (m_params.get_bool(":use-proofs", true)) { + if (m_params.get_bool(":use-farkas", true) && !classify.is_bool()) { + if (m_params.get_bool(":inline-proof-mode", true)) { m.toggle_proof_mode(PGM_FINE); m_fparams.m_proof_mode = PGM_FINE; m_fparams.m_arith_bound_prop = BP_NONE; diff --git a/lib/pdr_context.h b/lib/pdr_context.h index 52f280e31..3fdb067d6 100644 --- a/lib/pdr_context.h +++ b/lib/pdr_context.h @@ -324,10 +324,7 @@ namespace pdr { // Initialization - class is_propositional_proc; - bool is_propositional(datalog::rule_set& rules); - class is_bool_proc; - bool is_bool(datalog::rule_set& rules); + class classifier_proc; void init_model_generalizers(datalog::rule_set& rules); void init_core_generalizers(datalog::rule_set& rules); diff --git a/lib/pdr_dl_interface.cpp b/lib/pdr_dl_interface.cpp index 15d7755c1..900ee89c0 100644 --- a/lib/pdr_dl_interface.cpp +++ b/lib/pdr_dl_interface.cpp @@ -212,6 +212,7 @@ void dl_interface::collect_params(param_descrs& p) { "PDR: (default true) simplify clause set using slicing");); p.insert(":generate-proof-trace", CPK_BOOL, "PDR: (default false) trace for 'sat' answer as proof object"); + p.insert(":inline-proofs", CPK_BOOL, "PDR: (default true) run PDR with proof mode turned on and extract Farkas coefficients directly (instead of creating a separate proof object when extracting coefficients)"); } diff --git a/lib/pdr_util.cpp b/lib/pdr_util.cpp index d3e73a2f4..b2b54fe38 100644 --- a/lib/pdr_util.cpp +++ b/lib/pdr_util.cpp @@ -206,50 +206,49 @@ void th_rewriter_model_evaluator::check_model(ptr_vector const & formulas, m_rewriter.reset(); } - //00 -- non-visited - //01 -- X - //10 -- false - //11 -- true - -#define UNKNOWN(x) (!m1.is_marked(x) && !m2.is_marked(x)) -#define SET_UNKNOWN(x) { TRACE("pdr_verbose", tout << "unknown: " << mk_pp(x,m) << "\n";); m1.reset_mark(x); m2.reset_mark(x); } -#define IS_X(x) (!m1.is_marked(x) && m2.is_marked(x)) -#define IS_FALSE(x) (m1.is_marked(x) && !m2.is_marked(x)) -#define IS_TRUE(x) (m1.is_marked(x) && m2.is_marked(x)) -#define SET_X(x) { SASSERT(UNKNOWN(x)); m2.mark(x); } -#define SET_V(x) { SASSERT(UNKNOWN(x)); m1.mark(x); } -#define SET_FALSE(x) { SASSERT(UNKNOWN(x)); m1.mark(x); } -#define SET_TRUE(x) { SASSERT(UNKNOWN(x)); m1.mark(x); m2.mark(x); } -#define SET_BOOL(x, v) { if (v) { SET_TRUE(x); } else { SET_FALSE(x); } } -#define GET_VALUE(x) m_values.find(x) -#define SET_VALUE(x,y) { SET_V(x); TRACE("pdr_verbose", tout << mk_pp(x,m) << " " << y << "\n";); m_values.insert(x, y); } - -void ternary_model_evaluator::add_model(expr* e) { - expr* nlit, *var, *val; - rational r; - // SASSERT(UNKNOWN(e)); +bool ternary_model_evaluator::get_assignment(expr* e, expr*& var, expr*& val) { if (m.is_eq(e, var, val)) { if (!is_uninterp(var)) { std::swap(var, val); } - if (m.is_true(val) && UNKNOWN(var)) { - SET_TRUE(var); - } - else if (m.is_false(val) && UNKNOWN(var)) { - SET_FALSE(var); - } - else if (m_arith.is_numeral(val, r) && UNKNOWN(var)) { - SET_VALUE(var, r); - } - else { - TRACE("pdr_verbose", tout << "no value for " << mk_pp(val, m) << "\n";); + if (m.is_true(val) || m.is_false(val) || m_arith.is_numeral(val)) { + return true; } + TRACE("pdr_verbose", tout << "no value for " << mk_pp(val, m) << "\n";); + return false; } - else if (m.is_not(e, nlit)) { - SET_FALSE(nlit); + else if (m.is_not(e, var)) { + val = m.mk_false(); + return true; } else if (m.is_bool(e)) { - SET_TRUE(e); + val = m.mk_true(); + var = e; + return true; + } + else { + TRACE("pdr_verbose", tout << "no value set of " << mk_pp(e, m) << "\n";); + return false; + } +} + + +void ternary_model_evaluator::add_model(expr* e) { + expr* var, *val; + rational r; + // SASSERT(is_unknown(e)); + if (get_assignment(e, var, val)) { + if (is_unknown(var)) { + if (m.is_true(val)) { + set_true(var); + } + else if (m.is_false(val)) { + set_false(var); + } + else if (m_arith.is_numeral(val, r)) { + set_value(var, r); + } + } } else { TRACE("pdr_verbose", tout << "no value set of " << mk_pp(e, m) << "\n";); @@ -257,19 +256,12 @@ void ternary_model_evaluator::add_model(expr* e) { } void ternary_model_evaluator::del_model(expr* e) { - expr* nlit, *var, *val; - if (m.is_eq(e, var, val)) { - if (!is_uninterp(var)) { - std::swap(var, val); + expr *var, *val; + if (get_assignment(e, var, val)) { + set_unknown(var); + if (!m.is_bool(var)) { + m_values.remove(var); } - SET_UNKNOWN(var); - m_values.remove(var); - } - else if (m.is_not(e, nlit)) { - SET_UNKNOWN(nlit); - } - else if (m.is_bool(e)) { - SET_UNKNOWN(e); } else { TRACE("pdr_verbose", tout << "no value set of " << mk_pp(e, m) << "\n";); @@ -280,7 +272,7 @@ void ternary_model_evaluator::setup_model(expr_ref_vector const& model) { m_values.reset(); for (unsigned i = 0; i < model.size(); ++i) { expr* e = model[i]; - if (UNKNOWN(e)) { + if (is_unknown(e)) { add_model(e); } } @@ -297,6 +289,19 @@ void ternary_model_evaluator::minimize_model(ptr_vector const & formulas, tout << "formulas\n"; for (unsigned i = 0; i < formulas.size(); ++i) tout << mk_pp(formulas[i], m) << "\n"; ); + + prune_cone_of_influence(formulas, model); + + // prune_by_probing(formulas, model); + + m1.reset(); + m2.reset(); + m_values.reset(); +} + + +void ternary_model_evaluator::prune_by_probing(ptr_vector const& formulas, expr_ref_vector& model) { + unsigned sz1 = model.size(); for (unsigned i = 0; i < model.size(); ) { expr_ref removed(model[i].get(), m); if (i + 1 < model.size()) { @@ -308,10 +313,10 @@ void ternary_model_evaluator::minimize_model(ptr_vector const & formulas, m2.set_level(m_level2); bool formulas_hold = check_model(formulas); + m1.set_level(m_level1); m2.set_level(m_level2); - - + if (!formulas_hold) { // if we introduced unknown, we restore the removed element add_model(removed); @@ -327,9 +332,134 @@ void ternary_model_evaluator::minimize_model(ptr_vector const & formulas, i++; } } - m1.reset(); - m2.reset(); - m_values.reset(); + TRACE("pdr", tout << sz1 << " ==> " << model.size() << "\n";); +} + +void ternary_model_evaluator::prune_cone_of_influence(ptr_vector const & formulas, expr_ref_vector& model) { + ptr_vector todo, tocollect; + todo.append(formulas); + m_visited.reset(); + m1.set_level(m_level1); + m2.set_level(m_level2); + + VERIFY(check_model(formulas)); + + while (!todo.empty()) { + app* e = to_app(todo.back()); + todo.pop_back(); + if (m_visited.is_marked(e)) { + continue; + } + unsigned v = is_true(e); + SASSERT(m.is_bool(e)); + SASSERT(is_true(e) || is_false(e)); + unsigned sz = e->get_num_args(); + expr* const* args = e->get_args(); + if (e->get_family_id() == m.get_basic_family_id()) { + switch(e->get_decl_kind()) { + case OP_TRUE: + break; + case OP_FALSE: + break; + case OP_EQ: + case OP_IFF: + if (e->get_arg(0) == e->get_arg(1)) { + break; + } + if (!m.is_bool(e->get_arg(0))) { + tocollect.push_back(e); + break; + } + todo.append(sz, args); + break; + + case OP_DISTINCT: + tocollect.push_back(e); + break; + case OP_ITE: + if (e->get_arg(1) == e->get_arg(2)) { + break; + } + todo.push_back(args[0]); + if (is_true(args[0])) { + todo.push_back(args[1]); + } + else { + SASSERT(is_false(args[0])); + todo.push_back(args[2]); + } + break; + case OP_AND: + if (v) { + todo.append(sz, args); + } + else { + unsigned i = 0; + for (; !is_false(args[i]) && i < sz; ++i); + SASSERT(i < sz); + todo.push_back(args[i]); + } + break; + case OP_OR: + if (v) { + unsigned i = 0; + for (; !is_true(args[i]) && i < sz; ++i); + SASSERT(i < sz); + todo.push_back(args[i]); + } + else { + todo.append(sz, args); + } + break; + case OP_XOR: + case OP_NOT: + todo.append(sz, args); + break; + case OP_IMPLIES: + if (v) { + if (is_true(args[1])) { + todo.push_back(args[1]); + } + else if (is_false(args[0])) { + todo.push_back(args[0]); + } + else { + UNREACHABLE(); + } + } + else { + todo.append(sz, args); + } + break; + default: + UNREACHABLE(); + } + } + else { + tocollect.push_back(e); + } + m_visited.mark(e, true); + } + m1.set_level(m_level1); + m2.set_level(m_level2); + m_visited.reset(); + for (unsigned i = 0; i < tocollect.size(); ++i) { + for_each_expr(*this, m_visited, tocollect[i]); + } + unsigned sz1 = model.size(); + for (unsigned i = 0; i < model.size(); ++i) { + expr* e = model[i].get(), *var, *val; + if (get_assignment(e, var, val)) { + if (!m_visited.is_marked(var)) { + del_model(e); + model[i] = model.back(); + model.pop_back(); + --i; + } + } + } + m_visited.reset(); + TRACE("pdr", tout << sz1 << " ==> " << model.size() << "\n";); } @@ -353,7 +483,7 @@ bool ternary_model_evaluator::check_model(ptr_vector const& formulas) { #define ARG1 curr->get_arg(0) #define ARG2 curr->get_arg(1) - if (!UNKNOWN(curr)) { + if (!is_unknown(curr)) { todo.pop_back(); continue; } @@ -363,16 +493,16 @@ bool ternary_model_evaluator::check_model(ptr_vector const& formulas) { bool all_set = true, some_x = false; for (unsigned i = 0; !some_x && i < arity; ++i) { expr* arg = curr->get_arg(i); - if (UNKNOWN(arg)) { + if (is_unknown(arg)) { todo.push_back(arg); all_set = false; } - else if (IS_X(arg)) { + else if (is_x(arg)) { some_x = true; } } if (some_x) { - SET_X(curr); + set_x(curr); } else if (!all_set) { continue; @@ -381,105 +511,105 @@ bool ternary_model_evaluator::check_model(ptr_vector const& formulas) { switch(curr->get_decl_kind()) { case OP_NUM: VERIFY(m_arith.is_numeral(curr,r)); - SET_VALUE(curr, r); + set_value(curr, r); break; case OP_IRRATIONAL_ALGEBRAIC_NUM: - SET_X(curr); + set_x(curr); break; case OP_LE: - SET_BOOL(curr, GET_VALUE(ARG1) <= GET_VALUE(ARG2)); + set_bool(curr, get_value(ARG1) <= get_value(ARG2)); break; case OP_GE: - SET_BOOL(curr, GET_VALUE(ARG1) >= GET_VALUE(ARG2)); + set_bool(curr, get_value(ARG1) >= get_value(ARG2)); break; case OP_LT: - SET_BOOL(curr, GET_VALUE(ARG1) < GET_VALUE(ARG2)); + set_bool(curr, get_value(ARG1) < get_value(ARG2)); break; case OP_GT: - SET_BOOL(curr, GET_VALUE(ARG1) > GET_VALUE(ARG2)); + set_bool(curr, get_value(ARG1) > get_value(ARG2)); break; case OP_ADD: r = rational::zero(); for (unsigned i = 0; i < arity; ++i) { - r += GET_VALUE(curr->get_arg(i)); + r += get_value(curr->get_arg(i)); } - SET_VALUE(curr, r); + set_value(curr, r); break; case OP_SUB: - r = GET_VALUE(curr->get_arg(0)); + r = get_value(curr->get_arg(0)); for (unsigned i = 1; i < arity; ++i) { - r -= GET_VALUE(curr->get_arg(i)); + r -= get_value(curr->get_arg(i)); } - SET_VALUE(curr, r); + set_value(curr, r); break; case OP_UMINUS: SASSERT(arity == 1); - SET_VALUE(curr, GET_VALUE(curr->get_arg(0))); + set_value(curr, get_value(curr->get_arg(0))); break; case OP_MUL: r = rational::one(); for (unsigned i = 0; i < arity; ++i) { - r *= GET_VALUE(curr->get_arg(i)); + r *= get_value(curr->get_arg(i)); } - SET_VALUE(curr, r); + set_value(curr, r); break; case OP_DIV: SASSERT(arity == 2); - r = GET_VALUE(ARG2); + r = get_value(ARG2); if (r.is_zero()) { - SET_X(curr); + set_x(curr); } else { - SET_VALUE(curr, GET_VALUE(ARG1) / r); + set_value(curr, get_value(ARG1) / r); } break; case OP_IDIV: SASSERT(arity == 2); - r = GET_VALUE(ARG2); + r = get_value(ARG2); if (r.is_zero()) { - SET_X(curr); + set_x(curr); } else { - SET_VALUE(curr, div(GET_VALUE(ARG1), r)); + set_value(curr, div(get_value(ARG1), r)); } break; case OP_REM: // rem(v1,v2) = if v2 >= 0 then mod(v1,v2) else -mod(v1,v2) SASSERT(arity == 2); - r = GET_VALUE(ARG2); + r = get_value(ARG2); if (r.is_zero()) { - SET_X(curr); + set_x(curr); } else { - r2 = mod(GET_VALUE(ARG1), r); + r2 = mod(get_value(ARG1), r); if (r.is_neg()) r2.neg(); - SET_VALUE(curr, r2); + set_value(curr, r2); } break; case OP_MOD: SASSERT(arity == 2); - r = GET_VALUE(ARG2); + r = get_value(ARG2); if (r.is_zero()) { - SET_X(curr); + set_x(curr); } else { - SET_VALUE(curr, mod(GET_VALUE(ARG1), r)); + set_value(curr, mod(get_value(ARG1), r)); } break; case OP_TO_REAL: SASSERT(arity == 1); - SET_VALUE(curr, GET_VALUE(ARG1)); + set_value(curr, get_value(ARG1)); break; case OP_TO_INT: SASSERT(arity == 1); - SET_VALUE(curr, floor(GET_VALUE(ARG1))); + set_value(curr, floor(get_value(ARG1))); break; case OP_IS_INT: SASSERT(arity == 1); - SET_BOOL(curr, GET_VALUE(ARG1).is_int()); + set_bool(curr, get_value(ARG1).is_int()); break; case OP_POWER: - SET_X(curr); + set_x(curr); break; default: UNREACHABLE(); @@ -496,213 +626,217 @@ bool ternary_model_evaluator::check_model(ptr_vector const& formulas) { // we're adding unknowns on the top of the todo stack, if there is none added, // all arguments were known bool has_x = false, has_false = false; + unsigned sz = todo.size(); for (unsigned j = 0; !has_false && j < arity; ++j) { expr * arg = curr->get_arg(j); - if (IS_FALSE(arg)) { + if (is_false(arg)) { has_false = true; } - else if (IS_X(arg)) { + else if (is_x(arg)) { has_x = true; } - else if (UNKNOWN(arg)) { + else if (is_unknown(arg)) { todo.push_back(arg); } } if (has_false) { - SET_FALSE(curr); + todo.resize(sz); + set_false(curr); } else { if (todo.back() != curr) { continue; } else if (has_x) { - SET_X(curr); + set_x(curr); } else { - SET_TRUE(curr); + set_true(curr); } } } else if (m.is_or(curr)) { bool has_x = false, has_true = false; + unsigned sz = todo.size(); for (unsigned j = 0; !has_true && j < arity; ++j) { expr * arg = curr->get_arg(j); - if (IS_TRUE(arg)) { + if (is_true(arg)) { has_true = true; } - else if (IS_X(arg)) { + else if (is_x(arg)) { has_x = true; } - else if (UNKNOWN(arg)) { + else if (is_unknown(arg)) { todo.push_back(arg); } } if (has_true) { - SET_TRUE(curr); + todo.resize(sz); + set_true(curr); } else { if (todo.back() != curr) { continue; } else if (has_x) { - SET_X(curr); + set_x(curr); } else { - SET_FALSE(curr); + set_false(curr); } } } else if (m.is_not(curr, arg)) { - if (UNKNOWN(arg)) { + if (is_unknown(arg)) { todo.push_back(arg); continue; } - if (IS_TRUE(arg)) { - SET_FALSE(curr); + if (is_true(arg)) { + set_false(curr); } - else if (IS_FALSE(arg)) { - SET_TRUE(curr); + else if (is_false(arg)) { + set_true(curr); } else { - SASSERT(IS_X(arg)); - SET_X(curr); + SASSERT(is_x(arg)); + set_x(curr); } } else if (m.is_implies(curr, arg1, arg2)) { - if (IS_FALSE(arg1) || IS_TRUE(arg2)) { - SET_TRUE(curr); + if (is_false(arg1) || is_true(arg2)) { + set_true(curr); } - else if (UNKNOWN(arg1) || UNKNOWN(arg2)) { - if (UNKNOWN(arg1)) { todo.push_back(arg1); } - if (UNKNOWN(arg2)) { todo.push_back(arg2); } + else if (is_unknown(arg1) || is_unknown(arg2)) { + if (is_unknown(arg1)) { todo.push_back(arg1); } + if (is_unknown(arg2)) { todo.push_back(arg2); } continue; } - else if (IS_TRUE(arg1) && IS_FALSE(arg2)) { - SET_FALSE(curr); + else if (is_true(arg1) && is_false(arg2)) { + set_false(curr); } else { - SASSERT(IS_X(arg1) || IS_X(arg2)); - SET_X(curr); + SASSERT(is_x(arg1) || is_x(arg2)); + set_x(curr); } } else if (m.is_iff(curr, arg1, arg2) || (m.is_eq(curr, arg1, arg2) && m.is_bool(arg1))) { - if (IS_X(arg1) || IS_X(arg2)) { - SET_X(curr); + if (is_x(arg1) || is_x(arg2)) { + set_x(curr); } - else if (UNKNOWN(arg1) || UNKNOWN(arg2)) { - if (UNKNOWN(arg1)) { todo.push_back(arg1); } - if (UNKNOWN(arg2)) { todo.push_back(arg2); } + else if (is_unknown(arg1) || is_unknown(arg2)) { + if (is_unknown(arg1)) { todo.push_back(arg1); } + if (is_unknown(arg2)) { todo.push_back(arg2); } continue; } else { - bool val = IS_TRUE(arg1)==IS_TRUE(arg2); - SASSERT(val == (IS_FALSE(arg1)==IS_FALSE(arg2))); + bool val = is_true(arg1)==is_true(arg2); + SASSERT(val == (is_false(arg1)==is_false(arg2))); if (val) { - SET_TRUE(curr); + set_true(curr); } else { - SET_FALSE(curr); + set_false(curr); } } } else if (m.is_ite(curr, argCond, argThen, argElse) && m.is_bool(argThen)) { - if (IS_TRUE(argCond)) { - if (IS_TRUE(argThen)) { SET_TRUE(curr); } - else if (IS_FALSE(argThen)) { SET_FALSE(curr); } - else if (IS_X(argThen)) { SET_X(curr); } + if (is_true(argCond)) { + if (is_true(argThen)) { set_true(curr); } + else if (is_false(argThen)) { set_false(curr); } + else if (is_x(argThen)) { set_x(curr); } else { todo.push_back(argThen); continue; } } - else if (IS_FALSE(argCond)) { - if (IS_TRUE(argElse)) { SET_TRUE(curr); } - else if (IS_FALSE(argElse)) { SET_FALSE(curr); } - else if (IS_X(argElse)) { SET_X(curr); } + else if (is_false(argCond)) { + if (is_true(argElse)) { set_true(curr); } + else if (is_false(argElse)) { set_false(curr); } + else if (is_x(argElse)) { set_x(curr); } else { todo.push_back(argElse); continue; } } - else if (IS_TRUE(argThen) && IS_TRUE(argElse)) { - SET_TRUE(curr); + else if (is_true(argThen) && is_true(argElse)) { + set_true(curr); } - else if (IS_FALSE(argThen) && IS_FALSE(argElse)) { - SET_FALSE(curr); + else if (is_false(argThen) && is_false(argElse)) { + set_false(curr); } - else if (IS_X(argCond) && (IS_X(argThen) || IS_X(argElse)) ) { - SET_X(curr); - } else if (UNKNOWN(argCond) || UNKNOWN(argThen) || UNKNOWN(argElse)) { - if (UNKNOWN(argCond)) { todo.push_back(argCond); } - if (UNKNOWN(argThen)) { todo.push_back(argThen); } - if (UNKNOWN(argElse)) { todo.push_back(argElse); } + else if (is_x(argCond) && (is_x(argThen) || is_x(argElse)) ) { + set_x(curr); + } else if (is_unknown(argCond) || is_unknown(argThen) || is_unknown(argElse)) { + if (is_unknown(argCond)) { todo.push_back(argCond); } + if (is_unknown(argThen)) { todo.push_back(argThen); } + if (is_unknown(argElse)) { todo.push_back(argElse); } continue; } else { - SASSERT(IS_X(argCond)); - SASSERT((IS_TRUE(argThen) && IS_FALSE(argElse)) || - (IS_FALSE(argThen) && IS_TRUE(argElse))); - SET_X(curr); + SASSERT(is_x(argCond)); + SASSERT((is_true(argThen) && is_false(argElse)) || + (is_false(argThen) && is_true(argElse))); + set_x(curr); } } else if (m.is_true(curr)) { - SET_TRUE(curr); + set_true(curr); } else if (m.is_false(curr)) { - SET_FALSE(curr); + set_false(curr); } else if (m.is_eq(curr, arg1, arg2) && arg1 == arg2) { - SET_TRUE(curr); + set_true(curr); } else if (m.is_eq(curr, arg1, arg2)) { - if (UNKNOWN(arg1)) { + if (is_unknown(arg1)) { todo.push_back(arg1); } - if (UNKNOWN(arg2)) { + if (is_unknown(arg2)) { todo.push_back(arg2); } if (curr != todo.back()) { continue; } - if (IS_X(arg1) || IS_X(arg2)) { - SET_X(curr); + if (is_x(arg1) || is_x(arg2)) { + set_x(curr); } else { - SET_BOOL(curr, GET_VALUE(arg1) == GET_VALUE(arg2)); + set_bool(curr, get_value(arg1) == get_value(arg2)); } } else if (m.is_ite(curr, argCond, argThen, argElse) && m_arith.is_int_real(argThen)) { - if (IS_TRUE(argCond) || (argThen == argElse)) { - if (UNKNOWN(argThen)) { + if (is_true(argCond) || (argThen == argElse)) { + if (is_unknown(argThen)) { todo.push_back(argThen); continue; } - if (IS_X(argThen)) { - SET_X(curr); + if (is_x(argThen)) { + set_x(curr); } else { - SET_VALUE(curr, GET_VALUE(argThen)); + set_value(curr, get_value(argThen)); } } - else if (IS_FALSE(argCond)) { - if (UNKNOWN(argElse)) { + else if (is_false(argCond)) { + if (is_unknown(argElse)) { todo.push_back(argElse); continue; } - if (IS_X(argElse)) { - SET_X(curr); + if (is_x(argElse)) { + set_x(curr); } else { - SET_VALUE(curr, GET_VALUE(argElse)); + set_value(curr, get_value(argElse)); } } - else if (UNKNOWN(argCond)) { + else if (is_unknown(argCond)) { todo.push_back(argCond); continue; } else { - SET_X(curr); + set_x(curr); } } else { @@ -711,27 +845,27 @@ bool ternary_model_evaluator::check_model(ptr_vector const& formulas) { } else { TRACE("pdr_verbse", tout << "Not evaluated " << mk_pp(curr, m) << "\n";); - SET_X(curr); + set_x(curr); } IF_VERBOSE(35,verbose_stream() << "assigned "< const & formulas, expr_ref_vector& model); + void prune_by_probing(ptr_vector const & formulas, expr_ref_vector& model); + + //00 -- non-visited + //01 -- X + //10 -- false + //11 -- true + inline bool is_unknown(expr* x) { return !m1.is_marked(x) && !m2.is_marked(x); } + inline void set_unknown(expr* x) { m1.reset_mark(x); m2.reset_mark(x); } + inline bool is_x(expr* x) { return !m1.is_marked(x) && m2.is_marked(x); } + inline bool is_false(expr* x) { return m1.is_marked(x) && !m2.is_marked(x); } + inline bool is_true(expr* x) { return m1.is_marked(x) && m2.is_marked(x); } + inline void set_x(expr* x) { SASSERT(is_unknown(x)); m2.mark(x); } + inline void set_v(expr* x) { SASSERT(is_unknown(x)); m1.mark(x); } + inline void set_false(expr* x) { SASSERT(is_unknown(x)); m1.mark(x); } + inline void set_true(expr* x) { SASSERT(is_unknown(x)); m1.mark(x); m2.mark(x); } + inline void set_bool(expr* x, bool v) { if (v) { set_true(x); } else { set_false(x); } } + inline rational const& get_value(expr* x) const { return m_values.find(x); } + inline void set_value(expr* x, rational const& v) { set_v(x); TRACE("pdr_verbose", tout << mk_pp(x,m) << " " << v << "\n";); m_values.insert(x,v); } + protected: bool check_model(ptr_vector const & formulas); @@ -222,6 +245,8 @@ protected: public: ternary_model_evaluator(ast_manager& m) : m(m), m_arith(m), m_bv(m) {} virtual void minimize_model(ptr_vector const & formulas, expr_ref_vector & model); + + void operator()(expr* e) { m_visited.mark(e, true); } }; void get_value_from_model(const model_core & mdl, func_decl * f, expr_ref& res);