Merge branch 'master' of https://github.com/CVC4/CVC4 into sygusComp2018-2

10 files changed, 312 insertions, 597 deletions

diff --git a/contrib/run-script-cascj9-tfn-nr b/contrib/run-script-cascj9-tfn-nr
new file mode 100644
index 000000000..8124fd6f9
--- /dev/null
+++ b/contrib/run-script-cascj9-tfn-nr
@@ -0,0 +1,36 @@
+#!/bin/bash
+
+here=`dirname $0`
+cvc4=$here/cvc4
+bench="$1"
+
+file=${bench##*/}
+filename=${file%.*}
+
+echo "------- cvc4-tfn casc j9 : $bench at $2..."
+
+# use: trywith [params..]
+# to attempt a run.  If an SZS ontology result is printed, then
+# the run script terminates immediately.  Otherwise, this
+# function returns normally.
+function trywith {
+  limit=$1; shift;
+  echo "--- Run $@ at $limit...";
+  (ulimit -S -t "$limit";$cvc4 --lang=tptp --no-checking --no-interactive --force-logic="UFNIRA" --dump-models --produce-models --force-no-limit-cpu-while-dump "$@" $bench) 2>/dev/null |
+  (read w1 w2 w3 result w4 w5;
+  case "$result" in
+  Satisfiable) echo "$w1 $w2 $w3 $result $w4 $w5";cat;exit 0;;
+  CounterSatisfiable) echo "$w1 $w2 $w3 $result $w4 $w5";cat;exit 0;;
+  esac; exit 1)
+  if [ ${PIPESTATUS[1]} -eq 0 ]; then exit 0; fi
+}
+function finishwith {
+  echo "--- Run $@...";
+  $cvc4 --lang=tptp --no-checking --no-interactive --force-logic="UFNIRA" --dump-models --produce-models --force-no-limit-cpu-while-dump "$@" $bench
+}
+
+# designed for 300 seconds
+trywith 30 --finite-model-find --decision=internal --sort-inference --macros-quant --macros-quant-mode=all
+trywith 15 --nl-ext-tplanes --full-saturate-quant --macros-quant --macros-quant-mode=all
+finishwith --finite-model-find --fmf-inst-engine --sort-inference --macros-quant --macros-quant-mode=all
+# echo "% SZS status" "GaveUp for $filename"
diff --git a/src/printer/dagification_visitor.cpp b/src/printer/dagification_visitor.cpp
index 7c0cc3101..202249759 100644
--- a/src/printer/dagification_visitor.cpp
+++ b/src/printer/dagification_visitor.cpp
@@ -46,20 +46,25 @@ DagificationVisitor::~DagificationVisitor() {
 }
 
 bool DagificationVisitor::alreadyVisited(TNode current, TNode parent) {
+  Kind ck = current.getKind();
+  if (ck == kind::FORALL || ck == kind::EXISTS || ck == kind::LAMBDA
+      || ck == kind::CHOICE)
+  {
+    // for quantifiers, we visit them but we don't recurse on them
+    visit(current, parent);
+    return true;
+  }
   // don't visit variables, constants, or those exprs that we've
   // already seen more than the threshold: if we've increased
   // the count beyond the threshold already, we've done the same
   // for all subexpressions, so it isn't useful to traverse and
   // increment again (they'll be dagified anyway).
-  return current.isVar() ||
-         current.getMetaKind() == kind::metakind::CONSTANT ||
-         current.getNumChildren()==0 ||
-         ( ( current.getKind() == kind::NOT ||
-             current.getKind() == kind::UMINUS ) &&
-           ( current[0].isVar() ||
-             current[0].getMetaKind() == kind::metakind::CONSTANT ) ) ||
-         current.getKind() == kind::SORT_TYPE ||
-         d_nodeCount[current] > d_threshold;
+  return current.isVar() || current.getMetaKind() == kind::metakind::CONSTANT
+         || current.getNumChildren() == 0
+         || ((ck == kind::NOT || ck == kind::UMINUS)
+             && (current[0].isVar()
+                 || current[0].getMetaKind() == kind::metakind::CONSTANT))
+         || ck == kind::SORT_TYPE || d_nodeCount[current] > d_threshold;
 }
 
 void DagificationVisitor::visit(TNode current, TNode parent) {
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 22c0bcf13..331e27d95 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -1656,12 +1656,13 @@ void SmtEngine::setDefaults() {
     }
   }
 
-  // by default, symmetry breaker is on only for QF_UF
+  // by default, symmetry breaker is on only for non-incremental QF_UF
   if(! options::ufSymmetryBreaker.wasSetByUser()) {
-    bool qf_uf = d_logic.isPure(THEORY_UF) && !d_logic.isQuantified()
-                 && !options::proof() && !options::unsatCores();
-    Trace("smt") << "setting uf symmetry breaker to " << qf_uf << endl;
-    options::ufSymmetryBreaker.set(qf_uf);
+    bool qf_uf_noinc = d_logic.isPure(THEORY_UF) && !d_logic.isQuantified()
+                       && !options::incrementalSolving() && !options::proof()
+                       && !options::unsatCores();
+    Trace("smt") << "setting uf symmetry breaker to " << qf_uf_noinc << endl;
+    options::ufSymmetryBreaker.set(qf_uf_noinc);
   }
 
   // If in arrays, set the UF handler to arrays
diff --git a/src/theory/evaluator.cpp b/src/theory/evaluator.cpp
index 0d1536084..0d7ddbec8 100644
--- a/src/theory/evaluator.cpp
+++ b/src/theory/evaluator.cpp
@@ -1,499 +1,113 @@
 /*********************                                                        */
-/*! \file evaluator.cpp
+/*! \file evaluator.h
  ** \verbatim
  ** Top contributors (to current version):
  **   Andres Noetzli
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS
  ** in the top-level source directory) and their institutional affiliations.
  ** All rights reserved.  See the file COPYING in the top-level source
  ** directory for licensing information.\endverbatim
  **
  ** \brief The Evaluator class
  **
- ** The Evaluator class.
+ ** The Evaluator class can be used to evaluate terms with constant leaves
+ ** quickly, without going through the rewriter.
  **/
 
-#include "theory/evaluator.h"
+#include "cvc4_private.h"
 
-#include "theory/bv/theory_bv_utils.h"
-#include "theory/theory.h"
-#include "util/integer.h"
+#ifndef __CVC4__THEORY__EVALUATOR_H
+#define __CVC4__THEORY__EVALUATOR_H
+
+#include <utility>
+#include <vector>
+
+#include "base/output.h"
+#include "expr/node.h"
+#include "util/bitvector.h"
+#include "util/rational.h"
+#include "util/regexp.h"
 
 namespace CVC4 {
 namespace theory {
 
-Node Evaluator::eval(TNode n,
-                     const std::vector<Node>& args,
-                     const std::vector<Node>& vals)
-{
-  Trace("evaluator") << "Evaluating " << n << " under substitution " << args
-                     << " " << vals << std::endl;
-  return evalInternal(n, args, vals).toNode();
-}
-
-EvalResult Evaluator::evalInternal(TNode n,
-                                   const std::vector<Node>& args,
-                                   const std::vector<Node>& vals)
+/**
+ * Struct that holds the result of an evaluation. The actual value is stored in
+ * a union to avoid the overhead of a class hierarchy with virtual methods.
+ */
+struct EvalResult
 {
-  std::unordered_map<TNode, EvalResult, TNodeHashFunction> results;
-  std::vector<TNode> queue;
-  queue.emplace_back(n);
-
-  while (queue.size() != 0)
+  /* Describes which type of result is being stored */
+  enum
   {
-    TNode currNode = queue.back();
-
-    if (results.find(currNode) != results.end())
-    {
-      queue.pop_back();
-      continue;
-    }
-
-    bool doEval = true;
-    for (const auto& currNodeChild : currNode)
-    {
-      if (results.find(currNodeChild) == results.end())
-      {
-        queue.emplace_back(currNodeChild);
-        doEval = false;
-      }
-    }
-
-    if (doEval)
-    {
-      queue.pop_back();
-
-      Node currNodeVal = currNode;
-      if (currNode.isVar())
-      {
-        const auto& it = std::find(args.begin(), args.end(), currNode);
-
-        if (it == args.end())
-        {
-          return EvalResult();
-        }
-
-        ptrdiff_t pos = std::distance(args.begin(), it);
-        currNodeVal = vals[pos];
-      }
-      else if (currNode.getKind() == kind::APPLY_UF
-               && currNode.getOperator().getKind() == kind::LAMBDA)
-      {
-        std::vector<Node> lambdaArgs(args);
-        std::vector<Node> lambdaVals(vals);
-
-        Node op = currNode.getOperator();
-        for (const auto& lambdaArg : op[0])
-        {
-          lambdaArgs.insert(lambdaArgs.begin(), lambdaArg);
-        }
-
-        for (const auto& lambdaVal : currNode)
-        {
-          lambdaVals.insert(lambdaVals.begin(), results[lambdaVal].toNode());
-        }
-
-        results[currNode] = evalInternal(op[1], lambdaArgs, lambdaVals);
-        continue;
-      }
-
-      switch (currNodeVal.getKind())
-      {
-        case kind::CONST_BOOLEAN:
-          results[currNode] = EvalResult(currNodeVal.getConst<bool>());
-          break;
-
-        case kind::NOT:
-        {
-          results[currNode] = EvalResult(!(results[currNode[0]].d_bool));
-          break;
-        }
-
-        case kind::AND:
-        {
-          bool res = results[currNode[0]].d_bool;
-          for (size_t i = 1, end = currNode.getNumChildren(); i < end; i++)
-          {
-            res = res && results[currNode[i]].d_bool;
-          }
-          results[currNode] = EvalResult(res);
-          break;
-        }
-
-        case kind::OR:
-        {
-          bool res = results[currNode[0]].d_bool;
-          for (size_t i = 1, end = currNode.getNumChildren(); i < end; i++)
-          {
-            res = res || results[currNode[i]].d_bool;
-          }
-          results[currNode] = EvalResult(res);
-          break;
-        }
-
-        case kind::CONST_RATIONAL:
-        {
-          const Rational& r = currNodeVal.getConst<Rational>();
-          results[currNode] = EvalResult(r);
-          break;
-        }
-
-        case kind::PLUS:
-        {
-          Rational res = results[currNode[0]].d_rat;
-          for (size_t i = 1, end = currNode.getNumChildren(); i < end; i++)
-          {
-            res = res + results[currNode[i]].d_rat;
-          }
-          results[currNode] = EvalResult(res);
-          break;
-        }
-
-        case kind::MINUS:
-        {
-          const Rational& x = results[currNode[0]].d_rat;
-          const Rational& y = results[currNode[1]].d_rat;
-          results[currNode] = EvalResult(x - y);
-          break;
-        }
-
-        case kind::MULT:
-        {
-          Rational res = results[currNode[0]].d_rat;
-          for (size_t i = 1, end = currNode.getNumChildren(); i < end; i++)
-          {
-            res = res * results[currNode[i]].d_rat;
-          }
-          results[currNode] = EvalResult(res);
-          break;
-        }
-
-        case kind::GEQ:
-        {
-          const Rational& x = results[currNode[0]].d_rat;
-          const Rational& y = results[currNode[1]].d_rat;
-          results[currNode] = EvalResult(x >= y);
-          break;
-        }
-
-        case kind::CONST_STRING:
-          results[currNode] = EvalResult(currNodeVal.getConst<String>());
-          break;
-
-        case kind::STRING_CONCAT:
-        {
-          String res = results[currNode[0]].d_str;
-          for (size_t i = 1, end = currNode.getNumChildren(); i < end; i++)
-          {
-            res = res.concat(results[currNode[i]].d_str);
-          }
-          results[currNode] = EvalResult(res);
-          break;
-        }
-
-        case kind::STRING_LENGTH:
-        {
-          const String& s = results[currNode[0]].d_str;
-          results[currNode] = EvalResult(Rational(s.size()));
-          break;
-        }
-
-        case kind::STRING_SUBSTR:
-        {
-          const String& s = results[currNode[0]].d_str;
-          Integer s_len(s.size());
-          Integer i = results[currNode[1]].d_rat.getNumerator();
-          Integer j = results[currNode[2]].d_rat.getNumerator();
-
-          if (i.strictlyNegative() || j.strictlyNegative() || i >= s_len)
-          {
-            results[currNode] = EvalResult(String(""));
-          }
-          else if (i + j > s_len)
-          {
-            results[currNode] =
-                EvalResult(s.suffix((s_len - i).toUnsignedInt()));
-          }
-          else
-          {
-            results[currNode] =
-                EvalResult(s.substr(i.toUnsignedInt(), j.toUnsignedInt()));
-          }
-          break;
-        }
-
-        case kind::STRING_CHARAT:
-        {
-          const String& s = results[currNode[0]].d_str;
-          Integer s_len(s.size());
-          Integer i = results[currNode[1]].d_rat.getNumerator();
-          if (i.strictlyNegative() || i >= s_len)
-          {
-            results[currNode] = EvalResult(String(""));
-          }
-          else
-          {
-            results[currNode] = EvalResult(s.substr(i.toUnsignedInt(), 1));
-          }
-          break;
-        }
-
-        case kind::STRING_STRCTN:
-        {
-          const String& s = results[currNode[0]].d_str;
-          const String& t = results[currNode[1]].d_str;
-          results[currNode] = EvalResult(s.find(t) != std::string::npos);
-          break;
-        }
-
-        case kind::STRING_STRIDOF:
-        {
-          const String& s = results[currNode[0]].d_str;
-          Integer s_len(s.size());
-          const String& x = results[currNode[1]].d_str;
-          Integer i = results[currNode[2]].d_rat.getNumerator();
-
-          if (i.strictlyNegative() || i >= s_len)
-          {
-            results[currNode] = EvalResult(Rational(-1));
-          }
-          else
-          {
-            size_t r = s.find(x, i.toUnsignedInt());
-            if (r == std::string::npos)
-            {
-              results[currNode] = EvalResult(Rational(-1));
-            }
-            else
-            {
-              results[currNode] = EvalResult(Rational(r));
-            }
-          }
-          break;
-        }
-
-        case kind::STRING_STRREPL:
-        {
-          const String& s = results[currNode[0]].d_str;
-          const String& x = results[currNode[1]].d_str;
-          const String& y = results[currNode[2]].d_str;
-          results[currNode] = EvalResult(s.replace(x, y));
-          break;
-        }
-
-        case kind::STRING_PREFIX:
-        {
-          const String& t = results[currNode[0]].d_str;
-          const String& s = results[currNode[1]].d_str;
-          if (s.size() < t.size())
-          {
-            results[currNode] = EvalResult(false);
-          }
-          else
-          {
-            results[currNode] = EvalResult(s.prefix(t.size()) == t);
-          }
-          break;
-        }
-
-        case kind::STRING_SUFFIX:
-        {
-          const String& t = results[currNode[0]].d_str;
-          const String& s = results[currNode[1]].d_str;
-          if (s.size() < t.size())
-          {
-            results[currNode] = EvalResult(false);
-          }
-          else
-          {
-            results[currNode] = EvalResult(s.suffix(t.size()) == t);
-          }
-          break;
-        }
-
-        case kind::STRING_ITOS:
-        {
-          Integer i = results[currNode[0]].d_rat.getNumerator();
-          if (i.strictlyNegative())
-          {
-            results[currNode] = EvalResult(String(""));
-          }
-          else
-          {
-            results[currNode] = EvalResult(String(i.toString()));
-          }
-          break;
-        }
-
-        case kind::STRING_STOI:
-        {
-          const String& s = results[currNode[0]].d_str;
-          if (s.isNumber())
-          {
-            results[currNode] = EvalResult(Rational(-1));
-          }
-          else
-          {
-            results[currNode] = EvalResult(Rational(s.toNumber()));
-          }
-          break;
-        }
-
-        case kind::CONST_BITVECTOR:
-          results[currNode] = EvalResult(currNodeVal.getConst<BitVector>());
-          break;
-
-        case kind::BITVECTOR_NOT:
-          results[currNode] = EvalResult(~results[currNode[0]].d_bv);
-          break;
-
-        case kind::BITVECTOR_NEG:
-          results[currNode] = EvalResult(-results[currNode[0]].d_bv);
-          break;
-
-        case kind::BITVECTOR_EXTRACT:
-        {
-          unsigned lo = bv::utils::getExtractLow(currNodeVal);
-          unsigned hi = bv::utils::getExtractHigh(currNodeVal);
-          results[currNode] =
-              EvalResult(results[currNode[0]].d_bv.extract(hi, lo));
-          break;
-        }
-
-        case kind::BITVECTOR_CONCAT:
-        {
-          BitVector res = results[currNode[0]].d_bv;
-          for (size_t i = 1, end = currNode.getNumChildren(); i < end; i++)
-          {
-            res = res.concat(results[currNode[i]].d_bv);
-          }
-          results[currNode] = EvalResult(res);
-          break;
-        }
-
-        case kind::BITVECTOR_PLUS:
-        {
-          BitVector res = results[currNode[0]].d_bv;
-          for (size_t i = 1, end = currNode.getNumChildren(); i < end; i++)
-          {
-            res = res + results[currNode[i]].d_bv;
-          }
-          results[currNode] = EvalResult(res);
-          break;
-        }
-
-        case kind::BITVECTOR_MULT:
-        {
-          BitVector res = results[currNode[0]].d_bv;
-          for (size_t i = 1, end = currNode.getNumChildren(); i < end; i++)
-          {
-            res = res * results[currNode[i]].d_bv;
-          }
-          results[currNode] = EvalResult(res);
-          break;
-        }
-        case kind::BITVECTOR_AND:
-        {
-          BitVector res = results[currNode[0]].d_bv;
-          for (size_t i = 1, end = currNode.getNumChildren(); i < end; i++)
-          {
-            res = res & results[currNode[i]].d_bv;
-          }
-          results[currNode] = EvalResult(res);
-          break;
-        }
-
-        case kind::BITVECTOR_OR:
-        {
-          BitVector res = results[currNode[0]].d_bv;
-          for (size_t i = 1, end = currNode.getNumChildren(); i < end; i++)
-          {
-            res = res | results[currNode[i]].d_bv;
-          }
-          results[currNode] = EvalResult(res);
-          break;
-        }
-
-        case kind::BITVECTOR_XOR:
-        {
-          BitVector res = results[currNode[0]].d_bv;
-          for (size_t i = 1, end = currNode.getNumChildren(); i < end; i++)
-          {
-            res = res ^ results[currNode[i]].d_bv;
-          }
-          results[currNode] = EvalResult(res);
-          break;
-        }
-
-        case kind::EQUAL:
-        {
-          EvalResult lhs = results[currNode[0]];
-          EvalResult rhs = results[currNode[1]];
-
-          switch (lhs.d_tag)
-          {
-            case EvalResult::BOOL:
-            {
-              results[currNode] = EvalResult(lhs.d_bool == rhs.d_bool);
-              break;
-            }
-
-            case EvalResult::BITVECTOR:
-            {
-              results[currNode] = EvalResult(lhs.d_bv == rhs.d_bv);
-              break;
-            }
-
-            case EvalResult::RATIONAL:
-            {
-              results[currNode] = EvalResult(lhs.d_rat == rhs.d_rat);
-              break;
-            }
-
-            case EvalResult::STRING:
-            {
-              results[currNode] = EvalResult(lhs.d_str == rhs.d_str);
-              break;
-            }
-
-            default:
-            {
-              Trace("evaluator") << "Theory " << Theory::theoryOf(currNode[0])
-                                 << " not supported" << std::endl;
-              return EvalResult();
-              break;
-            }
-          }
-
-          break;
-        }
-
-        case kind::ITE:
-        {
-          if (results[currNode[0]].d_bool)
-          {
-            results[currNode] = results[currNode[1]];
-          }
-          else
-          {
-            results[currNode] = results[currNode[2]];
-          }
-          break;
-        }
-
-        default:
-        {
-          Trace("evaluator") << "Kind " << currNodeVal.getKind()
-                             << " not supported" << std::endl;
-          return EvalResult();
-        }
-      }
-    }
-  }
-
-  return results[n];
-}
+    BOOL,
+    BITVECTOR,
+    RATIONAL,
+    STRING,
+    INVALID
+  } d_tag;
+
+  /* Stores the actual result */
+  union
+  {
+    bool d_bool;
+    BitVector d_bv;
+    Rational d_rat;
+    String d_str;
+  };
+
+  EvalResult(const EvalResult& other);
+  EvalResult() : d_tag(INVALID) {}
+  EvalResult(bool b) : d_tag(BOOL), d_bool(b) {}
+  EvalResult(const BitVector& bv) : d_tag(BITVECTOR), d_bv(bv) {}
+  EvalResult(const Rational& i) : d_tag(RATIONAL), d_rat(i) {}
+  EvalResult(const String& str) : d_tag(STRING), d_str(str) {}
+
+  EvalResult& operator=(const EvalResult& other);
+
+  ~EvalResult();
+
+  /**
+   * Converts the result to a Node. If the result is not valid, this function
+   * returns the null node.
+   */
+  Node toNode() const;
+};
+
+/**
+ * The class that performs the actual evaluation of a term under a
+ * substitution. Right now, the class does not cache anything between different
+ * calls to `eval` but this might change in the future.
+ */
+class Evaluator
+{
+ public:
+  /**
+   * Evaluates node `n` under the substitution described by the variable names
+   * `args` and the corresponding values `vals`. The function returns a null
+   * node if there is a subterm that is not constant under the substitution or
+   * if an operator is not supported by the evaluator.
+   */
+  Node eval(TNode n,
+            const std::vector<Node>& args,
+            const std::vector<Node>& vals);
+
+ private:
+  /**
+   * Evaluates node `n` under the substitution described by the variable names
+   * `args` and the corresponding values `vals`. The internal version returns
+   * an EvalResult which has slightly less overhead for recursive calls. The
+   * function returns an invalid result if there is a subterm that is not
+   * constant under the substitution or if an operator is not supported by the
+   * evaluator.
+   */
+  EvalResult evalInternal(TNode n,
+                          const std::vector<Node>& args,
+                          const std::vector<Node>& vals);
+};
 
 }  // namespace theory
 }  // namespace CVC4
+
+#endif /* __CVC4__THEORY__EVALUATOR_H */
diff --git a/src/theory/evaluator.h b/src/theory/evaluator.h
index cee8a0d21..0d7ddbec8 100644
--- a/src/theory/evaluator.h
+++ b/src/theory/evaluator.h
@@ -4,19 +4,21 @@
  ** Top contributors (to current version):
  **   Andres Noetzli
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS
  ** in the top-level source directory) and their institutional affiliations.
  ** All rights reserved.  See the file COPYING in the top-level source
  ** directory for licensing information.\endverbatim
  **
  ** \brief The Evaluator class
  **
- ** The Evaluator class.
+ ** The Evaluator class can be used to evaluate terms with constant leaves
+ ** quickly, without going through the rewriter.
  **/
 
 #include "cvc4_private.h"
 
-#pragma once
+#ifndef __CVC4__THEORY__EVALUATOR_H
+#define __CVC4__THEORY__EVALUATOR_H
 
 #include <utility>
 #include <vector>
@@ -30,8 +32,13 @@
 namespace CVC4 {
 namespace theory {
 
+/**
+ * Struct that holds the result of an evaluation. The actual value is stored in
+ * a union to avoid the overhead of a class hierarchy with virtual methods.
+ */
 struct EvalResult
 {
+  /* Describes which type of result is being stored */
   enum
   {
     BOOL,
@@ -41,6 +48,7 @@ struct EvalResult
     INVALID
   } d_tag;
 
+  /* Stores the actual result */
   union
   {
     bool d_bool;
@@ -49,117 +57,51 @@ struct EvalResult
     String d_str;
   };
 
-  EvalResult(const EvalResult& other)
-  {
-    d_tag = other.d_tag;
-    switch (d_tag)
-    {
-      case BOOL: d_bool = other.d_bool; break;
-      case BITVECTOR:
-        new (&d_bv) BitVector;
-        d_bv = other.d_bv;
-        break;
-      case RATIONAL:
-        new (&d_rat) Rational;
-        d_rat = other.d_rat;
-        break;
-      case STRING:
-        new (&d_str) String;
-        d_str = other.d_str;
-        break;
-      case INVALID: break;
-    }
-  }
-
+  EvalResult(const EvalResult& other);
   EvalResult() : d_tag(INVALID) {}
-
   EvalResult(bool b) : d_tag(BOOL), d_bool(b) {}
-
   EvalResult(const BitVector& bv) : d_tag(BITVECTOR), d_bv(bv) {}
-
   EvalResult(const Rational& i) : d_tag(RATIONAL), d_rat(i) {}
-
   EvalResult(const String& str) : d_tag(STRING), d_str(str) {}
 
-  EvalResult& operator=(const EvalResult& other)
-  {
-    if (this != &other)
-    {
-      d_tag = other.d_tag;
-      switch (d_tag)
-      {
-        case BOOL: d_bool = other.d_bool; break;
-        case BITVECTOR:
-          new (&d_bv) BitVector;
-          d_bv = other.d_bv;
-          break;
-        case RATIONAL:
-          new (&d_rat) Rational;
-          d_rat = other.d_rat;
-          break;
-        case STRING:
-          new (&d_str) String;
-          d_str = other.d_str;
-          break;
-        case INVALID: break;
-      }
-    }
-    return *this;
-  }
-
-  ~EvalResult()
-  {
-    switch (d_tag)
-    {
-      case BITVECTOR:
-      {
-        d_bv.~BitVector();
-        break;
-      }
-      case RATIONAL:
-      {
-        d_rat.~Rational();
-        break;
-      }
-      case STRING:
-      {
-        d_str.~String();
-        break;
+  EvalResult& operator=(const EvalResult& other);
 
-        default: break;
-      }
-    }
-  }
+  ~EvalResult();
 
-  Node toNode()
-  {
-    NodeManager* nm = NodeManager::currentNM();
-    switch (d_tag)
-    {
-      case EvalResult::BOOL: return nm->mkConst(d_bool);
-      case EvalResult::BITVECTOR: return nm->mkConst(d_bv);
-      case EvalResult::RATIONAL: return nm->mkConst(d_rat);
-      case EvalResult::STRING: return nm->mkConst(d_str);
-      default:
-      {
-        Trace("evaluator") << "Missing conversion from " << d_tag << " to node"
-                           << std::endl;
-        return Node();
-      }
-    }
-
-    return Node();
-  }
+  /**
+   * Converts the result to a Node. If the result is not valid, this function
+   * returns the null node.
+   */
+  Node toNode() const;
 };
 
+/**
+ * The class that performs the actual evaluation of a term under a
+ * substitution. Right now, the class does not cache anything between different
+ * calls to `eval` but this might change in the future.
+ */
 class Evaluator
 {
  public:
+  /**
+   * Evaluates node `n` under the substitution described by the variable names
+   * `args` and the corresponding values `vals`. The function returns a null
+   * node if there is a subterm that is not constant under the substitution or
+   * if an operator is not supported by the evaluator.
+   */
   Node eval(TNode n,
             const std::vector<Node>& args,
             const std::vector<Node>& vals);
 
  private:
+  /**
+   * Evaluates node `n` under the substitution described by the variable names
+   * `args` and the corresponding values `vals`. The internal version returns
+   * an EvalResult which has slightly less overhead for recursive calls. The
+   * function returns an invalid result if there is a subterm that is not
+   * constant under the substitution or if an operator is not supported by the
+   * evaluator.
+   */
   EvalResult evalInternal(TNode n,
                           const std::vector<Node>& args,
                           const std::vector<Node>& vals);
@@ -167,3 +109,5 @@ class Evaluator
 
 }  // namespace theory
 }  // namespace CVC4
+
+#endif /* __CVC4__THEORY__EVALUATOR_H */
diff --git a/src/theory/quantifiers/ematching/inst_match_generator.cpp b/src/theory/quantifiers/ematching/inst_match_generator.cpp
index 6fd9ae418..90d1815a4 100644
--- a/src/theory/quantifiers/ematching/inst_match_generator.cpp
+++ b/src/theory/quantifiers/ematching/inst_match_generator.cpp
@@ -421,7 +421,7 @@ int InstMatchGenerator::getNextMatch(Node f,
         Trace("matching-summary") << "Try " << d_match_pattern << " : " << t << std::endl;
         success = getMatch(f, t, m, qe, tparent);
         if( d_independent_gen && success<0 ){
-          Assert( d_eq_class.isNull() );
+          Assert(d_eq_class.isNull() || !d_eq_class_rel.isNull());
           d_curr_exclude_match[t] = true;
         }
       }
diff --git a/src/theory/quantifiers/sygus/term_database_sygus.cpp b/src/theory/quantifiers/sygus/term_database_sygus.cpp
index a6b2b617c..5e2187e7a 100644
--- a/src/theory/quantifiers/sygus/term_database_sygus.cpp
+++ b/src/theory/quantifiers/sygus/term_database_sygus.cpp
@@ -24,6 +24,8 @@
 #include "theory/quantifiers/term_database.h"
 #include "theory/quantifiers/term_util.h"
 #include "theory/quantifiers_engine.h"
+#include "options/base_options.h"
+#include "printer/printer.h"
 
 using namespace CVC4::kind;
 
@@ -1761,14 +1763,6 @@ Node TermDbSygus::evaluateBuiltin(TypeNode tn,
     }
     if (!res.isNull())
     {
-      /*
-      std::cout << bn << std::endl;
-      std::cout << res << std::endl;
-      std::cout << Rewriter::rewrite(bn.substitute(it->second.begin(),
-                                                it->second.end(),
-                                                args.begin(),
-                                                args.end())) << std::endl;
-                                                */
       Assert(res
              == Rewriter::rewrite(bn.substitute(it->second.begin(),
                                                 it->second.end(),
diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp
index 1fa3514c8..37f11f9cd 100644
--- a/src/theory/quantifiers_engine.cpp
+++ b/src/theory/quantifiers_engine.cpp
@@ -799,8 +799,6 @@ void QuantifiersEngine::registerQuantifierInternal(Node f)
       // this call
       Assert(d_lemmas_waiting.size() == prev_lemma_waiting);
     }
-    // TODO (#2020): remove this
-    Node ceBody = d_term_util->getInstConstantBody(f);
     Trace("quant-debug") << "...finish." << std::endl;
     d_quants[f] = true;
     AlwaysAssert(d_lemmas_waiting.size() == prev_lemma_waiting);
diff --git a/test/unit/Makefile.am b/test/unit/Makefile.am
index a17687101..b81a729ee 100644
--- a/test/unit/Makefile.am
+++ b/test/unit/Makefile.am
@@ -6,6 +6,7 @@ UNIT_TESTS = \
 	util/cardinality_public
 if WHITE_AND_BLACK_TESTS
 UNIT_TESTS += \
+	theory/evaluator_white \
 	theory/logic_info_white \
 	theory/theory_arith_white \
 	theory/theory_black \
diff --git a/test/unit/theory/evaluator_white.h b/test/unit/theory/evaluator_white.h
new file mode 100644
index 000000000..4416ee00a
--- /dev/null
+++ b/test/unit/theory/evaluator_white.h
@@ -0,0 +1,122 @@
+/*********************                                                        */
+/*! \file evaluator_white.h
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   Andres Noetzli
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS
+ ** in the top-level source directory) and their institutional affiliations.
+ ** All rights reserved.  See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
+ **
+ ** \brief [[ Add one-line brief description here ]]
+ **
+ ** [[ Add lengthier description here ]]
+ ** \todo document this file
+ **/
+
+#include <cxxtest/TestSuite.h>
+#include <vector>
+
+#include "expr/node.h"
+#include "expr/node_manager.h"
+#include "smt/smt_engine.h"
+#include "smt/smt_engine_scope.h"
+#include "theory/bv/theory_bv_utils.h"
+#include "theory/evaluator.h"
+#include "theory/rewriter.h"
+#include "theory/theory_test_utils.h"
+
+using namespace CVC4;
+using namespace CVC4::smt;
+using namespace CVC4::theory;
+
+using namespace std;
+
+class TheoryEvaluatorWhite : public CxxTest::TestSuite
+{
+  ExprManager *d_em;
+  NodeManager *d_nm;
+  SmtEngine *d_smt;
+  SmtScope *d_scope;
+
+ public:
+  TheoryEvaluatorWhite() {}
+
+  void setUp()
+  {
+    Options opts;
+    opts.setOutputLanguage(language::output::LANG_SMTLIB_V2);
+    d_em = new ExprManager(opts);
+    d_nm = NodeManager::fromExprManager(d_em);
+    d_smt = new SmtEngine(d_em);
+    d_scope = new SmtScope(d_smt);
+  }
+
+  void tearDown()
+  {
+    delete d_scope;
+    delete d_smt;
+    delete d_em;
+  }
+
+  void testSimple()
+  {
+    TypeNode bv64Type = d_nm->mkBitVectorType(64);
+
+    Node w = d_nm->mkVar("w", bv64Type);
+    Node x = d_nm->mkVar("x", bv64Type);
+    Node y = d_nm->mkVar("y", bv64Type);
+    Node z = d_nm->mkVar("z", bv64Type);
+
+    Node zero = d_nm->mkConst(BitVector(64, (unsigned int)0));
+    Node one = d_nm->mkConst(BitVector(64, (unsigned int)1));
+    Node c1 = d_nm->mkConst(BitVector(
+        64,
+        (unsigned int)0b0000000100000101001110111001101000101110011101011011110011100111));
+    Node c2 = d_nm->mkConst(BitVector(
+        64,
+        (unsigned int)0b0000000100000101001110111001101000101110011101011011110011100111));
+
+    Node t = d_nm->mkNode(kind::ITE, d_nm->mkNode(kind::EQUAL, y, one), x, w);
+
+    std::vector<Node> args = {w, x, y, z};
+    std::vector<Node> vals = {c1, zero, one, c1};
+
+    Evaluator eval;
+    Node r = eval.eval(t, args, vals);
+    TS_ASSERT_EQUALS(r,
+                     Rewriter::rewrite(t.substitute(
+                         args.begin(), args.end(), vals.begin(), vals.end())));
+  }
+
+  void testLoop()
+  {
+    TypeNode bv64Type = d_nm->mkBitVectorType(64);
+
+    Node w = d_nm->mkBoundVar(bv64Type);
+    Node x = d_nm->mkVar("x", bv64Type);
+
+    Node zero = d_nm->mkConst(BitVector(1, (unsigned int)0));
+    Node one = d_nm->mkConst(BitVector(64, (unsigned int)1));
+    Node c = d_nm->mkConst(BitVector(
+        64,
+        (unsigned int)0b0001111000010111110000110110001101011110111001101100000101010100));
+
+    Node largs = d_nm->mkNode(kind::BOUND_VAR_LIST, w);
+    Node lbody = d_nm->mkNode(
+        kind::BITVECTOR_CONCAT, bv::utils::mkExtract(w, 62, 0), zero);
+    Node lambda = d_nm->mkNode(kind::LAMBDA, largs, lbody);
+    Node t = d_nm->mkNode(kind::BITVECTOR_AND,
+                          d_nm->mkNode(kind::APPLY_UF, lambda, one),
+                          d_nm->mkNode(kind::APPLY_UF, lambda, x));
+
+    std::vector<Node> args = {x};
+    std::vector<Node> vals = {c};
+    Evaluator eval;
+    Node r = eval.eval(t, args, vals);
+    TS_ASSERT_EQUALS(r,
+                     Rewriter::rewrite(t.substitute(
+                         args.begin(), args.end(), vals.begin(), vals.end())));
+  }
+};