Fix cached free variable identifiers in sygus term database (#4394)

Fixes an issue with over-pruning in SyGuS where using multiple sygus types that map to the same builtin type. Our mapping sygusToBuiltin did not ensure that free variables were unique.

Fixes #4383.

3 files changed, 52 insertions, 22 deletions

diff --git a/src/theory/quantifiers/sygus/ce_guided_single_inv_sol.cpp b/src/theory/quantifiers/sygus/ce_guided_single_inv_sol.cpp
index 908dde528..9a6728c29 100644
--- a/src/theory/quantifiers/sygus/ce_guided_single_inv_sol.cpp
+++ b/src/theory/quantifiers/sygus/ce_guided_single_inv_sol.cpp
@@ -873,7 +873,7 @@ bool CegSingleInvSol::getMatch(Node p,
   TermDbSygus* tds = d_qe->getTermDatabaseSygus();
   if (tds->isFreeVar(p))
   {
-    unsigned vnum = tds->getVarNum(p);
+    size_t vnum = tds->getFreeVarId(p);
     Node prev = s[vnum];
     s[vnum] = n;
     if (prev.isNull())
diff --git a/src/theory/quantifiers/sygus/term_database_sygus.cpp b/src/theory/quantifiers/sygus/term_database_sygus.cpp
index ee028bff0..f53637ebb 100644
--- a/src/theory/quantifiers/sygus/term_database_sygus.cpp
+++ b/src/theory/quantifiers/sygus/term_database_sygus.cpp
@@ -65,15 +65,21 @@ bool TermDbSygus::reset( Theory::Effort e ) {
 TNode TermDbSygus::getFreeVar( TypeNode tn, int i, bool useSygusType ) {
   unsigned sindex = 0;
   TypeNode vtn = tn;
-  if( useSygusType ){
-    if( tn.isDatatype() ){
-      const DType& dt = tn.getDType();
-      if( !dt.getSygusType().isNull() ){
-        vtn = dt.getSygusType();
+  TypeNode builtinType = tn;
+  if (tn.isDatatype())
+  {
+    const DType& dt = tn.getDType();
+    if (!dt.getSygusType().isNull())
+    {
+      builtinType = dt.getSygusType();
+      if (useSygusType)
+      {
+        vtn = builtinType;
         sindex = 1;
-      } 
+      }
     }
   }
+  NodeManager* nm = NodeManager::currentNM();
   while( i>=(int)d_fv[sindex][tn].size() ){
     std::stringstream ss;
     if( tn.isDatatype() ){
@@ -83,9 +89,13 @@ TNode TermDbSygus::getFreeVar( TypeNode tn, int i, bool useSygusType ) {
       ss << "fv_" << tn << "_" << i;
     }
     Assert(!vtn.isNull());
-    Node v = NodeManager::currentNM()->mkSkolem( ss.str(), vtn, "for sygus normal form testing" );
-    d_fv_stype[v] = tn;
-    d_fv_num[v] = i;
+    Node v = nm->mkSkolem(ss.str(), vtn, "for sygus invariance testing");
+    // store its id, which is unique per builtin type, regardless of how it is
+    // otherwise cached.
+    d_fvId[v] = d_fvTypeIdCounter[builtinType];
+    d_fvTypeIdCounter[builtinType]++;
+    Trace("sygus-db-debug") << "Free variable id " << v << " = " << d_fvId[v]
+                            << ", " << builtinType << std::endl;
     d_fv[sindex][tn].push_back( v );
   }
   return d_fv[sindex][tn][i];
@@ -103,6 +113,22 @@ TNode TermDbSygus::getFreeVarInc( TypeNode tn, std::map< TypeNode, int >& var_co
   }
 }
 
+bool TermDbSygus::isFreeVar(Node n) const
+{
+  return d_fvId.find(n) != d_fvId.end();
+}
+size_t TermDbSygus::getFreeVarId(Node n) const
+{
+  std::map<Node, size_t>::const_iterator it = d_fvId.find(n);
+  if (it == d_fvId.end())
+  {
+    Assert(false) << "TermDbSygus::isFreeVar: " << n
+                  << " is not a cached free variable.";
+    return 0;
+  }
+  return it->second;
+}
+
 bool TermDbSygus::hasFreeVar( Node n, std::map< Node, bool >& visited ){
   if( visited.find( n )==visited.end() ){
     visited[n] = true;
@@ -153,11 +179,6 @@ Node TermDbSygus::getProxyVariable(TypeNode tn, Node c)
   return it->second;
 }
 
-TypeNode TermDbSygus::getSygusTypeForVar( Node v ) {
-  Assert(d_fv_stype.find(v) != d_fv_stype.end());
-  return d_fv_stype[v];
-}
-
 Node TermDbSygus::mkGeneric(const DType& dt,
                             unsigned c,
                             std::map<TypeNode, int>& var_count,
@@ -321,10 +342,12 @@ Node TermDbSygus::sygusToBuiltin(Node n, TypeNode tn)
   }
   Assert(isFreeVar(n));
   // map to builtin variable type
-  int fv_num = getVarNum(n);
+  size_t fv_num = getFreeVarId(n);
   Assert(!dt.getSygusType().isNull());
   TypeNode vtn = dt.getSygusType();
   Node ret = getFreeVar(vtn, fv_num);
+  Trace("sygus-db-debug") << "SygusToBuiltin: variable for " << n << " is "
+                          << ret << ", fv_num=" << fv_num << std::endl;
   return ret;
 }
 
diff --git a/src/theory/quantifiers/sygus/term_database_sygus.h b/src/theory/quantifiers/sygus/term_database_sygus.h
index 516515c05..acc875780 100644
--- a/src/theory/quantifiers/sygus/term_database_sygus.h
+++ b/src/theory/quantifiers/sygus/term_database_sygus.h
@@ -201,9 +201,9 @@ class TermDbSygus {
                       std::map<TypeNode, int>& var_count,
                       bool useSygusType = false);
   /** returns true if n is a cached free variable (in d_fv). */
-  bool isFreeVar(Node n) { return d_fv_stype.find(n) != d_fv_stype.end(); }
-  /** returns the index of n in the free variable cache (d_fv). */
-  int getVarNum(Node n) { return d_fv_num[n]; }
+  bool isFreeVar(Node n) const;
+  /** returns the identifier for a cached free variable. */
+  size_t getFreeVarId(Node n) const;
   /** returns true if n has a cached free variable (in d_fv). */
   bool hasFreeVar(Node n);
   /** get sygus proxy variable
@@ -373,8 +373,16 @@ class TermDbSygus {
   std::map<TypeNode, std::vector<Node> > d_fv[2];
   /** Maps free variables to the domain type they are associated with in d_fv */
   std::map<Node, TypeNode> d_fv_stype;
-  /** Maps free variables to their index in d_fv. */
-  std::map<Node, int> d_fv_num;
+  /** Id count for free variables terms */
+  std::map<TypeNode, size_t> d_fvTypeIdCounter;
+  /**
+   * Maps free variables to a unique identifier for their builtin type. Notice
+   * that, e.g. free variables of type Int and those that are of a sygus
+   * datatype type that encodes Int must have unique identifiers. This is
+   * to ensure that sygusToBuiltin for non-ground terms maps variables to
+   * unique variabales.
+   */
+  std::map<Node, size_t> d_fvId;
   /** recursive helper for hasFreeVar, visited stores nodes we have visited. */
   bool hasFreeVar(Node n, std::map<Node, bool>& visited);
   /** cache of getProxyVariable */
@@ -440,7 +448,6 @@ class TermDbSygus {
                         std::vector<TypeNode>& argts,
                         bool aggr = false);
 
-  TypeNode getSygusTypeForVar( Node v );
   Node getSygusNormalized( Node n, std::map< TypeNode, int >& var_count, std::map< Node, Node >& subs );
   Node getNormalized(TypeNode t, Node prog);
   unsigned getSygusTermSize( Node n );