Use only symbols from the original goto as terminals in synthesizer

Collecting variables from trace will also collect those variables added during loop transformation, such as the car variables.
Such variables should not appear in the loop contracts.
This commit erases them from the terminals of the enumearting grammar used by the synthesizer.

Author: qinheping

src/goto-synthesizer/enumerative_loop_contracts_synthesizer.cpp

@@ -49,6 +49,12 @@ void replace_tmp_post(
 
 std::vector<exprt> construct_terminals(const std::set<symbol_exprt> &symbols)
 {
+  // Construct a vector of terminal expressions.
+  // Terminals include:
+  //   1: scalar type variables and their loop_entry version.
+  //   2: offsets of pointers and loop_entry of pointers.
+  //   3: constants 0 and 1.
+
   std::vector<exprt> result;
   for(const auto &e : symbols)
   {
@@ -244,6 +250,18 @@ enumerative_loop_contracts_synthesizert::compute_dependent_symbols(
   for(const auto &e : live_vars)
     find_symbols(e, result);
 
+  // Erase all variables added during loop transformations---they are not in
+  // the original symbol table.
+  for(auto it = result.begin(); it != result.end();)
+  {
+    if(original_symbol_table.lookup(it->get_identifier()) == nullptr)
+    {
+      it = result.erase(it);
+    }
+    else
+      it++;
+  }
+
   return result;
 }
 

src/goto-synthesizer/enumerative_loop_contracts_synthesizer.h

@@ -36,7 +36,8 @@ class enumerative_loop_contracts_synthesizert
     messaget &log)
     : loop_contracts_synthesizer_baset(goto_model, log),
       options(options),
-      ns(goto_model.symbol_table)
+      ns(goto_model.symbol_table),
+      original_symbol_table(goto_model.symbol_table)
   {
   }
 
@@ -97,6 +98,9 @@ class enumerative_loop_contracts_synthesizert
 
   /// Map from tmp_post variables to their original variables.
   std::unordered_map<exprt, exprt, irep_hash> tmp_post_map;
+
+  /// Symbol table of the input goto model
+  const symbol_tablet original_symbol_table;
 };
 
 // NOLINTNEXTLINE(whitespace/line_length)