diff --git a/src/goto-instrument/contracts/contracts.cpp b/src/goto-instrument/contracts/contracts.cpp index e55d53987f8..f99d87e4477 100644 --- a/src/goto-instrument/contracts/contracts.cpp +++ b/src/goto-instrument/contracts/contracts.cpp @@ -68,10 +68,6 @@ void code_contractst::check_apply_loop_contracts( // at the start of and end of a loop body std::vector old_decreases_vars, new_decreases_vars; - // replace bound variables by fresh instances - if(has_subexpr(invariant, ID_exists) || has_subexpr(invariant, ID_forall)) - add_quantified_variable(symbol_table, invariant, mode); - // instrument // // ... preamble ... @@ -571,13 +567,6 @@ static void generate_contract_constraints( goto_programt &program, const source_locationt &location) { - if( - has_subexpr(instantiated_clause, ID_exists) || - has_subexpr(instantiated_clause, ID_forall)) - { - add_quantified_variable(symbol_table, instantiated_clause, mode); - } - goto_programt constraint; if(location.get_property_class() == ID_assume) { diff --git a/src/goto-instrument/contracts/dynamic-frames/dfcc_instrument_loop.cpp b/src/goto-instrument/contracts/dynamic-frames/dfcc_instrument_loop.cpp index b14187a44e9..20952a1c939 100644 --- a/src/goto-instrument/contracts/dynamic-frames/dfcc_instrument_loop.cpp +++ b/src/goto-instrument/contracts/dynamic-frames/dfcc_instrument_loop.cpp @@ -235,9 +235,6 @@ dfcc_instrument_loopt::add_prehead_instructions( // GOTO HEAD; // ``` - // Replace bound variables by fresh instances in quantified formulas. - if(has_subexpr(invariant, ID_exists) || has_subexpr(invariant, ID_forall)) - add_quantified_variable(symbol_table, invariant, language_mode); // initialize loop_entry history vars; auto replace_history_result = replace_history_loop_entry( symbol_table, invariant, loop_head_location, language_mode); @@ -429,9 +426,6 @@ dfcc_instrument_loopt::add_step_instructions( dfcc_utilst::get_function_symbol(symbol_table, function_id).mode; { // Assume the loop invariant after havocing the state. - // Replace bound variables by fresh instances in quantified formulas. - if(has_subexpr(invariant, ID_exists) || has_subexpr(invariant, ID_forall)) - add_quantified_variable(symbol_table, invariant, language_mode); code_assumet assumption{invariant}; assumption.add_source_location() = loop_head_location; converter.goto_convert(assumption, step_instrs, language_mode); @@ -513,9 +507,6 @@ void dfcc_instrument_loopt::add_body_instructions( id2string(check_location.get_function()) + "." + std::to_string(cbmc_loop_id)); // Assume the loop invariant after havocing the state. - // Replace bound variables by fresh instances in quantified formulas. - if(has_subexpr(invariant, ID_exists) || has_subexpr(invariant, ID_forall)) - add_quantified_variable(symbol_table, invariant, language_mode); code_assertt assertion{invariant}; assertion.add_source_location() = check_location; converter.goto_convert(assertion, pre_loop_latch_instrs, language_mode); diff --git a/src/goto-instrument/contracts/dynamic-frames/dfcc_wrapper_program.cpp b/src/goto-instrument/contracts/dynamic-frames/dfcc_wrapper_program.cpp index 826e5283e11..45d83370521 100644 --- a/src/goto-instrument/contracts/dynamic-frames/dfcc_wrapper_program.cpp +++ b/src/goto-instrument/contracts/dynamic-frames/dfcc_wrapper_program.cpp @@ -555,13 +555,6 @@ void dfcc_wrapper_programt::encode_requires_clauses() { exprt requires_lmbd = to_lambda_expr(r).application(contract_lambda_parameters); - requires_lmbd.add_source_location() = r.source_location(); - if( - has_subexpr(requires_lmbd, ID_exists) || - has_subexpr(requires_lmbd, ID_forall)) - add_quantified_variable( - goto_model.symbol_table, requires_lmbd, language_mode); - source_locationt sl(r.source_location()); if(statement_type == ID_assert) { @@ -609,9 +602,6 @@ void dfcc_wrapper_programt::encode_ensures_clauses() .application(contract_lambda_parameters) .with_source_location(e); - if(has_subexpr(ensures, ID_exists) || has_subexpr(ensures, ID_forall)) - add_quantified_variable(goto_model.symbol_table, ensures, language_mode); - // this also rewrites ID_old expressions to fresh variables generate_history_variables_initialization( goto_model.symbol_table, ensures, language_mode, history); diff --git a/src/goto-instrument/contracts/utils.cpp b/src/goto-instrument/contracts/utils.cpp index 6dd6cf7e681..a33319509b2 100644 --- a/src/goto-instrument/contracts/utils.cpp +++ b/src/goto-instrument/contracts/utils.cpp @@ -381,48 +381,6 @@ void widen_assigns(assignst &assigns, const namespacet &ns) assigns = result; } -void add_quantified_variable( - symbol_table_baset &symbol_table, - exprt &expression, - const irep_idt &mode) -{ - auto visitor = [&symbol_table, &mode](exprt &expr) { - if(expr.id() != ID_exists && expr.id() != ID_forall) - return; - // When a quantifier expression is found, create a fresh symbol for each - // quantified variable and rewrite the expression to use those fresh - // symbols. - auto &quantifier_expression = to_quantifier_expr(expr); - std::vector fresh_variables; - fresh_variables.reserve(quantifier_expression.variables().size()); - for(const auto &quantified_variable : quantifier_expression.variables()) - { - // 1. create fresh symbol - symbolt new_symbol = get_fresh_aux_symbol( - quantified_variable.type(), - id2string(quantified_variable.source_location().get_function()), - "tmp_cc", - quantified_variable.source_location(), - mode, - symbol_table); - - // 2. add created fresh symbol to expression map - fresh_variables.push_back(new_symbol.symbol_expr()); - } - - // use fresh symbols - exprt where = quantifier_expression.instantiate(fresh_variables); - - // recursively check for nested quantified formulae - add_quantified_variable(symbol_table, where, mode); - - // replace previous variables and body - quantifier_expression.variables() = fresh_variables; - quantifier_expression.where() = std::move(where); - }; - expression.visit_pre(visitor); -} - static void replace_history_parameter_rec( symbol_table_baset &symbol_table, exprt &expr, diff --git a/src/goto-instrument/contracts/utils.h b/src/goto-instrument/contracts/utils.h index 99c455a2616..4fd310627b8 100644 --- a/src/goto-instrument/contracts/utils.h +++ b/src/goto-instrument/contracts/utils.h @@ -232,15 +232,6 @@ void infer_loop_assigns( /// *(b+i) when `i` is a known constant, keep the expression in the result. void widen_assigns(assignst &assigns, const namespacet &ns); -/// This function recursively searches \p expression to find nested or -/// non-nested quantified expressions. When a quantified expression is found, -/// a fresh quantified variable is added to the symbol table and \p expression -/// is updated to use this fresh variable. -void add_quantified_variable( - symbol_table_baset &symbol_table, - exprt &expression, - const irep_idt &mode); - struct replace_history_parametert { exprt expression_after_replacement;