mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-10-04 15:03:57 +00:00
Code Activity

Merge branch 'unstable' into contrib

Browse source
This commit is contained in:
Leonardo de Moura 2013-02-19 15:35:05 -08:00
commit b4d57e0ab1
171 changed files with 9433 additions and 3739 deletions
Download patch file Download diff file Expand all files Collapse all files

25
src/ast/arith_decl_plugin.cpp
View file

@ -154,6 +154,14 @@ void arith_decl_plugin::set_manager(ast_manager * m, family_id id) {
m->inc_ref(FIELD); \
}
#define MK_LEFT_ASSOC_OP(FIELD, NAME, KIND, SORT) { \
func_decl_info info(id, KIND); \
info.set_left_associative(); \
FIELD = m->mk_func_decl(symbol(NAME), SORT, SORT, SORT, info); \
m->inc_ref(FIELD); \
}
#define MK_OP(FIELD, NAME, KIND, SORT) \
FIELD = m->mk_func_decl(symbol(NAME), SORT, SORT, SORT, func_decl_info(id, KIND)); \
m->inc_ref(FIELD)
@ -163,15 +171,15 @@ void arith_decl_plugin::set_manager(ast_manager * m, family_id id) {
m->inc_ref(FIELD)
MK_AC_OP(m_r_add_decl, "+", OP_ADD, r);
MK_OP(m_r_sub_decl, "-", OP_SUB, r);
MK_LEFT_ASSOC_OP(m_r_sub_decl, "-", OP_SUB, r);
MK_AC_OP(m_r_mul_decl, "*", OP_MUL, r);
MK_OP(m_r_div_decl, "/", OP_DIV, r);
MK_LEFT_ASSOC_OP(m_r_div_decl, "/", OP_DIV, r);
MK_UNARY(m_r_uminus_decl, "-", OP_UMINUS, r);
MK_AC_OP(m_i_add_decl, "+", OP_ADD, i);
MK_OP(m_i_sub_decl, "-", OP_SUB, i);
MK_LEFT_ASSOC_OP(m_i_sub_decl, "-", OP_SUB, i);
MK_AC_OP(m_i_mul_decl, "*", OP_MUL, i);
MK_OP(m_i_div_decl, "div", OP_IDIV, i);
MK_LEFT_ASSOC_OP(m_i_div_decl, "div", OP_IDIV, i);
MK_OP(m_i_rem_decl, "rem", OP_REM, i);
MK_OP(m_i_mod_decl, "mod", OP_MOD, i);
MK_UNARY(m_i_uminus_decl, "-", OP_UMINUS, i);
@ -186,6 +194,9 @@ void arith_decl_plugin::set_manager(ast_manager * m, family_id id) {
MK_OP(m_r_power_decl, "^", OP_POWER, r);
MK_OP(m_i_power_decl, "^", OP_POWER, i);
MK_UNARY(m_i_abs_decl, "abs", OP_ABS, i);
MK_UNARY(m_r_abs_decl, "abs", OP_ABS, r);
MK_UNARY(m_sin_decl, "sin", OP_SIN, r);
MK_UNARY(m_cos_decl, "cos", OP_COS, r);
MK_UNARY(m_tan_decl, "tan", OP_TAN, r);
@ -255,6 +266,8 @@ arith_decl_plugin::arith_decl_plugin():
m_is_int_decl(0),
m_r_power_decl(0),
m_i_power_decl(0),
m_r_abs_decl(0),
m_i_abs_decl(0),
m_sin_decl(0),
m_cos_decl(0),
m_tan_decl(0),
@ -312,6 +325,8 @@ void arith_decl_plugin::finalize() {
DEC_REF(m_is_int_decl);
DEC_REF(m_i_power_decl);
DEC_REF(m_r_power_decl);
DEC_REF(m_i_abs_decl);
DEC_REF(m_r_abs_decl);
DEC_REF(m_sin_decl);
DEC_REF(m_cos_decl);
DEC_REF(m_tan_decl);
@ -364,6 +379,7 @@ inline func_decl * arith_decl_plugin::mk_func_decl(decl_kind k, bool is_real) {
case OP_TO_INT: return m_to_int_decl;
case OP_IS_INT: return m_is_int_decl;
case OP_POWER: return is_real ? m_r_power_decl : m_i_power_decl;
case OP_ABS: return is_real ? m_r_abs_decl : m_i_abs_decl;
case OP_SIN: return m_sin_decl;
case OP_COS: return m_cos_decl;
case OP_TAN: return m_tan_decl;
@ -530,6 +546,7 @@ void arith_decl_plugin::get_op_names(svector<builtin_name>& op_names, symbol con
op_names.push_back(builtin_name("to_real",OP_TO_REAL));
op_names.push_back(builtin_name("to_int",OP_TO_INT));
op_names.push_back(builtin_name("is_int",OP_IS_INT));
op_names.push_back(builtin_name("abs", OP_ABS));
if (logic == symbol::null) {
op_names.push_back(builtin_name("^", OP_POWER));
op_names.push_back(builtin_name("sin", OP_SIN));

4
src/ast/arith_decl_plugin.h
View file

@ -51,6 +51,7 @@ enum arith_op_kind {
OP_TO_REAL,
OP_TO_INT,
OP_IS_INT,
OP_ABS,
OP_POWER,
// hyperbolic and trigonometric functions
OP_SIN,
@ -121,6 +122,9 @@ protected:
func_decl * m_r_power_decl;
func_decl * m_i_power_decl;
func_decl * m_r_abs_decl;
func_decl * m_i_abs_decl;
func_decl * m_sin_decl;
func_decl * m_cos_decl;
func_decl * m_tan_decl;

27
src/ast/ast.cpp
View file

@ -1044,7 +1044,7 @@ func_decl * basic_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters
}
func_decl * basic_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters, parameter const * parameters,
unsigned num_args, expr * const * args, sort * range) {
unsigned num_args, expr * const * args, sort * range) {
switch (static_cast<basic_op_kind>(k)) {
case OP_TRUE: return m_true_decl;
case OP_FALSE: return m_false_decl;
@ -1816,6 +1816,12 @@ sort * ast_manager::mk_sort(symbol const & name, sort_info * info) {
return register_node(new_node);
}
sort * ast_manager::mk_uninterpreted_sort(symbol const & name, unsigned num_parameters, parameter const * parameters) {
user_sort_plugin * plugin = get_user_sort_plugin();
decl_kind kind = plugin->register_name(name);
return plugin->mk_sort(kind, num_parameters, parameters);
}
func_decl * ast_manager::mk_func_decl(symbol const & name, unsigned arity, sort * const * domain, sort * range,
bool assoc, bool comm, bool inj) {
func_decl_info info(null_family_id, null_decl_kind);
@ -1836,14 +1842,17 @@ func_decl * ast_manager::mk_func_decl(symbol const & name, unsigned arity, sort
}
void ast_manager::check_sort(func_decl const * decl, unsigned num_args, expr * const * args) const {
ast_manager& m = const_cast<ast_manager&>(*this);
if (decl->is_associative()) {
sort * expected = decl->get_domain(0);
for (unsigned i = 0; i < num_args; i++) {
sort * given = get_sort(args[i]);
if (!compatible_sorts(expected, given)) {
string_buffer<> buff;
buff << "invalid function application, sort mismatch on argument at position " << (i+1);
throw ast_exception(buff.c_str());
std::ostringstream buff;
buff << "invalid function application for " << decl->get_name() << ", ";
buff << "sort mismatch on argument at position " << (i+1) << ", ";
buff << "expected " << mk_pp(expected, m) << " but given " << mk_pp(given, m);
throw ast_exception(buff.str().c_str());
}
}
}
@ -1855,9 +1864,11 @@ void ast_manager::check_sort(func_decl const * decl, unsigned num_args, expr * c
sort * expected = decl->get_domain(i);
sort * given = get_sort(args[i]);
if (!compatible_sorts(expected, given)) {
string_buffer<> buff;
buff << "invalid function application, sort mismatch on argument at position " << (i+1);
throw ast_exception(buff.c_str());
std::ostringstream buff;
buff << "invalid function application for " << decl->get_name() << ", ";
buff << "sort mismatch on argument at position " << (i+1) << ", ";
buff << "expected " << mk_pp(expected, m) << " but given " << mk_pp(given, m);
throw ast_exception(buff.str().c_str());
}
}
}
@ -2058,7 +2069,7 @@ sort * ast_manager::mk_fresh_sort(char const * prefix) {
string_buffer<32> buffer;
buffer << prefix << "!" << m_fresh_id;
m_fresh_id++;
return mk_sort(symbol(buffer.c_str()));
return mk_uninterpreted_sort(symbol(buffer.c_str()));
}
symbol ast_manager::mk_fresh_var_name(char const * prefix) {

6
src/ast/ast.h
View file

@ -1622,11 +1622,13 @@ private:
sort * mk_sort(symbol const & name, sort_info * info);
public:
sort * mk_sort(symbol const & name) { return mk_sort(name, 0); }
sort * mk_uninterpreted_sort(symbol const & name, unsigned num_parameters, parameter const * parameters);
sort * mk_uninterpreted_sort(symbol const & name) { return mk_uninterpreted_sort(name, 0, 0); }
sort * mk_sort(symbol const & name, sort_info const & info) {
if (info.get_family_id() == null_family_id) {
return mk_sort(name, 0);
return mk_uninterpreted_sort(name);
}
else {
return mk_sort(name, &const_cast<sort_info &>(info));

22
src/ast/ast_ll_pp.cpp
View file

@ -126,7 +126,21 @@ public:
m_autil(m) {
}
void operator()(sort * n) {
void pp(ast* n) {
ast_mark visited;
pp(n, visited);
}
void pp(ast* n, ast_mark& visited) {
if (is_sort(n)) {
display_sort(to_sort(n));
}
else {
for_each_ast(*this, visited, n, true);
}
}
void operator()(sort* n) {
}
void operator()(func_decl * n) {
@ -296,17 +310,17 @@ public:
void ast_ll_pp(std::ostream & out, ast_manager & m, ast * n, bool only_exprs, bool compact) {
ll_printer p(out, m, n, only_exprs, compact);
for_each_ast(p, n, true);
p.pp(n);
}
void ast_ll_pp(std::ostream & out, ast_manager & m, ast * n, ast_mark & visited, bool only_exprs, bool compact) {
ll_printer p(out, m, n, only_exprs, compact);
for_each_ast(p, visited, n, true);
p.pp(n, visited);
}
void ast_def_ll_pp(std::ostream & out, ast_manager & m, ast * n, ast_mark & visited, bool only_exprs, bool compact) {
ll_printer p(out, m, 0, only_exprs, compact);
for_each_ast(p, visited, n, true);
p.pp(n, visited);
}
void ast_ll_bounded_pp(std::ostream & out, ast_manager & m, ast * n, unsigned depth) {

15
src/ast/ast_smt_pp.cpp
View file

@ -401,7 +401,12 @@ class smt_printer {
if (m_autil.is_numeral(n, val, is_int)) {
if (val.is_neg()) {
val.neg();
m_out << "(~ ";
if (m_is_smt2) {
m_out << "(- ";
}
else {
m_out << "(~ ";
}
display_rational(val, is_int);
m_out << ")";
}
@ -532,7 +537,7 @@ class smt_printer {
}
void print_bound(symbol const& name) {
if (name.is_numerical() || '?' != name.bare_str()[0]) {
if (!m_is_smt2 && (name.is_numerical() || '?' != name.bare_str()[0])) {
m_out << "?";
}
m_out << name;
@ -637,7 +642,9 @@ class smt_printer {
m_out << m_var_names[m_num_var_names - idx - 1];
}
else {
m_out << "?" << idx;
if (!m_is_smt2) {
m_out << "?" << idx;
}
}
}
@ -862,7 +869,7 @@ public:
for (unsigned j = 0; j < f->get_arity(); ++j) {
sort* s2 = f->get_domain(j);
if (!mark.is_marked(s2)) {
if (s2->get_family_id() == null_family_id) {
if (m_manager.is_uninterp(s2)) {
pp_sort_decl(mark, s2);
}
else if (!util.is_datatype(s2)) {

5
src/ast/ast_translation.cpp
View file

@ -111,7 +111,10 @@ void ast_translation::mk_sort(sort * s, frame & fr) {
sort_info * si = s->get_info();
sort * new_s;
if (si == 0) {
new_s = m_to_manager.mk_sort(s->get_name());
// TODO: investigate: this branch is probably unreachable.
// It became unreachable after we started using mk_uninterpreted_sort for creating uninterpreted sorts,
// and mk_uninterpreted_sort actually creates a user_sort.
new_s = m_to_manager.mk_uninterpreted_sort(s->get_name());
SASSERT(m_result_stack.size() == fr.m_rpos);
}
else {

7
src/ast/bv_decl_plugin.cpp
View file

@ -171,6 +171,9 @@ sort * bv_decl_plugin::mk_sort(decl_kind k, unsigned num_parameters, parameter c
m_manager->raise_exception("expecting one integer parameter to bit-vector sort");
}
unsigned bv_size = parameters[0].get_int();
if (bv_size == 0) {
m_manager->raise_exception("bit-vector size must be greater than zero");
}
mk_bv_sort(bv_size);
return m_bv_sorts[bv_size];
}
@ -457,7 +460,7 @@ func_decl * bv_decl_plugin::mk_mkbv(unsigned arity, sort * const * domain) {
}
func_decl * bv_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters, parameter const * parameters,
unsigned arity, sort * const * domain, sort * range) {
unsigned arity, sort * const * domain, sort * range) {
int bv_size;
if (k == OP_INT2BV && get_int2bv_size(num_parameters, parameters, bv_size)) {
// bv_size is filled in.
@ -555,7 +558,7 @@ func_decl * bv_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters, p
}
func_decl * bv_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters, parameter const * parameters,
unsigned num_args, expr * const * args, sort * range) {
unsigned num_args, expr * const * args, sort * range) {
int bv_size;
if (k == OP_INT2BV && get_int2bv_size(num_parameters, parameters, bv_size)) {
// bv_size is filled in.

6
src/ast/rewriter/arith_rewriter.cpp
View file

@ -70,6 +70,7 @@ br_status arith_rewriter::mk_app_core(func_decl * f, unsigned num_args, expr * c
case OP_TO_INT: SASSERT(num_args == 1); st = mk_to_int_core(args[0], result); break;
case OP_IS_INT: SASSERT(num_args == 1); st = mk_is_int(args[0], result); break;
case OP_POWER: SASSERT(num_args == 2); st = mk_power_core(args[0], args[1], result); break;
case OP_ABS: SASSERT(num_args == 1); st = mk_abs_core(args[0], result); break;
case OP_SIN: SASSERT(num_args == 1); st = mk_sin_core(args[0], result); break;
case OP_COS: SASSERT(num_args == 1); st = mk_cos_core(args[0], result); break;
case OP_TAN: SASSERT(num_args == 1); st = mk_tan_core(args[0], result); break;
@ -1024,6 +1025,11 @@ br_status arith_rewriter::mk_is_int(expr * arg, expr_ref & result) {
}
}
br_status arith_rewriter::mk_abs_core(expr * arg, expr_ref & result) {
result = m().mk_ite(m_util.mk_ge(arg, m_util.mk_numeral(rational(0), m_util.is_int(arg))), arg, m_util.mk_uminus(arg));
return BR_REWRITE2;
}
void arith_rewriter::set_cancel(bool f) {
m_util.set_cancel(f);
}

2
src/ast/rewriter/arith_rewriter.h
View file

@ -131,6 +131,8 @@ public:
}
void mk_gt(expr * arg1, expr * arg2, expr_ref & result) { mk_gt_core(arg1, arg2, result); }
br_status mk_abs_core(expr * arg, expr_ref & result);
br_status mk_div_core(expr * arg1, expr * arg2, expr_ref & result);
br_status mk_idiv_core(expr * arg1, expr * arg2, expr_ref & result);
br_status mk_mod_core(expr * arg1, expr * arg2, expr_ref & result);

4
src/ast/seq_decl_plugin.cpp
View file

@ -117,8 +117,8 @@ void seq_decl_plugin::init() {
if(m_init) return;
ast_manager& m = *m_manager;
m_init = true;
sort* A = m.mk_sort(symbol((unsigned)0));
sort* B = m.mk_sort(symbol((unsigned)1));
sort* A = m.mk_uninterpreted_sort(symbol((unsigned)0));
sort* B = m.mk_uninterpreted_sort(symbol((unsigned)1));
parameter paramA(A);
sort* seqA = m.mk_sort(m_family_id, SEQ_SORT, 1, &paramA);
sort* reA = m.mk_sort(m_family_id, RE_SORT, 1, &paramA);

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

@ -404,6 +404,7 @@ bool arith_simplifier_plugin::reduce(func_decl * f, unsigned num_args, expr * co
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:
UNREACHABLE();
@ -413,6 +414,14 @@ bool arith_simplifier_plugin::reduce(func_decl * f, unsigned num_args, expr * co
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;
}

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

@ -82,6 +82,7 @@ public:
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);

45
src/ast/static_features.cpp
View file

@ -165,7 +165,8 @@ void static_features::update_core(expr * e) {
// even if a benchmark does not contain any theory interpreted function decls, we still have to install
// the theory if the benchmark contains constants or function applications of an interpreted sort.
sort * s = m_manager.get_sort(e);
mark_theory(s->get_family_id());
if (!m_manager.is_uninterp(s))
mark_theory(s->get_family_id());
bool _is_gate = is_gate(e);
bool _is_eq = m_manager.is_eq(e);
@ -255,9 +256,11 @@ void static_features::update_core(expr * e) {
m_num_simple_eqs++;
}
sort * s = m_manager.get_sort(to_app(e)->get_arg(0));
family_id fid = s->get_family_id();
if (fid != null_family_id && fid != m_bfid)
inc_theory_eqs(fid);
if (!m_manager.is_uninterp(s)) {
family_id fid = s->get_family_id();
if (fid != null_family_id && fid != m_bfid)
inc_theory_eqs(fid);
}
}
if (!m_has_int && m_autil.is_int(e))
m_has_int = true;
@ -295,9 +298,11 @@ void static_features::update_core(expr * e) {
if (to_app(e)->get_num_args() == 0) {
m_num_uninterpreted_constants++;
sort * s = m_manager.get_sort(e);
family_id fid = s->get_family_id();
if (fid != null_family_id && fid != m_bfid)
inc_theory_constants(fid);
if (!m_manager.is_uninterp(s)) {
family_id fid = s->get_family_id();
if (fid != null_family_id && fid != m_bfid)
inc_theory_constants(fid);
}
}
}
func_decl * d = to_app(e)->get_decl();
@ -312,18 +317,20 @@ void static_features::update_core(expr * e) {
for (unsigned i = 0; i < num_args; i++) {
expr * arg = to_app(e)->get_arg(i);
sort * arg_s = m_manager.get_sort(arg);
family_id fid_arg = arg_s->get_family_id();
if (fid_arg != fid && fid_arg != null_family_id) {
m_num_aliens++;
inc_num_aliens(fid_arg);
if (fid_arg == m_afid) {
SASSERT(!_is_le_ge);
m_num_arith_terms++;
rational k;
TRACE("diff_term", tout << "diff_term: " << is_diff_term(arg, k) << "\n" << mk_pp(arg, m_manager) << "\n";);
if (is_diff_term(arg, k)) {
m_num_diff_terms++;
acc_num(k);
if (!m_manager.is_uninterp(arg_s)) {
family_id fid_arg = arg_s->get_family_id();
if (fid_arg != fid && fid_arg != null_family_id) {
m_num_aliens++;
inc_num_aliens(fid_arg);
if (fid_arg == m_afid) {
SASSERT(!_is_le_ge);
m_num_arith_terms++;
rational k;
TRACE("diff_term", tout << "diff_term: " << is_diff_term(arg, k) << "\n" << mk_pp(arg, m_manager) << "\n";);
if (is_diff_term(arg, k)) {
m_num_diff_terms++;
acc_num(k);
}
}
}
}

4
src/ast/substitution/matcher.cpp
View file

@ -49,6 +49,10 @@ bool matcher::operator()(expr * e1, expr * e2, substitution & s) {
if (is_var(p.second))
return false;
if (!is_app(p.first))
return false;
if (!is_app(p.second))
return false;
app * n1 = to_app(p.first);
app * n2 = to_app(p.second);

2
src/ast/substitution/matcher.h
View file

@ -32,7 +32,7 @@ class matcher {
ast_manager & m_manager;
substitution * m_subst;
cache m_cache;
// cache m_cache;
svector<expr_pair> m_todo;
void reset();

65
src/ast/substitution/substitution.cpp
View file

@ -20,22 +20,23 @@ Revision History:
#include"substitution.h"
#include"ast_pp.h"
#include"ast_ll_pp.h"
#include"rewriter.h"
substitution::substitution(ast_manager & m):
m_manager(m),
m_new_exprs(m) {
m_refs(m),
m_new_exprs(m),
m_state(CLEAN) {
}
void substitution::reset() {
reset_subst();
m_subst.reset();
m_vars.reset();
m_refs.reset();
m_scopes.reset();
reset_cache();
}
void substitution::reset_subst() {
m_subst.reset();
m_vars.reset();
m_scopes.reset();
}
void substitution::reset_cache() {
TRACE("subst_bug", tout << "substitution::reset_cache\n";
@ -43,6 +44,7 @@ void substitution::reset_cache() {
m_apply_cache.reset();
m_new_exprs.reset();
m_state = CLEAN;
}
void substitution::pop_scope(unsigned num_scopes) {
@ -57,7 +59,9 @@ void substitution::pop_scope(unsigned num_scopes) {
m_subst.erase(curr.first, curr.second);
}
m_vars.shrink(old_sz);
m_refs.shrink(old_sz);
m_scopes.shrink(new_lvl);
reset_cache();
}
inline void substitution::apply_visit(expr_offset const & n, bool & visited) {
@ -72,11 +76,14 @@ void substitution::apply(unsigned num_actual_offsets, unsigned const * deltas, e
TRACE("subst_bug", tout << "BEGIN substitution::apply\n";);
// It is incorrect to cache results between different calls if we are applying a substitution
// modulo a substitution s -> t.
if (s != expr_offset(0,0))
if (m_state == INSERT || s != expr_offset(0,0))
reset_cache();
m_state = APPLY;
unsigned j;
expr * e;
unsigned off;
@ -160,6 +167,48 @@ void substitution::apply(unsigned num_actual_offsets, unsigned const * deltas, e
}
}
break;
case AST_QUANTIFIER: {
quantifier* q = to_quantifier(e);
unsigned num_vars = q->get_num_decls();
substitution subst(m_manager);
expr_ref er(m_manager);
subst.reserve(m_subst.offsets_capacity(), m_subst.vars_capacity() + num_vars);
var_shifter var_sh(m_manager);
expr_offset r;
for (unsigned i = 0; i < m_subst.offsets_capacity(); i++) {
for (unsigned j = 0; j < m_subst.vars_capacity(); j++) {
if (find(j, i, r)) {
var_sh(r.get_expr(), num_vars, er);
subst.insert(j + num_vars, i, expr_offset(er, r.get_offset()));
}
}
}
expr_offset body(q->get_expr(), off);
expr_ref s1_ref(m_manager), t1_ref(m_manager);
if (s.get_expr() != 0) {
var_sh(s.get_expr(), num_vars, s1_ref);
}
if (t.get_expr() != 0) {
var_sh(t.get_expr(), num_vars, t1_ref);
}
expr_offset s1(s1_ref, s.get_offset());
expr_offset t1(t1_ref, t.get_offset());
expr_ref_vector pats(m_manager), no_pats(m_manager);
for (unsigned i = 0; i < q->get_num_patterns(); ++i) {
subst.apply(num_actual_offsets, deltas, expr_offset(q->get_pattern(i), off), s1, t1, er);
pats.push_back(er);
}
for (unsigned i = 0; i < q->get_num_no_patterns(); ++i) {
subst.apply(num_actual_offsets, deltas, expr_offset(q->get_no_pattern(i), off), s1, t1, er);
no_pats.push_back(er);
}
subst.apply(num_actual_offsets, deltas, body, s1, t1, er);
er = m_manager.update_quantifier(q, pats.size(), pats.c_ptr(), no_pats.size(), no_pats.c_ptr(), er);
m_todo.pop_back();
m_new_exprs.push_back(er);
m_apply_cache.insert(n, er);
break;
}
default:
UNREACHABLE();
}

23
src/ast/substitution/substitution.h
View file

@ -16,6 +16,19 @@ Author:
Revision History:
nbjorner 2013-01-21:
- reset the apply cache on pop_scope to make sure that popped
substitutions are invalidated.
- reset_cache if a new binding was added after application
of a substitution.
- Add m_refs to make sure terms in the range of the
substitution have the same life-time as the substitution.
- Remove reset_subst() function. If called without resetting the cache, then
results of applying substitutions are incoherent.
- Replace UNREACHABLE segment for quantifiers by recursive invocation of substitution
that updates expressions within quantifiers. It shifts all variables in the domain
of the current substitution by the number of quantified variables.
--*/
#ifndef _SUBSTITUTION_H_
#define _SUBSTITUTION_H_
@ -34,6 +47,7 @@ class substitution {
// field for backtracking
typedef std::pair<unsigned, unsigned> var_offset;
svector<var_offset> m_vars;
expr_ref_vector m_refs;
unsigned_vector m_scopes;
// fields for applying substitutions
@ -45,6 +59,11 @@ class substitution {
enum color { White, Grey, Black };
expr_offset_map<color> m_color;
// keep track of how substitution state was last updated.
enum state { CLEAN, APPLY, INSERT };
state m_state;
#ifdef Z3DEBUG
unsigned m_max_offset_since_reset;
#endif
@ -81,8 +100,6 @@ public:
// reset everything
void reset();
// reset only the mapping from variables to expressions
void reset_subst();
// reset only the substitution application cache
void reset_cache();
@ -119,7 +136,9 @@ public:
TRACE("subst_insert", tout << "inserting: #" << v_idx << ":" << offset << " --> " << mk_pp(t.get_expr(), m_manager)
<< ":" << t.get_offset() << "\n";);
m_vars.push_back(var_offset(v_idx, offset));
m_refs.push_back(t.get_expr());
m_subst.insert(v_idx, offset, t);
m_state = INSERT;
}
void insert(var * v, unsigned offset, expr_offset const & t) { insert(v->get_idx(), offset, t); }
void insert(expr_offset v, expr_offset const & t) {