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.

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 908dde5282a212d6f05fb0ee46bc42f7dc896e8c..9a6728c299f0c3643f884bc9e58974ba2227f9b1 100644 (file)
--- 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 ee028bff0dcc1c3e344164da97a4c80ed812e9ed..f53637ebba107f0223f18774d768f5a3341c670a 100644 (file)
--- 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 516515c052789dcc7d42b2229557bf55c3cfedc4..acc87578088976c96e0eccb8017ec0fceb9d8f5c 100644 (file)
--- 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 );

diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index 336bbdd3249e5d494b3a365f177d89031574d09c..8a9151c176982da5b6e67e03fbda6159be6666ee 100644 (file)
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -1003,6 +1003,7 @@ set(regress_0_tests
   regress0/sygus/issue3356-syg-inf-usort.smt2
   regress0/sygus/issue3624.sy
   regress0/sygus/issue3645-grammar-sets.smt2
+  regress0/sygus/issue4383-cache-fv-id.sy
   regress0/sygus/let-ringer.sy
   regress0/sygus/let-simp.sy
   regress0/sygus/no-logic.sy

diff --git a/test/regress/regress0/sygus/issue4383-cache-fv-id.sy b/test/regress/regress0/sygus/issue4383-cache-fv-id.sy
new file mode 100644 (file)
index 0000000..27378d9
--- /dev/null
+++ b/test/regress/regress0/sygus/issue4383-cache-fv-id.sy
@@ -0,0 +1,23 @@
+; EXPECT: unsat
+; COMMAND-LINE: --lang=sygus2 --sygus-out=status
+(set-logic ALL)
+(synth-fun args_0_refinement_0 
+       ((r Int)) Bool 
+       ((fv_B Bool)) 
+       (
+               (fv_B Bool (true)) 
+       )
+)
+(synth-fun ret_refinement_0 
+       ((x0 Int) (r Bool)) Bool 
+       ((fv_B Bool) (B Bool) (I Int)) 
+       (
+               (fv_B Bool (r true (=> B fv_B))) 
+               (B Bool ((Variable Bool) (= I I))) 
+               (I Int ((Variable Int) 1)) 
+       )
+)
+(constraint (ret_refinement_0 1 true))
+(constraint (not (ret_refinement_0 1 false)))
+(constraint (and (ret_refinement_0 0 false)))
+(check-synth)