From a594597906811390216e95b9ea3cf2ac71fa5491 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 12 Feb 2014 10:54:00 -0800 Subject: [PATCH] improve equality solving in qe-lite Signed-off-by: Nikolaj Bjorner --- src/math/simplex/simplex.h | 3 +- src/qe/qe_lite.cpp | 138 ++++++++++++++++++++++--------------- src/smt/theory_pb.cpp | 13 +++- src/smt/theory_pb.h | 1 + 4 files changed, 97 insertions(+), 58 deletions(-) diff --git a/src/math/simplex/simplex.h b/src/math/simplex/simplex.h index f7125588e..03c01482c 100644 --- a/src/math/simplex/simplex.h +++ b/src/math/simplex/simplex.h @@ -129,6 +129,8 @@ namespace simplex { unsigned get_num_vars() const { return m_vars.size(); } + row_iterator row_begin(row const& r) { return M.row_begin(r); } + row_iterator row_end(row const& r) { return M.row_end(r); } private: @@ -136,7 +138,6 @@ namespace simplex { pivot_strategy_t pivot_strategy(); var_t select_smallest_var() { return m_to_patch.empty()?null_var:m_to_patch.erase_min(); } var_t select_error_var(bool least); - // row get_infeasible_row() { } void check_blands_rule(var_t v, unsigned& num_repeated); bool make_var_feasible(var_t x_i); void update_and_pivot(var_t x_i, var_t x_j, numeral const& a_ij, eps_numeral const& new_value); diff --git a/src/qe/qe_lite.cpp b/src/qe/qe_lite.cpp index 130673527..41214acb3 100644 --- a/src/qe/qe_lite.cpp +++ b/src/qe/qe_lite.cpp @@ -238,67 +238,95 @@ namespace eq { } } - bool solve_arith_core(app * lhs, expr * rhs, expr * eq, ptr_vector& vs, expr_ref_vector& ts) { - SASSERT(a.is_add(lhs)); - bool is_int = a.is_int(lhs); - expr * a1, *v; - expr_ref def(m); - rational a_val; - unsigned num = lhs->get_num_args(); - unsigned i; - for (i = 0; i < num; i++) { - expr * arg = lhs->get_arg(i); - if (is_variable(arg)) { - a_val = rational(1); - v = arg; - break; - } - else if (a.is_mul(arg, a1, v) && - is_variable(v) && - a.is_numeral(a1, a_val) && - !a_val.is_zero() && - (!is_int || a_val.is_minus_one())) { - break; + bool is_invertible_const(bool is_int, expr* x, rational& a_val) { + expr* y; + if (a.is_uminus(x, y) && is_invertible_const(is_int, y, a_val)) { + a_val.neg(); + return true; + } + else if (a.is_numeral(x, a_val) && !a_val.is_zero()) { + if (!is_int || a_val.is_one() || a_val.is_minus_one()) { + return true; } } - if (i == num) - return false; - vs.push_back(to_var(v)); - expr_ref inv_a(m); - if (!a_val.is_one()) { - inv_a = a.mk_numeral(rational(1)/a_val, is_int); - rhs = a.mk_mul(inv_a, rhs); - } - - ptr_buffer other_args; - for (unsigned j = 0; j < num; j++) { - if (i != j) { - if (inv_a) - other_args.push_back(a.mk_mul(inv_a, lhs->get_arg(j))); - else - other_args.push_back(lhs->get_arg(j)); - } - } - switch (other_args.size()) { - case 0: - def = rhs; - break; - case 1: - def = a.mk_sub(rhs, other_args[0]); - break; - default: - def = a.mk_sub(rhs, a.mk_add(other_args.size(), other_args.c_ptr())); - break; - } - ts.push_back(def); - return true; + return false; } + bool is_invertible_mul(bool is_int, expr*& arg, rational& a_val) { + if (is_variable(arg)) { + a_val = rational(1); + return true; + } + expr* x, *y; + if (a.is_mul(arg, x, y)) { + if (is_variable(x) && is_invertible_const(is_int, y, a_val)) { + arg = x; + return true; + } + if (is_variable(y) && is_invertible_const(is_int, x, a_val)) { + arg = y; + return true; + } + } + return false; + } + + typedef std::pair signed_expr; + + expr_ref solve_arith(bool is_int, rational const& r, bool sign, svector const& exprs) { + expr_ref_vector result(m); + for (unsigned i = 0; i < exprs.size(); ++i) { + bool sign2 = exprs[i].first; + expr* e = exprs[i].second; + rational r2(r); + if (sign == sign2) { + r2.neg(); + } + if (!r2.is_one()) { + result.push_back(a.mk_mul(a.mk_numeral(r2, is_int), e)); + } + else { + result.push_back(e); + } + } + return expr_ref(a.mk_add(result.size(), result.c_ptr()), m); + } + + bool solve_arith(expr* lhs, expr* rhs, ptr_vector& vs, expr_ref_vector& ts) { + if (!a.is_int(lhs) && !a.is_real(rhs)) { + return false; + } + rational a_val; + bool is_int = a.is_int(lhs); + svector todo, done; + todo.push_back(std::make_pair(true, lhs)); + todo.push_back(std::make_pair(false, rhs)); + while (!todo.empty()) { + expr* e = todo.back().second; + bool sign = todo.back().first; + todo.pop_back(); + if (a.is_add(e)) { + for (unsigned i = 0; i < to_app(e)->get_num_args(); ++i) { + todo.push_back(std::make_pair(sign, to_app(e)->get_arg(i))); + } + } + else if (is_invertible_mul(is_int, e, a_val)) { + done.append(todo); + vs.push_back(to_var(e)); + a_val = rational(1)/a_val; + ts.push_back(solve_arith(is_int, a_val, sign, done)); + TRACE("qe_lite", tout << mk_pp(lhs, m) << " " << mk_pp(rhs, m) << " " << mk_pp(e, m) << " := " << mk_pp(ts.back(), m) << "\n";); + return true; + } + else { + done.push_back(std::make_pair(sign, e)); + } + } + return false; + } bool arith_solve(expr * lhs, expr * rhs, expr * eq, ptr_vector& vs, expr_ref_vector& ts) { - return - (a.is_add(lhs) && solve_arith_core(to_app(lhs), rhs, eq, vs, ts)) || - (a.is_add(rhs) && solve_arith_core(to_app(rhs), lhs, eq, vs, ts)); + return solve_arith(lhs, rhs, vs, ts); } bool trivial_solve(expr* lhs, expr* rhs, expr* eq, ptr_vector& vs, expr_ref_vector& ts) { diff --git a/src/smt/theory_pb.cpp b/src/smt/theory_pb.cpp index 399445f3d..f21ec9dc6 100644 --- a/src/smt/theory_pb.cpp +++ b/src/smt/theory_pb.cpp @@ -594,6 +594,8 @@ namespace smt { m_simplex.set_upper(v, zero); } ctx.push_trail(undo_bound(*this, v, is_true)); + lbool is_sat = m_simplex.make_feasible(); + std::cout << is_sat << "\n"; } for (unsigned i = 0; i < ineqs->size(); ++i) { @@ -628,8 +630,15 @@ namespace smt { } ctx.push_trail(reset_bound(*this, slack, is_true)); - // m_simplex.feasible(); - // + lbool is_sat = m_simplex.make_feasible(); + if (l_false == is_sat) { + row r = m_simplex.get_infeasible_row(); + row_iterator it = m_simplex.row_begin(r), end = m_simplex.row_end(r); + for (; it != end; ++it) { + it->m_var; + it->m_coeff; + } + } } if (c->is_ge()) { assign_ineq(*c, is_true); diff --git a/src/smt/theory_pb.h b/src/smt/theory_pb.h index a77561304..238ed5558 100644 --- a/src/smt/theory_pb.h +++ b/src/smt/theory_pb.h @@ -43,6 +43,7 @@ namespace smt { typedef vector > arg_t; typedef simplex::simplex simplex; typedef simplex::row row; + typedef simplex::row_iterator row_iterator; struct stats { unsigned m_num_conflicts;