diff --git a/scripts/mk_project.py b/scripts/mk_project.py index d11c5fd30..6ea794040 100644 --- a/scripts/mk_project.py +++ b/scripts/mk_project.py @@ -22,7 +22,7 @@ def init_project_def(): add_lib('normal_forms', ['rewriter'], 'ast/normal_forms') add_lib('model', ['rewriter']) add_lib('tactic', ['ast', 'model']) - add_lib('substitution', ['ast'], 'ast/substitution') + add_lib('substitution', ['ast', 'rewriter'], 'ast/substitution') add_lib('parser_util', ['ast'], 'parsers/util') add_lib('grobner', ['ast'], 'math/grobner') add_lib('euclid', ['util'], 'math/euclid') diff --git a/src/ast/substitution/substitution.cpp b/src/ast/substitution/substitution.cpp index 82d1fbfef..2427c9c25 100644 --- a/src/ast/substitution/substitution.cpp +++ b/src/ast/substitution/substitution.cpp @@ -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,8 +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); - m_apply_cache.reset(); + reset_cache(); } inline void substitution::apply_visit(expr_offset const & n, bool & visited) { @@ -73,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; @@ -161,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()); + 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, 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(); } diff --git a/src/ast/substitution/substitution.h b/src/ast/substitution/substitution.h index 1d12dc278..3227a6fec 100644 --- a/src/ast/substitution/substitution.h +++ b/src/ast/substitution/substitution.h @@ -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 var_offset; svector 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 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) {