mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-26 02:25:32 +00:00
Code Activity

remove simplify dependencies

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2017-08-25 23:56:09 -07:00
parent 9438ff848f
commit ac0bb6a3d0
11 changed files with 108 additions and 45 deletions
Download patch file Download diff file Expand all files Collapse all files

33
src/ast/expr_substitution.h
View file

@ -52,4 +52,37 @@ public:
void cleanup();
};
class scoped_expr_substitution {
expr_substitution& m_subst;
expr_ref_vector m_trail;
unsigned_vector m_trail_lim;
public:
scoped_expr_substitution(expr_substitution& s): m_subst(s), m_trail(s.m()) {}
~scoped_expr_substitution() {}
void insert(expr * s, expr * def, proof * def_pr = 0, expr_dependency * def_dep = 0) {
if (!m_subst.contains(s)) {
m_subst.insert(s, def, def_pr, def_dep);
m_trail.push_back(s);
}
}
void reset() { m_subst.reset(); m_trail.reset(); m_trail_lim.reset(); }
void push() { m_trail_lim.push_back(m_trail.size()); }
void pop(unsigned n) {
if (n > 0) {
unsigned new_sz = m_trail_lim.size() - n;
unsigned old_sz = m_trail_lim[new_sz];
for (unsigned i = old_sz; i < m_trail.size(); ++i) m_subst.erase(m_trail[i].get());
m_trail.resize(old_sz);
m_trail_lim.resize(new_sz);
}
}
bool empty() const { return m_subst.empty(); }
bool find(expr * s, expr * & def, proof * & def_pr) { return m_subst.find(s, def, def_pr); }
bool find(expr * s, expr * & def, proof * & def_pr, expr_dependency * & def_dep) { return m_subst.find(s, def, def_pr, def_dep); }
bool contains(expr * s) { return m_subst.contains(s); }
void cleanup() { m_subst.cleanup(); }
};
#endif

4
src/ast/rewriter/CMakeLists.txt
View file

@ -3,13 +3,16 @@ z3_add_component(rewriter
arith_rewriter.cpp
array_rewriter.cpp
ast_counter.cpp
bit2int.cpp
bool_rewriter.cpp
bv_bounds.cpp
bv_elim2.cpp
bv_rewriter.cpp
datatype_rewriter.cpp
der.cpp
distribute_forall.cpp
dl_rewriter.cpp
elim_bounds2.cpp
enum2bv_rewriter.cpp
expr_replacer.cpp
expr_safe_replace.cpp
@ -17,6 +20,7 @@ z3_add_component(rewriter
fpa_rewriter.cpp
inj_axiom.cpp
label_rewriter.cpp
maximize_ac_sharing.cpp
mk_simplified_app.cpp
pb_rewriter.cpp
pb2bv_rewriter.cpp

55
src/ast/simplifier/bit2int.cpp → src/ast/rewriter/bit2int.cpp
View file

@ -19,15 +19,16 @@ Revision History:
--*/
#include "ast/simplifier/bit2int.h"
#include "ast/ast_pp.h"
#include "ast/ast_ll_pp.h"
#include "ast/for_each_ast.h"
#include "ast/rewriter/bit2int.h"
#define CHECK(_x_) if (!(_x_)) { UNREACHABLE(); }
bit2int::bit2int(ast_manager & m) :
m_manager(m), m_bv_util(m), m_arith_util(m), m_cache(m), m_bit0(m) {
m_manager(m), m_bv_util(m), m_rewriter(m), m_arith_util(m), m_cache(m), m_bit0(m) {
m_bit0 = m_bv_util.mk_numeral(0,1);
}
@ -67,7 +68,7 @@ unsigned bit2int::get_numeral_bits(numeral const& k) {
void bit2int::align_size(expr* e, unsigned sz, expr_ref& result) {
unsigned sz1 = m_bv_util.get_bv_size(e);
SASSERT(sz1 <= sz);
m_bv_simplifier->mk_zeroext(sz-sz1, e, result);
result = m_rewriter.mk_zero_extend(sz-sz1, e);
}
void bit2int::align_sizes(expr_ref& a, expr_ref& b) {
@ -75,11 +76,11 @@ void bit2int::align_sizes(expr_ref& a, expr_ref& b) {
unsigned sz2 = m_bv_util.get_bv_size(b);
expr_ref tmp(m_manager);
if (sz1 > sz2) {
m_bv_simplifier->mk_zeroext(sz1-sz2, b, tmp);
tmp = m_rewriter.mk_zero_extend(sz1-sz2, b);
b = tmp;
}
else if (sz2 > sz1) {
m_bv_simplifier->mk_zeroext(sz2-sz1, a, tmp);
tmp = m_rewriter.mk_zero_extend(sz2-sz1, a);
a = tmp;
}
}
@ -123,11 +124,11 @@ bool bit2int::mk_add(expr* e1, expr* e2, expr_ref& result) {
return true;
}
align_sizes(tmp1, tmp2);
m_bv_simplifier->mk_zeroext(1, tmp1, tmp1);
m_bv_simplifier->mk_zeroext(1, tmp2, tmp2);
tmp1 = m_rewriter.mk_zero_extend(1, tmp1);
tmp2 = m_rewriter.mk_zero_extend(1, tmp2);
SASSERT(m_bv_util.get_bv_size(tmp1) == m_bv_util.get_bv_size(tmp2));
m_bv_simplifier->mk_add(tmp1, tmp2, tmp3);
m_bv_simplifier->mk_bv2int(tmp3, m_arith_util.mk_int(), result);
tmp3 = m_rewriter.mk_bv_add(tmp1, tmp2);
result = m_rewriter.mk_bv2int(tmp3);
return true;
}
return false;
@ -143,14 +144,14 @@ bool bit2int::mk_comp(eq_type ty, expr* e1, expr* e2, expr_ref& result) {
SASSERT(m_bv_util.get_bv_size(tmp1) == m_bv_util.get_bv_size(tmp2));
switch(ty) {
case lt:
m_bv_simplifier->mk_leq_core(false, tmp2, tmp1, tmp3);
tmp3 = m_rewriter.mk_ule(tmp2, tmp1);
result = m_manager.mk_not(tmp3);
break;
case le:
m_bv_simplifier->mk_leq_core(false,tmp1, tmp2, result);
result = m_rewriter.mk_ule(tmp1, tmp2);
break;
case eq:
result = m_manager.mk_eq(tmp1,tmp2);
result = m_manager.mk_eq(tmp1, tmp2);
break;
}
return true;
@ -167,12 +168,12 @@ bool bit2int::mk_mul(expr* e1, expr* e2, expr_ref& result) {
if (extract_bv(e1, sz1, sign1, tmp1) &&
extract_bv(e2, sz2, sign2, tmp2)) {
align_sizes(tmp1, tmp2);
m_bv_simplifier->mk_zeroext(m_bv_util.get_bv_size(tmp1), tmp1, tmp1);
m_bv_simplifier->mk_zeroext(m_bv_util.get_bv_size(tmp2), tmp2, tmp2);
tmp1 = m_rewriter.mk_zero_extend(m_bv_util.get_bv_size(tmp1), tmp1);
tmp2 = m_rewriter.mk_zero_extend(m_bv_util.get_bv_size(tmp2), tmp2);
SASSERT(m_bv_util.get_bv_size(tmp1) == m_bv_util.get_bv_size(tmp2));
m_bv_simplifier->mk_mul(tmp1, tmp2, tmp3);
m_bv_simplifier->mk_bv2int(tmp3, m_arith_util.mk_int(), result);
tmp3 = m_rewriter.mk_bv_mul(tmp1, tmp2);
result = m_rewriter.mk_bv2int(tmp3);
if (sign1 != sign2) {
result = m_arith_util.mk_uminus(result);
}
@ -187,8 +188,7 @@ bool bit2int::is_bv_poly(expr* n, expr_ref& pos, expr_ref& neg) {
numeral k;
bool is_int;
todo.push_back(n);
m_bv_simplifier->mk_bv2int(m_bit0, m_arith_util.mk_int(), pos);
m_bv_simplifier->mk_bv2int(m_bit0, m_arith_util.mk_int(), neg);
neg = pos = m_rewriter.mk_bv2int(m_bit0);
while (!todo.empty()) {
n = todo.back();
@ -372,8 +372,8 @@ void bit2int::visit(app* n) {
tmp1 = tmp_p;
tmp2 = e2bv;
align_sizes(tmp1, tmp2);
m_bv_simplifier->mk_bv_urem(tmp1, tmp2, tmp3);
m_bv_simplifier->mk_bv2int(tmp3, m_arith_util.mk_int(), result);
tmp3 = m_rewriter.mk_bv_urem(tmp1, tmp2);
result = m_rewriter.mk_bv2int(tmp3);
cache_result(n, result);
return;
}
@ -382,25 +382,24 @@ void bit2int::visit(app* n) {
tmp1 = tmp_n;
tmp2 = e2bv;
align_sizes(tmp1, tmp2);
m_bv_simplifier->mk_bv_urem(tmp1, tmp2, tmp3);
tmp3 = m_rewriter.mk_bv_urem(tmp1, tmp2);
// e2 - (neg1 mod e2)
tmp1 = e2bv;
tmp2 = tmp3;
align_sizes(tmp1, tmp2);
m_bv_simplifier->mk_sub(tmp1, tmp2, tmp3);
tmp3 = m_rewriter.mk_bv_sub(tmp1, tmp2);
// pos1 + (e2 - (neg1 mod e2))
tmp1 = tmp_p;
tmp2 = tmp3;
align_sizes(tmp1, tmp2);
m_bv_simplifier->mk_zeroext(1, tmp1, tmp_p);
m_bv_simplifier->mk_zeroext(1, tmp2, tmp_n);
m_bv_simplifier->mk_add(tmp_p, tmp_n, tmp1);
tmp_p = m_rewriter.mk_zero_extend(1, tmp1);
tmp_n = m_rewriter.mk_zero_extend(1, tmp2);
tmp1 = m_rewriter.mk_bv_add(tmp_p, tmp_n);
// (pos1 + (e2 - (neg1 mod e2))) mod e2
tmp2 = e2bv;
align_sizes(tmp1, tmp2);
m_bv_simplifier->mk_bv_urem(tmp1, tmp2, tmp3);
m_bv_simplifier->mk_bv2int(tmp3, m_arith_util.mk_int(), result);
tmp3 = m_rewriter.mk_bv_urem(tmp1, tmp2);
result = m_rewriter.mk_bv2int(tmp3);
cache_result(n, result);
}

7
src/ast/simplifier/bit2int.h → src/ast/rewriter/bit2int.h
View file

@ -22,9 +22,7 @@ Revision History:
#include "ast/bv_decl_plugin.h"
#include "ast/arith_decl_plugin.h"
#include "ast/act_cache.h"
#include "ast/simplifier/basic_simplifier_plugin.h"
#include "ast/simplifier/bv_simplifier_plugin.h"
#include "ast/rewriter/bv_rewriter.h"
class bit2int {
protected:
@ -60,8 +58,8 @@ protected:
typedef act_cache expr_map;
ast_manager & m_manager;
bv_util m_bv_util;
bv_rewriter m_rewriter;
arith_util m_arith_util;
bv_simplifier_plugin * m_bv_simplifier;
expr_map m_cache; // map: ast -> ast ref. counters are incremented when inserted here.
expr_ref m_bit0;
@ -88,7 +86,6 @@ protected:
public:
bit2int(ast_manager & m);
void set_bv_simplifier(bv_simplifier_plugin * p) { m_bv_simplifier = p; }
void operator()(expr * m, expr_ref & result, proof_ref& p);
};

39
src/ast/rewriter/bv_rewriter.h
View file

@ -98,11 +98,10 @@ class bv_rewriter : public poly_rewriter<bv_rewriter_core> {
br_status mk_bv_rotate_right(unsigned n, expr * arg, expr_ref & result);
br_status mk_bv_ext_rotate_left(expr * arg1, expr * arg2, expr_ref & result);
br_status mk_bv_ext_rotate_right(expr * arg1, expr * arg2, expr_ref & result);
br_status mk_bv_add(expr* a, expr* b, expr_ref& result) { expr* args[2] = { a, b }; return mk_bv_add(2, args, result); }
br_status mk_bv_sub(expr* a, expr* b, expr_ref& result) { expr* args[2] = { a, b }; return mk_sub(2, args, result); }
br_status mk_bv_mul(expr* a, expr* b, expr_ref& result) { expr* args[2] = { a, b }; return mk_bv_mul(2, args, result); }
br_status mk_bv_add(unsigned num_args, expr * const * args, expr_ref & result);
br_status mk_bv_add(expr * arg1, expr * arg2, expr_ref & result) {
expr * args[2] = { arg1, arg2 };
return mk_bv_add(2, args, result);
}
br_status mk_bv_mul(unsigned num_args, expr * const * args, expr_ref & result);
br_status mk_bv_shl(expr * arg1, expr * arg2, expr_ref & result);
br_status mk_bv_lshr(expr * arg1, expr * arg2, expr_ref & result);
@ -185,6 +184,38 @@ public:
bool hi_div0() const { return m_hi_div0; }
bv_util & get_util() { return m_util; }
#define MK_BV_BINARY(OP) \
expr_ref OP(expr* a, expr* b) { \
expr_ref result(m()); \
if (BR_FAILED == OP(a, b, result)) \
result = m_util.OP(a, b); \
return result; \
} \
expr_ref mk_zero_extend(unsigned n, expr * arg) {
expr_ref result(m());
if (BR_FAILED == mk_zero_extend(n, arg, result))
result = m_util.mk_zero_extend(n, arg);
return result;
}
MK_BV_BINARY(mk_bv_urem);
MK_BV_BINARY(mk_ule);
MK_BV_BINARY(mk_bv_add);
MK_BV_BINARY(mk_bv_mul);
MK_BV_BINARY(mk_bv_sub);
expr_ref mk_bv2int(expr* a) {
expr_ref result(m());
if (BR_FAILED == mk_bv2int(a, result))
result = m_util.mk_bv2int(a);
return result;
}
};
#endif

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

@ -5,7 +5,6 @@ z3_add_component(simplifier
array_simplifier_params.cpp
array_simplifier_plugin.cpp
basic_simplifier_plugin.cpp
bit2int.cpp
bv_elim.cpp
bv_simplifier_params.cpp
bv_simplifier_plugin.cpp

4
src/smt/asserted_formulas.cpp
View file

@ -33,7 +33,6 @@ Revision History:
#include "ast/simplifier/bv_simplifier_plugin.h"
#include "ast/simplifier/bv_elim.h"
#include "ast/simplifier/elim_bounds.h"
#include "ast/simplifier/bit2int.h"
#include "ast/normal_forms/pull_quant.h"
#include "ast/normal_forms/nnf.h"
#include "ast/pattern/pattern_inference.h"
@ -70,7 +69,6 @@ asserted_formulas::asserted_formulas(ast_manager & m, smt_params & p):
basic_simplifier_plugin * basic_simp = 0;
bv_simplifier_plugin * bv_simp = 0;
setup_simplifier_plugins(m_pre_simplifier, basic_simp, arith_simp, bv_simp);
m_bit2int.set_bv_simplifier(bv_simp);
m_pre_simplifier.enable_presimp();
}
@ -262,7 +260,7 @@ void asserted_formulas::reduce() {
INVOKE(m_params.m_propagate_values, propagate_values());
INVOKE(m_params.m_macro_finder && has_quantifiers(), find_macros());
INVOKE(m_params.m_nnf_cnf || (m_params.m_mbqi && has_quantifiers()), nnf_cnf());
INVOKE(m_params.m_eliminate_and, eliminate_and());
INVOKE(/*m_params.m_eliminate_and*/ true, eliminate_and());
INVOKE(m_params.m_pull_cheap_ite_trees, pull_cheap_ite_trees());
INVOKE(m_params.m_pull_nested_quantifiers && has_quantifiers(), pull_nested_quantifiers());
INVOKE(m_params.m_ng_lift_ite != LI_NONE, ng_lift_ite());

2
src/smt/asserted_formulas.h
View file

@ -24,7 +24,7 @@ Revision History:
#include "ast/simplifier/simplifier.h"
#include "ast/simplifier/basic_simplifier_plugin.h"
#include "ast/simplifier/maximise_ac_sharing.h"
#include "ast/simplifier/bit2int.h"
#include "ast/rewriter/bit2int.h"
#include "ast/macros/macro_manager.h"
#include "ast/macros/macro_finder.h"
#include "ast/normal_forms/defined_names.h"

2
src/smt/elim_term_ite.h
View file

@ -59,6 +59,7 @@ public:
}
virtual ~elim_term_ite_cfg() {}
vector<justified_expr> const& new_defs() const { return m_new_defs; }
void reset() { m_new_defs.reset(); }
br_status reduce_app(func_decl* f, unsigned n, expr *const* args, expr_ref& result, proof_ref& result_pr);
};
@ -70,6 +71,7 @@ public:
m_cfg(m, dn)
{}
vector<justified_expr> const& new_defs() const { return m_cfg.new_defs(); }
void reset() { m_cfg.reset(); }
};

2
src/smt/params/preprocessor_params.cpp
View file

@ -46,7 +46,7 @@ void preprocessor_params::display(std::ostream & out) const {
DISPLAY_PARAM(m_pull_cheap_ite_trees);
DISPLAY_PARAM(m_pull_nested_quantifiers);
DISPLAY_PARAM(m_eliminate_term_ite);
DISPLAY_PARAM(m_eliminate_and);
//DISPLAY_PARAM(m_eliminate_and);
DISPLAY_PARAM(m_macro_finder);
DISPLAY_PARAM(m_propagate_values);
DISPLAY_PARAM(m_propagate_booleans);

4
src/smt/params/preprocessor_params.h
View file

@ -39,7 +39,7 @@ struct preprocessor_params : public pattern_inference_params,
bool m_pull_cheap_ite_trees;
bool m_pull_nested_quantifiers;
bool m_eliminate_term_ite;
bool m_eliminate_and; // represent (and a b) as (not (or (not a) (not b)))
// bool m_eliminate_and; // represent (and a b) as (not (or (not a) (not b)))
bool m_macro_finder;
bool m_propagate_values;
bool m_propagate_booleans;
@ -62,7 +62,7 @@ public:
m_pull_cheap_ite_trees(false),
m_pull_nested_quantifiers(false),
m_eliminate_term_ite(false),
m_eliminate_and(true),
// m_eliminate_and(true),
m_macro_finder(false),
m_propagate_values(true),
m_propagate_booleans(false), // TODO << check peformance