From cadd35bf7a76abf5afd62399c56d0a35d1aa0325 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Thu, 1 Nov 2012 21:44:35 -0700 Subject: [PATCH] checkpoint Signed-off-by: Leonardo de Moura --- src/api/api_context.cpp | 16 +-- src/api/api_context.h | 6 +- src/api/api_datalog.h | 2 +- src/api/api_parsers.cpp | 2 +- src/api/api_solver_old.cpp | 38 +++---- src/api/api_user_theory.cpp | 4 +- src/muz_qe/dl_bmc_engine.cpp | 2 +- src/muz_qe/dl_bmc_engine.h | 4 +- src/muz_qe/dl_smt_relation.cpp | 8 +- src/muz_qe/pdr_context.cpp | 2 +- src/muz_qe/pdr_farkas_learner.cpp | 4 +- src/muz_qe/pdr_farkas_learner.h | 4 +- src/muz_qe/pdr_generalizers.cpp | 2 +- src/muz_qe/pdr_manager.cpp | 2 +- src/muz_qe/pdr_manager.h | 2 +- src/muz_qe/pdr_prop_solver.h | 2 +- src/muz_qe/pdr_quantifiers.cpp | 4 +- src/muz_qe/pdr_smt_context_manager.cpp | 10 +- src/muz_qe/pdr_smt_context_manager.h | 10 +- src/muz_qe/qe.cpp | 4 +- src/muz_qe/qe_sat_tactic.cpp | 22 ++--- src/smt/default_solver.cpp | 10 +- src/smt/default_solver.h | 2 +- src/smt/expr_context_simplifier.cpp | 2 +- src/smt/expr_context_simplifier.h | 4 +- src/smt/ni_solver.cpp | 10 +- src/smt/smt_implied_equalities.cpp | 6 +- src/smt/smt_implied_equalities.h | 4 +- src/smt/{smt_solver.cpp => smt_kernel.cpp} | 98 +++++++++---------- src/smt/{smt_solver.h => smt_kernel.h} | 42 ++++---- src/smt/smt_model_checker.cpp | 2 +- src/smt/smt_quantifier.cpp | 4 +- src/smt/smt_quantifier.h | 2 +- src/smt/tactic/ctx_solver_simplify_tactic.cpp | 4 +- src/smt/tactic/smt_tactic.cpp | 8 +- src/smt/user_plugin/user_smt_theory.cpp | 4 +- src/smt/user_plugin/user_smt_theory.h | 4 +- src/test/quant_solve.cpp | 6 +- 38 files changed, 185 insertions(+), 177 deletions(-) rename src/smt/{smt_solver.cpp => smt_kernel.cpp} (74%) rename src/smt/{smt_solver.h => smt_kernel.h} (82%) diff --git a/src/api/api_context.cpp b/src/api/api_context.cpp index c80b55fd9..ba8d2ae64 100644 --- a/src/api/api_context.cpp +++ b/src/api/api_context.cpp @@ -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 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); } diff --git a/src/api/api_context.h b/src/api/api_context.h index 4bb0b6d18..3da506b54 100644 --- a/src/api/api_context.h +++ b/src/api/api_context.h @@ -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(); diff --git a/src/api/api_datalog.h b/src/api/api_datalog.h index fad44de87..1d6bb995a 100644 --- a/src/api/api_datalog.h +++ b/src/api/api_datalog.h @@ -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" diff --git a/src/api/api_parsers.cpp b/src/api/api_parsers.cpp index 0a76c710e..2d5c3d0c4 100644 --- a/src/api/api_parsers.cpp +++ b/src/api/api_parsers.cpp @@ -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) {} diff --git a/src/api/api_solver_old.cpp b/src/api/api_solver_old.cpp index bb083b7fc..cd4b797e3 100644 --- a/src/api/api_solver_old.cpp +++ b/src/api/api_solver_old.cpp @@ -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 eh(mk_c(c)->get_solver()); + cancel_eh eh(mk_c(c)->get_smt_kernel()); api::context::set_interruptable(*(mk_c(c)), eh); flet _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(result); Z3_CATCH_RETURN(Z3_L_UNDEF); } @@ -136,13 +136,13 @@ extern "C" { CHECK_SEARCHING(c); expr * const* _assumptions = to_exprs(assumptions); flet _model(mk_c(c)->fparams().m_model, true); - cancel_eh eh(mk_c(c)->get_solver()); + cancel_eh 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 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); } diff --git a/src/api/api_user_theory.cpp b/src/api/api_user_theory.cpp index bb0c582bf..fde34bbb2 100644 --- a/src/api/api_user_theory.cpp +++ b/src/api/api_user_theory.cpp @@ -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(mk_user_theory(mk_c(c)->get_solver(), c, ext_data, th_name)); + return reinterpret_cast(mk_user_theory(mk_c(c)->get_smt_kernel(), c, ext_data, th_name)); Z3_CATCH_RETURN(0); } diff --git a/src/muz_qe/dl_bmc_engine.cpp b/src/muz_qe/dl_bmc_engine.cpp index 8e0e3b9b7..91c2d72ee 100644 --- a/src/muz_qe/dl_bmc_engine.cpp +++ b/src/muz_qe/dl_bmc_engine.cpp @@ -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" diff --git a/src/muz_qe/dl_bmc_engine.h b/src/muz_qe/dl_bmc_engine.h index e0e8ff3da..b8bb2e1e0 100644 --- a/src/muz_qe/dl_bmc_engine.h +++ b/src/muz_qe/dl_bmc_engine.h @@ -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 m_pred2sort; obj_map m_sort2pred; obj_map m_pred2newpred; diff --git a/src/muz_qe/dl_smt_relation.cpp b/src/muz_qe/dl_smt_relation.cpp index 572894d05..381b8f434 100644 --- a/src/muz_qe/dl_smt_relation.cpp +++ b/src/muz_qe/dl_smt_relation.cpp @@ -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 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 flet0(params.m_quant_elim, true); flet flet1(params.m_nnf_cnf, false); flet 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 flet4(params.m_model, true); - smt::solver ctx(m, params); + smt::kernel ctx(m, params); ctx.assert_expr(tmp); while (true) { diff --git a/src/muz_qe/pdr_context.cpp b/src/muz_qe/pdr_context.cpp index c544d9edf..1280810e3 100644 --- a/src/muz_qe/pdr_context.cpp +++ b/src/muz_qe/pdr_context.cpp @@ -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); diff --git a/src/muz_qe/pdr_farkas_learner.cpp b/src/muz_qe/pdr_farkas_learner.cpp index 00bb5d723..3206c64da 100644 --- a/src/muz_qe/pdr_farkas_learner.cpp +++ b/src/muz_qe/pdr_farkas_learner.cpp @@ -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(); diff --git a/src/muz_qe/pdr_farkas_learner.h b/src/muz_qe/pdr_farkas_learner.h index 888947049..56cb3640c 100644 --- a/src/muz_qe/pdr_farkas_learner.h +++ b/src/muz_qe/pdr_farkas_learner.h @@ -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 m_ctx; + scoped_ptr m_ctx; static front_end_params get_proof_params(front_end_params& orig_params); diff --git a/src/muz_qe/pdr_generalizers.cpp b/src/muz_qe/pdr_generalizers.cpp index e0d584f09..3105485e0 100644 --- a/src/muz_qe/pdr_generalizers.cpp +++ b/src/muz_qe/pdr_generalizers.cpp @@ -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"; diff --git a/src/muz_qe/pdr_manager.cpp b/src/muz_qe/pdr_manager.cpp index 29f299b91..87edbc618 100644 --- a/src/muz_qe/pdr_manager.cpp +++ b/src/muz_qe/pdr_manager.cpp @@ -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); } diff --git a/src/muz_qe/pdr_manager.h b/src/muz_qe/pdr_manager.h index 87eaa03bf..398f2716f 100644 --- a/src/muz_qe/pdr_manager.h +++ b/src/muz_qe/pdr_manager.h @@ -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" diff --git a/src/muz_qe/pdr_prop_solver.h b/src/muz_qe/pdr_prop_solver.h index 2b7c1af6d..da0a1b31e 100644 --- a/src/muz_qe/pdr_prop_solver.h +++ b/src/muz_qe/pdr_prop_solver.h @@ -25,7 +25,7 @@ Revision History: #include #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" diff --git a/src/muz_qe/pdr_quantifiers.cpp b/src/muz_qe/pdr_quantifiers.cpp index df3938acf..362575a8b 100644 --- a/src/muz_qe/pdr_quantifiers.cpp +++ b/src/muz_qe/pdr_quantifiers.cpp @@ -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()); } diff --git a/src/muz_qe/pdr_smt_context_manager.cpp b/src/muz_qe/pdr_smt_context_manager.cpp index ec813f606..36b8e2325 100644 --- a/src/muz_qe/pdr_smt_context_manager.cpp +++ b/src/muz_qe/pdr_smt_context_manager.cpp @@ -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()); + std::for_each(m_contexts.begin(), m_contexts.end(), delete_proc()); } 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; diff --git a/src/muz_qe/pdr_smt_context_manager.h b/src/muz_qe/pdr_smt_context_manager.h index cdff26a19..d6aef9776 100644 --- a/src/muz_qe/pdr_smt_context_manager.h +++ b/src/muz_qe/pdr_smt_context_manager.h @@ -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 m_contexts; + ptr_vector m_contexts; unsigned m_num_contexts; app_ref_vector m_predicate_list; func_decl_set m_predicate_set; diff --git a/src/muz_qe/qe.cpp b/src/muz_qe/qe.cpp index 1b92aa6e8..77750ced6 100644 --- a/src/muz_qe/qe.cpp +++ b/src/muz_qe/qe.cpp @@ -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; diff --git a/src/muz_qe/qe_sat_tactic.cpp b/src/muz_qe/qe_sat_tactic.cpp index e5a57871a..1480a8ca0 100644 --- a/src/muz_qe/qe_sat_tactic.cpp +++ b/src/muz_qe/qe_sat_tactic.cpp @@ -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 m_vars; - ptr_vector m_solvers; - smt::solver m_solver; + ptr_vector 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(); diff --git a/src/smt/default_solver.cpp b/src/smt/default_solver.cpp index 73ce084f3..1a895d212 100644 --- a/src/smt/default_solver.cpp +++ b/src/smt/default_solver.cpp @@ -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); diff --git a/src/smt/default_solver.h b/src/smt/default_solver.h index 170a55e56..adffac1c3 100644 --- a/src/smt/default_solver.h +++ b/src/smt/default_solver.h @@ -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: diff --git a/src/smt/expr_context_simplifier.cpp b/src/smt/expr_context_simplifier.cpp index a2a097ff5..b39e3fb9c 100644 --- a/src/smt/expr_context_simplifier.cpp +++ b/src/smt/expr_context_simplifier.cpp @@ -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. diff --git a/src/smt/expr_context_simplifier.h b/src/smt/expr_context_simplifier.h index 758c3af8b..6e13dcf43 100644 --- a/src/smt/expr_context_simplifier.h +++ b/src/smt/expr_context_simplifier.h @@ -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); diff --git a/src/smt/ni_solver.cpp b/src/smt/ni_solver.cpp index a0341cb32..cd0cd503a 100644 --- a/src/smt/ni_solver.cpp +++ b/src/smt/ni_solver.cpp @@ -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); } }; diff --git a/src/smt/smt_implied_equalities.cpp b/src/smt/smt_implied_equalities.cpp index 1dd0c412b..ef8d27e2f 100644 --- a/src/smt/smt_implied_equalities.cpp +++ b/src/smt/smt_implied_equalities.cpp @@ -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 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); } diff --git a/src/smt/smt_implied_equalities.h b/src/smt/smt_implied_equalities.h index dfb9bf611..6fc002ff1 100644 --- a/src/smt/smt_implied_equalities.h +++ b/src/smt/smt_implied_equalities.h @@ -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); diff --git a/src/smt/smt_solver.cpp b/src/smt/smt_kernel.cpp similarity index 74% rename from src/smt/smt_solver.cpp rename to src/smt/smt_kernel.cpp index 6bdfd0524..9d87b1363 100644 --- a/src/smt/smt_solver.cpp +++ b/src/smt/smt_kernel.cpp @@ -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 & result) { + void kernel::get_relevant_labels(expr * cnstr, buffer & 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; } diff --git a/src/smt/smt_solver.h b/src/smt/smt_kernel.h similarity index 82% rename from src/smt/smt_solver.h rename to src/smt/smt_kernel.h index 1d04df9ed..4c381e113 100644 --- a/src/smt/smt_solver.h +++ b/src/smt/smt_kernel.h @@ -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(); }; }; diff --git a/src/smt/smt_model_checker.cpp b/src/smt/smt_model_checker.cpp index 6e9cd01fc..58921bb35 100644 --- a/src/smt/smt_model_checker.cpp +++ b/src/smt/smt_model_checker.cpp @@ -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()); } /** diff --git a/src/smt/smt_quantifier.cpp b/src/smt/smt_quantifier.cpp index b6ed70180..c11f226ed 100644 --- a/src/smt/smt_quantifier.cpp +++ b/src/smt/smt_quantifier.cpp @@ -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(); diff --git a/src/smt/smt_quantifier.h b/src/smt/smt_quantifier.h index 9c4129c0d..3873c9737 100644 --- a/src/smt/smt_quantifier.h +++ b/src/smt/smt_quantifier.h @@ -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); diff --git a/src/smt/tactic/ctx_solver_simplify_tactic.cpp b/src/smt/tactic/ctx_solver_simplify_tactic.cpp index 76379e595..e5b625661 100644 --- a/src/smt/tactic/ctx_solver_simplify_tactic.cpp +++ b/src/smt/tactic/ctx_solver_simplify_tactic.cpp @@ -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; diff --git a/src/smt/tactic/smt_tactic.cpp b/src/smt/tactic/smt_tactic.cpp index 7afce667a..fd942d05c 100644 --- a/src/smt/tactic/smt_tactic.cpp +++ b/src/smt/tactic/smt_tactic.cpp @@ -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; diff --git a/src/smt/user_plugin/user_smt_theory.cpp b/src/smt/user_plugin/user_smt_theory.cpp index 19b25dcfa..d95346469 100644 --- a/src/smt/user_plugin/user_smt_theory.cpp +++ b/src/smt/user_plugin/user_smt_theory.cpp @@ -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); diff --git a/src/smt/user_plugin/user_smt_theory.h b/src/smt/user_plugin/user_smt_theory.h index a27b3af32..3dd664738 100644 --- a/src/smt/user_plugin/user_smt_theory.h +++ b/src/smt/user_plugin/user_smt_theory.h @@ -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); }; diff --git a/src/test/quant_solve.cpp b/src/test/quant_solve.cpp index fe3454336..af6861af0 100644 --- a/src/test/quant_solve.cpp +++ b/src/test/quant_solve.cpp @@ -6,7 +6,7 @@ #include "lbool.h" #include #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";