test/unit/theory/evaluator_white.cpp

   1 /*********************                                                        */
   2 /*! \file evaluator_white.cpp
   3  ** \verbatim
   4  ** Top contributors (to current version):
   5  **   Aina Niemetz, Andres Noetzli
   6  ** This file is part of the CVC4 project.
   7  ** Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
   8  ** in the top-level source directory and their institutional affiliations.
   9  ** All rights reserved.  See the file COPYING in the top-level source
  10  ** directory for licensing information.\endverbatim
  11  **
  12  ** \brief [[ Add one-line brief description here ]]
  13  **
  14  ** [[ Add lengthier description here ]]
  15  ** \todo document this file
  16  **/
  17
  18 #include <vector>
  19
  20 #include "expr/node.h"
  21 #include "test_smt.h"
  22 #include "theory/bv/theory_bv_utils.h"
  23 #include "theory/evaluator.h"
  24 #include "theory/rewriter.h"
  25 #include "util/rational.h"
  26
  27 namespace CVC5 {
  28
  29 using namespace theory;
  30
  31 namespace test {
  32
  33 class TestTheoryWhiteEvaluator : public TestSmt
  34 {
  35 };
  36
  37 TEST_F(TestTheoryWhiteEvaluator, simple)
  38 {
  39   TypeNode bv64Type = d_nodeManager->mkBitVectorType(64);
  40
  41   Node w = d_nodeManager->mkVar("w", bv64Type);
  42   Node x = d_nodeManager->mkVar("x", bv64Type);
  43   Node y = d_nodeManager->mkVar("y", bv64Type);
  44   Node z = d_nodeManager->mkVar("z", bv64Type);
  45
  46   Node zero = d_nodeManager->mkConst(BitVector(64, (unsigned int)0));
  47   Node one = d_nodeManager->mkConst(BitVector(64, (unsigned int)1));
  48   Node c1 = d_nodeManager->mkConst(BitVector(
  49       64,
  50       (unsigned int)0b0000000100000101001110111001101000101110011101011011110011100111));
  51   Node c2 = d_nodeManager->mkConst(BitVector(
  52       64,
  53       (unsigned int)0b0000000100000101001110111001101000101110011101011011110011100111));
  54
  55   Node t = d_nodeManager->mkNode(
  56       kind::ITE, d_nodeManager->mkNode(kind::EQUAL, y, one), x, w);
  57
  58   std::vector<Node> args = {w, x, y, z};
  59   std::vector<Node> vals = {c1, zero, one, c1};
  60
  61   Evaluator eval;
  62   Node r = eval.eval(t, args, vals);
  63   ASSERT_EQ(r,
  64             Rewriter::rewrite(t.substitute(
  65                 args.begin(), args.end(), vals.begin(), vals.end())));
  66 }
  67
  68 TEST_F(TestTheoryWhiteEvaluator, loop)
  69 {
  70   TypeNode bv64Type = d_nodeManager->mkBitVectorType(64);
  71
  72   Node w = d_nodeManager->mkBoundVar(bv64Type);
  73   Node x = d_nodeManager->mkVar("x", bv64Type);
  74
  75   Node zero = d_nodeManager->mkConst(BitVector(1, (unsigned int)0));
  76   Node one = d_nodeManager->mkConst(BitVector(64, (unsigned int)1));
  77   Node c = d_nodeManager->mkConst(BitVector(
  78       64,
  79       (unsigned int)0b0001111000010111110000110110001101011110111001101100000101010100));
  80
  81   Node largs = d_nodeManager->mkNode(kind::BOUND_VAR_LIST, w);
  82   Node lbody = d_nodeManager->mkNode(
  83       kind::BITVECTOR_CONCAT, bv::utils::mkExtract(w, 62, 0), zero);
  84   Node lambda = d_nodeManager->mkNode(kind::LAMBDA, largs, lbody);
  85   Node t =
  86       d_nodeManager->mkNode(kind::BITVECTOR_AND,
  87                             d_nodeManager->mkNode(kind::APPLY_UF, lambda, one),
  88                             d_nodeManager->mkNode(kind::APPLY_UF, lambda, x));
  89
  90   std::vector<Node> args = {x};
  91   std::vector<Node> vals = {c};
  92   Evaluator eval;
  93   Node r = eval.eval(t, args, vals);
  94   ASSERT_EQ(r,
  95             Rewriter::rewrite(t.substitute(
  96                 args.begin(), args.end(), vals.begin(), vals.end())));
  97 }
  98
  99 TEST_F(TestTheoryWhiteEvaluator, strIdOf)
 100 {
 101   Node a = d_nodeManager->mkConst(String("A"));
 102   Node empty = d_nodeManager->mkConst(String(""));
 103   Node one = d_nodeManager->mkConst(Rational(1));
 104   Node two = d_nodeManager->mkConst(Rational(2));
 105
 106   std::vector<Node> args;
 107   std::vector<Node> vals;
 108   Evaluator eval;
 109
 110   {
 111     Node n = d_nodeManager->mkNode(kind::STRING_STRIDOF, a, empty, one);
 112     Node r = eval.eval(n, args, vals);
 113     ASSERT_EQ(r, Rewriter::rewrite(n));
 114   }
 115
 116   {
 117     Node n = d_nodeManager->mkNode(kind::STRING_STRIDOF, a, a, one);
 118     Node r = eval.eval(n, args, vals);
 119     ASSERT_EQ(r, Rewriter::rewrite(n));
 120   }
 121
 122   {
 123     Node n = d_nodeManager->mkNode(kind::STRING_STRIDOF, a, empty, two);
 124     Node r = eval.eval(n, args, vals);
 125     ASSERT_EQ(r, Rewriter::rewrite(n));
 126   }
 127
 128   {
 129     Node n = d_nodeManager->mkNode(kind::STRING_STRIDOF, a, a, two);
 130     Node r = eval.eval(n, args, vals);
 131     ASSERT_EQ(r, Rewriter::rewrite(n));
 132   }
 133 }
 134
 135 TEST_F(TestTheoryWhiteEvaluator, code)
 136 {
 137   Node a = d_nodeManager->mkConst(String("A"));
 138   Node empty = d_nodeManager->mkConst(String(""));
 139
 140   std::vector<Node> args;
 141   std::vector<Node> vals;
 142   Evaluator eval;
 143
 144   // (str.code "A") ---> 65
 145   {
 146     Node n = d_nodeManager->mkNode(kind::STRING_TO_CODE, a);
 147     Node r = eval.eval(n, args, vals);
 148     ASSERT_EQ(r, d_nodeManager->mkConst(Rational(65)));
 149   }
 150
 151   // (str.code "") ---> -1
 152   {
 153     Node n = d_nodeManager->mkNode(kind::STRING_TO_CODE, empty);
 154     Node r = eval.eval(n, args, vals);
 155     ASSERT_EQ(r, d_nodeManager->mkConst(Rational(-1)));
 156   }
 157 }
 158 }  // namespace test
 159 }  // namespace CVC5