diff --git a/src/cmd_context/basic_cmds.cpp b/src/cmd_context/basic_cmds.cpp index f3bd0ed57..dc8836138 100644 --- a/src/cmd_context/basic_cmds.cpp +++ b/src/cmd_context/basic_cmds.cpp @@ -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(); if (pr == 0) 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"); - } context_params& params = ctx.params(); const std::string& file = params.m_dot_proof_file; @@ -235,11 +234,11 @@ static void print_core(cmd_context& ctx) { ctx.regular_stream() << "("; bool first = true; for (expr* e : core) { - if (first) - first = false; - else - ctx.regular_stream() << " "; - ctx.regular_stream() << mk_ismt2_pp(e, ctx.m()); + if (first) + first = false; + else + ctx.regular_stream() << " "; + ctx.regular_stream() << mk_ismt2_pp(e, ctx.m()); } ctx.regular_stream() << ")" << std::endl; } @@ -260,9 +259,8 @@ ATOMIC_CMD(get_unsat_assumptions_cmd, "get-unsat-assumptions", "retrieve subset return; if (!ctx.produce_unsat_assumptions()) 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"); - } 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) { try { 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)); } 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)); } 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)); } else if (m_option == m_produce_unsat_assumptions) { diff --git a/src/cmd_context/cmd_context.cpp b/src/cmd_context/cmd_context.cpp index 705396f53..ad150b674 100644 --- a/src/cmd_context/cmd_context.cpp +++ b/src/cmd_context/cmd_context.cpp @@ -538,22 +538,9 @@ public: cmd_context::cmd_context(bool main_ctx, ast_manager * m, symbol const & l): m_main_ctx(main_ctx), m_logic(l), - m_interactive_mode(false), - m_global_decls(false), 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_own_manager(m == nullptr), - m_manager_initialized(false), - m_pmanager(nullptr), - m_sexpr_manager(nullptr), m_regular("stdout", std::cout), m_diagnostic("stderr", std::cerr) { 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) { // can only be set before initialization - SASSERT(!has_manager()); + SASSERT(!has_assertions()); m_params.m_unsat_core |= f; } void cmd_context::set_produce_proofs(bool f) { - // can only be set before initialization - SASSERT(!has_manager()); + SASSERT(!has_assertions()); + if (has_manager()) + m().toggle_proof_mode(f ? PGM_ENABLED : PGM_DISABLED); m_params.m_proof = f; } diff --git a/src/cmd_context/cmd_context.h b/src/cmd_context/cmd_context.h index c51809190..3dc49624b 100644 --- a/src/cmd_context/cmd_context.h +++ b/src/cmd_context/cmd_context.h @@ -194,21 +194,21 @@ public: protected: - ast_context_params m_params; + ast_context_params m_params; bool m_main_ctx; symbol m_logic; - bool m_interactive_mode; - bool m_global_decls; + bool m_interactive_mode = false; + bool m_global_decls = false; bool m_print_success; - unsigned m_random_seed; - bool m_produce_unsat_cores; - bool m_produce_unsat_assumptions; - bool m_produce_assignments; - status m_status; - bool m_numeral_as_real; - bool m_ignore_check; // used by the API to disable check-sat() commands when parsing SMT 2.0 files. - bool m_exit_on_error; - bool m_allow_duplicate_declarations { false }; + unsigned m_random_seed = 0; + bool m_produce_unsat_cores = false; + bool m_produce_unsat_assumptions = false; + bool m_produce_assignments = false; + status m_status = UNKNOWN; + bool m_numeral_as_real = false; + 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 = false; + bool m_allow_duplicate_declarations = false; static std::ostringstream g_error_stream; @@ -216,9 +216,9 @@ protected: sref_vector m_mcs; ast_manager * m_manager; bool m_own_manager; - bool m_manager_initialized; - pdecl_manager * m_pmanager; - sexpr_manager * m_sexpr_manager; + bool m_manager_initialized = false; + pdecl_manager * m_pmanager = nullptr; + sexpr_manager * m_sexpr_manager = nullptr; check_logic m_check_logic; stream_ref m_regular; stream_ref m_diagnostic; @@ -362,6 +362,7 @@ public: bool produce_unsat_cores() const; bool well_sorted_check_enabled() const; bool validate_model_enabled() const; + bool has_assertions() const { return !m_assertions.empty(); } void set_produce_models(bool flag); void set_produce_unsat_cores(bool flag); void set_produce_proofs(bool flag);