diff --git a/src/muz_qe/pdr_util.cpp b/src/muz_qe/pdr_util.cpp index 9711cffc2..169eeec72 100644 --- a/src/muz_qe/pdr_util.cpp +++ b/src/muz_qe/pdr_util.cpp @@ -42,6 +42,10 @@ Notes: #include "arith_decl_plugin.h" #include "expr_replacer.h" #include "model_smt2_pp.h" +#include "poly_rewriter.h" +#include "poly_rewriter_def.h" +#include "arith_rewriter.h" + namespace pdr { @@ -1278,6 +1282,151 @@ namespace pdr { return test.is_dl(); } + class arith_normalizer : public poly_rewriter { + ast_manager& m; + arith_util m_util; + enum op_kind { LE, GE, EQ }; + public: + arith_normalizer(ast_manager& m, params_ref const& p = params_ref()): poly_rewriter(m, p), m(m), m_util(m) {} + + br_status mk_app_core(func_decl* f, unsigned num_args, expr* const* args, expr_ref& result) { + br_status st = BR_FAILED; + if (m.is_eq(f)) { + SASSERT(num_args == 2); return mk_eq_core(args[0], args[1], result); + } + + if (f->get_family_id() != get_fid()) { + return st; + } + switch (f->get_decl_kind()) { + case OP_NUM: st = BR_FAILED; break; + case OP_IRRATIONAL_ALGEBRAIC_NUM: st = BR_FAILED; break; + case OP_LE: SASSERT(num_args == 2); st = mk_le_core(args[0], args[1], result); break; + case OP_GE: SASSERT(num_args == 2); st = mk_ge_core(args[0], args[1], result); break; + case OP_LT: SASSERT(num_args == 2); st = mk_lt_core(args[0], args[1], result); break; + case OP_GT: SASSERT(num_args == 2); st = mk_gt_core(args[0], args[1], result); break; + default: st = BR_FAILED; break; + } + return st; + } + + private: + + br_status mk_eq_core(expr* arg1, expr* arg2, expr_ref& result) { + return mk_le_ge_eq_core(arg1, arg2, EQ, result); + } + br_status mk_le_core(expr* arg1, expr* arg2, expr_ref& result) { + return mk_le_ge_eq_core(arg1, arg2, LE, result); + } + br_status mk_ge_core(expr* arg1, expr* arg2, expr_ref& result) { + return mk_le_ge_eq_core(arg1, arg2, GE, result); + } + br_status mk_lt_core(expr* arg1, expr* arg2, expr_ref& result) { + result = m.mk_not(m_util.mk_ge(arg1, arg2)); + return BR_REWRITE2; + } + br_status mk_gt_core(expr* arg1, expr* arg2, expr_ref& result) { + result = m.mk_not(m_util.mk_le(arg1, arg2)); + return BR_REWRITE2; + } + + br_status mk_le_ge_eq_core(expr* arg1, expr* arg2, op_kind kind, expr_ref& result) { + if (m_util.is_real(arg1)) { + numeral g(0); + get_coeffs(arg1, g); + get_coeffs(arg2, g); + if (!g.is_one() && !g.is_zero()) { + SASSERT(g.is_pos()); + expr_ref new_arg1 = rdiv_polynomial(arg1, g); + expr_ref new_arg2 = rdiv_polynomial(arg2, g); + switch(kind) { + case LE: result = m_util.mk_le(new_arg1, new_arg2); return BR_DONE; + case GE: result = m_util.mk_ge(new_arg1, new_arg2); return BR_DONE; + case EQ: result = m_util.mk_eq(new_arg1, new_arg2); return BR_DONE; + } + } + } + return BR_FAILED; + } + + void update_coeff(numeral const& r, numeral& g) { + if (g.is_zero() || abs(r) < g) { + g = abs(r); + } + } + + void get_coeffs(expr* e, numeral& g) { + rational r; + unsigned sz; + expr* const* args = get_monomials(e, sz); + for (unsigned i = 0; i < sz; ++i) { + expr* arg = args[i]; + if (!m_util.is_numeral(arg, r)) { + get_power_product(arg, r); + } + update_coeff(r, g); + } + } + + expr_ref rdiv_polynomial(expr* e, numeral const& g) { + rational r; + SASSERT(g.is_pos()); + SASSERT(!g.is_one()); + expr_ref_vector monomes(m); + unsigned sz; + expr* const* args = get_monomials(e, sz); + for (unsigned i = 0; i < sz; ++i) { + expr* arg = args[i]; + if (m_util.is_numeral(arg, r)) { + monomes.push_back(m_util.mk_numeral(r/g, false)); + } + else { + expr* p = get_power_product(arg, r); + r /= g; + if (r.is_one()) { + monomes.push_back(p); + } + else { + monomes.push_back(m_util.mk_mul(m_util.mk_numeral(r, false), p)); + } + } + } + expr_ref result(m); + mk_add(monomes.size(), monomes.c_ptr(), result); + return result; + } + + }; + + + struct arith_normalizer_cfg: public default_rewriter_cfg { + arith_normalizer m_r; + bool rewrite_patterns() const { return false; } + br_status reduce_app(func_decl * f, unsigned num, expr * const * args, expr_ref & result, proof_ref & result_pr) { + return m_r.mk_app_core(f, num, args, result); + } + arith_normalizer_cfg(ast_manager & m, params_ref const & p):m_r(m,p) {} + }; + + class arith_normalizer_star : public rewriter_tpl { + arith_normalizer_cfg m_cfg; + public: + arith_normalizer_star(ast_manager & m, params_ref const & p): + rewriter_tpl(m, false, m_cfg), + m_cfg(m, p) {} + }; + + + void normalize_arithmetic(expr_ref& t) { + ast_manager& m = t.get_manager(); + datalog::scoped_no_proof _sp(m); + params_ref p; + arith_normalizer_star rw(m, p); + expr_ref tmp(m); + rw(t, tmp); + t = tmp; + } + } template class rewriter_tpl; diff --git a/src/muz_qe/pdr_util.h b/src/muz_qe/pdr_util.h index 5f2d22b76..67be6751b 100644 --- a/src/muz_qe/pdr_util.h +++ b/src/muz_qe/pdr_util.h @@ -142,6 +142,7 @@ namespace pdr { Assumption: the model satisfies the conjunctions. */ void reduce_disequalities(model& model, unsigned threshold, expr_ref& fml); + /** @@ -149,6 +150,16 @@ namespace pdr { */ void hoist_non_bool_if(expr_ref& fml); + + /** + \brief normalize coefficients in polynomials so that least coefficient is 1. + */ + void normalize_arithmetic(expr_ref& t); + + + /** + \brief determine if formulas belong to difference logic or UTVPI fragment. + */ bool is_difference_logic(ast_manager& m, unsigned num_fmls, expr* const* fmls); bool is_utvpi_logic(ast_manager& m, unsigned num_fmls, expr* const* fmls); diff --git a/src/test/arith_rewriter.cpp b/src/test/arith_rewriter.cpp index 0933e9d11..9eb9e559b 100644 --- a/src/test/arith_rewriter.cpp +++ b/src/test/arith_rewriter.cpp @@ -2,6 +2,33 @@ #include "bv_decl_plugin.h" #include "ast_pp.h" #include "reg_decl_plugins.h" +#include "th_rewriter.h" +#include "model.h" +#include "pdr_util.h" +#include "smt2parser.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 = "(<= (+ (* 1.3 x y) (* 2.3 y y) (* (- 1.1 x x))) 2.2)"; +static char const* example2 = "(= (+ 4 3 (- (* 3 x x) (* 5 y)) y) 0)"; + void tst_arith_rewriter() { ast_manager m; @@ -14,4 +41,19 @@ void tst_arith_rewriter() { expr* args[2] = { t1, t2 }; ar.mk_mul(2, args, result); std::cout << mk_pp(result, m) << "\n"; + + + th_rewriter rw(m); + expr_ref fml = parse_fml(m, example1); + rw(fml); + std::cout << mk_pp(fml, m) << "\n"; + pdr::normalize_arithmetic(fml); + std::cout << mk_pp(fml, m) << "\n"; + + + fml = parse_fml(m, example2); + rw(fml); + std::cout << mk_pp(fml, m) << "\n"; + pdr::normalize_arithmetic(fml); + std::cout << mk_pp(fml, m) << "\n"; }