From ff4b9daf1a9ae7df4332a8f724d7531368466980 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sun, 28 Oct 2012 17:55:11 -0700 Subject: [PATCH] fix solution generation for quantified integer arithmetic. Added unit tests Signed-off-by: Nikolaj Bjorner --- src/muz_qe/qe.cpp | 239 +++++++++++++++-------------- src/muz_qe/qe.h | 37 ++++- src/muz_qe/qe_arith_plugin.cpp | 138 ++++++++++------- src/muz_qe/qe_datatype_plugin.cpp | 28 +++- src/test/dead/qe_defs.cpp | 87 ----------- src/test/quant_solve.cpp | 241 +++++++++++++++++++----------- 6 files changed, 418 insertions(+), 352 deletions(-) delete mode 100644 src/test/dead/qe_defs.cpp diff --git a/src/muz_qe/qe.cpp b/src/muz_qe/qe.cpp index 2c384596d..6bda83d32 100644 --- a/src/muz_qe/qe.cpp +++ b/src/muz_qe/qe.cpp @@ -45,6 +45,7 @@ Revision History: #include "cooperate.h" #include "tactical.h" #include "model_v2_pp.h" +#include "obj_hashtable.h" namespace qe { @@ -723,6 +724,85 @@ namespace qe { } }; + // ---------------------------- + // def_vector + + void def_vector::normalize() { + // apply nested definitions into place. + ast_manager& m = m_vars.get_manager(); + expr_substitution sub(m); + scoped_ptr rep = mk_expr_simp_replacer(m); + if (size() <= 1) { + return; + } + for (unsigned i = size(); i > 0; ) { + --i; + expr_ref e(m); + e = def(i); + rep->set_substitution(&sub); + (*rep)(e); + sub.insert(m.mk_const(var(i)), e); + def_ref(i) = e; + } + } + + void def_vector::project(unsigned num_vars, app* const* vars) { + obj_hashtable fns; + for (unsigned i = 0; i < num_vars; ++i) { + fns.insert(vars[i]->get_decl()); + } + for (unsigned i = 0; i < size(); ++i) { + if (fns.contains(m_vars[i].get())) { + // + // retain only first occurrence of eliminated variable. + // later occurrences are just recycling the name. + // + fns.remove(m_vars[i].get()); + } + else { + for (unsigned j = i+1; j < size(); ++j) { + m_vars[j-1] = m_vars[j]; + m_defs[j-1] = m_defs[j]; + } + m_vars.pop_back(); + m_defs.pop_back(); + --i; + } + } + } + + // ---------------------------- + // guarded_defs + + std::ostream& guarded_defs::display(std::ostream& out) const { + ast_manager& m = m_guards.get_manager(); + for (unsigned i = 0; i < size(); ++i) { + for (unsigned j = 0; j < defs(i).size(); ++j) { + out << defs(i).var(j)->get_name() << " := " << mk_pp(defs(i).def(j), m) << "\n"; + } + out << "if " << mk_pp(guard(i), m) << "\n"; + } + return out; + } + + bool guarded_defs::inv() { + return m_defs.size() == m_guards.size(); + } + + void guarded_defs::add(expr* guard, def_vector const& defs) { + SASSERT(inv()); + m_defs.push_back(defs); + m_guards.push_back(guard); + m_defs.back().normalize(); + SASSERT(inv()); + } + + void guarded_defs::project(unsigned num_vars, app* const* vars) { + for (unsigned i = 0; i < size(); ++i) { + m_defs[i].project(num_vars, vars); + } + } + // ---------------------------- // Obtain atoms in NNF formula. @@ -810,7 +890,7 @@ namespace qe { virtual lbool eliminate_exists( unsigned num_vars, app* const* vars, - expr_ref& fml, app_ref_vector& free_vars, bool get_first, def_vector* defs) = 0; + expr_ref& fml, app_ref_vector& free_vars, bool get_first, guarded_defs* defs) = 0; virtual void set_assumption(expr* fml) = 0; @@ -918,40 +998,25 @@ namespace qe { } } - bool get_leaf_rec(expr_ref& fml, def_vector& defs) { + void get_leaves_rec(def_vector& defs, guarded_defs& gdefs) { expr* f = this->fml(); + unsigned sz = defs.size(); + defs.append(def()); if (m_children.empty() && f && !m.is_false(f) && m_vars.empty() && !has_var()) { - fml = f; - return true; + gdefs.add(f, defs); } - unsigned sz = defs.size(); - for (unsigned i = 0; i < m_children.size(); ++i) { - search_tree* st = m_children[i]; - defs.append(st->def()); - if (st->get_leaf_rec(fml, defs)) { - return true; + else { + for (unsigned i = 0; i < m_children.size(); ++i) { + m_children[i]->get_leaves_rec(defs, gdefs); } - defs.shrink(sz); } - return false; + defs.shrink(sz); } - void get_leaf(expr_ref& fml, def_vector& defs) { - get_leaf_rec(fml, defs); - - // apply nested definitions into place. - expr_substitution sub(m); - scoped_ptr rep = mk_expr_simp_replacer(m); - for (unsigned i = defs.size(); i > 0; ) { - --i; - expr_ref e(m); - e = defs.def(i); - rep->set_substitution(&sub); - (*rep)(e); - sub.insert(m.mk_const(defs.var(i)), e); - defs.def_ref(i) = e; - } + void get_leaves(guarded_defs& gdefs) { + def_vector defs(m); + get_leaves_rec(defs, gdefs); } void reset() { @@ -1248,7 +1313,7 @@ namespace qe { app_ref_vector m_new_vars; // variables added by solvers bool m_get_first; // get first satisfying branch. - def_vector* m_defs; + guarded_defs* m_defs; nnf_normalizer m_nnf; // nnf conversion @@ -1311,7 +1376,7 @@ namespace qe { void check(unsigned num_vars, app* const* vars, expr* assumption, expr_ref& fml, bool get_first, - app_ref_vector& free_vars, def_vector* defs) { + app_ref_vector& free_vars, guarded_defs* defs) { reset(); m_solver.push(); @@ -1366,9 +1431,11 @@ namespace qe { expr_ref_vector result(m); m_root.get_leaves(result); m_bool_rewriter.mk_or(result.size(), result.c_ptr(), fml); - } - else if (defs) { - m_root.get_leaf(fml, *defs); + } + + if (defs) { + m_root.get_leaves(*defs); + defs->project(num_vars, vars); } TRACE("qe", @@ -1401,7 +1468,7 @@ namespace qe { private: void final_check(model_evaluator& model_eval) { - TRACE("qe", tout << (m_fml?"fml":"null") << "\n";); + TRACE("qe", tout << "\n";); while (can_propagate_assignment(model_eval)) { propagate_assignment(model_eval); } @@ -1480,7 +1547,7 @@ namespace qe { m_qe.eliminate_exists(1, &var, fml, m_free_vars, false, 0); } - lbool eliminate_exists(unsigned num_vars, app* const* vars, expr_ref& fml, bool get_first, def_vector* defs) { + lbool eliminate_exists(unsigned num_vars, app* const* vars, expr_ref& fml, bool get_first, guarded_defs* defs) { return m_qe.eliminate_exists(num_vars, vars, fml, m_free_vars, get_first, defs); } @@ -1700,7 +1767,7 @@ namespace qe { void propagate_assignment(model_evaluator& model_eval) { if (m_fml) { - update_current(model_eval, true); + update_status st = update_current(model_eval, true); } } @@ -1982,7 +2049,7 @@ namespace qe { virtual lbool eliminate_exists( unsigned num_vars, app* const* vars, expr_ref& fml, - app_ref_vector& free_vars, bool get_first, def_vector* defs) { + app_ref_vector& free_vars, bool get_first, guarded_defs* defs) { if (get_first) { return eliminate_block(num_vars, vars, fml, free_vars, get_first, defs); } @@ -2008,7 +2075,7 @@ namespace qe { lbool eliminate_block( unsigned num_vars, app* const* vars, expr_ref& fml, - app_ref_vector& free_vars, bool get_first, def_vector* defs) { + app_ref_vector& free_vars, bool get_first, guarded_defs* defs) { checkpoint(); @@ -2094,54 +2161,6 @@ namespace qe { }; - - -#if 0 - // - // Instantiation based quantifier elimination procedure. - // try a few loops of checking satisfiability. - // substitute in model values for bound variables. - // - class quant_elim_inst : public quant_elim { - ast_manager& - public: - quant_elim_inst(ast_manager& m): m(m) {} - - virtual lbool eliminate_exists( - unsigned num_vars, app* const* vars, - expr_ref& fml, app_ref_vector& free_vars, bool get_first, def_vector* defs) { - - } - - virtual void set_assumption(expr* fml) {} - - virtual void collect_statistics(statistics & st) const { - m_solver.collect_statistics(st); - } - - virtual void eliminate(bool is_forall, unsigned num_vars, app* const* vars, expr_ref& fml) { - if (is_forall) { - fml = m.mk_not(fml); - r = eliminate_exists(num_vars, vars, fml, free_vars, false, defs); - fml = m.mk_not(fml); - } - else { - r = eliminate_exists(num_vars, vars, fml, free_vars, false, defs); - } - } - - virtual void set_cancel(bool f) { - m_solver.set_cancel(f); - } - - virtual void updt_params(params_ref const& p) { - m_solver.updt_params(p); - } - - }; -#endif - - // ------------------------------------------------ // expr_quant_elim @@ -2310,40 +2329,28 @@ namespace qe { lbool expr_quant_elim::first_elim(unsigned num_vars, app* const* vars, expr_ref& fml, def_vector& defs) { app_ref_vector fvs(m); init_qe(); - return m_qe->eliminate_exists(num_vars, vars, fml, fvs, true, &defs); - } - - bool expr_quant_elim::solve_for_var(app* var, expr* _fml, expr_ref_vector& terms, expr_ref_vector& fmls) { - expr_ref assms(m.mk_true(), m); - func_decl* v = var->get_decl(); - init_qe(); - while (true) { - def_vector defs(m); - app_ref_vector fvs(m); - m_qe->set_assumption(assms); - expr_ref fml(_fml, m); - lbool is_sat = m_qe->eliminate_exists(1, &var, fml, fvs, true, &defs); - switch (is_sat) { - case l_false: return true; - case l_undef: return false; - default: break; - } - bool found = false; - for (unsigned i = 0; !found && i < defs.size(); ++i) { - if (defs.var(i) == v) { - terms.push_back(defs.def(i)); - fmls.push_back(fml); - found = true; - } - } - if (!found) { - NOT_IMPLEMENTED_YET(); - } - assms = m.mk_and(assms, m.mk_not(fml)); + guarded_defs gdefs(m); + lbool res = m_qe->eliminate_exists(num_vars, vars, fml, fvs, true, &gdefs); + if (gdefs.size() > 0) { + defs.reset(); + defs.append(gdefs.defs(0)); + fml = gdefs.guard(0); } - return true; + return res; } + bool expr_quant_elim::solve_for_var(app* var, expr* fml, guarded_defs& defs) { + return solve_for_vars(1,&var, fml, defs); + } + + bool expr_quant_elim::solve_for_vars(unsigned num_vars, app* const* vars, expr* _fml, guarded_defs& defs) { + app_ref_vector fvs(m); + expr_ref fml(_fml, m); + TRACE("qe", tout << mk_pp(fml, m) << "\n";); + init_qe(); + lbool is_sat = m_qe->eliminate_exists(num_vars, vars, fml, fvs, false, &defs); + return is_sat != l_undef; + } void expr_quant_elim::set_cancel(bool f) { if (m_qe) { diff --git a/src/muz_qe/qe.h b/src/muz_qe/qe.h index 4a444ac26..4ca098f73 100644 --- a/src/muz_qe/qe.h +++ b/src/muz_qe/qe.h @@ -226,8 +226,10 @@ namespace qe { class def_vector { func_decl_ref_vector m_vars; expr_ref_vector m_defs; + def_vector& operator=(def_vector const& other); public: def_vector(ast_manager& m): m_vars(m), m_defs(m) {} + def_vector(def_vector const& other): m_vars(other.m_vars), m_defs(other.m_defs) {} void push_back(func_decl* v, expr* e) { m_vars.push_back(v); m_defs.push_back(e); @@ -240,6 +242,33 @@ namespace qe { func_decl* var(unsigned i) const { return m_vars[i]; } expr* def(unsigned i) const { return m_defs[i]; } expr_ref_vector::element_ref def_ref(unsigned i) { return m_defs[i]; } + void normalize(); + void project(unsigned num_vars, app* const* vars); + }; + + /** + \brief Guarded definitions. + + A realizer to a an existential quantified formula is a disjunction + together with a substitution from the existentially quantified variables + to terms such that: + 1. The original formula (exists (vars) fml) is equivalent to the disjunction of guards. + 2. Each guard is equivalent to fml where 'vars' are replaced by the substitution associated + with the guard. + */ + + class guarded_defs { + expr_ref_vector m_guards; + vector m_defs; + bool inv(); + public: + guarded_defs(ast_manager& m): m_guards(m) { SASSERT(inv()); } + void add(expr* guard, def_vector const& defs); + unsigned size() const { return m_guards.size(); } + def_vector const& defs(unsigned i) const { return m_defs[i]; } + expr* guard(unsigned i) const { return m_guards[i]; } + std::ostream& display(std::ostream& out) const; + void project(unsigned num_vars, app* const* vars); }; class quant_elim; @@ -277,10 +306,12 @@ namespace qe { \brief solve for (exists (var) fml). Return false if operation failed. Return true and list of pairs (t_i, fml_i) in - such that fml[t_1] \/ ... \/ fml[t_n] == (exists (var) fml) - and fml_i == fml[t_1] + such that fml_1 \/ ... \/ fml_n == (exists (var) fml) + and fml_i => fml[t_i] */ - bool solve_for_var(app* var, expr* fml, expr_ref_vector& terms, expr_ref_vector& fmls); + bool solve_for_var(app* var, expr* fml, guarded_defs& defs); + + bool solve_for_vars(unsigned num_vars, app* const* vars, expr* fml, guarded_defs& defs); void set_cancel(bool f); diff --git a/src/muz_qe/qe_arith_plugin.cpp b/src/muz_qe/qe_arith_plugin.cpp index 0dc1a63e2..f8fe967c0 100644 --- a/src/muz_qe/qe_arith_plugin.cpp +++ b/src/muz_qe/qe_arith_plugin.cpp @@ -367,16 +367,6 @@ namespace qe { simplify(result); } - expr_ref mk_idiv(expr* a, numeral const & k) { - if (k.is_one()) { - return expr_ref(a, m); - } - expr_ref result(m); - result = m_arith.mk_idiv(a, m_arith.mk_numeral(k, true)); - simplify(result); - return result; - } - expr* mk_numeral(numeral const& k, bool is_int = true) { return m_arith.mk_numeral(k, is_int); } expr* mk_numeral(int k, bool is_int) { return mk_numeral(numeral(k),is_int); } @@ -1699,6 +1689,40 @@ public: private: + /** + \brief Compute least upper/greatest lower bounds for x. + + Assume: + (not (= k 0)) + (<= 0 (mod m k)) + (< (mod m k) (abs k)) + (= m (+ (* k (div m k)) (mod m k))) + i.e. + k * (e div k) + (e mod k) = e + + + When k is positive, least upper bound + for x such that: k*x <= e is e div k + + When k is negative, greatest lower bound + for x such that k*x <= e is e div k + + k * (e div k) + (e mod k) = e + */ + expr_ref mk_idiv(expr* e, numeral k) { + SASSERT(!k.is_zero()); + arith_util& a = m_util.m_arith; + if (k.is_one()) { + return expr_ref(e, m); + } + if (k.is_minus_one()) { + return expr_ref(a.mk_uminus(e), m); + } + SASSERT(a.is_int(e)); + return expr_ref(a.mk_idiv(e, a.mk_numeral(k, true)), m); + } + + void get_def(contains_app& contains_x, unsigned v, expr* fml, expr_ref& def) { app* x = contains_x.x(); x_subst x_t(m_util); @@ -1730,35 +1754,30 @@ public: // a*x + term <= 0 expr_ref term(bounds.exprs(is_strict, !is_lower)[i], m); rational a = bounds.coeffs(is_strict, !is_lower)[i]; + if (x_t.get_term()) { - // a*(c*x' + s) + term <= 0 - // term <- a*s + term - // a <- a*c - term = m_util.mk_add(m_util.mk_mul(a,x_t.get_term()), term); - a = a * x_t.get_coeff(); + // x := coeff * x' + s + // solve instead for + // a*coeff*x' + term + a*s <= 0 + TRACE("qe", tout << x_t.get_coeff() << "* " << mk_pp(x,m) << " + " + << mk_pp(x_t.get_term(), m) << "\n";); + SASSERT(x_t.get_coeff().is_pos()); + term = m_util.mk_add(term, m_util.mk_mul(a, x_t.get_term())); + a = a * x_t.get_coeff(); } + + TRACE("qe", tout << a << "* " << mk_pp(x,m) << " + " << mk_pp(term, m) << " <= 0\n";); SASSERT(a.is_int()); - if (is_lower) { - // a*x + t <= 0 - // <= - // x <= -t div a - SASSERT(a.is_pos()); - term = m_util.mk_idiv(m_util.mk_uminus(term), a); - } - else { - // -a*x + t <= 0 - // <=> - // t <= a*x - // <= - // ((div t a) + 1) <= x - term = m_util.mk_idiv(term, abs(a)); - if (!(abs(a).is_one())) { - term = m_util.mk_add(term, m_util.mk_one(x)); - } - } - terms.push_back(term); SASSERT(is_lower == a.is_pos()); - TRACE("qe", tout << is_lower << " " << a << " " << mk_pp(term, m) << "\n";); + + // a*x + t <= 0 + // <= + // x <= -t div a + 1 + + term = m_util.mk_uminus(term); + term = mk_idiv(term, a); + terms.push_back(term); + TRACE("qe", tout << "a: " << a << " term: " << mk_pp(term, m) << "\n";); } is_strict = true; sz = bounds.size(is_strict, !is_lower); @@ -1788,14 +1807,11 @@ public: } if (x_t.get_term()) { - // - // x = x_t.get_coeff()*x' + x_t.get_term() - // => - // x' = (x - x_t.get_term()) div x_t.get_coeff() - // - def = m_util.mk_idiv(m_util.mk_sub(def, x_t.get_term()), x_t.get_coeff()); + // x := coeff * x + s + TRACE("qe", tout << x_t.get_coeff() << "* " << mk_pp(x,m) << " + " + << mk_pp(x_t.get_term(), m) << "\n";); + def = m_util.mk_add(m_util.mk_mul(x_t.get_coeff(), def), x_t.get_term()); } - m_util.simplify(def); return; } @@ -1822,25 +1838,39 @@ public: // assert v => (x <= t_i) // SASSERT(v < bounds.size(is_strict, is_lower)); - expr_ref t(bounds.exprs(is_strict, is_lower)[v], m); + def = bounds.exprs(is_strict, is_lower)[v]; rational a = bounds.coeffs(is_strict, is_lower)[v]; - - t = x_t.mk_term(a, t); - a = x_t.mk_coeff(a); - def = t; - if (a.is_pos()) { - def = m_util.mk_uminus(def); - } if (x_t.get_term()) { - def = m_util.mk_idiv(m_util.mk_sub(def, x_t.get_term()), x_t.get_coeff()); + // x := coeff * x' + s + // solve instead for + // a*coeff*x' + term + a*s <= 0 + TRACE("qe", tout << x_t.get_coeff() << "* " << mk_pp(x,m) << " + " + << mk_pp(x_t.get_term(), m) << "\n";); + SASSERT(x_t.get_coeff().is_pos()); + def = m_util.mk_add(def, m_util.mk_mul(a, x_t.get_term())); + a = a * x_t.get_coeff(); } - if (!a.is_one()) { - def = m_util.mk_idiv(def, a); + + SASSERT(a.is_int()); + SASSERT(is_lower != a.is_pos()); + + // a*x + t <= 0 + // <= + // x <= -t div a + + def = m_util.mk_uminus(def); + def = mk_idiv(def, a); + + if (x_t.get_term()) { + // x := coeff * x + s + def = m_util.mk_add(m_util.mk_mul(x_t.get_coeff(), def), x_t.get_term()); } + m_util.simplify(def); - TRACE("qe", tout << "TBD: " << a << " " << mk_pp(t, m) << "\n";); + + TRACE("qe", tout << "TBD: " << a << " " << mk_pp(def, m) << "\n";); } expr_ref mk_not(expr* e) { diff --git a/src/muz_qe/qe_datatype_plugin.cpp b/src/muz_qe/qe_datatype_plugin.cpp index 9584241db..f200262be 100644 --- a/src/muz_qe/qe_datatype_plugin.cpp +++ b/src/muz_qe/qe_datatype_plugin.cpp @@ -467,10 +467,10 @@ namespace qe { SASSERT(m_datatype_util.is_datatype(s)); TRACE("quant_elim", tout << mk_pp(x.x(), m) << " " << vl << "\n";); if (m_datatype_util.is_recursive(s)) { - subst_rec(x, vl, fml); + subst_rec(x, vl, fml, def); } else { - subst_nonrec(x, vl, fml); + subst_nonrec(x, vl, fml, def); } if (def) { *def = 0; // TBD @@ -501,14 +501,21 @@ namespace qe { private: + void add_def(expr* term, expr_ref* def) { + if (def) { + *def = term; + } + } + // // replace x by C(y1,..,yn) where y1,..,yn are fresh variables. // - void subst_constructor(contains_app& x, func_decl* c, expr_ref& fml) { + void subst_constructor(contains_app& x, func_decl* c, expr_ref& fml, expr_ref* def) { subst_clos* sub = 0; if (m_subst_cache.find(x.x(), c, sub)) { m_replace->apply_substitution(x.x(), sub->first, 0, fml); + add_def(sub->first, def); for (unsigned i = 0; i < sub->second.size(); ++i) { m_ctx.add_var(sub->second[i]); } @@ -529,6 +536,7 @@ namespace qe { m_trail.push_back(c); m_trail.push_back(t); + add_def(t, def); m_replace->apply_substitution(x.x(), t, 0, fml); sub->first = t; m_subst_cache.insert(x.x(), c, sub); @@ -643,7 +651,7 @@ namespace qe { } } - void subst_rec(contains_app& contains_x, rational const& vl, expr_ref& fml) { + void subst_rec(contains_app& contains_x, rational const& vl, expr_ref& fml, expr_ref* def) { app* x = contains_x.x(); sort* s = x->get_decl()->get_range(); SASSERT(m_datatype_util.is_datatype(s)); @@ -661,6 +669,7 @@ namespace qe { app_ref fresh_x(m.mk_fresh_const("x", s), m); m_ctx.add_var(fresh_x); m_replace->apply_substitution(x, fresh_x, 0, fml); + add_def(fresh_x, def); TRACE("quant_elim", tout << "Add recognizer " << mk_pp(is_c, m) << "\n";); return; } @@ -668,7 +677,7 @@ namespace qe { if (has_selector(contains_x, fml, c)) { TRACE("quant_elim", tout << "Eliminate selector " << mk_ll_pp(c, m) << "\n";); - subst_constructor(contains_x, c, fml); + subst_constructor(contains_x, c, fml, def); return; } @@ -697,6 +706,7 @@ namespace qe { if (idx < eqs.num_eqs()) { expr* t = eqs.eq(idx); expr* c = eqs.eq_cond(idx); + add_def(t, def); m_replace->apply_substitution(x, t, fml); if (!m.is_true(c)) { fml = m.mk_and(c, fml); @@ -710,6 +720,10 @@ namespace qe { for (unsigned i = 0; i < eqs.num_neqs(); ++i) { m_replace->apply_substitution(eqs.neq_atom(i), m.mk_true(), fml); } + if (def) { + NOT_IMPLEMENTED_YET(); + // you need to create a diagonal term + } } TRACE("quant_elim", tout << "reduced " << mk_pp(fml.get(), m) << "\n";); } @@ -753,7 +767,7 @@ namespace qe { m_ctx.add_constraint(true, is_c); } - virtual void subst_nonrec(contains_app& x, rational const& vl, expr_ref& fml) { + virtual void subst_nonrec(contains_app& x, rational const& vl, expr_ref& fml, expr_ref* def) { sort* s = x.x()->get_decl()->get_range(); SASSERT(m_datatype_util.is_datatype(s)); SASSERT(!m_datatype_util.is_recursive(s)); @@ -767,7 +781,7 @@ namespace qe { SASSERT(vl.get_unsigned() < sz); c = (*m_datatype_util.get_datatype_constructors(s))[vl.get_unsigned()]; } - subst_constructor(x, c, fml); + subst_constructor(x, c, fml, def); } diff --git a/src/test/dead/qe_defs.cpp b/src/test/dead/qe_defs.cpp deleted file mode 100644 index d1c8232d8..000000000 --- a/src/test/dead/qe_defs.cpp +++ /dev/null @@ -1,87 +0,0 @@ -#include "arith_decl_plugin.h" -#include "qe.h" -#include "ast_pp.h" -#include "smtparser.h" -#include "reg_decl_plugins.h" - - -static void test_defs(ast_manager& m, expr* _fml) { - arith_util a(m); - app_ref x(m); - qe::def_vector defs(m); - expr_ref fml(_fml, m); - x = m.mk_const(symbol("x"), a.mk_int()); - app* vars[1] = { x.get() }; - front_end_params fparams; - qe::expr_quant_elim qelim(m, fparams); - lbool result = qelim.first_elim(1, vars, fml, defs); - std::cout << mk_pp(_fml, m) << "\n--->\n"; - std::cout << mk_pp(fml, m) << "\n"; - for (unsigned i = 0; i < defs.size(); ++i) { - std::cout << defs.var(i)->get_name() << " " - << mk_pp(defs.def(i), m) << "\n"; - } - std::cout << "\n"; -} - -static void test_defs_all(ast_manager& m, expr* _fml) { - arith_util a(m); - app_ref x(m); - expr_ref fml(_fml, m), fml0(_fml, m); - x = m.mk_const(symbol("x"), a.mk_int()); - app* vars[1] = { x.get() }; - front_end_params fparams; - qe::expr_quant_elim qelim(m, fparams); - lbool result = l_true; - while (result == l_true) { - fml = fml0; - qe::def_vector defs(m); - result = qelim.first_elim(1, vars, fml, defs); - std::cout << result << "\n"; - std::cout << mk_pp(fml, m) << "\n"; - for (unsigned i = 0; i < defs.size(); ++i) { - std::cout << defs.var(i)->get_name() << " " - << mk_pp(defs.def(i), m) << "\n"; - } - fml0 = m.mk_and(fml0, m.mk_not(fml)); - } -} - -static void test_defs(char const* str) { - ast_manager m; - reg_decl_plugins(m); - scoped_ptr parser = smtlib::parser::create(m); - parser->initialize_smtlib(); - std::ostringstream buffer; - buffer << "(benchmark presburger :status unknown :logic AUFLIA " - << ":extrafuns ((x Int) (y Int) (z Int))\n" - << ":formula " << str << ")"; - parser->parse_string(buffer.str().c_str()); - smtlib::benchmark* b = parser->get_benchmark(); - smtlib::theory::expr_iterator it = b->begin_formulas(); - smtlib::theory::expr_iterator end = b->end_formulas(); - for (; it != end; ++it) { - test_defs(m, *it); - } -} - -void tst_qe_defs() { - enable_trace("qe"); - test_defs("(and (<= (* 2 x) y) (>= (* 3 x) z) (<= (* 4 x) (* 2 z)) (= (mod x 2) 0))"); - - return; - test_defs("(and (<= (* 2 x) y) (>= (* 3 x) z) (= (mod x 2) 0))"); - test_defs("(and (<= (* 2 x) y) (= (mod x 2) 0))"); - test_defs("(= (* 2 x) y)"); - test_defs("(or (< x 0) (> x 1))"); - test_defs("(or (< x y) (> x y))"); - test_defs("(= x y)"); - test_defs("(<= x y)"); - test_defs("(>= x y)"); - test_defs("(and (<= (+ x y) 0) (<= (+ x z) 0))"); - test_defs("(and (<= (+ x y) 0) (<= (+ (* 2 x) z) 0))"); - test_defs("(and (<= (+ (* 3 x) y) 0) (<= (+ (* 2 x) z) 0))"); - test_defs("(and (>= x y) (>= x z))"); - test_defs("(< x y)"); - test_defs("(> x y)"); -} diff --git a/src/test/quant_solve.cpp b/src/test/quant_solve.cpp index 003ae26b4..d78f61e34 100644 --- a/src/test/quant_solve.cpp +++ b/src/test/quant_solve.cpp @@ -8,39 +8,82 @@ #include "expr_replacer.h" #include "smt_solver.h" #include "reg_decl_plugins.h" +#include "smtparser.h" +#include "expr_abstract.h" +#include "model_smt2_pp.h" -static void validate_quant_solution(ast_manager& m, app* x, expr* fml, expr* t, expr* new_fml) { +static void validate_quant_solution(ast_manager& m, expr* fml, expr* guard, qe::def_vector const& defs) { // verify: - // new_fml <=> fml[t/x] + // new_fml => fml[t/x] scoped_ptr rep = mk_expr_simp_replacer(m); + app_ref_vector xs(m); expr_substitution sub(m); - sub.insert(x, t); + for (unsigned i = 0; i < defs.size(); ++i) { + xs.push_back(m.mk_const(defs.var(i))); + sub.insert(xs.back(), defs.def(i)); + } rep->set_substitution(&sub); expr_ref fml1(fml, m); (*rep)(fml1); expr_ref tmp(m); - tmp = m.mk_not(m.mk_iff(new_fml, fml1)); + tmp = m.mk_not(m.mk_implies(guard, fml1)); front_end_params fp; smt::solver solver(m, fp); solver.assert_expr(tmp); lbool res = solver.check(); - std::cout << res << "\n"; + //SASSERT(res == l_false); + if (res != l_false) { + std::cout << "Validation failed: " << res << "\n"; + std::cout << mk_pp(tmp, m) << "\n"; + model_ref model; + solver.get_model(model); + model_smt2_pp(std::cout, m, *model, 0); + fatal_error(0); + } +} + + +static void validate_quant_solutions(app* x, expr* fml, expr_ref_vector& guards) { + return; + // quant_elim option got removed... + // verify: + // fml <=> guard_1 \/ guard_2 \/ ... + ast_manager& m = guards.get_manager(); + expr_ref tmp(m), fml2(m); + tmp = m.mk_or(guards.size(), guards.c_ptr()); + expr* _x = x; + std::cout << mk_pp(fml, m) << "\n"; + expr_abstract(m, 0, 1, &_x, fml, fml2); + std::cout << mk_pp(fml2, m) << "\n"; + symbol name(x->get_decl()->get_name()); + sort* s = m.get_sort(x); + fml2 = m.mk_exists(1, &s, &name, fml2); + std::cout << mk_pp(fml2, m) << "\n"; + tmp = m.mk_not(m.mk_iff(fml2, tmp)); + std::cout << mk_pp(tmp, m) << "\n"; + front_end_params fp; + smt::solver solver(m, fp); + solver.assert_expr(tmp); + lbool res = solver.check(); + std::cout << "checked\n"; SASSERT(res == l_false); + if (res != l_false) { + std::cout << res << "\n"; + fatal_error(0); + } } static void test_quant_solver(ast_manager& m, app* x, expr* fml) { front_end_params params; - params.m_quant_elim = true; qe::expr_quant_elim qe(m, params); - expr_ref_vector terms(m); - expr_ref_vector fmls(m); - bool success = qe.solve_for_var(x, fml, terms, fmls); + qe::guarded_defs defs(m); + bool success = qe.solve_for_var(x, fml, defs); std::cout << "------------------------\n"; std::cout << mk_pp(fml, m) << "\n"; - if (success) { - for (unsigned i = 0; i < terms.size(); ++i) { - std::cout << mk_pp(x, m) << " = " << mk_pp(terms[i].get(), m) << "\n" << mk_pp(fmls[i].get(), m) << "\n"; - validate_quant_solution(m, x, fml, terms[i].get(), fmls[i].get()); + if (success) { + defs.display(std::cout); + for (unsigned i = 0; i < defs.size(); ++i) { + validate_quant_solution(m, fml, defs.guard(i), defs.defs(i)); } } else { @@ -48,32 +91,18 @@ static void test_quant_solver(ast_manager& m, app* x, expr* fml) { } } -static void test_quant_solver_rec(ast_manager& m, unsigned num_vars, app* const* xs, expr* fml) { - if (num_vars == 0) { - return; - } + +static void test_quant_solver(ast_manager& m, unsigned sz, app*const* xs, expr* fml) { front_end_params params; - params.m_quant_elim = true; qe::expr_quant_elim qe(m, params); - expr_ref_vector fmls(m), ors(m), terms(m); - app* x = xs[0]; - bool success = qe.solve_for_var(x, fml, terms, fmls); + qe::guarded_defs defs(m); + bool success = qe.solve_for_vars(sz, xs, fml, defs); std::cout << "------------------------\n"; std::cout << mk_pp(fml, m) << "\n"; - if (success) { - for (unsigned i = 0; i < terms.size(); ++i) { - std::cout << mk_pp(x, m) << " = " << mk_pp(terms[i].get(), m) << "\n" << mk_pp(fmls[i].get(), m) << "\n"; - validate_quant_solution(m, x, fml, terms[i].get(), fmls[i].get()); - ors.reset(); - if (m.is_or(fmls[i].get())) { - ors.append(to_app(fmls[i].get())->get_num_args(), to_app(fmls[i].get())->get_args()); - } - else { - ors.push_back(fmls[i].get()); - } - for (unsigned j = 0; j < ors.size(); ++j) { - test_quant_solver_rec(m, num_vars-1, xs+1, ors[j].get()); - } + if (success) { + defs.display(std::cout); + for (unsigned i = 0; i < defs.size(); ++i) { + validate_quant_solution(m, fml, defs.guard(i), defs.defs(i)); } } else { @@ -82,65 +111,107 @@ static void test_quant_solver_rec(ast_manager& m, unsigned num_vars, app* const* } +static expr_ref parse_fml(ast_manager& m, char const* str) { + expr_ref result(m); + reg_decl_plugins(m); + scoped_ptr parser = smtlib::parser::create(m); + parser->initialize_smtlib(); + std::ostringstream buffer; + buffer << "(benchmark presburger :status unknown :logic AUFLIA " + << ":extrafuns ((x Int) (y Int) (z Int) (a Int) (b Int))\n" + << ":formula " << str << ")"; + parser->parse_string(buffer.str().c_str()); + smtlib::benchmark* b = parser->get_benchmark(); + smtlib::theory::expr_iterator it = b->begin_formulas(); + smtlib::theory::expr_iterator end = b->end_formulas(); + SASSERT(it != b->end_formulas()); + result = *it; + return result; +} + +static void test_quant_solver(ast_manager& m, app* x, char const* str) { + expr_ref fml = parse_fml(m, str); + test_quant_solver(m, x, fml); +} + +static void test_quant_solver(ast_manager& m, unsigned sz, app*const* xs, char const* str) { + expr_ref fml = parse_fml(m, str); + test_quant_solver(m, sz, xs, fml); +} + + static void test_quant_solve1() { ast_manager m; arith_util ar(m); - reg_decl_plugins(m); sort* i = ar.mk_int(); - app_ref x(m.mk_const(symbol("x"),i), m); - app_ref y(m.mk_const(symbol("y"),i), m); - app_ref a(m.mk_const(symbol("a"),i), m); - app_ref b(m.mk_const(symbol("b"),i), m); - expr_ref n2(ar.mk_numeral(rational(2), true), m); - expr_ref n3(ar.mk_numeral(rational(3), true), m); - expr_ref n4(ar.mk_numeral(rational(4), true), m); - expr_ref n10(ar.mk_numeral(rational(10), true), m); - expr_ref n20(ar.mk_numeral(rational(20), true), m); - expr_ref x2(ar.mk_mul(n2, x), m); - expr_ref x3(ar.mk_mul(n3, x), m); - expr_ref fml1(m), fml2(m), fml3(m), fml4(m); - expr_ref fml(m), t1(m), t2(m); - - fml1 = m.mk_eq(x, a); - fml2 = ar.mk_lt(x, a); - fml3 = ar.mk_gt(x, a); - fml4 = m.mk_and(ar.mk_lt(x, a), ar.mk_lt(x, b)); - expr_ref fml5(m.mk_and(ar.mk_gt(x, a), ar.mk_lt(x, b)), m); - expr_ref fml6(ar.mk_le(x, a), m); - expr_ref fml7(ar.mk_ge(x, a), m); - expr_ref fml8(ar.mk_lt(ar.mk_mul(n2, x), a), m); - expr_ref fml9(m.mk_eq(ar.mk_mul(n2, x), a), m); - - test_quant_solver(m, x.get(), fml1.get()); - test_quant_solver(m, x.get(), fml2.get()); - test_quant_solver(m, x.get(), fml3.get()); - test_quant_solver(m, x.get(), fml4.get()); - test_quant_solver(m, x.get(), fml5.get()); - test_quant_solver(m, x.get(), fml6.get()); - test_quant_solver(m, x.get(), fml7.get()); - test_quant_solver(m, x.get(), fml8.get()); - test_quant_solver(m, x.get(), fml9.get()); - - fml = ar.mk_lt(x2, a); test_quant_solver(m, x.get(), fml.get()); - fml = ar.mk_gt(x2, a); test_quant_solver(m, x.get(), fml.get()); - fml = ar.mk_le(x2, a); test_quant_solver(m, x.get(), fml.get()); - fml = ar.mk_ge(x2, a); test_quant_solver(m, x.get(), fml.get()); + app_ref xr(m.mk_const(symbol("x"),i), m); + app_ref yr(m.mk_const(symbol("y"),i), m); + app* x = xr.get(); + app* y = yr.get(); + app* xy[2] = { x, y }; - fml = m.mk_and(ar.mk_lt(a, ar.mk_mul(n3,x)), ar.mk_lt(ar.mk_mul(n3,x), b)); - test_quant_solver(m, x.get(), fml.get()); + test_quant_solver(m, x, "(and (<= x y) (= (mod x 2) 0))"); + test_quant_solver(m, x, "(and (<= (* 2 x) y) (= (mod x 2) 0))"); + test_quant_solver(m, x, "(and (>= x y) (= (mod x 2) 0))"); + test_quant_solver(m, x, "(and (>= (* 2 x) y) (= (mod x 2) 0))"); + test_quant_solver(m, x, "(and (<= (* 2 x) y) (>= x z) (= (mod x 2) 0))"); + test_quant_solver(m, x, "(and (<= (* 2 x) y) (>= (* 3 x) z) (= (mod x 2) 0))"); + + test_quant_solver(m, x, "(>= (* 2 x) a)"); + + test_quant_solver(m, x, "(<= (* 2 x) a)"); + test_quant_solver(m, x, "(< (* 2 x) a)"); + test_quant_solver(m, x, "(= (* 2 x) a)"); + test_quant_solver(m, x, "(< (* 2 x) a)"); + test_quant_solver(m, x, "(> (* 2 x) a)"); + + + test_quant_solver(m, x, "(and (<= a x) (<= (* 2 x) b))"); + + test_quant_solver(m, x, "(and (<= a x) (<= x b))"); + test_quant_solver(m, x, "(and (<= (* 2 a) x) (<= x b))"); + test_quant_solver(m, x, "(and (<= (* 2 a) x) (<= (* 2 x) b))"); + test_quant_solver(m, x, "(and (<= a x) (<= (* 3 x) b))"); + test_quant_solver(m, x, "(and (<= (* 3 a) x) (<= x b))"); + test_quant_solver(m, x, "(and (<= (* 3 a) x) (<= (* 3 x) b))"); + + test_quant_solver(m, x, "(and (< a (* 3 x)) (< (* 3 x) b))"); + + test_quant_solver(m, x, "(< (* 3 x) a)"); + test_quant_solver(m, x, "(= (* 3 x) a)"); + test_quant_solver(m, x, "(< (* 3 x) a)"); + test_quant_solver(m, x, "(> (* 3 x) a)"); + test_quant_solver(m, x, "(<= (* 3 x) a)"); + test_quant_solver(m, x, "(>= (* 3 x) a)"); + + test_quant_solver(m, x, "(<= (* 2 x) a)"); + test_quant_solver(m, x, "(or (= (* 2 x) y) (= (+ (* 2 x) 1) y))"); + test_quant_solver(m, x, "(= x a)"); + test_quant_solver(m, x, "(< x a)"); + test_quant_solver(m, x, "(> x a)"); + test_quant_solver(m, x, "(and (> x a) (< x b))"); + test_quant_solver(m, x, "(and (> x a) (< x b))"); + test_quant_solver(m, x, "(<= x a)"); + test_quant_solver(m, x, "(>= x a)"); + test_quant_solver(m, x, "(and (<= (* 2 x) y) (= (mod x 2) 0))"); + test_quant_solver(m, x, "(= (* 2 x) y)"); + test_quant_solver(m, x, "(or (< x 0) (> x 1))"); + test_quant_solver(m, x, "(or (< x y) (> x y))"); + test_quant_solver(m, x, "(= x y)"); + test_quant_solver(m, x, "(<= x y)"); + test_quant_solver(m, x, "(>= x y)"); + test_quant_solver(m, x, "(and (<= (+ x y) 0) (<= (+ x z) 0))"); + test_quant_solver(m, x, "(and (<= (+ x y) 0) (<= (+ (* 2 x) z) 0))"); + test_quant_solver(m, x, "(and (<= (+ (* 3 x) y) 0) (<= (+ (* 2 x) z) 0))"); + test_quant_solver(m, x, "(and (>= x y) (>= x z))"); + test_quant_solver(m, x, "(< x y)"); + test_quant_solver(m, x, "(> x y)"); + + test_quant_solver(m, 2, xy, "(and (<= (- (* 2 y) b) (+ (* 3 x) a)) (<= (- (* 2 x) a) (+ (* 4 y) b)))"); - t1 = ar.mk_sub(ar.mk_mul(n2,y),b); - t2 = ar.mk_add(ar.mk_mul(n3,x),a); - fml1 = ar.mk_le(t1, t2); - t1 = ar.mk_sub(ar.mk_mul(n2,x),a); - t2 = ar.mk_add(ar.mk_mul(n4,y),b); - fml2 = ar.mk_le(t1,t2); - fml = m.mk_and(fml1, fml2); - app* xy[2] = { x.get(), y.get() }; - test_quant_solver_rec(m, 2, xy, fml.get()); }