diff --git a/src/qe/qe_arith.cpp b/src/qe/qe_arith.cpp index 2b00efba0..e80adb40e 100644 --- a/src/qe/qe_arith.cpp +++ b/src/qe/qe_arith.cpp @@ -117,9 +117,10 @@ namespace qe { else if (extract_mod(model, t, val)) { ts.push_back(mk_mul(mul, val)); } - else if (m.is_ite(t, t1, t2, t3)) { + else if (m.is_ite(t, t1, t2, t3)) { VERIFY(model.eval(t1, val)); SASSERT(m.is_true(val) || m.is_false(val)); + TRACE("qe", tout << mk_pp(t1, m) << " := " << val << "\n";); if (m.is_true(val)) { is_linear(model, mul, t2, c, ts); } diff --git a/src/qe/qe_mbp.cpp b/src/qe/qe_mbp.cpp index cb8546b6c..3d9046a4e 100644 --- a/src/qe/qe_mbp.cpp +++ b/src/qe/qe_mbp.cpp @@ -107,6 +107,7 @@ void project_plugin::push_back(expr_ref_vector& lits, expr* e) { class mbp::impl { ast_manager& m; ptr_vector m_plugins; + expr_mark m_visited; void add_plugin(project_plugin* p) { family_id fid = p->get_family_id(); @@ -175,12 +176,48 @@ class mbp::impl { return false; } + + void extract_bools(model& model, expr_ref_vector& fmls, expr* fml) { + TRACE("qe", tout << "extract bools: " << mk_pp(fml, m) << "\n";); + ptr_vector todo; + if (is_app(fml)) { + todo.append(to_app(fml)->get_num_args(), to_app(fml)->get_args()); + } + while (!todo.empty()) { + expr* e = todo.back(); + todo.pop_back(); + if (m_visited.is_marked(e)) { + continue; + } + m_visited.mark(e); + if (m.is_bool(e)) { + expr_ref val(m); + VERIFY(model.eval(e, val)); + TRACE("qe", tout << "found: " << mk_pp(e, m) << "\n";); + if (m.is_true(val)) { + fmls.push_back(e); + } + else { + fmls.push_back(mk_not(m, e)); + } + } + else if (is_app(e)) { + todo.append(to_app(e)->get_num_args(), to_app(e)->get_args()); + } + else { + TRACE("qe", tout << "expression not handled " << mk_pp(e, m) << "\n";); + } + } + } + public: + void extract_literals(model& model, expr_ref_vector& fmls) { expr_ref val(m); for (unsigned i = 0; i < fmls.size(); ++i) { expr* fml = fmls[i].get(), *nfml, *f1, *f2, *f3; + SASSERT(m.is_bool(fml)); if (m.is_not(fml, nfml) && m.is_distinct(nfml)) { fmls[i] = project_plugin::pick_equality(m, model, nfml); --i; @@ -205,26 +242,28 @@ public: f1 = mk_not(m, f1); f2 = mk_not(m, f2); } - project_plugin::push_back(fmls, f1); + fmls[i] = f1; project_plugin::push_back(fmls, f2); - project_plugin::erase(fmls, i); + --i; } else if (m.is_implies(fml, f1, f2)) { VERIFY (model.eval(f2, val)); if (m.is_true(val)) { - project_plugin::push_back(fmls, f2); + fmls[i] = f2; } else { - project_plugin::push_back(fmls, mk_not(m, f1)); + fmls[i] = mk_not(m, f1); } - project_plugin::erase(fmls, i); + --i; } else if (m.is_ite(fml, f1, f2, f3)) { VERIFY (model.eval(f1, val)); if (m.is_true(val)) { + project_plugin::push_back(fmls, f1); project_plugin::push_back(fmls, f2); } else { + project_plugin::push_back(fmls, mk_not(m, f1)); project_plugin::push_back(fmls, f3); } project_plugin::erase(fmls, i); @@ -269,17 +308,24 @@ public: else if (m.is_not(fml, nfml) && m.is_ite(nfml, f1, f2, f3)) { VERIFY (model.eval(f1, val)); if (m.is_true(val)) { + project_plugin::push_back(fmls, f1); project_plugin::push_back(fmls, mk_not(m, f2)); } else { + project_plugin::push_back(fmls, mk_not(m, f1)); project_plugin::push_back(fmls, mk_not(m, f3)); } project_plugin::erase(fmls, i); } + else if (m.is_not(fml, nfml)) { + extract_bools(model, fmls, nfml); + } else { + extract_bools(model, fmls, fml); // TBD other Boolean operations. } } + m_visited.reset(); } impl(ast_manager& m):m(m) { @@ -310,6 +356,7 @@ public: app_ref var(m); th_rewriter rw(m); bool progress = true; + TRACE("qe", tout << vars << " " << fmls << "\n";); while (progress && !vars.empty()) { preprocess_solve(model, vars, fmls); app_ref_vector new_vars(m); @@ -345,6 +392,7 @@ public: } vars.append(new_vars); } + TRACE("qe", tout << vars << " " << fmls << "\n";); } }; diff --git a/src/qe/qsat.cpp b/src/qe/qsat.cpp index 1b0555b22..01a429038 100644 --- a/src/qe/qsat.cpp +++ b/src/qe/qsat.cpp @@ -31,6 +31,8 @@ Notes: #include "expr_abstract.h" #include "qe.h" #include "label_rewriter.h" +#include "expr_replacer.h" +#include "th_rewriter.h" namespace qe { @@ -674,16 +676,19 @@ namespace qe { is_forall = true; hoist.pull_quantifier(is_forall, fml, vars); m_vars.push_back(vars); + filter_vars(vars); } else { hoist.pull_quantifier(is_forall, fml, vars); m_vars.back().append(vars); + filter_vars(vars); } do { is_forall = !is_forall; vars.reset(); hoist.pull_quantifier(is_forall, fml, vars); m_vars.push_back(vars); + filter_vars(vars); } while (!vars.empty()); SASSERT(m_vars.back().empty()); @@ -691,6 +696,101 @@ namespace qe { TRACE("qe", tout << fml << "\n";); } + void filter_vars(app_ref_vector const& vars) { + for (unsigned i = 0; i < vars.size(); ++i) { + m_pred_abs.fmc()->insert(vars[i]->get_decl()); + } + } + +#if 0 + void hoist_ite(expr_ref& fml) { + app* ite; + scoped_ptr replace = mk_default_expr_replacer(m); + th_rewriter rewriter(m); + while (find_ite(fml, ite)) { + expr* cond, *th, *el; + VERIFY(m.is_ite(ite, cond, th, el)); + expr_ref tmp1(fml, m), tmp2(fml, m); + replace->apply_substitution(cond, m.mk_true(), tmp1); + replace->apply_substitution(cond, m.mk_false(), tmp2); + fml = m.mk_ite(cond, tmp1, tmp2); + rewriter(fml); + } + } + + bool find_ite(expr* e, app*& ite) { + ptr_vector todo; + todo.push_back(e); + ast_mark visited; + while(!todo.empty()) { + e = todo.back(); + todo.pop_back(); + if (visited.is_marked(e)) { + continue; + } + visited.mark(e, true); + if (m.is_ite(e) && !m.is_bool(e)) { + ite = to_app(e); + return true; + } + if (is_app(e)) { + app* a = to_app(e); + todo.append(a->get_num_args(), a->get_args()); + } + } + return false; + } + + // slower + void hoist_ite2(expr_ref& fml) { + obj_map result; + expr_ref_vector trail(m); + ptr_vector todo, args; + todo.push_back(fml); + + while (!todo.empty()) { + expr* e = todo.back(); + if (result.contains(e)) { + todo.pop_back(); + continue; + } + if (!is_app(e)) { + todo.pop_back(); + result.insert(e, e); + continue; + } + app* a = to_app(e); + expr* r; + unsigned sz = a->get_num_args(); + args.reset(); + for (unsigned i = 0; i < sz; ++i) { + if (result.find(a->get_arg(i), r)) { + args.push_back(r); + } + else { + todo.push_back(a->get_arg(i)); + } + } + if (sz == args.size()) { + r = m.mk_app(a->get_decl(), args.size(), args.c_ptr()); + trail.push_back(r); + if (m.is_bool(e) && m.get_basic_family_id() != a->get_family_id()) { + expr_ref fml(r, m); + hoist_ite(fml); + trail.push_back(fml); + r = fml; + } + result.insert(e, r); + todo.pop_back(); + } + } + fml = result.find(fml); + } +#endif + + + + void initialize_levels() { // initialize levels. for (unsigned i = 0; i < m_vars.size(); ++i) { @@ -941,7 +1041,7 @@ namespace qe { expr_ref_vector fmls(m); fmls.append(core.size(), core.c_ptr()); fmls.append(k.size(), k.get_formulas()); - return check_fmls(fmls); + return check_fmls(fmls) || m.canceled(); } bool check_fmls(expr_ref_vector const& fmls) { @@ -953,7 +1053,7 @@ namespace qe { lbool is_sat = solver.check(); CTRACE("qe", is_sat != l_false, tout << fmls << "\nare not unsat\n";); - return (is_sat == l_false); + return (is_sat == l_false) || m.canceled(); } bool validate_model(expr_ref_vector const& asms) { @@ -967,7 +1067,7 @@ namespace qe { bool validate_model(model& mdl, unsigned sz, expr* const* fmls) { expr_ref val(m); for (unsigned i = 0; i < sz; ++i) { - if (!m_model->eval(fmls[i], val)) { + if (!m_model->eval(fmls[i], val) && !m.canceled()) { TRACE("qe", tout << "Formula does not evaluate in model: " << mk_pp(fmls[i], m) << "\n";); return false; } @@ -1001,6 +1101,9 @@ namespace qe { TRACE("qe", tout << "Projection is false in model\n";); return false; } + if (m.canceled()) { + return true; + } for (unsigned i = 0; i < m_avars.size(); ++i) { contains_app cont(m, m_avars[i].get()); if (cont(proj)) { @@ -1029,6 +1132,7 @@ namespace qe { return true; } + public: qsat(ast_manager& m, params_ref const& p, bool qelim, bool force_elim): @@ -1070,6 +1174,8 @@ namespace qe { expr_ref fml(m); mc = 0; pc = 0; core = 0; in->get_formulas(fmls); + + fml = mk_and(m, fmls.size(), fmls.c_ptr()); // for now: @@ -1091,6 +1197,7 @@ namespace qe { fml = push_not(fml); } hoist(fml); +// hoist_ite(fml); redundant provided theories understand to deal with ite terms. m_pred_abs.abstract_atoms(fml, defs); fml = m_pred_abs.mk_abstract(fml); m_ex.assert_expr(mk_and(defs)); diff --git a/src/tactic/smtlogics/quant_tactics.cpp b/src/tactic/smtlogics/quant_tactics.cpp index f501ed75a..045b0ec87 100644 --- a/src/tactic/smtlogics/quant_tactics.cpp +++ b/src/tactic/smtlogics/quant_tactics.cpp @@ -27,6 +27,7 @@ Revision History: #include"nlqsat.h" #include"ctx_simplify_tactic.h" #include"smt_tactic.h" +#include"elim_term_ite_tactic.h" static tactic * mk_quant_preprocessor(ast_manager & m, bool disable_gaussian = false) { params_ref pull_ite_p; @@ -112,6 +113,7 @@ tactic * mk_lra_tactic(ast_manager & m, params_ref const & p) { )); #else tactic * st = and_then(mk_quant_preprocessor(m), + mk_qe_lite_tactic(m, p), or_else(mk_qsat_tactic(m, p), and_then(mk_qe_tactic(m), mk_smt_tactic()))); #endif