mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-22 16:45:31 +00:00
Code Activity

Merge branch 'unstable' of https://git01.codeplex.com/z3 into unstable

Browse source
This commit is contained in:
Nikolaj Bjorner 2012-11-04 08:40:23 +02:00
commit bfbdad3ce6
79 changed files with 1497 additions and 1604 deletions
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"

16
src/api/api_parsers.cpp
View file

@ -23,6 +23,7 @@ Revision History:
#include"cmd_context.h"
#include"smt2parser.h"
#include"smtparser.h"
#include"solver_na2as.h"
extern "C" {
@ -251,20 +252,19 @@ extern "C" {
// ---------------
// Support for SMTLIB2
class z3_context_solver : public solver {
class z3_context_solver : public solver_na2as {
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) {}
virtual void init(ast_manager & m, symbol const & logic) {}
virtual void init_core(ast_manager & m, symbol const & logic) {}
virtual void collect_statistics(statistics & st) const {}
virtual void reset() { ctx().reset(); }
virtual void reset_core() { ctx().reset(); }
virtual void assert_expr(expr * t) { ctx().assert_expr(t); }
virtual void push() { ctx().push(); }
virtual void pop(unsigned n) { ctx().pop(n); }
virtual unsigned get_scope_level() const { return ctx().get_scope_level(); }
virtual lbool check_sat(unsigned num_assumptions, expr * const * assumptions) {
virtual void push_core() { ctx().push(); }
virtual void pop_core(unsigned n) { ctx().pop(n); }
virtual lbool check_sat_core(unsigned num_assumptions, expr * const * assumptions) {
return ctx().check(num_assumptions, assumptions);
}
virtual void get_unsat_core(ptr_vector<expr> & r) {

59
src/api/api_solver.cpp
View file

@ -29,18 +29,33 @@ Revision History:
#include"cancel_eh.h"
#include"scoped_timer.h"
#include"smt_strategic_solver.h"
#include"default_solver.h"
#include"smt_solver.h"
extern "C" {
static void init_solver_core(Z3_context c, Z3_solver _s) {
ast_manager & m = mk_c(c)->m();
Z3_solver_ref * s = to_solver(_s);
s->m_solver->set_produce_proofs(m.proofs_enabled());
s->m_solver->set_produce_unsat_cores(s->m_params.get_bool(":unsat-core", false));
s->m_solver->set_produce_models(s->m_params.get_bool(":model", true));
s->m_solver->set_front_end_params(mk_c(c)->fparams());
s->m_solver->updt_params(s->m_params);
s->m_solver->init(m, s->m_logic);
s->m_initialized = true;
}
static void init_solver(Z3_context c, Z3_solver s) {
if (!to_solver(s)->m_initialized)
init_solver_core(c, s);
}
Z3_solver Z3_API Z3_mk_simple_solver(Z3_context c) {
Z3_TRY;
LOG_Z3_mk_simple_solver(c);
RESET_ERROR_CODE();
Z3_solver_ref * s = alloc(Z3_solver_ref);
s->m_solver = mk_default_solver();
s->m_solver->set_front_end_params(mk_c(c)->fparams());
s->m_solver->init(mk_c(c)->m(), symbol::null);
s->m_solver = mk_smt_solver();
mk_c(c)->save_object(s);
Z3_solver r = of_solver(s);
RETURN_Z3(r);
@ -53,8 +68,6 @@ extern "C" {
RESET_ERROR_CODE();
Z3_solver_ref * s = alloc(Z3_solver_ref);
s->m_solver = mk_smt_strategic_solver();
s->m_solver->set_front_end_params(mk_c(c)->fparams());
s->m_solver->init(mk_c(c)->m(), symbol::null);
mk_c(c)->save_object(s);
Z3_solver r = of_solver(s);
RETURN_Z3(r);
@ -65,10 +78,8 @@ extern "C" {
Z3_TRY;
LOG_Z3_mk_solver_for_logic(c, logic);
RESET_ERROR_CODE();
Z3_solver_ref * s = alloc(Z3_solver_ref);
Z3_solver_ref * s = alloc(Z3_solver_ref, to_symbol(logic));
s->m_solver = mk_smt_strategic_solver(true /* force solver to use tactics even when auto_config is disabled */);
s->m_solver->set_front_end_params(mk_c(c)->fparams());
s->m_solver->init(mk_c(c)->m(), to_symbol(logic));
mk_c(c)->save_object(s);
Z3_solver r = of_solver(s);
RETURN_Z3(r);
@ -81,8 +92,6 @@ extern "C" {
RESET_ERROR_CODE();
Z3_solver_ref * s = alloc(Z3_solver_ref);
s->m_solver = alloc(tactic2solver, to_tactic_ref(t));
s->m_solver->set_front_end_params(mk_c(c)->fparams());
s->m_solver->init(mk_c(c)->m(), symbol::null);
mk_c(c)->save_object(s);
Z3_solver r = of_solver(s);
RETURN_Z3(r);
@ -117,7 +126,13 @@ extern "C" {
Z3_TRY;
LOG_Z3_solver_set_params(c, s, p);
RESET_ERROR_CODE();
to_solver_ref(s)->updt_params(to_param_ref(p));
if (to_solver(s)->m_initialized) {
bool old_model = to_solver(s)->m_params.get_bool(":model", true);
bool new_model = to_param_ref(p).get_bool(":model", true);
if (old_model != new_model)
to_solver_ref(s)->set_produce_models(new_model);
to_solver_ref(s)->updt_params(to_param_ref(p));
}
to_solver(s)->m_params = to_param_ref(p);
Z3_CATCH;
}
@ -142,6 +157,7 @@ extern "C" {
Z3_TRY;
LOG_Z3_solver_push(c, s);
RESET_ERROR_CODE();
init_solver(c, s);
to_solver_ref(s)->push();
Z3_CATCH;
}
@ -150,6 +166,7 @@ extern "C" {
Z3_TRY;
LOG_Z3_solver_pop(c, s, n);
RESET_ERROR_CODE();
init_solver(c, s);
if (n > to_solver_ref(s)->get_scope_level()) {
SET_ERROR_CODE(Z3_IOB);
return;
@ -164,7 +181,7 @@ extern "C" {
LOG_Z3_solver_reset(c, s);
RESET_ERROR_CODE();
to_solver_ref(s)->reset();
to_solver_ref(s)->init(mk_c(c)->m(), symbol::null);
to_solver(s)->m_initialized = false;
Z3_CATCH;
}
@ -172,6 +189,7 @@ extern "C" {
Z3_TRY;
LOG_Z3_solver_get_num_scopes(c, s);
RESET_ERROR_CODE();
init_solver(c, s);
return to_solver_ref(s)->get_scope_level();
Z3_CATCH_RETURN(0);
}
@ -180,7 +198,8 @@ extern "C" {
Z3_TRY;
LOG_Z3_solver_assert(c, s, a);
RESET_ERROR_CODE();
CHECK_FORMULA(a,);
init_solver(c, s);
CHECK_FORMULA(a,);
to_solver_ref(s)->assert_expr(to_expr(a));
Z3_CATCH;
}
@ -189,6 +208,7 @@ extern "C" {
Z3_TRY;
LOG_Z3_solver_get_assertions(c, s);
RESET_ERROR_CODE();
init_solver(c, s);
Z3_ast_vector_ref * v = alloc(Z3_ast_vector_ref, mk_c(c)->m());
mk_c(c)->save_object(v);
unsigned sz = to_solver_ref(s)->get_num_assertions();
@ -207,9 +227,6 @@ extern "C" {
}
}
expr * const * _assumptions = to_exprs(assumptions);
to_solver_ref(s)->set_produce_models(to_solver(s)->m_params.get_bool(":model", true));
to_solver_ref(s)->set_produce_proofs(mk_c(c)->m().proofs_enabled());
to_solver_ref(s)->set_produce_unsat_cores(num_assumptions > 0);
unsigned timeout = to_solver(s)->m_params.get_uint(":timeout", UINT_MAX);
bool use_ctrl_c = to_solver(s)->m_params.get_bool(":ctrl-c", false);
cancel_eh<solver> eh(*to_solver_ref(s));
@ -233,6 +250,7 @@ extern "C" {
Z3_TRY;
LOG_Z3_solver_check(c, s);
RESET_ERROR_CODE();
init_solver(c, s);
return _solver_check(c, s, 0, 0);
Z3_CATCH_RETURN(Z3_L_UNDEF);
}
@ -241,6 +259,7 @@ extern "C" {
Z3_TRY;
LOG_Z3_solver_check_assumptions(c, s, num_assumptions, assumptions);
RESET_ERROR_CODE();
init_solver(c, s);
return _solver_check(c, s, num_assumptions, assumptions);
Z3_CATCH_RETURN(Z3_L_UNDEF);
}
@ -249,6 +268,7 @@ extern "C" {
Z3_TRY;
LOG_Z3_solver_get_model(c, s);
RESET_ERROR_CODE();
init_solver(c, s);
model_ref _m;
to_solver_ref(s)->get_model(_m);
if (!_m) {
@ -266,6 +286,7 @@ extern "C" {
Z3_TRY;
LOG_Z3_solver_get_proof(c, s);
RESET_ERROR_CODE();
init_solver(c, s);
proof * p = to_solver_ref(s)->get_proof();
if (!p) {
SET_ERROR_CODE(Z3_INVALID_USAGE);
@ -280,6 +301,7 @@ extern "C" {
Z3_TRY;
LOG_Z3_solver_get_unsat_core(c, s);
RESET_ERROR_CODE();
init_solver(c, s);
ptr_vector<expr> core;
to_solver_ref(s)->get_unsat_core(core);
Z3_ast_vector_ref * v = alloc(Z3_ast_vector_ref, mk_c(c)->m());
@ -295,6 +317,7 @@ extern "C" {
Z3_TRY;
LOG_Z3_solver_get_reason_unknown(c, s);
RESET_ERROR_CODE();
init_solver(c, s);
return mk_c(c)->mk_external_string(to_solver_ref(s)->reason_unknown());
Z3_CATCH_RETURN("");
}
@ -303,6 +326,7 @@ extern "C" {
Z3_TRY;
LOG_Z3_solver_get_statistics(c, s);
RESET_ERROR_CODE();
init_solver(c, s);
Z3_stats_ref * st = alloc(Z3_stats_ref);
to_solver_ref(s)->collect_statistics(st->m_stats);
mk_c(c)->save_object(st);
@ -315,6 +339,7 @@ extern "C" {
Z3_TRY;
LOG_Z3_solver_to_string(c, s);
RESET_ERROR_CODE();
init_solver(c, s);
std::ostringstream buffer;
to_solver_ref(s)->display(buffer);
return mk_c(c)->mk_external_string(buffer.str());

5
src/api/api_solver.h
View file

@ -24,7 +24,10 @@ Revision History:
struct Z3_solver_ref : public api::object {
solver * m_solver;
params_ref m_params;
Z3_solver_ref():m_solver(0) {}
bool m_initialized;
symbol m_logic;
Z3_solver_ref():m_solver(0), m_initialized(false), m_logic(symbol::null) {}
Z3_solver_ref(symbol const & logic):m_solver(0), m_initialized(false), m_logic(logic) {}
virtual ~Z3_solver_ref() { dealloc(m_solver); }
};

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);
}

4
src/ast/expr_substitution.cpp
View file

@ -139,6 +139,10 @@ bool expr_substitution::find(expr * c, expr * & def, proof * & def_pr, expr_depe
return false;
}
bool expr_substitution::contains(expr * s) {
return m_subst.contains(s);
}
void expr_substitution::reset() {
dec_ref_map_key_values(m_manager, m_subst);
if (proofs_enabled())

1
src/ast/expr_substitution.h
View file

@ -47,6 +47,7 @@ public:
void erase(expr * s);
bool find(expr * s, expr * & def, proof * & def_pr);
bool find(expr * s, expr * & def, proof * & def_pr, expr_dependency * & def_dep);
bool contains(expr * s);
void reset();
void cleanup();
};

0
src/ast/macros/macro_substitution.cpp → src/ast/macro_substitution.cpp
View file

0
src/ast/macros/macro_substitution.h → src/ast/macro_substitution.h
View file

9
src/ast/rewriter/expr_replacer.cpp
View file

@ -114,6 +114,10 @@ public:
virtual unsigned get_num_steps() const {
return m_replacer.get_num_steps();
}
virtual void reset() {
m_replacer.reset();
}
};
expr_replacer * mk_default_expr_replacer(ast_manager & m) {
@ -149,6 +153,11 @@ public:
virtual unsigned get_num_steps() const {
return m_r.get_num_steps();
}
virtual void reset() {
m_r.reset();
}
};
expr_replacer * mk_expr_simp_replacer(ast_manager & m, params_ref const & p) {

4
src/ast/rewriter/expr_replacer.h
View file

@ -43,8 +43,8 @@ public:
void reset_cancel() { set_cancel(false); }
virtual void set_cancel(bool f) = 0;
virtual unsigned get_num_steps() const { return 0; }
virtual void reset() = 0;
void apply_substitution(expr * s, expr * def, proof * def_pr, expr_ref & t);
void apply_substitution(expr * s, expr * def, expr_ref & t);
};

4
src/ast/simplifier/poly_simplifier_plugin.h
View file

@ -134,6 +134,10 @@ public:
virtual bool reduce_distinct(unsigned num_args, expr * const * args, expr_ref & result);
virtual bool reduce(func_decl * f, unsigned num_args, rational const * mults, expr * const * args, expr_ref & result);
virtual bool reduce(func_decl * f, unsigned num_args, expr * const * args, expr_ref & result) {
return simplifier_plugin::reduce(f, num_args, args, result);
}
expr * get_monomial_body(expr * m);
int get_monomial_body_order(expr * m);

4
src/cmd_context/basic_cmds.cpp
View file

@ -359,14 +359,14 @@ class set_option_cmd : public set_get_option_cmd {
}
else if (m_option == m_produce_proofs) {
check_not_initialized(ctx, m_produce_proofs);
ctx.params().m_proof_mode = to_bool(value) ? PGM_FINE : PGM_DISABLED;
ctx.set_produce_proofs(to_bool(value));
}
else if (m_option == m_produce_unsat_cores) {
check_not_initialized(ctx, m_produce_unsat_cores);
ctx.set_produce_unsat_cores(to_bool(value));
}
else if (m_option == m_produce_models) {
ctx.params().m_model = to_bool(value);
ctx.set_produce_models(to_bool(value));
}
else if (m_option == m_produce_assignments) {
ctx.set_produce_assignments(to_bool(value));

81
src/cmd_context/cmd_context.cpp
View file

@ -348,6 +348,24 @@ cmd_context::~cmd_context() {
}
}
void cmd_context::set_produce_models(bool f) {
params().m_model = f;
if (m_solver)
m_solver->set_produce_models(f);
}
void cmd_context::set_produce_unsat_cores(bool f) {
// can only be set before initialization
SASSERT(!has_manager());
m_produce_unsat_cores = f;
}
void cmd_context::set_produce_proofs(bool f) {
// can only be set before initialization
SASSERT(!has_manager());
params().m_proof_mode = f ? PGM_FINE : PGM_DISABLED;
}
bool cmd_context::is_smtlib2_compliant() const {
return params().m_smtlib2_compliant;
}
@ -540,8 +558,12 @@ void cmd_context::init_manager_core(bool new_manager) {
// it prevents clashes with builtin types.
insert(pm().mk_plist_decl());
}
if (m_solver)
if (m_solver) {
m_solver->set_produce_unsat_cores(m_produce_unsat_cores);
m_solver->set_produce_models(params().m_model);
m_solver->set_produce_proofs(params().m_proof_mode == PGM_FINE);
m_solver->init(m(), m_logic);
}
m_check_logic.set_logic(m(), m_logic);
}
@ -1076,7 +1098,6 @@ void cmd_context::reset(bool finalize) {
reset_macros();
reset_func_decls();
restore_assertions(0);
restore_assumptions(0);
if (m_solver)
m_solver->reset();
m_pp_env = 0;
@ -1108,6 +1129,8 @@ void cmd_context::assert_expr(expr * t) {
m_check_sat_result = 0;
m().inc_ref(t);
m_assertions.push_back(t);
if (m_produce_unsat_cores)
m_assertion_names.push_back(0);
if (m_solver)
m_solver->assert_expr(t);
}
@ -1119,11 +1142,14 @@ void cmd_context::assert_expr(symbol const & name, expr * t) {
assert_expr(t);
return;
}
app * proxy = m().mk_const(name, m().mk_bool_sort());
expr * new_t = m().mk_implies(proxy, t);
m().inc_ref(proxy);
m_assumptions.push_back(proxy);
assert_expr(new_t);
m_check_sat_result = 0;
m().inc_ref(t);
m_assertions.push_back(t);
expr * ans = m().mk_const(name, m().mk_bool_sort());
m().inc_ref(ans);
m_assertion_names.push_back(ans);
if (m_solver)
m_solver->assert_expr(t, ans);
}
void cmd_context::push() {
@ -1137,7 +1163,6 @@ void cmd_context::push() {
s.m_macros_stack_lim = m_macros_stack.size();
s.m_aux_pdecls_lim = m_aux_pdecls.size();
s.m_assertions_lim = m_assertions.size();
s.m_assumptions_lim = m_assumptions.size();
if (m_solver)
m_solver->push();
}
@ -1200,29 +1225,25 @@ void cmd_context::restore_aux_pdecls(unsigned old_sz) {
m_aux_pdecls.shrink(old_sz);
}
static void restore(ast_manager & m, ptr_vector<expr> & c, unsigned old_sz) {
ptr_vector<expr>::iterator it = c.begin() + old_sz;
ptr_vector<expr>::iterator end = c.end();
for (; it != end; ++it) {
m.dec_ref(*it);
}
c.shrink(old_sz);
}
void cmd_context::restore_assertions(unsigned old_sz) {
SASSERT(old_sz <= m_assertions.size());
SASSERT(!m_interactive_mode || m_assertions.size() == m_assertion_strings.size());
ptr_vector<expr>::iterator it = m_assertions.begin() + old_sz;
ptr_vector<expr>::iterator end = m_assertions.end();
for (; it != end; ++it) {
m().dec_ref(*it);
}
m_assertions.shrink(old_sz);
restore(m(), m_assertions, old_sz);
if (m_produce_unsat_cores)
restore(m(), m_assertion_names, old_sz);
if (m_interactive_mode)
m_assertion_strings.shrink(old_sz);
}
void cmd_context::restore_assumptions(unsigned old_sz) {
SASSERT(old_sz <= m_assumptions.size());
ptr_vector<expr>::iterator it = m_assumptions.begin() + old_sz;
ptr_vector<expr>::iterator end = m_assumptions.end();
for (; it != end; ++it) {
m().dec_ref(*it);
}
m_assumptions.shrink(old_sz);
}
void cmd_context::pop(unsigned n) {
m_check_sat_result = 0;
if (n == 0)
@ -1240,7 +1261,6 @@ void cmd_context::pop(unsigned n) {
restore_macros(s.m_macros_stack_lim);
restore_aux_pdecls(s.m_aux_pdecls_lim);
restore_assertions(s.m_assertions_lim);
restore_assumptions(s.m_assumptions_lim);
m_scopes.shrink(new_lvl);
}
@ -1260,17 +1280,12 @@ void cmd_context::check_sat(unsigned num_assumptions, expr * const * assumptions
m_check_sat_result = m_solver.get(); // solver itself stores the result.
m_solver->set_front_end_params(params());
m_solver->set_progress_callback(this);
m_solver->set_produce_proofs(produce_proofs());
m_solver->set_produce_models(produce_models());
m_solver->set_produce_unsat_cores(produce_unsat_cores());
scoped_watch sw(*this);
cancel_eh<solver> eh(*m_solver);
scoped_ctrl_c ctrlc(eh);
unsigned old_sz = m_assumptions.size();
m_assumptions.append(num_assumptions, assumptions);
lbool r;
try {
r = m_solver->check_sat(m_assumptions.size(), m_assumptions.c_ptr());
r = m_solver->check_sat(num_assumptions, assumptions);
}
catch (z3_error & ex) {
throw ex;
@ -1278,7 +1293,6 @@ void cmd_context::check_sat(unsigned num_assumptions, expr * const * assumptions
catch (z3_exception & ex) {
throw cmd_exception(ex.msg());
}
m_assumptions.shrink(old_sz);
m_solver->set_status(r);
display_sat_result(r);
validate_check_sat_result(r);
@ -1410,6 +1424,9 @@ void cmd_context::set_solver(solver * s) {
m_solver = s;
m_solver->set_front_end_params(params());
if (has_manager() && s != 0) {
m_solver->set_produce_unsat_cores(m_produce_unsat_cores);
m_solver->set_produce_models(params().m_model);
m_solver->set_produce_proofs(params().m_proof_mode == PGM_FINE);
m_solver->init(m(), m_logic);
// assert formulas and create scopes in the new solver.
unsigned lim = 0;

15
src/cmd_context/cmd_context.h
View file

@ -175,16 +175,15 @@ protected:
ptr_vector<pdecl> m_aux_pdecls;
ptr_vector<expr> m_assertions;
vector<std::string> m_assertion_strings;
ptr_vector<expr> m_assumptions; // for unsat-core extraction
ptr_vector<expr> m_assertion_names; // named assertions are represented using boolean variables.
struct scope {
unsigned m_func_decls_stack_lim;
unsigned m_psort_decls_stack_lim;
unsigned m_macros_stack_lim;
unsigned m_aux_pdecls_lim;
// only m_assertions_lim and m_assumptions_lim are relevant when m_global_decls = true
// only m_assertions_lim is relevant when m_global_decls = true
unsigned m_assertions_lim;
unsigned m_assumptions_lim;
};
svector<scope> m_scopes;
@ -225,7 +224,6 @@ protected:
void restore_macros(unsigned old_sz);
void restore_aux_pdecls(unsigned old_sz);
void restore_assertions(unsigned old_sz);
void restore_assumptions(unsigned old_sz);
void erase_func_decl_core(symbol const & s, func_decl * f);
void erase_psort_decl_core(symbol const & s);
@ -272,7 +270,9 @@ public:
bool produce_models() const;
bool produce_proofs() const;
bool produce_unsat_cores() const { return m_produce_unsat_cores; }
void set_produce_unsat_cores(bool flag) { m_produce_unsat_cores = flag; }
void set_produce_models(bool flag);
void set_produce_unsat_cores(bool flag);
void set_produce_proofs(bool flag);
bool produce_assignments() const { return m_produce_assignments; }
void set_produce_assignments(bool flag) { m_produce_assignments = flag; }
void set_status(status st) { m_status = st; }
@ -369,8 +369,8 @@ public:
ptr_vector<expr>::const_iterator begin_assertions() const { return m_assertions.begin(); }
ptr_vector<expr>::const_iterator end_assertions() const { return m_assertions.end(); }
ptr_vector<expr>::const_iterator begin_assumptions() const { return m_assumptions.begin(); }
ptr_vector<expr>::const_iterator end_assumptions() const { return m_assumptions.end(); }
ptr_vector<expr>::const_iterator begin_assertion_names() const { return m_assertion_names.begin(); }
ptr_vector<expr>::const_iterator end_assertion_names() const { return m_assertion_names.end(); }
/**
\brief Hack: consume assertions if there are no scopes.
@ -380,7 +380,6 @@ public:
if (num_scopes() > 0)
return false;
restore_assertions(0);
restore_assumptions(0);
return true;
}

24
src/cmd_context/cmd_context_to_goal.cpp
View file

@ -27,20 +27,22 @@ void assert_exprs_from(cmd_context const & ctx, goal & t) {
throw cmd_exception("Frontend does not support simultaneous generation of proofs and unsat cores");
ast_manager & m = t.m();
bool proofs_enabled = t.proofs_enabled();
ptr_vector<expr>::const_iterator it = ctx.begin_assertions();
ptr_vector<expr>::const_iterator end = ctx.end_assertions();
for (; it != end; ++it) {
t.assert_expr(*it, proofs_enabled ? m.mk_asserted(*it) : 0, 0);
}
if (ctx.produce_unsat_cores()) {
SASSERT(!ctx.produce_proofs());
it = ctx.begin_assumptions();
end = ctx.end_assumptions();
for (; it != end; ++it) {
t.assert_expr(*it, 0, m.mk_leaf(*it));
ptr_vector<expr>::const_iterator it = ctx.begin_assertions();
ptr_vector<expr>::const_iterator end = ctx.end_assertions();
ptr_vector<expr>::const_iterator it2 = ctx.begin_assertion_names();
ptr_vector<expr>::const_iterator end2 = ctx.end_assertion_names();
SASSERT(end - it == end2 - it2);
for (; it != end; ++it, ++it2) {
t.assert_expr(*it, proofs_enabled ? m.mk_asserted(*it) : 0, m.mk_leaf(*it2));
}
}
else {
SASSERT(ctx.begin_assumptions() == ctx.end_assumptions());
ptr_vector<expr>::const_iterator it = ctx.begin_assertions();
ptr_vector<expr>::const_iterator end = ctx.end_assertions();
for (; it != end; ++it) {
t.assert_expr(*it, proofs_enabled ? m.mk_asserted(*it) : 0, 0);
}
SASSERT(ctx.begin_assertion_names() == ctx.end_assertion_names());
}
}

2
src/cmd_context/pdecl.h
View file

@ -181,6 +181,7 @@ class paccessor_decl : public pdecl {
ptype const & get_type() const { return m_type; }
virtual ~paccessor_decl() {}
public:
virtual void display(std::ostream & out) const { pdecl::display(out); }
void display(std::ostream & out, pdatatype_decl const * const * dts) const;
};
@ -201,6 +202,7 @@ class pconstructor_decl : public pdecl {
constructor_decl * instantiate_decl(pdecl_manager & m, sort * const * s);
virtual ~pconstructor_decl() {}
public:
virtual void display(std::ostream & out) const { pdecl::display(out); }
void display(std::ostream & out, pdatatype_decl const * const * dts) const;
};

34
src/cmd_context/strategic_solver_cmd.cpp
View file

@ -1,34 +0,0 @@
/*++
Copyright (c) 2012 Microsoft Corporation
Module Name:
strategic_solver_cmd.h
Abstract:
Specialization of the strategic solver that
used cmd_context to access the assertion set.
Author:
Leonardo (leonardo) 2012-11-01
Notes:
--*/
#include"strategic_solver_cmd.h"
#include"cmd_context.h"
strategic_solver_cmd::strategic_solver_cmd(cmd_context & ctx):
m_ctx(ctx) {
}
unsigned strategic_solver_cmd::get_num_assertions() const {
return static_cast<unsigned>(m_ctx.end_assertions() - m_ctx.begin_assertions());
}
expr * strategic_solver_cmd::get_assertion(unsigned idx) const {
SASSERT(idx < get_num_assertions());
return m_ctx.begin_assertions()[idx];
}

40
src/cmd_context/strategic_solver_cmd.h
View file

@ -1,40 +0,0 @@
/*++
Copyright (c) 2012 Microsoft Corporation
Module Name:
strategic_solver_cmd.h
Abstract:
Specialization of the strategic solver that
used cmd_context to access the assertion set.
Author:
Leonardo (leonardo) 2012-11-01
Notes:
--*/
#ifndef _STRATEGIC_SOLVER_CMD_H_
#define _STRATEGIC_SOLVER_CMD_H_
#include"strategic_solver.h"
class cmd_context;
/**
Specialization for the SMT 2.0 command language frontend.
The strategic solver does not have to maintain a copy of the assertion set in the cmd_context.
*/
class strategic_solver_cmd : public strategic_solver_core {
cmd_context & m_ctx;
public:
strategic_solver_cmd(cmd_context & ctx);
virtual unsigned get_num_assertions() const;
virtual expr * get_assertion(unsigned idx) const;
};
#endif

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

@ -1867,7 +1867,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);

2
src/muz_qe/pdr_context.h
View file

@ -274,7 +274,7 @@ namespace pdr {
(*this)(n, new_cores.back().first, new_cores.back().second);
}
}
virtual void collect_statistics(statistics& st) {}
virtual void collect_statistics(statistics& st) const {}
};
class context {

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();

2
src/parsers/smt/smtlib_solver.cpp
View file

@ -83,7 +83,7 @@ namespace smtlib {
benchmark.add_formula(m_ast_manager.mk_true());
}
m_ctx = alloc(cmd_context, &m_params, true, &m_ast_manager, benchmark.get_logic());
m_ctx->set_solver(mk_smt_strategic_solver(*m_ctx));
m_ctx->set_solver(mk_smt_strategic_solver(false));
theory::expr_iterator fit = benchmark.begin_formulas();
theory::expr_iterator fend = benchmark.end_formulas();
for (; fit != fend; ++fit)

2
src/shell/smtlib_frontend.cpp
View file

@ -106,7 +106,7 @@ unsigned read_smtlib2_commands(char const* file_name, front_end_params& front_en
ctx.set_solver(s);
}
else {
solver * s = mk_smt_strategic_solver(ctx);
solver * s = mk_smt_strategic_solver(false);
ctx.set_solver(s);
}
install_dl_cmds(ctx);

5
src/smt/asserted_formulas.cpp
View file

@ -60,7 +60,6 @@ asserted_formulas::asserted_formulas(ast_manager & m, front_end_params & p):
m_macro_manager(m, m_simplifier),
m_bit2int(m),
m_bv_sharing(m),
m_user_rewriter(m),
m_inconsistent(false),
m_cancel_flag(false) {
@ -282,7 +281,6 @@ void asserted_formulas::reset() {
}
void asserted_formulas::set_cancel_flag(bool f) {
m_user_rewriter.set_cancel(f);
m_cancel_flag = f;
}
@ -341,7 +339,6 @@ void asserted_formulas::reduce() {
TRACE("qbv_bug", tout << "after demod:\n"; display(tout););
INVOKE(m_params.m_quasi_macros && has_quantifiers(), apply_quasi_macros());
INVOKE(m_params.m_simplify_bit2int, apply_bit2int());
INVOKE(m_user_rewriter.enabled(), apply_user_rewriter());
INVOKE(m_params.m_eliminate_bounds && has_quantifiers(), cheap_quant_fourier_motzkin());
INVOKE(!m_params.m_bb_eager && has_quantifiers() && m_params.m_ematching, infer_patterns());
INVOKE(m_params.m_max_bv_sharing && has_bv(), max_bv_sharing());
@ -1414,8 +1411,6 @@ void asserted_formulas::refine_inj_axiom() {
MK_SIMPLIFIER(apply_bit2int, bit2int& functor = m_bit2int, "bit2int", "propagate bit-vector over integers", true);
MK_SIMPLIFIER(apply_user_rewriter, user_rewriter& functor = m_user_rewriter, "user_rewriter", "apply user supplied rewriting", true);
MK_SIMPLIFIER(apply_der_core, der_star functor(m_manager), "der", "destructive equality resolution", true);
void asserted_formulas::apply_der() {

5
src/smt/asserted_formulas.h
View file

@ -30,7 +30,6 @@ Revision History:
#include"maximise_ac_sharing.h"
#include"bit2int.h"
#include"statistics.h"
#include"user_rewriter.h"
#include"pattern_inference.h"
class arith_simplifier_plugin;
@ -66,8 +65,6 @@ class asserted_formulas {
maximise_bv_sharing m_bv_sharing;
user_rewriter m_user_rewriter;
bool m_inconsistent;
// qe::expr_quant_elim_star1 m_quant_elim;
@ -98,7 +95,6 @@ class asserted_formulas {
void apply_quasi_macros();
void nnf_cnf();
bool apply_eager_bit_blaster();
bool apply_user_rewriter();
void infer_patterns();
void eliminate_term_ite();
void reduce_and_solve();
@ -157,7 +153,6 @@ public:
void init(unsigned num_formulas, expr * const * formulas, proof * const * prs);
void register_simplifier_plugin(simplifier_plugin * p) { m_simplifier.register_plugin(p); }
simplifier & get_simplifier() { return m_simplifier; }
void set_user_rewriter(void* ctx, user_rewriter::fn* rw) { m_user_rewriter.set_rewriter(ctx, rw); }
void get_assertions(ptr_vector<expr> & result);
bool empty() const { return m_asserted_formulas.empty(); }
void collect_static_features();

181
src/smt/default_solver.cpp
View file

@ -1,181 +0,0 @@
/*++
Copyright (c) 2012 Microsoft Corporation
Module Name:
default_solver.cpp
Abstract:
Wrapps smt::solver as a solver for cmd_context
Author:
Leonardo (leonardo) 2012-10-21
Notes:
--*/
#include"solver.h"
#include"smt_solver.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;
public:
default_solver():m_params(0), m_context(0) {}
virtual ~default_solver() {
if (m_context != 0)
dealloc(m_context);
}
virtual void set_front_end_params(front_end_params & p) {
m_params = &p;
}
virtual void updt_params(params_ref const & p) {
if (m_context == 0)
return;
m_context->updt_params(p);
}
virtual void collect_param_descrs(param_descrs & r) {
if (m_context == 0) {
ast_manager m;
reg_decl_plugins(m);
front_end_params p;
smt::solver s(m, p);
s.collect_param_descrs(r);
}
else {
m_context->collect_param_descrs(r);
}
}
virtual void init(ast_manager & m, symbol const & logic) {
SASSERT(m_params);
reset();
#pragma omp critical (solver)
{
m_context = alloc(smt::solver, m, *m_params);
}
if (logic != symbol::null)
m_context->set_logic(logic);
}
virtual void collect_statistics(statistics & st) const {
if (m_context == 0) {
return;
}
else {
m_context->collect_statistics(st);
}
}
virtual void reset() {
if (m_context != 0) {
#pragma omp critical (solver)
{
dealloc(m_context);
m_context = 0;
}
}
}
virtual void assert_expr(expr * t) {
SASSERT(m_context);
m_context->assert_expr(t);
}
virtual void push() {
SASSERT(m_context);
m_context->push();
}
virtual void pop(unsigned n) {
SASSERT(m_context);
m_context->pop(n);
}
virtual unsigned get_scope_level() const {
if (m_context)
return m_context->get_scope_level();
else
return 0;
}
virtual lbool check_sat(unsigned num_assumptions, expr * const * assumptions) {
SASSERT(m_context);
return m_context->check(num_assumptions, assumptions);
}
virtual void get_unsat_core(ptr_vector<expr> & r) {
SASSERT(m_context);
unsigned sz = m_context->get_unsat_core_size();
for (unsigned i = 0; i < sz; i++)
r.push_back(m_context->get_unsat_core_expr(i));
}
virtual void get_model(model_ref & m) {
SASSERT(m_context);
m_context->get_model(m);
}
virtual proof * get_proof() {
SASSERT(m_context);
return m_context->get_proof();
}
virtual std::string reason_unknown() const {
SASSERT(m_context);
return m_context->last_failure_as_string();
}
virtual void get_labels(svector<symbol> & r) {
SASSERT(m_context);
buffer<symbol> tmp;
m_context->get_relevant_labels(0, tmp);
r.append(tmp.size(), tmp.c_ptr());
}
virtual void set_cancel(bool f) {
#pragma omp critical (solver)
{
if (m_context)
m_context->set_cancel(f);
}
}
virtual void set_progress_callback(progress_callback * callback) {
SASSERT(m_context);
m_context->set_progress_callback(callback);
}
virtual unsigned get_num_assertions() const {
if (m_context)
return m_context->size();
else
return 0;
}
virtual expr * get_assertion(unsigned idx) const {
SASSERT(m_context);
SASSERT(idx < get_num_assertions());
return m_context->get_formulas()[idx];
}
virtual void display(std::ostream & out) const {
if (m_context)
m_context->display(out);
else
out << "(solver)";
}
};
solver * mk_default_solver() {
return alloc(default_solver);
}

26
src/smt/default_solver.h
View file

@ -1,26 +0,0 @@
/*++
Copyright (c) 2012 Microsoft Corporation
Module Name:
default_solver.h
Abstract:
Wrapps smt::solver as a solver for cmd_context
Author:
Leonardo (leonardo) 2012-10-21
Notes:
--*/
#ifndef _DEFAULT_SOLVER_H_
#define _DEFAULT_SOLVER_H_
class solver;
solver * mk_default_solver();
#endif

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);

236
src/smt/ni_solver.cpp
View file

@ -1,236 +0,0 @@
/*++
Copyright (c) 2011 Microsoft Corporation
Module Name:
ni_solver.cpp
Abstract:
Wrappers for smt::solver that are non-incremental & (quasi-incremental).
Author:
Leonardo (leonardo) 2011-03-30
Notes:
--*/
#include"ni_solver.h"
#include"smt_solver.h"
#include"cmd_context.h"
class ni_smt_solver : public solver {
protected:
cmd_context & m_cmd_ctx;
smt::solver * m_context;
progress_callback * m_callback;
public:
ni_smt_solver(cmd_context & ctx):m_cmd_ctx(ctx), m_context(0), m_callback(0) {}
virtual ~ni_smt_solver() {
if (m_context != 0)
dealloc(m_context);
}
virtual void init(ast_manager & m, symbol const & logic) {
// do nothing
}
virtual void collect_statistics(statistics & st) const {
if (m_context == 0) {
return;
}
else {
m_context->collect_statistics(st);
}
}
virtual void reset() {
if (m_context != 0) {
#pragma omp critical (ni_solver)
{
dealloc(m_context);
m_context = 0;
}
}
}
virtual void assert_expr(expr * t) {
// do nothing
}
virtual void push() {
// do nothing
}
virtual void pop(unsigned n) {
// do nothing
}
virtual unsigned get_scope_level() const {
return m_cmd_ctx.num_scopes();
}
void assert_exprs() {
ptr_vector<expr>::const_iterator it = m_cmd_ctx.begin_assertions();
ptr_vector<expr>::const_iterator end = m_cmd_ctx.end_assertions();
for (; it != end; ++it) {
m_context->assert_expr(*it);
}
}
void init_solver() {
reset();
#pragma omp critical (ni_solver)
{
m_context = alloc(smt::solver, m_cmd_ctx.m(), m_cmd_ctx.params());
}
if (m_cmd_ctx.has_logic())
m_context->set_logic(m_cmd_ctx.get_logic());
if (m_callback)
m_context->set_progress_callback(m_callback);
assert_exprs();
}
virtual lbool check_sat(unsigned num_assumptions, expr * const * assumptions) {
// erase current solver, and create a new one.
init_solver();
if (num_assumptions == 0) {
return m_context->setup_and_check();
}
else {
return m_context->check(num_assumptions, assumptions);
}
}
virtual void get_unsat_core(ptr_vector<expr> & r) {
SASSERT(m_context);
unsigned sz = m_context->get_unsat_core_size();
for (unsigned i = 0; i < sz; i++)
r.push_back(m_context->get_unsat_core_expr(i));
}
virtual void get_model(model_ref & m) {
SASSERT(m_context);
m_context->get_model(m);
}
virtual proof * get_proof() {
SASSERT(m_context);
return m_context->get_proof();
}
virtual std::string reason_unknown() const {
SASSERT(m_context);
return m_context->last_failure_as_string();
}
virtual void get_labels(svector<symbol> & r) {
SASSERT(m_context);
buffer<symbol> tmp;
m_context->get_relevant_labels(0, tmp);
r.append(tmp.size(), tmp.c_ptr());
}
virtual void set_cancel(bool f) {
#pragma omp critical (ni_solver)
{
if (m_context)
m_context->set_cancel(f);
}
}
virtual void set_progress_callback(progress_callback * callback) {
m_callback = callback;
if (m_context)
m_context->set_progress_callback(callback);
}
virtual void collect_param_descrs(param_descrs & r) {
smt::solver::collect_param_descrs(r);
}
};
solver * mk_non_incremental_smt_solver(cmd_context & ctx) {
return alloc(ni_smt_solver, ctx);
}
class qi_smt_solver : public ni_smt_solver {
bool m_inc_mode;
public:
qi_smt_solver(cmd_context & ctx):ni_smt_solver(ctx), m_inc_mode(false) {}
virtual ~qi_smt_solver() {}
virtual void init(ast_manager & m, symbol const & logic) {
if (m_inc_mode) {
init_solver();
m_inc_mode = true;
}
}
virtual void reset() {
ni_smt_solver::reset();
m_inc_mode = false;
}
void switch_to_inc() {
if (!m_inc_mode) {
init_solver();
m_inc_mode = true;
}
SASSERT(m_inc_mode);
}
virtual void assert_expr(expr * t) {
if (m_context != 0 && !m_inc_mode) {
// solver was already created to solve a check_sat query...
switch_to_inc();
}
if (m_inc_mode) {
SASSERT(m_context);
m_context->assert_expr(t);
}
}
virtual void push() {
switch_to_inc();
SASSERT(m_context);
m_context->push();
SASSERT(m_inc_mode);
}
virtual void pop(unsigned n) {
switch_to_inc();
SASSERT(m_context);
m_context->pop(n);
SASSERT(m_inc_mode);
}
virtual unsigned get_scope_level() const {
if (!m_inc_mode)
return 0;
else
return m_context->get_scope_level();
}
virtual lbool check_sat(unsigned num_assumptions, expr * const * assumptions) {
if (!m_inc_mode) {
lbool r = ni_smt_solver::check_sat(num_assumptions, assumptions);
SASSERT(!m_inc_mode);
return r;
}
else {
return m_context->check(num_assumptions, assumptions);
}
}
};
solver * mk_quasi_incremental_smt_solver(cmd_context & ctx) {
return alloc(qi_smt_solver, ctx);
}

30
src/smt/ni_solver.h
View file

@ -1,30 +0,0 @@
/*++
Copyright (c) 2011 Microsoft Corporation
Module Name:
ni_solver.h
Abstract:
Wrappers for smt::context that are non-incremental & (quasi-incremental).
Author:
Leonardo (leonardo) 2011-03-30
Notes:
--*/
#ifndef _NI_SOLVER_H_
#define _NI_SOLVER_H_
#include"solver.h"
class cmd_context;
// Creates a solver that restarts from scratch for every call to check_sat
solver * mk_non_incremental_smt_solver(cmd_context & ctx);
// Creates a solver that restarts from scratch for the first call to check_sat, and then moves to incremental behavior.
solver * mk_quasi_incremental_smt_solver(cmd_context & ctx);
#endif

6
src/smt/smt_context.h
View file

@ -523,12 +523,6 @@ namespace smt {
friend class set_var_theory_trail;
void set_var_theory(bool_var v, theory_id tid);
/**
\brief set user-supplied rewriter.
*/
void set_user_rewriter(void* ctx, user_rewriter::fn* rw) { m_asserted_formulas.set_user_rewriter(ctx, rw); }
// -----------------------------------
//
// Backtracking support

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);

353
src/smt/smt_kernel.cpp Normal file
View file

@ -0,0 +1,353 @@
/*++
Copyright (c) 2012 Microsoft Corporation
Module Name:
smt_kernel.cpp
Abstract:
New frontend for smt::context.
Author:
Leonardo de Moura (leonardo) 2012-02-09.
Revision History:
--*/
#include"smt_kernel.h"
#include"smt_context.h"
#include"ast_smt2_pp.h"
#include"params2front_end_params.h"
namespace smt {
struct kernel::imp {
smt::context m_kernel;
params_ref m_params;
imp(ast_manager & m, front_end_params & fp, params_ref const & p):
m_kernel(m, fp, p),
m_params(p) {
}
front_end_params & fparams() {
return m_kernel.get_fparams();
}
params_ref const & params() {
return m_params;
}
ast_manager & m() const {
return m_kernel.get_manager();
}
bool set_logic(symbol logic) {
return m_kernel.set_logic(logic);
}
void set_progress_callback(progress_callback * callback) {
return m_kernel.set_progress_callback(callback);
}
void assert_expr(expr * e) {
TRACE("smt_kernel", tout << "assert:\n" << mk_ismt2_pp(e, m()) << "\n";);
m_kernel.assert_expr(e);
}
void assert_expr(expr * e, proof * pr) {
m_kernel.assert_expr(e, pr);
}
unsigned size() const {
return m_kernel.get_num_asserted_formulas();
}
expr * const * get_formulas() const {
return m_kernel.get_asserted_formulas();
}
bool reduce() {
return m_kernel.reduce_assertions();
}
void push() {
TRACE("smt_kernel", tout << "push()\n";);
m_kernel.push();
}
void pop(unsigned num_scopes) {
TRACE("smt_kernel", tout << "pop()\n";);
m_kernel.pop(num_scopes);
}
unsigned get_scope_level() const {
return m_kernel.get_scope_level();
}
lbool setup_and_check() {
return m_kernel.setup_and_check();
}
bool inconsistent() {
return m_kernel.inconsistent();
}
lbool check(unsigned num_assumptions, expr * const * assumptions) {
return m_kernel.check(num_assumptions, assumptions);
}
void get_model(model_ref & m) const {
m_kernel.get_model(m);
}
proof * get_proof() {
return m_kernel.get_proof();
}
unsigned get_unsat_core_size() const {
return m_kernel.get_unsat_core_size();
}
expr * get_unsat_core_expr(unsigned idx) const {
return m_kernel.get_unsat_core_expr(idx);
}
failure last_failure() const {
return m_kernel.get_last_search_failure();
}
std::string last_failure_as_string() const {
return m_kernel.last_failure_as_string();
}
void get_assignments(expr_ref_vector & result) {
m_kernel.get_assignments(result);
}
void get_relevant_labels(expr * cnstr, buffer<symbol> & result) {
m_kernel.get_relevant_labels(cnstr, result);
}
void get_relevant_labeled_literals(bool at_lbls, expr_ref_vector & result) {
m_kernel.get_relevant_labeled_literals(at_lbls, result);
}
void get_relevant_literals(expr_ref_vector & result) {
m_kernel.get_relevant_literals(result);
}
void get_guessed_literals(expr_ref_vector & result) {
m_kernel.get_guessed_literals(result);
}
void display(std::ostream & out) const {
// m_kernel.display(out); <<< for external users it is just junk
// 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 << "(kernel";
for (unsigned i = 0; i < num; i++) {
out << "\n " << mk_ismt2_pp(fms[i], m(), 2);
}
out << ")";
}
void collect_statistics(::statistics & st) const {
m_kernel.collect_statistics(st);
}
void reset_statistics() {
}
void display_statistics(std::ostream & out) const {
m_kernel.display_statistics(out);
}
void display_istatistics(std::ostream & out) const {
m_kernel.display_istatistics(out);
}
void set_cancel(bool f) {
m_kernel.set_cancel_flag(f);
}
bool canceled() {
return m_kernel.get_cancel_flag();
}
void updt_params(params_ref const & p) {
params2front_end_params(p, fparams());
}
};
kernel::kernel(ast_manager & m, front_end_params & fp, params_ref const & p) {
m_imp = alloc(imp, m, fp, p);
}
kernel::~kernel() {
dealloc(m_imp);
}
ast_manager & kernel::m() const {
return m_imp->m();
}
bool kernel::set_logic(symbol logic) {
return m_imp->set_logic(logic);
}
void kernel::set_progress_callback(progress_callback * callback) {
m_imp->set_progress_callback(callback);
}
void kernel::assert_expr(expr * e) {
m_imp->assert_expr(e);
}
void kernel::assert_expr(expr * e, proof * pr) {
m_imp->assert_expr(e, pr);
}
unsigned kernel::size() const {
return m_imp->size();
}
expr * const * kernel::get_formulas() const {
return m_imp->get_formulas();
}
bool kernel::reduce() {
return m_imp->reduce();
}
void kernel::push() {
m_imp->push();
}
void kernel::pop(unsigned num_scopes) {
m_imp->pop(num_scopes);
}
unsigned kernel::get_scope_level() const {
return m_imp->get_scope_level();
}
void kernel::reset() {
ast_manager & _m = m();
front_end_params & fps = m_imp->fparams();
params_ref ps = m_imp->params();
#pragma omp critical (smt_kernel)
{
dealloc(m_imp);
m_imp = alloc(imp, _m, fps, ps);
}
}
bool kernel::inconsistent() {
return m_imp->inconsistent();
}
lbool kernel::setup_and_check() {
set_cancel(false);
return m_imp->setup_and_check();
}
lbool kernel::check(unsigned num_assumptions, expr * const * assumptions) {
set_cancel(false);
lbool r = m_imp->check(num_assumptions, assumptions);
TRACE("smt_kernel", tout << "check result: " << r << "\n";);
return r;
}
void kernel::get_model(model_ref & m) const {
m_imp->get_model(m);
}
proof * kernel::get_proof() {
return m_imp->get_proof();
}
unsigned kernel::get_unsat_core_size() const {
return m_imp->get_unsat_core_size();
}
expr * kernel::get_unsat_core_expr(unsigned idx) const {
return m_imp->get_unsat_core_expr(idx);
}
failure kernel::last_failure() const {
return m_imp->last_failure();
}
std::string kernel::last_failure_as_string() const {
return m_imp->last_failure_as_string();
}
void kernel::get_assignments(expr_ref_vector & result) {
m_imp->get_assignments(result);
}
void kernel::get_relevant_labels(expr * cnstr, buffer<symbol> & result) {
m_imp->get_relevant_labels(cnstr, result);
}
void kernel::get_relevant_labeled_literals(bool at_lbls, expr_ref_vector & result) {
m_imp->get_relevant_labeled_literals(at_lbls, result);
}
void kernel::get_relevant_literals(expr_ref_vector & result) {
m_imp->get_relevant_literals(result);
}
void kernel::get_guessed_literals(expr_ref_vector & result) {
m_imp->get_guessed_literals(result);
}
void kernel::display(std::ostream & out) const {
m_imp->display(out);
}
void kernel::collect_statistics(::statistics & st) const {
m_imp->collect_statistics(st);
}
void kernel::reset_statistics() {
m_imp->reset_statistics();
}
void kernel::display_statistics(std::ostream & out) const {
m_imp->display_statistics(out);
}
void kernel::display_istatistics(std::ostream & out) const {
m_imp->display_istatistics(out);
}
void kernel::set_cancel(bool f) {
#pragma omp critical (smt_kernel)
{
if (m_imp)
m_imp->set_cancel(f);
}
}
bool kernel::canceled() const {
return m_imp->canceled();
}
void kernel::updt_params(params_ref const & p) {
return m_imp->updt_params(p);
}
void kernel::collect_param_descrs(param_descrs & d) {
solver_front_end_params_descrs(d);
}
context & kernel::get_context() {
return m_imp->m_kernel;
}
};

255
src/smt/smt_kernel.h Normal file
View file

@ -0,0 +1,255 @@
/*++
Copyright (c) 2012 Microsoft Corporation
Module Name:
smt_kernel.h
Abstract:
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:
Leonardo de Moura (leonardo) 2012-02-09.
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_KERNEL_H_
#define _SMT_KERNEL_H_
#include"ast.h"
#include"params.h"
#include"model.h"
#include"lbool.h"
#include"statistics.h"
#include"smt_failure.h"
struct front_end_params;
class progress_callback;
namespace smt {
class enode;
class context;
class kernel {
struct imp;
imp * m_imp;
public:
kernel(ast_manager & m, front_end_params & fp, params_ref const & p = params_ref());
~kernel();
ast_manager & m() const;
/**
\brief Set logic. It must be invoked before any assertions.
Return true if succeeded.
*/
bool set_logic(symbol logic);
/**
brief Set progress meter. Kernel will invoke the callback from time to time.
*/
void set_progress_callback(progress_callback * callback);
/**
\brief Assert the given assetion into the logical context.
This method uses the "asserted" proof as a justification for e.
*/
void assert_expr(expr * e);
/**
\brief Assert the given assertion with the given proof as a justification.
*/
void assert_expr(expr * e, proof * pr);
/**
\brief Return the number of asserted formulas in the kernel.
*/
unsigned size() const;
/**
\brief Return the array of asserted formulas.
*/
expr * const * get_formulas() const;
/**
\brief Reduce the set of asserted formulas using preprocessors.
Return true if an inconsistency is detected.
\remark This is mainly used by dl_smt_relation. This method
seens to be misplaced. This is not the right place.
*/
bool reduce();
/**
\brief Create a backtracking point (aka scope level).
*/
void push();
/**
\brief Backtrack the given number of scope levels.
*/
void pop(unsigned num_scopes);
/**
\brief Return the number of backtracking points.
*/
unsigned get_scope_level() const;
/**
\brief Reset the kernel.
All assertions are erased.
*/
void reset();
/**
\brief Return true if the set of asserted formulas is known to be inconsistent.
*/
bool inconsistent();
/**
\brief Setup the logical context and invoke check.
*/
lbool setup_and_check();
/**
\brief Satisfiability check.
*/
lbool check(unsigned num_assumptions = 0, expr * const * assumptions = 0);
/**
\brief Return the model associated with the last check command.
*/
void get_model(model_ref & m) const;
/**
\brief Return the proof of unsatisfiability associated with the last check command.
*/
proof * get_proof();
/**
\brief Return the size of the unsat core associated with the last check command.
*/
unsigned get_unsat_core_size() const;
/**
\brief Return the i-th expression in the unsat core associated with the last check command.
\pre i < get_unsat_core_size()
*/
expr * get_unsat_core_expr(unsigned i) const;
/**
\brief Return the reason for failure for the last check command.
Failure means, it returned l_undef
*/
failure last_failure() const;
/**
\brief Return a string describing the failure.
*/
std::string last_failure_as_string() const;
/**
\brief Return the set of formulas assigned by the kernel.
*/
void get_assignments(expr_ref_vector & result);
/**
\brief Return the set of relevant labels in the last check command.
*/
void get_relevant_labels(expr * cnstr, buffer<symbol> & result);
/**
\brief Return the relevant labeled_literals in the last check command.
*/
void get_relevant_labeled_literals(bool at_lbls, expr_ref_vector & result);
/**
\brief Return the relevant literals in the last check command.
*/
void get_relevant_literals(expr_ref_vector & result);
/**
\brief Return the set of guessed literals (decisions) performed in the last check command.
*/
void get_guessed_literals(expr_ref_vector & result);
/**
\brief (For debubbing purposes) Prints the state of the kernel
*/
void display(std::ostream & out) const;
/**
\brief Collect runtime statistics.
*/
void collect_statistics(::statistics & st) const;
/**
\brief Reset kernel statistics.
*/
void reset_statistics();
/**
\brief Display statistics.
*/
void display_statistics(std::ostream & out) const;
/**
\brief Display statistics in low level format.
*/
void display_istatistics(std::ostream & out) const;
/**
\brief Interrupt the kernel.
*/
void set_cancel(bool f = true);
void cancel() { set_cancel(true); }
/**
\brief Reset interruption.
*/
void reset_cancel() { set_cancel(false); }
/**
\brief Return true if the kernel was interrupted.
*/
bool canceled() const;
/**
\brief Update configuration parameters.
*/
void updt_params(params_ref const & p);
/**
\brief Collect a description of the configuration parameters.
*/
static void collect_param_descrs(param_descrs & d);
/**
\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.
This method breaks the abstraction barrier.
\warning We should not use this method
*/
context & get_context();
};
};
#endif

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);

470
src/smt/smt_solver.cpp
View file

@ -3,351 +3,181 @@ Copyright (c) 2012 Microsoft Corporation
Module Name:
smt_solver.h
smt_solver.cpp
Abstract:
New frontend for the incremental solver.
Wraps smt::kernel as a solver for the external API and cmd_context.
Author:
Leonardo de Moura (leonardo) 2012-02-09.
Leonardo (leonardo) 2012-10-21
Revision History:
Notes:
--*/
#include"smt_solver.h"
#include"smt_context.h"
#include"ast_smt2_pp.h"
#include"params2front_end_params.h"
#include"solver_na2as.h"
#include"smt_kernel.h"
#include"reg_decl_plugins.h"
#include"front_end_params.h"
namespace smt {
struct solver::imp {
smt::context m_kernel;
params_ref m_params;
imp(ast_manager & m, front_end_params & fp, params_ref const & p):
m_kernel(m, fp, p),
m_params(p) {
class solver : public solver_na2as {
front_end_params * m_params;
smt::kernel * m_context;
progress_callback * m_callback;
public:
solver():m_params(0), m_context(0), m_callback(0) {}
virtual ~solver() {
if (m_context != 0)
dealloc(m_context);
}
front_end_params & fparams() {
return m_kernel.get_fparams();
virtual void set_front_end_params(front_end_params & p) {
m_params = &p;
}
params_ref const & params() {
return m_params;
}
ast_manager & m() const {
return m_kernel.get_manager();
virtual void updt_params(params_ref const & p) {
if (m_context == 0)
return;
m_context->updt_params(p);
}
bool set_logic(symbol logic) {
return m_kernel.set_logic(logic);
}
void set_progress_callback(progress_callback * callback) {
return m_kernel.set_progress_callback(callback);
}
void assert_expr(expr * e) {
TRACE("smt_solver", tout << "assert:\n" << mk_ismt2_pp(e, m()) << "\n";);
m_kernel.assert_expr(e);
}
void assert_expr(expr * e, proof * pr) {
m_kernel.assert_expr(e, pr);
}
unsigned size() const {
return m_kernel.get_num_asserted_formulas();
}
expr * const * get_formulas() const {
return m_kernel.get_asserted_formulas();
}
bool reduce() {
return m_kernel.reduce_assertions();
}
void push() {
TRACE("smt_solver", tout << "push()\n";);
m_kernel.push();
}
void pop(unsigned num_scopes) {
TRACE("smt_solver", tout << "pop()\n";);
m_kernel.pop(num_scopes);
}
unsigned get_scope_level() const {
return m_kernel.get_scope_level();
}
lbool setup_and_check() {
return m_kernel.setup_and_check();
}
bool inconsistent() {
return m_kernel.inconsistent();
}
lbool check(unsigned num_assumptions, expr * const * assumptions) {
return m_kernel.check(num_assumptions, assumptions);
}
void get_model(model_ref & m) const {
m_kernel.get_model(m);
}
proof * get_proof() {
return m_kernel.get_proof();
}
unsigned get_unsat_core_size() const {
return m_kernel.get_unsat_core_size();
}
expr * get_unsat_core_expr(unsigned idx) const {
return m_kernel.get_unsat_core_expr(idx);
}
failure last_failure() const {
return m_kernel.get_last_search_failure();
}
std::string last_failure_as_string() const {
return m_kernel.last_failure_as_string();
}
void get_assignments(expr_ref_vector & result) {
m_kernel.get_assignments(result);
}
void get_relevant_labels(expr * cnstr, buffer<symbol> & result) {
m_kernel.get_relevant_labels(cnstr, result);
}
void get_relevant_labeled_literals(bool at_lbls, expr_ref_vector & result) {
m_kernel.get_relevant_labeled_literals(at_lbls, result);
}
void get_relevant_literals(expr_ref_vector & result) {
m_kernel.get_relevant_literals(result);
}
void get_guessed_literals(expr_ref_vector & result) {
m_kernel.get_guessed_literals(result);
}
void display(std::ostream & out) const {
// m_kernel.display(out); <<< for external users it is just junk
// 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";
for (unsigned i = 0; i < num; i++) {
out << "\n " << mk_ismt2_pp(fms[i], m(), 2);
virtual void collect_param_descrs(param_descrs & r) {
if (m_context == 0) {
ast_manager m;
reg_decl_plugins(m);
front_end_params p;
smt::kernel s(m, p);
s.collect_param_descrs(r);
}
else {
m_context->collect_param_descrs(r);
}
out << ")";
}
void collect_statistics(::statistics & st) const {
m_kernel.collect_statistics(st);
}
void reset_statistics() {
}
void display_statistics(std::ostream & out) const {
m_kernel.display_statistics(out);
}
void display_istatistics(std::ostream & out) const {
m_kernel.display_istatistics(out);
virtual void init_core(ast_manager & m, symbol const & logic) {
SASSERT(m_params);
reset();
#pragma omp critical (solver)
{
m_context = alloc(smt::kernel, m, *m_params);
if (m_callback)
m_context->set_progress_callback(m_callback);
}
if (logic != symbol::null)
m_context->set_logic(logic);
}
void set_cancel(bool f) {
m_kernel.set_cancel_flag(f);
}
bool canceled() {
return m_kernel.get_cancel_flag();
virtual void collect_statistics(statistics & st) const {
if (m_context == 0) {
return;
}
else {
m_context->collect_statistics(st);
}
}
void updt_params(params_ref const & p) {
params2front_end_params(p, fparams());
virtual void reset_core() {
if (m_context != 0) {
#pragma omp critical (solver)
{
dealloc(m_context);
m_context = 0;
}
}
}
virtual void assert_expr(expr * t) {
SASSERT(m_context);
m_context->assert_expr(t);
}
virtual void push_core() {
SASSERT(m_context);
m_context->push();
}
virtual void pop_core(unsigned n) {
SASSERT(m_context);
m_context->pop(n);
}
virtual lbool check_sat_core(unsigned num_assumptions, expr * const * assumptions) {
SASSERT(m_context);
TRACE("solver_na2as", tout << "smt_solver::check_sat_core: " << num_assumptions << "\n";);
return m_context->check(num_assumptions, assumptions);
}
virtual void get_unsat_core(ptr_vector<expr> & r) {
SASSERT(m_context);
unsigned sz = m_context->get_unsat_core_size();
for (unsigned i = 0; i < sz; i++)
r.push_back(m_context->get_unsat_core_expr(i));
}
virtual void get_model(model_ref & m) {
SASSERT(m_context);
m_context->get_model(m);
}
virtual proof * get_proof() {
SASSERT(m_context);
return m_context->get_proof();
}
virtual std::string reason_unknown() const {
SASSERT(m_context);
return m_context->last_failure_as_string();
}
virtual void get_labels(svector<symbol> & r) {
SASSERT(m_context);
buffer<symbol> tmp;
m_context->get_relevant_labels(0, tmp);
r.append(tmp.size(), tmp.c_ptr());
}
virtual void set_cancel(bool f) {
#pragma omp critical (solver)
{
if (m_context)
m_context->set_cancel(f);
}
}
virtual void set_progress_callback(progress_callback * callback) {
m_callback = callback;
if (m_context)
m_context->set_progress_callback(callback);
}
virtual unsigned get_num_assertions() const {
if (m_context)
return m_context->size();
else
return 0;
}
virtual expr * get_assertion(unsigned idx) const {
SASSERT(m_context);
SASSERT(idx < get_num_assertions());
return m_context->get_formulas()[idx];
}
virtual void display(std::ostream & out) const {
if (m_context)
m_context->display(out);
else
out << "(solver)";
}
};
solver::solver(ast_manager & m, front_end_params & fp, params_ref const & p) {
m_imp = alloc(imp, m, fp, p);
}
solver::~solver() {
dealloc(m_imp);
}
ast_manager & solver::m() const {
return m_imp->m();
}
bool solver::set_logic(symbol logic) {
return m_imp->set_logic(logic);
}
void solver::set_progress_callback(progress_callback * callback) {
m_imp->set_progress_callback(callback);
}
void solver::assert_expr(expr * e) {
m_imp->assert_expr(e);
}
void solver::assert_expr(expr * e, proof * pr) {
m_imp->assert_expr(e, pr);
}
unsigned solver::size() const {
return m_imp->size();
}
expr * const * solver::get_formulas() const {
return m_imp->get_formulas();
}
bool solver::reduce() {
return m_imp->reduce();
}
void solver::push() {
m_imp->push();
}
void solver::pop(unsigned num_scopes) {
m_imp->pop(num_scopes);
}
unsigned solver::get_scope_level() const {
return m_imp->get_scope_level();
}
void solver::reset() {
ast_manager & _m = m();
front_end_params & fps = m_imp->fparams();
params_ref ps = m_imp->params();
#pragma omp critical (smt_solver)
{
dealloc(m_imp);
m_imp = alloc(imp, _m, fps, ps);
}
}
bool solver::inconsistent() {
return m_imp->inconsistent();
}
lbool solver::setup_and_check() {
set_cancel(false);
return m_imp->setup_and_check();
}
lbool solver::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";);
return r;
}
void solver::get_model(model_ref & m) const {
m_imp->get_model(m);
}
proof * solver::get_proof() {
return m_imp->get_proof();
}
unsigned solver::get_unsat_core_size() const {
return m_imp->get_unsat_core_size();
}
expr * solver::get_unsat_core_expr(unsigned idx) const {
return m_imp->get_unsat_core_expr(idx);
}
failure solver::last_failure() const {
return m_imp->last_failure();
}
std::string solver::last_failure_as_string() const {
return m_imp->last_failure_as_string();
}
void solver::get_assignments(expr_ref_vector & result) {
m_imp->get_assignments(result);
}
void solver::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) {
m_imp->get_relevant_labeled_literals(at_lbls, result);
}
void solver::get_relevant_literals(expr_ref_vector & result) {
m_imp->get_relevant_literals(result);
}
void solver::get_guessed_literals(expr_ref_vector & result) {
m_imp->get_guessed_literals(result);
}
void solver::display(std::ostream & out) const {
m_imp->display(out);
}
void solver::collect_statistics(::statistics & st) const {
m_imp->collect_statistics(st);
}
void solver::reset_statistics() {
m_imp->reset_statistics();
}
void solver::display_statistics(std::ostream & out) const {
m_imp->display_statistics(out);
}
void solver::display_istatistics(std::ostream & out) const {
m_imp->display_istatistics(out);
}
void solver::set_cancel(bool f) {
#pragma omp critical (smt_solver)
{
if (m_imp)
m_imp->set_cancel(f);
}
}
bool solver::canceled() const {
return m_imp->canceled();
}
void solver::updt_params(params_ref const & p) {
return m_imp->updt_params(p);
}
void solver::collect_param_descrs(param_descrs & d) {
solver_front_end_params_descrs(d);
}
context & solver::kernel() {
return m_imp->m_kernel;
}
};
solver * mk_smt_solver() {
return alloc(smt::solver);
}

235
src/smt/smt_solver.h
View file

@ -7,241 +7,22 @@ Module Name:
Abstract:
New frontend for the incremental solver.
Wraps smt::kernel as a solver for the external API and cmd_context.
Author:
Leonardo de Moura (leonardo) 2012-02-09.
Leonardo (leonardo) 2012-10-21
Revision History:
Notes:
This file was called default_solver.h. It was a bad name.
--*/
#ifndef _SMT_SOLVER_H_
#define _SMT_SOLVER_H_
#include"ast.h"
#include"params.h"
#include"model.h"
#include"lbool.h"
#include"statistics.h"
#include"smt_failure.h"
class solver;
struct front_end_params;
class progress_callback;
namespace smt {
class enode;
class context;
class solver {
struct imp;
imp * m_imp;
public:
solver(ast_manager & m, front_end_params & fp, params_ref const & p = params_ref());
~solver();
ast_manager & m() const;
/**
\brief Set logic. It must be invoked before any assertions.
Return true if succeeded.
*/
bool set_logic(symbol logic);
/**
brief Set progress meter. Solver will invoke the callback from time to time.
*/
void set_progress_callback(progress_callback * callback);
/**
\brief Assert the given assetion into the logical context.
This method uses the "asserted" proof as a justification for e.
*/
void assert_expr(expr * e);
/**
\brief Assert the given assertion with the given proof as a justification.
*/
void assert_expr(expr * e, proof * pr);
/**
\brief Return the number of asserted formulas in the solver.
*/
unsigned size() const;
/**
\brief Return the array of asserted formulas.
*/
expr * const * get_formulas() const;
/**
\brief Reduce the set of asserted formulas using preprocessors.
Return true if an inconsistency is detected.
\remark This is mainly used by dl_smt_relation. This method
seens to be misplaced. This is not the right place.
*/
bool reduce();
/**
\brief Create a backtracking point (aka scope level).
*/
void push();
/**
\brief Backtrack the given number of scope levels.
*/
void pop(unsigned num_scopes);
/**
\brief Return the number of backtracking points.
*/
unsigned get_scope_level() const;
/**
\brief Reset the solver.
All assertions are erased.
*/
void reset();
/**
\brief Return true if the set of asserted formulas is known to be inconsistent.
*/
bool inconsistent();
/**
\brief Setup the logical context and invoke check.
*/
lbool setup_and_check();
/**
\brief Satisfiability check.
*/
lbool check(unsigned num_assumptions = 0, expr * const * assumptions = 0);
/**
\brief Return the model associated with the last check command.
*/
void get_model(model_ref & m) const;
/**
\brief Return the proof of unsatisfiability associated with the last check command.
*/
proof * get_proof();
/**
\brief Return the size of the unsat core associated with the last check command.
*/
unsigned get_unsat_core_size() const;
/**
\brief Return the i-th expression in the unsat core associated with the last check command.
\pre i < get_unsat_core_size()
*/
expr * get_unsat_core_expr(unsigned i) const;
/**
\brief Return the reason for failure for the last check command.
Failure means, it returned l_undef
*/
failure last_failure() const;
/**
\brief Return a string describing the failure.
*/
std::string last_failure_as_string() const;
/**
\brief Return the set of formulas assigned by the solver.
*/
void get_assignments(expr_ref_vector & result);
/**
\brief Return the set of relevant labels in the last check command.
*/
void get_relevant_labels(expr * cnstr, buffer<symbol> & result);
/**
\brief Return the relevant labeled_literals in the last check command.
*/
void get_relevant_labeled_literals(bool at_lbls, expr_ref_vector & result);
/**
\brief Return the relevant literals in the last check command.
*/
void get_relevant_literals(expr_ref_vector & result);
/**
\brief Return the set of guessed literals (decisions) performed in the last check command.
*/
void get_guessed_literals(expr_ref_vector & result);
/**
\brief (For debubbing purposes) Prints the state of the solver
*/
void display(std::ostream & out) const;
/**
\brief Collect runtime statistics.
*/
void collect_statistics(::statistics & st) const;
/**
\brief Reset solver statistics.
*/
void reset_statistics();
/**
\brief Display statistics.
*/
void display_statistics(std::ostream & out) const;
/**
\brief Display statistics in low level format.
*/
void display_istatistics(std::ostream & out) const;
/**
\brief Interrupt the solver.
*/
void set_cancel(bool f = true);
void cancel() { set_cancel(true); }
/**
\brief Reset interruption.
*/
void reset_cancel() { set_cancel(false); }
/**
\brief Return true if the solver was interrupted.
*/
bool canceled() const;
/**
\brief Update configuration parameters.
*/
void updt_params(params_ref const & p);
/**
\brief Collect a description of the configuration parameters.
*/
static void collect_param_descrs(param_descrs & d);
/**
\brief Return a reference to the kernel.
This is a temporary hack to support user theories.
TODO: remove this hack.
We need to revamp user theories too.
This method breaks the abstraction barrier.
\warning We should not use this method
*/
context & kernel();
};
};
solver * mk_smt_solver();
#endif

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;

2
src/smt/theory_diff_logic.cpp
View file

@ -22,9 +22,11 @@ Revision History:
#include"rational.h"
#include"theory_diff_logic_def.h"
namespace smt {
template class theory_diff_logic<idl_ext>;
template class theory_diff_logic<sidl_ext>;
template class theory_diff_logic<rdl_ext>;
template class theory_diff_logic<srdl_ext>;
};

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);
};

24
src/smt/user_rewriter.cpp
View file

@ -1,24 +0,0 @@
/*++
Copyright (c) 2012 Microsoft Corporation
Module Name:
user_rewriter.cpp
Abstract:
Rewriter for applying user-defined rewrite routine.
Author:
Nikolaj (nbjorner) 2012-01-08
Notes:
--*/
#include "rewriter_def.h"
#include "user_rewriter.h"
template class rewriter_tpl<user_rewriter>;

58
src/smt/user_rewriter.h
View file

@ -1,58 +0,0 @@
/*++
Copyright (c) 2011 Microsoft Corporation
Module Name:
user_rewriter.h
Abstract:
Rewriter for applying user-defined rewrite routine.
Author:
Nikolaj (nbjorner) 2012-01-08
Notes:
--*/
#ifndef _USER_REWRITER_H_
#define _USER_REWRITER_H_
#include "ast.h"
#include "rewriter.h"
class user_rewriter : public default_rewriter_cfg {
public:
typedef bool fn(void* context, expr* expr_in, expr** expr_out, proof** proof_out);
private:
ast_manager& m;
rewriter_tpl<user_rewriter> m_rw;
void* m_ctx;
fn* m_rewriter;
bool m_rec;
public:
user_rewriter(ast_manager & m): m(m), m_rw(m, m.proofs_enabled(), *this), m_rewriter(0), m_rec(false) {}
~user_rewriter() {}
void set_rewriter(void * ctx, fn* rw) { m_ctx = ctx; m_rewriter = rw; }
bool enabled() { return m_rewriter != 0; }
void operator()(expr_ref& term) { expr_ref tmp(m); (*this)(tmp, term); }
void operator()(expr * t, expr_ref & result) { proof_ref pr(m); (*this)(t, result, pr); }
void operator()(expr * t, expr_ref & result, proof_ref & result_pr) { m_rw(t, result, result_pr); }
void cancel() { set_cancel(true); }
void reset_cancel() { set_cancel(false); }
void set_cancel(bool f) { m_rw.set_cancel(f); }
void cleanup() { if (!m_rec) { m_rec = true; m_rw.cleanup(); m_rec = false; } }
void reset() { if (!m_rec) { m_rec = true; m_rw.reset(); m_rec = false; } }
bool get_subst(expr* s, expr*& t, proof*& t_pr) {
return enabled() && m_rewriter(m_ctx, s, &t, &t_pr);
}
};
#endif

10
src/solver/solver.h
View file

@ -70,7 +70,8 @@ public:
/**
\brief Enable/Disable model generation for this solver object.
It is invoked before init(m, logic).
It is invoked before init(m, logic).
The user may optionally invoke it after init(m, logic).
*/
virtual void set_produce_models(bool f) {}
/**
@ -95,6 +96,13 @@ public:
*/
virtual void assert_expr(expr * t) = 0;
/**
\brief Add a new formula \c t to the assertion stack, and "tag" it with \c a.
The propositional varialbe \c a is used to track the use of \c t in a proof
of unsatisfiability.
*/
virtual void assert_expr(expr * t, expr * a) = 0;
/**
\brief Create a backtracking point.
*/

101
src/solver/solver_na2as.cpp Normal file
View file

@ -0,0 +1,101 @@
/*++
Copyright (c) 2012 Microsoft Corporation
Module Name:
solver_na2as.cpp
Abstract:
Solver that implements "named" assertions using assumptions (aka answer literals).
That is, a named assertion assert_expr(t, a) is mapped into
a implies t
and 'a' is used as an extra assumption for check_sat.
Author:
Leonardo (leonardo) 2012-11-02
Notes:
--*/
#include"solver_na2as.h"
#include"ast_smt2_pp.h"
solver_na2as::solver_na2as() {
m_manager = 0;
}
solver_na2as::~solver_na2as() {
restore_assumptions(0);
}
void solver_na2as::assert_expr(expr * t, expr * a) {
SASSERT(m_manager != 0);
SASSERT(is_uninterp_const(a));
SASSERT(m_manager->is_bool(a));
TRACE("solver_na2as", tout << "asserting\n" << mk_ismt2_pp(t, *m_manager) << "\n" << mk_ismt2_pp(a, *m_manager) << "\n";);
m_manager->inc_ref(a);
m_assumptions.push_back(a);
expr_ref new_t(*m_manager);
new_t = m_manager->mk_implies(a, t);
assert_expr(new_t);
}
void solver_na2as::init(ast_manager & m, symbol const & logic) {
SASSERT(m_assumptions.empty());
m_manager = &m;
init_core(m, logic);
}
struct append_assumptions {
ptr_vector<expr> & m_assumptions;
unsigned m_old_sz;
append_assumptions(ptr_vector<expr> & _m_assumptions,
unsigned num_assumptions,
expr * const * assumptions):
m_assumptions(_m_assumptions) {
m_old_sz = m_assumptions.size();
m_assumptions.append(num_assumptions, assumptions);
}
~append_assumptions() {
m_assumptions.shrink(m_old_sz);
}
};
lbool solver_na2as::check_sat(unsigned num_assumptions, expr * const * assumptions) {
append_assumptions app(m_assumptions, num_assumptions, assumptions);
return check_sat_core(m_assumptions.size(), m_assumptions.c_ptr());
}
void solver_na2as::push() {
m_scopes.push_back(m_assumptions.size());
push_core();
}
void solver_na2as::pop(unsigned n) {
pop_core(n);
unsigned lvl = m_scopes.size();
SASSERT(n <= lvl);
unsigned new_lvl = lvl - n;
restore_assumptions(m_scopes[new_lvl]);
m_scopes.shrink(new_lvl);
}
void solver_na2as::restore_assumptions(unsigned old_sz) {
SASSERT(old_sz == 0 || m_manager != 0);
for (unsigned i = old_sz; i < m_assumptions.size(); i++) {
m_manager->dec_ref(m_assumptions[i]);
}
m_assumptions.shrink(old_sz);
}
unsigned solver_na2as::get_scope_level() const {
return m_scopes.size();
}
void solver_na2as::reset() {
reset_core();
restore_assumptions(0);
}

55
src/solver/solver_na2as.h Normal file
View file

@ -0,0 +1,55 @@
/*++
Copyright (c) 2012 Microsoft Corporation
Module Name:
solver_na2as.h
Abstract:
Solver that implements "named" assertions using assumptions (aka answer literals).
That is, a named assertion assert_expr(t, a) is mapped into
a implies t
and 'a' is used as an extra assumption for check_sat.
Author:
Leonardo (leonardo) 2012-11-02
Notes:
--*/
#ifndef _SOLVER_NA2AS_H_
#define _SOLVER_NA2AS_H_
#include"solver.h"
class solver_na2as : public solver {
ast_manager * m_manager;
ptr_vector<expr> m_assumptions;
unsigned_vector m_scopes;
void restore_assumptions(unsigned old_sz);
public:
solver_na2as();
virtual ~solver_na2as();
virtual void assert_expr(expr * t, expr * a);
virtual void assert_expr(expr * t) = 0;
// Subclasses of solver_na2as should redefine the following *_core methods instead of these ones.
virtual void init(ast_manager & m, symbol const & logic);
virtual lbool check_sat(unsigned num_assumptions, expr * const * assumptions);
virtual void push();
virtual void pop(unsigned n);
virtual unsigned get_scope_level() const;
virtual void reset();
protected:
virtual void init_core(ast_manager & m, symbol const & logic) = 0;
virtual lbool check_sat_core(unsigned num_assumptions, expr * const * assumptions) = 0;
virtual void push_core() = 0;
virtual void pop_core(unsigned n) = 0;
virtual void reset_core() = 0;
};
#endif

235
src/solver/strategic_solver.cpp
View file

@ -25,7 +25,13 @@ Notes:
// minimum verbosity level for portfolio verbose messages
#define PS_VB_LVL 15
strategic_solver_core::strategic_solver_core():
strategic_solver::ctx::ctx(ast_manager & m):
m_assertions(m),
m_assertion_names(m) {
}
strategic_solver::strategic_solver():
m_manager(0),
m_fparams(0),
m_force_tactic(false),
@ -37,6 +43,7 @@ strategic_solver_core::strategic_solver_core():
m_default_fct(0),
m_curr_tactic(0),
m_proof(0),
m_core(0),
m_callback(0) {
m_use_inc_solver_results = false;
DEBUG_CODE(m_num_scopes = 0;);
@ -45,7 +52,7 @@ strategic_solver_core::strategic_solver_core():
m_produce_unsat_cores = false;
}
strategic_solver_core::~strategic_solver_core() {
strategic_solver::~strategic_solver() {
SASSERT(!m_curr_tactic);
dictionary<tactic_factory*>::iterator it = m_logic2fct.begin();
dictionary<tactic_factory*>::iterator end = m_logic2fct.end();
@ -54,9 +61,11 @@ strategic_solver_core::~strategic_solver_core() {
}
if (m_proof)
m().dec_ref(m_proof);
if (m_core)
m().dec_ref(m_core);
}
bool strategic_solver_core::has_quantifiers() const {
bool strategic_solver::has_quantifiers() const {
unsigned sz = get_num_assertions();
for (unsigned i = 0; i < sz; i++) {
if (::has_quantifiers(get_assertion(i)))
@ -68,7 +77,7 @@ bool strategic_solver_core::has_quantifiers() const {
/**
\brief Return true if a tactic should be used when the incremental solver returns unknown.
*/
bool strategic_solver_core::use_tactic_when_undef() const {
bool strategic_solver::use_tactic_when_undef() const {
switch (m_inc_unknown_behavior) {
case IUB_RETURN_UNDEF: return false;
case IUB_USE_TACTIC_IF_QF: return !has_quantifiers();
@ -79,7 +88,7 @@ bool strategic_solver_core::use_tactic_when_undef() const {
}
}
void strategic_solver_core::set_inc_solver(solver * s) {
void strategic_solver::set_inc_solver(solver * s) {
SASSERT(m_inc_solver == 0);
SASSERT(m_num_scopes == 0);
m_inc_solver = s;
@ -87,7 +96,7 @@ void strategic_solver_core::set_inc_solver(solver * s) {
m_inc_solver->set_progress_callback(m_callback);
}
void strategic_solver_core::updt_params(params_ref const & p) {
void strategic_solver::updt_params(params_ref const & p) {
if (m_inc_solver)
m_inc_solver->updt_params(p);
if (m_fparams)
@ -95,7 +104,7 @@ void strategic_solver_core::updt_params(params_ref const & p) {
}
void strategic_solver_core::collect_param_descrs(param_descrs & r) {
void strategic_solver::collect_param_descrs(param_descrs & r) {
if (m_inc_solver)
m_inc_solver->collect_param_descrs(r);
}
@ -105,7 +114,7 @@ void strategic_solver_core::collect_param_descrs(param_descrs & r) {
timeout == UINT_MAX means infinite
After the timeout a strategy is used.
*/
void strategic_solver_core::set_inc_solver_timeout(unsigned timeout) {
void strategic_solver::set_inc_solver_timeout(unsigned timeout) {
m_inc_solver_timeout = timeout;
}
@ -113,14 +122,14 @@ void strategic_solver_core::set_inc_solver_timeout(unsigned timeout) {
\brief Set the default tactic factory.
It is used if there is no tactic for a given logic.
*/
void strategic_solver_core::set_default_tactic(tactic_factory * fct) {
void strategic_solver::set_default_tactic(tactic_factory * fct) {
m_default_fct = fct;
}
/**
\brief Set a tactic factory for a given logic.
*/
void strategic_solver_core::set_tactic_for(symbol const & logic, tactic_factory * fct) {
void strategic_solver::set_tactic_for(symbol const & logic, tactic_factory * fct) {
tactic_factory * old_fct;
if (m_logic2fct.find(logic, old_fct)) {
dealloc(old_fct);
@ -128,31 +137,77 @@ void strategic_solver_core::set_tactic_for(symbol const & logic, tactic_factory
m_logic2fct.insert(logic, fct);
}
void strategic_solver_core::init(ast_manager & m, symbol const & logic) {
void strategic_solver::init(ast_manager & m, symbol const & logic) {
m_manager = &m;
m_logic = logic;
if (m_inc_mode) {
SASSERT(m_inc_solver);
m_inc_solver->init(m, logic);
}
m_ctx = alloc(ctx, m);
TRACE("strategic_solver", tout << "strategic_solver was initialized.\n";);
}
unsigned strategic_solver::get_num_assertions() const {
if (m_ctx == 0)
return 0;
return m_ctx->m_assertions.size();
}
expr * strategic_solver::get_assertion(unsigned idx) const {
SASSERT(m_ctx);
return m_ctx->m_assertions.get(idx);
}
expr * strategic_solver::get_assertion_name(unsigned idx) const {
SASSERT(m_ctx);
SASSERT(m_produce_unsat_cores);
return m_ctx->m_assertion_names.get(idx);
}
void strategic_solver::set_produce_proofs(bool f) {
m_produce_proofs = f;
// do not need to propagate to inc_solver since flag cannot be changed after initialization
}
void strategic_solver::set_produce_models(bool f) {
m_produce_models = f;
if (m_inc_solver)
m_inc_solver->set_produce_models(f);
}
void strategic_solver::set_produce_unsat_cores(bool f) {
m_produce_unsat_cores = f;
// do not need to propagate to inc_solver since flag cannot be changed after initialization
}
// delayed inc solver initialization
void strategic_solver_core::init_inc_solver() {
void strategic_solver::init_inc_solver() {
if (m_inc_mode)
return; // solver was already initialized
if (!m_inc_solver)
return; // inc solver was not installed
m_inc_mode = true;
m_inc_solver->set_produce_proofs(m_produce_proofs);
m_inc_solver->set_produce_models(m_produce_models);
m_inc_solver->set_produce_unsat_cores(m_produce_unsat_cores);
m_inc_solver->set_front_end_params(*m_fparams);
m_inc_solver->init(m(), m_logic);
unsigned sz = get_num_assertions();
for (unsigned i = 0; i < sz; i++) {
m_inc_solver->assert_expr(get_assertion(i));
if (m_produce_unsat_cores) {
SASSERT(m_ctx->m_assertions.size() == m_ctx->m_assertion_names.size());
for (unsigned i = 0; i < sz; i++) {
m_inc_solver->assert_expr(get_assertion(i), get_assertion_name(i));
}
}
else {
for (unsigned i = 0; i < sz; i++) {
m_inc_solver->assert_expr(get_assertion(i));
}
}
}
void strategic_solver_core::collect_statistics(statistics & st) const {
void strategic_solver::collect_statistics(statistics & st) const {
if (m_use_inc_solver_results) {
SASSERT(m_inc_solver);
m_inc_solver->collect_statistics(st);
@ -165,7 +220,8 @@ void strategic_solver_core::collect_statistics(statistics & st) const {
}
}
void strategic_solver_core::reset() {
void strategic_solver::reset() {
m_ctx = 0;
m_logic = symbol::null;
m_inc_mode = false;
m_check_sat_executed = false;
@ -176,18 +232,22 @@ void strategic_solver_core::reset() {
reset_results();
}
void strategic_solver_core::reset_results() {
void strategic_solver::reset_results() {
m_use_inc_solver_results = false;
m_model = 0;
if (m_proof) {
m().dec_ref(m_proof);
m_proof = 0;
}
if (m_core) {
m().dec_ref(m_core);
m_core = 0;
}
m_reason_unknown.clear();
m_stats.reset();
}
void strategic_solver_core::assert_expr(expr * t) {
void strategic_solver::assert_expr(expr * t) {
if (m_check_sat_executed && !m_inc_mode) {
// a check sat was already executed --> switch to incremental mode
init_inc_solver();
@ -197,16 +257,37 @@ void strategic_solver_core::assert_expr(expr * t) {
SASSERT(m_inc_solver);
m_inc_solver->assert_expr(t);
}
SASSERT(m_ctx);
m_ctx->m_assertions.push_back(t);
if (m_produce_unsat_cores)
m_ctx->m_assertion_names.push_back(0);
}
void strategic_solver_core::push() {
void strategic_solver::assert_expr(expr * t, expr * a) {
if (m_check_sat_executed && !m_inc_mode) {
// a check sat was already executed --> switch to incremental mode
init_inc_solver();
SASSERT(m_inc_solver == 0 || m_inc_mode);
}
if (m_inc_mode) {
SASSERT(m_inc_solver);
m_inc_solver->assert_expr(t, a);
}
SASSERT(m_ctx);
m_ctx->m_assertions.push_back(t);
if (m_produce_unsat_cores)
m_ctx->m_assertion_names.push_back(a);
}
void strategic_solver::push() {
DEBUG_CODE(m_num_scopes++;);
init_inc_solver();
if (m_inc_solver)
m_inc_solver->push();
m_ctx->m_scopes.push_back(m_ctx->m_assertions.size());
}
void strategic_solver_core::pop(unsigned n) {
void strategic_solver::pop(unsigned n) {
DEBUG_CODE({
SASSERT(n <= m_num_scopes);
m_num_scopes -= n;
@ -214,13 +295,20 @@ void strategic_solver_core::pop(unsigned n) {
init_inc_solver();
if (m_inc_solver)
m_inc_solver->pop(n);
SASSERT(m_ctx);
unsigned new_lvl = m_ctx->m_scopes.size() - n;
unsigned old_sz = m_ctx->m_scopes[new_lvl];
m_ctx->m_assertions.shrink(old_sz);
if (m_produce_unsat_cores)
m_ctx->m_assertion_names.shrink(old_sz);
m_ctx->m_scopes.shrink(new_lvl);
}
unsigned strategic_solver_core::get_scope_level() const {
if (m_inc_solver)
return m_inc_solver->get_scope_level();
else
unsigned strategic_solver::get_scope_level() const {
if (m_ctx == 0)
return 0;
return m_ctx->m_assertions.size();
}
struct aux_timeout_eh : public event_handler {
@ -233,10 +321,10 @@ struct aux_timeout_eh : public event_handler {
}
};
struct strategic_solver_core::mk_tactic {
strategic_solver_core * m_solver;
struct strategic_solver::mk_tactic {
strategic_solver * m_solver;
mk_tactic(strategic_solver_core * s, tactic_factory * f):m_solver(s) {
mk_tactic(strategic_solver * s, tactic_factory * f):m_solver(s) {
ast_manager & m = s->m();
params_ref p;
front_end_params2params(*s->m_fparams, p);
@ -259,14 +347,14 @@ struct strategic_solver_core::mk_tactic {
}
};
tactic_factory * strategic_solver_core::get_tactic_factory() const {
tactic_factory * strategic_solver::get_tactic_factory() const {
tactic_factory * f = 0;
if (m_logic2fct.find(m_logic, f))
return f;
return m_default_fct.get();
}
lbool strategic_solver_core::check_sat_with_assumptions(unsigned num_assumptions, expr * const * assumptions) {
lbool strategic_solver::check_sat_with_assumptions(unsigned num_assumptions, expr * const * assumptions) {
if (!m_inc_solver) {
IF_VERBOSE(PS_VB_LVL, verbose_stream() << "incremental solver was not installed, returning unknown...\n";);
m_use_inc_solver_results = false;
@ -275,10 +363,16 @@ lbool strategic_solver_core::check_sat_with_assumptions(unsigned num_assumptions
}
init_inc_solver();
m_use_inc_solver_results = true;
TRACE("strategic_solver", tout << "invoking inc_solver with " << num_assumptions << " assumptions\n";);
return m_inc_solver->check_sat(num_assumptions, assumptions);
}
lbool strategic_solver_core::check_sat(unsigned num_assumptions, expr * const * assumptions) {
lbool strategic_solver::check_sat(unsigned num_assumptions, expr * const * assumptions) {
TRACE("strategic_solver", tout << "assumptions at strategic_solver:\n";
for (unsigned i = 0; i < num_assumptions; i++) {
tout << mk_ismt2_pp(assumptions[i], m()) << "\n";
}
tout << "m_produce_unsat_cores: " << m_produce_unsat_cores << ", m_inc_mode: " << m_inc_mode << "\n";);
reset_results();
m_check_sat_executed = true;
if (num_assumptions > 0 || // assumptions were provided
@ -333,10 +427,18 @@ lbool strategic_solver_core::check_sat(unsigned num_assumptions, expr * const *
goal_ref g = alloc(goal, m(), m_produce_proofs, m_produce_models, m_produce_unsat_cores);
unsigned sz = get_num_assertions();
for (unsigned i = 0; i < sz; i++) {
g->assert_expr(get_assertion(i));
if (m_produce_unsat_cores) {
SASSERT(m_ctx->m_assertions.size() == m_ctx->m_assertion_names.size());
for (unsigned i = 0; i < sz; i++)
g->assert_expr(get_assertion(i), get_assertion_name(i));
}
else {
for (unsigned i = 0; i < sz; i++)
g->assert_expr(get_assertion(i));
}
expr_dependency_ref core(m());
TRACE("strategic_solver", tout << "using goal...\n"; g->display_with_dependencies(tout););
mk_tactic tct_maker(this, factory);
SASSERT(m_curr_tactic);
@ -348,10 +450,14 @@ lbool strategic_solver_core::check_sat(unsigned num_assumptions, expr * const *
m_proof = pr;
m().inc_ref(m_proof);
}
if (core) {
m_core = core;
m().inc_ref(m_core);
}
return r;
}
void strategic_solver_core::set_cancel(bool f) {
void strategic_solver::set_cancel(bool f) {
if (m_inc_solver)
m_inc_solver->set_cancel(f);
#pragma omp critical (strategic_solver)
@ -361,14 +467,18 @@ void strategic_solver_core::set_cancel(bool f) {
}
}
void strategic_solver_core::get_unsat_core(ptr_vector<expr> & r) {
void strategic_solver::get_unsat_core(ptr_vector<expr> & r) {
TRACE("strategic_solver", tout << "get_unsat_core, m_use_inc_solver_results: " << m_use_inc_solver_results << "\n";);
if (m_use_inc_solver_results) {
SASSERT(m_inc_solver);
m_inc_solver->get_unsat_core(r);
}
else {
m().linearize(m_core, r);
}
}
void strategic_solver_core::get_model(model_ref & m) {
void strategic_solver::get_model(model_ref & m) {
if (m_use_inc_solver_results) {
SASSERT(m_inc_solver);
m_inc_solver->get_model(m);
@ -378,7 +488,7 @@ void strategic_solver_core::get_model(model_ref & m) {
}
}
proof * strategic_solver_core::get_proof() {
proof * strategic_solver::get_proof() {
if (m_use_inc_solver_results) {
SASSERT(m_inc_solver);
return m_inc_solver->get_proof();
@ -388,7 +498,7 @@ proof * strategic_solver_core::get_proof() {
}
}
std::string strategic_solver_core::reason_unknown() const {
std::string strategic_solver::reason_unknown() const {
if (m_use_inc_solver_results) {
SASSERT(m_inc_solver);
return m_inc_solver->reason_unknown();
@ -396,20 +506,20 @@ std::string strategic_solver_core::reason_unknown() const {
return m_reason_unknown;
}
void strategic_solver_core::get_labels(svector<symbol> & r) {
void strategic_solver::get_labels(svector<symbol> & r) {
if (m_use_inc_solver_results) {
SASSERT(m_inc_solver);
m_inc_solver->get_labels(r);
}
}
void strategic_solver_core::set_progress_callback(progress_callback * callback) {
void strategic_solver::set_progress_callback(progress_callback * callback) {
m_callback = callback;
if (m_inc_solver)
m_inc_solver->set_progress_callback(callback);
}
void strategic_solver_core::display(std::ostream & out) const {
void strategic_solver::display(std::ostream & out) const {
if (m_manager) {
unsigned num = get_num_assertions();
out << "(solver";
@ -424,50 +534,7 @@ void strategic_solver_core::display(std::ostream & out) const {
}
strategic_solver::ctx::ctx(ast_manager & m):m_assertions(m) {
}
void strategic_solver::init(ast_manager & m, symbol const & logic) {
strategic_solver_core::init(m, logic);
m_ctx = alloc(ctx, m);
}
unsigned strategic_solver::get_num_assertions() const {
if (m_ctx == 0)
return 0;
return m_ctx->m_assertions.size();
}
expr * strategic_solver::get_assertion(unsigned idx) const {
SASSERT(m_ctx);
return m_ctx->m_assertions.get(idx);
}
void strategic_solver::assert_expr(expr * t) {
SASSERT(m_ctx);
strategic_solver_core::assert_expr(t);
m_ctx->m_assertions.push_back(t);
}
void strategic_solver::push() {
SASSERT(m_ctx);
strategic_solver_core::push();
m_ctx->m_scopes.push_back(m_ctx->m_assertions.size());
}
void strategic_solver::pop(unsigned n) {
SASSERT(m_ctx);
unsigned new_lvl = m_ctx->m_scopes.size() - n;
unsigned old_sz = m_ctx->m_scopes[new_lvl];
m_ctx->m_assertions.shrink(old_sz);
m_ctx->m_scopes.shrink(new_lvl);
strategic_solver_core::pop(n);
}
void strategic_solver::reset() {
m_ctx = 0;
strategic_solver_core::reset();
}

55
src/solver/strategic_solver.h
View file

@ -46,7 +46,7 @@ struct front_end_params;
It goes back to non_incremental mode when:
- reset is invoked.
*/
class strategic_solver_core : public solver {
class strategic_solver : public solver {
public:
// Behavior when the incremental solver returns unknown.
enum inc_unknown_behavior {
@ -73,9 +73,18 @@ private:
bool m_use_inc_solver_results;
model_ref m_model;
proof * m_proof;
expr_dependency * m_core;
std::string m_reason_unknown;
statistics m_stats;
struct ctx {
expr_ref_vector m_assertions;
expr_ref_vector m_assertion_names;
unsigned_vector m_scopes;
ctx(ast_manager & m);
};
scoped_ptr<ctx> m_ctx;
#ifdef Z3DEBUG
unsigned m_num_scopes;
#endif
@ -97,8 +106,8 @@ private:
bool use_tactic_when_undef() const;
public:
strategic_solver_core();
~strategic_solver_core();
strategic_solver();
~strategic_solver();
ast_manager & m() const { SASSERT(m_manager); return *m_manager; }
@ -114,19 +123,21 @@ public:
virtual void updt_params(params_ref const & p);
virtual void collect_param_descrs(param_descrs & r);
virtual void set_produce_proofs(bool f) { m_produce_proofs = f; }
virtual void set_produce_models(bool f) { m_produce_models = f; }
virtual void set_produce_unsat_cores(bool f) { m_produce_unsat_cores = f; }
virtual void set_produce_proofs(bool f);
virtual void set_produce_models(bool f);
virtual void set_produce_unsat_cores(bool f);
unsigned get_num_assertions() const;
expr * get_assertion(unsigned idx) const;
expr * get_assertion_name(unsigned idx) const;
virtual unsigned get_num_assertions() const = 0;
virtual expr * get_assertion(unsigned idx) const = 0;
virtual void display(std::ostream & out) const;
virtual void init(ast_manager & m, symbol const & logic);
virtual void collect_statistics(statistics & st) const;
virtual void reset();
virtual void assert_expr(expr * t);
virtual void assert_expr(expr * t, expr * a);
virtual void push();
virtual void pop(unsigned n);
virtual unsigned get_scope_level() const;
@ -140,30 +151,4 @@ public:
virtual void set_progress_callback(progress_callback * callback);
};
/**
\brief Default implementation of strategic_solver_core
*/
class strategic_solver : public strategic_solver_core {
struct ctx {
expr_ref_vector m_assertions;
unsigned_vector m_scopes;
ctx(ast_manager & m);
};
scoped_ptr<ctx> m_ctx;
public:
strategic_solver() {}
virtual void init(ast_manager & m, symbol const & logic);
virtual void assert_expr(expr * t);
virtual void push();
virtual void pop(unsigned n);
virtual void reset();
virtual unsigned get_num_assertions() const;
virtual expr * get_assertion(unsigned idx) const;
};
#endif

15
src/solver/tactic2solver.cpp
View file

@ -31,7 +31,7 @@ tactic2solver_core::ctx::ctx(ast_manager & m, symbol const & logic):
tactic2solver_core::~tactic2solver_core() {
}
void tactic2solver_core::init(ast_manager & m, symbol const & logic) {
void tactic2solver_core::init_core(ast_manager & m, symbol const & logic) {
m_ctx = alloc(ctx, m, logic);
}
@ -62,7 +62,7 @@ void tactic2solver_core::collect_param_descrs(param_descrs & r) {
}
}
void tactic2solver_core::reset() {
void tactic2solver_core::reset_core() {
SASSERT(m_ctx);
m_ctx->m_assertions.reset();
m_ctx->m_scopes.reset();
@ -75,13 +75,13 @@ void tactic2solver_core::assert_expr(expr * t) {
m_ctx->m_result = 0;
}
void tactic2solver_core::push() {
void tactic2solver_core::push_core() {
SASSERT(m_ctx);
m_ctx->m_scopes.push_back(m_ctx->m_assertions.size());
m_ctx->m_result = 0;
}
void tactic2solver_core::pop(unsigned n) {
void tactic2solver_core::pop_core(unsigned n) {
SASSERT(m_ctx);
unsigned new_lvl = m_ctx->m_scopes.size() - n;
unsigned old_sz = m_ctx->m_scopes[new_lvl];
@ -90,12 +90,7 @@ void tactic2solver_core::pop(unsigned n) {
m_ctx->m_result = 0;
}
unsigned tactic2solver_core::get_scope_level() const {
SASSERT(m_ctx);
return m_ctx->m_scopes.size();
}
lbool tactic2solver_core::check_sat(unsigned num_assumptions, expr * const * assumptions) {
lbool tactic2solver_core::check_sat_core(unsigned num_assumptions, expr * const * assumptions) {
SASSERT(m_ctx);
ast_manager & m = m_ctx->m();
params_ref p = m_params;

16
src/solver/tactic2solver.h
View file

@ -22,7 +22,7 @@ Notes:
#ifndef _TACTIC2SOLVER_H_
#define _TACTIC2SOLVER_H_
#include"solver.h"
#include"solver_na2as.h"
#include"tactic.h"
/**
@ -32,7 +32,7 @@ Notes:
option for applications trying to solve many easy queries that a
similar to each other.
*/
class tactic2solver_core : public solver {
class tactic2solver_core : public solver_na2as {
struct ctx {
symbol m_logic;
expr_ref_vector m_assertions;
@ -63,13 +63,13 @@ public:
virtual void set_produce_models(bool f) { m_produce_models = f; }
virtual void set_produce_unsat_cores(bool f) { m_produce_unsat_cores = f; }
virtual void init(ast_manager & m, symbol const & logic);
virtual void reset();
virtual void assert_expr(expr * t);
virtual void push();
virtual void pop(unsigned n);
virtual unsigned get_scope_level() const;
virtual lbool check_sat(unsigned num_assumptions, expr * const * assumptions);
virtual void init_core(ast_manager & m, symbol const & logic);
virtual void reset_core();
virtual void push_core();
virtual void pop_core(unsigned n);
virtual lbool check_sat_core(unsigned num_assumptions, expr * const * assumptions);
virtual void set_cancel(bool f);

1
src/tactic/core/propagate_values_tactic.cpp
View file

@ -209,6 +209,7 @@ class propagate_values_tactic : public tactic {
result.push_back(m_goal);
SASSERT(m_goal->is_well_sorted());
TRACE("propagate_values", m_goal->display(tout););
TRACE("propagate_values_core", m_goal->display_with_dependencies(tout););
m_goal = 0;
}
};

84
src/tactic/goal.cpp
View file

@ -22,6 +22,13 @@ Revision History:
#include"for_each_expr.h"
#include"well_sorted.h"
goal::precision goal::mk_union(precision p1, precision p2) {
if (p1 == PRECISE) return p2;
if (p2 == PRECISE) return p1;
if (p1 != p2) return UNDER_OVER;
return p1;
}
std::ostream & operator<<(std::ostream & out, goal::precision p) {
switch (p) {
case goal::PRECISE: out << "precise"; break;
@ -32,6 +39,58 @@ std::ostream & operator<<(std::ostream & out, goal::precision p) {
return out;
}
goal::goal(ast_manager & m, bool models_enabled, bool core_enabled):
m_manager(m),
m_ref_count(0),
m_depth(0),
m_models_enabled(models_enabled),
m_proofs_enabled(m.proofs_enabled()),
m_core_enabled(core_enabled),
m_inconsistent(false),
m_precision(PRECISE) {
}
goal::goal(ast_manager & m, bool proofs_enabled, bool models_enabled, bool core_enabled):
m_manager(m),
m_ref_count(0),
m_depth(0),
m_models_enabled(models_enabled),
m_proofs_enabled(proofs_enabled),
m_core_enabled(core_enabled),
m_inconsistent(false),
m_precision(PRECISE) {
SASSERT(!proofs_enabled || m.proofs_enabled());
}
goal::goal(goal const & src):
m_manager(src.m()),
m_ref_count(0),
m_depth(0),
m_models_enabled(src.models_enabled()),
m_proofs_enabled(src.proofs_enabled()),
m_core_enabled(src.unsat_core_enabled()),
m_inconsistent(false),
m_precision(PRECISE) {
copy_from(src);
}
// Copy configuration: depth, models/proofs/cores flags, and precision from src.
// The assertions are not copied
goal::goal(goal const & src, bool):
m_manager(src.m()),
m_ref_count(0),
m_depth(src.m_depth),
m_models_enabled(src.models_enabled()),
m_proofs_enabled(src.proofs_enabled()),
m_core_enabled(src.unsat_core_enabled()),
m_inconsistent(false),
m_precision(src.m_precision) {
}
goal::~goal() {
reset_core();
}
void goal::copy_to(goal & target) const {
SASSERT(&m_manager == &(target.m_manager));
if (this == &target)
@ -174,6 +233,10 @@ void goal::assert_expr(expr * f, proof * pr, expr_dependency * d) {
quick_process(false, f, d);
}
void goal::assert_expr(expr * f, expr_dependency * d) {
assert_expr(f, proofs_enabled() ? m().mk_asserted(f) : 0, d);
}
void goal::get_formulas(ptr_vector<expr> & result) {
unsigned sz = size();
for (unsigned i = 0; i < sz; i++) {
@ -570,6 +633,27 @@ goal * goal::translate(ast_translation & translator) const {
return res;
}
bool goal::sat_preserved() const {
return prec() == PRECISE || prec() == UNDER;
}
bool goal::unsat_preserved() const {
return prec() == PRECISE || prec() == OVER;
}
bool goal::is_decided_sat() const {
return size() == 0 && sat_preserved();
}
bool goal::is_decided_unsat() const {
return inconsistent() && unsat_preserved();
}
bool goal::is_decided() const {
return is_decided_sat() || is_decided_unsat();
}
bool is_equal(goal const & s1, goal const & s2) {
if (s1.size() != s2.size())
return false;

90
src/tactic/goal.h
View file

@ -45,12 +45,7 @@ public:
UNDER_OVER // goal is garbage: the produce of combined under and over approximation steps.
};
static precision mk_union(precision p1, precision p2) {
if (p1 == PRECISE) return p2;
if (p2 == PRECISE) return p1;
if (p1 != p2) return UNDER_OVER;
return p1;
}
static precision mk_union(precision p1, precision p2);
protected:
ast_manager & m_manager;
@ -78,55 +73,13 @@ protected:
void reset_core();
public:
goal(ast_manager & m, bool models_enabled = true, bool core_enabled = false):
m_manager(m),
m_ref_count(0),
m_depth(0),
m_models_enabled(models_enabled),
m_proofs_enabled(m.proofs_enabled()),
m_core_enabled(core_enabled),
m_inconsistent(false),
m_precision(PRECISE) {
}
goal(ast_manager & m, bool proofs_enabled, bool models_enabled, bool core_enabled):
m_manager(m),
m_ref_count(0),
m_depth(0),
m_models_enabled(models_enabled),
m_proofs_enabled(proofs_enabled),
m_core_enabled(core_enabled),
m_inconsistent(false),
m_precision(PRECISE) {
SASSERT(!proofs_enabled || m.proofs_enabled());
}
goal(goal const & src):
m_manager(src.m()),
m_ref_count(0),
m_depth(0),
m_models_enabled(src.models_enabled()),
m_proofs_enabled(src.proofs_enabled()),
m_core_enabled(src.unsat_core_enabled()),
m_inconsistent(false),
m_precision(PRECISE) {
copy_from(src);
}
goal(ast_manager & m, bool models_enabled = true, bool core_enabled = false);
goal(ast_manager & m, bool proofs_enabled, bool models_enabled, bool core_enabled);
goal(goal const & src);
// Copy configuration: depth, models/proofs/cores flags, and precision from src.
// The assertions are not copied
goal(goal const & src, bool):
m_manager(src.m()),
m_ref_count(0),
m_depth(src.m_depth),
m_models_enabled(src.models_enabled()),
m_proofs_enabled(src.proofs_enabled()),
m_core_enabled(src.unsat_core_enabled()),
m_inconsistent(false),
m_precision(src.m_precision) {
}
~goal() { reset_core(); }
goal(goal const & src, bool);
~goal();
void inc_ref() { ++m_ref_count; }
void dec_ref() { --m_ref_count; if (m_ref_count == 0) dealloc(this); }
@ -152,9 +105,9 @@ public:
void copy_from(goal const & src) { src.copy_to(*this); }
void assert_expr(expr * f, proof * pr, expr_dependency * d);
void assert_expr(expr * f) {
assert_expr(f, proofs_enabled() ? m().mk_asserted(f) : 0, 0);
}
void assert_expr(expr * f, expr_dependency * d);
void assert_expr(expr * f, expr * d) { assert_expr(f, m().mk_leaf(d)); }
void assert_expr(expr * f) { assert_expr(f, static_cast<expr_dependency*>(0)); }
unsigned size() const { return m().size(m_forms); }
@ -181,26 +134,11 @@ public:
void display_with_dependencies(ast_printer_context & ctx) const;
void display_with_dependencies(std::ostream & out) const;
bool sat_preserved() const {
return prec() == PRECISE || prec() == UNDER;
}
bool unsat_preserved() const {
return prec() == PRECISE || prec() == OVER;
}
bool is_decided_sat() const {
return size() == 0 && sat_preserved();
}
bool is_decided_unsat() const {
return inconsistent() && unsat_preserved();
}
bool is_decided() const {
return is_decided_sat() || is_decided_unsat();
}
bool sat_preserved() const;
bool unsat_preserved() const;
bool is_decided_sat() const;
bool is_decided_unsat() const;
bool is_decided() const;
bool is_well_sorted() const;
goal * translate(ast_translation & translator) const;

16
src/tactic/portfolio/smt_strategic_solver.cpp
View file

@ -18,8 +18,7 @@ Notes:
--*/
#include"cmd_context.h"
#include"ni_solver.h"
#include"strategic_solver_cmd.h"
#include"strategic_solver.h"
#include"qfbv_tactic.h"
#include"qflia_tactic.h"
#include"qfnia_tactic.h"
@ -34,7 +33,7 @@ Notes:
#include"default_tactic.h"
#include"ufbv_tactic.h"
#include"qffpa_tactic.h"
#include"default_solver.h"
#include"smt_solver.h"
MK_SIMPLE_TACTIC_FACTORY(qfuf_fct, mk_qfuf_tactic(m, p));
MK_SIMPLE_TACTIC_FACTORY(qfidl_fct, mk_qfidl_tactic(m, p));
@ -56,7 +55,7 @@ MK_SIMPLE_TACTIC_FACTORY(qfnra_fct, mk_qfnra_tactic(m, p));
MK_SIMPLE_TACTIC_FACTORY(qffpa_fct, mk_qffpa_tactic(m, p));
MK_SIMPLE_TACTIC_FACTORY(ufbv_fct, mk_ufbv_tactic(m, p));
static void init(strategic_solver_core * s) {
static void init(strategic_solver * s) {
s->set_default_tactic(alloc(default_fct));
s->set_tactic_for(symbol("QF_UF"), alloc(qfuf_fct));
s->set_tactic_for(symbol("QF_BV"), alloc(qfbv_fct));
@ -80,17 +79,10 @@ static void init(strategic_solver_core * s) {
s->set_tactic_for(symbol("QF_FPA"), alloc(qffpa_fct));
}
solver * mk_smt_strategic_solver(cmd_context & ctx) {
strategic_solver_cmd * s = alloc(strategic_solver_cmd, ctx);
s->set_inc_solver(mk_quasi_incremental_smt_solver(ctx));
init(s);
return s;
}
solver * mk_smt_strategic_solver(bool force_tactic) {
strategic_solver * s = alloc(strategic_solver);
s->force_tactic(force_tactic);
s->set_inc_solver(mk_default_solver());
s->set_inc_solver(mk_smt_solver());
init(s);
return s;
}

4
src/tactic/portfolio/smt_strategic_solver.h
View file

@ -20,9 +20,7 @@ Notes:
#ifndef _SMT_STRATEGIC_SOLVER_H_
#define _SMT_STRATEGIC_SOLVER_H_
class cmd_context;
// Create a strategic solver for the SMT 2.0 frontend.
solver * mk_smt_strategic_solver(cmd_context & ctx);
class solver;
// Create a strategic solver for the Z3 API
solver * mk_smt_strategic_solver(bool force_tactic=false);

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";