1 |
|
/****************************************************************************** |
2 |
|
* Top contributors (to current version): |
3 |
|
* Andrew Reynolds |
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 |
|
* Unit tests for arithmetic polynomial normalization. |
14 |
|
*/ |
15 |
|
|
16 |
|
#include <iostream> |
17 |
|
#include <memory> |
18 |
|
#include <vector> |
19 |
|
|
20 |
|
#include "expr/node.h" |
21 |
|
#include "expr/node_manager.h" |
22 |
|
#include "test_smt.h" |
23 |
|
#include "theory/arith/arith_poly_norm.h" |
24 |
|
#include "util/rational.h" |
25 |
|
|
26 |
|
namespace cvc5 { |
27 |
|
|
28 |
|
using namespace theory; |
29 |
|
using namespace theory::arith; |
30 |
|
using namespace kind; |
31 |
|
|
32 |
|
namespace test { |
33 |
|
|
34 |
8 |
class TestTheoryWhiteArithPolyNorm : public TestSmt |
35 |
|
{ |
36 |
|
protected: |
37 |
4 |
void SetUp() override { TestSmt::SetUp(); } |
38 |
|
}; |
39 |
|
|
40 |
11 |
TEST_F(TestTheoryWhiteArithPolyNorm, check_poly_norm_int) |
41 |
|
{ |
42 |
4 |
TypeNode intType = d_nodeManager->integerType(); |
43 |
4 |
Node zero = d_nodeManager->mkConst(Rational(0)); |
44 |
4 |
Node one = d_nodeManager->mkConst(Rational(1)); |
45 |
4 |
Node two = d_nodeManager->mkConst(Rational(2)); |
46 |
4 |
Node x = d_nodeManager->mkVar("x", intType); |
47 |
4 |
Node y = d_nodeManager->mkVar("y", intType); |
48 |
4 |
Node z = d_nodeManager->mkVar("z", intType); |
49 |
4 |
Node w = d_nodeManager->mkVar("w", intType); |
50 |
|
|
51 |
4 |
Node t1, t2; |
52 |
|
|
53 |
2 |
t1 = zero; |
54 |
2 |
t2 = one; |
55 |
2 |
ASSERT_FALSE(PolyNorm::isArithPolyNorm(t1, t2)); |
56 |
|
|
57 |
2 |
t1 = d_nodeManager->mkNode(PLUS, x, y); |
58 |
2 |
t2 = d_nodeManager->mkNode(PLUS, y, d_nodeManager->mkNode(MULT, one, x)); |
59 |
2 |
ASSERT_TRUE(PolyNorm::isArithPolyNorm(t1, t2)); |
60 |
|
|
61 |
2 |
t2 = d_nodeManager->mkNode(PLUS, x, x, y); |
62 |
2 |
ASSERT_FALSE(PolyNorm::isArithPolyNorm(t1, t2)); |
63 |
|
|
64 |
2 |
t1 = d_nodeManager->mkNode(PLUS, x, d_nodeManager->mkNode(MULT, y, zero)); |
65 |
2 |
t2 = x; |
66 |
2 |
ASSERT_TRUE(PolyNorm::isArithPolyNorm(t1, t2)); |
67 |
|
|
68 |
2 |
t1 = d_nodeManager->mkNode(MULT, y, d_nodeManager->mkNode(PLUS, one, one)); |
69 |
2 |
t2 = d_nodeManager->mkNode(PLUS, y, y); |
70 |
2 |
ASSERT_TRUE(PolyNorm::isArithPolyNorm(t1, t2)); |
71 |
|
|
72 |
8 |
t1 = d_nodeManager->mkNode(MULT, |
73 |
4 |
d_nodeManager->mkNode(PLUS, one, zero), |
74 |
4 |
d_nodeManager->mkNode(PLUS, x, y)); |
75 |
2 |
t2 = d_nodeManager->mkNode(PLUS, x, y); |
76 |
2 |
ASSERT_TRUE(PolyNorm::isArithPolyNorm(t1, t2)); |
77 |
|
|
78 |
2 |
t1 = d_nodeManager->mkNode(PLUS, {x, y, z, w, y}); |
79 |
2 |
t2 = d_nodeManager->mkNode(PLUS, {w, y, y, z, x}); |
80 |
2 |
ASSERT_TRUE(PolyNorm::isArithPolyNorm(t1, t2)); |
81 |
|
|
82 |
2 |
t1 = d_nodeManager->mkNode(MINUS, t1, t2); |
83 |
2 |
t2 = zero; |
84 |
2 |
ASSERT_TRUE(PolyNorm::isArithPolyNorm(t1, t2)); |
85 |
|
|
86 |
2 |
t1 = d_nodeManager->mkNode(UMINUS, d_nodeManager->mkNode(PLUS, x, y)); |
87 |
2 |
t2 = d_nodeManager->mkNode(MINUS, zero, d_nodeManager->mkNode(PLUS, y, x)); |
88 |
2 |
ASSERT_TRUE(PolyNorm::isArithPolyNorm(t1, t2)); |
89 |
|
|
90 |
2 |
t1 = d_nodeManager->mkNode(MULT, d_nodeManager->mkNode(UMINUS, x), y); |
91 |
2 |
t2 = d_nodeManager->mkNode(MULT, d_nodeManager->mkNode(UMINUS, y), x); |
92 |
2 |
ASSERT_TRUE(PolyNorm::isArithPolyNorm(t1, t2)); |
93 |
|
|
94 |
2 |
t1 = d_nodeManager->mkNode(MULT, x, d_nodeManager->mkNode(PLUS, y, z)); |
95 |
8 |
t2 = d_nodeManager->mkNode(PLUS, |
96 |
4 |
d_nodeManager->mkNode(MULT, x, y), |
97 |
4 |
d_nodeManager->mkNode(MULT, z, x)); |
98 |
2 |
ASSERT_TRUE(PolyNorm::isArithPolyNorm(t1, t2)); |
99 |
|
} |
100 |
|
|
101 |
11 |
TEST_F(TestTheoryWhiteArithPolyNorm, check_poly_norm_real) |
102 |
|
{ |
103 |
4 |
TypeNode realType = d_nodeManager->realType(); |
104 |
4 |
Node zero = d_nodeManager->mkConst(Rational(0)); |
105 |
4 |
Node one = d_nodeManager->mkConst(Rational(1)); |
106 |
4 |
Node half = d_nodeManager->mkConst(Rational(1) / Rational(2)); |
107 |
4 |
Node two = d_nodeManager->mkConst(Rational(2)); |
108 |
4 |
Node x = d_nodeManager->mkVar("x", realType); |
109 |
4 |
Node y = d_nodeManager->mkVar("y", realType); |
110 |
|
|
111 |
4 |
Node t1, t2; |
112 |
|
|
113 |
2 |
t1 = d_nodeManager->mkNode(PLUS, x, y, y); |
114 |
2 |
t2 = d_nodeManager->mkNode(PLUS, y, x, y); |
115 |
2 |
ASSERT_TRUE(PolyNorm::isArithPolyNorm(t1, t2)); |
116 |
|
|
117 |
2 |
t1 = one; |
118 |
2 |
t2 = d_nodeManager->mkNode(MULT, two, half); |
119 |
2 |
ASSERT_TRUE(PolyNorm::isArithPolyNorm(t1, t2)); |
120 |
|
|
121 |
2 |
t1 = d_nodeManager->mkNode(PLUS, y, x); |
122 |
6 |
t2 = d_nodeManager->mkNode( |
123 |
|
MULT, |
124 |
10 |
d_nodeManager->mkNode(PLUS, |
125 |
4 |
d_nodeManager->mkNode(MULT, half, x), |
126 |
4 |
d_nodeManager->mkNode(MULT, half, y)), |
127 |
|
two); |
128 |
2 |
ASSERT_TRUE(PolyNorm::isArithPolyNorm(t1, t2)); |
129 |
|
} |
130 |
|
|
131 |
|
} // namespace test |
132 |
9 |
} // namespace cvc5 |