3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-06 17:44:08 +00:00

add initial stubs for model reconstruction trail

This commit is contained in:
Nikolaj Bjorner 2022-11-03 21:35:07 -07:00
parent 9007bdf780
commit e8112a6564
4 changed files with 126 additions and 1 deletions

View file

@ -3,6 +3,7 @@ z3_add_component(simplifiers
bv_slice.cpp
euf_completion.cpp
extract_eqs.cpp
model_reconstruction_trail.cpp
solve_eqs.cpp
COMPONENT_DEPENDENCIES
euf

View file

@ -32,8 +32,9 @@ Author:
#include "util/trail.h"
#include "util/statistics.h"
#include "util/params.h"
#include "ast/simplifiers/dependent_expr.h"
#include "ast/converters/model_converter.h"
#include "ast/simplifiers/dependent_expr.h"
/**
abstract interface to state updated by simplifiers.

View file

@ -0,0 +1,43 @@
/*++
Copyright (c) 2022 Microsoft Corporation
Module Name:
model_reconstruction_trail.cpp
Author:
Nikolaj Bjorner (nbjorner) 2022-11-3.
--*/
#include "ast/simplifiers/model_reconstruction_trail.h"
#include "ast/converters/generic_model_converter.h"
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;
auto [f, dep] = d;
for (expr* t : subterms::all(expr_ref(f, m)))
free_vars.mark(t);
NOT_IMPLEMENTED_YET();
}
/**
* retrieve the current model converter corresponding to chaining substitutions from the trail.
*/
model_converter_ref model_reconstruction_trail::get_model_converter() {
model_converter_ref mc = alloc(generic_model_converter, m, "dependent-expr-model");
// walk the trail from the back.
// add substitutions from the back to the generic model converter
// after they have been normalized using a global replace that replaces
// substituted variables by their terms.
NOT_IMPLEMENTED_YET();
return mc;
}

View file

@ -0,0 +1,80 @@
/*++
Copyright (c) 2022 Microsoft Corporation
Module Name:
model_reconstruction_trail.h
Abstract:
Model reconstruction trail
A model reconstruction trail comprises of a sequence of assignments
together with assertions that were removed in favor of the assignments.
The assignments satisfy the removed assertions but are not (necessarily)
equivalent to the removed assertions. For the case where assignments
are equivalent to removed assertions, we squash the removed assertions
and don't track them.
Author:
Nikolaj Bjorner (nbjorner) 2022-11-3.
--*/
#pragma once
#include "util/scoped_ptr_vector.h"
#include "ast/rewriter/expr_replacer.h"
#include "ast/simplifiers/dependent_expr.h"
#include "ast/converters/model_converter.h"
class model_reconstruction_trail {
ast_manager& m;
struct model_reconstruction_trail_entry {
scoped_ptr<expr_replacer> m_replace;
vector<dependent_expr> m_removed;
model_reconstruction_trail_entry(expr_replacer* r, vector<dependent_expr> const& rem) :
m_replace(r), m_removed(rem) {}
};
scoped_ptr_vector<model_reconstruction_trail_entry> m_trail;
unsigned_vector m_limit;
public:
model_reconstruction_trail(ast_manager& m) : m(m) {}
/**
* add a new substitution to the stack
*/
void push(expr_replacer* r, vector<dependent_expr> const& removed) {
m_trail.push_back(alloc(model_reconstruction_trail_entry, r, removed));
}
/**
* register a new depedent expression, update the trail
* by removing substitutions that are not equivalence preserving.
*/
void replay(dependent_expr const& d, vector<dependent_expr>& added);
/**
* retrieve the current model converter corresponding to chaining substitutions from the trail.
*/
model_converter_ref get_model_converter();
/**
* push a context. Portions of the trail added within a context are removed after a context pop.
*/
void push() {
m_limit.push_back(m_trail.size());
}
void pop(unsigned n) {
unsigned old_sz = m_limit[m_limit.size() - n];
m_trail.resize(old_sz);
m_limit.shrink(m_limit.size() - n);
}
};