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

Merge pull request #298 from NikolajBjorner/nsb/master

Browse source 
Nsb/master
This commit is contained in:
Nikolaj Bjorner 2015-11-07 10:13:47 -08:00
parent 396875bedf 13b19eb351
commit 73c4e938ce
33 changed files with 322 additions and 36 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

13
src/api/api_solver.cpp
View file

@ -97,6 +97,19 @@ extern "C" {
Z3_CATCH_RETURN(0);
}
Z3_solver Z3_API Z3_solver_translate(Z3_context c, Z3_solver s, Z3_context target) {
Z3_TRY;
LOG_Z3_solver_translate(c, s, target);
RESET_ERROR_CODE();
params_ref const& p = to_solver(s)->m_params;
Z3_solver_ref * sr = alloc(Z3_solver_ref, 0);
sr->m_solver = to_solver(s)->m_solver->translate(mk_c(target)->m(), p);
mk_c(target)->save_object(sr);
Z3_solver r = of_solver(sr);
RETURN_Z3(r);
Z3_CATCH_RETURN(0);
}
Z3_string Z3_API Z3_solver_get_help(Z3_context c, Z3_solver s) {
Z3_TRY;
LOG_Z3_solver_get_help(c, s);

4
src/api/c++/z3++.h
View file

@ -1359,9 +1359,13 @@ namespace z3 {
Z3_solver_inc_ref(ctx(), s);
}
public:
struct simple {};
struct translate {};
solver(context & c):object(c) { init(Z3_mk_solver(c)); }
solver(context & c, simple):object(c) { init(Z3_mk_simple_solver(c)); }
solver(context & c, Z3_solver s):object(c) { init(s); }
solver(context & c, char const * logic):object(c) { init(Z3_mk_solver_for_logic(c, c.str_symbol(logic))); }
solver(context & c, solver const& src, translate): object(c) { init(Z3_solver_translate(src.ctx(), src, c)); }
solver(solver const & s):object(s) { init(s.m_solver); }
~solver() { Z3_solver_dec_ref(ctx(), m_solver); }
operator Z3_solver() const { return m_solver; }

11
src/api/dotnet/Solver.cs
View file

@ -290,6 +290,17 @@ namespace Microsoft.Z3
}
}
/// <summary>
/// Create a clone of the current solver with respect to <c>ctx</c>.
/// </summary>
public Solver Translate(Context ctx)
{
Contract.Requires(ctx != null);
Contract.Ensures(Contract.Result<Solver>() != null);
return new Solver(ctx, Native.Z3_solver_translate(Context.nCtx, NativeObject, ctx.nCtx));
}
/// <summary>
/// Solver statistics.
/// </summary>

8
src/api/java/Solver.java
View file

@ -293,6 +293,14 @@ public class Solver extends Z3Object
getNativeObject());
}
/**
* Create a clone of the current solver with respect to <c>ctx</c>.
*/
public Solver translate(Context ctx)
{
return new Solver(ctx, Native.solverTranslate(getContext().nCtx(), getNativeObject(), ctx.nCtx()));
}
/**
* Solver statistics.
*

13
src/api/python/z3.py
View file

@ -6084,6 +6084,19 @@ class Solver(Z3PPObject):
"""Return a formatted string with all added constraints."""
return obj_to_string(self)
def translate(self, target):
"""Translate `self` to the context `target`. That is, return a copy of `self` in the context `target`.
>>> c1 = Context()
>>> c2 = Context()
>>> s1 = Solver(ctx=c1)
>>> s2 = s1.translate(c2)
"""
if __debug__:
_z3_assert(isinstance(target, Context), "argument must be a Z3 context")
solver = Z3_solver_translate(self.ctx.ref(), self.solver, target.ref())
return Solver(solver, target)
def sexpr(self):
"""Return a formatted string (in Lisp-like format) with all added constraints. We say the string is in s-expression format.

8
src/api/z3_api.h
View file

@ -7062,6 +7062,14 @@ END_MLAPI_EXCLUDE
*/
Z3_solver Z3_API Z3_mk_solver_from_tactic(Z3_context c, Z3_tactic t);
/**
\brief Copy a solver \c s from the context \c source to a the context \c target.
def_API('Z3_solver_translate', SOLVER, (_in(CONTEXT), _in(SOLVER), _in(CONTEXT)))
*/
Z3_solver Z3_API Z3_solver_translate(Z3_context source, Z3_solver s, Z3_context target);
/**
\brief Return a string describing all solver available parameters.

1
src/ast/array_decl_plugin.cpp
View file

@ -519,6 +519,7 @@ void array_decl_plugin::get_op_names(svector<builtin_name>& op_names, symbol con
op_names.push_back(builtin_name("complement",OP_SET_COMPLEMENT));
op_names.push_back(builtin_name("subset",OP_SET_SUBSET));
op_names.push_back(builtin_name("as-array", OP_AS_ARRAY));
//op_names.push_back(builtin_name("array-ext", OP_ARRAY_EXT_SKOLEM));
}
}

1
src/ast/ast_translation.cpp
View file

@ -184,6 +184,7 @@ void ast_translation::mk_func_decl(func_decl * f, frame & fr) {
}
ast * ast_translation::process(ast const * _n) {
if (!_n) return 0;
SASSERT(m_result_stack.empty());
SASSERT(m_frame_stack.empty());
SASSERT(m_extra_children_stack.empty());

4
src/ast/ast_translation.h
View file

@ -58,9 +58,9 @@ public:
template<typename T>
T * operator()(T const * n) {
SASSERT(from().contains(const_cast<T*>(n)));
SASSERT(!n || from().contains(const_cast<T*>(n)));
ast * r = process(n);
SASSERT(to().contains(const_cast<ast*>(r)));
SASSERT((!n && !r) || to().contains(const_cast<ast*>(r)));
return static_cast<T*>(r);
}

5
src/opt/opt_solver.cpp
View file

@ -63,6 +63,11 @@ namespace opt {
m_context.updt_params(_p);
}
solver* opt_solver::translate(ast_manager& m, params_ref const& p) {
UNREACHABLE();
return 0;
}
void opt_solver::collect_param_descrs(param_descrs & r) {
m_context.collect_param_descrs(r);
}

1
src/opt/opt_solver.h
View file

@ -86,6 +86,7 @@ namespace opt {
opt_solver(ast_manager & m, params_ref const & p, filter_model_converter& fm);
virtual ~opt_solver();
virtual solver* translate(ast_manager& m, params_ref const& p);
virtual void updt_params(params_ref & p);
virtual void collect_param_descrs(param_descrs & r);
virtual void collect_statistics(statistics & st) const;

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

@ -32,6 +32,7 @@ Notes:
#include "model_smt2_pp.h"
#include "filter_model_converter.h"
#include "bit_blaster_model_converter.h"
#include "ast_translation.h"
// incremental SAT solver.
class inc_sat_solver : public solver {
@ -93,7 +94,25 @@ public:
}
virtual ~inc_sat_solver() {}
virtual solver* translate(ast_manager& dst_m, params_ref const& p) {
ast_translation tr(m, dst_m);
if (m_num_scopes > 0) {
throw default_exception("Cannot translate sat solver at non-base level");
}
inc_sat_solver* result = alloc(inc_sat_solver, dst_m, p);
expr_ref fml(dst_m);
for (unsigned i = 0; i < m_fmls.size(); ++i) {
fml = tr(m_fmls[i].get());
result->m_fmls.push_back(fml);
}
for (unsigned i = 0; i < m_asmsf.size(); ++i) {
fml = tr(m_asmsf[i].get());
result->m_asmsf.push_back(fml);
}
return result;
}
virtual void set_progress_callback(progress_callback * callback) {}
virtual lbool check_sat(unsigned num_assumptions, expr * const * assumptions) {

166
src/smt/smt_context.cpp
View file

@ -36,6 +36,7 @@ Revision History:
#include"smt_model_finder.h"
#include"model_pp.h"
#include"ast_smt2_pp.h"
#include"ast_translation.h"
namespace smt {
@ -98,38 +99,159 @@ namespace smt {
m_model_generator->set_context(this);
}
literal context::translate_literal(
literal lit, context& src_ctx, context& dst_ctx,
vector<bool_var> b2v, ast_translation& tr) {
ast_manager& dst_m = dst_ctx.get_manager();
ast_manager& src_m = src_ctx.get_manager();
expr_ref dst_f(dst_m);
SASSERT(lit != false_literal && lit != true_literal);
bool_var v = b2v.get(lit.var(), null_bool_var);
if (v == null_bool_var) {
expr* e = src_ctx.m_bool_var2expr.get(lit.var(), 0);
SASSERT(e);
dst_f = tr(e);
v = dst_ctx.get_bool_var_of_id_option(dst_f->get_id());
if (v != null_bool_var) {
}
else if (src_m.is_not(e) || src_m.is_and(e) || src_m.is_or(e) ||
src_m.is_iff(e) || src_m.is_ite(e)) {
v = dst_ctx.mk_bool_var(dst_f);
}
else {
dst_ctx.internalize_formula(dst_f, false);
v = dst_ctx.get_bool_var(dst_f);
}
b2v.setx(lit.var(), v, null_bool_var);
}
return literal(v, lit.sign());
}
void context::copy(context& src_ctx, context& dst_ctx) {
ast_manager& dst_m = dst_ctx.get_manager();
ast_manager& src_m = src_ctx.get_manager();
src_ctx.pop_to_base_lvl();
if (src_ctx.m_base_lvl > 0) {
throw default_exception("Cloning contexts within a user-scope is not allowed");
}
SASSERT(src_ctx.m_base_lvl == 0);
ast_translation tr(src_m, dst_m, false);
dst_ctx.set_logic(src_ctx.m_setup.get_logic());
dst_ctx.copy_plugins(src_ctx, dst_ctx);
asserted_formulas& src_af = src_ctx.m_asserted_formulas;
asserted_formulas& dst_af = dst_ctx.m_asserted_formulas;
// Copy asserted formulas.
for (unsigned i = 0; i < src_af.get_num_formulas(); ++i) {
expr_ref fml(dst_m);
proof_ref pr(dst_m);
proof* pr_src = src_af.get_formula_proof(i);
fml = tr(src_af.get_formula(i));
if (pr_src) {
pr = tr(pr_src);
}
dst_af.assert_expr(fml, pr);
}
if (!src_ctx.m_setup.already_configured()) {
return;
}
dst_ctx.setup_context(dst_ctx.m_fparams.m_auto_config);
dst_ctx.internalize_assertions();
vector<bool_var> b2v;
#define TRANSLATE(_lit) translate_literal(_lit, src_ctx, dst_ctx, b2v, tr)
for (unsigned i = 0; i < src_ctx.m_assigned_literals.size(); ++i) {
literal lit;
lit = TRANSLATE(src_ctx.m_assigned_literals[i]);
dst_ctx.mk_clause(1, &lit, 0, CLS_AUX, 0);
}
#if 0
literal_vector lits;
expr_ref_vector cls(src_m);
for (unsigned i = 0; i < src_ctx.m_lemmas.size(); ++i) {
lits.reset();
cls.reset();
clause& src_cls = *src_ctx.m_lemmas[i];
unsigned sz = src_cls.get_num_literals();
for (unsigned j = 0; j < sz; ++j) {
literal lit = TRANSLATE(src_cls.get_literal(j));
lits.push_back(lit);
}
dst_ctx.mk_clause(lits.size(), lits.c_ptr(), 0, src_cls.get_kind(), 0);
}
vector<watch_list>::const_iterator it = src_ctx.m_watches.begin();
vector<watch_list>::const_iterator end = src_ctx.m_watches.end();
literal ls[2];
for (unsigned l_idx = 0; it != end; ++it, ++l_idx) {
literal l1 = to_literal(l_idx);
literal neg_l1 = ~l1;
watch_list const & wl = *it;
literal const * it2 = wl.begin_literals();
literal const * end2 = wl.end_literals();
for (; it2 != end2; ++it2) {
literal l2 = *it2;
if (l1.index() < l2.index()) {
ls[0] = TRANSLATE(neg_l1);
ls[1] = TRANSLATE(l2);
dst_ctx.mk_clause(2, ls, 0, CLS_AUX, 0);
}
}
}
#endif
TRACE("smt_context",
src_ctx.display(tout);
dst_ctx.display(tout););
}
context::~context() {
flush();
}
void context::copy_plugins(context& src, context& dst) {
// copy missing simplifier_plugins
// remark: some simplifier_plugins are automatically created by the asserted_formulas class.
simplifier & src_s = src.get_simplifier();
simplifier & dst_s = dst.get_simplifier();
ptr_vector<simplifier_plugin>::const_iterator it1 = src_s.begin_plugins();
ptr_vector<simplifier_plugin>::const_iterator end1 = src_s.end_plugins();
for (; it1 != end1; ++it1) {
simplifier_plugin * p = *it1;
if (dst_s.get_plugin(p->get_family_id()) == 0) {
dst.register_plugin(p->mk_fresh());
}
SASSERT(dst_s.get_plugin(p->get_family_id()) != 0);
}
// copy theory plugins
ptr_vector<theory>::iterator it2 = src.m_theory_set.begin();
ptr_vector<theory>::iterator end2 = src.m_theory_set.end();
for (; it2 != end2; ++it2) {
theory * new_th = (*it2)->mk_fresh(&dst);
dst.register_plugin(new_th);
}
}
context * context::mk_fresh(symbol const * l, smt_params * p) {
context * new_ctx = alloc(context, m_manager, p == 0 ? m_fparams : *p);
new_ctx->set_logic(l == 0 ? m_setup.get_logic() : *l);
// copy missing simplifier_plugins
// remark: some simplifier_plugins are automatically created by the asserted_formulas class.
simplifier & s = get_simplifier();
simplifier & new_s = new_ctx->get_simplifier();
ptr_vector<simplifier_plugin>::const_iterator it1 = s.begin_plugins();
ptr_vector<simplifier_plugin>::const_iterator end1 = s.end_plugins();
for (; it1 != end1; ++it1) {
simplifier_plugin * p = *it1;
if (new_s.get_plugin(p->get_family_id()) == 0) {
new_ctx->register_plugin(p->mk_fresh());
}
SASSERT(new_s.get_plugin(p->get_family_id()) != 0);
}
// copy theory plugins
ptr_vector<theory>::iterator it2 = m_theory_set.begin();
ptr_vector<theory>::iterator end2 = m_theory_set.end();
for (; it2 != end2; ++it2) {
theory * new_th = (*it2)->mk_fresh(new_ctx);
new_ctx->register_plugin(new_th);
}
new_ctx->m_setup.mark_already_configured();
copy_plugins(*this, *new_ctx);
return new_ctx;
}
void context::init() {
app * t = m_manager.mk_true();
mk_bool_var(t);

15
src/smt/smt_context.h
View file

@ -1326,9 +1326,18 @@ namespace smt {
// -----------------------------------
void assert_expr_core(expr * e, proof * pr);
// copy plugins into a fresh context.
void copy_plugins(context& src, context& dst);
static literal translate_literal(
literal lit, context& src_ctx, context& dst_ctx,
vector<bool_var> b2v, ast_translation& tr);
public:
context(ast_manager & m, smt_params & fp, params_ref const & p = params_ref());
virtual ~context();
/**
@ -1340,6 +1349,12 @@ namespace smt {
*/
context * mk_fresh(symbol const * l = 0, smt_params * p = 0);
static void copy(context& src, context& dst);
/**
\brief Translate context to use new manager m.
*/
app * mk_eq_atom(expr * lhs, expr * rhs);
bool set_logic(symbol logic) { return m_setup.set_logic(logic); }

9
src/smt/smt_kernel.cpp
View file

@ -32,6 +32,10 @@ namespace smt {
m_params(p) {
}
static void copy(imp& src, imp& dst) {
context::copy(src.m_kernel, dst.m_kernel);
}
smt_params & fparams() {
return m_kernel.get_fparams();
}
@ -193,6 +197,11 @@ namespace smt {
return m_imp->m();
}
void kernel::copy(kernel& src, kernel& dst) {
imp::copy(*src.m_imp, *dst.m_imp);
}
bool kernel::set_logic(symbol logic) {
return m_imp->set_logic(logic);
}

2
src/smt/smt_kernel.h
View file

@ -50,6 +50,8 @@ namespace smt {
~kernel();
static void copy(kernel& src, kernel& dst);
ast_manager & m() const;
/**

6
src/smt/smt_solver.cpp
View file

@ -37,6 +37,12 @@ namespace smt {
if (m_logic != symbol::null)
m_context.set_logic(m_logic);
}
virtual solver* translate(ast_manager& m, params_ref const& p) {
solver* result = alloc(solver, m, p, m_logic);
smt::kernel::copy(m_context, result->m_context);
return result;
}
virtual ~solver() {
}

2
src/smt/theory_arith.h
View file

@ -1029,7 +1029,7 @@ namespace smt {
theory_arith(ast_manager & m, theory_arith_params & params);
virtual ~theory_arith();
virtual theory * mk_fresh(context * new_ctx) { return alloc(theory_arith, get_manager(), m_params); }
virtual theory * mk_fresh(context * new_ctx);
virtual void setup();

5
src/smt/theory_arith_core.h
View file

@ -1538,6 +1538,11 @@ namespace smt {
theory_arith<Ext>::~theory_arith() {
}
template<typename Ext>
theory* theory_arith<Ext>::mk_fresh(context* new_ctx) {
return alloc(theory_arith<Ext>, new_ctx->get_manager(), m_params);
}
template<typename Ext>
void theory_arith<Ext>::setup() {
m_random.set_seed(m_params.m_arith_random_seed);

2
src/smt/theory_array.h
View file

@ -98,7 +98,7 @@ namespace smt {
theory_array(ast_manager & m, theory_array_params & params);
virtual ~theory_array();
virtual theory * mk_fresh(context * new_ctx) { return alloc(theory_array, get_manager(), m_params); }
virtual theory * mk_fresh(context * new_ctx) { return alloc(theory_array, new_ctx->get_manager(), m_params); }
virtual char const * get_name() const { return "array"; }

2
src/smt/theory_array_full.h
View file

@ -91,7 +91,7 @@ namespace smt {
theory_array_full(ast_manager & m, theory_array_params & params);
virtual ~theory_array_full();
virtual theory * mk_fresh(context * new_ctx) { return alloc(theory_array_full, get_manager(), m_params); }
virtual theory * mk_fresh(context * new_ctx) { return alloc(theory_array_full, new_ctx->get_manager(), m_params); }
virtual void merge_eh(theory_var v1, theory_var v2, theory_var, theory_var);
virtual void display_var(std::ostream & out, theory_var v) const;

5
src/smt/theory_bv.cpp
View file

@ -1312,6 +1312,11 @@ namespace smt {
theory_bv::~theory_bv() {
}
theory* theory_bv::mk_fresh(context* new_ctx) {
return alloc(theory_bv, new_ctx->get_manager(), m_params, m_bb.get_params());
}
void theory_bv::merge_eh(theory_var r1, theory_var r2, theory_var v1, theory_var v2) {
TRACE("bv", tout << "merging: #" << get_enode(v1)->get_owner_id() << " #" << get_enode(v2)->get_owner_id() << "\n";);

2
src/smt/theory_bv.h
View file

@ -253,7 +253,7 @@ namespace smt {
theory_bv(ast_manager & m, theory_bv_params const & params, bit_blaster_params const & bb_params);
virtual ~theory_bv();
virtual theory * mk_fresh(context * new_ctx) { return alloc(theory_bv, get_manager(), m_params, m_bb.get_params()); }
virtual theory * mk_fresh(context * new_ctx);
virtual char const * get_name() const { return "bit-vector"; }

2
src/smt/theory_datatype.h
View file

@ -101,7 +101,7 @@ namespace smt {
public:
theory_datatype(ast_manager & m, theory_datatype_params & p);
virtual ~theory_datatype();
virtual theory * mk_fresh(context * new_ctx) { return alloc(theory_datatype, get_manager(), m_params); }
virtual theory * mk_fresh(context * new_ctx) { return alloc(theory_datatype, new_ctx->get_manager(), m_params); }
virtual void display(std::ostream & out) const;
virtual void collect_statistics(::statistics & st) const;
virtual void init_model(model_generator & m);

2
src/smt/theory_dense_diff_logic.h
View file

@ -282,7 +282,7 @@ namespace smt {
theory_dense_diff_logic(ast_manager & m, theory_arith_params & p);
virtual ~theory_dense_diff_logic() { reset_eh(); }
virtual theory * mk_fresh(context * new_ctx) { return alloc(theory_dense_diff_logic, get_manager(), m_params); }
virtual theory * mk_fresh(context * new_ctx) { return alloc(theory_dense_diff_logic, new_ctx->get_manager(), m_params); }
virtual char const * get_name() const { return "difference-logic"; }

2
src/smt/theory_diff_logic.h
View file

@ -243,7 +243,7 @@ namespace smt {
reset_eh();
}
virtual theory * mk_fresh(context * new_ctx) { return alloc(theory_diff_logic, get_manager(), m_params); }
virtual theory * mk_fresh(context * new_ctx) { return alloc(theory_diff_logic, new_ctx->get_manager(), m_params); }
virtual char const * get_name() const { return "difference-logic"; }

2
src/smt/theory_dl.cpp
View file

@ -155,7 +155,7 @@ namespace smt {
}
virtual theory * mk_fresh(context * new_ctx) {
return alloc(theory_dl, get_manager());
return alloc(theory_dl, new_ctx->get_manager());
}
virtual void init_model(smt::model_generator & m) {

2
src/smt/theory_fpa.h
View file

@ -158,7 +158,7 @@ namespace smt {
virtual void push_scope_eh();
virtual void pop_scope_eh(unsigned num_scopes);
virtual void reset_eh();
virtual theory* mk_fresh(context*) { return alloc(theory_fpa, get_manager()); }
virtual theory* mk_fresh(context* new_ctx) { return alloc(theory_fpa, new_ctx->get_manager()); }
virtual char const * get_name() const { return "fpa"; }
virtual model_value_proc * mk_value(enode * n, model_generator & mg);

2
src/smt/theory_seq_empty.h
View file

@ -29,7 +29,7 @@ namespace smt {
virtual bool internalize_term(app*) { return internalize_atom(0,false); }
virtual void new_eq_eh(theory_var, theory_var) { }
virtual void new_diseq_eh(theory_var, theory_var) {}
virtual theory* mk_fresh(context*) { return alloc(theory_seq_empty, get_manager()); }
virtual theory* mk_fresh(context* new_ctx) { return alloc(theory_seq_empty, new_ctx->get_manager()); }
virtual char const * get_name() const { return "seq-empty"; }
public:
theory_seq_empty(ast_manager& m):theory(m.mk_family_id("seq")), m_used(false) {}

2
src/smt/theory_utvpi.h
View file

@ -183,7 +183,7 @@ namespace smt {
virtual ~theory_utvpi();
virtual theory * mk_fresh(context * new_ctx) { return alloc(theory_utvpi, get_manager()); }
virtual theory * mk_fresh(context * new_ctx) { return alloc(theory_utvpi, new_ctx->get_manager()); }
virtual char const * get_name() const { return "utvpi-logic"; }

11
src/solver/combined_solver.cpp
View file

@ -127,6 +127,17 @@ public:
m_use_solver1_results = true;
}
solver* translate(ast_manager& m, params_ref const& p) {
solver* s1 = m_solver1->translate(m, p);
solver* s2 = m_solver2->translate(m, p);
combined_solver* r = alloc(combined_solver, s1, s2, p);
r->m_solver2_initialized = m_solver2_initialized;
r->m_inc_mode = m_inc_mode;
r->m_check_sat_executed = m_check_sat_executed;
r->m_use_solver1_results = m_use_solver1_results;
return r;
}
virtual void updt_params(params_ref const & p) {
m_solver1->updt_params(p);
m_solver2->updt_params(p);

8
src/solver/solver.h
View file

@ -46,6 +46,12 @@ public:
class solver : public check_sat_result {
public:
virtual ~solver() {}
/**
\brief Creates a clone of the solver.
*/
virtual solver* translate(ast_manager& m, params_ref const& p) = 0;
/**
\brief Update the solver internal settings.
*/
@ -135,6 +141,8 @@ public:
*/
virtual expr * get_assumption(unsigned idx) const = 0;
/**
\brief Display the content of this solver.
*/

19
src/solver/tactic2solver.cpp
View file

@ -22,6 +22,7 @@ Notes:
#include"solver_na2as.h"
#include"tactic.h"
#include"ast_pp_util.h"
#include"ast_translation.h"
/**
\brief Simulates the incremental solver interface using a tactic.
@ -45,6 +46,8 @@ public:
tactic2solver(ast_manager & m, tactic * t, params_ref const & p, bool produce_proofs, bool produce_models, bool produce_unsat_cores, symbol const & logic);
virtual ~tactic2solver();
virtual solver* translate(ast_manager& m, params_ref const& p);
virtual void updt_params(params_ref const & p);
virtual void collect_param_descrs(param_descrs & r);
@ -183,6 +186,22 @@ void tactic2solver::set_cancel(bool f) {
}
}
solver* tactic2solver::translate(ast_manager& m, params_ref const& p) {
tactic* t = m_tactic->translate(m);
tactic2solver* r = alloc(tactic2solver, m, t, p, m_produce_proofs, m_produce_models, m_produce_unsat_cores, m_logic);
r->m_result = 0;
if (!m_scopes.empty()) {
throw default_exception("translation of contexts is only supported at base level");
}
ast_translation tr(m_assertions.get_manager(), m, false);
for (unsigned i = 0; i < get_num_assertions(); ++i) {
r->m_assertions.push_back(tr(get_assertion(i)));
}
return r;
}
void tactic2solver::collect_statistics(statistics & st) const {
st.copy(m_stats);
//SASSERT(m_stats.size() > 0);