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.

1 files changed, 4 insertions, 6 deletions

diff --git a/src/theory/quantifiers/sygus/term_database_sygus.cpp b/src/theory/quantifiers/sygus/term_database_sygus.cpp
index bce46fb6b..0279ca531 100644
--- 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);