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