Fix evaluator for non-evaluatable nodes (#3575)

This ensures that the Evaluator always returns the result of substitution + rewriting for constant substitutions.

This requires a few further extensions to the code, namely:
(1) Applying substutitions to operators,
(2) Reconstructing all nodes that fail to evaluate by taking into account evaluation of their children.

diff --git a/src/theory/evaluator.cpp b/src/theory/evaluator.cpp
index 406fb5ead7322a4d847450b9a4f3b73525088956..b5fa79cd0f30aea203d20484a18f9cc7f259f97e 100644 (file)
--- a/src/theory/evaluator.cpp
+++ b/src/theory/evaluator.cpp
@@ -121,7 +121,21 @@ Node Evaluator::eval(TNode n,
   Trace("evaluator") << "Evaluating " << n << " under substitution " << args
                      << " " << vals << std::endl;
   std::unordered_map<TNode, Node, NodeHashFunction> evalAsNode;
-  return evalInternal(n, args, vals, evalAsNode).toNode();
+  Node ret = evalInternal(n, args, vals, evalAsNode).toNode();
+  // if we failed to evaluate
+  if (ret.isNull())
+  {
+    // should be stored in the evaluation-as-node map
+    std::unordered_map<TNode, Node, NodeHashFunction>::iterator itn =
+        evalAsNode.find(n);
+    Assert(itn != evalAsNode.end());
+    ret = itn->second;
+  }
+  // should be the same as substitution + rewriting
+  Assert(ret
+         == Rewriter::rewrite(
+             n.substitute(args.begin(), args.end(), vals.begin(), vals.end())));
+  return ret;
 }
 
 EvalResult Evaluator::evalInternal(
@@ -133,9 +147,7 @@ EvalResult Evaluator::evalInternal(
   std::unordered_map<TNode, EvalResult, TNodeHashFunction> results;
   std::vector<TNode> queue;
   queue.emplace_back(n);
-  std::unordered_map<TNode, Node, NodeHashFunction>::iterator itn;
   std::unordered_map<TNode, EvalResult, TNodeHashFunction>::iterator itr;
-  NodeManager* nm = NodeManager::currentNM();
 
   while (queue.size() != 0)
   {
@@ -149,6 +161,20 @@ EvalResult Evaluator::evalInternal(
 
     bool doProcess = true;
     bool doEval = true;
+    if (currNode.getMetaKind() == kind::metakind::PARAMETERIZED)
+    {
+      TNode op = currNode.getOperator();
+      itr = results.find(op);
+      if (itr == results.end())
+      {
+        queue.emplace_back(op);
+        doProcess = false;
+      }
+      else if (itr->second.d_tag == EvalResult::INVALID)
+      {
+        doEval = false;
+      }
+    }
     for (const auto& currNodeChild : currNode)
     {
       itr = results.find(currNodeChild);
@@ -172,6 +198,8 @@ EvalResult Evaluator::evalInternal(
       queue.pop_back();
 
       Node currNodeVal = currNode;
+      // whether we need to reconstruct the current node in the case of failure
+      bool needsReconstruct = true;
 
       // The code below should either:
       // (1) store a valid EvalResult into results[currNode], or
@@ -185,35 +213,8 @@ EvalResult Evaluator::evalInternal(
         // Reconstruct the node with a combination of the children that
         // successfully evaluated, and the children that did not.
         Trace("evaluator") << "Evaluator: collect arguments" << std::endl;
-        std::vector<Node> echildren;
-        if (currNode.getMetaKind() == kind::metakind::PARAMETERIZED)
-        {
-          echildren.push_back(currNode.getOperator());
-        }
-        for (const auto& currNodeChild : currNode)
-        {
-          itr = results.find(currNodeChild);
-          if (itr->second.d_tag == EvalResult::INVALID)
-          {
-            // could not evaluate this child, look in the node cache
-            itn = evalAsNode.find(currNodeChild);
-            Assert(itn != evalAsNode.end());
-            echildren.push_back(itn->second);
-          }
-          else
-          {
-            // otherwise, use the evaluation
-            echildren.push_back(itr->second.toNode());
-          }
-        }
-        // The value is the result of our (partially) successful evaluation
-        // of the children.
-        currNodeVal = nm->mkNode(currNode.getKind(), echildren);
-        Trace("evaluator") << "Evaluator: partially evaluated " << currNodeVal
-                           << std::endl;
-        // Use rewriting. Notice we do not need to substitute here since
-        // all substitutions should already have been applied recursively.
-        currNodeVal = Rewriter::rewrite(currNodeVal);
+        currNodeVal = reconstruct(currNodeVal, results, evalAsNode);
+        needsReconstruct = false;
         Trace("evaluator") << "Evaluator: now after substitution + rewriting: "
                            << currNodeVal << std::endl;
         if (currNodeVal.getNumChildren() > 0)
@@ -235,16 +236,34 @@ EvalResult Evaluator::evalInternal(
         const auto& it = std::find(args.begin(), args.end(), currNode);
         if (it == args.end())
         {
+          // variable with no substitution is itself
           evalAsNode[currNode] = currNode;
           results[currNode] = EvalResult();
           continue;
         }
         ptrdiff_t pos = std::distance(args.begin(), it);
         currNodeVal = vals[pos];
+        // Don't need to reconstruct since range of substitution should already
+        // be normalized.
+        Assert(vals[pos] == Rewriter::rewrite(vals[pos]));
+        needsReconstruct = false;
       }
-      else if (currNode.getKind() == kind::APPLY_UF
-               && currNode.getOperator().getKind() == kind::LAMBDA)
+      else if (currNode.getKind() == kind::APPLY_UF)
       {
+        Trace("evaluator") << "Evaluate " << currNode << std::endl;
+        TNode op = currNode.getOperator();
+        Assert(evalAsNode.find(op) != evalAsNode.end());
+        // no function can be a valid EvalResult
+        op = evalAsNode[op];
+        Trace("evaluator") << "Operator evaluated to " << op << std::endl;
+        if (op.getKind() != kind::LAMBDA)
+        {
+          // this node is not evaluatable due to operator, must add to
+          // evalAsNode
+          results[currNode] = EvalResult();
+          evalAsNode[currNode] = reconstruct(currNode, results, evalAsNode);
+          continue;
+        }
         // Create a copy of the current substitutions
         std::vector<Node> lambdaArgs(args);
         std::vector<Node> lambdaVals(vals);
@@ -252,7 +271,6 @@ EvalResult Evaluator::evalInternal(
         // Add the values for the arguments of the lambda as substitutions at
         // the beginning of the vector to shadow variables from outer scopes
         // with the same name
-        Node op = currNode.getOperator();
         for (const auto& lambdaArg : op[0])
         {
           lambdaArgs.insert(lambdaArgs.begin(), lambdaArg);
@@ -271,10 +289,14 @@ EvalResult Evaluator::evalInternal(
         std::unordered_map<TNode, Node, NodeHashFunction> evalAsNodeC;
         results[currNode] =
             evalInternal(op[1], lambdaArgs, lambdaVals, evalAsNodeC);
+        Trace("evaluator") << "Evaluated via arguments to "
+                           << results[currNode].d_tag << std::endl;
         if (results[currNode].d_tag == EvalResult::INVALID)
         {
           // evaluation was invalid, we take the node of op[1] as the result
           evalAsNode[currNode] = evalAsNodeC[op[1]];
+          Trace("evaluator")
+              << "Take node evaluation: " << evalAsNodeC[op[1]] << std::endl;
         }
         continue;
       }
@@ -667,7 +689,9 @@ EvalResult Evaluator::evalInternal(
           else
           {
             results[currNode] = EvalResult();
-            evalAsNode[currNode] = currNodeVal;
+            evalAsNode[currNode] =
+                needsReconstruct ? reconstruct(currNode, results, evalAsNode)
+                                 : currNodeVal;
           }
           break;
         }
@@ -684,7 +708,9 @@ EvalResult Evaluator::evalInternal(
           else
           {
             results[currNode] = EvalResult();
-            evalAsNode[currNode] = currNodeVal;
+            evalAsNode[currNode] =
+                needsReconstruct ? reconstruct(currNode, results, evalAsNode)
+                                 : currNodeVal;
           }
           break;
         }
@@ -725,7 +751,9 @@ EvalResult Evaluator::evalInternal(
               Trace("evaluator") << "Theory " << Theory::theoryOf(currNode[0])
                                  << " not supported" << std::endl;
               results[currNode] = EvalResult();
-              evalAsNode[currNode] = currNodeVal;
+              evalAsNode[currNode] =
+                  needsReconstruct ? reconstruct(currNode, results, evalAsNode)
+                                   : currNodeVal;
               break;
             }
           }
@@ -751,7 +779,9 @@ EvalResult Evaluator::evalInternal(
           Trace("evaluator") << "Kind " << currNodeVal.getKind()
                              << " not supported" << std::endl;
           results[currNode] = EvalResult();
-          evalAsNode[currNode] = currNodeVal;
+          evalAsNode[currNode] =
+              needsReconstruct ? reconstruct(currNode, results, evalAsNode)
+                               : currNodeVal;
         }
       }
     }
@@ -760,5 +790,63 @@ EvalResult Evaluator::evalInternal(
   return results[n];
 }
 
+Node Evaluator::reconstruct(
+    TNode n,
+    std::unordered_map<TNode, EvalResult, TNodeHashFunction>& eresults,
+    std::unordered_map<TNode, Node, NodeHashFunction>& evalAsNode)
+{
+  if (n.getNumChildren() == 0)
+  {
+    return n;
+  }
+  Trace("evaluator") << "Evaluator: reconstruct " << n << std::endl;
+  NodeManager* nm = NodeManager::currentNM();
+  std::unordered_map<TNode, EvalResult, TNodeHashFunction>::iterator itr;
+  std::unordered_map<TNode, Node, NodeHashFunction>::iterator itn;
+  std::vector<Node> echildren;
+  if (n.getMetaKind() == kind::metakind::PARAMETERIZED)
+  {
+    TNode op = n.getOperator();
+    itr = eresults.find(op);
+    Assert(itr != eresults.end());
+    if (itr->second.d_tag == EvalResult::INVALID)
+    {
+      // could not evaluate the operator, look in the node cache
+      itn = evalAsNode.find(op);
+      Assert(itn != evalAsNode.end());
+      echildren.push_back(itn->second);
+    }
+    else
+    {
+      // otherwise, use the evaluation of the operator
+      echildren.push_back(itr->second.toNode());
+    }
+  }
+  for (const auto& currNodeChild : n)
+  {
+    itr = eresults.find(currNodeChild);
+    Assert(itr != eresults.end());
+    if (itr->second.d_tag == EvalResult::INVALID)
+    {
+      // could not evaluate this child, look in the node cache
+      itn = evalAsNode.find(currNodeChild);
+      Assert(itn != evalAsNode.end());
+      echildren.push_back(itn->second);
+    }
+    else
+    {
+      // otherwise, use the evaluation
+      echildren.push_back(itr->second.toNode());
+    }
+  }
+  // The value is the result of our (partially) successful evaluation
+  // of the children.
+  Node nn = nm->mkNode(n.getKind(), echildren);
+  Trace("evaluator") << "Evaluator: reconstructed " << nn << std::endl;
+  // Use rewriting. Notice we do not need to substitute here since
+  // all substitutions should already have been applied recursively.
+  return Rewriter::rewrite(nn);
+}
+
 }  // namespace theory
 }  // namespace CVC4

diff --git a/src/theory/evaluator.h b/src/theory/evaluator.h
index a65ffdf1985c7cd20d7dc74f0358a5208483604b..94e6fc5188dbc88abb88e89d8d1e21db6d313076 100644 (file)
--- a/src/theory/evaluator.h
+++ b/src/theory/evaluator.h
@@ -118,6 +118,19 @@ class Evaluator
       const std::vector<Node>& args,
       const std::vector<Node>& vals,
       std::unordered_map<TNode, Node, NodeHashFunction>& evalAsNode);
+  /** reconstruct
+   *
+   * This function reconstructs the result of evaluating n using a combination
+   * of evaluation results (eresults) and substitution+rewriting (evalAsNode).
+   *
+   * Arguments eresults and evalAsNode are built within the context of the
+   * above method for some args and vals. This method ensures that the return
+   * value is equivalent to the rewritten form of n * { args -> vals }.
+   */
+  Node reconstruct(
+      TNode n,
+      std::unordered_map<TNode, EvalResult, TNodeHashFunction>& eresults,
+      std::unordered_map<TNode, Node, NodeHashFunction>& evalAsNode);
 };
 
 }  // namespace theory

diff --git a/src/theory/quantifiers/sygus/term_database_sygus.cpp b/src/theory/quantifiers/sygus/term_database_sygus.cpp
index bce46fb6b98f1d3961b58e10b6800bfab44d1196..0279ca531a4960e8d7827f374b5b69ecfb466fb7 100644 (file)
--- a/src/theory/quantifiers/sygus/term_database_sygus.cpp
+++ b/src/theory/quantifiers/sygus/term_database_sygus.cpp
@@ -981,14 +981,12 @@ Node TermDbSygus::evaluateBuiltin(TypeNode tn,
     // supported by the evaluator
     res = d_eval->eval(bn, varlist, args);
   }
-  if (!res.isNull())
+  if (res.isNull())
   {
-    Assert(res
-           == Rewriter::rewrite(bn.substitute(
-               varlist.begin(), varlist.end(), args.begin(), args.end())));
-    return res;
+    // must do substitution
+    res =
+        bn.substitute(varlist.begin(), varlist.end(), args.begin(), args.end());
   }
-  res = bn.substitute(varlist.begin(), varlist.end(), args.begin(), args.end());
   // Call the rewrite node function, which may involve recursive function
   // evaluation.
   return rewriteNode(res);