GCC Code Coverage Report
Directory: . Exec Total Coverage
File: test/unit/theory/theory_engine_white.cpp Lines: 78 79 98.7 %
Date: 2021-03-22 Branches: 198 432 45.8 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file theory_engine_white.cpp
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Aina Niemetz, Morgan Deters, Andres Noetzli
6
 ** This file is part of the CVC4 project.
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.\endverbatim
11
 **
12
 ** \brief White box testing of CVC4::theory::Theory.
13
 **
14
 ** White box testing of CVC4::theory::Theory.  This test creates
15
 ** "fake" theory interfaces and injects them into TheoryEngine, so we
16
 ** can test TheoryEngine's behavior without relying on independent
17
 ** theory behavior.  This is done in TheoryEngineWhite::setUp() by
18
 ** means of the TheoryEngineWhite::registerTheory() interface.
19
 **/
20
21
#include <memory>
22
#include <string>
23
24
#include "base/check.h"
25
#include "context/context.h"
26
#include "expr/kind.h"
27
#include "expr/node.h"
28
#include "options/options.h"
29
#include "test_smt.h"
30
#include "theory/bv/theory_bv_rewrite_rules_normalization.h"
31
#include "theory/bv/theory_bv_rewrite_rules_simplification.h"
32
#include "theory/theory_engine.h"
33
#include "util/integer.h"
34
#include "util/rational.h"
35
36
namespace CVC4 {
37
38
using namespace theory;
39
using namespace expr;
40
using namespace context;
41
using namespace kind;
42
using namespace theory::bv;
43
44
namespace test {
45
46
12
class TestTheoryWhiteEngine : public TestSmt
47
{
48
 protected:
49
6
  void SetUp() override
50
  {
51
6
    TestSmt::SetUp();
52
6
    d_context = d_smtEngine->getContext();
53
6
    d_user_context = d_smtEngine->getUserContext();
54
55
6
    d_theoryEngine = d_smtEngine->getTheoryEngine();
56
84
    for (TheoryId id = THEORY_FIRST; id != THEORY_LAST; ++id)
57
    {
58
78
      delete d_theoryEngine->d_theoryOut[id];
59
78
      delete d_theoryEngine->d_theoryTable[id];
60
78
      d_theoryEngine->d_theoryOut[id] = nullptr;
61
78
      d_theoryEngine->d_theoryTable[id] = nullptr;
62
    }
63
6
    d_theoryEngine->addTheory<DummyTheory<THEORY_BUILTIN> >(THEORY_BUILTIN);
64
6
    d_theoryEngine->addTheory<DummyTheory<THEORY_BOOL> >(THEORY_BOOL);
65
6
    d_theoryEngine->addTheory<DummyTheory<THEORY_UF> >(THEORY_UF);
66
6
    d_theoryEngine->addTheory<DummyTheory<THEORY_ARITH> >(THEORY_ARITH);
67
6
    d_theoryEngine->addTheory<DummyTheory<THEORY_ARRAYS> >(THEORY_ARRAYS);
68
6
    d_theoryEngine->addTheory<DummyTheory<THEORY_BV> >(THEORY_BV);
69
6
  }
70
71
  Context* d_context;
72
  UserContext* d_user_context;
73
  TheoryEngine* d_theoryEngine;
74
};
75
76
12
TEST_F(TestTheoryWhiteEngine, rewriter_simple)
77
{
78
4
  Node x = d_nodeManager->mkVar("x", d_nodeManager->integerType());
79
4
  Node y = d_nodeManager->mkVar("y", d_nodeManager->integerType());
80
4
  Node z = d_nodeManager->mkVar("z", d_nodeManager->integerType());
81
82
  // make the expression (PLUS x y (MULT z 0))
83
4
  Node zero = d_nodeManager->mkConst(Rational("0"));
84
4
  Node zTimesZero = d_nodeManager->mkNode(MULT, z, zero);
85
4
  Node n = d_nodeManager->mkNode(PLUS, x, y, zTimesZero);
86
87
4
  Node nExpected = n;
88
4
  Node nOut;
89
90
  // do a full rewrite; DummyTheory::preRewrite() and DummyTheory::postRewrite()
91
  // assert that the rewrite calls that are made match the expected sequence
92
  // set up above
93
2
  nOut = Rewriter::rewrite(n);
94
95
  // assert that the rewritten node is what we expect
96
2
  ASSERT_EQ(nOut, nExpected);
97
}
98
99
12
TEST_F(TestTheoryWhiteEngine, rewriter_complex)
100
{
101
4
  Node x = d_nodeManager->mkVar("x", d_nodeManager->integerType());
102
4
  Node y = d_nodeManager->mkVar("y", d_nodeManager->realType());
103
4
  TypeNode u = d_nodeManager->mkSort("U");
104
4
  Node z1 = d_nodeManager->mkVar("z1", u);
105
4
  Node z2 = d_nodeManager->mkVar("z2", u);
106
  Node f = d_nodeManager->mkVar(
107
      "f",
108
6
      d_nodeManager->mkFunctionType(d_nodeManager->integerType(),
109
10
                                    d_nodeManager->integerType()));
110
  Node g = d_nodeManager->mkVar(
111
      "g",
112
6
      d_nodeManager->mkFunctionType(d_nodeManager->realType(),
113
10
                                    d_nodeManager->integerType()));
114
4
  Node one = d_nodeManager->mkConst(Rational("1"));
115
4
  Node two = d_nodeManager->mkConst(Rational("2"));
116
117
4
  Node f1 = d_nodeManager->mkNode(APPLY_UF, f, one);
118
4
  Node f2 = d_nodeManager->mkNode(APPLY_UF, f, two);
119
4
  Node fx = d_nodeManager->mkNode(APPLY_UF, f, x);
120
4
  Node ffx = d_nodeManager->mkNode(APPLY_UF, f, fx);
121
4
  Node gy = d_nodeManager->mkNode(APPLY_UF, g, y);
122
4
  Node z1eqz2 = d_nodeManager->mkNode(EQUAL, z1, z2);
123
4
  Node f1eqf2 = d_nodeManager->mkNode(EQUAL, f1, f2);
124
4
  Node ffxeqgy = d_nodeManager->mkNode(EQUAL, ffx, gy);
125
4
  Node and1 = d_nodeManager->mkNode(AND, ffxeqgy, z1eqz2);
126
4
  Node ffxeqf1 = d_nodeManager->mkNode(EQUAL, ffx, f1);
127
4
  Node or1 = d_nodeManager->mkNode(OR, and1, ffxeqf1);
128
  // make the expression:
129
  // (IMPLIES (EQUAL (f 1) (f 2))
130
  //   (OR (AND (EQUAL (f (f x)) (g y))
131
  //            (EQUAL z1 z2))
132
  //       (EQUAL (f (f x)) (f 1))))
133
4
  Node n = d_nodeManager->mkNode(IMPLIES, f1eqf2, or1);
134
4
  Node nExpected = n;
135
4
  Node nOut;
136
137
  // do a full rewrite; DummyTheory::preRewrite() and DummyTheory::postRewrite()
138
  // assert that the rewrite calls that are made match the expected sequence
139
  // set up above
140
2
  nOut = Rewriter::rewrite(n);
141
142
  // assert that the rewritten node is what we expect
143
2
  ASSERT_EQ(nOut, nExpected);
144
}
145
146
12
TEST_F(TestTheoryWhiteEngine, rewrite_rules)
147
{
148
4
  TypeNode t = d_nodeManager->mkBitVectorType(8);
149
4
  Node x = d_nodeManager->mkVar("x", t);
150
4
  Node y = d_nodeManager->mkVar("y", t);
151
4
  Node z = d_nodeManager->mkVar("z", t);
152
153
  // (x - y) * z --> (x * z) - (y * z)
154
  Node expr = d_nodeManager->mkNode(
155
4
      BITVECTOR_MULT, d_nodeManager->mkNode(BITVECTOR_SUB, x, y), z);
156
4
  Node result = expr;
157
2
  if (RewriteRule<MultDistrib>::applies(expr))
158
  {
159
2
    result = RewriteRule<MultDistrib>::apply(expr);
160
  }
161
  Node expected =
162
      d_nodeManager->mkNode(BITVECTOR_SUB,
163
4
                            d_nodeManager->mkNode(BITVECTOR_MULT, x, z),
164
8
                            d_nodeManager->mkNode(BITVECTOR_MULT, y, z));
165
2
  ASSERT_EQ(result, expected);
166
167
  // Try to apply MultSlice to a multiplication of two and three different
168
  // variables, expect different results (x * y and x * y * z should not get
169
  // rewritten to the same term).
170
2
  expr = d_nodeManager->mkNode(BITVECTOR_MULT, x, y, z);
171
2
  result = expr;
172
4
  Node expr2 = d_nodeManager->mkNode(BITVECTOR_MULT, x, y);
173
4
  Node result2 = expr;
174
2
  if (RewriteRule<MultSlice>::applies(expr))
175
  {
176
    result = RewriteRule<MultSlice>::apply(expr);
177
  }
178
2
  if (RewriteRule<MultSlice>::applies(expr2))
179
  {
180
2
    result2 = RewriteRule<MultSlice>::apply(expr2);
181
  }
182
2
  ASSERT_NE(result, result2);
183
}
184
185
}  // namespace test
186
47246
}  // namespace CVC4