GCC Code Coverage Report
Directory: . Exec Total Coverage
File: test/unit/prop/cnf_stream_white.cpp Lines: 117 129 90.7 %
Date: 2021-03-23 Branches: 205 514 39.9 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file cnf_stream_white.cpp
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Aina Niemetz, Christopher L. Conway, 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::prop::CnfStream.
13
 **
14
 ** White box testing of CVC4::prop::CnfStream.
15
 **/
16
17
#include "base/check.h"
18
#include "context/context.h"
19
#include "prop/cnf_stream.h"
20
#include "prop/prop_engine.h"
21
#include "prop/registrar.h"
22
#include "prop/sat_solver.h"
23
#include "prop/theory_proxy.h"
24
#include "test_smt.h"
25
#include "theory/arith/theory_arith.h"
26
#include "theory/booleans/theory_bool.h"
27
#include "theory/builtin/theory_builtin.h"
28
#include "theory/theory.h"
29
#include "theory/theory_engine.h"
30
31
namespace CVC4 {
32
33
using namespace context;
34
using namespace prop;
35
using namespace smt;
36
using namespace theory;
37
38
namespace test {
39
40
/* This fake class relies on the fact that a MiniSat variable is just an int. */
41
44
class FakeSatSolver : public SatSolver
42
{
43
 public:
44
22
  FakeSatSolver() : d_nextVar(0), d_addClauseCalled(false) {}
45
46
56
  SatVariable newVar(bool theoryAtom, bool preRegister, bool canErase) override
47
  {
48
56
    return d_nextVar++;
49
  }
50
51
2
  SatVariable trueVar() override { return d_nextVar++; }
52
53
2
  SatVariable falseVar() override { return d_nextVar++; }
54
55
64
  ClauseId addClause(SatClause& c, bool lemma) override
56
  {
57
64
    d_addClauseCalled = true;
58
64
    return ClauseIdUndef;
59
  }
60
61
  ClauseId addXorClause(SatClause& clause, bool rhs, bool removable) override
62
  {
63
    d_addClauseCalled = true;
64
    return ClauseIdUndef;
65
  }
66
67
  bool nativeXor() override { return false; }
68
69
2
  void reset() { d_addClauseCalled = false; }
70
71
24
  unsigned int addClauseCalled() { return d_addClauseCalled; }
72
73
  unsigned getAssertionLevel() const override { return 0; }
74
75
  bool isDecision(Node) const { return false; }
76
77
  void unregisterVar(SatLiteral lit) {}
78
79
  void renewVar(SatLiteral lit, int level = -1) {}
80
81
  bool spendResource() { return false; }
82
83
  void interrupt() override {}
84
85
  SatValue solve() override { return SAT_VALUE_UNKNOWN; }
86
87
  SatValue solve(long unsigned int& resource) override
88
  {
89
    return SAT_VALUE_UNKNOWN;
90
  }
91
92
  SatValue value(SatLiteral l) override { return SAT_VALUE_UNKNOWN; }
93
94
  SatValue modelValue(SatLiteral l) override { return SAT_VALUE_UNKNOWN; }
95
96
  bool properExplanation(SatLiteral lit, SatLiteral expl) const { return true; }
97
98
  bool ok() const override { return true; }
99
100
 private:
101
  SatVariable d_nextVar;
102
  bool d_addClauseCalled;
103
};
104
105
44
class TestPropWhiteCnfStream : public TestSmt
106
{
107
 protected:
108
22
  void SetUp() override
109
  {
110
22
    TestSmt::SetUp();
111
22
    d_theoryEngine = d_smtEngine->getTheoryEngine();
112
22
    d_satSolver.reset(new FakeSatSolver());
113
22
    d_cnfContext.reset(new context::Context());
114
22
    d_cnfRegistrar.reset(new prop::NullRegistrar);
115
66
    d_cnfStream.reset(
116
22
        new CVC4::prop::CnfStream(d_satSolver.get(),
117
22
                                  d_cnfRegistrar.get(),
118
22
                                  d_cnfContext.get(),
119
22
                                  &d_smtEngine->getOutputManager(),
120
44
                                  d_smtEngine->getResourceManager()));
121
22
  }
122
123
22
  void TearDown() override
124
  {
125
22
    d_cnfStream.reset(nullptr);
126
22
    d_cnfRegistrar.reset(nullptr);
127
22
    d_cnfContext.reset(nullptr);
128
22
    d_satSolver.reset(nullptr);
129
22
    TestSmt::TearDown();
130
22
  }
131
132
  /** The SAT solver proxy */
133
  std::unique_ptr<FakeSatSolver> d_satSolver;
134
  /** The theory engine */
135
  TheoryEngine* d_theoryEngine;
136
  /** The CNF converter in use */
137
  std::unique_ptr<CnfStream> d_cnfStream;
138
  /** The context of the CnfStream. */
139
  std::unique_ptr<Context> d_cnfContext;
140
  /** The registrar used by the CnfStream. */
141
  std::unique_ptr<prop::NullRegistrar> d_cnfRegistrar;
142
};
143
144
/**
145
 * [chris 5/26/2010] In the tests below, we don't attempt to delve into the
146
 * deep structure of the CNF conversion. Firstly, we just want to make sure
147
 * that the conversion doesn't choke on any boolean Exprs. We'll also check
148
 * that addClause got called. We won't check that it gets called a particular
149
 * number of times, or with what.
150
 */
151
152
20
TEST_F(TestPropWhiteCnfStream, and)
153
{
154
4
  NodeManagerScope nms(d_nodeManager.get());
155
4
  Node a = d_nodeManager->mkVar(d_nodeManager->booleanType());
156
4
  Node b = d_nodeManager->mkVar(d_nodeManager->booleanType());
157
4
  Node c = d_nodeManager->mkVar(d_nodeManager->booleanType());
158
4
  d_cnfStream->convertAndAssert(
159
4
      d_nodeManager->mkNode(kind::AND, a, b, c), false, false);
160
2
  ASSERT_TRUE(d_satSolver->addClauseCalled());
161
}
162
163
20
TEST_F(TestPropWhiteCnfStream, complex_expr)
164
{
165
4
  NodeManagerScope nms(d_nodeManager.get());
166
4
  Node a = d_nodeManager->mkVar(d_nodeManager->booleanType());
167
4
  Node b = d_nodeManager->mkVar(d_nodeManager->booleanType());
168
4
  Node c = d_nodeManager->mkVar(d_nodeManager->booleanType());
169
4
  Node d = d_nodeManager->mkVar(d_nodeManager->booleanType());
170
4
  Node e = d_nodeManager->mkVar(d_nodeManager->booleanType());
171
4
  Node f = d_nodeManager->mkVar(d_nodeManager->booleanType());
172
4
  d_cnfStream->convertAndAssert(
173
10
      d_nodeManager->mkNode(
174
          kind::IMPLIES,
175
4
          d_nodeManager->mkNode(kind::AND, a, b),
176
10
          d_nodeManager->mkNode(
177
              kind::EQUAL,
178
4
              d_nodeManager->mkNode(kind::OR, c, d),
179
6
              d_nodeManager->mkNode(kind::NOT,
180
4
                                    d_nodeManager->mkNode(kind::XOR, e, f)))),
181
      false,
182
      false);
183
2
  ASSERT_TRUE(d_satSolver->addClauseCalled());
184
}
185
186
20
TEST_F(TestPropWhiteCnfStream, true)
187
{
188
4
  NodeManagerScope nms(d_nodeManager.get());
189
2
  d_cnfStream->convertAndAssert(d_nodeManager->mkConst(true), false, false);
190
2
  ASSERT_TRUE(d_satSolver->addClauseCalled());
191
}
192
193
20
TEST_F(TestPropWhiteCnfStream, false)
194
{
195
4
  NodeManagerScope nms(d_nodeManager.get());
196
2
  d_cnfStream->convertAndAssert(d_nodeManager->mkConst(false), false, false);
197
2
  ASSERT_TRUE(d_satSolver->addClauseCalled());
198
}
199
200
20
TEST_F(TestPropWhiteCnfStream, iff)
201
{
202
4
  NodeManagerScope nms(d_nodeManager.get());
203
4
  Node a = d_nodeManager->mkVar(d_nodeManager->booleanType());
204
4
  Node b = d_nodeManager->mkVar(d_nodeManager->booleanType());
205
4
  d_cnfStream->convertAndAssert(
206
4
      d_nodeManager->mkNode(kind::EQUAL, a, b), false, false);
207
2
  ASSERT_TRUE(d_satSolver->addClauseCalled());
208
}
209
210
20
TEST_F(TestPropWhiteCnfStream, implies)
211
{
212
4
  NodeManagerScope nms(d_nodeManager.get());
213
4
  Node a = d_nodeManager->mkVar(d_nodeManager->booleanType());
214
4
  Node b = d_nodeManager->mkVar(d_nodeManager->booleanType());
215
4
  d_cnfStream->convertAndAssert(
216
4
      d_nodeManager->mkNode(kind::IMPLIES, a, b), false, false);
217
2
  ASSERT_TRUE(d_satSolver->addClauseCalled());
218
}
219
220
20
TEST_F(TestPropWhiteCnfStream, not )
221
{
222
4
  NodeManagerScope nms(d_nodeManager.get());
223
4
  Node a = d_nodeManager->mkVar(d_nodeManager->booleanType());
224
4
  d_cnfStream->convertAndAssert(
225
4
      d_nodeManager->mkNode(kind::NOT, a), false, false);
226
2
  ASSERT_TRUE(d_satSolver->addClauseCalled());
227
}
228
229
20
TEST_F(TestPropWhiteCnfStream, or)
230
{
231
4
  NodeManagerScope nms(d_nodeManager.get());
232
4
  Node a = d_nodeManager->mkVar(d_nodeManager->booleanType());
233
4
  Node b = d_nodeManager->mkVar(d_nodeManager->booleanType());
234
4
  Node c = d_nodeManager->mkVar(d_nodeManager->booleanType());
235
4
  d_cnfStream->convertAndAssert(
236
4
      d_nodeManager->mkNode(kind::OR, a, b, c), false, false);
237
2
  ASSERT_TRUE(d_satSolver->addClauseCalled());
238
}
239
240
20
TEST_F(TestPropWhiteCnfStream, var)
241
{
242
4
  NodeManagerScope nms(d_nodeManager.get());
243
4
  Node a = d_nodeManager->mkVar(d_nodeManager->booleanType());
244
4
  Node b = d_nodeManager->mkVar(d_nodeManager->booleanType());
245
2
  d_cnfStream->convertAndAssert(a, false, false);
246
2
  ASSERT_TRUE(d_satSolver->addClauseCalled());
247
2
  d_satSolver->reset();
248
2
  d_cnfStream->convertAndAssert(b, false, false);
249
2
  ASSERT_TRUE(d_satSolver->addClauseCalled());
250
}
251
252
20
TEST_F(TestPropWhiteCnfStream, xor)
253
{
254
4
  NodeManagerScope nms(d_nodeManager.get());
255
4
  Node a = d_nodeManager->mkVar(d_nodeManager->booleanType());
256
4
  Node b = d_nodeManager->mkVar(d_nodeManager->booleanType());
257
4
  d_cnfStream->convertAndAssert(
258
4
      d_nodeManager->mkNode(kind::XOR, a, b), false, false);
259
2
  ASSERT_TRUE(d_satSolver->addClauseCalled());
260
}
261
262
20
TEST_F(TestPropWhiteCnfStream, ensure_literal)
263
{
264
4
  NodeManagerScope nms(d_nodeManager.get());
265
4
  Node a = d_nodeManager->mkVar(d_nodeManager->booleanType());
266
4
  Node b = d_nodeManager->mkVar(d_nodeManager->booleanType());
267
4
  Node a_and_b = d_nodeManager->mkNode(kind::AND, a, b);
268
2
  d_cnfStream->ensureLiteral(a_and_b);
269
  // Clauses are necessary to "literal-ize" a_and_b
270
2
  ASSERT_TRUE(d_satSolver->addClauseCalled());
271
2
  ASSERT_TRUE(d_cnfStream->hasLiteral(a_and_b));
272
}
273
}  // namespace test
274
152822
}  // namespace CVC4