Head

GCC Code Coverage Report

Directory:	.		Exec	Total	Coverage
File:	test/unit/theory/evaluator_white.cpp	Lines:	79	79	100.0 %
Date:	2021-09-29	Branches:	223	510	43.7 %


/******************************************************************************
 * Top contributors (to current version):
 *   Aina Niemetz, Andres Noetzli
 *
 * This file is part of the cvc5 project.
 *
 * Copyright (c) 2009-2021 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.
 * ****************************************************************************
 *
 * [[ Add one-line brief description here ]]
 *
 * [[ Add lengthier description here ]]
 * \todo document this file
 */

#include <vector>

#include "expr/node.h"
#include "test_smt.h"
#include "theory/bv/theory_bv_utils.h"
#include "theory/evaluator.h"
#include "theory/rewriter.h"
#include "util/rational.h"

namespace cvc5 {

using namespace theory;

namespace test {

class TestTheoryWhiteEvaluator : public TestSmt
{
};

TEST_F(TestTheoryWhiteEvaluator, simple)
{
  TypeNode bv64Type = d_nodeManager->mkBitVectorType(64);

  Node w = d_nodeManager->mkVar("w", bv64Type);
  Node x = d_nodeManager->mkVar("x", bv64Type);
  Node y = d_nodeManager->mkVar("y", bv64Type);
  Node z = d_nodeManager->mkVar("z", bv64Type);

  Node zero = d_nodeManager->mkConst(BitVector(64, (unsigned int)0));
  Node one = d_nodeManager->mkConst(BitVector(64, (unsigned int)1));
  Node c1 = d_nodeManager->mkConst(BitVector(
      64,
      (unsigned int)0b0000000100000101001110111001101000101110011101011011110011100111));
  Node c2 = d_nodeManager->mkConst(BitVector(
      64,
      (unsigned int)0b0000000100000101001110111001101000101110011101011011110011100111));

  Node t = d_nodeManager->mkNode(
      kind::ITE, d_nodeManager->mkNode(kind::EQUAL, y, one), x, w);

  std::vector<Node> args = {w, x, y, z};
  std::vector<Node> vals = {c1, zero, one, c1};

  Rewriter* rr = d_smtEngine->getRewriter();
  Evaluator eval(rr);
  Node r = eval.eval(t, args, vals);
  ASSERT_EQ(r,
            rr->rewrite(t.substitute(
                args.begin(), args.end(), vals.begin(), vals.end())));
}

TEST_F(TestTheoryWhiteEvaluator, loop)
{
  TypeNode bv64Type = d_nodeManager->mkBitVectorType(64);

  Node w = d_nodeManager->mkBoundVar(bv64Type);
  Node x = d_nodeManager->mkVar("x", bv64Type);

  Node zero = d_nodeManager->mkConst(BitVector(1, (unsigned int)0));
  Node one = d_nodeManager->mkConst(BitVector(64, (unsigned int)1));
  Node c = d_nodeManager->mkConst(BitVector(
      64,
      (unsigned int)0b0001111000010111110000110110001101011110111001101100000101010100));

  Node largs = d_nodeManager->mkNode(kind::BOUND_VAR_LIST, w);
  Node lbody = d_nodeManager->mkNode(
      kind::BITVECTOR_CONCAT, bv::utils::mkExtract(w, 62, 0), zero);
  Node lambda = d_nodeManager->mkNode(kind::LAMBDA, largs, lbody);
  Node t =
      d_nodeManager->mkNode(kind::BITVECTOR_AND,
                            d_nodeManager->mkNode(kind::APPLY_UF, lambda, one),
                            d_nodeManager->mkNode(kind::APPLY_UF, lambda, x));

  std::vector<Node> args = {x};
  std::vector<Node> vals = {c};
  Rewriter* rr = d_smtEngine->getRewriter();
  Evaluator eval(rr);
  Node r = eval.eval(t, args, vals);
  ASSERT_EQ(r,
            rr->rewrite(t.substitute(
                args.begin(), args.end(), vals.begin(), vals.end())));
}

TEST_F(TestTheoryWhiteEvaluator, strIdOf)
{
  Node a = d_nodeManager->mkConst(String("A"));
  Node empty = d_nodeManager->mkConst(String(""));
  Node one = d_nodeManager->mkConst(Rational(1));
  Node two = d_nodeManager->mkConst(Rational(2));

  std::vector<Node> args;
  std::vector<Node> vals;
  Rewriter* rr = d_smtEngine->getRewriter();
  Evaluator eval(rr);

  {
    Node n = d_nodeManager->mkNode(kind::STRING_INDEXOF, a, empty, one);
    Node r = eval.eval(n, args, vals);
    ASSERT_EQ(r, rr->rewrite(n));
  }

  {
    Node n = d_nodeManager->mkNode(kind::STRING_INDEXOF, a, a, one);
    Node r = eval.eval(n, args, vals);
    ASSERT_EQ(r, rr->rewrite(n));
  }

  {
    Node n = d_nodeManager->mkNode(kind::STRING_INDEXOF, a, empty, two);
    Node r = eval.eval(n, args, vals);
    ASSERT_EQ(r, rr->rewrite(n));
  }

  {
    Node n = d_nodeManager->mkNode(kind::STRING_INDEXOF, a, a, two);
    Node r = eval.eval(n, args, vals);
    ASSERT_EQ(r, rr->rewrite(n));
  }
}

TEST_F(TestTheoryWhiteEvaluator, code)
{
  Node a = d_nodeManager->mkConst(String("A"));
  Node empty = d_nodeManager->mkConst(String(""));

  std::vector<Node> args;
  std::vector<Node> vals;
  Rewriter* rr = d_smtEngine->getRewriter();
  Evaluator eval(rr);

  // (str.code "A") ---> 65
  {
    Node n = d_nodeManager->mkNode(kind::STRING_TO_CODE, a);
    Node r = eval.eval(n, args, vals);
    ASSERT_EQ(r, d_nodeManager->mkConst(Rational(65)));
  }

  // (str.code "") ---> -1
  {
    Node n = d_nodeManager->mkNode(kind::STRING_TO_CODE, empty);
    Node r = eval.eval(n, args, vals);
    ASSERT_EQ(r, d_nodeManager->mkConst(Rational(-1)));
  }
}
}  // namespace test
}  // namespace cvc5


Generated by: GCOVR (Version 3.2)

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