Lazy evaluation via rec-funs of ITE expressions (#3482)

2 files changed, 56 insertions, 4 deletions

diff --git a/src/theory/quantifiers/fun_def_evaluator.cpp b/src/theory/quantifiers/fun_def_evaluator.cpp
index 376d0eb47..1528d5338 100644
--- a/src/theory/quantifiers/fun_def_evaluator.cpp
+++ b/src/theory/quantifiers/fun_def_evaluator.cpp
@@ -75,6 +75,13 @@ Node FunDefEvaluator::evaluate(Node n) const
         Trace("fd-eval-debug") << "constant " << cur << std::endl;
         visited[cur] = cur;
       }
+      else if (cur.getKind() == ITE)
+      {
+        Trace("fd-eval-debug") << "ITE " << cur << std::endl;
+        visited[cur] = Node::null();
+        visit.push_back(cur);
+        visit.push_back(cur[0]);
+      }
       else
       {
         Trace("fd-eval-debug") << "recurse " << cur << std::endl;
@@ -102,6 +109,28 @@ Node FunDefEvaluator::evaluate(Node n) const
         {
           children.push_back(cur.getOperator());
         }
+        else if (ck == ITE)
+        {
+          // get evaluation of condition
+          it = visited.find(cur[0]);
+          Assert(it != visited.end());
+          Assert(!it->second.isNull());
+          Assert(it->second.isConst());
+          // pick child to evaluate depending on condition eval
+          unsigned childIdxToEval = it->second.getConst<bool>() ? 1 : 2;
+          Trace("fd-eval-debug2")
+              << "FunDefEvaluator: result of ITE condition : "
+              << it->second.getConst<bool>() << "\n";
+          // the result will be the result of evaluation the child
+          visited[cur] = cur[childIdxToEval];
+          // push back self and child. The child will be evaluated first and
+          // result will be the result of evaluation child
+          visit.push_back(cur);
+          visit.push_back(cur[childIdxToEval]);
+          Trace("fd-eval-debug2") << "FunDefEvaluator: result will be from : "
+                                  << cur[childIdxToEval] << "\n";
+          continue;
+        }
         for (const Node& cn : cur)
         {
           it = visited.find(cn);
@@ -114,6 +143,8 @@ Node FunDefEvaluator::evaluate(Node n) const
         {
           // need to evaluate it
           f = cur.getOperator();
+          Trace("fd-eval-debug2")
+              << "FunDefEvaluator: need to eval " << f << "\n";
           itf = d_funDefMap.find(f);
           if (itf == d_funDefMap.end())
           {
@@ -123,6 +154,8 @@ Node FunDefEvaluator::evaluate(Node n) const
           }
           // get the function definition
           Node sbody = itf->second.d_body;
+          Trace("fd-eval-debug2")
+              << "FunDefEvaluator: definition: " << sbody << "\n";
           const std::vector<Node>& args = itf->second.d_args;
           if (!args.empty())
           {
@@ -131,6 +164,17 @@ Node FunDefEvaluator::evaluate(Node n) const
                 args.begin(), args.end(), children.begin(), children.end());
             // rewrite it
             sbody = Rewriter::rewrite(sbody);
+            if (Trace.isOn("fd-eval-debug2"))
+            {
+              Trace("fd-eval-debug2")
+                  << "FunDefEvaluator: evaluation with args:\n";
+              for (const Node& child : children)
+              {
+                Trace("fd-eval-debug2") << "..." << child << "\n";
+              }
+              Trace("fd-eval-debug2")
+                  << "FunDefEvaluator: results in " << sbody << "\n";
+            }
           }
           // our result is the result of the body
           visited[cur] = sbody;
@@ -164,11 +208,18 @@ Node FunDefEvaluator::evaluate(Node n) const
       }
     }
   } while (!visit.empty());
+  Trace("fd-eval") << "FunDefEvaluator: return " << visited[n];
   Assert(visited.find(n) != visited.end());
   Assert(!visited.find(n)->second.isNull());
-  Assert(visited.find(n)->second.isConst());
-  Trace("fd-eval") << "FunDefEvaluator: return SUCCESS " << visited[n]
-                   << std::endl;
+  if (!visited.find(n)->second.isConst())
+  {
+    visited[n] = Node::null();
+    Trace("fd-eval") << "\n with NONCONST\n";
+  }
+  else
+  {
+    Trace("fd-eval") << "\n with SUCCESS\n";
+  }
   return visited[n];
 }
 
diff --git a/src/theory/quantifiers/sygus/synth_conjecture.cpp b/src/theory/quantifiers/sygus/synth_conjecture.cpp
index 6e69715ef..6591e6828 100644
--- a/src/theory/quantifiers/sygus/synth_conjecture.cpp
+++ b/src/theory/quantifiers/sygus/synth_conjecture.cpp
@@ -591,7 +591,8 @@ bool SynthConjecture::doCheck(std::vector<Node>& lems)
         Trace("cegqi-debug") << "...squery : " << squery << std::endl;
         squery = Rewriter::rewrite(squery);
         Trace("cegqi-debug") << "...rewrites to : " << squery << std::endl;
-        Assert(squery.isConst() && squery.getConst<bool>());
+        Assert(options::sygusRecFun()
+               || (squery.isConst() && squery.getConst<bool>()));
 #endif
         return false;
       }