Optimization for evaluation with unfolding (#2979)

diff --git a/src/theory/quantifiers/sygus/term_database_sygus.cpp b/src/theory/quantifiers/sygus/term_database_sygus.cpp
index b1e6dc96d7ecab8a9d7011e5199d3c5a074512b5..af820b0fcc54105f9386e96fb0459ee889a36127 100644 (file)
--- a/src/theory/quantifiers/sygus/term_database_sygus.cpp
+++ b/src/theory/quantifiers/sygus/term_database_sygus.cpp
@@ -1633,6 +1633,33 @@ Node TermDbSygus::evaluateWithUnfolding(
     while (ret.getKind() == DT_SYGUS_EVAL
            && ret[0].getKind() == APPLY_CONSTRUCTOR)
     {
+      if (ret == n && ret[0].isConst())
+      {
+        Trace("dt-eval-unfold-debug")
+            << "Optimize: evaluate constant head " << ret << std::endl;
+        // can just do direct evaluation here
+        std::vector<Node> args;
+        bool success = true;
+        for (unsigned i = 1, nchild = ret.getNumChildren(); i < nchild; i++)
+        {
+          if (!ret[i].isConst())
+          {
+            success = false;
+            break;
+          }
+          args.push_back(ret[i]);
+        }
+        if (success)
+        {
+          TypeNode rt = ret[0].getType();
+          Node bret = sygusToBuiltin(ret[0], rt);
+          Node rete = evaluateBuiltin(rt, bret, args);
+          visited[n] = rete;
+          Trace("dt-eval-unfold-debug")
+              << "Return " << rete << " for " << n << std::endl;
+          return rete;
+        }
+      }
       ret = unfold( ret );
     }    
     if( ret.getNumChildren()>0 ){