From 4af4466821c1489da0427c6cb0db5171d84a1185 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 12 Sep 2013 12:19:46 -0700 Subject: [PATCH] add qe_arith routine for LW projection on monomomes Signed-off-by: Nikolaj Bjorner --- src/muz/pdr/pdr_farkas_learner.cpp | 22 +- src/muz/pdr/pdr_farkas_learner.h | 3 + src/muz/pdr/pdr_util.h | 2 - src/qe/qe_arith.cpp | 321 +++++++++++++++++++++++++++++ src/qe/qe_arith.h | 16 ++ src/test/main.cpp | 1 + src/test/qe_arith.cpp | 64 ++++++ 7 files changed, 422 insertions(+), 7 deletions(-) create mode 100644 src/qe/qe_arith.cpp create mode 100644 src/qe/qe_arith.h create mode 100644 src/test/qe_arith.cpp diff --git a/src/muz/pdr/pdr_farkas_learner.cpp b/src/muz/pdr/pdr_farkas_learner.cpp index d7ef01aaa..b54eb0117 100644 --- a/src/muz/pdr/pdr_farkas_learner.cpp +++ b/src/muz/pdr/pdr_farkas_learner.cpp @@ -151,6 +151,11 @@ namespace pdr { public: constr(ast_manager& m) : m(m), a(m), m_ineqs(m), m_time(0) {} + void reset() { + m_ineqs.reset(); + m_coeffs.reset(); + } + /** add a multiple of constraint c to the current constr */ void add(rational const & coef, app * c) { bool is_pos = true; @@ -300,7 +305,6 @@ namespace pdr { return r; } - expr_ref extract_consequence(unsigned lo, unsigned hi) { bool is_int = is_int_sort(); app_ref zero(a.mk_numeral(rational::zero(), is_int), m); @@ -373,6 +377,7 @@ namespace pdr { farkas_learner::farkas_learner(smt_params& params, ast_manager& outer_mgr) : m_proof_params(get_proof_params(params)), m_pr(PROOF_MODE), + m_constr(0), m_combine_farkas_coefficients(true), p2o(m_pr, outer_mgr), o2p(outer_mgr, m_pr) @@ -381,6 +386,10 @@ namespace pdr { m_ctx = alloc(smt::kernel, m_pr, m_proof_params); } + farkas_learner::~farkas_learner() { + dealloc(m_constr); + } + smt_params farkas_learner::get_proof_params(smt_params& orig_params) { smt_params res(orig_params); res.m_arith_bound_prop = BP_NONE; @@ -538,11 +547,14 @@ namespace pdr { { ast_manager& m = res.get_manager(); if (m_combine_farkas_coefficients) { - constr res_c(m); - for(unsigned i = 0; i < n; ++i) { - res_c.add(coeffs[i], lits[i]); + if (!m_constr) { + m_constr = alloc(constr, m); } - res_c.get(res); + m_constr->reset(); + for (unsigned i = 0; i < n; ++i) { + m_constr->add(coeffs[i], lits[i]); + } + m_constr->get(res); } else { bool_rewriter rw(m); diff --git a/src/muz/pdr/pdr_farkas_learner.h b/src/muz/pdr/pdr_farkas_learner.h index b623c2035..546759a33 100644 --- a/src/muz/pdr/pdr_farkas_learner.h +++ b/src/muz/pdr/pdr_farkas_learner.h @@ -42,6 +42,7 @@ class farkas_learner { smt_params m_proof_params; ast_manager m_pr; scoped_ptr m_ctx; + constr* m_constr; // // true: produce a combined constraint by applying Farkas coefficients. @@ -80,6 +81,8 @@ class farkas_learner { public: farkas_learner(smt_params& params, ast_manager& m); + ~farkas_learner(); + /** All ast objects have the ast_manager which was passed as an argument to the constructor (i.e. m_outer_mgr) diff --git a/src/muz/pdr/pdr_util.h b/src/muz/pdr/pdr_util.h index 67be6751b..446bde8aa 100644 --- a/src/muz/pdr/pdr_util.h +++ b/src/muz/pdr/pdr_util.h @@ -143,8 +143,6 @@ namespace pdr { */ void reduce_disequalities(model& model, unsigned threshold, expr_ref& fml); - - /** \brief hoist non-boolean if expressions. */ diff --git a/src/qe/qe_arith.cpp b/src/qe/qe_arith.cpp new file mode 100644 index 000000000..85229de44 --- /dev/null +++ b/src/qe/qe_arith.cpp @@ -0,0 +1,321 @@ +/*++ +Copyright (c) 2010 Microsoft Corporation + +Module Name: + + qe_arith.cpp + +Abstract: + + Simple projection function for real arithmetic based on Loos-W. + +Author: + + Nikolaj Bjorner (nbjorner) 2013-09-12 + +Revision History: + + +--*/ + +#include "qe_arith.h" +#include "qe_util.h" +#include "arith_decl_plugin.h" +#include "ast_pp.h" +#include "th_rewriter.h" + +namespace qe { + + class arith_project_util { + ast_manager& m; + arith_util a; + th_rewriter m_rw; + expr_ref_vector m_ineq_terms; + vector m_ineq_coeffs; + svector m_ineq_strict; + + 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) { + expr* t1, *t2; + rational mul1; + if (t == var) { + c += mul; + } + else if (a.is_mul(t, t1, t2) && a.is_numeral(t1, mul1)) { + is_linear(var, 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); + } + 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); + } + } + else if (a.is_sub(t, t1, t2)) { + is_linear(var, mul, t1, c, ts); + is_linear(var, -mul, t2, c, ts); + } + else if (a.is_uminus(t, t1)) { + is_linear(var, -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)) { + IF_VERBOSE(1, verbose_stream() << mk_pp(t, m) << "\n";); + throw cant_project(); + } + else if (mul.is_one()) { + ts.push_back(t); + } + else { + ts.push_back(a.mk_mul(a.mk_numeral(mul, m.get_sort(t)), t)); + } + } + + bool is_linear(app* var, expr* lit, rational& c, expr_ref& t, bool& is_strict) { + if (!contains(var, lit)) { + return false; + } + expr* e1, *e2; + c.reset(); + sort* s; + expr_ref_vector ts(m); + bool is_not = m.is_not(lit, lit); + rational mul(1); + if (is_not) { + mul.neg(); + } + 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); + 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); + 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); + s = m.get_sort(e1); + is_strict = false; + } + else { + throw cant_project(); + } + if (ts.empty()) { + t = a.mk_numeral(rational(0), s); + } + else { + t = a.mk_add(ts.size(), ts.c_ptr()); + } + return true; + } + + void project(model& model, app* var, expr_ref_vector& lits) { + unsigned num_pos = 0, 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)) { + m_ineq_coeffs.push_back(c); + m_ineq_terms.push_back(t); + m_ineq_strict.push_back(is_strict); + if (c.is_pos()) { + ++num_pos; + } + else { + --num_neg; + } + } + else { + new_lits.push_back(lits[i].get()); + } + } + lits.reset(); + lits.append(new_lits); + 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)); + } + } + } + } + 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)); + } + } + } + } + } + + 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 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) { + VERIFY(mdl.eval(m_ineq_terms[i].get(), val)); + VERIFY(a.is_numeral(val, r)); + r /= ac; + 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; + } + + // ax + t <= 0 + // bx + s <= 0 + // a and b have different signs. + // Infer: a|b|x + |b|t + |a|bx + |a|s <= 0 + // e.g. |b|t + |a|s <= 0 + expr_ref mk_lt(unsigned i, unsigned j) { + rational const& ac = m_ineq_coeffs[i]; + rational const& bc = m_ineq_coeffs[j]; + SASSERT(ac.is_pos() != bc.is_pos()); + SASSERT(ac.is_neg() != bc.is_neg()); + expr* t = m_ineq_terms[i].get(); + expr* s = m_ineq_terms[j].get(); + expr_ref bt = mk_mul(abs(bc), t); + expr_ref as = mk_mul(abs(ac), s); + expr_ref ts = mk_add(bt, as); + expr* z = a.mk_numeral(rational(0), m.get_sort(t)); + expr_ref result(m); + if (m_ineq_strict[i] || m_ineq_strict[j]) { + result = a.mk_lt(ts, z); + } + else { + result = a.mk_le(ts, z); + } + return result; + } + + // ax + t <= 0 + // bx + s <= 0 + // a and b have same signs. + // encode:// t/|a| <= s/|b| + // e.g. |b|t <= |a|s + expr_ref mk_le(unsigned i, unsigned j) { + rational const& ac = m_ineq_coeffs[i]; + rational const& bc = m_ineq_coeffs[j]; + SASSERT(ac.is_pos() == bc.is_pos()); + SASSERT(ac.is_neg() == bc.is_neg()); + expr* t = m_ineq_terms[i].get(); + expr* s = m_ineq_terms[j].get(); + expr_ref bt = mk_mul(abs(bc), t); + expr_ref as = mk_mul(abs(ac), s); + if (m_ineq_strict[j] && !m_ineq_strict[i]) { + return expr_ref(a.mk_lt(bt, as), m); + } + else { + return expr_ref(a.mk_le(bt, as), m); + } + } + + + expr_ref mk_add(expr* t1, expr* t2) { + return expr_ref(a.mk_add(t1, t2), m); + } + expr_ref mk_mul(rational const& r, expr* t2) { + expr* t1 = a.mk_numeral(r, m.get_sort(t2)); + return expr_ref(a.mk_mul(t1, t2), m); + } + + public: + arith_project_util(ast_manager& m): + 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) { + expr_ref_vector result(lits); + for (unsigned i = 0; i < vars.size(); ++i) { + project(model, vars[i].get(), result); + } + vars.reset(); + expr_ref res1(m); + expr_ref tmp = qe::mk_and(result); + m_rw(tmp, res1); + return res1; + } + }; + + expr_ref arith_project(model& model, app_ref_vector& vars, expr_ref_vector const& lits) { + ast_manager& m = vars.get_manager(); + arith_project_util ap(m); + return ap(model, vars, lits); + } + +} diff --git a/src/qe/qe_arith.h b/src/qe/qe_arith.h new file mode 100644 index 000000000..230cb36f6 --- /dev/null +++ b/src/qe/qe_arith.h @@ -0,0 +1,16 @@ + +#ifndef __QE_ARITH_H_ +#define __QE_ARITH_H_ + +#include "model.h" + +namespace qe { + /** + Loos-Weispfenning model-based projection for a basic conjunction. + Lits is a vector of literals. + return vector of variables that could not be projected. + */ + expr_ref arith_project(model& model, app_ref_vector& vars, expr_ref_vector const& lits); +}; + +#endif diff --git a/src/test/main.cpp b/src/test/main.cpp index b769b20fd..333456369 100644 --- a/src/test/main.cpp +++ b/src/test/main.cpp @@ -214,6 +214,7 @@ int main(int argc, char ** argv) { TST(quant_solve); TST(rcf); TST(polynorm); + TST(qe_arith); } void initialize_mam() {} diff --git a/src/test/qe_arith.cpp b/src/test/qe_arith.cpp new file mode 100644 index 000000000..a2789ee80 --- /dev/null +++ b/src/test/qe_arith.cpp @@ -0,0 +1,64 @@ +#include "qe_arith.h" +#include "th_rewriter.h" +#include "smt2parser.h" +#include "arith_decl_plugin.h" +#include "reg_decl_plugins.h" +#include "arith_rewriter.h" +#include "ast_pp.h" +#include "qe_util.h" +#include "smt_context.h" + + +static expr_ref parse_fml(ast_manager& m, char const* str) { + expr_ref result(m); + cmd_context ctx(false, &m); + ctx.set_ignore_check(true); + std::ostringstream buffer; + buffer << "(declare-const x Real)\n" + << "(declare-const y Real)\n" + << "(declare-const z Real)\n" + << "(declare-const a Real)\n" + << "(declare-const b Real)\n" + << "(assert " << str << ")\n"; + std::istringstream is(buffer.str()); + VERIFY(parse_smt2_commands(ctx, is)); + SASSERT(ctx.begin_assertions() != ctx.end_assertions()); + result = *ctx.begin_assertions(); + return result; +} + +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 void test(char const *ex) { + smt_params params; + params.m_model = true; + ast_manager m; + reg_decl_plugins(m); + arith_util a(m); + expr_ref fml = parse_fml(m, ex); + app_ref_vector vars(m); + expr_ref_vector lits(m); + vars.push_back(m.mk_const(symbol("x"), a.mk_real())); + qe::flatten_and(fml, lits); + + smt::context ctx(m, params); + ctx.assert_expr(fml); + lbool result = ctx.check(); + SASSERT(result == l_true); + ref md; + ctx.get_model(md); + expr_ref pr = qe::arith_project(*md, vars, lits); + + std::cout << mk_pp(fml, m) << "\n"; + std::cout << mk_pp(pr, m) << "\n"; +} + +void tst_qe_arith() { + test(example1); + test(example2); + test(example3); + test(example4); +}