Refactor skolemisation

Author: thomasspriggs

src/goto-programs/skolemization.cpp

@@ -6,13 +6,41 @@
 
 #include "goto_model.h"
 
-#include <ansi-c/expr2c.h>
-
-#include <util/expr_util.h>
 #include <util/fresh_symbol.h>
 #include <util/irep.h> // for id2string
 #include <util/mathematical_expr.h>
 
+/// Perform the first part of skolemisation, by identifying an existentially
+/// quantified statement and substituting the variables with skolem constants.
+/// \param condition The condition on which we search for quantifiers.
+/// \param symbol_table The symbol_table new symbols are inserted into.
+static void rename_variables_in_existential_quantifiers(
+  exprt &condition,
+  symbol_table_baset &symbol_table)
+{
+  condition.visit_post([&symbol_table](exprt &sub_expression) {
+    if(can_cast_expr<exists_exprt>(sub_expression))
+    {
+      quantifier_exprt &quantifier_expr = to_quantifier_expr(sub_expression);
+      const auto &quantifier_sym = quantifier_expr.symbol();
+
+      const auto new_symbol = get_fresh_aux_symbol(
+        quantifier_sym.type(),
+        CPROVER_PREFIX,
+        id2string(
+          symbol_table.lookup(quantifier_sym.get_identifier())->base_name),
+        quantifier_expr.source_location(),
+        symbol_table.lookup(quantifier_sym.get_identifier())->mode,
+        symbol_table);
+      const auto symbol_expr = new_symbol.symbol_expr();
+      const std::vector<exprt> new_sym_vec{symbol_expr};
+
+      sub_expression =
+        exists_exprt(symbol_expr, quantifier_expr.instantiate(new_sym_vec));
+    }
+  });
+}
+
 void rename_variables_in_existential_quantifiers(goto_modelt &goto_model)
 {
   for(auto &function : goto_model.goto_functions.function_map)
@@ -21,49 +49,9 @@ void rename_variables_in_existential_quantifiers(goto_modelt &goto_model)
     {
       if(instruction.has_condition())
       {
-        auto &cond = instruction.condition_nonconst();
-        recurse_on_condition(cond, goto_model);
+        rename_variables_in_existential_quantifiers(
+          instruction.condition_nonconst(), goto_model.symbol_table);
       }
     }
   }
 }
-
-void recurse_on_condition(exprt &cond, goto_modelt &model)
-{
-  // recurse on the condition's subexpressions first - that allows us
-  // to correctly identify the nodes we care about in a compound
-  // expression, for instance something like `1 == 1 && exists(i.i>=0 && i>1)`
-  for(exprt &subexpr : cond.operands())
-  {
-    recurse_on_condition(subexpr, model);
-  }
-
-  // if the expression we're in doesn't have any more operands,
-  // it means it's a leaf node, so we go ahead and process it.
-  rename_and_substitute(cond, model);
-}
-
-void rename_and_substitute(exprt &cond, goto_modelt &model)
-{
-  // perform the first part of skolemisation, by identifying an existentially
-  // quantified statement and substituting the variables with skolem constants.
-  if(can_cast_expr<exists_exprt>(cond))
-  {
-    quantifier_exprt &quantifier_expr = to_quantifier_expr(cond);
-    const auto &quantifier_sym = quantifier_expr.symbol();
-
-    const auto new_symbol = get_fresh_aux_symbol(
-      quantifier_sym.type(),
-      CPROVER_PREFIX,
-      id2string(
-        model.symbol_table.lookup(quantifier_sym.get_identifier())->base_name),
-      quantifier_expr.source_location(),
-      ID_C,
-      model.symbol_table);
-    const auto symbol_expr =
-      symbol_exprt(new_symbol.name, quantifier_sym.type());
-    const std::vector<exprt> new_sym_vec{symbol_expr};
-
-    cond = exists_exprt(symbol_expr, quantifier_expr.instantiate(new_sym_vec));
-  }
-}

src/goto-programs/skolemization.h

@@ -14,17 +14,4 @@ class goto_modelt;
 ///    for making changes to the symbol table at variable renaming time.
 void rename_variables_in_existential_quantifiers(goto_modelt &goto_model);
 
-/// Helper function that recurses over the condition expression of instructions.
-/// \param cond The condition on which we recurse over the operands (subexpressions).
-/// \param model The goto_model we are inserting the new symbol to.
-void recurse_on_condition(exprt &cond, goto_modelt &model);
-
-/// Helper function that does the actual renaming of the variables.
-/// This is called when we reach the atomic parts of the condition expression,
-/// to identify and rename the variables of any quantified statements that
-/// exist as part of the guard.
-/// \param cond The condition in which we are doing the renaming.
-/// \param model The goto_model we are inserting the new symbol to.
-void rename_and_substitute(exprt &cond, goto_modelt &model);
-
 #endif