mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-13 20:38:43 +00:00
Code Activity

added support for named assertions

Browse source
This commit is contained in:
Leonardo de Moura 2012-11-02 14:00:15 -07:00
parent e1eb3ee8ee
commit e2f6a65aa2
12 changed files with 62 additions and 319 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

51
src/cmd_context/cmd_context.cpp
View file

@ -1076,7 +1076,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 +1107,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 +1120,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 +1141,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 +1203,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 +1239,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);
}
@ -1266,11 +1264,9 @@ void cmd_context::check_sat(unsigned num_assumptions, expr * const * assumptions
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 +1274,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);

11
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);
@ -369,8 +367,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 +378,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/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);

225
src/smt/ni_solver.cpp
View file

@ -1,225 +0,0 @@
/*++
Copyright (c) 2011 Microsoft Corporation
Module Name:
ni_solver.cpp
Abstract:
Wrappers for smt::kernel that are non-incremental & (quasi-incremental).
Author:
Leonardo (leonardo) 2011-03-30
Notes:
--*/
#include"ni_solver.h"
#include"smt_kernel.h"
#include"cmd_context.h"
#include"solver_na2as.h"
class ni_smt_solver : public solver_na2as {
protected:
cmd_context & m_cmd_ctx;
smt::kernel * m_context;
progress_callback * m_callback;
public:
ni_smt_solver(cmd_context & ctx):m_cmd_ctx(ctx), m_context(0), m_callback(0) {}
virtual ~ni_smt_solver() {
if (m_context != 0)
dealloc(m_context);
}
virtual void init_core(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_core() {
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_core() {
// do nothing
}
virtual void pop_core(unsigned n) {
// do nothing
}
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_core();
#pragma omp critical (ni_solver)
{
m_context = alloc(smt::kernel, m_cmd_ctx.m(), m_cmd_ctx.params());
}
if (m_cmd_ctx.has_logic())
m_context->set_logic(m_cmd_ctx.get_logic());
if (m_callback)
m_context->set_progress_callback(m_callback);
assert_exprs();
}
virtual lbool check_sat_core(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::kernel::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_core(ast_manager & m, symbol const & logic) {
if (m_inc_mode) {
init_solver();
m_inc_mode = true;
}
}
virtual void reset_core() {
ni_smt_solver::reset_core();
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_core() {
switch_to_inc();
SASSERT(m_context);
m_context->push();
SASSERT(m_inc_mode);
}
virtual void pop_core(unsigned n) {
switch_to_inc();
SASSERT(m_context);
m_context->pop(n);
SASSERT(m_inc_mode);
}
virtual lbool check_sat_core(unsigned num_assumptions, expr * const * assumptions) {
if (!m_inc_mode) {
lbool r = ni_smt_solver::check_sat_core(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

14
src/smt/smt_solver.cpp
View file

@ -24,10 +24,11 @@ Notes:
namespace smt {
class solver : public solver_na2as {
front_end_params * m_params;
smt::kernel * m_context;
front_end_params * m_params;
smt::kernel * m_context;
progress_callback * m_callback;
public:
solver():m_params(0), m_context(0) {}
solver():m_params(0), m_context(0), m_callback(0) {}
virtual ~solver() {
if (m_context != 0)
@ -63,6 +64,8 @@ namespace smt {
#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);
@ -145,8 +148,9 @@ namespace smt {
}
virtual void set_progress_callback(progress_callback * callback) {
SASSERT(m_context);
m_context->set_progress_callback(callback);
m_callback = callback;
if (m_context)
m_context->set_progress_callback(callback);
}
virtual unsigned get_num_assertions() const {

4
src/solver/solver_na2as.cpp
View file

@ -20,6 +20,7 @@ Notes:
--*/
#include"solver_na2as.h"
#include"ast_smt2_pp.h"
solver_na2as::solver_na2as() {
m_manager = 0;
@ -31,6 +32,9 @@ solver_na2as::~solver_na2as() {
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);

6
src/solver/strategic_solver.cpp
View file

@ -268,10 +268,15 @@ lbool strategic_solver_core::check_sat_with_assumptions(unsigned num_assumptions
}
init_inc_solver();
m_use_inc_solver_results = true;
TRACE("solver_na2as", tout << "invoking inc_solver with " << num_assumptions << " assumptions\n";);
return m_inc_solver->check_sat(num_assumptions, assumptions);
}
lbool strategic_solver_core::check_sat_core(unsigned num_assumptions, expr * const * assumptions) {
TRACE("solver_na2as", tout << "assumptions at strategic_solver_core:\n";
for (unsigned i = 0; i < num_assumptions; i++) {
tout << mk_ismt2_pp(assumptions[i], m()) << "\n";
});
reset_results();
m_check_sat_executed = true;
if (num_assumptions > 0 || // assumptions were provided
@ -355,6 +360,7 @@ void strategic_solver_core::set_cancel(bool f) {
}
void strategic_solver_core::get_unsat_core(ptr_vector<expr> & r) {
TRACE("solver_na2as", 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);

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

@ -18,7 +18,6 @@ Notes:
--*/
#include"cmd_context.h"
#include"ni_solver.h"
#include"strategic_solver_cmd.h"
#include"qfbv_tactic.h"
#include"qflia_tactic.h"
@ -80,13 +79,6 @@ 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);

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