diff --git a/src/cmd_context/basic_cmds.cpp b/src/cmd_context/basic_cmds.cpp index 836ade9ce..a80c5bc6c 100644 --- a/src/cmd_context/basic_cmds.cpp +++ b/src/cmd_context/basic_cmds.cpp @@ -241,7 +241,6 @@ protected: symbol m_produce_models; symbol m_produce_assignments; symbol m_produce_interpolants; - symbol m_check_interpolants; symbol m_regular_output_channel; symbol m_diagnostic_output_channel; symbol m_random_seed; @@ -256,7 +255,6 @@ protected: s == m_print_success || s == m_print_warning || s == m_expand_definitions || s == m_interactive_mode || s == m_produce_proofs || s == m_produce_unsat_cores || s == m_produce_models || s == m_produce_assignments || s == m_produce_interpolants || - s == m_check_interpolants || s == m_regular_output_channel || s == m_diagnostic_output_channel || s == m_random_seed || s == m_verbosity || s == m_global_decls; } @@ -275,7 +273,6 @@ public: m_produce_models(":produce-models"), m_produce_assignments(":produce-assignments"), m_produce_interpolants(":produce-interpolants"), - m_check_interpolants(":check-interpolants"), m_regular_output_channel(":regular-output-channel"), m_diagnostic_output_channel(":diagnostic-output-channel"), m_random_seed(":random-seed"), @@ -347,9 +344,6 @@ class set_option_cmd : public set_get_option_cmd { check_not_initialized(ctx, m_produce_interpolants); ctx.set_produce_interpolants(to_bool(value)); } - else if (m_option == m_check_interpolants) { - ctx.set_check_interpolants(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)); diff --git a/src/cmd_context/cmd_context.cpp b/src/cmd_context/cmd_context.cpp index ce2838aba..731608524 100644 --- a/src/cmd_context/cmd_context.cpp +++ b/src/cmd_context/cmd_context.cpp @@ -397,10 +397,6 @@ void cmd_context::set_produce_interpolants(bool f) { // set_solver_factory(mk_smt_solver_factory()); } -void cmd_context::set_check_interpolants(bool f) { - m_params.m_check_interpolants = f; -} - bool cmd_context::produce_models() const { return m_params.m_model; } @@ -414,10 +410,6 @@ bool cmd_context::produce_interpolants() const { return m_params.m_proof; } -bool cmd_context::check_interpolants() const { - return m_params.m_check_interpolants; -} - bool cmd_context::produce_unsat_cores() const { return m_params.m_unsat_core; } diff --git a/src/cmd_context/cmd_context.h b/src/cmd_context/cmd_context.h index e34975183..8ad07e8cc 100644 --- a/src/cmd_context/cmd_context.h +++ b/src/cmd_context/cmd_context.h @@ -279,7 +279,6 @@ public: bool produce_models() const; bool produce_proofs() const; bool produce_interpolants() const; - bool check_interpolants() const; bool produce_unsat_cores() const; bool well_sorted_check_enabled() const; bool validate_model_enabled() const; @@ -287,7 +286,6 @@ public: void set_produce_unsat_cores(bool flag); void set_produce_proofs(bool flag); void set_produce_interpolants(bool flag); - void set_check_interpolants(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; } diff --git a/src/cmd_context/context_params.cpp b/src/cmd_context/context_params.cpp index 254a1d931..f87c8d264 100644 --- a/src/cmd_context/context_params.cpp +++ b/src/cmd_context/context_params.cpp @@ -61,9 +61,6 @@ void context_params::set(char const * param, char const * value) { else if (p == "proof") { set_bool(m_proof, param, value); } - else if (p == "check_interpolants") { - set_bool(m_check_interpolants, param, value); - } else if (p == "model") { set_bool(m_model, param, value); } @@ -105,7 +102,6 @@ void context_params::updt_params(params_ref const & p) { m_well_sorted_check = p.get_bool("type_check", p.get_bool("well_sorted_check", true)); m_auto_config = p.get_bool("auto_config", true); m_proof = p.get_bool("proof", false); - m_check_interpolants = p.get_bool("check_interpolants", false); m_model = p.get_bool("model", true); m_model_validate = p.get_bool("model_validate", false); m_trace = p.get_bool("trace", false); @@ -120,7 +116,6 @@ void context_params::collect_param_descrs(param_descrs & d) { d.insert("well_sorted_check", CPK_BOOL, "type checker", "true"); d.insert("type_check", CPK_BOOL, "type checker (alias for well_sorted_check)", "true"); d.insert("auto_config", CPK_BOOL, "use heuristics to automatically select solver and configure it", "true"); - d.insert("check_interpolants", CPK_BOOL, "check correctness of interpolants", "false"); d.insert("model_validate", CPK_BOOL, "validate models produced by solvers", "false"); d.insert("trace", CPK_BOOL, "trace generation for VCC", "false"); d.insert("trace_file_name", CPK_STRING, "trace out file name (see option 'trace')", "z3.log"); diff --git a/src/cmd_context/context_params.h b/src/cmd_context/context_params.h index e26fd3fe5..506e559db 100644 --- a/src/cmd_context/context_params.h +++ b/src/cmd_context/context_params.h @@ -30,7 +30,6 @@ public: bool m_auto_config; bool m_proof; bool m_interpolants; - bool m_check_interpolants; bool m_debug_ref_count; bool m_trace; std::string m_trace_file_name; diff --git a/src/cmd_context/interpolant_cmds.cpp b/src/cmd_context/interpolant_cmds.cpp index cb83b52f6..42646a99d 100644 --- a/src/cmd_context/interpolant_cmds.cpp +++ b/src/cmd_context/interpolant_cmds.cpp @@ -65,7 +65,7 @@ static void show_interpolant_and_maybe_check(cmd_context & ctx, s.cleanup(); // verify, for the paranoid... - if(check || ctx.check_interpolants()){ + if(check || interp_params(m_params).check()){ std::ostringstream err; ast_manager &_m = ctx.m(); diff --git a/src/interp/iz3params.pyg b/src/interp/iz3params.pyg index 5b574c859..3116a18db 100644 --- a/src/interp/iz3params.pyg +++ b/src/interp/iz3params.pyg @@ -2,4 +2,5 @@ def_module_params('interp', description='interpolation parameters', export=True, params=(('profile', BOOL, False, '(INTERP) profile interpolation'), + ('check', BOOL, False, '(INTERP) check interpolants'), ))