mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-10 19:27:06 +00:00
Code Activity

remove simplifier files

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2017-08-29 09:22:27 -07:00
parent 8d8e4cbc51
commit cf87b6d622
44 changed files with 17 additions and 7695 deletions

2
src/ast/macros/macro_util.cpp
View file

@ -20,8 +20,6 @@ Revision History:
#include "ast/macros/macro_util.h"
#include "ast/occurs.h"
#include "ast/ast_util.h"
#include "ast/simplifier/arith_simplifier_plugin.h"
#include "ast/simplifier/bv_simplifier_plugin.h"
#include "ast/rewriter/var_subst.h"
#include "ast/ast_pp.h"
#include "ast/ast_ll_pp.h"

22
src/ast/simplifier/CMakeLists.txt
View file

@ -1,22 +0,0 @@
z3_add_component(simplifier
SOURCES
arith_simplifier_params.cpp
# arith_simplifier_plugin.cpp
# array_simplifier_params.cpp
# array_simplifier_plugin.cpp
# basic_simplifier_plugin.cpp
# bv_elim.cpp
# bv_simplifier_params.cpp
# bv_simplifier_plugin.cpp
# datatype_simplifier_plugin.cpp
# elim_bounds.cpp
# fpa_simplifier_plugin.cpp
# maximise_ac_sharing.cpp
# poly_simplifier_plugin.cpp
# seq_simplifier_plugin.cpp
# simplifier.cpp
# simplifier_plugin.cpp
COMPONENT_DEPENDENCIES
rewriter
)

2
src/ast/simplifier/README
View file

@ -1,2 +0,0 @@
Simplifier module is now obsolete.
It is still being used in many places, but we will eventually replace all occurrences with the new rewriter module.

33
src/ast/simplifier/arith_simplifier_params.cpp
View file

@ -1,33 +0,0 @@
/*++
Copyright (c) 2006 Microsoft Corporation
Module Name:
arith_simplifier_params.cpp
Abstract:
<abstract>
Author:
Leonardo de Moura (leonardo) 2012-12-02.
Revision History:
--*/
#include "ast/simplifier/arith_simplifier_params.h"
#include "ast/simplifier/arith_simplifier_params_helper.hpp"
void arith_simplifier_params::updt_params(params_ref const & _p) {
arith_simplifier_params_helper p(_p);
m_arith_expand_eqs = p.arith_expand_eqs();
m_arith_process_all_eqs = p.arith_process_all_eqs();
}
#define DISPLAY_PARAM(X) out << #X"=" << X << std::endl;
void arith_simplifier_params::display(std::ostream & out) const {
DISPLAY_PARAM(m_arith_expand_eqs);
DISPLAY_PARAM(m_arith_process_all_eqs);
}

38
src/ast/simplifier/arith_simplifier_params.h
View file

@ -1,38 +0,0 @@
/*++
Copyright (c) 2006 Microsoft Corporation
Module Name:
arith_simplifier_params.h
Abstract:
<abstract>
Author:
Leonardo de Moura (leonardo) 2008-05-09.
Revision History:
--*/
#ifndef ARITH_SIMPLIFIER_PARAMS_H_
#define ARITH_SIMPLIFIER_PARAMS_H_
#include "util/params.h"
struct arith_simplifier_params {
bool m_arith_expand_eqs;
bool m_arith_process_all_eqs;
arith_simplifier_params(params_ref const & p = params_ref()) {
updt_params(p);
}
void updt_params(params_ref const & _p);
void display(std::ostream & out) const;
};
#endif /* ARITH_SIMPLIFIER_PARAMS_H_ */

7
src/ast/simplifier/arith_simplifier_params_helper.pyg
View file

@ -1,7 +0,0 @@
def_module_params(class_name='arith_simplifier_params_helper',
module_name="old_simplify", # Parameters will be in the old_simplify module
description="old simplification (stack) still used in the smt module",
export=True,
params=(
('arith.expand_eqs', BOOL, False, 'expand equalities into two inequalities'),
('arith.process_all_eqs', BOOL, False, 'put all equations in the form (= t c), where c is a numeral')))

449
src/ast/simplifier/arith_simplifier_plugin.cpp
View file

@ -1,449 +0,0 @@
/*++
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: return false;
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_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;
}

96
src/ast/simplifier/arith_simplifier_plugin.h
View file

@ -1,96 +0,0 @@
/*++
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_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_ */

26
src/ast/simplifier/array_simplifier_params.cpp
View file

@ -1,26 +0,0 @@
/*++
Copyright (c) 2012 Microsoft Corporation
Module Name:
array_simplifier_params.cpp
Abstract:
This file was created during code reorg.
Author:
Leonardo de Moura (leonardo) 2012-12-02.
Revision History:
--*/
#include "ast/simplifier/array_simplifier_params.h"
#include "ast/simplifier/array_simplifier_params_helper.hpp"
void array_simplifier_params::updt_params(params_ref const & _p) {
array_simplifier_params_helper p(_p);
m_array_canonize_simplify = p.array_canonize();
m_array_simplify = p.array_simplify();
}

34
src/ast/simplifier/array_simplifier_params.h
View file

@ -1,34 +0,0 @@
/*++
Copyright (c) 2012 Microsoft Corporation
Module Name:
array_simplifier_params.h
Abstract:
This file was created during code reorg.
Author:
Leonardo de Moura (leonardo) 2012-12-02.
Revision History:
--*/
#ifndef ARRAY_SIMPLIFIER_PARAMS_H_
#define ARRAY_SIMPLIFIER_PARAMS_H_
#include "util/params.h"
struct array_simplifier_params1 {
array_simplifier_params1(params_ref const & p = params_ref()) {
updt_params(p);
}
void updt_params(params_ref const & _p);
};
#endif /* ARITH_SIMPLIFIER_PARAMS_H_ */

6
src/ast/simplifier/array_simplifier_params_helper.pyg
View file

@ -1,6 +0,0 @@
def_module_params(class_name='array_simplifier_params_helper',
module_name="old_simplify", # Parameters will be in the old_simplify module
export=True,
params=(
('array.canonize', BOOL, False, 'normalize array terms into normal form during simplification'),
('array.simplify', BOOL, True, 'enable/disable array simplifications')))

877
src/ast/simplifier/array_simplifier_plugin.cpp
View file

@ -1,877 +0,0 @@
/*++
Copyright (c) 2008 Microsoft Corporation
Module Name:
array_simplifier_plugin.cpp
Abstract:
<abstract>
Author:
Nikolaj Bjorner (nbjorner) 2008-05-05
Revision History:
Notes TODO:
Examine quadratic cost of simplification vs. model-based procedure.
Parameterize cache replacement strategy.
Some parameters are hard-wired.
--*/
#include "ast/simplifier/array_simplifier_plugin.h"
#include "ast/ast_ll_pp.h"
#include "ast/ast_pp.h"
array_simplifier_plugin::array_simplifier_plugin(
ast_manager & m,
basic_simplifier_plugin& s,
simplifier& simp,
array_simplifier_params const& p) :
simplifier_plugin(symbol("array"),m),
m_util(m),
m_simp(s),
m_simplifier(simp),
m_params(p),
m_store_cache_size(0)
{}
array_simplifier_plugin::~array_simplifier_plugin() {
select_cache::iterator it = m_select_cache.begin();
select_cache::iterator end = m_select_cache.end();
for ( ; it != end; ++it) {
m_manager.dec_array_ref(it->m_key->size(), it->m_key->c_ptr());
m_manager.dec_ref(it->m_value);
dealloc(it->m_key);
}
store_cache::iterator it2 = m_store_cache.begin();
store_cache::iterator end2 = m_store_cache.end();
for (; it2 != end2; ++it2) {
m_manager.dec_ref(it->m_value);
dealloc(it->m_key);
}
}
bool array_simplifier_plugin::reduce(func_decl * f, unsigned num_args, expr * const * args, expr_ref & result) {
if (!m_params.m_array_simplify)
return false;
set_reduce_invoked();
if (m_presimp)
return false;
#if Z3DEBUG
for (unsigned i = 0; i < num_args && i < f->get_arity(); ++i) {
SASSERT(m_manager.get_sort(args[i]) == f->get_domain(i));
}
#endif
TRACE("array_simplifier", {
tout << mk_pp(f, m_manager) << " ";
for (unsigned i = 0; i < num_args; ++i) {
tout << mk_pp(args[i], m_manager) << " ";
}
tout << "\n";
}
);
SASSERT(f->get_family_id() == m_fid);
switch(f->get_decl_kind()) {
case OP_SELECT:
mk_select(num_args, args, result);
break;
case OP_STORE:
mk_store(f, num_args, args, result);
break;
case OP_SET_UNION: {
sort* s = f->get_range();
expr_ref empty(m_manager);
mk_empty_set(s, empty);
switch(num_args) {
case 0:
result = empty;
break;
case 1:
result = args[0];
break;
default: {
result = args[0];
func_decl* f_or = m_manager.mk_or_decl();
for (unsigned i = 1; i < num_args; ++i) {
mk_map(f_or, result, args[i], result);
}
break;
}
}
break;
}
case OP_SET_INTERSECT: {
expr_ref full(m_manager);
mk_full_set(f->get_range(), full);
switch(num_args) {
case 0:
result = full;
break;
case 1:
result = args[0];
break;
default: {
result = args[0];
func_decl* f_and = m_manager.mk_and_decl();
for (unsigned i = 1; i < num_args; ++i) {
mk_map(f_and, result, args[i], result);
}
break;
}
}
TRACE("array_simplifier", tout << "sort " << mk_pp(result.get(), m_manager) << "\n";);
break;
}
case OP_SET_SUBSET: {
SASSERT(num_args == 2);
expr_ref diff(m_manager), emp(m_manager);
mk_set_difference(num_args, args, diff);
mk_empty_set(m_manager.get_sort(args[0]), emp);
m_simp.mk_eq(diff.get(), emp.get(), result);
break;
}
case OP_SET_COMPLEMENT: {
SASSERT(num_args == 1);
func_decl* f_not = m_manager.mk_not_decl();
mk_map(f_not, args[0], result);
break;
}
case OP_SET_DIFFERENCE: {
SASSERT(num_args == 2);
expr_ref r1(m_manager);
mk_map(m_manager.mk_not_decl(), args[1], r1);
mk_map(m_manager.mk_and_decl(), args[0], r1, result);
break;
}
case OP_ARRAY_MAP: {
SASSERT(f->get_num_parameters() == 1);
SASSERT(f->get_parameter(0).is_ast());
SASSERT(is_func_decl(f->get_parameter(0).get_ast()));
//
// map_d (store a j v) = (store (map_f a) v (d v))
//
if (num_args == 1 && is_store(args[0])) {
app* store_expr = to_app(args[0]);
unsigned num_args = store_expr->get_num_args();
SASSERT(num_args >= 3);
parameter p = f->get_parameter(0);
func_decl* d = to_func_decl(p.get_ast());
expr* a = store_expr->get_arg(0);
expr* v = store_expr->get_arg(num_args-1);
// expr*const* args = store_expr->get_args()+1;
expr_ref r1(m_manager), r2(m_manager);
ptr_vector<expr> new_args;
reduce(f, 1, &a, r1);
m_simplifier.mk_app(d, 1, &v, r2);
new_args.push_back(r1);
for (unsigned i = 1; i + 1 < num_args; ++i) {
new_args.push_back(store_expr->get_arg(i));
}
new_args.push_back(r2);
mk_store(store_expr->get_decl(), num_args, new_args.c_ptr(), result);
break;
}
//
// map_d (store a j v) (store b j w) = (store (map_f a b) j (d v w))
//
if (num_args > 1 && same_store(num_args, args)) {
app* store_expr1 = to_app(args[0]);
unsigned num_indices = store_expr1->get_num_args();
SASSERT(num_indices >= 3);
parameter p = f->get_parameter(0);
func_decl* d = to_func_decl(p.get_ast());
ptr_vector<expr> arrays;
ptr_vector<expr> values;
for (unsigned i = 0; i < num_args; ++i) {
arrays.push_back(to_app(args[i])->get_arg(0));
values.push_back(to_app(args[i])->get_arg(num_indices-1));
}
expr_ref r1(m_manager), r2(m_manager);
reduce(f, arrays.size(), arrays.c_ptr(), r1);
m_simplifier.mk_app(d, values.size(), values.c_ptr(), r2);
ptr_vector<expr> new_args;
new_args.push_back(r1);
for (unsigned i = 1; i + 1 < num_indices; ++i) {
new_args.push_back(store_expr1->get_arg(i));
}
new_args.push_back(r2);
mk_store(store_expr1->get_decl(), new_args.size(), new_args.c_ptr(), result);
break;
}
//
// map_d (const v) = (const (d v))
//
if (num_args == 1 && is_const_array(args[0])) {
app* const_expr = to_app(args[0]);
SASSERT(const_expr->get_num_args() == 1);
parameter p = f->get_parameter(0);
func_decl* d = to_func_decl(p.get_ast());
expr* v = const_expr->get_arg(0);
expr_ref r1(m_manager);
m_simplifier.mk_app(d, 1, &v, r1);
expr* arg = r1.get();
parameter param(f->get_range());
result = m_manager.mk_app(m_fid, OP_CONST_ARRAY, 1, &param, 1, &arg);
break;
}
//
// map_d (const v) (const w) = (const (d v w))
//
if (num_args > 1 && all_const_array(num_args, args)) {
parameter p = f->get_parameter(0);
func_decl* d = to_func_decl(p.get_ast());
ptr_vector<expr> values;
for (unsigned i = 0; i < num_args; ++i) {
values.push_back(to_app(args[i])->get_arg(0));
}
expr_ref r1(m_manager);
m_simplifier.mk_app(d, values.size(), values.c_ptr(), r1);
expr* arg = r1.get();
parameter param(f->get_range());
result = m_manager.mk_app(m_fid, OP_CONST_ARRAY, 1, &param, 1, &arg);
break;
}
result = m_manager.mk_app(f, num_args, args);
break;
}
default:
result = m_manager.mk_app(f, num_args, args);
break;
}
TRACE("array_simplifier",
tout << mk_pp(result.get(), m_manager) << "\n";);
return true;
}
bool array_simplifier_plugin::same_store(unsigned num_args, expr* const* args) const {
if (num_args == 0) {
return true;
}
if (!is_store(args[0])) {
return false;
}
SASSERT(to_app(args[0])->get_num_args() >= 3);
unsigned num_indices = to_app(args[0])->get_num_args() - 2;
for (unsigned i = 1; i < num_args; ++i) {
if (!is_store(args[i])) {
return false;
}
for (unsigned j = 1; j < num_indices + 1; ++j) {
if (to_app(args[0])->get_arg(j) != to_app(args[i])->get_arg(j)) {
return false;
}
}
}
return true;
}
bool array_simplifier_plugin::all_const_array(unsigned num_args, expr* const* args) const {
bool is_const = true;
for (unsigned i = 0; is_const && i < num_args; ++i) {
is_const = is_const_array(args[i]);
}
return is_const;
}
bool array_simplifier_plugin::all_values(unsigned num_args, expr* const* args) const {
for (unsigned i = 0; i < num_args; ++i) {
if (!m_manager.is_unique_value(args[i])) {
return false;
}
}
return true;
}
bool array_simplifier_plugin::lex_lt(unsigned num_args, expr* const* args1, expr* const* args2) {
for (unsigned i = 0; i < num_args; ++i) {
TRACE("array_simplifier",
tout << mk_pp(args1[i], m_manager) << "\n";
tout << mk_pp(args2[i], m_manager) << "\n";
tout << args1[i]->get_id() << " " << args2[i]->get_id() << "\n";
);
if (args1[i]->get_id() < args2[i]->get_id()) return true;
if (args1[i]->get_id() > args2[i]->get_id()) return false;
}
return false;
}
void array_simplifier_plugin::get_stores(expr* n, unsigned& arity, expr*& m, ptr_vector<expr*const>& stores) {
while (is_store(n)) {
app* a = to_app(n);
SASSERT(a->get_num_args() > 2);
arity = a->get_num_args()-2;
n = a->get_arg(0);
stores.push_back(a->get_args()+1);
}
m = n;
}
lbool array_simplifier_plugin::eq_default(expr* def, unsigned arity, unsigned num_st, expr*const* const* st) {
bool all_diseq = m_manager.is_unique_value(def) && num_st > 0;
bool all_eq = true;
for (unsigned i = 0; i < num_st; ++i) {
all_eq &= (st[i][arity] == def);
all_diseq &= m_manager.is_unique_value(st[i][arity]) && (st[i][arity] != def);
TRACE("array_simplifier", tout << m_manager.is_unique_value(st[i][arity]) << " " << mk_pp(st[i][arity], m_manager) << "\n";);
}
if (all_eq) {
return l_true;
}
if (all_diseq) {
return l_false;
}
return l_undef;
}
bool array_simplifier_plugin::insert_table(expr* def, unsigned arity, unsigned num_st, expr*const* const* st, arg_table& table) {
for (unsigned i = 0; i < num_st; ++i ) {
for (unsigned j = 0; j < arity; ++j) {
if (!m_manager.is_unique_value(st[i][j])) {
return false;
}
}
TRACE("array_simplifier", tout << "inserting: ";
for (unsigned j = 0; j < arity; ++j) {
tout << mk_pp(st[i][j], m_manager) << " ";
}
tout << " |-> " << mk_pp(def, m_manager) << "\n";
);
args_entry e(arity, st[i]);
table.insert_if_not_there(e);
}
return true;
}
lbool array_simplifier_plugin::eq_stores(expr* def, unsigned arity, unsigned num_st1, expr*const* const* st1, unsigned num_st2, expr*const* const* st2) {
if (num_st1 == 0) {
return eq_default(def, arity, num_st2, st2);
}
if (num_st2 == 0) {
return eq_default(def, arity, num_st1, st1);
}
arg_table table1, table2;
if (!insert_table(def, arity, num_st1, st1, table1)) {
return l_undef;
}
if (!insert_table(def, arity, num_st2, st2, table2)) {
return l_undef;
}
arg_table::iterator it = table1.begin();
arg_table::iterator end = table1.end();
for (; it != end; ++it) {
args_entry const & e1 = *it;
args_entry e2;
expr* v1 = e1.m_args[arity];
if (table2.find(e1, e2)) {
expr* v2 = e2.m_args[arity];
if (v1 == v2) {
table2.erase(e1);
continue;
}
if (m_manager.is_unique_value(v1) && m_manager.is_unique_value(v2)) {
return l_false;
}
return l_undef;
}
else if (m_manager.is_unique_value(v1) && m_manager.is_unique_value(def) && v1 != def) {
return l_false;
}
}
it = table2.begin();
end = table2.end();
for (; it != end; ++it) {
args_entry const & e = *it;
expr* v = e.m_args[arity];
if (m_manager.is_unique_value(v) && m_manager.is_unique_value(def) && v != def) {
return l_false;
}
}
if (!table2.empty() || !table1.empty()) {
return l_undef;
}
return l_true;
}
bool array_simplifier_plugin::reduce_eq(expr * lhs, expr * rhs, expr_ref & result) {
set_reduce_invoked();
expr* c1, *c2;
ptr_vector<expr*const> st1, st2;
unsigned arity1 = 0;
unsigned arity2 = 0;
get_stores(lhs, arity1, c1, st1);
get_stores(rhs, arity2, c2, st2);
if (arity1 == arity2 && is_const_array(c1) && is_const_array(c2)) {
c1 = to_app(c1)->get_arg(0);
c2 = to_app(c2)->get_arg(0);
if (c1 == c2) {
lbool eq = eq_stores(c1, arity2, st1.size(), st1.c_ptr(), st2.size(), st2.c_ptr());
TRACE("array_simplifier",
tout << mk_pp(lhs, m_manager) << " = "
<< mk_pp(rhs, m_manager) << " := " << eq << "\n";
tout << "arity: " << arity1 << "\n";);
switch(eq) {
case l_false:
result = m_manager.mk_false();
return true;
case l_true:
result = m_manager.mk_true();
return true;
default:
return false;
}
}
else if (m_manager.is_unique_value(c1) && m_manager.is_unique_value(c2)) {
result = m_manager.mk_false();
return true;
}
}
return false;
}
bool array_simplifier_plugin::reduce_distinct(unsigned num_args, expr * const * args, expr_ref & result) {
set_reduce_invoked();
return false;
}
array_simplifier_plugin::const_select_result
array_simplifier_plugin::mk_select_const(expr* m, app* index, expr_ref& result) {
store_info* info = 0;
expr* r = 0, *a = 0;
if (!is_store(m)) {
return NOT_CACHED;
}
if (!m_store_cache.find(m, info)) {
return NOT_CACHED;
}
if (info->m_map.find(index, r)) {
result = r;
return FOUND_VALUE;
}
a = info->m_default.get();
//
// Unfold and cache the store while searching for value of index.
//
while (is_store(a) && m_manager.is_unique_value(to_app(a)->get_arg(1))) {
app* b = to_app(a);
app* c = to_app(b->get_arg(1));
if (!info->m_map.contains(c)) {
info->m_map.insert(c, b->get_arg(2));
m_manager.inc_ref(b->get_arg(2));
++m_store_cache_size;
}
a = b->get_arg(0);
info->m_default = a;
if (c == index) {
result = b->get_arg(2);
return FOUND_VALUE;
}
}
result = info->m_default.get();
return FOUND_DEFAULT;
}
void array_simplifier_plugin::cache_store(unsigned num_stores, expr* store_term)
{
if (num_stores <= m_const_store_threshold) {
return;
}
prune_store_cache();
if (!m_store_cache.contains(store_term)) {
store_info * info = alloc(store_info, m_manager, store_term);
m_manager.inc_ref(store_term);
m_store_cache.insert(store_term, info);
TRACE("cache_store", tout << m_store_cache.size() << "\n";);
++m_store_cache_size;
}
}
void array_simplifier_plugin::cache_select(unsigned num_args, expr * const * args, expr * result) {
ptr_vector<expr> * entry = alloc(ptr_vector<expr>);
entry->append(num_args, const_cast<expr**>(args));
const select_cache::key_data & kd = m_select_cache.insert_if_not_there(entry, result);
if (kd.m_key != entry) {
dealloc(entry);
return;
}
m_manager.inc_array_ref(num_args, args);
m_manager.inc_ref(result);
TRACE("cache_select", tout << m_select_cache.size() << "\n";);
}
void array_simplifier_plugin::prune_select_cache() {
if (m_select_cache.size() > m_select_cache_max_size) {
flush_select_cache();
}
}
void array_simplifier_plugin::prune_store_cache() {
if (m_store_cache_size > m_store_cache_max_size) {
flush_store_cache();
}
}
void array_simplifier_plugin::flush_select_cache() {
select_cache::iterator it = m_select_cache.begin();
select_cache::iterator end = m_select_cache.end();
for (; it != end; ++it) {
ptr_vector<expr> * e = (*it).m_key;
m_manager.dec_array_ref(e->size(), e->begin());
m_manager.dec_ref((*it).m_value);
dealloc(e);
}
m_select_cache.reset();
}
void array_simplifier_plugin::flush_store_cache() {
store_cache::iterator it = m_store_cache.begin();
store_cache::iterator end = m_store_cache.end();
for (; it != end; ++it) {
m_manager.dec_ref((*it).m_key);
const_map::iterator mit = (*it).m_value->m_map.begin();
const_map::iterator mend = (*it).m_value->m_map.end();
for (; mit != mend; ++mit) {
m_manager.dec_ref((*mit).m_value);
}
dealloc((*it).m_value);
}
m_store_cache.reset();
m_store_cache_size = 0;
}
void array_simplifier_plugin::flush_caches() {
flush_select_cache();
flush_store_cache();
}
void array_simplifier_plugin::mk_set_difference(unsigned num_args, expr * const * args, expr_ref & result) {
SASSERT(num_args == 2);
result = m_manager.mk_app(m_fid, OP_SET_DIFFERENCE, 0, 0, num_args, args);
}
void array_simplifier_plugin::mk_empty_set(sort* ty, expr_ref & result) {
parameter param(ty);
expr* args[1] = { m_manager.mk_false() };
result = m_manager.mk_app(m_fid, OP_CONST_ARRAY, 1, &param, 1, args);
}
void array_simplifier_plugin::mk_full_set(sort* ty, expr_ref & result) {
parameter param(ty);
expr* args[1] = { m_manager.mk_true() };
result = m_manager.mk_app(m_fid, OP_CONST_ARRAY, 1, &param, 1, args);
}
bool array_simplifier_plugin::same_args(unsigned num_args, expr * const * args1, expr * const * args2) {
for (unsigned i = 0; i < num_args; ++i) {
if (args1[i] != args2[i]) {
return false;
}
}
return true;
}
void array_simplifier_plugin::mk_store(func_decl* f, unsigned num_args, expr * const * args, expr_ref & result) {
SASSERT(num_args >= 3);
expr* arg0 = args[0];
expr* argn = args[num_args-1];
//
// store(store(a,i,v),i,w) = store(a,i,w)
//
if (is_store(arg0) &&
same_args(num_args-2, args+1, to_app(arg0)->get_args()+1)) {
expr_ref_buffer new_args(m_manager);
new_args.push_back(to_app(arg0)->get_arg(0));
for (unsigned i = 1; i < num_args; ++i) {
new_args.push_back(args[i]);
}
reduce(f, num_args, new_args.c_ptr(), result);
TRACE("array_simplifier", tout << mk_pp(result.get(), m_manager) << "\n";);
return;
}
//
// store(const(v),i,v) = const(v)
//
if (is_const_array(arg0) &&
to_app(arg0)->get_arg(0) == args[num_args-1]) {
result = arg0;
TRACE("array_simplifier", tout << mk_pp(result.get(), m_manager) << "\n";);
return;
}
//
// store(a, i, select(a, i)) = a
//
if (is_select(argn) &&
(to_app(argn)->get_num_args() == num_args - 1) &&
same_args(num_args-1, args, to_app(argn)->get_args())) {
TRACE("dummy_store", tout << "dummy store simplified mk_store(\n";
for (unsigned i = 0; i < num_args; i++) ast_ll_pp(tout, m_manager, args[i]);
tout << ") =====>\n";
ast_ll_pp(tout, m_manager, arg0););
result = arg0;
TRACE("array_simplifier", tout << mk_pp(result.get(), m_manager) << "\n";);
return;
}
//
// store(store(a,i,v),j,w) -> store(store(a,j,w),i,v)
// if i, j are values, i->get_id() < j->get_id()
//
if (m_params.m_array_canonize_simplify &&
is_store(arg0) &&
all_values(num_args-2, args+1) &&
all_values(num_args-2, to_app(arg0)->get_args()+1) &&
lex_lt(num_args-2, args+1, to_app(arg0)->get_args()+1)) {
expr* const* args2 = to_app(arg0)->get_args();
expr_ref_buffer new_args(m_manager);
new_args.push_back(args2[0]);
for (unsigned i = 1; i < num_args; ++i) {
new_args.push_back(args[i]);
}
reduce(f, num_args, new_args.c_ptr(), result);
new_args.reset();
new_args.push_back(result);
for (unsigned i = 1; i < num_args; ++i) {
new_args.push_back(args2[i]);
}
result = m_manager.mk_app(m_fid, OP_STORE, num_args, new_args.c_ptr());
TRACE("array_simplifier", tout << mk_pp(result.get(), m_manager) << "\n";);
return;
}
result = m_manager.mk_app(m_fid, OP_STORE, num_args, args);
TRACE("array_simplifier", tout << "default: " << mk_pp(result.get(), m_manager) << "\n";);
}
void array_simplifier_plugin::mk_select_as_array(unsigned num_args, expr * const * args, expr_ref & result) {
SASSERT(is_as_array(args[0]));
func_decl * f = get_as_array_func_decl(to_app(args[0]));
result = m_manager.mk_app(f, num_args - 1, args+1);
}
void array_simplifier_plugin::mk_select_as_array_tree(unsigned num_args, expr * const * args, expr_ref & result) {
SASSERT(is_as_array_tree(args[0]));
SASSERT(m_manager.is_ite(args[0]));
ptr_buffer<app, 32> todo;
obj_map<app, app *> cache;
app_ref_buffer trail(m_manager);
todo.push_back(to_app(args[0]));
while (!todo.empty()) {
app * curr = todo.back();
SASSERT(m_manager.is_ite(curr));
expr * branches[2] = {0, 0};
bool visited = true;
for (unsigned i = 0; i < 2; i++) {
expr * arg = curr->get_arg(i+1);
if (is_as_array(arg)) {
branches[i] = m_manager.mk_app(get_as_array_func_decl(to_app(arg)), num_args - 1, args+1);
}
else {
SASSERT(m_manager.is_ite(arg));
app * new_arg = 0;
if (!cache.find(to_app(arg), new_arg)) {
todo.push_back(to_app(arg));
visited = false;
}
else {
branches[i] = new_arg;
}
}
}
if (visited) {
todo.pop_back();
app * new_curr = m_manager.mk_ite(curr->get_arg(0), branches[0], branches[1]);
trail.push_back(new_curr);
cache.insert(curr, new_curr);
}
}
SASSERT(cache.contains(to_app(args[0])));
app * r = 0;
cache.find(to_app(args[0]), r);
result = r;
}
void array_simplifier_plugin::mk_select(unsigned num_args, expr * const * args, expr_ref & result) {
expr * r = 0;
if (is_as_array(args[0])) {
mk_select_as_array(num_args, args, result);
return;
}
if (is_as_array_tree(args[0])) {
mk_select_as_array_tree(num_args, args, result);
return;
}
bool is_const_select = num_args == 2 && m_manager.is_unique_value(args[1]);
app* const_index = is_const_select?to_app(args[1]):0;
unsigned num_const_stores = 0;
expr_ref tmp(m_manager);
expr* args2[2];
if (is_const_select) {
switch(mk_select_const(args[0], const_index, tmp)) {
case NOT_CACHED:
break;
case FOUND_VALUE:
TRACE("mk_select", tout << "found value\n"; ast_ll_pp(tout, m_manager, tmp.get()); );
result = tmp.get();
// value of select is stored under result.
return;
case FOUND_DEFAULT:
args2[0] = tmp.get();
args2[1] = args[1];
args = args2;
is_const_select = false;
break;
}
}
SASSERT(num_args > 0);
ptr_vector<expr> & entry = m_tmp2;
entry.reset();
entry.append(num_args, args);
expr * entry0 = entry[0];
SASSERT(m_todo.empty());
m_todo.push_back(entry0);
while (!m_todo.empty()) {
expr * m = m_todo.back();
TRACE("array_simplifier", tout << mk_bounded_pp(m, m_manager) << "\n";);
if (is_store(m)) {
expr * nested_array = to_app(m)->get_arg(0);
expr * else_branch = 0;
entry[0] = nested_array;
if (is_const_select) {
if (m_manager.is_unique_value(to_app(m)->get_arg(1))) {
app* const_index2 = to_app(to_app(m)->get_arg(1));
//
// we found the value, all other stores are different.
// there is no need to recurse.
//
if (const_index == const_index2) {
result = to_app(m)->get_arg(2);
cache_store(num_const_stores, args[0]);
m_todo.reset();
return;
}
++num_const_stores;
}
else {
is_const_select = false;
}
}
if (m_select_cache.find(&entry, else_branch)) {
expr_ref_buffer eqs(m_manager);
for (unsigned i = 1; i < num_args ; ++i) {
expr * a = args[i];
expr * b = to_app(m)->get_arg(i);
expr_ref eq(m_manager);
m_simp.mk_eq(a, b, eq);
eqs.push_back(eq.get());
}
expr_ref cond(m_manager);
m_simp.mk_and(eqs.size(), eqs.c_ptr(), cond);
expr * then_branch = to_app(m)->get_arg(num_args);
if (m_manager.is_true(cond.get())) {
result = then_branch;
}
else if (m_manager.is_false(cond.get())) {
result = else_branch;
}
else {
m_simp.mk_ite(cond.get(), then_branch, else_branch, result);
}
entry[0] = m;
cache_select(entry.size(), entry.c_ptr(), result.get());
m_todo.pop_back();
}
else {
m_todo.push_back(nested_array);
}
}
else if (is_const_array(m)) {
entry[0] = m;
cache_select(entry.size(), entry.c_ptr(), to_app(m)->get_arg(0));
m_todo.pop_back();
}
else {
entry[0] = m;
TRACE("array_simplifier", {
for (unsigned i = 0; i < entry.size(); ++i) {
tout << mk_bounded_pp(entry[i], m_manager) << ": "
<< mk_bounded_pp(m_manager.get_sort(entry[i]), m_manager) << "\n";
}}
);
r = m_manager.mk_app(m_fid, OP_SELECT, 0, 0, entry.size(), entry.c_ptr());
cache_select(entry.size(), entry.c_ptr(), r);
m_todo.pop_back();
}
}
cache_store(num_const_stores, args[0]);
entry[0] = entry0;
#ifdef Z3DEBUG
bool f =
#endif
m_select_cache.find(&entry, r);
SASSERT(f);
result = r;
prune_select_cache();
prune_store_cache();
TRACE("mk_select",
for (unsigned i = 0; i < num_args; i++) {
ast_ll_pp(tout, m_manager, args[i]); tout << "\n";
};
tout << "is_store: " << is_store(args[0]) << "\n";
ast_ll_pp(tout, m_manager, r););
}
void array_simplifier_plugin::mk_map(func_decl* f, expr* a, expr* b, expr_ref& result) {
expr* exprs[2] = { a, b };
parameter param(f);
result = m_manager.mk_app(m_fid, OP_ARRAY_MAP, 1, &param, 2, exprs );
}
void array_simplifier_plugin::mk_map(func_decl* f, expr* a, expr_ref& result) {
parameter param(f);
result = m_manager.mk_app(m_fid, OP_ARRAY_MAP, 1, &param, 1, &a );
}

154
src/ast/simplifier/array_simplifier_plugin.h
View file

@ -1,154 +0,0 @@
/*++
Copyright (c) 2008 Microsoft Corporation
Module Name:
array_simplifier_plugin.h
Abstract:
<abstract>
Author:
Nikolaj Bjorner (nbjorner) 2008-05-05
Revision History:
--*/
#ifndef ARRAY_SIMPLIFIER_PLUGIN_H_
#define ARRAY_SIMPLIFIER_PLUGIN_H_
#include "ast/ast.h"
#include "util/map.h"
#include "ast/array_decl_plugin.h"
#include "ast/simplifier/simplifier_plugin.h"
#include "ast/simplifier/basic_simplifier_plugin.h"
#include "ast/simplifier/array_simplifier_params.h"
#include "ast/simplifier/simplifier.h"
#include "util/obj_hashtable.h"
#include "util/lbool.h"
class array_simplifier_plugin : public simplifier_plugin {
typedef ptr_vector<expr> entry;
struct entry_hash_proc {
unsigned operator()(ptr_vector<expr> * entry) const {
return get_exprs_hash(entry->size(), entry->begin(), 0xbeef1010);
}
};
struct entry_eq_proc {
bool operator()(ptr_vector<expr> * entry1, ptr_vector<expr> * entry2) const {
if (entry1->size() != entry2->size()) return false;
return compare_arrays(entry1->begin(), entry2->begin(), entry1->size());
}
};
typedef map<entry *, expr *, entry_hash_proc, entry_eq_proc> select_cache;
struct args_entry {
unsigned m_arity;
expr* const* m_args;
args_entry(unsigned a, expr* const* args) : m_arity(a), m_args(args) {}
args_entry() : m_arity(0), m_args(0) {}
};
struct args_entry_hash_proc {
unsigned operator()(args_entry const& e) const {
return get_exprs_hash(e.m_arity, e.m_args, 0xbeef1010);
}
};
struct args_entry_eq_proc {
bool operator()(args_entry const& e1, args_entry const& e2) const {
if (e1.m_arity != e2.m_arity) return false;
return compare_arrays(e1.m_args, e2.m_args, e1.m_arity);
}
};
typedef hashtable<args_entry, args_entry_hash_proc, args_entry_eq_proc> arg_table;
array_util m_util;
basic_simplifier_plugin& m_simp;
simplifier& m_simplifier;
array_simplifier_params const& m_params;
select_cache m_select_cache;
ptr_vector<expr> m_tmp;
ptr_vector<expr> m_tmp2;
ptr_vector<expr> m_todo;
static const unsigned m_select_cache_max_size = 100000;
typedef obj_map<expr, expr*> const_map;
class store_info {
store_info();
store_info(store_info const&);
public:
const_map m_map;
expr_ref m_default;
store_info(ast_manager& m, expr* d): m_default(d, m) {}
};
typedef obj_map<expr, store_info*> store_cache;
store_cache m_store_cache;
unsigned m_store_cache_size;
static const unsigned m_store_cache_max_size = 10000;
static const unsigned m_const_store_threshold = 5;
enum const_select_result {
NOT_CACHED,
FOUND_DEFAULT,
FOUND_VALUE
};
public:
array_simplifier_plugin(ast_manager & m, basic_simplifier_plugin& s, simplifier& simp, array_simplifier_params const& p);
virtual ~array_simplifier_plugin();
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);
virtual bool reduce_distinct(unsigned num_args, expr * const * args, expr_ref & result);
virtual void flush_caches();
private:
bool is_select(expr* n) const { return m_util.is_select(n); }
bool is_store(expr * n) const { return m_util.is_store(n); }
bool is_const_array(expr * n) const { return m_util.is_const(n); }
bool is_as_array(expr * n) const { return m_util.is_as_array(n); }
bool is_as_array_tree(expr * n) { return m_util.is_as_array_tree(n); }
func_decl * get_as_array_func_decl(app * n) const { return m_util.get_as_array_func_decl(n); }
void mk_select_as_array(unsigned num_args, expr * const * args, expr_ref & result);
void mk_select_as_array_tree(unsigned num_args, expr * const * args, expr_ref & result);
bool is_enumerated(expr* n, expr_ref& c, ptr_vector<expr>& keys, ptr_vector<expr>& vals);
const_select_result mk_select_const(expr* m, app* index, expr_ref& result);
void cache_store(unsigned num_stores, expr* nested_store);
void cache_select(unsigned num_args, expr * const * args, expr * result);
void prune_select_cache();
void prune_store_cache();
void flush_select_cache();
void flush_store_cache();
void mk_set_difference(unsigned num_args, expr * const * args, expr_ref & result);
void mk_empty_set(sort* ty, expr_ref & result);
void mk_full_set(sort* ty, expr_ref & result);
void mk_select(unsigned num_args, expr * const * args, expr_ref & result);
void mk_store(func_decl* f, unsigned num_args, expr * const * args, expr_ref & result);
void mk_map(func_decl* f, expr* a, expr* b, expr_ref & result);
void mk_map(func_decl* f, expr* a, expr_ref & result);
bool same_args(unsigned num_args, expr * const * args1, expr * const * args2);
void get_stores(expr* n, unsigned& arity, expr*& m, ptr_vector<expr*const>& stores);
lbool eq_default(expr* def, unsigned arity, unsigned num_st, expr*const* const* st);
bool insert_table(expr* def, unsigned arity, unsigned num_st, expr*const* const* st, arg_table& table);
lbool eq_stores(expr* def, unsigned arity, unsigned num_st1, expr*const* const* st1, unsigned num_st2, expr*const* const* st2);
bool same_store(unsigned num_args, expr* const* args) const;
bool all_const_array(unsigned num_args, expr* const* args) const;
bool all_values(unsigned num_args, expr* const* args) const;
bool lex_lt(unsigned num_args, expr* const* args1, expr* const* args2);
};
#endif /* ARRAY_SIMPLIFIER_PLUGIN_H_ */

76
src/ast/simplifier/base_simplifier.h
View file

@ -1,76 +0,0 @@
/*++
Copyright (c) 2007 Microsoft Corporation
Module Name:
base_simplifier.h
Abstract:
Base class for expression simplifier functors.
Author:
Leonardo (leonardo) 2008-01-11
Notes:
--*/
#ifndef BASE_SIMPLIFIER_H_
#define BASE_SIMPLIFIER_H_
#include "ast/expr_map.h"
#include "ast/ast_pp.h"
/**
\brief Implements basic functionality used by expression simplifiers.
*/
class base_simplifier {
protected:
ast_manager & m;
expr_map m_cache;
ptr_vector<expr> m_todo;
void cache_result(expr * n, expr * r, proof * p) {
m_cache.insert(n, r, p);
CTRACE("simplifier", !is_rewrite_proof(n, r, p),
tout << mk_pp(n, m) << "\n";
tout << mk_pp(r, m) << "\n";
tout << mk_pp(p, m) << "\n";);
SASSERT(is_rewrite_proof(n, r, p));
}
void reset_cache() { m_cache.reset(); }
void flush_cache() { m_cache.flush(); }
void get_cached(expr * n, expr * & r, proof * & p) const { m_cache.get(n, r, p); }
void reinitialize() { m_cache.set_store_proofs(m.fine_grain_proofs()); }
void visit(expr * n, bool & visited) {
if (!is_cached(n)) {
m_todo.push_back(n);
visited = false;
}
}
public:
base_simplifier(ast_manager & m):
m(m),
m_cache(m, m.fine_grain_proofs()) {
}
bool is_cached(expr * n) const { return m_cache.contains(n); }
ast_manager & get_manager() { return m; }
bool is_rewrite_proof(expr* n, expr* r, proof* p) {
if (p &&
!m.is_undef_proof(p) &&
!(m.has_fact(p) &&
(m.is_eq(m.get_fact(p)) || m.is_oeq(m.get_fact(p)) || m.is_iff(m.get_fact(p))) &&
to_app(m.get_fact(p))->get_arg(0) == n &&
to_app(m.get_fact(p))->get_arg(1) == r)) return false;
return (!m.fine_grain_proofs() || p || (n == r));
}
};
#endif /* BASE_SIMPLIFIER_H_ */

147
src/ast/simplifier/basic_simplifier_plugin.cpp
View file

@ -1,147 +0,0 @@
/*++
Copyright (c) 2007 Microsoft Corporation
Module Name:
basic_simplifier_plugin.cpp
Abstract:
Simplifier for the basic family.
Author:
Leonardo (leonardo) 2008-01-07
--*/
#include "ast/simplifier/basic_simplifier_plugin.h"
#include "ast/ast_ll_pp.h"
#include "ast/rewriter/bool_rewriter.h"
basic_simplifier_plugin::basic_simplifier_plugin(ast_manager & m):
simplifier_plugin(symbol("basic"), m),
m_rewriter(alloc(bool_rewriter, m)) {
}
basic_simplifier_plugin::~basic_simplifier_plugin() {
dealloc(m_rewriter);
}
bool basic_simplifier_plugin::reduce(func_decl * f, unsigned num_args, expr * const * args, expr_ref & result) {
set_reduce_invoked();
SASSERT(f->get_family_id() == m_manager.get_basic_family_id());
basic_op_kind k = static_cast<basic_op_kind>(f->get_decl_kind());
switch (k) {
case OP_FALSE:
case OP_TRUE:
return false;
case OP_EQ:
SASSERT(num_args == 2);
mk_eq(args[0], args[1], result);
return true;
case OP_DISTINCT:
mk_distinct(num_args, args, result);
return true;
case OP_ITE:
SASSERT(num_args == 3);
mk_ite(args[0], args[1], args[2], result);
return true;
case OP_AND:
mk_and(num_args, args, result);
return true;
case OP_OR:
mk_or(num_args, args, result);
return true;
case OP_IMPLIES:
mk_implies(args[0], args[1], result);
return true;
case OP_IFF:
mk_iff(args[0], args[1], result);
return true;
case OP_XOR:
switch (num_args) {
case 0: result = m_manager.mk_true(); break;
case 1: result = args[0]; break;
case 2: mk_xor(args[0], args[1], result); break;
default: UNREACHABLE(); break;
}
return true;
case OP_NOT:
SASSERT(num_args == 1);
mk_not(args[0], result);
return true;
default:
UNREACHABLE();
return false;
}
}
/**
\brief Return true if \c rhs is of the form (ite c t1 t2) and are_distinct(lhs, t1) and are_distinct(lhs, t2).
*/
static bool is_lhs_diseq_rhs_ite_branches(ast_manager & m, expr * lhs, expr * rhs) {
return m.is_ite(rhs) && m.are_distinct(lhs, to_app(rhs)->get_arg(1)) && m.are_distinct(lhs, to_app(rhs)->get_arg(2));
}
/**
\brief Return true if \c rhs is of the form (ite c t1 t2) and lhs = t1 && are_distinct(lhs, t2)
*/
static bool is_lhs_eq_rhs_ite_then(ast_manager & m, expr * lhs, expr * rhs) {
return m.is_ite(rhs) && lhs == to_app(rhs)->get_arg(1) && m.are_distinct(lhs, to_app(rhs)->get_arg(2));
}
/**
\brief Return true if \c rhs is of the form (ite c t1 t2) and are_distinct(lhs,t1) && lhs = t2
*/
static bool is_lhs_eq_rhs_ite_else(ast_manager & m, expr * lhs, expr * rhs) {
return m.is_ite(rhs) && lhs == to_app(rhs)->get_arg(2) && m.are_distinct(lhs, to_app(rhs)->get_arg(1));
}
void basic_simplifier_plugin::mk_eq(expr * lhs, expr * rhs, expr_ref & result) {
// (= t1 (ite C t2 t3)) --> false if are_distinct(t1, t2) && are_distinct(t1, t3)
if (is_lhs_diseq_rhs_ite_branches(m_manager, lhs, rhs) || is_lhs_diseq_rhs_ite_branches(m_manager, rhs, lhs)) {
result = m_manager.mk_false();
}
// (= t1 (ite C t2 t3)) --> C if t1 = t2 && are_distinct(t1, t3)
else if (is_lhs_eq_rhs_ite_then(m_manager, lhs, rhs)) {
result = to_app(rhs)->get_arg(0);
}
// (= t1 (ite C t2 t3)) --> C if t1 = t2 && are_distinct(t1, t3)
else if (is_lhs_eq_rhs_ite_then(m_manager, rhs, lhs)) {
result = to_app(lhs)->get_arg(0);
}
// (= t1 (ite C t2 t3)) --> (not C) if t1 = t3 && are_distinct(t1, t2)
else if (is_lhs_eq_rhs_ite_else(m_manager, lhs, rhs)) {
mk_not(to_app(rhs)->get_arg(0), result);
}
// (= t1 (ite C t2 t3)) --> (not C) if t1 = t3 && are_distinct(t1, t2)
else if (is_lhs_eq_rhs_ite_else(m_manager, rhs, lhs)) {
mk_not(to_app(lhs)->get_arg(0), result);
}
else {
m_rewriter->mk_eq(lhs, rhs, result);
}
}
bool basic_simplifier_plugin::eliminate_and() const { return m_rewriter->elim_and(); }
void basic_simplifier_plugin::set_eliminate_and(bool f) { m_rewriter->set_elim_and(f); }
void basic_simplifier_plugin::mk_iff(expr * lhs, expr * rhs, expr_ref & result) { mk_eq(lhs, rhs, result); }
void basic_simplifier_plugin::mk_xor(expr * lhs, expr * rhs, expr_ref & result) { m_rewriter->mk_xor(lhs, rhs, result); }
void basic_simplifier_plugin::mk_implies(expr * lhs, expr * rhs, expr_ref & result) { m_rewriter->mk_implies(lhs, rhs, result); }
void basic_simplifier_plugin::mk_ite(expr * c, expr * t, expr * e, expr_ref & result) { m_rewriter->mk_ite(c, t, e, result); }
void basic_simplifier_plugin::mk_and(unsigned num_args, expr * const * args, expr_ref & result) { m_rewriter->mk_and(num_args, args, result); }
void basic_simplifier_plugin::mk_or(unsigned num_args, expr * const * args, expr_ref & result) { m_rewriter->mk_or(num_args, args, result); }
void basic_simplifier_plugin::mk_and(expr * arg1, expr * arg2, expr_ref & result) { m_rewriter->mk_and(arg1, arg2, result); }
void basic_simplifier_plugin::mk_or(expr * arg1, expr * arg2, expr_ref & result) { m_rewriter->mk_or(arg1, arg2, result); }
void basic_simplifier_plugin::mk_and(expr * arg1, expr * arg2, expr * arg3, expr_ref & result) { m_rewriter->mk_and(arg1, arg2, arg3, result); }
void basic_simplifier_plugin::mk_or(expr * arg1, expr * arg2, expr * arg3, expr_ref & result) { m_rewriter->mk_or(arg1, arg2, arg3, result); }
void basic_simplifier_plugin::mk_nand(unsigned num_args, expr * const * args, expr_ref & result) { m_rewriter->mk_nand(num_args, args, result); }
void basic_simplifier_plugin::mk_nor(unsigned num_args, expr * const * args, expr_ref & result) { m_rewriter->mk_nor(num_args, args, result); }
void basic_simplifier_plugin::mk_nand(expr * arg1, expr * arg2, expr_ref & result) { m_rewriter->mk_nand(arg1, arg2, result); }
void basic_simplifier_plugin::mk_nor(expr * arg1, expr * arg2, expr_ref & result) { m_rewriter->mk_nor(arg1, arg2, result); }
void basic_simplifier_plugin::mk_distinct(unsigned num_args, expr * const * args, expr_ref & result) { m_rewriter->mk_distinct(num_args, args, result); }
void basic_simplifier_plugin::mk_not(expr * n, expr_ref & result) { m_rewriter->mk_not(n, result); }
void basic_simplifier_plugin::enable_ac_support(bool flag) {
m_rewriter->set_flat(flag);
}

78
src/ast/simplifier/basic_simplifier_plugin.h
View file

@ -1,78 +0,0 @@
/*++
Copyright (c) 2007 Microsoft Corporation
Module Name:
basic_simplifier_plugin.h
Abstract:
Simplifier for the basic family.
Author:
Leonardo (leonardo) 2008-01-07
--*/
#ifndef BASIC_SIMPLIFIER_PLUGIN_H_
#define BASIC_SIMPLIFIER_PLUGIN_H_
#include "ast/simplifier/simplifier_plugin.h"
class bool_rewriter;
/**
\brief Simplifier for the basic family.
*/
class basic_simplifier_plugin : public simplifier_plugin {
bool_rewriter * m_rewriter;
public:
basic_simplifier_plugin(ast_manager & m);
virtual ~basic_simplifier_plugin();
bool_rewriter & get_rewriter() { return *m_rewriter; }
bool eliminate_and() const;
void set_eliminate_and(bool f);
void mk_eq(expr * lhs, expr * rhs, expr_ref & result);
void mk_iff(expr * lhs, expr * rhs, expr_ref & result);
void mk_xor(expr * lhs, expr * rhs, expr_ref & result);
void mk_implies(expr * lhs, expr * rhs, expr_ref & result);
void mk_ite(expr * c, expr * t, expr * e, expr_ref & result);
void mk_and(unsigned num_args, expr * const * args, expr_ref & result);
void mk_or(unsigned num_args, expr * const * args, expr_ref & result);
void mk_and(expr * arg1, expr * arg2, expr_ref & result);
void mk_or(expr * arg1, expr * arg2, expr_ref & result);
void mk_and(expr * arg1, expr * arg2, expr * arg3, expr_ref & result);
void mk_or(expr * arg1, expr * arg2, expr * arg3, expr_ref & result);
void mk_nand(unsigned num_args, expr * const * args, expr_ref & result);
void mk_nor(unsigned num_args, expr * const * args, expr_ref & result);
void mk_nand(expr * arg1, expr * arg2, expr_ref & result);
void mk_nor(expr * arg1, expr * arg2, expr_ref & result);
void mk_distinct(unsigned num_args, expr * const * args, expr_ref & result);
void mk_not(expr * n, expr_ref & result);
virtual bool reduce(func_decl * f, unsigned num_args, expr * const * args, expr_ref & result);
virtual void enable_ac_support(bool flag);
};
/**
\brief Functor that compares expressions, but puts the expressions e and f(e) close to each other, where
f is in family m_fid, and has kind m_dkind;
*/
struct expr_lt_proc {
family_id m_fid;
decl_kind m_dkind;
expr_lt_proc(family_id fid = null_family_id, decl_kind k = null_decl_kind):m_fid(fid), m_dkind(k) {}
unsigned get_id(expr * n) const {
if (m_fid != null_family_id && is_app_of(n, m_fid, m_dkind))
return (to_app(n)->get_arg(0)->get_id() << 1) + 1;
else
return n->get_id() << 1;
}
bool operator()(expr * n1, expr * n2) const {
return get_id(n1) < get_id(n2);
}
};
#endif /* BASIC_SIMPLIFIER_PLUGIN_H_ */

119
src/ast/simplifier/bv_elim.cpp
View file

@ -1,119 +0,0 @@
/*++
Copyright (c) 2015 Microsoft Corporation
--*/
#include "ast/simplifier/bv_elim.h"
#include "ast/bv_decl_plugin.h"
#include "ast/rewriter/var_subst.h"
#include <sstream>
void bv_elim::elim(quantifier* q, quantifier_ref& r) {
svector<symbol> names, _names;
sort_ref_buffer sorts(m), _sorts(m);
expr_ref_buffer pats(m);
expr_ref_buffer no_pats(m);
expr_ref_buffer subst_map(m), _subst_map(m);
var_subst subst(m);
bv_util bv(m);
expr_ref new_body(m);
expr* old_body = q->get_expr();
unsigned num_decls = q->get_num_decls();
family_id bfid = m.mk_family_id("bv");
//
// Traverse sequence of bound variables to eliminate
// bit-vecctor variables and replace them by
// Booleans.
//
unsigned var_idx = 0;
for (unsigned i = num_decls; i > 0; ) {
--i;
sort* s = q->get_decl_sort(i);
symbol nm = q->get_decl_name(i);
if (bv.is_bv_sort(s)) {
// convert n-bit bit-vector variable into sequence of n-Booleans.
unsigned num_bits = bv.get_bv_size(s);
expr_ref_buffer args(m);
expr_ref bv(m);
for (unsigned j = 0; j < num_bits; ++j) {
std::ostringstream new_name;
new_name << nm.str();
new_name << "_";
new_name << j;
var* v = m.mk_var(var_idx++, m.mk_bool_sort());
args.push_back(v);
_sorts.push_back(m.mk_bool_sort());
_names.push_back(symbol(new_name.str().c_str()));
}
bv = m.mk_app(bfid, OP_MKBV, 0, 0, args.size(), args.c_ptr());
_subst_map.push_back(bv.get());
}
else {
_subst_map.push_back(m.mk_var(var_idx++, s));
_sorts.push_back(s);
_names.push_back(nm);
}
}
//
// reverse the vectors.
//
SASSERT(_names.size() == _sorts.size());
for (unsigned i = _names.size(); i > 0; ) {
--i;
names.push_back(_names[i]);
sorts.push_back(_sorts[i]);
}
for (unsigned i = _subst_map.size(); i > 0; ) {
--i;
subst_map.push_back(_subst_map[i]);
}
expr* const* sub = subst_map.c_ptr();
unsigned sub_size = subst_map.size();
subst(old_body, sub_size, sub, new_body);
for (unsigned j = 0; j < q->get_num_patterns(); j++) {
expr_ref pat(m);
subst(q->get_pattern(j), sub_size, sub, pat);
pats.push_back(pat);
}
for (unsigned j = 0; j < q->get_num_no_patterns(); j++) {
expr_ref nopat(m);
subst(q->get_no_pattern(j), sub_size, sub, nopat);
no_pats.push_back(nopat);
}
r = m.mk_quantifier(true,
names.size(),
sorts.c_ptr(),
names.c_ptr(),
new_body.get(),
q->get_weight(),
q->get_qid(),
q->get_skid(),
pats.size(), pats.c_ptr(),
no_pats.size(), no_pats.c_ptr());
}
bool bv_elim_star::visit_quantifier(quantifier* q) {
// behave like destructive resolution, do not recurse.
return true;
}
void bv_elim_star::reduce1_quantifier(quantifier* q) {
quantifier_ref r(m);
proof_ref pr(m);
m_bv_elim.elim(q, r);
if (m.fine_grain_proofs()) {
pr = m.mk_rewrite(q, r.get());
}
else {
pr = 0;
}
cache_result(q, r, pr);
}

45
src/ast/simplifier/bv_elim.h
View file

@ -1,45 +0,0 @@
/*++
Copyright (c) 2006 Microsoft Corporation
Module Name:
bv_elim.h
Abstract:
Eliminate bit-vectors variables from clauses, by
replacing them by bound Boolean variables.
Author:
Nikolaj Bjorner (nbjorner) 2008-12-16.
Revision History:
--*/
#ifndef BV_ELIM_H_
#define BV_ELIM_H_
#include "ast/ast.h"
#include "ast/simplifier/simplifier.h"
class bv_elim {
ast_manager& m;
public:
bv_elim(ast_manager& m) : m(m) {};
void elim(quantifier* q, quantifier_ref& r);
};
class bv_elim_star : public simplifier {
protected:
bv_elim m_bv_elim;
virtual bool visit_quantifier(quantifier* q);
virtual void reduce1_quantifier(quantifier* q);
public:
bv_elim_star(ast_manager& m) : simplifier(m), m_bv_elim(m) { enable_ac_support(false); }
virtual ~bv_elim_star() {}
};
#endif /* BV_ELIM_H_ */

36
src/ast/simplifier/bv_simplifier_params.cpp
View file

@ -1,36 +0,0 @@
/*++
Copyright (c) 2006 Microsoft Corporation
Module Name:
bv_simplifier_params.cpp
Abstract:
<abstract>
Author:
Leonardo de Moura (leonardo) 2012-12-02.
Revision History:
--*/
#include "ast/simplifier/bv_simplifier_params.h"
#include "ast/simplifier/bv_simplifier_params_helper.hpp"
#include "ast/rewriter/bv_rewriter_params.hpp"
void bv_simplifier_params::updt_params(params_ref const & _p) {
bv_simplifier_params_helper p(_p);
bv_rewriter_params rp(_p);
m_hi_div0 = rp.hi_div0();
m_bv2int_distribute = p.bv_bv2int_distribute();
}
#define DISPLAY_PARAM(X) out << #X"=" << X << std::endl;
void bv_simplifier_params::display(std::ostream & out) const {
DISPLAY_PARAM(m_hi_div0);
DISPLAY_PARAM(m_bv2int_distribute);
}

38
src/ast/simplifier/bv_simplifier_params.h
View file

@ -1,38 +0,0 @@
/*++
Copyright (c) 2006 Microsoft Corporation
Module Name:
bv_simplifier_params.h
Abstract:
<abstract>
Author:
Leonardo de Moura (leonardo) 2008-10-10.
Revision History:
--*/
#ifndef BV_SIMPLIFIER_PARAMS_H_
#define BV_SIMPLIFIER_PARAMS_H_
#include "util/params.h"
struct bv_simplifier_params {
bool m_hi_div0; //!< if true, uses the hardware interpretation for div0, mod0, ... if false, div0, mod0, ... are considered uninterpreted.
bool m_bv2int_distribute; //!< if true allows downward propagation of bv2int.
bv_simplifier_params(params_ref const & p = params_ref()) {
updt_params(p);
}
void updt_params(params_ref const & _p);
void display(std::ostream & out) const;
};
#endif /* BV_SIMPLIFIER_PARAMS_H_ */

4
src/ast/simplifier/bv_simplifier_params_helper.pyg
View file

@ -1,4 +0,0 @@
def_module_params(class_name='bv_simplifier_params_helper',
module_name="old_simplify", # Parameters will be in the old_simplify module
export=True,
params=(('bv.bv2int_distribute', BOOL, True, 'if true, then int2bv is distributed over arithmetical operators'),))

2261
src/ast/simplifier/bv_simplifier_plugin.cpp
View file

File diff suppressed because it is too large Load diff

187
src/ast/simplifier/bv_simplifier_plugin.h
View file

@ -1,187 +0,0 @@
/*++
Copyright (c) 2007 Microsoft Corporation
Module Name:
bv_simplifier_plugin.h
Abstract:
Simplifier for the bv family.
Author:
Leonardo (leonardo) 2008-01-08
--*/
#ifndef BV_SIMPLIFIER_PLUGIN_H_
#define BV_SIMPLIFIER_PLUGIN_H_
#include "ast/simplifier/basic_simplifier_plugin.h"
#include "ast/simplifier/poly_simplifier_plugin.h"
#include "ast/bv_decl_plugin.h"
#include "util/map.h"
#include "ast/simplifier/bv_simplifier_params.h"
#include "ast/arith_decl_plugin.h"
/**
\brief Simplifier for the bv family.
*/
class bv_simplifier_plugin : public poly_simplifier_plugin {
typedef rational numeral;
struct extract_entry {
unsigned m_high;
unsigned m_low;
expr * m_arg;
extract_entry():m_high(0), m_low(0), m_arg(0) {}
extract_entry(unsigned h, unsigned l, expr * n):m_high(h), m_low(l), m_arg(n) {}
unsigned hash() const {
unsigned a = m_high;
unsigned b = m_low;
unsigned c = m_arg->get_id();
mix(a,b,c);
return c;
}
bool operator==(const extract_entry & e) const {
return m_high == e.m_high && m_low == e.m_low && m_arg == e.m_arg;
}
struct hash_proc {
unsigned operator()(extract_entry const& e) const { return e.hash(); }
};
struct eq_proc {
bool operator()(extract_entry const& a, extract_entry const& b) const { return a == b; }
};
};
typedef map<extract_entry, expr *, extract_entry::hash_proc , extract_entry::eq_proc > extract_cache;
protected:
ast_manager& m_manager;
bv_util m_util;
arith_util m_arith;
basic_simplifier_plugin & m_bsimp;
bv_simplifier_params & m_params;
expr_ref_vector m_zeros;
extract_cache m_extract_cache;
unsigned_vector m_lows, m_highs;
ptr_vector<expr> m_extract_args;
rational mk_bv_and(numeral const& a0, numeral const& b0, unsigned sz);
rational mk_bv_or(numeral const& a0, numeral const& b0, unsigned sz);
rational mk_bv_xor(numeral const& a0, numeral const& b0, unsigned sz);
rational mk_bv_not(numeral const& a0, unsigned sz);
rational num(expr* e);
bool has_sign_bit(numeral const& n, unsigned bv_size) { return m_util.has_sign_bit(n, bv_size); }
bool shift_shift(bv_op_kind k, expr* arg1, expr* arg2, expr_ref& result);
void bit2bool_simplify(unsigned idx, expr* e, expr_ref& result);
void mk_add_concat(expr_ref& result);
bool is_zero_bit(expr* x, unsigned idx);
void mk_bv_rotate_left_core(unsigned shift, numeral r, unsigned bv_size, expr_ref& result);
void mk_bv_rotate_right_core(unsigned shift, numeral r, unsigned bv_size, expr_ref& result);
public:
bv_simplifier_plugin(ast_manager & m, basic_simplifier_plugin & b, bv_simplifier_params & p);
virtual ~bv_simplifier_plugin();
// simplifier_plugin:
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);
virtual bool reduce_distinct(unsigned num_args, expr * const * args, expr_ref & result);
virtual void flush_caches();
// poly_simplifier_plugin
virtual rational norm(const rational & n);
virtual bool is_numeral(expr * n, rational & val) const;
bool is_numeral(expr * n) const { return m_util.is_numeral(n); }
virtual bool is_minus_one(expr * n) const { return is_minus_one_core(n); }
virtual expr * get_zero(sort * s) const;
virtual app * mk_numeral(rational const & n);
bool is_bv(expr * n) const { return m_util.is_bv(n); }
bool is_bv_sort(sort * s) const { return m_util.is_bv_sort(s); }
bool is_le(expr * n) const { return m_util.is_bv_ule(n) || m_util.is_bv_sle(n); }
// REMARK: simplified bv expressions are never of the form a >= b.
virtual bool is_le_ge(expr * n) const { return is_le(n); }
uint64 to_uint64(const numeral & n, unsigned bv_size);
rational norm(rational const& n, unsigned bv_size, bool is_signed) { return m_util.norm(n, bv_size, is_signed); }
unsigned get_bv_size(expr const * n) { return get_bv_size(m_manager.get_sort(n)); }
unsigned get_bv_size(sort const * s) { return m_util.get_bv_size(s); }
void mk_leq_core(bool is_signed, expr * arg1, expr * arg2, expr_ref & result);
void mk_ule(expr* a, expr* b, expr_ref& result);
void mk_ult(expr* a, expr* b, expr_ref& result);
void mk_sle(expr* a, expr* b, expr_ref& result);
void mk_slt(expr* a, expr* b, expr_ref& result);
void mk_bv_and(unsigned num_args, expr * const* args, expr_ref & result);
void mk_bv_or(unsigned num_args, expr * const* args, expr_ref & result);
void mk_bv_xor(unsigned num_args, expr * const* args, expr_ref & result);
void mk_bv_not(expr * arg, expr_ref & result);
void mk_extract(unsigned hi,unsigned lo, expr* bv, expr_ref& result);
void mk_extract_core(unsigned high, unsigned low, expr * arg, expr_ref& result);
void cache_extract(unsigned h, unsigned l, expr * arg, expr * result);
expr* get_cached_extract(unsigned h, unsigned l, expr * arg);
bool lookup_mk_extract(unsigned high, unsigned low, expr * arg, expr_ref& result);
bool try_mk_extract(unsigned high, unsigned low, expr * arg, expr_ref& result);
void mk_bv_eq(expr* a1, expr* a2, expr_ref& result);
void mk_eq_core(expr * arg1, expr * arg2, expr_ref & result);
void mk_args_eq_numeral(app * app, expr * n, expr_ref & result);
void mk_concat(unsigned num_args, expr * const * args, expr_ref & result);
void mk_concat(expr * arg1, expr * arg2, expr_ref & result) {
expr * args[2] = { arg1, arg2 };
mk_concat(2, args, result);
}
void mk_zeroext(unsigned n, expr * arg, expr_ref & result);
void mk_repeat(unsigned n, expr * arg, expr_ref & result);
void mk_sign_extend(unsigned n, expr * arg, expr_ref & result);
void mk_bv_lshr(expr * arg1, expr * arg2, expr_ref & result);
void mk_bv_shl(expr * arg1, expr * arg2, expr_ref & result);
void mk_bv_ashr(expr* arg1, expr* arg2, expr_ref& result);
void mk_bv_smod(expr* arg1, expr* arg2, expr_ref& result);
void mk_bv_urem(expr * arg1, expr * arg2, expr_ref & result);
void mk_bv_srem(expr* arg1, expr* arg2, expr_ref& result);
void mk_bv_udiv(expr* arg1, expr* arg2, expr_ref& result);
void mk_bv_sdiv(expr* arg1, expr* arg2, expr_ref& result);
void mk_bv_smod_i(expr* arg1, expr* arg2, expr_ref& result);
void mk_bv_urem_i(expr * arg1, expr * arg2, expr_ref & result);
void mk_bv_srem_i(expr* arg1, expr* arg2, expr_ref& result);
void mk_bv_udiv_i(expr* arg1, expr* arg2, expr_ref& result);
void mk_bv_sdiv_i(expr* arg1, expr* arg2, expr_ref& result);
void mk_bv_nand(unsigned num_args, expr* const* args, expr_ref& result);
void mk_bv_nor(unsigned num_args, expr* const* args, expr_ref& result);
void mk_bv_xnor(unsigned num_args, expr* const* args, expr_ref& result);
void mk_bv_rotate_right(func_decl* f, expr* arg, expr_ref& result);
void mk_bv_rotate_left(func_decl* f, expr* arg, expr_ref& result);
void mk_bv_ext_rotate_right(expr* arg1, expr* arg2, expr_ref& result);
void mk_bv_ext_rotate_left(expr* arg1, expr* arg2, expr_ref& result);
void mk_bv_redor(expr* arg, expr_ref& result);
void mk_bv_redand(expr* arg, expr_ref& result);
void mk_bv_comp(expr* arg1, expr* arg2, expr_ref& result);
bool are_numerals(unsigned num_args, expr * const* args, unsigned& bv_size);
app * mk_numeral(rational const & n, unsigned bv_size);
app * mk_numeral(uint64 n, unsigned bv_size) { return mk_numeral(numeral(n, numeral::ui64()), bv_size); }
app* mk_bv0(unsigned bv_size) { return m_util.mk_numeral(numeral(0), bv_size); }
rational mk_allone(unsigned bv_size) { return rational::power_of_two(bv_size) - numeral(1); }
bool is_minus_one_core(expr * arg) const;
bool is_x_minus_one(expr * arg, expr * & x);
void mk_int2bv(expr * arg, sort* range, expr_ref & result);
void mk_bv2int(expr * arg, sort* range, expr_ref & result);
uint64 n64(expr* e);
bool is_mul_no_overflow(expr* e);
bool is_add_no_overflow(expr* e);
unsigned num_leading_zero_bits(expr* e);
};
#endif /* BV_SIMPLIFIER_PLUGIN_H_ */

115
src/ast/simplifier/datatype_simplifier_plugin.cpp
View file

@ -1,115 +0,0 @@
/*++
Copyright (c) 2008 Microsoft Corporation
Module Name:
datatype_simplifier_plugin.cpp
Abstract:
Simplifier for algebraic datatypes.
Author:
nbjorner 2008-11-6
--*/
#include "ast/simplifier/datatype_simplifier_plugin.h"
datatype_simplifier_plugin::datatype_simplifier_plugin(ast_manager & m, basic_simplifier_plugin & b):
simplifier_plugin(symbol("datatype"), m),
m_util(m),
m_bsimp(b) {
}
datatype_simplifier_plugin::~datatype_simplifier_plugin() {
}
bool datatype_simplifier_plugin::reduce(func_decl * f, unsigned num_args, expr * const * args, expr_ref & result) {
set_reduce_invoked();
SASSERT(f->get_family_id() == get_family_id());
switch(f->get_decl_kind()) {
case OP_DT_CONSTRUCTOR: {
return false;
}
case OP_DT_RECOGNISER: {
//
// simplify is_cons(cons(x,y)) -> true
// simplify is_cons(nil) -> false
//
SASSERT(num_args == 1);
if (!is_app_of(args[0], get_family_id(), OP_DT_CONSTRUCTOR)) {
return false;
}
app* a = to_app(args[0]);
func_decl* f1 = a->get_decl();
func_decl* f2 = m_util.get_recognizer_constructor(f);
if (f1 == f2) {
result = m_manager.mk_true();
}
else {
result = m_manager.mk_false();
}
return true;
}
case OP_DT_ACCESSOR: {
//
// simplify head(cons(x,y)) -> x
//
SASSERT(num_args == 1);
if (!is_app_of(args[0], get_family_id(), OP_DT_CONSTRUCTOR)) {
return false;
}
app* a = to_app(args[0]);
func_decl* f1 = a->get_decl();
func_decl* f2 = m_util.get_accessor_constructor(f);
if (f1 != f2) {
return false;
}
ptr_vector<func_decl> const* acc = m_util.get_constructor_accessors(f1);
SASSERT(acc && acc->size() == a->get_num_args());
for (unsigned i = 0; i < acc->size(); ++i) {
if (f == (*acc)[i]) {
// found it.
result = a->get_arg(i);
return true;
}
}
UNREACHABLE();
}
case OP_DT_UPDATE_FIELD:
return false;
default:
UNREACHABLE();
}
return false;
}
bool datatype_simplifier_plugin::reduce_eq(expr * lhs, expr * rhs, expr_ref & result) {
set_reduce_invoked();
if (is_app_of(lhs, get_family_id(), OP_DT_CONSTRUCTOR) &&
is_app_of(rhs, get_family_id(), OP_DT_CONSTRUCTOR)) {
app* a = to_app(lhs);
app* b = to_app(rhs);
if (a->get_decl() != b->get_decl()) {
result = m_manager.mk_false();
return true;
}
expr_ref_vector eqs(m_manager);
for (unsigned i = 0; i < a->get_num_args(); ++i) {
m_bsimp.mk_eq(a->get_arg(i),b->get_arg(i), result);
eqs.push_back(result);
}
m_bsimp.mk_and(eqs.size(), eqs.c_ptr(), result);
return true;
}
// TBD: occurs check, constructor check.
return false;
}

42
src/ast/simplifier/datatype_simplifier_plugin.h
View file

@ -1,42 +0,0 @@
/*++
Copyright (c) 2008 Microsoft Corporation
Module Name:
datatype_simplifier_plugin.h
Abstract:
Simplifier for algebraic datatypes.
Author:
nbjorner 2008-11-6
--*/
#ifndef DATATYPE_SIMPLIFIER_PLUGIN_H_
#define DATATYPE_SIMPLIFIER_PLUGIN_H_
#include "ast/simplifier/basic_simplifier_plugin.h"
#include "ast/datatype_decl_plugin.h"
/**
\brief Simplifier for the arith family.
*/
class datatype_simplifier_plugin : public simplifier_plugin {
datatype_util m_util;
basic_simplifier_plugin & m_bsimp;
public:
datatype_simplifier_plugin(ast_manager & m, basic_simplifier_plugin & b);
~datatype_simplifier_plugin();
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);
};
#endif /* DATATYPE_SIMPLIFIER_PLUGIN_H_ */

224
src/ast/simplifier/elim_bounds.cpp
View file

@ -1,224 +0,0 @@
/*++
Copyright (c) 2006 Microsoft Corporation
Module Name:
elim_bounds.cpp
Abstract:
<abstract>
Author:
Leonardo de Moura (leonardo) 2008-06-28.
Revision History:
--*/
#include "ast/simplifier/elim_bounds.h"
#include "ast/used_vars.h"
#include "util/obj_hashtable.h"
#include "ast/rewriter/var_subst.h"
#include "ast/ast_pp.h"
elim_bounds::elim_bounds(ast_manager & m):
m_manager(m),
m_util(m) {
}
/**
\brief Find bounds of the form
(<= x k)
(<= (+ x (* -1 y)) k)
(<= (+ x (* -1 t)) k)
(<= (+ t (* -1 x)) k)
x and y are a bound variables, t is a ground term and k is a numeral
It also detects >=, and the atom can be negated.
*/
bool elim_bounds::is_bound(expr * n, var * & lower, var * & upper) {
upper = 0;
lower = 0;
bool neg = false;
if (m_manager.is_not(n)) {
n = to_app(n)->get_arg(0);
neg = true;
}
bool le = false;
if (m_util.is_le(n)) {
SASSERT(m_util.is_numeral(to_app(n)->get_arg(1)));
n = to_app(n)->get_arg(0);
le = true;
}
else if (m_util.is_ge(n)) {
SASSERT(m_util.is_numeral(to_app(n)->get_arg(1)));
n = to_app(n)->get_arg(0);
le = false;
}
else {
return false;
}
if (neg)
le = !le;
if (is_var(n)) {
upper = to_var(n);
}
else if (m_util.is_add(n) && to_app(n)->get_num_args() == 2) {
expr * arg1 = to_app(n)->get_arg(0);
expr * arg2 = to_app(n)->get_arg(1);
if (is_var(arg1))
upper = to_var(arg1);
else if (!is_ground(arg1))
return false;
rational k;
bool is_int;
if (m_util.is_mul(arg2) && m_util.is_numeral(to_app(arg2)->get_arg(0), k, is_int) && k.is_minus_one()) {
arg2 = to_app(arg2)->get_arg(1);
if (is_var(arg2))
lower = to_var(arg2);
else if (!is_ground(arg2))
return false; // not supported
}
else {
return false; // not supported
}
}
else {
return false;
}
if (!le)
std::swap(upper, lower);
return true;
}
bool elim_bounds::is_bound(expr * n) {
var * lower, * upper;
return is_bound(n, lower, upper);
}
void elim_bounds::operator()(quantifier * q, expr_ref & r) {
if (!q->is_forall()) {
r = q;
return;
}
expr * n = q->get_expr();
unsigned num_vars = q->get_num_decls();
ptr_buffer<expr> atoms;
if (m_manager.is_or(n))
atoms.append(to_app(n)->get_num_args(), to_app(n)->get_args());
else
atoms.push_back(n);
used_vars m_used_vars;
// collect non-candidates
unsigned sz = atoms.size();
for (unsigned i = 0; i < sz; i++) {
expr * a = atoms[i];
if (!is_bound(a))
m_used_vars.process(a);
}
if (m_used_vars.uses_all_vars(q->get_num_decls())) {
r = q;
return;
}
// collect candidates
obj_hashtable<var> m_lowers;
obj_hashtable<var> m_uppers;
obj_hashtable<var> m_candidate_set;
ptr_buffer<var> m_candidates;
#define ADD_CANDIDATE(V) if (!m_lowers.contains(V) && !m_uppers.contains(V)) { m_candidate_set.insert(V); m_candidates.push_back(V); }
for (unsigned i = 0; i < sz; i++) {
expr * a = atoms[i];
var * lower = 0;
var * upper = 0;
if (is_bound(a, lower, upper)) {
if (lower != 0 && !m_used_vars.contains(lower->get_idx()) && lower->get_idx() < num_vars) {
ADD_CANDIDATE(lower);
m_lowers.insert(lower);
}
if (upper != 0 && !m_used_vars.contains(upper->get_idx()) && upper->get_idx() < num_vars) {
ADD_CANDIDATE(upper);
m_uppers.insert(upper);
}
}
}
TRACE("elim_bounds", tout << "candidates:\n"; for (unsigned i = 0; i < m_candidates.size(); i++) tout << mk_pp(m_candidates[i], m_manager) << "\n";);
// remove candidates that have lower and upper bounds
for (unsigned i = 0; i < m_candidates.size(); i++) {
var * v = m_candidates[i];
if (m_lowers.contains(v) && m_uppers.contains(v))
m_candidate_set.erase(v);
}
TRACE("elim_bounds", tout << "candidates after filter:\n"; for (unsigned i = 0; i < m_candidates.size(); i++) tout << mk_pp(m_candidates[i], m_manager) << "\n";);
if (m_candidate_set.empty()) {
r = q;
return;
}
// remove bounds that contain variables in m_candidate_set
unsigned j = 0;
for (unsigned i = 0; i < sz; i++) {
expr * a = atoms[i];
var * lower = 0;
var * upper = 0;
if (is_bound(a, lower, upper) && ((lower != 0 && m_candidate_set.contains(lower)) || (upper != 0 && m_candidate_set.contains(upper))))
continue;
atoms[j] = a;
j++;
}
atoms.resize(j);
expr * new_body = 0;
switch (atoms.size()) {
case 0:
r = m_manager.mk_false();
TRACE("elim_bounds", tout << mk_pp(q, m_manager) << "\n" << mk_pp(r, m_manager) << "\n";);
return;
case 1:
new_body = atoms[0];
break;
default:
new_body = m_manager.mk_or(atoms.size(), atoms.c_ptr());
break;
}
quantifier_ref new_q(m_manager);
new_q = m_manager.update_quantifier(q, new_body);
elim_unused_vars(m_manager, new_q, params_ref(), r);
TRACE("elim_bounds", tout << mk_pp(q, m_manager) << "\n" << mk_pp(r, m_manager) << "\n";);
}
bool elim_bounds_star::visit_quantifier(quantifier * q) {
if (!q->is_forall() || q->get_num_patterns() != 0)
return true;
bool visited = true;
visit(q->get_expr(), visited);
return visited;
}
void elim_bounds_star::reduce1_quantifier(quantifier * q) {
if (!q->is_forall() || q->get_num_patterns() != 0) {
cache_result(q, q, 0);
return;
}
quantifier_ref new_q(m);
expr * new_body = 0;
proof * new_pr;
get_cached(q->get_expr(), new_body, new_pr);
new_q = m.update_quantifier(q, new_body);
expr_ref r(m);
m_elim(new_q, r);
if (q == r.get()) {
cache_result(q, q, 0);
return;
}
proof_ref pr(m);
if (m.fine_grain_proofs())
pr = m.mk_rewrite(q, r); // TODO: improve justification
cache_result(q, r, pr);
}

69
src/ast/simplifier/elim_bounds.h
View file

@ -1,69 +0,0 @@
/*++
Copyright (c) 2006 Microsoft Corporation
Module Name:
elim_bounds.h
Abstract:
<abstract>
Author:
Leonardo de Moura (leonardo) 2008-06-28.
Revision History:
--*/
#ifndef ELIM_BOUNDS_H_
#define ELIM_BOUNDS_H_
#include "ast/ast.h"
#include "ast/arith_decl_plugin.h"
#include "ast/simplifier/simplifier.h"
/**
\brief Functor for eliminating irrelevant bounds in quantified formulas.
Example:
(forall (x Int) (y Int) (or (not (>= y x) (not (>= x 0)) (= (select a x) 1))))
The bound (>= y x) is irrelevant and can be eliminated.
This can be easily proved by using Fourier-Motzkin elimination.
Limitations & Assumptions:
- It assumes the input formula was already simplified.
- It can only handle bounds in the diff-logic fragment.
\remark This operation is subsumed by Fourier-Motzkin elimination.
*/
class elim_bounds {
ast_manager & m_manager;
arith_util m_util;
bool is_bound(expr * n, var * & lower, var * & upper);
bool is_bound(expr * n);
public:
elim_bounds(ast_manager & m);
void operator()(quantifier * q, expr_ref & r);
};
/**
\brief Functor for applying elim_bounds in all
universal quantifiers in an expression.
Assumption: the formula was already skolemized.
*/
class elim_bounds_star : public simplifier {
protected:
elim_bounds m_elim;
virtual bool visit_quantifier(quantifier * q);
virtual void reduce1_quantifier(quantifier * q);
public:
elim_bounds_star(ast_manager & m):simplifier(m), m_elim(m) { enable_ac_support(false); }
virtual ~elim_bounds_star() {}
};
#endif /* ELIM_BOUNDS_H_ */

39
src/ast/simplifier/fpa_simplifier_plugin.cpp
View file

@ -1,39 +0,0 @@
/*++
Copyright (c) 2015 Microsoft Corporation
Module Name:
fpa_simplifier_plugin.cpp
Abstract:
Simplifier for the floating-point theory
Author:
Christoph (cwinter) 2015-01-14
--*/
#include "ast/simplifier/fpa_simplifier_plugin.h"
fpa_simplifier_plugin::fpa_simplifier_plugin(ast_manager & m, basic_simplifier_plugin & b) :
simplifier_plugin(symbol("fpa"), m),
m_util(m),
m_rw(m) {}
fpa_simplifier_plugin::~fpa_simplifier_plugin() {}
bool fpa_simplifier_plugin::reduce(func_decl * f, unsigned num_args, expr * const * args, expr_ref & result) {
set_reduce_invoked();
SASSERT(f->get_family_id() == get_family_id());
return m_rw.mk_app_core(f, num_args, args, result) != BR_FAILED;
}
bool fpa_simplifier_plugin::reduce_eq(expr * lhs, expr * rhs, expr_ref & result) {
set_reduce_invoked();
return m_rw.mk_eq_core(lhs, rhs, result) != BR_FAILED;
}

39
src/ast/simplifier/fpa_simplifier_plugin.h
View file

@ -1,39 +0,0 @@
/*++
Copyright (c) 2015 Microsoft Corporation
Module Name:
fpa_simplifier_plugin.h
Abstract:
Simplifier for the floating-point theory
Author:
Christoph (cwinter) 2015-01-14
--*/
#ifndef FPA_SIMPLIFIER_PLUGIN_H_
#define FPA_SIMPLIFIER_PLUGIN_H_
#include "ast/simplifier/basic_simplifier_plugin.h"
#include "ast/fpa_decl_plugin.h"
#include "ast/rewriter/fpa_rewriter.h"
class fpa_simplifier_plugin : public simplifier_plugin {
fpa_util m_util;
fpa_rewriter m_rw;
public:
fpa_simplifier_plugin(ast_manager & m, basic_simplifier_plugin & b);
~fpa_simplifier_plugin();
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);
};
#endif /* FPA_SIMPLIFIER_PLUGIN_H_ */

835
src/ast/simplifier/poly_simplifier_plugin.cpp
View file

@ -1,835 +0,0 @@
/*++
Copyright (c) 2007 Microsoft Corporation
Module Name:
poly_simplifier_plugin.cpp
Abstract:
Abstract class for families that have polynomials.
Author:
Leonardo (leonardo) 2008-01-08
--*/
#include "ast/simplifier/poly_simplifier_plugin.h"
#include "ast/ast_pp.h"
#include "ast/ast_util.h"
#include "ast/ast_smt2_pp.h"
#include "ast/ast_ll_pp.h"
poly_simplifier_plugin::poly_simplifier_plugin(symbol const & fname, ast_manager & m, decl_kind add, decl_kind mul, decl_kind uminus, decl_kind sub,
decl_kind num):
simplifier_plugin(fname, m),
m_ADD(add),
m_MUL(mul),
m_SUB(sub),
m_UMINUS(uminus),
m_NUM(num),
m_curr_sort(0),
m_curr_sort_zero(0) {
}
expr * poly_simplifier_plugin::mk_add(unsigned num_args, expr * const * args) {
SASSERT(num_args > 0);
#ifdef Z3DEBUG
// check for incorrect use of mk_add
for (unsigned i = 0; i < num_args; i++) {
SASSERT(!is_zero(args[i]));
}
#endif
if (num_args == 1)
return args[0];
else
return m_manager.mk_app(m_fid, m_ADD, num_args, args);
}
expr * poly_simplifier_plugin::mk_mul(unsigned num_args, expr * const * args) {
SASSERT(num_args > 0);
#ifdef Z3DEBUG
// check for incorrect use of mk_mul
set_curr_sort(args[0]);
SASSERT(!is_zero(args[0]));
numeral k;
for (unsigned i = 0; i < num_args; i++) {
SASSERT(!is_numeral(args[i], k) || !k.is_one());
SASSERT(i == 0 || !is_numeral(args[i]));
}
#endif
if (num_args == 1)
return args[0];
else if (num_args == 2)
return m_manager.mk_app(m_fid, m_MUL, args[0], args[1]);
else if (is_numeral(args[0]))
return m_manager.mk_app(m_fid, m_MUL, args[0], m_manager.mk_app(m_fid, m_MUL, num_args - 1, args+1));
else
return m_manager.mk_app(m_fid, m_MUL, num_args, args);
}
expr * poly_simplifier_plugin::mk_mul(numeral const & c, expr * body) {
numeral c_prime, d;
c_prime = norm(c);
if (c_prime.is_zero())
return 0;
if (body == 0)
return mk_numeral(c_prime);
if (c_prime.is_one())
return body;
if (is_numeral(body, d)) {
c_prime = norm(c_prime*d);
if (c_prime.is_zero())
return 0;
return mk_numeral(c_prime);
}
set_curr_sort(body);
expr * args[2] = { mk_numeral(c_prime), body };
return mk_mul(2, args);
}
/**
\brief Traverse args, and copy the non-numeral exprs to result, and accumulate the
value of the numerals in k.
*/
void poly_simplifier_plugin::process_monomial(unsigned num_args, expr * const * args, numeral & k, ptr_buffer<expr> & result) {
rational v;
for (unsigned i = 0; i < num_args; i++) {
expr * arg = args[i];
if (is_numeral(arg, v))
k *= v;
else
result.push_back(arg);
}
}
#ifdef Z3DEBUG
/**
\brief Return true if m is a wellformed monomial.
*/
bool poly_simplifier_plugin::wf_monomial(expr * m) const {
SASSERT(!is_add(m));
if (is_mul(m)) {
app * curr = to_app(m);
expr * pp = 0;
if (is_numeral(curr->get_arg(0)))
pp = curr->get_arg(1);
else
pp = curr;
if (is_mul(pp)) {
for (unsigned i = 0; i < to_app(pp)->get_num_args(); i++) {
expr * arg = to_app(pp)->get_arg(i);
CTRACE("wf_monomial_bug", is_mul(arg),
tout << "m: " << mk_ismt2_pp(m, m_manager) << "\n";
tout << "pp: " << mk_ismt2_pp(pp, m_manager) << "\n";
tout << "arg: " << mk_ismt2_pp(arg, m_manager) << "\n";
tout << "i: " << i << "\n";
);
SASSERT(!is_mul(arg));
SASSERT(!is_numeral(arg));
}
}
}
return true;
}
/**
\brief Return true if m is a wellformed polynomial.
*/
bool poly_simplifier_plugin::wf_polynomial(expr * m) const {
if (is_add(m)) {
for (unsigned i = 0; i < to_app(m)->get_num_args(); i++) {
expr * arg = to_app(m)->get_arg(i);
SASSERT(!is_add(arg));
SASSERT(wf_monomial(arg));
}
}
else if (is_mul(m)) {
SASSERT(wf_monomial(m));
}
return true;
}
#endif
/**
\brief Functor used to sort the elements of a monomial.
Force numeric constants to be in the beginning.
*/
struct monomial_element_lt_proc {
poly_simplifier_plugin & m_plugin;
monomial_element_lt_proc(poly_simplifier_plugin & p):m_plugin(p) {}
bool operator()(expr * m1, expr * m2) const {
SASSERT(!m_plugin.is_numeral(m1) || !m_plugin.is_numeral(m2));
if (m_plugin.is_numeral(m1))
return true;
if (m_plugin.is_numeral(m2))
return false;
return m1->get_id() < m2->get_id();
}
};
/**
\brief Create a monomial (* args).
*/
void poly_simplifier_plugin::mk_monomial(unsigned num_args, expr * * args, expr_ref & result) {
switch(num_args) {
case 0:
result = mk_one();
break;
case 1:
result = args[0];
break;
default:
std::stable_sort(args, args + num_args, monomial_element_lt_proc(*this));
result = mk_mul(num_args, args);
SASSERT(wf_monomial(result));
break;
}
}
/**
\brief Return the body of the monomial. That is, the monomial without a coefficient.
Examples: (* 2 (* x y)) ==> (* x y)
(* x x) ==> (* x x)
x ==> x
10 ==> 10
*/
expr * poly_simplifier_plugin::get_monomial_body(expr * m) {
TRACE("get_monomial_body_bug", tout << mk_pp(m, m_manager) << "\n";);
SASSERT(wf_monomial(m));
if (!is_mul(m))
return m;
if (is_numeral(to_app(m)->get_arg(0)))
return to_app(m)->get_arg(1);
return m;
}
inline bool is_essentially_var(expr * n, family_id fid) {
SASSERT(is_var(n) || is_app(n));
return is_var(n) || to_app(n)->get_family_id() != fid;
}
/**
\brief Hack for ordering monomials.
We want an order << where
- (* c1 m1) << (* c2 m2) when m1->get_id() < m2->get_id(), and c1 and c2 are numerals.
- c << m when c is a numeral, and m is not.
So, this method returns -1 for numerals, and the id of the body of the monomial
*/
int poly_simplifier_plugin::get_monomial_body_order(expr * m) {
if (is_essentially_var(m, m_fid)) {
return m->get_id();
}
else if (is_mul(m)) {
if (is_numeral(to_app(m)->get_arg(0)))
return to_app(m)->get_arg(1)->get_id();
else
return m->get_id();
}
else if (is_numeral(m)) {
return -1;
}
else {
return m->get_id();
}
}
void poly_simplifier_plugin::get_monomial_coeff(expr * m, numeral & result) {
SASSERT(!is_numeral(m));
SASSERT(wf_monomial(m));
if (!is_mul(m))
result = numeral::one();
else if (is_numeral(to_app(m)->get_arg(0), result))
return;
else
result = numeral::one();
}
/**
\brief Return true if n1 and n2 can be written as k1 * t and k2 * t, where k1 and
k2 are numerals, or n1 and n2 are both numerals.
*/
bool poly_simplifier_plugin::eq_monomials_modulo_k(expr * n1, expr * n2) {
bool is_num1 = is_numeral(n1);
bool is_num2 = is_numeral(n2);
if (is_num1 != is_num2)
return false;
if (is_num1 && is_num2)
return true;
return get_monomial_body(n1) == get_monomial_body(n2);
}
/**
\brief Return (k1 + k2) * t (or (k1 - k2) * t when inv = true), where n1 = k1 * t, and n2 = k2 * t
Return false if the monomials cancel each other.
*/
bool poly_simplifier_plugin::merge_monomials(bool inv, expr * n1, expr * n2, expr_ref & result) {
numeral k1;
numeral k2;
bool is_num1 = is_numeral(n1, k1);
bool is_num2 = is_numeral(n2, k2);
SASSERT(is_num1 == is_num2);
if (!is_num1 && !is_num2) {
get_monomial_coeff(n1, k1);
get_monomial_coeff(n2, k2);
SASSERT(eq_monomials_modulo_k(n1, n2));
}
if (inv)
k1 -= k2;
else
k1 += k2;
if (k1.is_zero())
return false;
if (is_num1 && is_num2) {
result = mk_numeral(k1);
}
else {
expr * b = get_monomial_body(n1);
if (k1.is_one())
result = b;
else
result = m_manager.mk_app(m_fid, m_MUL, mk_numeral(k1), b);
}
TRACE("merge_monomials", tout << mk_pp(n1, m_manager) << "\n" << mk_pp(n2, m_manager) << "\n" << mk_pp(result, m_manager) << "\n";);
return true;
}
/**
\brief Return a monomial equivalent to -n.
*/
void poly_simplifier_plugin::inv_monomial(expr * n, expr_ref & result) {
set_curr_sort(n);
SASSERT(wf_monomial(n));
rational v;
SASSERT(n != 0);
TRACE("inv_monomial_bug", tout << "n:\n" << mk_ismt2_pp(n, m_manager) << "\n";);
if (is_numeral(n, v)) {
TRACE("inv_monomial_bug", tout << "is numeral\n";);
v.neg();
result = mk_numeral(v);
}
else {
TRACE("inv_monomial_bug", tout << "is not numeral\n";);
numeral k;
get_monomial_coeff(n, k);
expr * b = get_monomial_body(n);
k.neg();
if (k.is_one())
result = b;
else
result = m_manager.mk_app(m_fid, m_MUL, mk_numeral(k), b);
}
}
/**
\brief Add a monomial n to result.
*/
template<bool Inv>
void poly_simplifier_plugin::add_monomial_core(expr * n, expr_ref_vector & result) {
if (is_zero(n))
return;
if (Inv) {
expr_ref n_prime(m_manager);
inv_monomial(n, n_prime);
result.push_back(n_prime);
}
else {
result.push_back(n);
}
}
void poly_simplifier_plugin::add_monomial(bool inv, expr * n, expr_ref_vector & result) {
if (inv)
add_monomial_core<true>(n, result);
else
add_monomial_core<false>(n, result);
}
/**
\brief Copy the monomials in n to result. The monomials are inverted if inv is true.
Equivalent monomials are merged.
*/
template<bool Inv>
void poly_simplifier_plugin::process_sum_of_monomials_core(expr * n, expr_ref_vector & result) {
SASSERT(wf_polynomial(n));
if (is_add(n)) {
for (unsigned i = 0; i < to_app(n)->get_num_args(); i++)
add_monomial_core<Inv>(to_app(n)->get_arg(i), result);
}
else {
add_monomial_core<Inv>(n, result);
}
}
void poly_simplifier_plugin::process_sum_of_monomials(bool inv, expr * n, expr_ref_vector & result) {
if (inv)
process_sum_of_monomials_core<true>(n, result);
else
process_sum_of_monomials_core<false>(n, result);
}
/**
\brief Copy the (non-numeral) monomials in n to result. The monomials are inverted if inv is true.
Equivalent monomials are merged. The constant (numeral) monomials are accumulated in k.
*/
void poly_simplifier_plugin::process_sum_of_monomials(bool inv, expr * n, expr_ref_vector & result, numeral & k) {
SASSERT(wf_polynomial(n));
numeral val;
if (is_add(n)) {
for (unsigned i = 0; i < to_app(n)->get_num_args(); i++) {
expr * arg = to_app(n)->get_arg(i);
if (is_numeral(arg, val)) {
k += inv ? -val : val;
}
else {
add_monomial(inv, arg, result);
}
}
}
else if (is_numeral(n, val)) {
k += inv ? -val : val;
}
else {
add_monomial(inv, n, result);
}
}
/**
\brief Functor used to sort monomials.
Force numeric constants to be in the beginning of a polynomial.
*/
struct monomial_lt_proc {
poly_simplifier_plugin & m_plugin;
monomial_lt_proc(poly_simplifier_plugin & p):m_plugin(p) {}
bool operator()(expr * m1, expr * m2) const {
return m_plugin.get_monomial_body_order(m1) < m_plugin.get_monomial_body_order(m2);
}
};
void poly_simplifier_plugin::mk_sum_of_monomials_core(unsigned sz, expr ** ms, expr_ref & result) {
switch (sz) {
case 0:
result = mk_zero();
break;
case 1:
result = ms[0];
break;
default:
result = mk_add(sz, ms);
break;
}
}
/**
\brief Return true if m is essentially a variable, or is of the form (* c x),
where c is a numeral and x is essentially a variable.
Store the "variable" in x.
*/
bool poly_simplifier_plugin::is_simple_monomial(expr * m, expr * & x) {
if (is_essentially_var(m, m_fid)) {
x = m;
return true;
}
if (is_app(m) && to_app(m)->get_num_args() == 2) {
expr * arg1 = to_app(m)->get_arg(0);
expr * arg2 = to_app(m)->get_arg(1);
if (is_numeral(arg1) && is_essentially_var(arg2, m_fid)) {
x = arg2;
return true;
}
}
return false;
}
/**
\brief Return true if all monomials are simple, and each "variable" occurs only once.
The method assumes the monomials were sorted using monomial_lt_proc.
*/
bool poly_simplifier_plugin::is_simple_sum_of_monomials(expr_ref_vector & monomials) {
expr * last_var = 0;
expr * curr_var = 0;
unsigned size = monomials.size();
for (unsigned i = 0; i < size; i++) {
expr * m = monomials.get(i);
if (!is_simple_monomial(m, curr_var))
return false;
if (curr_var == last_var)
return false;
last_var = curr_var;
}
return true;
}
/**
\brief Store in result the sum of the given monomials.
*/
void poly_simplifier_plugin::mk_sum_of_monomials(expr_ref_vector & monomials, expr_ref & result) {
switch (monomials.size()) {
case 0:
result = mk_zero();
break;
case 1:
result = monomials.get(0);
break;
default: {
TRACE("mk_sum_sort", tout << "before\n"; for (unsigned i = 0; i < monomials.size(); i++) tout << mk_ll_pp(monomials.get(i), m_manager) << "\n";);
std::stable_sort(monomials.c_ptr(), monomials.c_ptr() + monomials.size(), monomial_lt_proc(*this));
TRACE("mk_sum_sort", tout << "after\n"; for (unsigned i = 0; i < monomials.size(); i++) tout << mk_ll_pp(monomials.get(i), m_manager) << "\n";);
if (is_simple_sum_of_monomials(monomials)) {
mk_sum_of_monomials_core(monomials.size(), monomials.c_ptr(), result);
return;
}
ptr_buffer<expr> new_monomials;
expr * last_body = 0;
numeral last_coeff;
numeral coeff;
unsigned sz = monomials.size();
for (unsigned i = 0; i < sz; i++) {
expr * m = monomials.get(i);
expr * body = 0;
if (!is_numeral(m, coeff)) {
body = get_monomial_body(m);
get_monomial_coeff(m, coeff);
}
if (last_body == body) {
last_coeff += coeff;
continue;
}
expr * new_m = mk_mul(last_coeff, last_body);
if (new_m)
new_monomials.push_back(new_m);
last_body = body;
last_coeff = coeff;
}
expr * new_m = mk_mul(last_coeff, last_body);
if (new_m)
new_monomials.push_back(new_m);
TRACE("mk_sum", for (unsigned i = 0; i < monomials.size(); i++) tout << mk_pp(monomials.get(i), m_manager) << "\n";
tout << "======>\n";
for (unsigned i = 0; i < new_monomials.size(); i++) tout << mk_pp(new_monomials.get(i), m_manager) << "\n";);
mk_sum_of_monomials_core(new_monomials.size(), new_monomials.c_ptr(), result);
break;
} }
}
/**
\brief Auxiliary template for mk_add_core
*/
template<bool Inv>
void poly_simplifier_plugin::mk_add_core_core(unsigned num_args, expr * const * args, expr_ref & result) {
SASSERT(num_args >= 2);
expr_ref_vector monomials(m_manager);
process_sum_of_monomials_core<false>(args[0], monomials);
for (unsigned i = 1; i < num_args; i++) {
process_sum_of_monomials_core<Inv>(args[i], monomials);
}
TRACE("mk_add_core_bug",
for (unsigned i = 0; i < monomials.size(); i++) {
SASSERT(monomials.get(i) != 0);
tout << mk_ismt2_pp(monomials.get(i), m_manager) << "\n";
});
mk_sum_of_monomials(monomials, result);
}
/**
\brief Return a sum of monomials. The method assume that each arg in args is a sum of monomials.
If inv is true, then all but the first argument in args are inverted.
*/
void poly_simplifier_plugin::mk_add_core(bool inv, unsigned num_args, expr * const * args, expr_ref & result) {
TRACE("mk_add_core_bug",
for (unsigned i = 0; i < num_args; i++) {
SASSERT(args[i] != 0);
tout << mk_ismt2_pp(args[i], m_manager) << "\n";
});
switch (num_args) {
case 0:
result = mk_zero();
break;
case 1:
result = args[0];
break;
default:
if (inv)
mk_add_core_core<true>(num_args, args, result);
else
mk_add_core_core<false>(num_args, args, result);
break;
}
}
void poly_simplifier_plugin::mk_add(unsigned num_args, expr * const * args, expr_ref & result) {
SASSERT(num_args > 0);
set_curr_sort(args[0]);
mk_add_core(false, num_args, args, result);
}
void poly_simplifier_plugin::mk_add(expr * arg1, expr * arg2, expr_ref & result) {
expr * args[2] = { arg1, arg2 };
mk_add(2, args, result);
}
void poly_simplifier_plugin::mk_sub(unsigned num_args, expr * const * args, expr_ref & result) {
SASSERT(num_args > 0);
set_curr_sort(args[0]);
mk_add_core(true, num_args, args, result);
}
void poly_simplifier_plugin::mk_sub(expr * arg1, expr * arg2, expr_ref & result) {
expr * args[2] = { arg1, arg2 };
mk_sub(2, args, result);
}
void poly_simplifier_plugin::mk_uminus(expr * arg, expr_ref & result) {
set_curr_sort(arg);
rational v;
if (is_numeral(arg, v)) {
v.neg();
result = mk_numeral(v);
}
else {
expr_ref zero(mk_zero(), m_manager);
mk_sub(zero.get(), arg, result);
}
}
/**
\brief Add monomial n to result, the coeff of n is stored in k.
*/
void poly_simplifier_plugin::append_to_monomial(expr * n, numeral & k, ptr_buffer<expr> & result) {
SASSERT(wf_monomial(n));
rational val;
if (is_numeral(n, val)) {
k *= val;
return;
}
get_monomial_coeff(n, val);
k *= val;
n = get_monomial_body(n);
unsigned hd = result.size();
result.push_back(n);
while (hd < result.size()) {
n = result[hd];
if (is_mul(n)) {
result[hd] = result.back();
result.pop_back();
for (unsigned i = 0; i < to_app(n)->get_num_args(); i++) {
result.push_back(to_app(n)->get_arg(i));
}
}
else if (is_numeral(n, val)) {
k *= val;
result[hd] = result.back();
result.pop_back();
}
else {
++hd;
}
}
}
/**
\brief Return a sum of monomials that is equivalent to (* args[0] ... args[num_args-1]).
This method assumes that each arg[i] is a sum of monomials.
*/
void poly_simplifier_plugin::mk_mul(unsigned num_args, expr * const * args, expr_ref & result) {
if (num_args == 1) {
result = args[0];
return;
}
rational val;
if (num_args == 2 && is_numeral(args[0], val) && is_essentially_var(args[1], m_fid)) {
if (val.is_one())
result = args[1];
else if (val.is_zero())
result = args[0];
else
result = mk_mul(num_args, args);
return;
}
if (num_args == 2 && is_essentially_var(args[0], m_fid) && is_numeral(args[1], val)) {
if (val.is_one())
result = args[0];
else if (val.is_zero())
result = args[1];
else {
expr * inv_args[2] = { args[1], args[0] };
result = mk_mul(2, inv_args);
}
return;
}
TRACE("mk_mul_bug",
for (unsigned i = 0; i < num_args; i++) {
tout << mk_pp(args[i], m_manager) << "\n";
});
set_curr_sort(args[0]);
buffer<unsigned> szs;
buffer<unsigned> it;
vector<ptr_vector<expr> > sums;
for (unsigned i = 0; i < num_args; i ++) {
it.push_back(0);
expr * arg = args[i];
SASSERT(wf_polynomial(arg));
sums.push_back(ptr_vector<expr>());
ptr_vector<expr> & v = sums.back();
if (is_add(arg)) {
v.append(to_app(arg)->get_num_args(), to_app(arg)->get_args());
}
else {
v.push_back(arg);
}
szs.push_back(v.size());
}
expr_ref_vector monomials(m_manager);
do {
rational k(1);
ptr_buffer<expr> m;
for (unsigned i = 0; i < num_args; i++) {
ptr_vector<expr> & v = sums[i];
expr * arg = v[it[i]];
TRACE("mk_mul_bug", tout << "k: " << k << " arg: " << mk_pp(arg, m_manager) << "\n";);
append_to_monomial(arg, k, m);
TRACE("mk_mul_bug", tout << "after k: " << k << "\n";);
}
expr_ref num(m_manager);
if (!k.is_zero() && !k.is_one()) {
num = mk_numeral(k);
m.push_back(num);
// bit-vectors can normalize
// to 1 during
// internalization.
if (is_numeral(num, k) && k.is_one()) {
m.pop_back();
}
}
if (!k.is_zero()) {
expr_ref new_monomial(m_manager);
TRACE("mk_mul_bug",
for (unsigned i = 0; i < m.size(); i++) {
tout << mk_pp(m[i], m_manager) << "\n";
});
mk_monomial(m.size(), m.c_ptr(), new_monomial);
TRACE("mk_mul_bug", tout << "new_monomial:\n" << mk_pp(new_monomial, m_manager) << "\n";);
add_monomial_core<false>(new_monomial, monomials);
}
}
while (product_iterator_next(szs.size(), szs.c_ptr(), it.c_ptr()));
mk_sum_of_monomials(monomials, result);
}
void poly_simplifier_plugin::mk_mul(expr * arg1, expr * arg2, expr_ref & result) {
expr * args[2] = { arg1, arg2 };
mk_mul(2, args, result);
}
bool poly_simplifier_plugin::reduce_distinct(unsigned num_args, expr * const * args, expr_ref & result) {
set_reduce_invoked();
unsigned i = 0;
for (; i < num_args; i++)
if (!is_numeral(args[i]))
break;
if (i == num_args) {
// all arguments are numerals
// check if arguments are different...
ptr_buffer<expr> buffer;
buffer.append(num_args, args);
std::sort(buffer.begin(), buffer.end(), ast_lt_proc());
for (unsigned i = 0; i < num_args; i++) {
if (i > 0 && buffer[i] == buffer[i-1]) {
result = m_manager.mk_false();
return true;
}
}
result = m_manager.mk_true();
return true;
}
return false;
}
bool poly_simplifier_plugin::reduce(func_decl * f, unsigned num_args, rational const * mults, expr * const * args, expr_ref & result) {
set_reduce_invoked();
if (is_decl_of(f, m_fid, m_ADD)) {
SASSERT(num_args > 0);
set_curr_sort(args[0]);
expr_ref_buffer args1(m_manager);
for (unsigned i = 0; i < num_args; ++i) {
expr * arg = args[i];
rational m = norm(mults[i]);
if (m.is_zero()) {
// skip
}
else if (m.is_one()) {
args1.push_back(arg);
}
else {
expr_ref k(m_manager);
k = mk_numeral(m);
expr_ref new_arg(m_manager);
mk_mul(k, args[i], new_arg);
args1.push_back(new_arg);
}
}
if (args1.empty()) {
result = mk_zero();
}
else {
mk_add(args1.size(), args1.c_ptr(), result);
}
return true;
}
else {
return simplifier_plugin::reduce(f, num_args, mults, args, result);
}
}
/**
\brief Return true if n is can be put into the form (+ v t) or (+ (- v) t)
\c inv = true will contain true if (- v) is found, and false otherwise.
*/
bool poly_simplifier_plugin::is_var_plus_ground(expr * n, bool & inv, var * & v, expr_ref & t) {
if (!is_add(n) || is_ground(n))
return false;
ptr_buffer<expr> args;
v = 0;
expr * curr = to_app(n);
bool stop = false;
inv = false;
while (!stop) {
expr * arg;
expr * neg_arg;
if (is_add(curr)) {
arg = to_app(curr)->get_arg(0);
curr = to_app(curr)->get_arg(1);
}
else {
arg = curr;
stop = true;
}
if (is_ground(arg)) {
TRACE("model_checker_bug", tout << "pushing:\n" << mk_pp(arg, m_manager) << "\n";);
args.push_back(arg);
}
else if (is_var(arg)) {
if (v != 0)
return false; // already found variable
v = to_var(arg);
}
else if (is_times_minus_one(arg, neg_arg) && is_var(neg_arg)) {
if (v != 0)
return false; // already found variable
v = to_var(neg_arg);
inv = true;
}
else {
return false; // non ground term.
}
}
if (v == 0)
return false; // did not find variable
SASSERT(!args.empty());
mk_add(args.size(), args.c_ptr(), t);
return true;
}

155
src/ast/simplifier/poly_simplifier_plugin.h
View file

@ -1,155 +0,0 @@
/*++
Copyright (c) 2007 Microsoft Corporation
Module Name:
poly_simplifier_plugin.h
Abstract:
Abstract class for families that have polynomials.
Author:
Leonardo (leonardo) 2008-01-08
--*/
#ifndef POLY_SIMPLIFIER_PLUGIN_H_
#define POLY_SIMPLIFIER_PLUGIN_H_
#include "ast/simplifier/simplifier_plugin.h"
/**
\brief Abstract class that provides simplification functions for polynomials.
*/
class poly_simplifier_plugin : public simplifier_plugin {
protected:
typedef rational numeral;
decl_kind m_ADD;
decl_kind m_MUL;
decl_kind m_SUB;
decl_kind m_UMINUS;
decl_kind m_NUM;
sort * m_curr_sort;
expr * m_curr_sort_zero;
expr * mk_add(unsigned num_args, expr * const * args);
expr * mk_add(expr * arg1, expr * arg2) { expr * args[2] = { arg1, arg2 }; return mk_add(2, args); }
expr * mk_mul(unsigned num_args, expr * const * args);
expr * mk_mul(expr * arg1, expr * arg2) { expr * args[2] = { arg1, arg2 }; return mk_mul(2, args); }
// expr * mk_sub(unsigned num_args, expr * const * args) { return m_manager.mk_app(m_fid, m_SUB, num_args, args); }
expr * mk_uminus(expr * arg) { return m_manager.mk_app(m_fid, m_UMINUS, arg); }
void process_monomial(unsigned num_args, expr * const * args, numeral & k, ptr_buffer<expr> & result);
void mk_monomial(unsigned num_args, expr * * args, expr_ref & result);
bool eq_monomials_modulo_k(expr * n1, expr * n2);
bool merge_monomials(bool inv, expr * n1, expr * n2, expr_ref & result);
template<bool Inv>
void add_monomial_core(expr * n, expr_ref_vector & result);
void add_monomial(bool inv, expr * n, expr_ref_vector & result);
template<bool Inv>
void process_sum_of_monomials_core(expr * n, expr_ref_vector & result);
void process_sum_of_monomials(bool inv, expr * n, expr_ref_vector & result);
void process_sum_of_monomials(bool inv, expr * n, expr_ref_vector & result, numeral & k);
void mk_sum_of_monomials(expr_ref_vector & monomials, expr_ref & result);
template<bool Inv>
void mk_add_core_core(unsigned num_args, expr * const * args, expr_ref & result);
void mk_add_core(bool inv, unsigned num_args, expr * const * args, expr_ref & result);
void append_to_monomial(expr * n, numeral & k, ptr_buffer<expr> & result);
expr * mk_mul(numeral const & c, expr * body);
void mk_sum_of_monomials_core(unsigned sz, expr ** ms, expr_ref & result);
bool is_simple_sum_of_monomials(expr_ref_vector & monomials);
bool is_simple_monomial(expr * m, expr * & x);
public:
poly_simplifier_plugin(symbol const & fname, ast_manager & m, decl_kind add, decl_kind mul, decl_kind uminus, decl_kind sub, decl_kind num);
virtual ~poly_simplifier_plugin() {}
/**
\brief Return true if the given expression is a numeral, and store its value in \c val.
*/
virtual bool is_numeral(expr * n, numeral & val) const = 0;
bool is_numeral(expr * n) const { return is_app_of(n, m_fid, m_NUM); }
bool is_zero(expr * n) const {
SASSERT(m_curr_sort_zero != 0);
SASSERT(m_manager.get_sort(n) == m_manager.get_sort(m_curr_sort_zero));
return n == m_curr_sort_zero;
}
bool is_zero_safe(expr * n) {
set_curr_sort(m_manager.get_sort(n));
return is_zero(n);
}
virtual bool is_minus_one(expr * n) const = 0;
virtual expr * get_zero(sort * s) const = 0;
/**
\brief Return true if n is of the form (* -1 r)
*/
bool is_times_minus_one(expr * n, expr * & r) const {
if (is_mul(n) && to_app(n)->get_num_args() == 2 && is_minus_one(to_app(n)->get_arg(0))) {
r = to_app(n)->get_arg(1);
return true;
}
return false;
}
/**
\brief Return true if n is of the form: a <= b or a >= b.
*/
virtual bool is_le_ge(expr * n) const = 0;
/**
\brief Return a constant representing the giving numeral and sort m_curr_sort.
*/
virtual app * mk_numeral(numeral const & n) = 0;
app * mk_zero() { return mk_numeral(numeral::zero()); }
app * mk_one() { return mk_numeral(numeral::one()); }
app * mk_minus_one() { return mk_numeral(numeral::minus_one()); }
/**
\brief Normalize the given numeral with respect to m_curr_sort
*/
virtual numeral norm(numeral const & n) = 0;
void set_curr_sort(sort * s) {
if (s != m_curr_sort) {
// avoid virtual function call
m_curr_sort = s;
m_curr_sort_zero = get_zero(m_curr_sort);
}
}
void set_curr_sort(expr * n) { set_curr_sort(m_manager.get_sort(n)); }
bool is_add(expr const * n) const { return is_app_of(n, m_fid, m_ADD); }
bool is_mul(expr const * n) const { return is_app_of(n, m_fid, m_MUL); }
void mk_add(unsigned num_args, expr * const * args, expr_ref & result);
void mk_add(expr * arg1, expr * arg2, expr_ref & result);
void mk_sub(unsigned num_args, expr * const * args, expr_ref & result);
void mk_sub(expr * arg1, expr * arg2, expr_ref & result);
void mk_uminus(expr * arg, expr_ref & result);
void mk_mul(unsigned num_args, expr * const * args, expr_ref & result);
void mk_mul(expr * arg1, expr * arg2, expr_ref & result);
virtual bool reduce_distinct(unsigned num_args, expr * const * args, expr_ref & result);
virtual bool reduce(func_decl * f, unsigned num_args, rational const * mults, expr * const * args, expr_ref & result);
virtual bool reduce(func_decl * f, unsigned num_args, expr * const * args, expr_ref & result) {
return simplifier_plugin::reduce(f, num_args, args, result);
}
expr * get_monomial_body(expr * m);
int get_monomial_body_order(expr * m);
void get_monomial_coeff(expr * m, numeral & result);
void inv_monomial(expr * n, expr_ref & result);
bool is_var_plus_ground(expr * n, bool & inv, var * & v, expr_ref & t);
#ifdef Z3DEBUG
bool wf_monomial(expr * m) const;
bool wf_polynomial(expr * m) const;
#endif
};
#endif /* POLY_SIMPLIFIER_PLUGIN_H_ */

39
src/ast/simplifier/seq_simplifier_plugin.cpp
View file

@ -1,39 +0,0 @@
/*++
Copyright (c) 2016 Microsoft Corporation
Module Name:
seq_simplifier_plugin.cpp
Abstract:
Simplifier for the theory of sequences
Author:
Nikolaj Bjorner (nbjorner) 2016-02-05
--*/
#include "ast/simplifier/seq_simplifier_plugin.h"
seq_simplifier_plugin::seq_simplifier_plugin(ast_manager & m, basic_simplifier_plugin & b) :
simplifier_plugin(symbol("seq"), m),
m_util(m),
m_rw(m) {}
seq_simplifier_plugin::~seq_simplifier_plugin() {}
bool seq_simplifier_plugin::reduce(func_decl * f, unsigned num_args, expr * const * args, expr_ref & result) {
set_reduce_invoked();
SASSERT(f->get_family_id() == get_family_id());
return m_rw.mk_app_core(f, num_args, args, result) != BR_FAILED;
}
bool seq_simplifier_plugin::reduce_eq(expr * lhs, expr * rhs, expr_ref & result) {
set_reduce_invoked();
return m_rw.mk_eq_core(lhs, rhs, result) != BR_FAILED;
}

39
src/ast/simplifier/seq_simplifier_plugin.h
View file

@ -1,39 +0,0 @@
/*++
Copyright (c) 2016 Microsoft Corporation
Module Name:
seq_simplifier_plugin.h
Abstract:
Simplifier for the sequence theory
Author:
Nikolaj Bjorner (nbjorner) 2016-02-05
--*/
#ifndef SEQ_SIMPLIFIER_PLUGIN_H_
#define SEQ_SIMPLIFIER_PLUGIN_H_
#include "ast/simplifier/basic_simplifier_plugin.h"
#include "ast/seq_decl_plugin.h"
#include "ast/rewriter/seq_rewriter.h"
class seq_simplifier_plugin : public simplifier_plugin {
seq_util m_util;
seq_rewriter m_rw;
public:
seq_simplifier_plugin(ast_manager & m, basic_simplifier_plugin & b);
~seq_simplifier_plugin();
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);
};
#endif /* SEQ_SIMPLIFIER_PLUGIN_H_ */

962
src/ast/simplifier/simplifier.cpp
View file

@ -1,962 +0,0 @@
/*++
Copyright (c) 2007 Microsoft Corporation
Module Name:
simplifier.cpp
Abstract:
Expression simplifier.
Author:
Leonardo (leonardo) 2008-01-03
Notes:
--*/
#include "ast/simplifier/simplifier.h"
#include "ast/rewriter/var_subst.h"
#include "ast/ast_ll_pp.h"
#include "ast/ast_pp.h"
#include "ast/well_sorted.h"
#include "ast/ast_smt_pp.h"
simplifier::simplifier(ast_manager & m):
base_simplifier(m),
m_proofs(m),
m_subst_proofs(m),
m_need_reset(false),
m_use_oeq(false),
m_visited_quantifier(false),
m_ac_support(true) {
}
void simplifier::register_plugin(plugin * p) {
m_plugins.register_plugin(p);
}
simplifier::~simplifier() {
flush_cache();
}
void simplifier::enable_ac_support(bool flag) {
m_ac_support = flag;
ptr_vector<plugin>::const_iterator it = m_plugins.begin();
ptr_vector<plugin>::const_iterator end = m_plugins.end();
for (; it != end; ++it) {
if (*it != 0)
(*it)->enable_ac_support(flag);
}
}
/**
\brief External interface for the simplifier.
A client will invoke operator()(s, r, p) to simplify s.
The result is stored in r.
When proof generation is enabled, a proof for the equivalence (or equisatisfiability)
of s and r is stored in p.
When proof generation is disabled, this method stores the "undefined proof" object in p.
*/
void simplifier::operator()(expr * s, expr_ref & r, proof_ref & p) {
m_need_reset = true;
reinitialize();
expr * s_orig = s;
(void)s_orig;
expr * old_s;
expr * result;
proof * result_proof;
switch (m.proof_mode()) {
case PGM_DISABLED: // proof generation is disabled.
reduce_core(s);
// after executing reduce_core, the result of the simplification is in the cache
get_cached(s, result, result_proof);
r = result;
p = m.mk_undef_proof();
break;
case PGM_COARSE: // coarse proofs... in this case, we do not produce a step by step (fine grain) proof to show the equivalence (or equisatisfiability) of s an r.
m_subst_proofs.reset(); // m_subst_proofs is an auxiliary vector that is used to justify substitutions. See comment on method get_subst.
reduce_core(s);
get_cached(s, result, result_proof);
r = result;
if (result == s)
p = m.mk_reflexivity(s);
else {
remove_duplicates(m_subst_proofs);
p = m.mk_rewrite_star(s, result, m_subst_proofs.size(), m_subst_proofs.c_ptr());
}
break;
case PGM_FINE: // fine grain proofs... in this mode, every proof step (or most of them) is described.
m_proofs.reset();
old_s = 0;
// keep simplyfing until no further simplifications are possible.
while (s != old_s) {
TRACE("simplifier", tout << "simplification pass... " << s->get_id() << "\n";);
TRACE("simplifier_loop", tout << mk_ll_pp(s, m) << "\n";);
reduce_core(s);
get_cached(s, result, result_proof);
SASSERT(is_rewrite_proof(s, result, result_proof));
if (result_proof != 0) {
m_proofs.push_back(result_proof);
}
old_s = s;
s = result;
}
SASSERT(s != 0);
r = s;
p = m_proofs.empty() ? m.mk_reflexivity(s) : m.mk_transitivity(m_proofs.size(), m_proofs.c_ptr());
SASSERT(is_rewrite_proof(s_orig, r, p));
break;
default:
UNREACHABLE();
}
}
void simplifier::flush_cache() {
m_cache.flush();
ptr_vector<plugin>::const_iterator it = m_plugins.begin();
ptr_vector<plugin>::const_iterator end = m_plugins.end();
for (; it != end; ++it) {
if (*it != 0) {
(*it)->flush_caches();
}
}
}
bool simplifier::get_subst(expr * n, expr_ref & r, proof_ref & p) {
return false;
}
void simplifier::reduce_core(expr * n1) {
if (!is_cached(n1)) {
// We do not assume m_todo is empty... So, we store the current size of the todo-stack.
unsigned sz = m_todo.size();
m_todo.push_back(n1);
while (m_todo.size() != sz) {
expr * n = m_todo.back();
if (is_cached(n))
m_todo.pop_back();
else if (visit_children(n)) {
// if all children were already simplified, then remove n from the todo stack and apply a
// simplification step to it.
m_todo.pop_back();
reduce1(n);
}
if (m.canceled()) {
cache_result(n1, n1, 0);
break;
}
}
}
}
/**
\brief Return true if all children of n have been already simplified.
*/
bool simplifier::visit_children(expr * n) {
switch(n->get_kind()) {
case AST_VAR:
return true;
case AST_APP:
// The simplifier has support for flattening AC (associative-commutative) operators.
// The method ast_manager::mk_app is used to create the flat version of an AC operator.
// In Z3 1.x, we used multi-ary operators. This creates problems for the superposition engine.
// So, starting at Z3 2.x, only boolean operators can be multi-ary.
// Example:
// (and (and a b) (and c d)) --> (and a b c d)
// (+ (+ a b) (+ c d)) --> (+ a (+ b (+ c d)))
// Remark: The flattening is only applied if m_ac_support is true.
if (m_ac_support && to_app(n)->get_decl()->is_associative() && to_app(n)->get_decl()->is_commutative())
return visit_ac(to_app(n));
else {
bool visited = true;
unsigned j = to_app(n)->get_num_args();
while (j > 0) {
--j;
visit(to_app(n)->get_arg(j), visited);
}
return visited;
}
case AST_QUANTIFIER:
return visit_quantifier(to_quantifier(n));
default:
UNREACHABLE();
return true;
}
}
/**
\brief Visit the children of n assuming it is an AC (associative-commutative) operator.
For example, if n is of the form (+ (+ a b) (+ c d)), this method
will return true if the nodes a, b, c and d have been already simplified.
The nodes (+ a b) and (+ c d) are not really checked.
*/
bool simplifier::visit_ac(app * n) {
bool visited = true;
func_decl * decl = n->get_decl();
SASSERT(m_ac_support);
SASSERT(decl->is_associative());
SASSERT(decl->is_commutative());
m_ac_marked.reset();
ptr_buffer<app> todo;
todo.push_back(n);
while (!todo.empty()) {
app * n = todo.back();
todo.pop_back();
if (m_ac_mark.is_marked(n))
continue;
m_ac_mark.mark(n, true);
m_ac_marked.push_back(n);
SASSERT(n->get_decl() == decl);
unsigned i = n->get_num_args();
while (i > 0) {
--i;
expr * arg = n->get_arg(i);
if (is_app_of(arg, decl))
todo.push_back(to_app(arg));
else
visit(arg, visited);
}
}
ptr_vector<expr>::const_iterator it = m_ac_marked.begin();
ptr_vector<expr>::const_iterator end = m_ac_marked.end();
for (; it != end; ++it)
m_ac_mark.mark(*it, false);
return visited;
}
bool simplifier::visit_quantifier(quantifier * n) {
m_visited_quantifier = true;
bool visited = true;
unsigned j = to_quantifier(n)->get_num_patterns();
while (j > 0) {
--j;
visit(to_quantifier(n)->get_pattern(j), visited);
}
j = to_quantifier(n)->get_num_no_patterns();
while (j > 0) {
--j;
visit(to_quantifier(n)->get_no_pattern(j), visited);
}
visit(to_quantifier(n)->get_expr(), visited);
return visited;
}
/**
\brief Simplify n and store the result in the cache.
*/
void simplifier::reduce1(expr * n) {
switch (n->get_kind()) {
case AST_VAR:
cache_result(n, n, 0);
break;
case AST_APP:
reduce1_app(to_app(n));
break;
case AST_QUANTIFIER:
reduce1_quantifier(to_quantifier(n));
break;
default:
UNREACHABLE();
}
}
/**
\brief Simplify the given application using the cached values,
associativity flattening, the given substitution, and family/theory
specific simplifications via plugins.
*/
void simplifier::reduce1_app(app * n) {
expr_ref r(m);
proof_ref p(m);
TRACE("reduce", tout << "reducing...\n" << mk_pp(n, m) << "\n";);
if (get_subst(n, r, p)) {
TRACE("reduce", tout << "applying substitution...\n";);
cache_result(n, r, p);
return;
}
func_decl * decl = n->get_decl();
if (m_ac_support && decl->is_associative() && decl->is_commutative())
reduce1_ac_app_core(n);
else
reduce1_app_core(n);
}
void simplifier::reduce1_app_core(app * n) {
m_args.reset();
func_decl * decl = n->get_decl();
proof_ref p1(m);
// Stores the new arguments of n in m_args.
// Let n be of the form
// (decl arg_0 ... arg_{n-1})
// then
// m_args contains [arg_0', ..., arg_{n-1}'],
// where arg_i' is the simplification of arg_i
// and
// p1 is a proof for
// (decl arg_0 ... arg_{n-1}) is equivalente/equisatisfiable to (decl arg_0' ... arg_{n-1}')
// p1 is built using the congruence proof step and the proofs for arg_0' ... arg_{n-1}'.
// Of course, p1 is 0 if proofs are not enabled or coarse grain proofs are used.
bool has_new_args = get_args(n, m_args, p1);
// The following if implements a simple trick.
// If none of the arguments have been simplified, and n is not a theory symbol,
// Then no simplification is possible, and we can cache the result of the simplification of n as n.
if (has_new_args || decl->get_family_id() != null_family_id) {
expr_ref r(m);
TRACE("reduce", tout << "reduce1_app\n"; for(unsigned i = 0; i < m_args.size(); i++) tout << mk_ll_pp(m_args[i], m););
// the method mk_app invokes get_subst and plugins to simplify
// (decl arg_0' ... arg_{n-1}')
mk_app(decl, m_args.size(), m_args.c_ptr(), r);
if (!m.fine_grain_proofs()) {
cache_result(n, r, 0);
}
else {
expr * s = m.mk_app(decl, m_args.size(), m_args.c_ptr());
proof * p;
if (n == r)
p = 0;
else if (r != s)
// we use a "theory rewrite generic proof" to justify the step
// s = (decl arg_0' ... arg_{n-1}') --> r
p = m.mk_transitivity(p1, m.mk_rewrite(s, r));
else
p = p1;
cache_result(n, r, p);
}
}
else {
cache_result(n, n, 0);
}
}
bool is_ac_list(app * n, ptr_vector<expr> & args) {
args.reset();
func_decl * f = n->get_decl();
app * curr = n;
while (true) {
if (curr->get_num_args() != 2)
return false;
expr * arg1 = curr->get_arg(0);
if (is_app_of(arg1, f))
return false;
args.push_back(arg1);
expr * arg2 = curr->get_arg(1);
if (!is_app_of(arg2, f)) {
args.push_back(arg2);
return true;
}
curr = to_app(arg2);
}
}
bool is_ac_vector(app * n) {
func_decl * f = n->get_decl();
unsigned num_args = n->get_num_args();
for (unsigned i = 0; i < num_args; i++) {
if (is_app_of(n->get_arg(i), f))
return false;
}
return true;
}
void simplifier::reduce1_ac_app_core(app * n) {
app_ref n_c(m);
proof_ref p1(m);
mk_ac_congruent_term(n, n_c, p1);
TRACE("ac", tout << "expr:\n" << mk_pp(n, m) << "\ncongruent term:\n" << mk_pp(n_c, m) << "\n";);
expr_ref r(m);
func_decl * decl = n->get_decl();
family_id fid = decl->get_family_id();
plugin * p = get_plugin(fid);
if (is_ac_vector(n_c)) {
if (p != 0 && p->reduce(decl, n_c->get_num_args(), n_c->get_args(), r)) {
// done...
}
else {
r = n_c;
}
}
else if (is_ac_list(n_c, m_args)) {
// m_args contains the arguments...
if (p != 0 && p->reduce(decl, m_args.size(), m_args.c_ptr(), r)) {
// done...
}
else {
r = m.mk_app(decl, m_args.size(), m_args.c_ptr());
}
}
else {
m_args.reset();
m_mults.reset();
get_ac_args(n_c, m_args, m_mults);
TRACE("ac", tout << "AC args:\n";
for (unsigned i = 0; i < m_args.size(); i++) {
tout << mk_pp(m_args[i], m) << " * " << m_mults[i] << "\n";
});
if (p != 0 && p->reduce(decl, m_args.size(), m_mults.c_ptr(), m_args.c_ptr(), r)) {
// done...
}
else {
ptr_buffer<expr> new_args;
expand_args(m_args.size(), m_mults.c_ptr(), m_args.c_ptr(), new_args);
r = m.mk_app(decl, new_args.size(), new_args.c_ptr());
}
}
TRACE("ac", tout << "AC result:\n" << mk_pp(r, m) << "\n";);
if (!m.fine_grain_proofs()) {
cache_result(n, r, 0);
}
else {
proof * p;
if (n == r.get())
p = 0;
else if (r.get() != n_c.get())
p = m.mk_transitivity(p1, m.mk_rewrite(n_c, r));
else
p = p1;
cache_result(n, r, p);
}
}
static unsigned g_rewrite_lemma_id = 0;
void simplifier::dump_rewrite_lemma(func_decl * decl, unsigned num_args, expr * const * args, expr* result) {
expr_ref arg(m);
arg = m.mk_app(decl, num_args, args);
if (arg.get() != result) {
char buffer[128];
#ifdef _WINDOWS
sprintf_s(buffer, ARRAYSIZE(buffer), "lemma_%d.smt", g_rewrite_lemma_id);
#else
sprintf(buffer, "rewrite_lemma_%d.smt", g_rewrite_lemma_id);
#endif
ast_smt_pp pp(m);
pp.set_benchmark_name("rewrite_lemma");
pp.set_status("unsat");
expr_ref n(m);
n = m.mk_not(m.mk_eq(arg.get(), result));
std::ofstream out(buffer);
pp.display(out, n);
out.close();
++g_rewrite_lemma_id;
}
}
/**
\brief Return in \c result an expression \c e equivalent to <tt>(f args[0] ... args[num_args - 1])</tt>, and
store in \c pr a proof for <tt>(= (f args[0] ... args[num_args - 1]) e)</tt>
If e is identical to (f args[0] ... args[num_args - 1]), then pr is set to 0.
*/
void simplifier::mk_app(func_decl * decl, unsigned num_args, expr * const * args, expr_ref & result) {
m_need_reset = true;
if (m.is_eq(decl)) {
sort * s = m.get_sort(args[0]);
plugin * p = get_plugin(s->get_family_id());
if (p != 0 && p->reduce_eq(args[0], args[1], result))
return;
}
else if (m.is_distinct(decl)) {
sort * s = m.get_sort(args[0]);
plugin * p = get_plugin(s->get_family_id());
if (p != 0 && p->reduce_distinct(num_args, args, result))
return;
}
family_id fid = decl->get_family_id();
plugin * p = get_plugin(fid);
if (p != 0 && p->reduce(decl, num_args, args, result)) {
//uncomment this line if you want to trace rewrites as lemmas:
//dump_rewrite_lemma(decl, num_args, args, result.get());
return;
}
result = m.mk_app(decl, num_args, args);
}
/**
\brief Create a term congruence to n (f a[0] ... a[num_args-1]) using the
cached values for the a[i]'s. Store the result in r, and the proof for (= n r) in p.
If n and r are identical, then set p to 0.
*/
void simplifier::mk_congruent_term(app * n, app_ref & r, proof_ref & p) {
bool has_new_args = false;
ptr_vector<expr> args;
ptr_vector<proof> proofs;
unsigned num = n->get_num_args();
for (unsigned j = 0; j < num; j++) {
expr * arg = n->get_arg(j);
expr * new_arg;
proof * arg_proof;
get_cached(arg, new_arg, arg_proof);
CTRACE("simplifier_bug", (arg != new_arg) != (arg_proof != 0),
tout << mk_ll_pp(arg, m) << "\n---->\n" << mk_ll_pp(new_arg, m) << "\n";
tout << "#" << arg->get_id() << " #" << new_arg->get_id() << "\n";
tout << arg << " " << new_arg << "\n";);
if (arg != new_arg) {
has_new_args = true;
proofs.push_back(arg_proof);
SASSERT(arg_proof);
}
else {
SASSERT(arg_proof == 0);
}
args.push_back(new_arg);
}
if (has_new_args) {
r = m.mk_app(n->get_decl(), args.size(), args.c_ptr());
if (m_use_oeq)
p = m.mk_oeq_congruence(n, r, proofs.size(), proofs.c_ptr());
else
p = m.mk_congruence(n, r, proofs.size(), proofs.c_ptr());
}
else {
r = n;
p = 0;
}
}
/**
\brief Store the new arguments of \c n in result. Store in p a proof for
(= n (f result[0] ... result[num_args - 1])), where f is the function symbol of n.
If there are no new arguments or fine grain proofs are disabled, then p is set to 0.
Return true there are new arguments.
*/
bool simplifier::get_args(app * n, ptr_vector<expr> & result, proof_ref & p) {
bool has_new_args = false;
unsigned num = n->get_num_args();
if (m.fine_grain_proofs()) {
app_ref r(m);
mk_congruent_term(n, r, p);
result.append(r->get_num_args(), r->get_args());
SASSERT(n->get_num_args() == result.size());
has_new_args = r != n;
}
else {
p = 0;
for (unsigned j = 0; j < num; j++) {
expr * arg = n->get_arg(j);
expr * new_arg;
proof * arg_proof;
get_cached(arg, new_arg, arg_proof);
if (arg != new_arg) {
has_new_args = true;
}
result.push_back(new_arg);
}
}
return has_new_args;
}
/**
\brief Create a term congruence to n (where n is an expression such as: (f (f a_1 a_2) (f a_3 (f a_4 a_5))) using the
cached values for the a_i's. Store the result in r, and the proof for (= n r) in p.
If n and r are identical, then set p to 0.
*/
void simplifier::mk_ac_congruent_term(app * n, app_ref & r, proof_ref & p) {
SASSERT(m_ac_support);
func_decl * f = n->get_decl();
m_ac_cache.reset();
m_ac_pr_cache.reset();
ptr_buffer<app> todo;
ptr_buffer<expr> new_args;
ptr_buffer<proof> new_arg_prs;
todo.push_back(n);
while (!todo.empty()) {
app * curr = todo.back();
if (m_ac_cache.contains(curr)) {
todo.pop_back();
continue;
}
bool visited = true;
bool has_new_arg = false;
new_args.reset();
new_arg_prs.reset();
unsigned num_args = curr->get_num_args();
for (unsigned j = 0; j < num_args; j ++) {
expr * arg = curr->get_arg(j);
if (is_app_of(arg, f)) {
app * new_arg = 0;
if (m_ac_cache.find(to_app(arg), new_arg)) {
SASSERT(new_arg != 0);
new_args.push_back(new_arg);
if (arg != new_arg)
has_new_arg = true;
if (m.fine_grain_proofs()) {
proof * pr = 0;
m_ac_pr_cache.find(to_app(arg), pr);
if (pr != 0)
new_arg_prs.push_back(pr);
}
}
else {
visited = false;
todo.push_back(to_app(arg));
}
}
else {
expr * new_arg = 0;
proof * pr;
get_cached(arg, new_arg, pr);
new_args.push_back(new_arg);
if (arg != new_arg)
has_new_arg = true;
if (m.fine_grain_proofs() && pr != 0)
new_arg_prs.push_back(pr);
}
}
if (visited) {
SASSERT(new_args.size() == curr->get_num_args());
todo.pop_back();
if (!has_new_arg) {
m_ac_cache.insert(curr, curr);
if (m.fine_grain_proofs())
m_ac_pr_cache.insert(curr, 0);
}
else {
app * new_curr = m.mk_app(f, new_args.size(), new_args.c_ptr());
m_ac_cache.insert(curr, new_curr);
if (m.fine_grain_proofs()) {
proof * p = m.mk_congruence(curr, new_curr, new_arg_prs.size(), new_arg_prs.c_ptr());
m_ac_pr_cache.insert(curr, p);
}
}
}
}
SASSERT(m_ac_cache.contains(n));
app * new_n = 0;
m_ac_cache.find(n, new_n);
r = new_n;
if (m.fine_grain_proofs()) {
proof * new_pr = 0;
m_ac_pr_cache.find(n, new_pr);
p = new_pr;
}
}
#define White 0
#define Grey 1
#define Black 2
#ifdef Z3DEBUG
static int get_color(obj_map<expr, int> & colors, expr * n) {
obj_map<expr, int>::obj_map_entry * entry = colors.insert_if_not_there2(n, White);
return entry->get_data().m_value;
}
#endif
static bool visit_ac_children(func_decl * f, expr * n, obj_map<expr, int> & colors, ptr_buffer<expr> & todo, ptr_buffer<expr> & result) {
if (is_app_of(n, f)) {
unsigned num_args = to_app(n)->get_num_args();
bool visited = true;
// Put the arguments in 'result' in reverse order.
// Reason: preserve the original order of the arguments in the final result.
// Remark: get_ac_args will traverse 'result' backwards.
for (unsigned i = 0; i < num_args; i++) {
expr * arg = to_app(n)->get_arg(i);
obj_map<expr, int>::obj_map_entry * entry = colors.insert_if_not_there2(arg, White);
if (entry->get_data().m_value == White) {
todo.push_back(arg);
visited = false;
}
}
return visited;
}
else {
return true;
}
}
void simplifier::ac_top_sort(app * n, ptr_buffer<expr> & result) {
ptr_buffer<expr> todo;
func_decl * f = n->get_decl();
obj_map<expr, int> & colors = m_colors;
colors.reset();
todo.push_back(n);
while (!todo.empty()) {
expr * curr = todo.back();
int color;
obj_map<expr, int>::obj_map_entry * entry = colors.insert_if_not_there2(curr, White);
SASSERT(entry);
color = entry->get_data().m_value;
switch (color) {
case White:
// Remark: entry becomes invalid if an element is inserted into the hashtable.
// So, I must set Grey before executing visit_ac_children.
entry->get_data().m_value = Grey;
SASSERT(get_color(colors, curr) == Grey);
if (visit_ac_children(f, curr, colors, todo, result)) {
// If visit_ac_children succeeded, then the hashtable was not modified,
// and entry is still valid.
SASSERT(todo.back() == curr);
entry->get_data().m_value = Black;
SASSERT(get_color(colors, curr) == Black);
result.push_back(curr);
todo.pop_back();
}
break;
case Grey:
SASSERT(visit_ac_children(f, curr, colors, todo, result));
SASSERT(entry);
entry->get_data().m_value = Black;
SASSERT(get_color(colors, curr) == Black);
result.push_back(curr);
SASSERT(todo.back() == curr);
todo.pop_back();
break;
case Black:
todo.pop_back();
break;
default:
UNREACHABLE();
}
}
}
void simplifier::get_ac_args(app * n, ptr_vector<expr> & args, vector<rational> & mults) {
SASSERT(m_ac_support);
ptr_buffer<expr> sorted_exprs;
ac_top_sort(n, sorted_exprs);
SASSERT(!sorted_exprs.empty());
SASSERT(sorted_exprs[sorted_exprs.size()-1] == n);
TRACE("ac", tout << mk_ll_pp(n, m, true, false) << "#" << n->get_id() << "\nsorted expressions...\n";
for (unsigned i = 0; i < sorted_exprs.size(); i++) {
tout << "#" << sorted_exprs[i]->get_id() << " ";
}
tout << "\n";);
m_ac_mults.reset();
m_ac_mults.insert(n, rational(1));
func_decl * decl = n->get_decl();
unsigned j = sorted_exprs.size();
while (j > 0) {
--j;
expr * curr = sorted_exprs[j];
rational mult;
m_ac_mults.find(curr, mult);
SASSERT(!mult.is_zero());
if (is_app_of(curr, decl)) {
unsigned num_args = to_app(curr)->get_num_args();
for (unsigned i = 0; i < num_args; i++) {
expr * arg = to_app(curr)->get_arg(i);
rational zero;
obj_map<expr, rational>::obj_map_entry * entry = m_ac_mults.insert_if_not_there2(arg, zero);
entry->get_data().m_value += mult;
}
}
else {
args.push_back(curr);
mults.push_back(mult);
}
}
}
void simplifier::reduce1_quantifier(quantifier * q) {
expr * new_body;
proof * new_body_pr;
SASSERT(is_well_sorted(m, q));
get_cached(q->get_expr(), new_body, new_body_pr);
quantifier_ref q1(m);
proof * p1 = 0;
if (is_quantifier(new_body) &&
to_quantifier(new_body)->is_forall() == q->is_forall() &&
!to_quantifier(q)->has_patterns() &&
!to_quantifier(new_body)->has_patterns()) {
quantifier * nested_q = to_quantifier(new_body);
ptr_buffer<sort> sorts;
buffer<symbol> names;
sorts.append(q->get_num_decls(), q->get_decl_sorts());
names.append(q->get_num_decls(), q->get_decl_names());
sorts.append(nested_q->get_num_decls(), nested_q->get_decl_sorts());
names.append(nested_q->get_num_decls(), nested_q->get_decl_names());
q1 = m.mk_quantifier(q->is_forall(),
sorts.size(),
sorts.c_ptr(),
names.c_ptr(),
nested_q->get_expr(),
std::min(q->get_weight(), nested_q->get_weight()),
q->get_qid(),
q->get_skid(),
0, 0, 0, 0);
SASSERT(is_well_sorted(m, q1));
if (m.fine_grain_proofs()) {
quantifier * q0 = m.update_quantifier(q, new_body);
proof * p0 = q == q0 ? 0 : m.mk_quant_intro(q, q0, new_body_pr);
p1 = m.mk_pull_quant(q0, q1);
p1 = m.mk_transitivity(p0, p1);
}
}
else {
ptr_buffer<expr> new_patterns;
ptr_buffer<expr> new_no_patterns;
expr * new_pattern;
proof * new_pattern_pr;
// Remark: we can ignore the proofs for the patterns.
unsigned num = q->get_num_patterns();
for (unsigned i = 0; i < num; i++) {
get_cached(q->get_pattern(i), new_pattern, new_pattern_pr);
if (m.is_pattern(new_pattern)) {
new_patterns.push_back(new_pattern);
}
}
num = q->get_num_no_patterns();
for (unsigned i = 0; i < num; i++) {
get_cached(q->get_no_pattern(i), new_pattern, new_pattern_pr);
new_no_patterns.push_back(new_pattern);
}
remove_duplicates(new_patterns);
remove_duplicates(new_no_patterns);
q1 = m.mk_quantifier(q->is_forall(),
q->get_num_decls(),
q->get_decl_sorts(),
q->get_decl_names(),
new_body,
q->get_weight(),
q->get_qid(),
q->get_skid(),
new_patterns.size(),
new_patterns.c_ptr(),
new_no_patterns.size(),
new_no_patterns.c_ptr());
SASSERT(is_well_sorted(m, q1));
TRACE("simplifier", tout << mk_pp(q, m) << "\n" << mk_pp(q1, m) << "\n";);
if (m.fine_grain_proofs()) {
if (q != q1 && !new_body_pr) {
new_body_pr = m.mk_rewrite(q->get_expr(), new_body);
}
p1 = q == q1 ? 0 : m.mk_quant_intro(q, q1, new_body_pr);
}
}
expr_ref r(m);
elim_unused_vars(m, q1, params_ref(), r);
proof * pr = 0;
if (m.fine_grain_proofs()) {
proof * p2 = 0;
if (q1.get() != r.get())
p2 = m.mk_elim_unused_vars(q1, r);
pr = m.mk_transitivity(p1, p2);
}
cache_result(q, r, pr);
}
/**
\see release_plugins
*/
void simplifier::borrow_plugins(simplifier const & s) {
ptr_vector<plugin>::const_iterator it = s.begin_plugins();
ptr_vector<plugin>::const_iterator end = s.end_plugins();
for (; it != end; ++it)
register_plugin(*it);
}
/**
\brief Make the simplifier behave as a pre-simplifier: No AC, and plugins are marked in pre-simplification mode.
*/
void simplifier::enable_presimp() {
enable_ac_support(false);
ptr_vector<plugin>::const_iterator it = begin_plugins();
ptr_vector<plugin>::const_iterator end = end_plugins();
for (; it != end; ++it)
(*it)->enable_presimp(true);
}
/**
\brief This method should be invoked if the plugins of this simplifier were borrowed from a different simplifier.
*/
void simplifier::release_plugins() {
m_plugins.release();
}
void subst_simplifier::set_subst_map(expr_map * s) {
flush_cache();
m_subst_map = s;
}
bool subst_simplifier::get_subst(expr * n, expr_ref & r, proof_ref & p) {
if (m_subst_map && m_subst_map->contains(n)) {
expr * _r;
proof * _p = 0;
m_subst_map->get(n, _r, _p);
r = _r;
p = _p;
if (m.coarse_grain_proofs())
m_subst_proofs.push_back(p);
return true;
}
return false;
}
static void push_core(ast_manager & m, expr * e, proof * pr, expr_ref_vector & result, proof_ref_vector & result_prs) {
SASSERT(pr == 0 || m.is_undef_proof(pr) || e == m.get_fact(pr));
TRACE("preprocessor",
tout << mk_pp(e, m) << "\n";
if (pr) tout << mk_ll_pp(pr, m) << "\n\n";);
if (m.is_true(e))
return;
result.push_back(e);
if (m.proofs_enabled())
result_prs.push_back(pr);
}
static void push_and(ast_manager & m, app * e, proof * pr, expr_ref_vector & result, proof_ref_vector & result_prs) {
unsigned num = e->get_num_args();
TRACE("push_and", tout << mk_pp(e, m) << "\n";);
for (unsigned i = 0; i < num; i++)
push_assertion(m, e->get_arg(i), m.mk_and_elim(pr, i), result, result_prs);
}
static void push_not_or(ast_manager & m, app * e, proof * pr, expr_ref_vector & result, proof_ref_vector & result_prs) {
unsigned num = e->get_num_args();
TRACE("push_not_or", tout << mk_pp(e, m) << "\n";);
for (unsigned i = 0; i < num; i++) {
expr * child = e->get_arg(i);
if (m.is_not(child)) {
expr * not_child = to_app(child)->get_arg(0);
push_assertion(m, not_child, m.mk_not_or_elim(pr, i), result, result_prs);
}
else {
expr_ref not_child(m);
not_child = m.mk_not(child);
push_assertion(m, not_child, m.mk_not_or_elim(pr, i), result, result_prs);
}
}
}
void push_assertion(ast_manager & m, expr * e, proof * pr, expr_ref_vector & result, proof_ref_vector & result_prs) {
CTRACE("push_assertion", !(pr == 0 || m.is_undef_proof(pr) || m.get_fact(pr) == e),
tout << mk_pp(e, m) << "\n" << mk_pp(m.get_fact(pr), m) << "\n";);
SASSERT(pr == 0 || m.is_undef_proof(pr) || m.get_fact(pr) == e);
if (m.is_and(e))
push_and(m, to_app(e), pr, result, result_prs);
else if (m.is_not(e) && m.is_or(to_app(e)->get_arg(0)))
push_not_or(m, to_app(to_app(e)->get_arg(0)), pr, result, result_prs);
else
push_core(m, e, pr, result, result_prs);
}

232
src/ast/simplifier/simplifier.h
View file

@ -1,232 +0,0 @@
/*++
Copyright (c) 2007 Microsoft Corporation
Module Name:
simplifier.h
Abstract:
Generic expression simplifier with support for theory specific "plugins".
Author:
Leonardo (leonardo) 2008-01-03
Notes:
--*/
#ifndef SIMPLIFIER_H_
#define SIMPLIFIER_H_
#include "ast/simplifier/base_simplifier.h"
#include "ast/simplifier/simplifier_plugin.h"
#include "util/plugin_manager.h"
#include "ast/ast_util.h"
#include "util/obj_hashtable.h"
/**
\brief Local simplifier.
Proof production can be enabled/disabled.
The simplifier can also apply substitutions during the
simplification. A substitution is a mapping from expression
to expression+proof, where for each entry e_1->(e_2,p) p is
a proof for (= e_1 e_2).
The simplifier can also generate coarse grain proofs. In a coarse
proof, local rewrite steps are omitted, and only the substitutions
used are tracked.
Example:
Consider the expression (+ a b), and the substitution b->(0, p)
When fine grain proofs are enabled, the simplifier will produce the
following proof
Assume the id of the proof object p is $0. Note that p is a proof for (= b 0).
$1: [reflexivity] |- (= a a)
$2: [congruence] $1 $0 |- (= (+ a b) (+ a 0))
$3: [plus-0] |- (= (+ a 0) a)
$4: [transitivity] $2 $3 |- (= (+ a b) a)
When coarse grain proofs are enabled, the simplifier produces the following
proof:
$1: [simplifier] $0 |- (= (+ a b) a)
*/
class simplifier : public base_simplifier {
protected:
typedef simplifier_plugin plugin;
plugin_manager<plugin> m_plugins;
ptr_vector<expr> m_args;
vector<rational> m_mults;
ptr_vector<expr> m_args2;
proof_ref_vector m_proofs; // auxiliary vector for implementing exhaustive simplification.
proof_ref_vector m_subst_proofs; // in coarse grain proof generation mode, this vector tracks the justification for substitutions (see method get_subst).
bool m_need_reset;
bool m_use_oeq;
bool m_visited_quantifier; //!< true, if the simplifier found a quantifier
bool m_ac_support;
expr_mark m_ac_mark;
ptr_vector<expr> m_ac_marked;
obj_map<app, app *> m_ac_cache; // temporary cache for ac
obj_map<app, proof *> m_ac_pr_cache; // temporary cache for ac
obj_map<expr, int> m_colors; // temporary cache for topological sort.
obj_map<expr, rational> m_ac_mults;
/*
Simplifier uses an idiom for rewriting ASTs without using recursive calls.
- It uses a cache (field m_cache in base_simplifier) and a todo-stack (field m_todo in base_simplifier).
- The cache is a mapping from AST to (AST + Proof). An entry [n -> (n',pr)] is used to store the fact
that n and n' are equivalent and pr is a proof for that. If proofs are disabled, then pr is 0.
We say n' is the result of the simplification of n.
Note: Some simplifications do not preserve equivalence, but equisatisfiability.
For saving space, we use pr = 0 also to represent the reflexivity proof [n -> (n, 0)].
- The simplifier can be extended using plugin (subclasses of the class simplifier_plugin).
Each theory has a family ID. All operators (func_decls) and sorts from a given theory have
the same family_id. Given an application (object of the class app), we use the method
get_family_id() to obtain the family id of the operator in this application.
The simplifier uses plugin to apply theory specific simplifications. The basic idea is:
whenever an AST with family_id X is found, invoke the plugin for this family_id.
A simplifier_plugin implements the following API:
1) bool reduce(func_decl * f, unsigned num_args, expr * const * args, expr_ref & result)
This method is invoked when the simplifier is trying to reduce/simplify an application
of the form (f args[0] ... args[num_args - 1]), and f has a family_id associated with
the plugin. The plugin may return false to indicate it could not simplify this application.
If it returns true (success), the result should be stored in the argument result.
2) bool reduce(func_decl * f, unsigned num_args, rational const * mults, expr * const * args, expr_ref & result);
This method is a similar to the previous one, and it is used to handle associative operators.
A plugin does not need to implement this method, the default implementation will use the previous one.
The arguments mults indicates the multiplicity of every argument in args.
For example, suppose this reduce is invoked with the arguments (f, 2, [3, 2], [a, b], result).
This represents the application (f a a a b b).
Some theory simplifiers may have efficient ways to encode this multiplicity. For example,
the arithmetic solver, if f is "+", the multiplicity can be encoded using "*".
This optimization is used because some benchmarks can create term that are very huge when
flattened. One "real" example (that motivated this optimization) is:
let a1 = x1 + x1
let a2 = a1 + a1
...
let an = a{n-1} + a{n-1}
an
In this example, n was 32, so after AC flattening, we had an application
(+ x1 ... x1) with 2^32 arguments. Using the simple reduce would produce a stack overflow.
This class uses a topological sort for computing the multiplicities efficiently.
So, the field m_colors is used to implement the topological sort.
3) bool reduce_eq(expr * lhs, expr * rhs, expr_ref & result)
This method is invoked when the sort of lhs and rhs has a family_id associated with the plugin.
This method allows theory specific simplifications such as:
(= (+ a b) b) --> (= a 0)
Assuming n1 is a reference to (+ a b) and n2 to b, the simplifier would invoke
reduce_eq(n1, n2, result)
Like reduce, false can be returned if a simplification could not be applied.
And if true is returned, then the result is stored in the argument result.
4) bool reduce_distinct(unsigned num_args, expr * const * args, expr_ref & result)
It is similar to reduce_eq, but it used for theory specific simplifications for
(distinct args[0] ... args[num_args-1])
Example:
(distinct 0 1 ... n) --> true
- The idiom used in this class is implemented in the methdo reduce_core.
See reduce_core for more details. The basic idea is:
1) Get the next ast to be simplified from the todo-stack.
2) If it is already cached, then do nothing. That is, this expression was already simplified.
3) Otherwise, check whether all arguments already have been simplified (method visit_children).
3a) The arguments that have not been simplified are added to the todo-stack by visit_children.
In this case visit_children will return false.
3b) If all arguments have already been simplified, then invoke reduce1 to perform a reduction/simplification
step. The cache is updated with the result.
- After invoking reduce_core(n), the cache contains an entry [n -> (n', pr)].
*/
void flush_cache();
/**
\brief This method can be redefined in subclasses of simplifier to implement substitutions.
It returns true if n should be substituted by r, where the substitution is justified by the
proof p. The field m_subst_proofs is used to store these justifications when coarse proofs are used (PGM_COARSE).
This method is redefined in the class subst_simplifier. It is used in asserted_formulas
for implementing constant elimination. For example, if asserted_formulas contains the atoms
(= a (+ b 1)) (p a c), then the constant "a" can be eliminated. This is achieved by set (+ b 1) as
a substitution for "a".
*/
virtual bool get_subst(expr * n, expr_ref & r, proof_ref & p);
void reduce_core(expr * n);
bool visit_children(expr * n);
bool visit_ac(app * n);
virtual bool visit_quantifier(quantifier * q);
void reduce1(expr * n);
void reduce1_app(app * n);
void reduce1_app_core(app * n);
void reduce1_ac_app_core(app * n);
void mk_congruent_term(app * n, app_ref & r, proof_ref & p);
void mk_ac_congruent_term(app * n, app_ref & r, proof_ref & p);
bool get_args(app * n, ptr_vector<expr> & result, proof_ref & p);
void get_ac_args(app * n, ptr_vector<expr> & args, vector<rational> & mults);
virtual void reduce1_quantifier(quantifier * q);
void dump_rewrite_lemma(func_decl * decl, unsigned num_args, expr * const * args, expr* result);
void ac_top_sort(app * n, ptr_buffer<expr> & result);
public:
simplifier(ast_manager & manager);
virtual ~simplifier();
void enable_ac_support(bool flag);
/**
\brief Simplify the expression \c s. Store the result in \c r, and a proof that <tt>(= s r)</tt> in \c p.
*/
void operator()(expr * s, expr_ref & r, proof_ref & p);
void reset() { if (m_need_reset) { flush_cache(); m_need_reset = false; } }
bool visited_quantifier() const { return m_visited_quantifier; }
void mk_app(func_decl * decl, unsigned num_args, expr * const * args, expr_ref & r);
void cache_result(expr * n, expr * r, proof * p) { m_need_reset = true; base_simplifier::cache_result(n, r, p); }
void register_plugin(plugin * p);
ptr_vector<plugin>::const_iterator begin_plugins() const { return m_plugins.begin(); }
ptr_vector<plugin>::const_iterator end_plugins() const { return m_plugins.end(); }
plugin * get_plugin(family_id fid) const { return m_plugins.get_plugin(fid); }
ast_manager & get_manager() { return m; }
void borrow_plugins(simplifier const & s);
void release_plugins();
void enable_presimp();
};
class subst_simplifier : public simplifier {
protected:
expr_map * m_subst_map;
virtual bool get_subst(expr * n, expr_ref & r, proof_ref & p);
public:
subst_simplifier(ast_manager & manager):simplifier(manager), m_subst_map(0) {}
void set_subst_map(expr_map * s);
};
void push_assertion(ast_manager & m, expr * e, proof * pr, expr_ref_vector & result, proof_ref_vector & result_prs);
#endif

46
src/ast/simplifier/simplifier_plugin.cpp
View file

@ -1,46 +0,0 @@
/*++
Copyright (c) 2006 Microsoft Corporation
Module Name:
simplifier_plugin.cpp
Abstract:
<abstract>
Author:
Leonardo de Moura (leonardo) 2008-12-29.
Revision History:
--*/
#include "ast/simplifier/simplifier_plugin.h"
/**
\brief Copy every args[i] mult[i] times to new_args.
*/
void expand_args(unsigned num_args, rational const * mults, expr * const * args, ptr_buffer<expr> & new_args) {
for (unsigned i = 0; i < num_args; i++) {
rational const & c = mults[i];
SASSERT(c.is_int());
rational j(0);
while (j < c) {
new_args.push_back(args[i]);
j++;
}
}
}
bool simplifier_plugin::reduce(func_decl * f, unsigned num_args, rational const * mults, expr * const * args, expr_ref & result) {
set_reduce_invoked();
if (f->is_idempotent()) {
return reduce(f, num_args, args, result);
}
else {
ptr_buffer<expr> new_args;
expand_args(num_args, mults, args, new_args);
return reduce(f, new_args.size(), new_args.c_ptr(), result);
}
}

94
src/ast/simplifier/simplifier_plugin.h
View file

@ -1,94 +0,0 @@
/*++
Copyright (c) 2007 Microsoft Corporation
Module Name:
simplifier_plugin.h
Abstract:
Expression simplifier plugin interface.
Author:
Leonardo (leonardo) 2008-01-03
--*/
#ifndef SIMPLIFIER_PLUGIN_H_
#define SIMPLIFIER_PLUGIN_H_
#include "ast/ast.h"
class simplifier;
void expand_args(unsigned num_args, rational const * mults, expr * const * args, ptr_buffer<expr> & new_args);
/**
\brief Abstract simplifier for the operators in a given family.
*/
class simplifier_plugin {
protected:
ast_manager & m_manager;
family_id m_fid;
bool m_presimp; // true if simplifier is performing pre-simplification...
bool m_reduce_invoked; // true if one of the reduce methods were invoked.
void set_reduce_invoked() { m_reduce_invoked = true; }
public:
simplifier_plugin(symbol const & fname, ast_manager & m):m_manager(m), m_fid(m.mk_family_id(fname)), m_presimp(false), m_reduce_invoked(false) {}
bool reduce_invoked() const { return m_reduce_invoked; }
virtual ~simplifier_plugin() {}
virtual simplifier_plugin * mk_fresh() {
UNREACHABLE();
return 0;
}
/**
\brief Return in \c result an expression \c e equivalent to <tt>(f args[0] ... args[num_args - 1])</tt>.
Return true if succeeded.
*/
virtual bool reduce(func_decl * f, unsigned num_args, expr * const * args, expr_ref & result) { set_reduce_invoked(); return false; }
/**
\brief Return in \c result an expression \c e equivalent to <tt>(f args[0] ... args[0] ... args[num_args - 1])</tt>.
Where each args[i] occurs mults[i] times.
Return true if succeeded.
*/
virtual bool reduce(func_decl * f, unsigned num_args, rational const * mults, expr * const * args, expr_ref & result);
/**
\brief Return in \c result an expression \c e equivalent to <tt>(= lhs rhs)</tt>.
Return true if succeeded.
*/
virtual bool reduce_eq(expr * lhs, expr * rhs, expr_ref & result) { set_reduce_invoked(); return false; }
/**
\brief Return in \c result an expression \c e equivalent to <tt>(distinct args[0] ... args[num_args-1])</tt>.
Return true if succeeded.
*/
virtual bool reduce_distinct(unsigned num_args, expr * const * args, expr_ref & result) { set_reduce_invoked(); return false; }
family_id get_family_id() const { return m_fid; }
/**
\brief Simplifiers may maintain local caches. These caches must be flushed when this method is invoked.
*/
virtual void flush_caches() { /* do nothing */ }
ast_manager & get_manager() { return m_manager; }
void enable_presimp(bool flag) { m_presimp = flag; }
virtual void enable_ac_support(bool flag) {}
};
#endif

27
src/muz/pdr/pdr_util.cpp
View file

@ -22,29 +22,26 @@ Notes:
--*/
#include <sstream>
#include "ast/simplifier/arith_simplifier_plugin.h"
#include "util/util.h"
#include "util/ref_vector.h"
#include "ast/array_decl_plugin.h"
#include "ast/ast_pp.h"
#include "ast/simplifier/basic_simplifier_plugin.h"
#include "ast/simplifier/bv_simplifier_plugin.h"
#include "ast/rewriter/bool_rewriter.h"
#include "muz/base/dl_util.h"
#include "ast/for_each_expr.h"
#include "smt/params/smt_params.h"
#include "model/model.h"
#include "util/ref_vector.h"
#include "ast/rewriter/rewriter.h"
#include "ast/rewriter/rewriter_def.h"
#include "util/util.h"
#include "muz/pdr/pdr_manager.h"
#include "muz/pdr/pdr_util.h"
#include "ast/scoped_proof.h"
#include "ast/arith_decl_plugin.h"
#include "ast/rewriter/expr_replacer.h"
#include "model/model_smt2_pp.h"
#include "ast/rewriter/bool_rewriter.h"
#include "ast/rewriter/poly_rewriter.h"
#include "ast/rewriter/poly_rewriter_def.h"
#include "ast/rewriter/arith_rewriter.h"
#include "ast/scoped_proof.h"
#include "ast/rewriter/rewriter.h"
#include "ast/rewriter/rewriter_def.h"
#include "smt/params/smt_params.h"
#include "model/model.h"
#include "muz/base/dl_util.h"
#include "muz/pdr/pdr_manager.h"
#include "muz/pdr/pdr_util.h"
#include "model/model_smt2_pp.h"

1
src/muz/rel/dl_bound_relation.h
View file

@ -26,7 +26,6 @@ Revision History:
#include "muz/rel/dl_vector_relation.h"
#include "muz/rel/dl_interval_relation.h"
#include "ast/arith_decl_plugin.h"
#include "ast/simplifier/basic_simplifier_plugin.h"
#include "ast/rewriter/bool_rewriter.h"
namespace datalog {

5
src/muz/rel/dl_interval_relation.h
View file

@ -20,13 +20,12 @@ Revision History:
#define DL_INTERVAL_RELATION_H_
#include "ast/arith_decl_plugin.h"
#include "smt/old_interval.h"
#include "muz/base/dl_context.h"
#include "muz/rel/dl_relation_manager.h"
#include "muz/rel/dl_base.h"
#include "smt/old_interval.h"
#include "muz/rel/dl_vector_relation.h"
#include "ast/arith_decl_plugin.h"
#include "ast/simplifier/basic_simplifier_plugin.h"
namespace datalog {

3
src/muz/spacer/spacer_legacy_mbp.cpp
View file

@ -20,9 +20,6 @@ Notes:
#include "ast/array_decl_plugin.h"
#include "ast/ast_pp.h"
#include "ast/simplifier/arith_simplifier_plugin.h"
#include "ast/simplifier/basic_simplifier_plugin.h"
#include "ast/simplifier/bv_simplifier_plugin.h"
#include "ast/rewriter/bool_rewriter.h"
#include "muz/base/dl_util.h"
#include "ast/for_each_expr.h"

1
src/smt/arith_eq_adapter.h
View file

@ -23,7 +23,6 @@ Revision History:
#include "util/obj_pair_hashtable.h"
#include "ast/arith_decl_plugin.h"
#include "util/statistics.h"
#include "ast/simplifier/arith_simplifier_plugin.h"
namespace smt {

1
src/smt/theory_arith.h
View file

@ -34,7 +34,6 @@ Revision History:
#include "util/obj_pair_hashtable.h"
#include "smt/old_interval.h"
#include "math/grobner/grobner.h"
#include "ast/simplifier/arith_simplifier_plugin.h"
#include "smt/arith_eq_solver.h"
#include "smt/theory_opt.h"
#include "util/uint_set.h"

7
src/smt/theory_arith_int.h
View file

@ -19,12 +19,11 @@ Revision History:
#ifndef THEORY_ARITH_INT_H_
#define THEORY_ARITH_INT_H_
#include "ast/ast_ll_pp.h"
#include "ast/simplifier/arith_simplifier_plugin.h"
#include "ast/well_sorted.h"
#include "math/euclid/euclidean_solver.h"
#include "util/numeral_buffer.h"
#include "ast/ast_ll_pp.h"
#include "ast/well_sorted.h"
#include "ast/ast_smt2_pp.h"
#include "math/euclid/euclidean_solver.h"
namespace smt {