Head

GCC Code Coverage Report

Directory:	.		Exec	Total	Coverage
File:	test/unit/theory/evaluator_white.cpp	Lines:	68	68	100.0 %
Date:	2021-08-15	Branches:	215	494	43.5 %


/******************************************************************************
 * 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};

  Evaluator eval;
  Node r = eval.eval(t, args, vals);
  ASSERT_EQ(r,
            Rewriter::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};
  Evaluator eval;
  Node r = eval.eval(t, args, vals);
  ASSERT_EQ(r,
            Rewriter::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;
  Evaluator eval;

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

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

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

  {
    Node n = d_nodeManager->mkNode(kind::STRING_INDEXOF, a, a, two);
    Node r = eval.eval(n, args, vals);
    ASSERT_EQ(r, Rewriter::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;
  Evaluator eval;

  // (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	6	(unsigned int)0b0000000100000101001110111001101000101110011101011011110011100111));
52	4	Node c2 = d_nodeManager->mkConst(BitVector(
53		64,
54	6	(unsigned int)0b0000000100000101001110111001101000101110011101011011110011100111));
55
56		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		Evaluator eval;
63	4	Node r = eval.eval(t, args, vals);
64	2	ASSERT_EQ(r,
65		Rewriter::rewrite(t.substitute(
66	2	args.begin(), args.end(), vals.begin(), vals.end())));
67		}
68
69	13	TEST_F(TestTheoryWhiteEvaluator, loop)
70		{
71	4	TypeNode bv64Type = d_nodeManager->mkBitVectorType(64);
72
73	4	Node w = d_nodeManager->mkBoundVar(bv64Type);
74	4	Node x = d_nodeManager->mkVar("x", bv64Type);
75
76	4	Node zero = d_nodeManager->mkConst(BitVector(1, (unsigned int)0));
77	4	Node one = d_nodeManager->mkConst(BitVector(64, (unsigned int)1));
78	4	Node c = d_nodeManager->mkConst(BitVector(
79		64,
80	6	(unsigned int)0b0001111000010111110000110110001101011110111001101100000101010100));
81
82	4	Node largs = d_nodeManager->mkNode(kind::BOUND_VAR_LIST, w);
83		Node lbody = d_nodeManager->mkNode(
84	4	kind::BITVECTOR_CONCAT, bv::utils::mkExtract(w, 62, 0), zero);
85	4	Node lambda = d_nodeManager->mkNode(kind::LAMBDA, largs, lbody);
86		Node t =
87		d_nodeManager->mkNode(kind::BITVECTOR_AND,
88	4	d_nodeManager->mkNode(kind::APPLY_UF, lambda, one),
89	8	d_nodeManager->mkNode(kind::APPLY_UF, lambda, x));
90
91	4	std::vector<Node> args = {x};
92	4	std::vector<Node> vals = {c};
93		Evaluator eval;
94	4	Node r = eval.eval(t, args, vals);
95	2	ASSERT_EQ(r,
96		Rewriter::rewrite(t.substitute(
97	2	args.begin(), args.end(), vals.begin(), vals.end())));
98		}
99
100	13	TEST_F(TestTheoryWhiteEvaluator, strIdOf)
101		{
102	4	Node a = d_nodeManager->mkConst(String("A"));
103	4	Node empty = d_nodeManager->mkConst(String(""));
104	4	Node one = d_nodeManager->mkConst(Rational(1));
105	4	Node two = d_nodeManager->mkConst(Rational(2));
106
107	4	std::vector<Node> args;
108	4	std::vector<Node> vals;
109		Evaluator eval;
110
111		{
112	4	Node n = d_nodeManager->mkNode(kind::STRING_INDEXOF, a, empty, one);
113	4	Node r = eval.eval(n, args, vals);
114	2	ASSERT_EQ(r, Rewriter::rewrite(n));
115		}
116
117		{
118	4	Node n = d_nodeManager->mkNode(kind::STRING_INDEXOF, a, a, one);
119	4	Node r = eval.eval(n, args, vals);
120	2	ASSERT_EQ(r, Rewriter::rewrite(n));
121		}
122
123		{
124	4	Node n = d_nodeManager->mkNode(kind::STRING_INDEXOF, a, empty, two);
125	4	Node r = eval.eval(n, args, vals);
126	2	ASSERT_EQ(r, Rewriter::rewrite(n));
127		}
128
129		{
130	4	Node n = d_nodeManager->mkNode(kind::STRING_INDEXOF, a, a, two);
131	4	Node r = eval.eval(n, args, vals);
132	2	ASSERT_EQ(r, Rewriter::rewrite(n));
133		}
134		}
135
136	13	TEST_F(TestTheoryWhiteEvaluator, code)
137		{
138	4	Node a = d_nodeManager->mkConst(String("A"));
139	4	Node empty = d_nodeManager->mkConst(String(""));
140
141	4	std::vector<Node> args;
142	4	std::vector<Node> vals;
143		Evaluator eval;
144
145		// (str.code "A") ---> 65
146		{
147	4	Node n = d_nodeManager->mkNode(kind::STRING_TO_CODE, a);
148	4	Node r = eval.eval(n, args, vals);
149	2	ASSERT_EQ(r, d_nodeManager->mkConst(Rational(65)));
150		}
151
152		// (str.code "") ---> -1
153		{
154	4	Node n = d_nodeManager->mkNode(kind::STRING_TO_CODE, empty);
155	4	Node r = eval.eval(n, args, vals);
156	2	ASSERT_EQ(r, d_nodeManager->mkConst(Rational(-1)));
157		}
158		}
159		} // namespace test
160	67679	} // namespace cvc5