Merge pull request #7970 from qinheping/features/better-terminals-in-synthesizer

SYNTHESIZER: Use only symbols from the original goto as terminals

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)