Merge pull request #3 from 4tXJ7f/eval

6 files changed, 448 insertions, 1 deletions

diff --git a/src/Makefile.am b/src/Makefile.am
index aa4487c42..9e7762af4 100644
--- a/src/Makefile.am
+++ b/src/Makefile.am
@@ -179,6 +179,8 @@ libcvc4_la_SOURCES = \
 	theory/atom_requests.cpp \
 	theory/atom_requests.h \
 	theory/care_graph.h \
+	theory/evaluator.cpp \
+	theory/evaluator.h \
 	theory/interrupted.h \
 	theory/ite_utilities.cpp \
 	theory/ite_utilities.h \
diff --git a/src/theory/evaluator.cpp b/src/theory/evaluator.cpp
new file mode 100644
index 000000000..1d5b56bd4
--- /dev/null
+++ b/src/theory/evaluator.cpp
@@ -0,0 +1,215 @@
+/*********************                                                        */
+/*! \file evaluator.cpp
+ ** \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
+ ** 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.
+ **/
+
+#include "theory/evaluator.h"
+
+#include "theory/bv/theory_bv_utils.h"
+
+namespace CVC4 {
+namespace theory {
+
+Node Evaluator::eval(TNode n,
+                     const std::vector<Node>& args,
+                     const std::vector<Node>& vals)
+{
+  d_results.clear();
+  d_hasResult = true;
+
+  std::vector<TNode> queue;
+  queue.emplace_back(n);
+
+  while (queue.size() != 0)
+  {
+    TNode currNode = queue.back();
+
+    if (d_results.find(currNode) != d_results.end())
+    {
+      queue.pop_back();
+      continue;
+    }
+
+    bool doEval = true;
+    for (const auto& currNodeChild : currNode)
+    {
+      if (d_results.find(currNodeChild) == d_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 Node::null();
+        }
+
+        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(), d_results[lambdaVal].toNode());
+        }
+
+        currNodeVal = eval(op[1], lambdaArgs, lambdaVals);
+      }
+
+      switch (currNodeVal.getKind())
+      {
+        case kind::CONST_BITVECTOR:
+          d_results[currNode] = Result(currNodeVal.getConst<BitVector>());
+          break;
+
+        case kind::BITVECTOR_NOT:
+          d_results[currNode] = Result(~d_results[currNode[0]].d_bv);
+          break;
+
+        case kind::BITVECTOR_NEG:
+          d_results[currNode] = Result(-d_results[currNode[0]].d_bv);
+          break;
+
+        case kind::BITVECTOR_EXTRACT:
+        {
+          unsigned lo = bv::utils::getExtractLow(currNodeVal);
+          unsigned hi = bv::utils::getExtractHigh(currNodeVal);
+          d_results[currNode] =
+              Result(d_results[currNode[0]].d_bv.extract(hi, lo));
+          break;
+        }
+
+        case kind::BITVECTOR_CONCAT:
+        {
+          BitVector res = d_results[currNode[0]].d_bv;
+          for (size_t i = 1, end = currNode.getNumChildren(); i < end; i++)
+          {
+            res = res.concat(d_results[currNode[i]].d_bv);
+          }
+          d_results[currNode] = Result(res);
+          break;
+        }
+
+        case kind::BITVECTOR_PLUS:
+        {
+          BitVector res = d_results[currNode[0]].d_bv;
+          for (size_t i = 1, end = currNode.getNumChildren(); i < end; i++)
+          {
+            res = res + d_results[currNode[i]].d_bv;
+          }
+          d_results[currNode] = Result(res);
+          break;
+        }
+
+        case kind::BITVECTOR_MULT:
+        {
+          BitVector res = d_results[currNode[0]].d_bv;
+          for (size_t i = 1, end = currNode.getNumChildren(); i < end; i++)
+          {
+            res = res * d_results[currNode[i]].d_bv;
+          }
+          d_results[currNode] = Result(res);
+          break;
+        }
+        case kind::BITVECTOR_AND:
+        {
+          BitVector res = d_results[currNode[0]].d_bv;
+          for (size_t i = 1, end = currNode.getNumChildren(); i < end; i++)
+          {
+            res = res & d_results[currNode[i]].d_bv;
+          }
+          d_results[currNode] = Result(res);
+          break;
+        }
+
+        case kind::BITVECTOR_OR:
+        {
+          BitVector res = d_results[currNode[0]].d_bv;
+          for (size_t i = 1, end = currNode.getNumChildren(); i < end; i++)
+          {
+            res = res | d_results[currNode[i]].d_bv;
+          }
+          d_results[currNode] = Result(res);
+          break;
+        }
+
+        case kind::BITVECTOR_XOR:
+        {
+          BitVector res = d_results[currNode[0]].d_bv;
+          for (size_t i = 1, end = currNode.getNumChildren(); i < end; i++)
+          {
+            res = res ^ d_results[currNode[i]].d_bv;
+          }
+          d_results[currNode] = Result(res);
+          break;
+        }
+
+        case kind::EQUAL:
+        {
+          Result lhs = d_results[currNode[0]];
+          Result rhs = d_results[currNode[1]];
+
+          d_results[currNode] = Result(lhs.d_bv == rhs.d_bv);
+          break;
+        }
+
+        case kind::ITE:
+        {
+          if (d_results[currNode[0]].d_bool)
+          {
+            d_results[currNode] = d_results[currNode[1]];
+          }
+          else
+          {
+            d_results[currNode] = d_results[currNode[2]];
+          }
+          break;
+        }
+
+        default:
+        {
+          Debug("evaluator") << "Kind " << currNodeVal.getKind()
+                             << " not supported" << std::endl;
+          d_results[currNode] = Result();
+        }
+      }
+    }
+  }
+
+  return d_results[n].toNode();
+}
+
+}  // namespace theory
+}  // namespace CVC4
diff --git a/src/theory/evaluator.h b/src/theory/evaluator.h
new file mode 100644
index 000000000..17aeb4381
--- /dev/null
+++ b/src/theory/evaluator.h
@@ -0,0 +1,122 @@
+/*********************                                                        */
+/*! \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
+ ** 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.
+ **/
+
+#include "cvc4_private.h"
+
+#pragma once
+
+#include <utility>
+#include <vector>
+
+#include "expr/node.h"
+#include "util/bitvector.h"
+
+namespace CVC4 {
+namespace theory {
+
+struct Result
+{
+  enum
+  {
+    BITVECTOR,
+    BOOL,
+    INVALID
+  } d_tag;
+  union
+  {
+    bool d_bool;
+    BitVector d_bv;
+  };
+
+  Result(const Result& other)
+  {
+    d_tag = other.d_tag;
+    switch (d_tag)
+    {
+      case BITVECTOR:
+        new (&d_bv) BitVector;
+        d_bv = other.d_bv;
+        break;
+      case BOOL: d_bool = other.d_bool; break;
+      case INVALID: break;
+    }
+  }
+
+  Result() : d_tag(INVALID) {}
+
+  Result(bool b) : d_tag(BOOL), d_bool(b) {}
+
+  Result(const BitVector& bv) : d_tag(BITVECTOR), d_bv(bv) {}
+
+  Result& operator=(const Result& other)
+  {
+    if (this != &other)
+    {
+      d_tag = other.d_tag;
+      switch (d_tag)
+      {
+        case BITVECTOR:
+          new (&d_bv) BitVector;
+          d_bv = other.d_bv;
+          break;
+        case BOOL: d_bool = other.d_bool; break;
+        case INVALID: break;
+      }
+    }
+    return *this;
+  }
+
+  ~Result()
+  {
+    if (d_tag == BITVECTOR)
+    {
+      d_bv.~BitVector();
+    }
+  }
+
+  Node toNode()
+  {
+    NodeManager* nm = NodeManager::currentNM();
+    switch (d_tag)
+    {
+      case Result::BITVECTOR: return nm->mkConst(d_bv);
+      case Result::BOOL: return nm->mkConst(d_bool);
+      default:
+      {
+        Debug("evaluator") << "Missing conversion from " << d_tag << " to node"
+                           << std::endl;
+        return Node();
+      }
+    }
+
+    return Node();
+  }
+};
+
+class Evaluator
+{
+ public:
+  Node eval(TNode n,
+            const std::vector<Node>& args,
+            const std::vector<Node>& vals);
+
+ private:
+  bool d_hasResult;
+  std::unordered_map<TNode, Result, TNodeHashFunction> d_results;
+};
+
+}  // namespace theory
+}  // namespace CVC4
diff --git a/src/theory/quantifiers/sygus/term_database_sygus.cpp b/src/theory/quantifiers/sygus/term_database_sygus.cpp
index 416e9825b..0d09b20d8 100644
--- a/src/theory/quantifiers/sygus/term_database_sygus.cpp
+++ b/src/theory/quantifiers/sygus/term_database_sygus.cpp
@@ -18,6 +18,7 @@
 #include "options/quantifiers_options.h"
 #include "theory/arith/arith_msum.h"
 #include "theory/datatypes/datatypes_rewriter.h"
+#include "theory/evaluator.h"
 #include "theory/quantifiers/quantifiers_attributes.h"
 #include "theory/quantifiers/term_database.h"
 #include "theory/quantifiers/term_util.h"
@@ -1635,7 +1636,24 @@ Node TermDbSygus::evaluateBuiltin( TypeNode tn, Node bn, std::vector< Node >& ar
     std::map< TypeNode, std::vector< Node > >::iterator it = d_var_list.find( tn );
     Assert( it!=d_var_list.end() );
     Assert( it->second.size()==args.size() );
-    return Rewriter::rewrite( bn.substitute( it->second.begin(), it->second.end(), args.begin(), args.end() ) );
+
+    Evaluator eval;
+    Node res = eval.eval(bn, it->second, args);
+    //Node res;
+    if (!res.isNull())
+    {
+      Assert(res
+             == Rewriter::rewrite(bn.substitute(it->second.begin(),
+                                                it->second.end(),
+                                                args.begin(),
+                                                args.end())));
+      return res;
+    }
+    else
+    {
+      return Rewriter::rewrite(bn.substitute(
+          it->second.begin(), it->second.end(), args.begin(), args.end()));
+    }
   }else{
     return Rewriter::rewrite( bn );
   }
diff --git a/test/unit/Makefile.am b/test/unit/Makefile.am
index cc9f6fb1b..a17687101 100644
--- a/test/unit/Makefile.am
+++ b/test/unit/Makefile.am
@@ -11,6 +11,7 @@ UNIT_TESTS += \
 	theory/theory_black \
 	theory/theory_bv_white \
 	theory/theory_engine_white \
+	theory/theory_evaluator_white \
 	theory/theory_quantifiers_bv_instantiator_white \
 	theory/theory_quantifiers_bv_inverter_white \
 	theory/theory_strings_rewriter_white \
diff --git a/test/unit/theory/theory_evaluator_white.h b/test/unit/theory/theory_evaluator_white.h
new file mode 100644
index 000000000..d9acca310
--- /dev/null
+++ b/test/unit/theory/theory_evaluator_white.h
@@ -0,0 +1,89 @@
+/*********************                                                        */
+/*! \file theory_evaluator_white.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
+ ** 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/evaluator.h"
+#include "theory/rewriter.h"
+#include "theory/strings/theory_strings_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 testCheckEntailArithWithAssumption()
+  {
+    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));
+
+    std::vector<Node> args = {w, x, y, z};
+    std::vector<Node> vals = {c1, zero, one, c1};
+
+    Evaluator eval;
+    eval.eval(d_nm->mkNode(kind::ITE, d_nm->mkNode(kind::EQUAL, y, one), x, w),
+              args,
+              vals);
+  }
+};