mirror of
https://github.com/Z3Prover/z3
synced 2025-04-15 05:18:44 +00:00
add normalizer of monomial coefficients
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner
parent
c2b26300fb
commit
d94f1b3fd6
|
|
@ -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<arith_rewriter_core> {
|
||||
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<arith_rewriter_core>(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> {
|
||||
arith_normalizer_cfg m_cfg;
|
||||
public:
|
||||
arith_normalizer_star(ast_manager & m, params_ref const & p):
|
||||
rewriter_tpl<arith_normalizer_cfg>(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<pdr::ite_hoister_cfg>;
|
||||
|
|
|
|||
|
|
@ -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);
|
||||
|
|
|
|||
|
|
@ -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";
|
||||
}
|
||||
|
|
|
|||
Loading…
Reference in a new issue