TermPrinter: Guarantee unique let variable names

For a let term
`(let ((l1 phi1) ... (ln phin)) psi[l1/phi1 ...  ln/phin])`
it must not be the case that `li` appears in `psi[l1/phi1 ...  ln/phin]`
as a free variable.  This commit guarantees this by introducing a let
prefix in `Logic` and modifying it whenever a new variable is introduced
such that its name is a proper prefix of the current let prefix.

The current let prefix is modified by postfixing it with a character
different from the first character after the proper prefix in the new
variable.

Author: aehyvari

src/common/TermPrinter.cc

@@ -49,8 +49,7 @@ void TermPrinterConfig::visit(PTRef tr) {
 }
 
 void DagPrinterConfig::visit(PTRef tr) {
-    // Todo: Ensure that the let identifier does not also appear as a symbol
-    auto getLetSymbol = [](PTRef tr) { return "?l" + std::to_string(tr.x); };
+    auto getLetSymbol = [&](PTRef tr) { return logic.getLetPrefix() + std::to_string(tr.x); };
 
     assert(termStrings.find(tr) == termStrings.end());
     Pterm const & term = logic.getPterm(tr);
@@ -71,7 +70,7 @@ void DagPrinterConfig::visit(PTRef tr) {
         auto const & defTerms = defsInNode->second;
         for (int i = defTerms.size()-1; i >= 0; i--) {
             // Note: Reverse order guarantees that dependencies are respected in let terms
-            // Todo: Figure out if there is a dependency between two definitions
+            // Todo: Use parallel lets if there is no dependency between two definitions
             PTRef def = defTerms[i];
             std::string letSymbol = getLetSymbol(def);
             openLetStatements += "(let ((" + letSymbol + " " + termStrings.at(def) + ")) ";

src/logics/Logic.cc

@@ -53,13 +53,15 @@ const char* Logic::s_sort_bool = "Bool";
 const char* Logic::s_ite_prefix = ".oite";
 const char* Logic::s_framev_prefix = ".frame";
 const char* Logic::s_abstract_value_prefix = "@";
-
+const char Logic::c_let_var_primary_prefix = '?';
+const char Logic::c_let_var_secondary_prefix = 'l';
 
 // The constructor initiates the base logic (Boolean)
 Logic::Logic(opensmt::Logic_t _logicType) :
       logicType(_logicType)
     , abstractValueCount(0)
     , distinctClassCount(0)
+    , letVarPrefix(1,c_let_var_primary_prefix)
     , sort_store()
     , term_store(sym_store)
     , sym_IndexedSort(sort_store.newSortSymbol(SortSymbol(tk_indexed, 2, SortSymbol::INTERNAL)))
@@ -701,6 +703,12 @@ PTRef Logic::mkVar(SRef s, const char* name, bool isInterpreted) {
     }
     PTRef ptr = mkFun(sr, {});
     assert (ptr != PTRef_Undef);
+    // The prefix of the names of the local variables introduced with let needs to be changed if
+    // the current prefix is a proper prefix of the new variable's name
+    if (letVarPrefix.size() < strlen(name) and letVarPrefix.compare(0, std::string::npos, name, letVarPrefix.size() == 0)) {
+        char charAfterCurrentPrefix = name[letVarPrefix.size()];
+        letVarPrefix += (charAfterCurrentPrefix != c_let_var_primary_prefix) ? c_let_var_primary_prefix : c_let_var_secondary_prefix;
+    }
 
     return ptr;
 }

src/logics/Logic.h

@@ -49,6 +49,7 @@ class Logic {
     bool isKnownToUser(SymRef sr) const { return isKnownToUser(getSymName(sr)); }
     std::size_t abstractValueCount;
     int distinctClassCount;
+    std::string letVarPrefix;
 
     class DefinedFunctions {
         std::unordered_map<std::string,TemplateFunction> defined_functions;
@@ -147,6 +148,8 @@ class Logic {
     static const char*  s_ite_prefix;
     static const char*  s_framev_prefix;
     static const char*  s_abstract_value_prefix;
+    static const char   c_let_var_primary_prefix;
+    static const char   c_let_var_secondary_prefix;
 
     Logic(opensmt::Logic_t type);
     virtual ~Logic();
@@ -399,6 +402,7 @@ class Logic {
 
     PTRef learnEqTransitivity(PTRef); // Learn limited transitivity information
 
+    std::string const & getLetPrefix() const { return letVarPrefix; }
 
     bool hasQuotableChars(std::string const & name) const;
     bool isReservedWord(std::string const & name) const;