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

translation?

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2017-11-28 15:17:00 -08:00
parent a57628fbcc
commit 7e56d05dcf
7 changed files with 33 additions and 10 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

9
src/ast/ast_translation.h
View file

@ -50,15 +50,18 @@ class ast_translation {
public:
ast_translation(ast_manager & from, ast_manager & to, bool copy_plugins = true) : m_from_manager(from), m_to_manager(to) {
if (copy_plugins)
m_to_manager.copy_families_plugins(m_from_manager);
m_to_manager.update_fresh_id(m_from_manager);
if (&from != &to) {
if (copy_plugins)
m_to_manager.copy_families_plugins(m_from_manager);
m_to_manager.update_fresh_id(m_from_manager);
}
}
~ast_translation();
template<typename T>
T * operator()(T const * n) {
if (&from() == &to()) return const_cast<T*>(n);
SASSERT(!n || from().contains(const_cast<T*>(n)));
ast * r = process(n);
SASSERT((!n && !r) || to().contains(const_cast<ast*>(r)));

13
src/sat/sat_solver/inc_sat_solver.cpp
View file

@ -108,11 +108,20 @@ public:
for (unsigned l : m_fmls_lim) result->m_fmls_lim.push_back(l);
for (unsigned a : m_asms_lim) result->m_asms_lim.push_back(a);
for (unsigned h : m_fmls_head_lim) result->m_fmls_head_lim.push_back(h);
std::cout << "translate internalized " << m_internalized_fmls.size() << "\n";
std::cout.flush();
for (expr* f : m_internalized_fmls) result->m_internalized_fmls.push_back(tr(f));
if (m_mc0.get()) result->m_mc0 = m_mc0->translate(tr);
std::cout << "mc0\n";
std::cout.flush();
model_converter_ref mc = concat(mc0(), get_model_converter().get());
if (mc) {
ast_translation tr(m, dst_m);
result->set_model_converter(mc->translate(tr));
}
std::cout << "mc1\n";
std::cout.flush();
result->m_internalized = m_internalized;
result->m_internalized_converted = m_internalized_converted;
if (mc0()) result->set_model_converter(mc0()->translate(tr));
return result;
}

4
src/solver/solver.cpp
View file

@ -212,3 +212,7 @@ void solver::updt_params(params_ref const & p) {
m_enforce_model_conversion = m_params.get_bool("solver.enforce_model_conversion", true);
}
void solver::hoist_converter(model_converter_ref& mc) {
}

1
src/solver/solver.h
View file

@ -226,6 +226,7 @@ protected:
bool is_literal(ast_manager& m, expr* e);
void hoist_converter(model_converter_ref& mc);
};
typedef ref<solver> solver_ref;

6
src/tactic/portfolio/bounded_int2bv_solver.cpp
View file

@ -81,7 +81,11 @@ public:
for (func_decl* f : m_bv_fns) result->m_bv_fns.push_back(tr(f));
for (func_decl* f : m_int_fns) result->m_int_fns.push_back(tr(f));
for (bound_manager* b : m_bounds) result->m_bounds.push_back(b->translate(dst_m));
if (mc0()) result->set_model_converter(mc0()->translate(tr));
model_converter_ref mc = concat(mc0(), m_solver->get_model_converter().get());
if (mc) {
ast_translation tr(m, dst_m);
result->set_model_converter(mc->translate(tr));
}
return result;
}

5
src/tactic/portfolio/enum2bv_solver.cpp
View file

@ -50,9 +50,10 @@ public:
virtual solver* translate(ast_manager& dst_m, params_ref const& p) {
solver* result = alloc(enum2bv_solver, dst_m, p, m_solver->translate(dst_m, p));
if (mc0()) {
model_converter_ref mc = concat(mc0(), m_solver->get_model_converter().get());
if (mc) {
ast_translation tr(m, dst_m);
result->set_model_converter(mc0()->translate(tr));
result->set_model_converter(mc->translate(tr));
}
return result;
}

5
src/tactic/portfolio/pb2bv_solver.cpp
View file

@ -50,9 +50,10 @@ public:
virtual solver* translate(ast_manager& dst_m, params_ref const& p) {
flush_assertions();
solver* result = alloc(pb2bv_solver, dst_m, p, m_solver->translate(dst_m, p));
if (mc0()) {
model_converter_ref mc = concat(mc0(), m_solver->get_model_converter().get());
if (mc) {
ast_translation tr(m, dst_m);
result->set_model_converter(mc0()->translate(tr));
result->set_model_converter(mc->translate(tr));
}
return result;
}