mirror of
https://github.com/Z3Prover/z3
synced 2025-04-07 18:05:21 +00:00
replaced check_interpolants option with interp.check
This commit is contained in:
parent
6e18f44d99
commit
5454e38935
|
@ -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));
|
||||
|
|
|
@ -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;
|
||||
}
|
||||
|
|
|
@ -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; }
|
||||
|
|
|
@ -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");
|
||||
|
|
|
@ -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;
|
||||
|
|
|
@ -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();
|
||||
|
||||
|
|
|
@ -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'),
|
||||
))
|
||||
|
|
Loading…
Reference in a new issue