mirror of
https://github.com/Z3Prover/z3
synced 2025-04-08 18:31:49 +00:00
merge
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
commit
6969e6024b
|
@ -1727,7 +1727,6 @@ ast * ast_manager::register_node_core(ast * n) {
|
|||
|
||||
n->m_id = is_decl(n) ? m_decl_id_gen.mk() : m_expr_id_gen.mk();
|
||||
|
||||
|
||||
TRACE("ast", tout << "Object " << n->m_id << " was created.\n";);
|
||||
TRACE("mk_var_bug", tout << "mk_ast: " << n->m_id << "\n";);
|
||||
// increment reference counters
|
||||
|
|
|
@ -37,23 +37,6 @@ macro_util::macro_util(ast_manager & m):
|
|||
m_curr_clause(0) {
|
||||
}
|
||||
|
||||
#if 0
|
||||
arith_simplifier_plugin * macro_util::get_arith_simp() const {
|
||||
if (m_arith_simp == 0) {
|
||||
const_cast<macro_util*>(this)->m_arith_simp = static_cast<arith_simplifier_plugin*>(m_simplifier.get_plugin(m_manager.mk_family_id("arith")));
|
||||
}
|
||||
SASSERT(m_arith_simp != 0);
|
||||
return m_arith_simp;
|
||||
}
|
||||
|
||||
bv_simplifier_plugin * macro_util::get_bv_simp() const {
|
||||
if (m_bv_simp == 0) {
|
||||
const_cast<macro_util*>(this)->m_bv_simp = static_cast<bv_simplifier_plugin*>(m_simplifier.get_plugin(m_manager.mk_family_id("bv")));
|
||||
}
|
||||
SASSERT(m_bv_simp != 0);
|
||||
return m_bv_simp;
|
||||
}
|
||||
#endif
|
||||
|
||||
bool macro_util::is_bv(expr * n) const {
|
||||
return m_bv.is_bv(n);
|
||||
|
|
468
src/ast/simplifier/arith_simplifier_plugin.cpp
Normal file
468
src/ast/simplifier/arith_simplifier_plugin.cpp
Normal file
|
@ -0,0 +1,468 @@
|
|||
/*++
|
||||
Copyright (c) 2007 Microsoft Corporation
|
||||
|
||||
Module Name:
|
||||
|
||||
arith_simplifier_plugin.cpp
|
||||
|
||||
Abstract:
|
||||
|
||||
Simplifier for the arithmetic family.
|
||||
|
||||
Author:
|
||||
|
||||
Leonardo (leonardo) 2008-01-08
|
||||
|
||||
--*/
|
||||
#include "ast/simplifier/arith_simplifier_plugin.h"
|
||||
#include "ast/ast_pp.h"
|
||||
#include "ast/ast_ll_pp.h"
|
||||
#include "ast/ast_smt2_pp.h"
|
||||
|
||||
arith_simplifier_plugin::~arith_simplifier_plugin() {
|
||||
}
|
||||
|
||||
arith_simplifier_plugin::arith_simplifier_plugin(ast_manager & m, basic_simplifier_plugin & b, arith_simplifier_params & p):
|
||||
poly_simplifier_plugin(symbol("arith"), m, OP_ADD, OP_MUL, OP_UMINUS, OP_SUB, OP_NUM),
|
||||
m_params(p),
|
||||
m_util(m),
|
||||
m_bsimp(b),
|
||||
m_int_zero(m),
|
||||
m_real_zero(m) {
|
||||
m_int_zero = m_util.mk_numeral(rational(0), true);
|
||||
m_real_zero = m_util.mk_numeral(rational(0), false);
|
||||
}
|
||||
|
||||
/**
|
||||
\brief Return true if the first monomial of t is negative.
|
||||
*/
|
||||
bool arith_simplifier_plugin::is_neg_poly(expr * t) const {
|
||||
if (m_util.is_add(t)) {
|
||||
t = to_app(t)->get_arg(0);
|
||||
}
|
||||
if (m_util.is_mul(t)) {
|
||||
t = to_app(t)->get_arg(0);
|
||||
rational r;
|
||||
if (is_numeral(t, r))
|
||||
return r.is_neg();
|
||||
}
|
||||
return false;
|
||||
}
|
||||
|
||||
void arith_simplifier_plugin::get_monomial_gcd(expr_ref_vector& monomials, numeral& g) {
|
||||
g = numeral::zero();
|
||||
numeral n;
|
||||
for (unsigned i = 0; !g.is_one() && i < monomials.size(); ++i) {
|
||||
expr* e = monomials[i].get();
|
||||
if (is_numeral(e, n)) {
|
||||
g = gcd(abs(n), g);
|
||||
}
|
||||
else if (is_mul(e) && is_numeral(to_app(e)->get_arg(0), n)) {
|
||||
g = gcd(abs(n), g);
|
||||
}
|
||||
else {
|
||||
g = numeral::one();
|
||||
return;
|
||||
}
|
||||
}
|
||||
if (g.is_zero()) {
|
||||
g = numeral::one();
|
||||
}
|
||||
}
|
||||
|
||||
void arith_simplifier_plugin::div_monomial(expr_ref_vector& monomials, numeral const& g) {
|
||||
numeral n;
|
||||
for (unsigned i = 0; i < monomials.size(); ++i) {
|
||||
expr* e = monomials[i].get();
|
||||
if (is_numeral(e, n)) {
|
||||
SASSERT((n/g).is_int());
|
||||
monomials[i] = mk_numeral(n/g);
|
||||
}
|
||||
else if (is_mul(e) && is_numeral(to_app(e)->get_arg(0), n)) {
|
||||
SASSERT((n/g).is_int());
|
||||
monomials[i] = mk_mul(n/g, to_app(e)->get_arg(1));
|
||||
}
|
||||
else {
|
||||
UNREACHABLE();
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
void arith_simplifier_plugin::gcd_reduce_monomial(expr_ref_vector& monomials, numeral& k) {
|
||||
numeral g, n;
|
||||
|
||||
get_monomial_gcd(monomials, g);
|
||||
g = gcd(abs(k), g);
|
||||
|
||||
if (g.is_one()) {
|
||||
return;
|
||||
}
|
||||
SASSERT(g.is_pos());
|
||||
|
||||
k = k / g;
|
||||
div_monomial(monomials, g);
|
||||
|
||||
}
|
||||
|
||||
template<arith_simplifier_plugin::op_kind Kind>
|
||||
void arith_simplifier_plugin::mk_le_ge_eq_core(expr * arg1, expr * arg2, expr_ref & result) {
|
||||
set_curr_sort(arg1);
|
||||
bool is_int = m_curr_sort->get_decl_kind() == INT_SORT;
|
||||
expr_ref_vector monomials(m_manager);
|
||||
rational k;
|
||||
TRACE("arith_eq_bug", tout << mk_ismt2_pp(arg1, m_manager) << "\n" << mk_ismt2_pp(arg2, m_manager) << "\n";);
|
||||
process_sum_of_monomials(false, arg1, monomials, k);
|
||||
process_sum_of_monomials(true, arg2, monomials, k);
|
||||
k.neg();
|
||||
if (is_int) {
|
||||
numeral g;
|
||||
get_monomial_gcd(monomials, g);
|
||||
if (!g.is_one()) {
|
||||
div_monomial(monomials, g);
|
||||
switch(Kind) {
|
||||
case LE:
|
||||
//
|
||||
// g*monmials' <= k
|
||||
// <=>
|
||||
// monomials' <= floor(k/g)
|
||||
//
|
||||
k = floor(k/g);
|
||||
break;
|
||||
case GE:
|
||||
//
|
||||
// g*monmials' >= k
|
||||
// <=>
|
||||
// monomials' >= ceil(k/g)
|
||||
//
|
||||
k = ceil(k/g);
|
||||
break;
|
||||
case EQ:
|
||||
k = k/g;
|
||||
if (!k.is_int()) {
|
||||
result = m_manager.mk_false();
|
||||
return;
|
||||
}
|
||||
break;
|
||||
}
|
||||
}
|
||||
}
|
||||
expr_ref lhs(m_manager);
|
||||
mk_sum_of_monomials(monomials, lhs);
|
||||
if (m_util.is_numeral(lhs)) {
|
||||
SASSERT(lhs == mk_zero());
|
||||
if (( Kind == LE && numeral::zero() <= k) ||
|
||||
( Kind == GE && numeral::zero() >= k) ||
|
||||
( Kind == EQ && numeral::zero() == k))
|
||||
result = m_manager.mk_true();
|
||||
else
|
||||
result = m_manager.mk_false();
|
||||
}
|
||||
else {
|
||||
|
||||
if (is_neg_poly(lhs)) {
|
||||
expr_ref neg_lhs(m_manager);
|
||||
mk_uminus(lhs, neg_lhs);
|
||||
lhs = neg_lhs;
|
||||
k.neg();
|
||||
expr * rhs = m_util.mk_numeral(k, is_int);
|
||||
switch (Kind) {
|
||||
case LE:
|
||||
result = m_util.mk_ge(lhs, rhs);
|
||||
break;
|
||||
case GE:
|
||||
result = m_util.mk_le(lhs, rhs);
|
||||
break;
|
||||
case EQ:
|
||||
result = m_manager.mk_eq(lhs, rhs);
|
||||
break;
|
||||
}
|
||||
}
|
||||
else {
|
||||
expr * rhs = m_util.mk_numeral(k, is_int);
|
||||
switch (Kind) {
|
||||
case LE:
|
||||
result = m_util.mk_le(lhs, rhs);
|
||||
break;
|
||||
case GE:
|
||||
result = m_util.mk_ge(lhs, rhs);
|
||||
break;
|
||||
case EQ:
|
||||
result = m_manager.mk_eq(lhs, rhs);
|
||||
break;
|
||||
}
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
void arith_simplifier_plugin::mk_arith_eq(expr * arg1, expr * arg2, expr_ref & result) {
|
||||
mk_le_ge_eq_core<EQ>(arg1, arg2, result);
|
||||
}
|
||||
|
||||
void arith_simplifier_plugin::mk_le(expr * arg1, expr * arg2, expr_ref & result) {
|
||||
mk_le_ge_eq_core<LE>(arg1, arg2, result);
|
||||
}
|
||||
|
||||
void arith_simplifier_plugin::mk_ge(expr * arg1, expr * arg2, expr_ref & result) {
|
||||
mk_le_ge_eq_core<GE>(arg1, arg2, result);
|
||||
}
|
||||
|
||||
void arith_simplifier_plugin::mk_lt(expr * arg1, expr * arg2, expr_ref & result) {
|
||||
expr_ref tmp(m_manager);
|
||||
mk_le(arg2, arg1, tmp);
|
||||
m_bsimp.mk_not(tmp, result);
|
||||
}
|
||||
|
||||
void arith_simplifier_plugin::mk_gt(expr * arg1, expr * arg2, expr_ref & result) {
|
||||
expr_ref tmp(m_manager);
|
||||
mk_le(arg1, arg2, tmp);
|
||||
m_bsimp.mk_not(tmp, result);
|
||||
}
|
||||
|
||||
void arith_simplifier_plugin::gcd_normalize(numeral & coeff, expr_ref& term) {
|
||||
if (!abs(coeff).is_one()) {
|
||||
set_curr_sort(term);
|
||||
SASSERT(m_curr_sort->get_decl_kind() == INT_SORT);
|
||||
expr_ref_vector monomials(m_manager);
|
||||
rational k;
|
||||
monomials.push_back(mk_numeral(numeral(coeff), true));
|
||||
process_sum_of_monomials(false, term, monomials, k);
|
||||
gcd_reduce_monomial(monomials, k);
|
||||
numeral coeff1;
|
||||
if (!is_numeral(monomials[0].get(), coeff1)) {
|
||||
UNREACHABLE();
|
||||
}
|
||||
if (coeff1 == coeff) {
|
||||
return;
|
||||
}
|
||||
monomials[0] = mk_numeral(k, true);
|
||||
coeff = coeff1;
|
||||
mk_sum_of_monomials(monomials, term);
|
||||
}
|
||||
}
|
||||
|
||||
|
||||
void arith_simplifier_plugin::mk_div(expr * arg1, expr * arg2, expr_ref & result) {
|
||||
set_curr_sort(arg1);
|
||||
numeral v1, v2;
|
||||
bool is_int;
|
||||
if (m_util.is_numeral(arg2, v2, is_int) && !v2.is_zero()) {
|
||||
SASSERT(!is_int);
|
||||
if (m_util.is_numeral(arg1, v1, is_int))
|
||||
result = m_util.mk_numeral(v1/v2, false);
|
||||
else {
|
||||
numeral k(1);
|
||||
k /= v2;
|
||||
|
||||
expr_ref inv_arg2(m_util.mk_numeral(k, false), m_manager);
|
||||
mk_mul(inv_arg2, arg1, result);
|
||||
}
|
||||
}
|
||||
else
|
||||
result = m_util.mk_div(arg1, arg2);
|
||||
}
|
||||
|
||||
void arith_simplifier_plugin::mk_idiv(expr * arg1, expr * arg2, expr_ref & result) {
|
||||
set_curr_sort(arg1);
|
||||
numeral v1, v2;
|
||||
bool is_int;
|
||||
if (m_util.is_numeral(arg1, v1, is_int) && m_util.is_numeral(arg2, v2, is_int) && !v2.is_zero())
|
||||
result = m_util.mk_numeral(div(v1, v2), is_int);
|
||||
else
|
||||
result = m_util.mk_idiv(arg1, arg2);
|
||||
}
|
||||
|
||||
void arith_simplifier_plugin::prop_mod_const(expr * e, unsigned depth, numeral const& k, expr_ref& result) {
|
||||
SASSERT(m_util.is_int(e));
|
||||
SASSERT(k.is_int() && k.is_pos());
|
||||
numeral n;
|
||||
bool is_int;
|
||||
|
||||
if (depth == 0) {
|
||||
result = e;
|
||||
}
|
||||
else if (is_add(e) || is_mul(e)) {
|
||||
expr_ref_vector args(m_manager);
|
||||
expr_ref tmp(m_manager);
|
||||
app* a = to_app(e);
|
||||
for (unsigned i = 0; i < a->get_num_args(); ++i) {
|
||||
prop_mod_const(a->get_arg(i), depth - 1, k, tmp);
|
||||
args.push_back(tmp);
|
||||
}
|
||||
reduce(a->get_decl(), args.size(), args.c_ptr(), result);
|
||||
}
|
||||
else if (m_util.is_numeral(e, n, is_int) && is_int) {
|
||||
result = mk_numeral(mod(n, k), true);
|
||||
}
|
||||
else {
|
||||
result = e;
|
||||
}
|
||||
}
|
||||
|
||||
void arith_simplifier_plugin::mk_mod(expr * arg1, expr * arg2, expr_ref & result) {
|
||||
set_curr_sort(arg1);
|
||||
numeral v1, v2;
|
||||
bool is_int;
|
||||
if (m_util.is_numeral(arg1, v1, is_int) && m_util.is_numeral(arg2, v2, is_int) && !v2.is_zero()) {
|
||||
result = m_util.mk_numeral(mod(v1, v2), is_int);
|
||||
}
|
||||
else if (m_util.is_numeral(arg2, v2, is_int) && is_int && v2.is_one()) {
|
||||
result = m_util.mk_numeral(numeral(0), true);
|
||||
}
|
||||
else if (m_util.is_numeral(arg2, v2, is_int) && is_int && v2.is_pos()) {
|
||||
expr_ref tmp(m_manager);
|
||||
prop_mod_const(arg1, 5, v2, tmp);
|
||||
result = m_util.mk_mod(tmp, arg2);
|
||||
}
|
||||
else {
|
||||
result = m_util.mk_mod(arg1, arg2);
|
||||
}
|
||||
}
|
||||
|
||||
void arith_simplifier_plugin::mk_rem(expr * arg1, expr * arg2, expr_ref & result) {
|
||||
set_curr_sort(arg1);
|
||||
numeral v1, v2;
|
||||
bool is_int;
|
||||
if (m_util.is_numeral(arg1, v1, is_int) && m_util.is_numeral(arg2, v2, is_int) && !v2.is_zero()) {
|
||||
numeral m = mod(v1, v2);
|
||||
//
|
||||
// rem(v1,v2) = if v2 >= 0 then mod(v1,v2) else -mod(v1,v2)
|
||||
//
|
||||
if (v2.is_neg()) {
|
||||
m.neg();
|
||||
}
|
||||
result = m_util.mk_numeral(m, is_int);
|
||||
}
|
||||
else if (m_util.is_numeral(arg2, v2, is_int) && is_int && v2.is_one()) {
|
||||
result = m_util.mk_numeral(numeral(0), true);
|
||||
}
|
||||
else if (m_util.is_numeral(arg2, v2, is_int) && is_int && !v2.is_zero()) {
|
||||
expr_ref tmp(m_manager);
|
||||
prop_mod_const(arg1, 5, v2, tmp);
|
||||
result = m_util.mk_mod(tmp, arg2);
|
||||
if (v2.is_neg()) {
|
||||
result = m_util.mk_uminus(result);
|
||||
}
|
||||
}
|
||||
else {
|
||||
result = m_util.mk_rem(arg1, arg2);
|
||||
}
|
||||
}
|
||||
|
||||
void arith_simplifier_plugin::mk_to_real(expr * arg, expr_ref & result) {
|
||||
numeral v;
|
||||
if (m_util.is_numeral(arg, v))
|
||||
result = m_util.mk_numeral(v, false);
|
||||
else
|
||||
result = m_util.mk_to_real(arg);
|
||||
}
|
||||
|
||||
void arith_simplifier_plugin::mk_to_int(expr * arg, expr_ref & result) {
|
||||
numeral v;
|
||||
if (m_util.is_numeral(arg, v))
|
||||
result = m_util.mk_numeral(floor(v), true);
|
||||
else if (m_util.is_to_real(arg))
|
||||
result = to_app(arg)->get_arg(0);
|
||||
else
|
||||
result = m_util.mk_to_int(arg);
|
||||
}
|
||||
|
||||
void arith_simplifier_plugin::mk_is_int(expr * arg, expr_ref & result) {
|
||||
numeral v;
|
||||
if (m_util.is_numeral(arg, v))
|
||||
result = v.is_int()?m_manager.mk_true():m_manager.mk_false();
|
||||
else if (m_util.is_to_real(arg))
|
||||
result = m_manager.mk_true();
|
||||
else
|
||||
result = m_util.mk_is_int(arg);
|
||||
}
|
||||
|
||||
bool arith_simplifier_plugin::reduce(func_decl * f, unsigned num_args, expr * const * args, expr_ref & result) {
|
||||
set_reduce_invoked();
|
||||
SASSERT(f->get_family_id() == m_fid);
|
||||
TRACE("arith_simplifier_plugin", tout << mk_pp(f, m_manager) << "\n";
|
||||
for (unsigned i = 0; i < num_args; i++) tout << mk_pp(args[i], m_manager) << "\n";);
|
||||
arith_op_kind k = static_cast<arith_op_kind>(f->get_decl_kind());
|
||||
switch (k) {
|
||||
case OP_NUM: return false;
|
||||
case OP_LE: if (m_presimp) return false; SASSERT(num_args == 2); mk_le(args[0], args[1], result); break;
|
||||
case OP_GE: if (m_presimp) return false; SASSERT(num_args == 2); mk_ge(args[0], args[1], result); break;
|
||||
case OP_LT: if (m_presimp) return false; SASSERT(num_args == 2); mk_lt(args[0], args[1], result); break;
|
||||
case OP_GT: if (m_presimp) return false; SASSERT(num_args == 2); mk_gt(args[0], args[1], result); break;
|
||||
case OP_ADD: mk_add(num_args, args, result); break;
|
||||
case OP_SUB: mk_sub(num_args, args, result); break;
|
||||
case OP_UMINUS: SASSERT(num_args == 1); mk_uminus(args[0], result); break;
|
||||
case OP_MUL:
|
||||
mk_mul(num_args, args, result);
|
||||
TRACE("arith_simplifier_plugin", tout << mk_pp(result, m_manager) << "\n";);
|
||||
break;
|
||||
case OP_DIV: SASSERT(num_args == 2); mk_div(args[0], args[1], result); break;
|
||||
case OP_IDIV: SASSERT(num_args == 2); mk_idiv(args[0], args[1], result); break;
|
||||
case OP_REM: SASSERT(num_args == 2); mk_rem(args[0], args[1], result); break;
|
||||
case OP_MOD: SASSERT(num_args == 2); mk_mod(args[0], args[1], result); break;
|
||||
case OP_TO_REAL: SASSERT(num_args == 1); mk_to_real(args[0], result); break;
|
||||
case OP_TO_INT: SASSERT(num_args == 1); mk_to_int(args[0], result); break;
|
||||
case OP_IS_INT: SASSERT(num_args == 1); mk_is_int(args[0], result); break;
|
||||
case OP_POWER: SASSERT(num_args == 2); mk_power(args[0], args[1], result); break;
|
||||
case OP_ABS: SASSERT(num_args == 1); mk_abs(args[0], result); break;
|
||||
case OP_IRRATIONAL_ALGEBRAIC_NUM: return false;
|
||||
default:
|
||||
return false;
|
||||
}
|
||||
TRACE("arith_simplifier_plugin", tout << mk_pp(result.get(), m_manager) << "\n";);
|
||||
return true;
|
||||
}
|
||||
|
||||
void arith_simplifier_plugin::mk_power(expr* x, expr* y, expr_ref& result) {
|
||||
rational a, b;
|
||||
if (is_numeral(y, b) && b.is_one()) {
|
||||
result = x;
|
||||
return;
|
||||
}
|
||||
if (is_numeral(x, a) && is_numeral(y, b) && b.is_unsigned()) {
|
||||
if (b.is_zero() && !a.is_zero()) {
|
||||
result = m_util.mk_numeral(rational(1), m_manager.get_sort(x));
|
||||
return;
|
||||
}
|
||||
if (!b.is_zero()) {
|
||||
result = m_util.mk_numeral(power(a, b.get_unsigned()), m_manager.get_sort(x));
|
||||
return;
|
||||
}
|
||||
}
|
||||
result = m_util.mk_power(x, y);
|
||||
}
|
||||
|
||||
void arith_simplifier_plugin::mk_abs(expr * arg, expr_ref & result) {
|
||||
expr_ref c(m_manager);
|
||||
expr_ref m_arg(m_manager);
|
||||
mk_uminus(arg, m_arg);
|
||||
mk_ge(arg, m_util.mk_numeral(rational(0), m_util.is_int(arg)), c);
|
||||
m_bsimp.mk_ite(c, arg, m_arg, result);
|
||||
}
|
||||
|
||||
bool arith_simplifier_plugin::is_arith_term(expr * n) const {
|
||||
return n->get_kind() == AST_APP && to_app(n)->get_family_id() == m_fid;
|
||||
}
|
||||
|
||||
bool arith_simplifier_plugin::reduce_eq(expr * lhs, expr * rhs, expr_ref & result) {
|
||||
TRACE("reduce_eq_bug", tout << mk_ismt2_pp(lhs, m_manager) << "\n" << mk_ismt2_pp(rhs, m_manager) << "\n";);
|
||||
set_reduce_invoked();
|
||||
if (m_presimp) {
|
||||
return false;
|
||||
}
|
||||
if (m_params.m_arith_expand_eqs) {
|
||||
expr_ref le(m_manager), ge(m_manager);
|
||||
mk_le_ge_eq_core<LE>(lhs, rhs, le);
|
||||
mk_le_ge_eq_core<GE>(lhs, rhs, ge);
|
||||
m_bsimp.mk_and(le, ge, result);
|
||||
return true;
|
||||
}
|
||||
|
||||
if (m_params.m_arith_process_all_eqs || is_arith_term(lhs) || is_arith_term(rhs)) {
|
||||
mk_arith_eq(lhs, rhs, result);
|
||||
return true;
|
||||
}
|
||||
return false;
|
||||
}
|
||||
|
||||
|
||||
|
97
src/ast/simplifier/arith_simplifier_plugin.h
Normal file
97
src/ast/simplifier/arith_simplifier_plugin.h
Normal file
|
@ -0,0 +1,97 @@
|
|||
/*++
|
||||
Copyright (c) 2007 Microsoft Corporation
|
||||
|
||||
Module Name:
|
||||
|
||||
arith_simplifier_plugin.h
|
||||
|
||||
Abstract:
|
||||
|
||||
Simplifier for the arithmetic family.
|
||||
|
||||
Author:
|
||||
|
||||
Leonardo (leonardo) 2008-01-08
|
||||
|
||||
--*/
|
||||
#ifndef ARITH_SIMPLIFIER_PLUGIN_H_
|
||||
#define ARITH_SIMPLIFIER_PLUGIN_H_
|
||||
|
||||
#include "ast/simplifier/basic_simplifier_plugin.h"
|
||||
#include "ast/simplifier/poly_simplifier_plugin.h"
|
||||
#include "ast/arith_decl_plugin.h"
|
||||
#include "ast/simplifier/arith_simplifier_params.h"
|
||||
|
||||
/**
|
||||
\brief Simplifier for the arith family.
|
||||
*/
|
||||
class arith_simplifier_plugin : public poly_simplifier_plugin {
|
||||
public:
|
||||
enum op_kind {
|
||||
LE, GE, EQ
|
||||
};
|
||||
protected:
|
||||
arith_simplifier_params & m_params;
|
||||
arith_util m_util;
|
||||
basic_simplifier_plugin & m_bsimp;
|
||||
expr_ref m_int_zero;
|
||||
expr_ref m_real_zero;
|
||||
|
||||
bool is_neg_poly(expr * t) const;
|
||||
|
||||
template<op_kind k>
|
||||
void mk_le_ge_eq_core(expr * arg1, expr * arg2, expr_ref & result);
|
||||
|
||||
void prop_mod_const(expr * e, unsigned depth, numeral const& k, expr_ref& result);
|
||||
|
||||
void gcd_reduce_monomial(expr_ref_vector& monomials, numeral& k);
|
||||
|
||||
void div_monomial(expr_ref_vector& monomials, numeral const& g);
|
||||
void get_monomial_gcd(expr_ref_vector& monomials, numeral& g);
|
||||
|
||||
public:
|
||||
arith_simplifier_plugin(ast_manager & m, basic_simplifier_plugin & b, arith_simplifier_params & p);
|
||||
~arith_simplifier_plugin();
|
||||
arith_util & get_arith_util() { return m_util; }
|
||||
virtual numeral norm(const numeral & n) { return n; }
|
||||
virtual bool is_numeral(expr * n, rational & val) const { bool f; return m_util.is_numeral(n, val, f); }
|
||||
bool is_numeral(expr * n) const { return m_util.is_numeral(n); }
|
||||
virtual bool is_minus_one(expr * n) const { numeral tmp; return is_numeral(n, tmp) && tmp.is_minus_one(); }
|
||||
virtual expr * get_zero(sort * s) const { return m_util.is_int(s) ? m_int_zero.get() : m_real_zero.get(); }
|
||||
|
||||
virtual app * mk_numeral(numeral const & n) { return m_util.mk_numeral(n, m_curr_sort->get_decl_kind() == INT_SORT); }
|
||||
app * mk_numeral(numeral const & n, bool is_int) { return m_util.mk_numeral(n, is_int); }
|
||||
bool is_int_sort(sort const * s) const { return m_util.is_int(s); }
|
||||
bool is_real_sort(sort const * s) const { return m_util.is_real(s); }
|
||||
bool is_arith_sort(sort const * s) const { return is_int_sort(s) || is_real_sort(s); }
|
||||
bool is_int(expr const * n) const { return m_util.is_int(n); }
|
||||
bool is_le(expr const * n) const { return m_util.is_le(n); }
|
||||
bool is_ge(expr const * n) const { return m_util.is_ge(n); }
|
||||
|
||||
virtual bool is_le_ge(expr * n) const { return is_le(n) || is_ge(n); }
|
||||
|
||||
void mk_le(expr * arg1, expr * arg2, expr_ref & result);
|
||||
void mk_ge(expr * arg1, expr * arg2, expr_ref & result);
|
||||
void mk_lt(expr * arg1, expr * arg2, expr_ref & result);
|
||||
void mk_gt(expr * arg1, expr * arg2, expr_ref & result);
|
||||
void mk_arith_eq(expr * arg1, expr * arg2, expr_ref & result);
|
||||
void mk_div(expr * arg1, expr * arg2, expr_ref & result);
|
||||
void mk_idiv(expr * arg1, expr * arg2, expr_ref & result);
|
||||
void mk_mod(expr * arg1, expr * arg2, expr_ref & result);
|
||||
void mk_rem(expr * arg1, expr * arg2, expr_ref & result);
|
||||
void mk_to_real(expr * arg, expr_ref & result);
|
||||
void mk_to_int(expr * arg, expr_ref & result);
|
||||
void mk_is_int(expr * arg, expr_ref & result);
|
||||
void mk_power(expr* x, expr* y, expr_ref& result);
|
||||
void mk_abs(expr * arg, expr_ref & result);
|
||||
|
||||
virtual bool reduce(func_decl * f, unsigned num_args, expr * const * args, expr_ref & result);
|
||||
virtual bool reduce_eq(expr * lhs, expr * rhs, expr_ref & result);
|
||||
|
||||
bool is_arith_term(expr * n) const;
|
||||
|
||||
void gcd_normalize(numeral & coeff, expr_ref& term);
|
||||
|
||||
};
|
||||
|
||||
#endif /* ARITH_SIMPLIFIER_PLUGIN_H_ */
|
|
@ -107,11 +107,10 @@ public:
|
|||
m_init = init;
|
||||
m_delta.push_back(moves());
|
||||
m_delta_inv.push_back(moves());
|
||||
for (unsigned i = 0; i < final.size(); ++i) {
|
||||
add_to_final_states(final[i]);
|
||||
for (unsigned f : final) {
|
||||
add_to_final_states(f);
|
||||
}
|
||||
for (unsigned i = 0; i < mvs.size(); ++i) {
|
||||
move const& mv = mvs[i];
|
||||
for (move const& mv : mvs) {
|
||||
unsigned n = std::max(mv.src(), mv.dst());
|
||||
if (n >= m_delta.size()) {
|
||||
m_delta.resize(n+1, moves());
|
||||
|
@ -280,8 +279,8 @@ public:
|
|||
}
|
||||
else {
|
||||
init = a.num_states();
|
||||
for (unsigned i = 0; i < a.m_final_states.size(); ++i) {
|
||||
mvs.push_back(move(m, init, a.m_final_states[i]));
|
||||
for (unsigned st : a.m_final_states) {
|
||||
mvs.push_back(move(m, init, st));
|
||||
}
|
||||
}
|
||||
return alloc(automaton, m, init, final, mvs);
|
||||
|
@ -471,18 +470,17 @@ public:
|
|||
moves const& get_moves_to(unsigned state) const { return m_delta_inv[state]; }
|
||||
bool initial_state_is_source() const { return m_delta_inv[m_init].empty(); }
|
||||
bool is_final_state(unsigned s) const { return m_final_set.contains(s); }
|
||||
bool is_final_configuration(uint_set s) const {
|
||||
for (uint_set::iterator it = s.begin(), end = s.end(); it != end; ++it) {
|
||||
if (is_final_state(*it))
|
||||
return true;
|
||||
}
|
||||
return false;
|
||||
}
|
||||
bool is_final_configuration(uint_set s) const {
|
||||
for (unsigned i : s) {
|
||||
if (is_final_state(i))
|
||||
return true;
|
||||
}
|
||||
return false;
|
||||
}
|
||||
bool is_epsilon_free() const {
|
||||
for (unsigned i = 0; i < m_delta.size(); ++i) {
|
||||
moves const& mvs = m_delta[i];
|
||||
for (unsigned j = 0; j < mvs.size(); ++j) {
|
||||
if (!mvs[j].t()) return false;
|
||||
for (moves const& mvs : m_delta) {
|
||||
for (move const & m : mvs) {
|
||||
if (!m.t()) return false;
|
||||
}
|
||||
}
|
||||
return true;
|
||||
|
@ -490,8 +488,8 @@ public:
|
|||
|
||||
bool all_epsilon_in(unsigned s) {
|
||||
moves const& mvs = m_delta_inv[s];
|
||||
for (unsigned j = 0; j < mvs.size(); ++j) {
|
||||
if (mvs[j].t()) return false;
|
||||
for (move const& m : mvs) {
|
||||
if (m.t()) return false;
|
||||
}
|
||||
return true;
|
||||
}
|
||||
|
@ -504,15 +502,15 @@ public:
|
|||
bool is_loop_state(unsigned s) const {
|
||||
moves mvs;
|
||||
get_moves_from(s, mvs);
|
||||
for (unsigned i = 0; i < mvs.size(); ++i) {
|
||||
if (s == mvs[i].dst()) return true;
|
||||
for (move const& m : mvs) {
|
||||
if (s == m.dst()) return true;
|
||||
}
|
||||
return false;
|
||||
}
|
||||
|
||||
unsigned move_count() const {
|
||||
unsigned result = 0;
|
||||
for (unsigned i = 0; i < m_delta.size(); result += m_delta[i].size(), ++i) {}
|
||||
for (moves const& mvs : m_delta) result += mvs.size();
|
||||
return result;
|
||||
}
|
||||
void get_epsilon_closure(unsigned state, unsigned_vector& states) {
|
||||
|
@ -524,13 +522,13 @@ public:
|
|||
void get_moves_from(unsigned state, moves& mvs, bool epsilon_closure = true) const {
|
||||
get_moves(state, m_delta, mvs, epsilon_closure);
|
||||
}
|
||||
void get_moves_from_states(uint_set states, moves& mvs, bool epsilon_closure = true) const {
|
||||
for (uint_set::iterator it = states.begin(), end = states.end(); it != end; ++it) {
|
||||
moves curr;
|
||||
get_moves(*it, m_delta, curr, epsilon_closure);
|
||||
mvs.append(curr);
|
||||
}
|
||||
}
|
||||
void get_moves_from_states(uint_set states, moves& mvs, bool epsilon_closure = true) const {
|
||||
for (unsigned i : states) {
|
||||
moves curr;
|
||||
get_moves(i, m_delta, curr, epsilon_closure);
|
||||
mvs.append(curr);
|
||||
}
|
||||
}
|
||||
void get_moves_to(unsigned state, moves& mvs, bool epsilon_closure = true) {
|
||||
get_moves(state, m_delta_inv, mvs, epsilon_closure);
|
||||
}
|
||||
|
@ -543,8 +541,7 @@ public:
|
|||
out << "\n";
|
||||
for (unsigned i = 0; i < m_delta.size(); ++i) {
|
||||
moves const& mvs = m_delta[i];
|
||||
for (unsigned j = 0; j < mvs.size(); ++j) {
|
||||
move const& mv = mvs[j];
|
||||
for (move const& mv : mvs) {
|
||||
out << i << " -> " << mv.dst() << " ";
|
||||
if (mv.t()) {
|
||||
out << "if ";
|
||||
|
|
|
@ -130,13 +130,14 @@ private:
|
|||
else {
|
||||
//true case
|
||||
curr_bv.push_back(true);
|
||||
ref_t new_pred_pos(m_ba.mk_and(curr_pred, constraints[i]), m);
|
||||
ref_t new_pred_pos(m_ba.mk_and(curr_pred, constraints[i]), m);
|
||||
generate_min_terms_rec(constraints, min_terms, i + 1, curr_bv, new_pred_pos);
|
||||
curr_bv.pop_back();
|
||||
|
||||
//false case
|
||||
curr_bv.push_back(false);
|
||||
ref_t new_pred_neg(m_ba.mk_and(curr_pred, m_ba.mk_not(constraints[i])), m);
|
||||
ref_t neg(m_ba.mk_not(constraints[i]), m);
|
||||
ref_t new_pred_neg(m_ba.mk_and(curr_pred, neg), m);
|
||||
generate_min_terms_rec(constraints, min_terms, i + 1, curr_bv, new_pred_neg);
|
||||
curr_bv.pop_back();
|
||||
}
|
||||
|
|
|
@ -288,7 +288,7 @@ typename symbolic_automata<T, M>::automaton_t*
|
|||
symbolic_automata<T, M>::mk_determinstic_param(automaton_t& a, bool flip_acceptance) {
|
||||
vector<std::pair<vector<bool>, ref_t> > min_terms;
|
||||
vector<ref_t> predicates;
|
||||
|
||||
|
||||
map<uint_set, unsigned, uint_set::hash, uint_set::eq> s2id; // set of states to unique id
|
||||
vector<uint_set> id2s; // unique id to set of b-states
|
||||
uint_set set;
|
||||
|
@ -296,13 +296,18 @@ symbolic_automata<T, M>::mk_determinstic_param(automaton_t& a, bool flip_accepta
|
|||
moves_t new_mvs; // moves in the resulting automaton
|
||||
unsigned_vector new_final_states; // new final states
|
||||
unsigned p_state_id = 0; // next state identifier
|
||||
|
||||
// adds non-final states of a to final if flipping and and final otherwise
|
||||
|
||||
TRACE("seq", tout << "mk-deterministic " << flip_acceptance << " " << set << " " << a.is_final_configuration(set) << "\n";);
|
||||
// adds non-final states of a to final if flipping and final otherwise
|
||||
unsigned_vector init_states;
|
||||
a.get_epsilon_closure(a.init(), init_states);
|
||||
for (unsigned s : init_states) {
|
||||
set.insert(s);
|
||||
}
|
||||
if (a.is_final_configuration(set) != flip_acceptance) {
|
||||
new_final_states.push_back(p_state_id);
|
||||
}
|
||||
|
||||
set.insert(a.init()); // Initial state as aset
|
||||
s2id.insert(set, p_state_id++); // the index to the initial state is 0
|
||||
id2s.push_back(set);
|
||||
|
||||
|
@ -342,6 +347,7 @@ symbolic_automata<T, M>::mk_determinstic_param(automaton_t& a, bool flip_accepta
|
|||
|
||||
bool is_new = !s2id.contains(set);
|
||||
if (is_new) {
|
||||
TRACE("seq", tout << "mk-deterministic " << flip_acceptance << " " << set << " " << a.is_final_configuration(set) << "\n";);
|
||||
if (a.is_final_configuration(set) != flip_acceptance) {
|
||||
new_final_states.push_back(p_state_id);
|
||||
}
|
||||
|
|
|
@ -388,6 +388,9 @@ private:
|
|||
m_subgoals.reset();
|
||||
init_preprocess();
|
||||
SASSERT(g->models_enabled());
|
||||
if (g->proofs_enabled()) {
|
||||
throw default_exception("generation of proof objects is not supported in this mode");
|
||||
}
|
||||
SASSERT(!g->proofs_enabled());
|
||||
TRACE("sat", g->display(tout););
|
||||
try {
|
||||
|
|
|
@ -3392,15 +3392,22 @@ void theory_seq::propagate_in_re(expr* n, bool is_true) {
|
|||
return;
|
||||
}
|
||||
|
||||
eautomaton* a = get_automaton(e2);
|
||||
expr_ref e3(e2, m);
|
||||
context& ctx = get_context();
|
||||
literal lit = ctx.get_literal(n);
|
||||
if (!is_true) {
|
||||
e3 = m_util.re.mk_complement(e2);
|
||||
is_true = true;
|
||||
lit.neg();
|
||||
}
|
||||
eautomaton* a = get_automaton(e3);
|
||||
if (!a) return;
|
||||
|
||||
context& ctx = get_context();
|
||||
|
||||
expr_ref len(m_util.str.mk_length(e1), m);
|
||||
for (unsigned i = 0; i < a->num_states(); ++i) {
|
||||
literal acc = mk_accept(e1, len, e2, i);
|
||||
literal rej = mk_reject(e1, len, e2, i);
|
||||
literal acc = mk_accept(e1, len, e3, i);
|
||||
literal rej = mk_reject(e1, len, e3, i);
|
||||
add_axiom(a->is_final_state(i)?acc:~acc);
|
||||
add_axiom(a->is_final_state(i)?~rej:rej);
|
||||
}
|
||||
|
@ -3409,17 +3416,16 @@ void theory_seq::propagate_in_re(expr* n, bool is_true) {
|
|||
unsigned_vector states;
|
||||
a->get_epsilon_closure(a->init(), states);
|
||||
literal_vector lits;
|
||||
literal lit = ctx.get_literal(n);
|
||||
if (is_true) {
|
||||
lits.push_back(~lit);
|
||||
}
|
||||
for (unsigned i = 0; i < states.size(); ++i) {
|
||||
if (is_true) {
|
||||
lits.push_back(mk_accept(e1, zero, e2, states[i]));
|
||||
lits.push_back(mk_accept(e1, zero, e3, states[i]));
|
||||
}
|
||||
else {
|
||||
literal nlit = ~lit;
|
||||
propagate_lit(0, 1, &nlit, mk_reject(e1, zero, e2, states[i]));
|
||||
propagate_lit(0, 1, &nlit, mk_reject(e1, zero, e3, states[i]));
|
||||
}
|
||||
}
|
||||
if (is_true) {
|
||||
|
|
|
@ -93,7 +93,7 @@ tactic * mk_tactic_for_logic(ast_manager & m, params_ref const & p, symbol const
|
|||
return mk_qffpbv_tactic(m, p);
|
||||
else if (logic=="HORN")
|
||||
return mk_horn_tactic(m, p);
|
||||
else if (logic == "QF_FD" || logic == "SAT")
|
||||
else if ((logic == "QF_FD" || logic == "SAT") && !m.proofs_enabled())
|
||||
return mk_solver2tactic(mk_fd_solver(m, p));
|
||||
//else if (logic=="QF_UFNRA")
|
||||
// return mk_qfufnra_tactic(m, p);
|
||||
|
@ -102,7 +102,7 @@ tactic * mk_tactic_for_logic(ast_manager & m, params_ref const & p, symbol const
|
|||
}
|
||||
|
||||
static solver* mk_special_solver_for_logic(ast_manager & m, params_ref const & p, symbol const& logic) {
|
||||
if (logic == "QF_FD" || logic == "SAT")
|
||||
if ((logic == "QF_FD" || logic == "SAT") && !m.proofs_enabled())
|
||||
return mk_fd_solver(m, p);
|
||||
return 0;
|
||||
}
|
||||
|
|
Loading…
Reference in a new issue