From 7e56d05dcf4598b04d925ccebd8b786a5722e6ef Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Tue, 28 Nov 2017 15:17:00 -0800
Subject: [PATCH] translation?
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
src/ast/ast_translation.h | 9 ++++++---
src/sat/sat_solver/inc_sat_solver.cpp | 13 +++++++++++--
src/solver/solver.cpp | 4 ++++
src/solver/solver.h | 1 +
src/tactic/portfolio/bounded_int2bv_solver.cpp | 6 +++++-
src/tactic/portfolio/enum2bv_solver.cpp | 5 +++--
src/tactic/portfolio/pb2bv_solver.cpp | 5 +++--
7 files changed, 33 insertions(+), 10 deletions(-)
diff --git a/src/ast/ast_translation.h b/src/ast/ast_translation.h
index 886aaf417..9d09fbb76 100644
--- a/src/ast/ast_translation.h
+++ b/src/ast/ast_translation.h
@@ -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)));
diff --git a/src/sat/sat_solver/inc_sat_solver.cpp b/src/sat/sat_solver/inc_sat_solver.cpp
index 86b7e477d..60f185695 100644
--- a/src/sat/sat_solver/inc_sat_solver.cpp
+++ b/src/sat/sat_solver/inc_sat_solver.cpp
@@ -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;
}
diff --git a/src/solver/solver.cpp b/src/solver/solver.cpp
index eb2b0d016..606c32bed 100644
--- a/src/solver/solver.cpp
+++ b/src/solver/solver.cpp
@@ -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) {
+
+}
+
diff --git a/src/solver/solver.h b/src/solver/solver.h
index f6ad74042..2b1824cd3 100644
--- a/src/solver/solver.h
+++ b/src/solver/solver.h
@@ -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;
diff --git a/src/tactic/portfolio/bounded_int2bv_solver.cpp b/src/tactic/portfolio/bounded_int2bv_solver.cpp
index a2f4cabe4..0eb5cef18 100644
--- a/src/tactic/portfolio/bounded_int2bv_solver.cpp
+++ b/src/tactic/portfolio/bounded_int2bv_solver.cpp
@@ -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;
}
diff --git a/src/tactic/portfolio/enum2bv_solver.cpp b/src/tactic/portfolio/enum2bv_solver.cpp
index 4feaa622b..9c522a714 100644
--- a/src/tactic/portfolio/enum2bv_solver.cpp
+++ b/src/tactic/portfolio/enum2bv_solver.cpp
@@ -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;
}
diff --git a/src/tactic/portfolio/pb2bv_solver.cpp b/src/tactic/portfolio/pb2bv_solver.cpp
index ffc1ea09f..e22a41ad3 100644
--- a/src/tactic/portfolio/pb2bv_solver.cpp
+++ b/src/tactic/portfolio/pb2bv_solver.cpp
@@ -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;
}