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