From 196aed785e43861064d28461f94f0d97b522c6cc Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 12 Sep 2013 13:27:31 -0700 Subject: [PATCH] fixes for qe_arith Signed-off-by: Nikolaj Bjorner --- src/qe/qe_arith.cpp | 134 +++++++++++++++--------------------------- src/test/qe_arith.cpp | 5 ++ 2 files changed, 51 insertions(+), 88 deletions(-) diff --git a/src/qe/qe_arith.cpp b/src/qe/qe_arith.cpp index 85229de44..393467cc7 100644 --- a/src/qe/qe_arith.cpp +++ b/src/qe/qe_arith.cpp @@ -23,6 +23,7 @@ Revision History: #include "arith_decl_plugin.h" #include "ast_pp.h" #include "th_rewriter.h" +#include "expr_functors.h" namespace qe { @@ -33,61 +34,39 @@ namespace qe { expr_ref_vector m_ineq_terms; vector m_ineq_coeffs; svector m_ineq_strict; + scoped_ptr m_var; struct cant_project {}; - // TBD: replace by "contains_x" class. - - bool contains(app* var, expr* t) const { - ast_mark mark; - ptr_vector todo; - todo.push_back(t); - while (!todo.empty()) { - t = todo.back(); - todo.pop_back(); - if (mark.is_marked(t)) { - continue; - } - mark.mark(t, true); - if (var == t) { - return true; - } - SASSERT(is_app(t)); - app* ap = to_app(t); - todo.append(ap->get_num_args(), ap->get_args()); - } - return false; - } - - void is_linear(app* var, rational const& mul, expr* t, rational& c, expr_ref_vector& ts) { + void is_linear(rational const& mul, expr* t, rational& c, expr_ref_vector& ts) { expr* t1, *t2; rational mul1; - if (t == var) { + if (t == m_var->x()) { c += mul; } else if (a.is_mul(t, t1, t2) && a.is_numeral(t1, mul1)) { - is_linear(var, mul* mul1, t2, c, ts); + is_linear(mul* mul1, t2, c, ts); } else if (a.is_mul(t, t1, t2) && a.is_numeral(t2, mul1)) { - is_linear(var, mul* mul1, t1, c, ts); + is_linear(mul* mul1, t1, c, ts); } else if (a.is_add(t)) { app* ap = to_app(t); for (unsigned i = 0; i < ap->get_num_args(); ++i) { - is_linear(var, mul, ap->get_arg(i), c, ts); + is_linear(mul, ap->get_arg(i), c, ts); } } else if (a.is_sub(t, t1, t2)) { - is_linear(var, mul, t1, c, ts); - is_linear(var, -mul, t2, c, ts); + is_linear(mul, t1, c, ts); + is_linear(-mul, t2, c, ts); } else if (a.is_uminus(t, t1)) { - is_linear(var, -mul, t1, c, ts); + is_linear(-mul, t1, c, ts); } else if (a.is_numeral(t, mul1)) { ts.push_back(a.mk_numeral(mul*mul1, m.get_sort(t))); } - else if (contains(var, t)) { + else if ((*m_var)(t)) { IF_VERBOSE(1, verbose_stream() << mk_pp(t, m) << "\n";); throw cant_project(); } @@ -99,8 +78,8 @@ namespace qe { } } - bool is_linear(app* var, expr* lit, rational& c, expr_ref& t, bool& is_strict) { - if (!contains(var, lit)) { + bool is_linear(expr* lit, rational& c, expr_ref& t, bool& is_strict) { + if (!(*m_var)(lit)) { return false; } expr* e1, *e2; @@ -114,20 +93,20 @@ namespace qe { } SASSERT(!m.is_not(lit)); if (a.is_le(lit, e1, e2) || a.is_ge(lit, e2, e1)) { - is_linear(var, mul, e1, c, ts); - is_linear(var, -mul, e2, c, ts); + is_linear( mul, e1, c, ts); + is_linear(-mul, e2, c, ts); s = m.get_sort(e1); is_strict = is_not; } else if (a.is_lt(lit, e1, e2) || a.is_gt(lit, e2, e1)) { - is_linear(var, mul, e1, c, ts); - is_linear(var, -mul, e2, c, ts); + is_linear( mul, e1, c, ts); + is_linear(-mul, e2, c, ts); s = m.get_sort(e1); is_strict = !is_not; } else if (m.is_eq(lit, e1, e2) && !is_not) { - is_linear(var, mul, e1, c, ts); - is_linear(var, -mul, e2, c, ts); + is_linear( mul, e1, c, ts); + is_linear(-mul, e2, c, ts); s = m.get_sort(e1); is_strict = false; } @@ -143,14 +122,15 @@ namespace qe { return true; } - void project(model& model, app* var, expr_ref_vector& lits) { - unsigned num_pos = 0, num_neg = 0; + void project(model& model, expr_ref_vector& lits) { + unsigned num_pos = 0; + unsigned num_neg = 0; expr_ref_vector new_lits(m); for (unsigned i = 0; i < lits.size(); ++i) { rational c(0); expr_ref t(m); bool is_strict; - if (is_linear(var, lits[i].get(), c, t, is_strict)) { + if (is_linear(lits[i].get(), c, t, is_strict)) { m_ineq_coeffs.push_back(c); m_ineq_terms.push_back(t); m_ineq_strict.push_back(is_strict); @@ -158,7 +138,7 @@ namespace qe { ++num_pos; } else { - --num_neg; + ++num_neg; } } else { @@ -170,69 +150,39 @@ namespace qe { if (num_pos == 0 || num_neg == 0) { return; } - if (num_pos < num_neg) { - unsigned max_t = find_max(model); - for (unsigned i = 0; i < m_ineq_terms.size(); ++i) { - if (i != max_t) { - if (m_ineq_coeffs[i].is_pos()) { - lits.push_back(mk_le(i, max_t)); - } - else { - lits.push_back(mk_lt(i, max_t)); - } + bool use_pos = num_pos < num_neg; + unsigned max_t = find_max(model, use_pos); + + for (unsigned i = 0; i < m_ineq_terms.size(); ++i) { + if (i != max_t) { + if (m_ineq_coeffs[i].is_pos() == use_pos) { + lits.push_back(mk_le(i, max_t)); } - } - } - else { - unsigned min_t = find_min(model); - for (unsigned i = 0; i < m_ineq_terms.size(); ++i) { - if (i != min_t) { - if (m_ineq_coeffs[i].is_neg()) { - lits.push_back(mk_le(min_t, i)); - } - else { - lits.push_back(mk_lt(min_t, i)); - } + else { + lits.push_back(mk_lt(i, max_t)); } } } } - unsigned find_max(model& mdl) { - return find_min_max(mdl, true); - } - - unsigned find_min(model& mdl) { - return find_min_max(mdl, false); - } - - unsigned find_min_max(model& mdl, bool do_max) { + unsigned find_max(model& mdl, bool do_pos) { unsigned result; bool found = false; rational found_val(0), r; expr_ref val(m); for (unsigned i = 0; i < m_ineq_terms.size(); ++i) { rational const& ac = m_ineq_coeffs[i]; - if (ac.is_pos() && do_max) { + if (ac.is_pos() == do_pos) { VERIFY(mdl.eval(m_ineq_terms[i].get(), val)); VERIFY(a.is_numeral(val, r)); - r /= ac; + r /= abs(ac); + IF_VERBOSE(1, verbose_stream() << "max: " << mk_pp(m_ineq_terms[i].get(), m) << " " << r << " " << (!found || r > found_val) << "\n";); if (!found || r > found_val) { result = i; found_val = r; found = true; } } - else if (ac.is_neg() && !do_max) { - VERIFY(mdl.eval(m_ineq_terms[i].get(), val)); - VERIFY(a.is_numeral(val, r)); - r /= abs(ac); //// review. - if (!found || r < found_val) { - result = i; - found_val = r; - found = true; - } - } } SASSERT(found); return result; @@ -300,11 +250,19 @@ namespace qe { m(m), a(m), m_rw(m), m_ineq_terms(m) {} expr_ref operator()(model& model, app_ref_vector& vars, expr_ref_vector const& lits) { + app_ref_vector new_vars(m); expr_ref_vector result(lits); for (unsigned i = 0; i < vars.size(); ++i) { - project(model, vars[i].get(), result); + m_var = alloc(contains_app, m, vars[i].get()); + try { + project(model, result); + } + catch (cant_project) { + new_vars.push_back(vars[i].get()); + } } vars.reset(); + vars.append(new_vars); expr_ref res1(m); expr_ref tmp = qe::mk_and(result); m_rw(tmp, res1); diff --git a/src/test/qe_arith.cpp b/src/test/qe_arith.cpp index a2789ee80..8d04e2489 100644 --- a/src/test/qe_arith.cpp +++ b/src/test/qe_arith.cpp @@ -17,6 +17,9 @@ static expr_ref parse_fml(ast_manager& m, char const* str) { buffer << "(declare-const x Real)\n" << "(declare-const y Real)\n" << "(declare-const z Real)\n" + << "(declare-const u Real)\n" + << "(declare-const v Real)\n" + << "(declare-const t Real)\n" << "(declare-const a Real)\n" << "(declare-const b Real)\n" << "(assert " << str << ")\n"; @@ -31,6 +34,7 @@ static char const* example1 = "(and (<= x 3.0) (<= (* 3.0 x) y) (<= z y))"; static char const* example2 = "(and (<= z x) (<= x 3.0) (<= (* 3.0 x) y) (<= z y))"; static char const* example3 = "(and (<= z x) (<= x 3.0) (< (* 3.0 x) y) (<= z y))"; static char const* example4 = "(and (<= z x) (<= x 3.0) (not (>= (* 3.0 x) y)) (<= z y))"; +static char const* example5 = "(and (<= y x) (<= z x) (<= x u) (<= x v) (<= x t))"; static void test(char const *ex) { smt_params params; @@ -61,4 +65,5 @@ void tst_qe_arith() { test(example2); test(example3); test(example4); + test(example5); }