mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-12 12:08:18 +00:00
Code Activity

enable incrementality for model reconstruction

Browse source
This commit is contained in:
Nikolaj Bjorner 2022-11-25 15:28:38 +07:00
parent 4e9f21c2a1
commit 6454014119
2 changed files with 29 additions and 18 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

33
src/ast/simplifiers/model_reconstruction_trail.cpp
View file

@ -18,9 +18,12 @@ Author:
#include "ast/converters/generic_model_converter.h" #include "ast/converters/generic_model_converter.h"
// accumulate a set of dependent exprs, updating m_trail to exclude loose
// substitutions that use variables from the dependent expressions.
// TODO: add filters to skip sections of the trail that do not touch the current free variables.
void model_reconstruction_trail::replay(dependent_expr const& d, vector<dependent_expr>& added) { void model_reconstruction_trail::replay(dependent_expr const& d, vector<dependent_expr>& added) {
// accumulate a set of dependent exprs, updating m_trail to exclude loose
// substitutions that use variables from the dependent expressions.
ast_mark free_vars; ast_mark free_vars;
scoped_ptr<expr_replacer> rp = mk_default_expr_replacer(m, false); scoped_ptr<expr_replacer> rp = mk_default_expr_replacer(m, false);
add_vars(d, free_vars); add_vars(d, free_vars);
@ -49,7 +52,6 @@ void model_reconstruction_trail::replay(dependent_expr const& d, vector<dependen
continue; continue;
} }
if (t->is_def()) { if (t->is_def()) {
macro_replacer mrp(m); macro_replacer mrp(m);
app_ref head(m); app_ref head(m);
@ -72,7 +74,6 @@ void model_reconstruction_trail::replay(dependent_expr const& d, vector<dependen
continue; continue;
} }
rp->set_substitution(t->m_subst.get()); rp->set_substitution(t->m_subst.get());
// rigid entries: // rigid entries:
// apply substitution to added in case of rigid model convertions // apply substitution to added in case of rigid model convertions
@ -89,25 +90,29 @@ void model_reconstruction_trail::replay(dependent_expr const& d, vector<dependen
* retrieve the current model converter corresponding to chaining substitutions from the trail. * retrieve the current model converter corresponding to chaining substitutions from the trail.
*/ */
model_converter_ref model_reconstruction_trail::get_model_converter() { model_converter_ref model_reconstruction_trail::get_model_converter() {
scoped_ptr<expr_replacer> rp = mk_default_expr_replacer(m, false);
expr_substitution subst(m, true, false);
rp->set_substitution(&subst);
generic_model_converter_ref mc = alloc(generic_model_converter, m, "dependent-expr-model"); generic_model_converter_ref mc = alloc(generic_model_converter, m, "dependent-expr-model");
for (unsigned i = 0; i < m_trail.size(); ++i) { unsigned i = 0;
append(*mc, i);
return model_converter_ref(mc.get());
}
/**
* Append model conversions starting at index i
*/
void model_reconstruction_trail::append(generic_model_converter& mc, unsigned& i) {
for (; i < m_trail.size(); ++i) {
auto* t = m_trail[i]; auto* t = m_trail[i];
if (!t->m_active) if (!t->m_active)
continue; continue;
else if (t->is_hide()) else if (t->is_hide())
mc->hide(t->m_decl); mc.hide(t->m_decl);
else if (t->is_def()) else if (t->is_def())
mc->add(t->m_decl, t->m_def); mc.add(t->m_decl, t->m_def);
else { else {
for (auto const& [v, def] : t->m_subst->sub()) for (auto const& [v, def] : t->m_subst->sub())
mc->add(v, def); mc.add(v, def);
} }
} }
return model_converter_ref(mc.get());
} }

6
src/ast/simplifiers/model_reconstruction_trail.h
View file

@ -29,6 +29,7 @@ Author:
#include "ast/rewriter/expr_replacer.h" #include "ast/rewriter/expr_replacer.h"
#include "ast/simplifiers/dependent_expr.h" #include "ast/simplifiers/dependent_expr.h"
#include "ast/converters/model_converter.h" #include "ast/converters/model_converter.h"
#include "ast/converters/generic_model_converter.h"
class model_reconstruction_trail { class model_reconstruction_trail {
@ -125,5 +126,10 @@ public:
* retrieve the current model converter corresponding to chaining substitutions from the trail. * retrieve the current model converter corresponding to chaining substitutions from the trail.
*/ */
model_converter_ref get_model_converter(); model_converter_ref get_model_converter();
/**
* Append new updates to model converter, update the current index into the trail in the process.
*/
void append(generic_model_converter& mc, unsigned& index);
}; };