mirror of
https://github.com/Z3Prover/z3
synced 2025-04-06 09:34:08 +00:00
removing last refs to assertion_set
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
parent
96676efeb6
commit
4f6b34bc7b
|
@ -53,7 +53,7 @@ add_lib('grobner', ['ast'], 'math/grobner')
|
|||
add_lib('euclid', ['util'], 'math/euclid')
|
||||
add_lib('proof_checker', ['rewriter', 'spc'], 'ast/proof_checker')
|
||||
add_lib('bit_blaster', ['rewriter', 'simplifier', 'old_params', 'tactic'], 'tactic/bit_blaster')
|
||||
add_lib('smt', ['assertion_set', 'bit_blaster', 'macros', 'normal_forms', 'cmd_context',
|
||||
add_lib('smt', ['bit_blaster', 'macros', 'normal_forms', 'cmd_context',
|
||||
'substitution', 'grobner', 'euclid', 'proof_checker', 'pattern', 'parser_util'])
|
||||
add_lib('user_plugin', ['smt'], 'smt/user_plugin')
|
||||
add_lib('core_tactics', ['tactic', 'normal_forms'], 'tactic/core_tactics')
|
||||
|
|
|
@ -1,7 +1,6 @@
|
|||
|
||||
|
||||
#include"arith_bounds_tactic.h"
|
||||
#include"assertion_set_util.h"
|
||||
#include"arith_decl_plugin.h"
|
||||
|
||||
struct arith_bounds_tactic : public tactic {
|
||||
|
|
|
@ -22,7 +22,7 @@ Revision History:
|
|||
#include <sstream>
|
||||
#include"ast_pp.h"
|
||||
#include"dl_mk_coi_filter.h"
|
||||
#include"elim_var_model_converter.h"
|
||||
#include"extension_model_converter.h"
|
||||
|
||||
namespace datalog {
|
||||
|
||||
|
@ -93,7 +93,7 @@ namespace datalog {
|
|||
if (res && mc) {
|
||||
decl_set::iterator end = pruned_preds.end();
|
||||
decl_set::iterator it = pruned_preds.begin();
|
||||
elim_var_model_converter* mc0 = alloc(elim_var_model_converter, m);
|
||||
extension_model_converter* mc0 = alloc(extension_model_converter, m);
|
||||
for (; it != end; ++it) {
|
||||
mc0->insert(*it, m.mk_true());
|
||||
}
|
||||
|
|
|
@ -1,182 +0,0 @@
|
|||
/*++
|
||||
Copyright (c) 2012 Microsoft Corporation
|
||||
|
||||
Module Name:
|
||||
|
||||
smt_solver_strategy.cpp
|
||||
|
||||
Abstract:
|
||||
|
||||
Wraps a solver as an assertion_set strategy.
|
||||
**Temporary code**
|
||||
It should be deleted when we finish porting the assertion_set code to the tactic framework.
|
||||
|
||||
Author:
|
||||
|
||||
Leonardo (leonardo) 2012-10-20
|
||||
|
||||
Notes:
|
||||
|
||||
--*/
|
||||
#include"smt_solver_strategy.h"
|
||||
#include"smt_solver.h"
|
||||
#include"front_end_params.h"
|
||||
#include"params2front_end_params.h"
|
||||
|
||||
class as_st_solver : public assertion_set_strategy {
|
||||
scoped_ptr<front_end_params> m_params;
|
||||
params_ref m_params_ref;
|
||||
statistics m_stats;
|
||||
std::string m_failure;
|
||||
smt::solver * m_ctx;
|
||||
bool m_candidate_models;
|
||||
symbol m_logic;
|
||||
progress_callback * m_callback;
|
||||
public:
|
||||
as_st_solver(bool candidate_models):m_ctx(0), m_candidate_models(candidate_models), m_callback(0) {}
|
||||
|
||||
front_end_params & fparams() {
|
||||
if (!m_params)
|
||||
m_params = alloc(front_end_params);
|
||||
return *m_params;
|
||||
}
|
||||
|
||||
struct scoped_init_ctx {
|
||||
as_st_solver & m_owner;
|
||||
|
||||
scoped_init_ctx(as_st_solver & o, ast_manager & m):m_owner(o) {
|
||||
smt::solver * new_ctx = alloc(smt::solver, m, o.fparams());
|
||||
TRACE("as_solver", tout << "logic: " << o.m_logic << "\n";);
|
||||
new_ctx->set_logic(o.m_logic);
|
||||
if (o.m_callback) {
|
||||
new_ctx->set_progress_callback(o.m_callback);
|
||||
}
|
||||
#pragma omp critical (as_st_solver)
|
||||
{
|
||||
o.m_ctx = new_ctx;
|
||||
}
|
||||
}
|
||||
|
||||
~scoped_init_ctx() {
|
||||
smt::solver * d = m_owner.m_ctx;
|
||||
#pragma omp critical (as_st_cancel)
|
||||
{
|
||||
m_owner.m_ctx = 0;
|
||||
}
|
||||
if (d)
|
||||
dealloc(d);
|
||||
}
|
||||
};
|
||||
|
||||
virtual ~as_st_solver() {
|
||||
SASSERT(m_ctx == 0);
|
||||
}
|
||||
|
||||
virtual void updt_params(params_ref const & p) {
|
||||
TRACE("as_solver", tout << "updt_params: " << p << "\n";);
|
||||
m_params_ref = p;
|
||||
params2front_end_params(m_params_ref, fparams());
|
||||
}
|
||||
|
||||
virtual void collect_param_descrs(param_descrs & r) {
|
||||
}
|
||||
|
||||
virtual void set_cancel(bool f) {
|
||||
if (m_ctx)
|
||||
m_ctx->set_cancel(f);
|
||||
}
|
||||
|
||||
virtual void operator()(assertion_set & s, model_converter_ref & mc) {
|
||||
SASSERT(is_well_sorted(s));
|
||||
IF_VERBOSE(ST_VERBOSITY_LVL, verbose_stream() << "(smt-solver)" << std::endl;);
|
||||
TRACE("as_solver", tout << "AUTO_CONFIG: " << fparams().m_auto_config << " HIDIV0: " << fparams().m_hi_div0 << " "
|
||||
<< " PREPROCESS: " << fparams().m_preprocess << ", SOLVER:" << fparams().m_solver << "\n";);
|
||||
TRACE("as_solver_detail", s.display(tout););
|
||||
ast_manager & m = s.m();
|
||||
TRACE("as_solver_memory", tout << "wasted_size: " << m.get_allocator().get_wasted_size() << "\n";);
|
||||
// verbose_stream() << "wasted_size: " << m.get_allocator().get_wasted_size() << ", free_objs: " << m.get_allocator().get_num_free_objs() << "\n";
|
||||
// m.get_allocator().consolidate();
|
||||
scoped_init_ctx init(*this, m);
|
||||
SASSERT(m_ctx != 0);
|
||||
unsigned sz = s.size();
|
||||
for (unsigned i = 0; i < sz; i++) {
|
||||
expr * f = s.form(i);
|
||||
m_ctx->assert_expr(f);
|
||||
}
|
||||
lbool r = m_ctx->setup_and_check();
|
||||
m_ctx->collect_statistics(m_stats);
|
||||
switch (r) {
|
||||
case l_true: {
|
||||
// the empty assertion set is trivially satifiable.
|
||||
s.reset();
|
||||
// store the model in a do nothin model converter.
|
||||
model_ref md;
|
||||
m_ctx->get_model(md);
|
||||
mc = model2model_converter(md.get());
|
||||
return;
|
||||
}
|
||||
case l_false:
|
||||
// formula is unsat, reset the assertion set, and store false there.
|
||||
s.reset();
|
||||
s.assert_expr(m.mk_false(), m_ctx->get_proof());
|
||||
return;
|
||||
case l_undef:
|
||||
if (m_candidate_models) {
|
||||
switch (m_ctx->last_failure()) {
|
||||
case smt::NUM_CONFLICTS:
|
||||
case smt::THEORY:
|
||||
case smt::QUANTIFIERS: {
|
||||
model_ref md;
|
||||
m_ctx->get_model(md);
|
||||
mc = model2model_converter(md.get());
|
||||
return;
|
||||
}
|
||||
default:
|
||||
break;
|
||||
}
|
||||
}
|
||||
m_failure = m_ctx->last_failure_as_string();
|
||||
throw strategy_exception(m_failure.c_str());
|
||||
}
|
||||
}
|
||||
|
||||
virtual void collect_statistics(statistics & st) const {
|
||||
if (m_ctx)
|
||||
m_ctx->collect_statistics(st); // ctx is still running...
|
||||
else
|
||||
st.copy(m_stats);
|
||||
}
|
||||
|
||||
virtual void cleanup() {
|
||||
}
|
||||
|
||||
virtual void reset_statistics() {
|
||||
m_stats.reset();
|
||||
}
|
||||
|
||||
// for backward compatibility
|
||||
virtual void set_front_end_params(front_end_params & p) {
|
||||
m_params = alloc(front_end_params, p);
|
||||
// must propagate the params_ref to fparams
|
||||
params2front_end_params(m_params_ref, fparams());
|
||||
}
|
||||
|
||||
virtual void set_logic(symbol const & l) {
|
||||
m_logic = l;
|
||||
}
|
||||
|
||||
virtual void set_progress_callback(progress_callback * callback) {
|
||||
m_callback = callback;
|
||||
}
|
||||
};
|
||||
|
||||
as_st * mk_smt_solver_core(bool candidate_models) {
|
||||
return alloc(as_st_solver, candidate_models);
|
||||
}
|
||||
|
||||
as_st * mk_smt_solver(bool auto_config, bool candidate_models) {
|
||||
as_st * solver = mk_smt_solver_core(candidate_models);
|
||||
params_ref solver_p;
|
||||
solver_p.set_bool(":auto-config", auto_config);
|
||||
return using_params(solver, solver_p);
|
||||
};
|
|
@ -1,31 +0,0 @@
|
|||
/*++
|
||||
Copyright (c) 2012 Microsoft Corporation
|
||||
|
||||
Module Name:
|
||||
|
||||
smt_solver_strategy.h
|
||||
|
||||
Abstract:
|
||||
|
||||
Wraps a solver as an assertion_set strategy.
|
||||
**Temporary code**
|
||||
It should be deleted when we finish porting the assertion_set code to the tactic framework.
|
||||
|
||||
Author:
|
||||
|
||||
Leonardo (leonardo) 2012-10-20
|
||||
|
||||
Notes:
|
||||
|
||||
--*/
|
||||
#ifndef _SMT_SOLVER_STRATEGY_H_
|
||||
#define _SMT_SOLVER_STRATEGY_H_
|
||||
|
||||
#include"assertion_set_strategy.h"
|
||||
|
||||
as_st * mk_smt_solver_core(bool candidate_models = false);
|
||||
as_st * mk_smt_solver(bool auto_config = true, bool candidate_models = false);
|
||||
|
||||
MK_SIMPLE_ST_FACTORY(smt_solver_stf, mk_smt_solver());
|
||||
|
||||
#endif
|
|
@ -28,8 +28,8 @@ Notes:
|
|||
#include"macro_manager.h"
|
||||
#include"macro_finder.h"
|
||||
#include"quasi_macros.h"
|
||||
#include"elim_var_model_converter.h"
|
||||
#include"ufbv_rewriter.h"
|
||||
#include"extension_model_converter.h"
|
||||
#include"distribute_forall_tactic.h"
|
||||
#include"der_tactic.h"
|
||||
#include"reduce_args_tactic.h"
|
||||
|
@ -97,7 +97,7 @@ class macro_finder_tactic : public tactic {
|
|||
for (; i < new_forms.size(); i++)
|
||||
g->assert_expr(new_forms.get(i), new_proofs.get(i), 0);
|
||||
|
||||
elim_var_model_converter * evmc = alloc(elim_var_model_converter, mm.get_manager());
|
||||
extension_model_converter * evmc = alloc(extension_model_converter, mm.get_manager());
|
||||
unsigned num = mm.get_num_macros();
|
||||
for (unsigned i = 0; i < num; i++) {
|
||||
expr_ref f_interp(mm.get_manager());
|
||||
|
@ -377,7 +377,7 @@ class quasi_macros_tactic : public tactic {
|
|||
for (; i < new_forms.size(); i++)
|
||||
g->assert_expr(new_forms.get(i), new_proofs.get(i), 0);
|
||||
|
||||
elim_var_model_converter * evmc = alloc(elim_var_model_converter, mm.get_manager());
|
||||
extension_model_converter * evmc = alloc(extension_model_converter, mm.get_manager());
|
||||
unsigned num = mm.get_num_macros();
|
||||
for (unsigned i = 0; i < num; i++) {
|
||||
expr_ref f_interp(mm.get_manager());
|
||||
|
|
Loading…
Reference in a new issue