mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-16 19:06:17 +00:00
Code Activity

allow for toggling proof and core mode until the first assertion.

Browse source
This commit is contained in:
Nikolaj Bjorner 2022-07-02 09:31:36 -07:00
parent 4d23f2801c
commit f20db3e644
3 changed files with 38 additions and 42 deletions
Download patch file Download diff file Expand all files Collapse all files

29
src/cmd_context/basic_cmds.cpp
View file

@ -219,9 +219,8 @@ ATOMIC_CMD(get_proof_graph_cmd, "get-proof-graph", "retrieve proof and print it
pr = ctx.get_check_sat_result()->get_proof(); pr = ctx.get_check_sat_result()->get_proof();
if (pr == 0) if (pr == 0)
throw cmd_exception("proof is not available"); throw cmd_exception("proof is not available");
if (ctx.well_sorted_check_enabled() && !is_well_sorted(ctx.m(), pr)) { if (ctx.well_sorted_check_enabled() && !is_well_sorted(ctx.m(), pr))
throw cmd_exception("proof is not well sorted"); throw cmd_exception("proof is not well sorted");
}
context_params& params = ctx.params(); context_params& params = ctx.params();
const std::string& file = params.m_dot_proof_file; const std::string& file = params.m_dot_proof_file;
@ -235,11 +234,11 @@ static void print_core(cmd_context& ctx) {
ctx.regular_stream() << "("; ctx.regular_stream() << "(";
bool first = true; bool first = true;
for (expr* e : core) { for (expr* e : core) {
if (first) if (first)
first = false; first = false;
else else
ctx.regular_stream() << " "; ctx.regular_stream() << " ";
ctx.regular_stream() << mk_ismt2_pp(e, ctx.m()); ctx.regular_stream() << mk_ismt2_pp(e, ctx.m());
} }
ctx.regular_stream() << ")" << std::endl; ctx.regular_stream() << ")" << std::endl;
} }
@ -260,9 +259,8 @@ ATOMIC_CMD(get_unsat_assumptions_cmd, "get-unsat-assumptions", "retrieve subset
return; return;
if (!ctx.produce_unsat_assumptions()) if (!ctx.produce_unsat_assumptions())
throw cmd_exception("unsat assumptions construction is not enabled, use command (set-option :produce-unsat-assumptions true)"); throw cmd_exception("unsat assumptions construction is not enabled, use command (set-option :produce-unsat-assumptions true)");
if (!ctx.has_manager() || ctx.cs_state() != cmd_context::css_unsat) { if (!ctx.has_manager() || ctx.cs_state() != cmd_context::css_unsat)
throw cmd_exception("unsat assumptions is not available"); throw cmd_exception("unsat assumptions is not available");
}
print_core(ctx); print_core(ctx);
}); });
@ -410,6 +408,15 @@ class set_option_cmd : public set_get_option_cmd {
} }
} }
static void check_no_assertions(cmd_context & ctx, symbol const & opt_name) {
if (ctx.has_assertions()) {
std::string msg = "error setting '";
msg += opt_name.str();
msg += "', option value cannot be modified after assertions have been added";
throw cmd_exception(std::move(msg));
}
}
void set_param(cmd_context & ctx, char const * value) { void set_param(cmd_context & ctx, char const * value) {
try { try {
gparams::set(m_option, value); gparams::set(m_option, value);
@ -437,11 +444,11 @@ class set_option_cmd : public set_get_option_cmd {
ctx.set_interactive_mode(to_bool(value)); ctx.set_interactive_mode(to_bool(value));
} }
else if (m_option == m_produce_proofs) { else if (m_option == m_produce_proofs) {
check_not_initialized(ctx, m_produce_proofs); check_no_assertions(ctx, m_produce_proofs);
ctx.set_produce_proofs(to_bool(value)); ctx.set_produce_proofs(to_bool(value));
} }
else if (m_option == m_produce_unsat_cores) { else if (m_option == m_produce_unsat_cores) {
check_not_initialized(ctx, m_produce_unsat_cores); check_no_assertions(ctx, m_produce_unsat_cores);
ctx.set_produce_unsat_cores(to_bool(value)); ctx.set_produce_unsat_cores(to_bool(value));
} }
else if (m_option == m_produce_unsat_assumptions) { else if (m_option == m_produce_unsat_assumptions) {

20
src/cmd_context/cmd_context.cpp
View file

@ -538,22 +538,9 @@ public:
cmd_context::cmd_context(bool main_ctx, ast_manager * m, symbol const & l): cmd_context::cmd_context(bool main_ctx, ast_manager * m, symbol const & l):
m_main_ctx(main_ctx), m_main_ctx(main_ctx),
m_logic(l), m_logic(l),
m_interactive_mode(false),
m_global_decls(false),
m_print_success(m_params.m_smtlib2_compliant), m_print_success(m_params.m_smtlib2_compliant),
m_random_seed(0),
m_produce_unsat_cores(false),
m_produce_unsat_assumptions(false),
m_produce_assignments(false),
m_status(UNKNOWN),
m_numeral_as_real(false),
m_ignore_check(false),
m_exit_on_error(false),
m_manager(m), m_manager(m),
m_own_manager(m == nullptr), m_own_manager(m == nullptr),
m_manager_initialized(false),
m_pmanager(nullptr),
m_sexpr_manager(nullptr),
m_regular("stdout", std::cout), m_regular("stdout", std::cout),
m_diagnostic("stderr", std::cerr) { m_diagnostic("stderr", std::cerr) {
SASSERT(m != 0 || !has_manager()); SASSERT(m != 0 || !has_manager());
@ -626,13 +613,14 @@ void cmd_context::set_produce_models(bool f) {
void cmd_context::set_produce_unsat_cores(bool f) { void cmd_context::set_produce_unsat_cores(bool f) {
// can only be set before initialization // can only be set before initialization
SASSERT(!has_manager()); SASSERT(!has_assertions());
m_params.m_unsat_core |= f; m_params.m_unsat_core |= f;
} }
void cmd_context::set_produce_proofs(bool f) { void cmd_context::set_produce_proofs(bool f) {
// can only be set before initialization SASSERT(!has_assertions());
SASSERT(!has_manager()); if (has_manager())
m().toggle_proof_mode(f ? PGM_ENABLED : PGM_DISABLED);
m_params.m_proof = f; m_params.m_proof = f;
} }

31
src/cmd_context/cmd_context.h
View file

@ -194,21 +194,21 @@ public:
protected: protected:
ast_context_params m_params; ast_context_params m_params;
bool m_main_ctx; bool m_main_ctx;
symbol m_logic; symbol m_logic;
bool m_interactive_mode; bool m_interactive_mode = false;
bool m_global_decls; bool m_global_decls = false;
bool m_print_success; bool m_print_success;
unsigned m_random_seed; unsigned m_random_seed = 0;
bool m_produce_unsat_cores; bool m_produce_unsat_cores = false;
bool m_produce_unsat_assumptions; bool m_produce_unsat_assumptions = false;
bool m_produce_assignments; bool m_produce_assignments = false;
status m_status; status m_status = UNKNOWN;
bool m_numeral_as_real; bool m_numeral_as_real = false;
bool m_ignore_check; // used by the API to disable check-sat() commands when parsing SMT 2.0 files. bool m_ignore_check = false; // used by the API to disable check-sat() commands when parsing SMT 2.0 files.
bool m_exit_on_error; bool m_exit_on_error = false;
bool m_allow_duplicate_declarations { false }; bool m_allow_duplicate_declarations = false;
static std::ostringstream g_error_stream; static std::ostringstream g_error_stream;
@ -216,9 +216,9 @@ protected:
sref_vector<generic_model_converter> m_mcs; sref_vector<generic_model_converter> m_mcs;
ast_manager * m_manager; ast_manager * m_manager;
bool m_own_manager; bool m_own_manager;
bool m_manager_initialized; bool m_manager_initialized = false;
pdecl_manager * m_pmanager; pdecl_manager * m_pmanager = nullptr;
sexpr_manager * m_sexpr_manager; sexpr_manager * m_sexpr_manager = nullptr;
check_logic m_check_logic; check_logic m_check_logic;
stream_ref m_regular; stream_ref m_regular;
stream_ref m_diagnostic; stream_ref m_diagnostic;
@ -362,6 +362,7 @@ public:
bool produce_unsat_cores() const; bool produce_unsat_cores() const;
bool well_sorted_check_enabled() const; bool well_sorted_check_enabled() const;
bool validate_model_enabled() const; bool validate_model_enabled() const;
bool has_assertions() const { return !m_assertions.empty(); }
void set_produce_models(bool flag); void set_produce_models(bool flag);
void set_produce_unsat_cores(bool flag); void set_produce_unsat_cores(bool flag);
void set_produce_proofs(bool flag); void set_produce_proofs(bool flag);