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

checkpoint

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2012-11-01 21:44:35 -07:00
parent adb6d05805
commit cadd35bf7a
38 changed files with 185 additions and 177 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

16
src/api/api_context.cpp
View file

@ -333,28 +333,28 @@ namespace api {
//
// ------------------------
smt::solver & context::get_solver() {
smt::kernel & context::get_smt_kernel() {
if (!m_solver) {
m_solver = alloc(smt::solver, m_manager, m_params);
m_solver = alloc(smt::kernel, m_manager, m_params);
}
return *m_solver;
}
void context::assert_cnstr(expr * a) {
get_solver().assert_expr(a);
get_smt_kernel().assert_expr(a);
}
lbool context::check(model_ref & m) {
flet<bool> searching(m_searching, true);
lbool r;
r = get_solver().check();
r = get_smt_kernel().check();
if (r != l_false)
get_solver().get_model(m);
get_smt_kernel().get_model(m);
return r;
}
void context::push() {
get_solver().push();
get_smt_kernel().push();
if (!m_user_ref_count) {
m_ast_lim.push_back(m_ast_trail.size());
m_replay_stack.push_back(0);
@ -373,7 +373,7 @@ namespace api {
}
}
}
get_solver().pop(num_scopes);
get_smt_kernel().pop(num_scopes);
}
// ------------------------
@ -476,7 +476,7 @@ extern "C" {
Z3_TRY;
LOG_Z3_set_logic(c, logic);
RESET_ERROR_CODE();
return mk_c(c)->get_solver().set_logic(symbol(logic));
return mk_c(c)->get_smt_kernel().set_logic(symbol(logic));
Z3_CATCH_RETURN(Z3_FALSE);
}

6
src/api/api_context.h
View file

@ -27,7 +27,7 @@ Revision History:
#include"bv_decl_plugin.h"
#include"datatype_decl_plugin.h"
#include"dl_decl_plugin.h"
#include"smt_solver.h"
#include"smt_kernel.h"
#include"front_end_params.h"
#include"event_handler.h"
#include"tactic_manager.h"
@ -62,7 +62,7 @@ namespace api {
bv_util m_bv_util;
datalog::dl_decl_util m_datalog_util;
smt::solver * m_solver; // General purpose solver for backward compatibility
smt::kernel * m_solver; // General purpose solver for backward compatibility
ast_ref_vector m_last_result; //!< used when m_user_ref_count == true
ast_ref_vector m_ast_trail; //!< used when m_user_ref_count == false
@ -175,7 +175,7 @@ namespace api {
// ------------------------
bool has_solver() const { return m_solver != 0; }
smt::solver & get_solver();
smt::kernel & get_smt_kernel();
void assert_cnstr(expr * a);
lbool check(model_ref & m);
void push();

2
src/api/api_datalog.h
View file

@ -24,7 +24,7 @@ Revision History:
#include"front_end_params.h"
#include"dl_external_relation.h"
#include"dl_decl_plugin.h"
#include"smt_solver.h"
#include"smt_kernel.h"
#include"api_util.h"
#include"dl_context.h"

2
src/api/api_parsers.cpp
View file

@ -253,7 +253,7 @@ extern "C" {
class z3_context_solver : public solver {
api::context & m_ctx;
smt::solver & ctx() const { return m_ctx.get_solver(); }
smt::kernel & ctx() const { return m_ctx.get_smt_kernel(); }
public:
virtual ~z3_context_solver() {}
z3_context_solver(api::context& c) : m_ctx(c) {}

38
src/api/api_solver_old.cpp
View file

@ -41,7 +41,7 @@ extern "C" {
LOG_Z3_pop(c, num_scopes);
RESET_ERROR_CODE();
CHECK_SEARCHING(c);
if (num_scopes > mk_c(c)->get_solver().get_scope_level()) {
if (num_scopes > mk_c(c)->get_smt_kernel().get_scope_level()) {
SET_ERROR_CODE(Z3_IOB);
return;
}
@ -73,7 +73,7 @@ extern "C" {
LOG_Z3_check_and_get_model(c, m);
RESET_ERROR_CODE();
CHECK_SEARCHING(c);
cancel_eh<smt::solver> eh(mk_c(c)->get_solver());
cancel_eh<smt::kernel> eh(mk_c(c)->get_smt_kernel());
api::context::set_interruptable(*(mk_c(c)), eh);
flet<bool> _model(mk_c(c)->fparams().m_model, true);
lbool result;
@ -120,7 +120,7 @@ extern "C" {
LOG_Z3_get_implied_equalities(c, num_terms, terms, class_ids);
RESET_ERROR_CODE();
CHECK_SEARCHING(c);
lbool result = smt::implied_equalities(mk_c(c)->get_solver(), num_terms, to_exprs(terms), class_ids);
lbool result = smt::implied_equalities(mk_c(c)->get_smt_kernel(), num_terms, to_exprs(terms), class_ids);
return static_cast<Z3_lbool>(result);
Z3_CATCH_RETURN(Z3_L_UNDEF);
}
@ -136,13 +136,13 @@ extern "C" {
CHECK_SEARCHING(c);
expr * const* _assumptions = to_exprs(assumptions);
flet<bool> _model(mk_c(c)->fparams().m_model, true);
cancel_eh<smt::solver> eh(mk_c(c)->get_solver());
cancel_eh<smt::kernel> eh(mk_c(c)->get_smt_kernel());
api::context::set_interruptable(*(mk_c(c)), eh);
lbool result;
result = mk_c(c)->get_solver().check(num_assumptions, _assumptions);
result = mk_c(c)->get_smt_kernel().check(num_assumptions, _assumptions);
if (result != l_false && m) {
model_ref _m;
mk_c(c)->get_solver().get_model(_m);
mk_c(c)->get_smt_kernel().get_model(_m);
if (_m) {
Z3_model_ref * m_ref = alloc(Z3_model_ref);
m_ref->m_model = _m;
@ -156,19 +156,19 @@ extern "C" {
}
}
if (result == l_false && core_size) {
*core_size = mk_c(c)->get_solver().get_unsat_core_size();
*core_size = mk_c(c)->get_smt_kernel().get_unsat_core_size();
if (*core_size > num_assumptions) {
SET_ERROR_CODE(Z3_INVALID_ARG);
}
for (unsigned i = 0; i < *core_size; ++i) {
core[i] = of_ast(mk_c(c)->get_solver().get_unsat_core_expr(i));
core[i] = of_ast(mk_c(c)->get_smt_kernel().get_unsat_core_expr(i));
}
}
else if (core_size) {
*core_size = 0;
}
if (result == l_false && proof) {
*proof = of_ast(mk_c(c)->get_solver().get_proof());
*proof = of_ast(mk_c(c)->get_smt_kernel().get_proof());
}
else if (proof) {
*proof = 0; // breaks abstraction.
@ -182,7 +182,7 @@ extern "C" {
LOG_Z3_get_search_failure(c);
RESET_ERROR_CODE();
CHECK_SEARCHING(c);
smt::failure f = mk_c(c)->get_solver().last_failure();
smt::failure f = mk_c(c)->get_smt_kernel().last_failure();
return api::mk_Z3_search_failure(f);
Z3_CATCH_RETURN(Z3_UNKNOWN);
}
@ -209,8 +209,8 @@ extern "C" {
buffer<symbol> labl_syms;
ast_manager& m = mk_c(c)->m();
expr_ref_vector lits(m);
mk_c(c)->get_solver().get_relevant_labels(0, labl_syms);
mk_c(c)->get_solver().get_relevant_labeled_literals(mk_c(c)->fparams().m_at_labels_cex, lits);
mk_c(c)->get_smt_kernel().get_relevant_labels(0, labl_syms);
mk_c(c)->get_smt_kernel().get_relevant_labeled_literals(mk_c(c)->fparams().m_at_labels_cex, lits);
labels* lbls = alloc(labels);
SASSERT(labl_syms.size() == lits.size());
for (unsigned i = 0; i < lits.size(); ++i) {
@ -226,7 +226,7 @@ extern "C" {
RESET_ERROR_CODE();
ast_manager& m = mk_c(c)->m();
expr_ref_vector lits(m);
mk_c(c)->get_solver().get_relevant_literals(lits);
mk_c(c)->get_smt_kernel().get_relevant_literals(lits);
labels* lbls = alloc(labels);
for (unsigned i = 0; i < lits.size(); ++i) {
lbls->push_back(labeled_literal(m,lits[i].get()));
@ -241,7 +241,7 @@ extern "C" {
RESET_ERROR_CODE();
ast_manager& m = mk_c(c)->m();
expr_ref_vector lits(m);
mk_c(c)->get_solver().get_guessed_literals(lits);
mk_c(c)->get_smt_kernel().get_guessed_literals(lits);
labels* lbls = alloc(labels);
for (unsigned i = 0; i < lits.size(); ++i) {
lbls->push_back(labeled_literal(m,lits[i].get()));
@ -316,7 +316,7 @@ extern "C" {
LOG_Z3_context_to_string(c);
RESET_ERROR_CODE();
std::ostringstream buffer;
mk_c(c)->get_solver().display(buffer);
mk_c(c)->get_smt_kernel().display(buffer);
return mk_c(c)->mk_external_string(buffer.str());
Z3_CATCH_RETURN(0);
}
@ -328,7 +328,7 @@ extern "C" {
ast_manager& m = mk_c(c)->m();
expr_ref result(m);
expr_ref_vector assignment(m);
mk_c(c)->get_solver().get_assignments(assignment);
mk_c(c)->get_smt_kernel().get_assignments(assignment);
result = mk_c(c)->mk_and(assignment.size(), assignment.c_ptr());
RETURN_Z3(of_ast(result.get()));
Z3_CATCH_RETURN(0);
@ -339,7 +339,7 @@ extern "C" {
LOG_Z3_statistics_to_string(c);
RESET_ERROR_CODE();
std::ostringstream buffer;
mk_c(c)->get_solver().display_statistics(buffer);
mk_c(c)->get_smt_kernel().display_statistics(buffer);
memory::display_max_usage(buffer);
return mk_c(c)->mk_external_string(buffer.str());
Z3_CATCH_RETURN(0);
@ -356,10 +356,10 @@ extern "C" {
};
void Z3_display_statistics(Z3_context c, std::ostream& s) {
mk_c(c)->get_solver().display_statistics(s);
mk_c(c)->get_smt_kernel().display_statistics(s);
}
void Z3_display_istatistics(Z3_context c, std::ostream& s) {
mk_c(c)->get_solver().display_istatistics(s);
mk_c(c)->get_smt_kernel().display_istatistics(s);
}

4
src/api/api_user_theory.cpp
View file

@ -35,11 +35,11 @@ extern "C" {
Z3_theory Z3_mk_theory(Z3_context c, Z3_string th_name, void * ext_data) {
Z3_TRY;
RESET_ERROR_CODE();
if (mk_c(c)->get_solver().get_scope_level() > 0) {
if (mk_c(c)->get_smt_kernel().get_scope_level() > 0) {
SET_ERROR_CODE(Z3_INVALID_USAGE);
return 0;
}
return reinterpret_cast<Z3_theory>(mk_user_theory(mk_c(c)->get_solver(), c, ext_data, th_name));
return reinterpret_cast<Z3_theory>(mk_user_theory(mk_c(c)->get_smt_kernel(), c, ext_data, th_name));
Z3_CATCH_RETURN(0);
}

2
src/muz_qe/dl_bmc_engine.cpp
View file

@ -21,7 +21,7 @@ Revision History:
#include "dl_rule_transformer.h"
#include "dl_bmc_engine.h"
#include "dl_mk_slice.h"
#include "smt_solver.h"
#include "smt_kernel.h"
#include "datatype_decl_plugin.h"
#include "dl_mk_rule_inliner.h"
#include "dl_decl_plugin.h"

4
src/muz_qe/dl_bmc_engine.h
View file

@ -22,7 +22,7 @@ Revision History:
#include "params.h"
#include "statistics.h"
#include "smt_solver.h"
#include "smt_kernel.h"
#include "bv_decl_plugin.h"
@ -33,7 +33,7 @@ namespace datalog {
context& m_ctx;
ast_manager& m;
front_end_params m_fparams;
smt::solver m_solver;
smt::kernel m_solver;
obj_map<func_decl, sort*> m_pred2sort;
obj_map<sort, func_decl*> m_sort2pred;
obj_map<func_decl, func_decl*> m_pred2newpred;

8
src/muz_qe/dl_smt_relation.cpp
View file

@ -23,7 +23,7 @@ Revision History:
#include "dl_context.h"
#include "dl_smt_relation.h"
#include "expr_abstract.h"
#include "smt_solver.h"
#include "smt_kernel.h"
#include "th_rewriter.h"
#include "qe.h"
#include "datatype_decl_plugin.h"
@ -131,7 +131,7 @@ namespace datalog {
front_end_params& params = get_plugin().get_fparams();
flet<bool> flet2(params.m_der, true);
smt::solver ctx(m, params);
smt::kernel ctx(m, params);
expr_ref tmp(m);
instantiate(r, tmp);
ctx.assert_expr(tmp);
@ -184,7 +184,7 @@ namespace datalog {
flet<bool> flet0(params.m_quant_elim, true);
flet<bool> flet1(params.m_nnf_cnf, false);
flet<bool> flet2(params.m_der, true);
smt::solver ctx(m, params);
smt::kernel ctx(m, params);
ctx.assert_expr(fml_inst);
lbool result = ctx.check();
TRACE("smt_relation",
@ -242,7 +242,7 @@ namespace datalog {
eqs.resize(num_vars);
instantiate(r, tmp);
flet<bool> flet4(params.m_model, true);
smt::solver ctx(m, params);
smt::kernel ctx(m, params);
ctx.assert_expr(tmp);
while (true) {

2
src/muz_qe/pdr_context.cpp
View file

@ -1866,7 +1866,7 @@ namespace pdr {
}
bool context::check_invariant(unsigned lvl, func_decl* fn) {
smt::solver ctx(m, m_fparams);
smt::kernel ctx(m, m_fparams);
pred_transformer& pt = *m_rels.find(fn);
expr_ref_vector conj(m);
expr_ref inv = pt.get_formulas(next_level(lvl), false);

4
src/muz_qe/pdr_farkas_learner.cpp
View file

@ -251,7 +251,7 @@ namespace pdr {
o2p(outer_mgr, m_pr)
{
reg_decl_plugins(m_pr);
m_ctx = alloc(smt::solver, m_pr, m_proof_params);
m_ctx = alloc(smt::kernel, m_pr, m_proof_params);
}
front_end_params farkas_learner::get_proof_params(front_end_params& orig_params) {
@ -325,7 +325,7 @@ namespace pdr {
if (!m_ctx) {
m_ctx = alloc(smt::solver, m_pr, m_proof_params);
m_ctx = alloc(smt::kernel, m_pr, m_proof_params);
}
m_ctx->push();

4
src/muz_qe/pdr_farkas_learner.h
View file

@ -23,7 +23,7 @@ Revision History:
#include "arith_decl_plugin.h"
#include "ast_translation.h"
#include "bv_decl_plugin.h"
#include "smt_solver.h"
#include "smt_kernel.h"
#include "bool_rewriter.h"
#include "pdr_util.h"
#include "front_end_params.h"
@ -41,7 +41,7 @@ class farkas_learner {
front_end_params m_proof_params;
ast_manager m_pr;
scoped_ptr<smt::solver> m_ctx;
scoped_ptr<smt::kernel> m_ctx;
static front_end_params get_proof_params(front_end_params& orig_params);

2
src/muz_qe/pdr_generalizers.cpp
View file

@ -463,7 +463,7 @@ namespace pdr {
imp imp(m_ctx);
ast_manager& m = core.get_manager();
expr_ref goal = imp.mk_induction_goal(p->pt(), p->level(), depth);
smt::solver ctx(m, m_ctx.get_fparams(), m_ctx.get_params());
smt::kernel ctx(m, m_ctx.get_fparams(), m_ctx.get_params());
ctx.assert_expr(goal);
lbool r = ctx.check();
TRACE("pdr", tout << r << "\n";

2
src/muz_qe/pdr_manager.cpp
View file

@ -329,7 +329,7 @@ namespace pdr {
bool manager::implication_surely_holds(expr * lhs, expr * rhs, expr * bg) {
smt::solver sctx(m, get_fparams());
smt::kernel sctx(m, get_fparams());
if(bg) {
sctx.assert_expr(bg);
}

2
src/muz_qe/pdr_manager.h
View file

@ -28,7 +28,7 @@ Revision History:
#include "expr_substitution.h"
#include "map.h"
#include "ref_vector.h"
#include "smt_solver.h"
#include "smt_kernel.h"
#include "pdr_util.h"
#include "pdr_sym_mux.h"
#include "pdr_farkas_learner.h"

2
src/muz_qe/pdr_prop_solver.h
View file

@ -25,7 +25,7 @@ Revision History:
#include <utility>
#include "ast.h"
#include "obj_hashtable.h"
#include "smt_solver.h"
#include "smt_kernel.h"
#include "util.h"
#include "vector.h"
#include "pdr_manager.h"

4
src/muz_qe/pdr_quantifiers.cpp
View file

@ -152,7 +152,7 @@ namespace pdr {
bool found_instance = false;
expr_ref C(m);
front_end_params fparams;
smt::solver solver(m, fparams);
smt::kernel solver(m, fparams);
solver.assert_expr(m_A);
for (unsigned i = 0; i < m_Bs.size(); ++i) {
expr_ref_vector fresh_vars(m);
@ -344,7 +344,7 @@ namespace pdr {
for (unsigned i = 0; i < fmls.size(); ++i) {
tout << mk_pp(fmls[i].get(), mp) << "\n";
});
smt::solver solver(mp, fparams);
smt::kernel solver(mp, fparams);
for (unsigned i = 0; i < fmls.size(); ++i) {
solver.assert_expr(fmls[i].get());
}

10
src/muz_qe/pdr_smt_context_manager.cpp
View file

@ -52,7 +52,7 @@ namespace pdr {
}
_smt_context::_smt_context(smt::solver & ctx, smt_context_manager& p, app* pred):
_smt_context::_smt_context(smt::kernel & ctx, smt_context_manager& p, app* pred):
smt_context(p, ctx.m(), pred),
m_context(ctx)
{}
@ -104,21 +104,21 @@ namespace pdr {
smt_context_manager::~smt_context_manager() {
TRACE("pdr",tout << "\n";);
std::for_each(m_contexts.begin(), m_contexts.end(), delete_proc<smt::solver>());
std::for_each(m_contexts.begin(), m_contexts.end(), delete_proc<smt::kernel>());
}
smt_context* smt_context_manager::mk_fresh() {
++m_num_contexts;
app_ref pred(m);
smt::solver * ctx = 0;
smt::kernel * ctx = 0;
if (m_max_num_contexts == 0) {
m_contexts.push_back(alloc(smt::solver, m, m_fparams));
m_contexts.push_back(alloc(smt::kernel, m, m_fparams));
pred = m.mk_true();
ctx = m_contexts[m_num_contexts-1];
}
else {
if (m_contexts.size() < m_max_num_contexts) {
m_contexts.push_back(alloc(smt::solver, m, m_fparams));
m_contexts.push_back(alloc(smt::kernel, m, m_fparams));
}
std::stringstream name;
name << "#context" << m_num_contexts;

10
src/muz_qe/pdr_smt_context_manager.h
View file

@ -20,7 +20,7 @@ Revision History:
#ifndef _PDR_SMT_CONTEXT_MANAGER_H_
#define _PDR_SMT_CONTEXT_MANAGER_H_
#include "smt_solver.h"
#include "smt_kernel.h"
#include "sat_solver.h"
#include "func_decl_dependencies.h"
@ -56,9 +56,9 @@ namespace pdr {
};
class _smt_context : public smt_context {
smt::solver & m_context;
smt::kernel & m_context;
public:
_smt_context(smt::solver & ctx, smt_context_manager& p, app* pred);
_smt_context(smt::kernel & ctx, smt_context_manager& p, app* pred);
virtual ~_smt_context() {}
virtual void assert_expr(expr* e);
virtual lbool check(expr_ref_vector& assumptions);
@ -74,7 +74,7 @@ namespace pdr {
class sat_context : public smt_context {
sat::solver m_solver;
public:
sat_context(smt::solver & ctx, smt_context_manager& p, app* pred);
sat_context(smt::kernel & ctx, smt_context_manager& p, app* pred);
virtual ~sat_context() {}
virtual void assert_expr(expr* e);
virtual lbool check(expr_ref_vector& assumptions);
@ -91,7 +91,7 @@ namespace pdr {
front_end_params& m_fparams;
ast_manager& m;
unsigned m_max_num_contexts;
ptr_vector<smt::solver> m_contexts;
ptr_vector<smt::kernel> m_contexts;
unsigned m_num_contexts;
app_ref_vector m_predicate_list;
func_decl_set m_predicate_set;

4
src/muz_qe/qe.cpp
View file

@ -38,7 +38,7 @@ Revision History:
#include "bool_rewriter.h"
#include "dl_util.h"
#include "th_rewriter.h"
#include "smt_solver.h"
#include "smt_kernel.h"
#include "model_evaluator.h"
#include "has_free_vars.h"
#include "rewriter_def.h"
@ -1288,7 +1288,7 @@ namespace qe {
ast_manager& m;
quant_elim& m_qe;
th_rewriter m_rewriter;
smt::solver m_solver;
smt::kernel m_solver;
bv_util m_bv;
expr_ref_vector m_literals;

22
src/muz_qe/qe_sat_tactic.cpp
View file

@ -23,7 +23,7 @@ Revision History:
#include "qe_sat_tactic.h"
#include "quant_hoist.h"
#include "ast_pp.h"
#include "smt_solver.h"
#include "smt_kernel.h"
#include "qe.h"
#include "cooperate.h"
#include "model_v2_pp.h"
@ -66,8 +66,8 @@ namespace qe {
bool m_strong_context_simplify_param;
bool m_ctx_simplify_local_param;
vector<app_ref_vector> m_vars;
ptr_vector<smt::solver> m_solvers;
smt::solver m_solver;
ptr_vector<smt::kernel> m_solvers;
smt::kernel m_solver;
expr_ref m_fml;
expr_ref_vector m_Ms;
expr_ref_vector m_assignments;
@ -80,7 +80,7 @@ namespace qe {
ast_manager& m;
sat_tactic& m_super;
smt::solver& m_solver;
smt::kernel& m_solver;
atom_set m_pos;
atom_set m_neg;
app_ref_vector m_vars;
@ -322,10 +322,10 @@ namespace qe {
void init_Ms() {
for (unsigned i = 0; i < num_alternations(); ++i) {
m_Ms.push_back(m.mk_true());
m_solvers.push_back(alloc(smt::solver, m, m_fparams, m_params));
m_solvers.push_back(alloc(smt::kernel, m, m_fparams, m_params));
}
m_Ms.push_back(m_fml);
m_solvers.push_back(alloc(smt::solver, m, m_fparams, m_params));
m_solvers.push_back(alloc(smt::kernel, m, m_fparams, m_params));
m_solvers.back()->assert_expr(m_fml);
}
@ -333,7 +333,7 @@ namespace qe {
app_ref_vector const& vars(unsigned i) { return m_vars[i]; }
smt::solver& solver(unsigned i) { return *m_solvers[i]; }
smt::kernel& solver(unsigned i) { return *m_solvers[i]; }
void reset() {
m_fml = 0;
@ -468,7 +468,7 @@ namespace qe {
remove_duplicates(pos, neg);
// Assumption: B is already asserted in solver[i].
smt::solver& solver = *m_solvers[i];
smt::kernel& solver = *m_solvers[i];
solver.push();
solver.assert_expr(A);
nnf_strengthen(solver, pos, m.mk_false(), sub);
@ -506,7 +506,7 @@ namespace qe {
return Bnnf;
}
void nnf_strengthen(smt::solver& solver, atom_set& atoms, expr* value, expr_substitution& sub) {
void nnf_strengthen(smt::kernel& solver, atom_set& atoms, expr* value, expr_substitution& sub) {
atom_set::iterator it = atoms.begin(), end = atoms.end();
for (; it != end; ++it) {
solver.push();
@ -565,7 +565,7 @@ namespace qe {
return Bnnf;
}
void nnf_weaken(smt::solver& solver, expr_ref& B, atom_set& atoms, expr* value, expr_substitution& sub) {
void nnf_weaken(smt::kernel& solver, expr_ref& B, atom_set& atoms, expr* value, expr_substitution& sub) {
atom_set::iterator it = atoms.begin(), end = atoms.end();
for (; it != end; ++it) {
solver.push();
@ -678,7 +678,7 @@ namespace qe {
}
bool is_sat(unsigned i, expr* ctx, model_ref& model) {
smt::solver& solver = *m_solvers[i];
smt::kernel& solver = *m_solvers[i];
solver.push();
solver.assert_expr(ctx);
lbool r = solver.check();

10
src/smt/default_solver.cpp
View file

@ -7,7 +7,7 @@ Module Name:
Abstract:
Wrapps smt::solver as a solver for cmd_context
Wrapps smt::kernel as a solver for cmd_context
Author:
@ -17,13 +17,13 @@ Notes:
--*/
#include"solver.h"
#include"smt_solver.h"
#include"smt_kernel.h"
#include"reg_decl_plugins.h"
#include"front_end_params.h"
class default_solver : public solver {
front_end_params * m_params;
smt::solver * m_context;
smt::kernel * m_context;
public:
default_solver():m_params(0), m_context(0) {}
@ -47,7 +47,7 @@ public:
ast_manager m;
reg_decl_plugins(m);
front_end_params p;
smt::solver s(m, p);
smt::kernel s(m, p);
s.collect_param_descrs(r);
}
else {
@ -60,7 +60,7 @@ public:
reset();
#pragma omp critical (solver)
{
m_context = alloc(smt::solver, m, *m_params);
m_context = alloc(smt::kernel, m, *m_params);
}
if (logic != symbol::null)
m_context->set_logic(logic);

2
src/smt/default_solver.h
View file

@ -7,7 +7,7 @@ Module Name:
Abstract:
Wrapps smt::solver as a solver for cmd_context
Wrapps smt::kernel as a solver for cmd_context and external API
Author:

2
src/smt/expr_context_simplifier.cpp
View file

@ -20,7 +20,7 @@ Revision History:
#include "expr_context_simplifier.h"
#include "ast_pp.h"
#include "obj_hashtable.h"
#include "smt_solver.h"
#include "smt_kernel.h"
#include "for_each_expr.h"
// table lookup before/after simplification.

4
src/smt/expr_context_simplifier.h
View file

@ -23,7 +23,7 @@ Revision History:
#include "obj_hashtable.h"
#include "basic_simplifier_plugin.h"
#include "front_end_params.h"
#include "smt_solver.h"
#include "smt_kernel.h"
#include "arith_decl_plugin.h"
class expr_context_simplifier {
@ -61,7 +61,7 @@ class expr_strong_context_simplifier {
arith_util m_arith;
unsigned m_id;
func_decl_ref m_fn;
smt::solver m_solver;
smt::kernel m_solver;
void simplify(expr* e, expr_ref& result) { simplify_model_based(e, result); }
void simplify_basic(expr* fml, expr_ref& result);

10
src/smt/ni_solver.cpp
View file

@ -6,7 +6,7 @@ Module Name:
ni_solver.cpp
Abstract:
Wrappers for smt::solver that are non-incremental & (quasi-incremental).
Wrappers for smt::kernel that are non-incremental & (quasi-incremental).
Author:
@ -16,13 +16,13 @@ Notes:
--*/
#include"ni_solver.h"
#include"smt_solver.h"
#include"smt_kernel.h"
#include"cmd_context.h"
class ni_smt_solver : public solver {
protected:
cmd_context & m_cmd_ctx;
smt::solver * m_context;
smt::kernel * m_context;
progress_callback * m_callback;
public:
ni_smt_solver(cmd_context & ctx):m_cmd_ctx(ctx), m_context(0), m_callback(0) {}
@ -83,7 +83,7 @@ public:
reset();
#pragma omp critical (ni_solver)
{
m_context = alloc(smt::solver, m_cmd_ctx.m(), m_cmd_ctx.params());
m_context = alloc(smt::kernel, m_cmd_ctx.m(), m_cmd_ctx.params());
}
if (m_cmd_ctx.has_logic())
m_context->set_logic(m_cmd_ctx.get_logic());
@ -149,7 +149,7 @@ public:
virtual void collect_param_descrs(param_descrs & r) {
smt::solver::collect_param_descrs(r);
smt::kernel::collect_param_descrs(r);
}
};

6
src/smt/smt_implied_equalities.cpp
View file

@ -36,7 +36,7 @@ namespace smt {
class get_implied_equalities_impl {
ast_manager& m;
smt::solver& m_solver;
smt::kernel& m_solver;
union_find_default_ctx m_df;
union_find<union_find_default_ctx> m_uf;
array_util m_array_util;
@ -357,7 +357,7 @@ namespace smt {
public:
get_implied_equalities_impl(smt::solver& s) : m(s.m()), m_solver(s), m_uf(m_df), m_array_util(m), m_stats_calls(0) {}
get_implied_equalities_impl(smt::kernel& s) : m(s.m()), m_solver(s), m_uf(m_df), m_array_util(m), m_stats_calls(0) {}
lbool operator()(unsigned num_terms, expr* const* terms, unsigned* class_ids) {
params_ref p;
@ -410,7 +410,7 @@ namespace smt {
stopwatch get_implied_equalities_impl::s_timer;
stopwatch get_implied_equalities_impl::s_stats_val_eq_timer;
lbool implied_equalities(smt::solver& solver, unsigned num_terms, expr* const* terms, unsigned* class_ids) {
lbool implied_equalities(smt::kernel& solver, unsigned num_terms, expr* const* terms, unsigned* class_ids) {
get_implied_equalities_impl gi(solver);
return gi(num_terms, terms, class_ids);
}

4
src/smt/smt_implied_equalities.h
View file

@ -23,13 +23,13 @@ Revision History:
#ifndef __SMT_IMPLIED_EQUALITIES_H__
#define __SMT_IMPLIED_EQUALITIES_H__
#include"smt_solver.h"
#include"smt_kernel.h"
namespace smt {
lbool implied_equalities(
solver& solver,
kernel & solver,
unsigned num_terms, expr* const* terms,
unsigned* class_ids);

98
src/smt/smt_solver.cpp → src/smt/smt_kernel.cpp
View file

@ -3,11 +3,11 @@ Copyright (c) 2012 Microsoft Corporation
Module Name:
smt_solver.h
smt_kernel.cpp
Abstract:
New frontend for the incremental solver.
New frontend for smt::context.
Author:
@ -16,14 +16,14 @@ Author:
Revision History:
--*/
#include"smt_solver.h"
#include"smt_kernel.h"
#include"smt_context.h"
#include"ast_smt2_pp.h"
#include"params2front_end_params.h"
namespace smt {
struct solver::imp {
struct kernel::imp {
smt::context m_kernel;
params_ref m_params;
@ -53,7 +53,7 @@ namespace smt {
}
void assert_expr(expr * e) {
TRACE("smt_solver", tout << "assert:\n" << mk_ismt2_pp(e, m()) << "\n";);
TRACE("smt_kernel", tout << "assert:\n" << mk_ismt2_pp(e, m()) << "\n";);
m_kernel.assert_expr(e);
}
@ -74,12 +74,12 @@ namespace smt {
}
void push() {
TRACE("smt_solver", tout << "push()\n";);
TRACE("smt_kernel", tout << "push()\n";);
m_kernel.push();
}
void pop(unsigned num_scopes) {
TRACE("smt_solver", tout << "pop()\n";);
TRACE("smt_kernel", tout << "pop()\n";);
m_kernel.pop(num_scopes);
}
@ -148,7 +148,7 @@ namespace smt {
// TODO: it will be replaced with assertion_stack.display
unsigned num = m_kernel.get_num_asserted_formulas();
expr * const * fms = m_kernel.get_asserted_formulas();
out << "(solver";
out << "(kernel";
for (unsigned i = 0; i < num; i++) {
out << "\n " << mk_ismt2_pp(fms[i], m(), 2);
}
@ -183,170 +183,170 @@ namespace smt {
}
};
solver::solver(ast_manager & m, front_end_params & fp, params_ref const & p) {
kernel::kernel(ast_manager & m, front_end_params & fp, params_ref const & p) {
m_imp = alloc(imp, m, fp, p);
}
solver::~solver() {
kernel::~kernel() {
dealloc(m_imp);
}
ast_manager & solver::m() const {
ast_manager & kernel::m() const {
return m_imp->m();
}
bool solver::set_logic(symbol logic) {
bool kernel::set_logic(symbol logic) {
return m_imp->set_logic(logic);
}
void solver::set_progress_callback(progress_callback * callback) {
void kernel::set_progress_callback(progress_callback * callback) {
m_imp->set_progress_callback(callback);
}
void solver::assert_expr(expr * e) {
void kernel::assert_expr(expr * e) {
m_imp->assert_expr(e);
}
void solver::assert_expr(expr * e, proof * pr) {
void kernel::assert_expr(expr * e, proof * pr) {
m_imp->assert_expr(e, pr);
}
unsigned solver::size() const {
unsigned kernel::size() const {
return m_imp->size();
}
expr * const * solver::get_formulas() const {
expr * const * kernel::get_formulas() const {
return m_imp->get_formulas();
}
bool solver::reduce() {
bool kernel::reduce() {
return m_imp->reduce();
}
void solver::push() {
void kernel::push() {
m_imp->push();
}
void solver::pop(unsigned num_scopes) {
void kernel::pop(unsigned num_scopes) {
m_imp->pop(num_scopes);
}
unsigned solver::get_scope_level() const {
unsigned kernel::get_scope_level() const {
return m_imp->get_scope_level();
}
void solver::reset() {
void kernel::reset() {
ast_manager & _m = m();
front_end_params & fps = m_imp->fparams();
params_ref ps = m_imp->params();
#pragma omp critical (smt_solver)
#pragma omp critical (smt_kernel)
{
dealloc(m_imp);
m_imp = alloc(imp, _m, fps, ps);
}
}
bool solver::inconsistent() {
bool kernel::inconsistent() {
return m_imp->inconsistent();
}
lbool solver::setup_and_check() {
lbool kernel::setup_and_check() {
set_cancel(false);
return m_imp->setup_and_check();
}
lbool solver::check(unsigned num_assumptions, expr * const * assumptions) {
lbool kernel::check(unsigned num_assumptions, expr * const * assumptions) {
set_cancel(false);
lbool r = m_imp->check(num_assumptions, assumptions);
TRACE("smt_solver", tout << "check result: " << r << "\n";);
TRACE("smt_kernel", tout << "check result: " << r << "\n";);
return r;
}
void solver::get_model(model_ref & m) const {
void kernel::get_model(model_ref & m) const {
m_imp->get_model(m);
}
proof * solver::get_proof() {
proof * kernel::get_proof() {
return m_imp->get_proof();
}
unsigned solver::get_unsat_core_size() const {
unsigned kernel::get_unsat_core_size() const {
return m_imp->get_unsat_core_size();
}
expr * solver::get_unsat_core_expr(unsigned idx) const {
expr * kernel::get_unsat_core_expr(unsigned idx) const {
return m_imp->get_unsat_core_expr(idx);
}
failure solver::last_failure() const {
failure kernel::last_failure() const {
return m_imp->last_failure();
}
std::string solver::last_failure_as_string() const {
std::string kernel::last_failure_as_string() const {
return m_imp->last_failure_as_string();
}
void solver::get_assignments(expr_ref_vector & result) {
void kernel::get_assignments(expr_ref_vector & result) {
m_imp->get_assignments(result);
}
void solver::get_relevant_labels(expr * cnstr, buffer<symbol> & result) {
void kernel::get_relevant_labels(expr * cnstr, buffer<symbol> & result) {
m_imp->get_relevant_labels(cnstr, result);
}
void solver::get_relevant_labeled_literals(bool at_lbls, expr_ref_vector & result) {
void kernel::get_relevant_labeled_literals(bool at_lbls, expr_ref_vector & result) {
m_imp->get_relevant_labeled_literals(at_lbls, result);
}
void solver::get_relevant_literals(expr_ref_vector & result) {
void kernel::get_relevant_literals(expr_ref_vector & result) {
m_imp->get_relevant_literals(result);
}
void solver::get_guessed_literals(expr_ref_vector & result) {
void kernel::get_guessed_literals(expr_ref_vector & result) {
m_imp->get_guessed_literals(result);
}
void solver::display(std::ostream & out) const {
void kernel::display(std::ostream & out) const {
m_imp->display(out);
}
void solver::collect_statistics(::statistics & st) const {
void kernel::collect_statistics(::statistics & st) const {
m_imp->collect_statistics(st);
}
void solver::reset_statistics() {
void kernel::reset_statistics() {
m_imp->reset_statistics();
}
void solver::display_statistics(std::ostream & out) const {
void kernel::display_statistics(std::ostream & out) const {
m_imp->display_statistics(out);
}
void solver::display_istatistics(std::ostream & out) const {
void kernel::display_istatistics(std::ostream & out) const {
m_imp->display_istatistics(out);
}
void solver::set_cancel(bool f) {
#pragma omp critical (smt_solver)
void kernel::set_cancel(bool f) {
#pragma omp critical (smt_kernel)
{
if (m_imp)
m_imp->set_cancel(f);
}
}
bool solver::canceled() const {
bool kernel::canceled() const {
return m_imp->canceled();
}
void solver::updt_params(params_ref const & p) {
void kernel::updt_params(params_ref const & p) {
return m_imp->updt_params(p);
}
void solver::collect_param_descrs(param_descrs & d) {
void kernel::collect_param_descrs(param_descrs & d) {
solver_front_end_params_descrs(d);
}
context & solver::kernel() {
context & kernel::get_context() {
return m_imp->m_kernel;
}

42
src/smt/smt_solver.h → src/smt/smt_kernel.h
View file

@ -3,11 +3,13 @@ Copyright (c) 2012 Microsoft Corporation
Module Name:
smt_solver.h
smt_kernel.h
Abstract:
New frontend for the incremental solver.
New frontend for smt::context.
The "kernel" tries to hide details of the smt::context object.
From now on, clients (code outside of the smt module) should be use smt::kernel instead of smt::context.
Author:
@ -15,9 +17,15 @@ Author:
Revision History:
I initially called it smt::solver. This was confusing to others since we have the abstract solver API,
and smt::kernel is not a subclass of ::solver.
To increase the confusion I had a class default_solver that implemented the solver API on top of smt::context.
To avoid this problem I renamed them in the following way:
smt::solver ---> smt::kernel
default_solver ---> smt::solver
--*/
#ifndef _SMT_SOLVER_H_
#define _SMT_SOLVER_H_
#ifndef _SMT_KERNEL_H_
#define _SMT_KERNEL_H_
#include"ast.h"
#include"params.h"
@ -34,13 +42,13 @@ namespace smt {
class enode;
class context;
class solver {
class kernel {
struct imp;
imp * m_imp;
public:
solver(ast_manager & m, front_end_params & fp, params_ref const & p = params_ref());
kernel(ast_manager & m, front_end_params & fp, params_ref const & p = params_ref());
~solver();
~kernel();
ast_manager & m() const;
@ -51,7 +59,7 @@ namespace smt {
bool set_logic(symbol logic);
/**
brief Set progress meter. Solver will invoke the callback from time to time.
brief Set progress meter. Kernel will invoke the callback from time to time.
*/
void set_progress_callback(progress_callback * callback);
@ -67,7 +75,7 @@ namespace smt {
void assert_expr(expr * e, proof * pr);
/**
\brief Return the number of asserted formulas in the solver.
\brief Return the number of asserted formulas in the kernel.
*/
unsigned size() const;
@ -101,7 +109,7 @@ namespace smt {
unsigned get_scope_level() const;
/**
\brief Reset the solver.
\brief Reset the kernel.
All assertions are erased.
*/
void reset();
@ -155,7 +163,7 @@ namespace smt {
std::string last_failure_as_string() const;
/**
\brief Return the set of formulas assigned by the solver.
\brief Return the set of formulas assigned by the kernel.
*/
void get_assignments(expr_ref_vector & result);
@ -180,7 +188,7 @@ namespace smt {
void get_guessed_literals(expr_ref_vector & result);
/**
\brief (For debubbing purposes) Prints the state of the solver
\brief (For debubbing purposes) Prints the state of the kernel
*/
void display(std::ostream & out) const;
@ -190,7 +198,7 @@ namespace smt {
void collect_statistics(::statistics & st) const;
/**
\brief Reset solver statistics.
\brief Reset kernel statistics.
*/
void reset_statistics();
@ -205,7 +213,7 @@ namespace smt {
void display_istatistics(std::ostream & out) const;
/**
\brief Interrupt the solver.
\brief Interrupt the kernel.
*/
void set_cancel(bool f = true);
void cancel() { set_cancel(true); }
@ -216,7 +224,7 @@ namespace smt {
void reset_cancel() { set_cancel(false); }
/**
\brief Return true if the solver was interrupted.
\brief Return true if the kernel was interrupted.
*/
bool canceled() const;
@ -231,7 +239,7 @@ namespace smt {
static void collect_param_descrs(param_descrs & d);
/**
\brief Return a reference to the kernel.
\brief Return a reference to smt::context.
This is a temporary hack to support user theories.
TODO: remove this hack.
We need to revamp user theories too.
@ -240,7 +248,7 @@ namespace smt {
\warning We should not use this method
*/
context & kernel();
context & get_context();
};
};

2
src/smt/smt_model_checker.cpp
View file

@ -56,7 +56,7 @@ namespace smt {
SASSERT(m_qm == 0);
SASSERT(m_context == 0);
m_qm = &qm;
m_context = &(m_qm->kernel());
m_context = &(m_qm->get_context());
}
/**

4
src/smt/smt_quantifier.cpp
View file

@ -248,7 +248,7 @@ namespace smt {
dealloc(m_imp);
}
context & quantifier_manager::kernel() const {
context & quantifier_manager::get_context() const {
return m_imp->m_context;
}
@ -414,7 +414,7 @@ namespace smt {
virtual void set_manager(quantifier_manager & qm) {
SASSERT(m_qm == 0);
m_qm = &qm;
m_context = &(qm.kernel());
m_context = &(qm.get_context());
m_fparams = &(m_context->get_fparams());
ast_manager & m = m_context->get_manager();

2
src/smt/smt_quantifier.h
View file

@ -38,7 +38,7 @@ namespace smt {
quantifier_manager(context & ctx, front_end_params & fp, params_ref const & p);
~quantifier_manager();
context & kernel() const;
context & get_context() const;
void set_plugin(quantifier_manager_plugin * plugin);

4
src/smt/tactic/ctx_solver_simplify_tactic.cpp
View file

@ -20,7 +20,7 @@ Notes:
#include"ctx_solver_simplify_tactic.h"
#include"arith_decl_plugin.h"
#include"front_end_params.h"
#include"smt_solver.h"
#include"smt_kernel.h"
#include"ast_pp.h"
#include"mk_simplified_app.h"
@ -29,7 +29,7 @@ class ctx_solver_simplify_tactic : public tactic {
ast_manager& m;
params_ref m_params;
front_end_params m_front_p;
smt::solver m_solver;
smt::kernel m_solver;
arith_util m_arith;
mk_simplified_app m_mk_app;
func_decl_ref m_fn;

8
src/smt/tactic/smt_tactic.cpp
View file

@ -18,7 +18,7 @@ Notes:
--*/
#include"tactic.h"
#include"tactical.h"
#include"smt_solver.h"
#include"smt_kernel.h"
#include"front_end_params.h"
#include"params2front_end_params.h"
#include"rewriter_types.h"
@ -28,7 +28,7 @@ class smt_tactic : public tactic {
params_ref m_params_ref;
statistics m_stats;
std::string m_failure;
smt::solver * m_ctx;
smt::kernel * m_ctx;
symbol m_logic;
progress_callback * m_callback;
bool m_candidate_models;
@ -117,7 +117,7 @@ public:
smt_tactic & m_owner;
scoped_init_ctx(smt_tactic & o, ast_manager & m):m_owner(o) {
smt::solver * new_ctx = alloc(smt::solver, m, o.fparams());
smt::kernel * new_ctx = alloc(smt::kernel, m, o.fparams());
TRACE("smt_tactic", tout << "logic: " << o.m_logic << "\n";);
new_ctx->set_logic(o.m_logic);
if (o.m_callback) {
@ -130,7 +130,7 @@ public:
}
~scoped_init_ctx() {
smt::solver * d = m_owner.m_ctx;
smt::kernel * d = m_owner.m_ctx;
#pragma omp critical (as_st_cancel)
{
m_owner.m_ctx = 0;

4
src/smt/user_plugin/user_smt_theory.cpp
View file

@ -642,8 +642,8 @@ namespace smt {
out << "Theory " << get_name() << ":\n";
}
user_theory * mk_user_theory(solver & _s, void * ext_context, void * ext_data, char const * name) {
context & ctx = _s.kernel(); // HACK
user_theory * mk_user_theory(kernel & _s, void * ext_context, void * ext_data, char const * name) {
context & ctx = _s.get_context(); // HACK
symbol _name(name);
ast_manager & m = ctx.get_manager();
family_id fid = m.get_family_id(_name);

4
src/smt/user_plugin/user_smt_theory.h
View file

@ -23,7 +23,7 @@ Revision History:
#include"user_simplifier_plugin.h"
#include"smt_theory.h"
#include"union_find.h"
#include"smt_solver.h"
#include"smt_kernel.h"
namespace smt {
@ -316,7 +316,7 @@ namespace smt {
virtual void display(std::ostream & out) const;
};
user_theory * mk_user_theory(solver & s, void * ext_context, void * ext_data, char const * name);
user_theory * mk_user_theory(kernel & s, void * ext_context, void * ext_data, char const * name);
};

6
src/test/quant_solve.cpp
View file

@ -6,7 +6,7 @@
#include "lbool.h"
#include <sstream>
#include "expr_replacer.h"
#include "smt_solver.h"
#include "smt_kernel.h"
#include "reg_decl_plugins.h"
#include "expr_abstract.h"
#include "model_smt2_pp.h"
@ -29,7 +29,7 @@ static void validate_quant_solution(ast_manager& m, expr* fml, expr* guard, qe::
expr_ref tmp(m);
tmp = m.mk_not(m.mk_implies(guard, fml1));
front_end_params fp;
smt::solver solver(m, fp);
smt::kernel solver(m, fp);
solver.assert_expr(tmp);
lbool res = solver.check();
//SASSERT(res == l_false);
@ -64,7 +64,7 @@ static void validate_quant_solutions(app* x, expr* fml, expr_ref_vector& guards)
tmp = m.mk_not(m.mk_iff(fml2, tmp));
std::cout << mk_pp(tmp, m) << "\n";
front_end_params fp;
smt::solver solver(m, fp);
smt::kernel solver(m, fp);
solver.assert_expr(tmp);
lbool res = solver.check();
std::cout << "checked\n";