GCC Code Coverage Report
Directory: . Exec Total Coverage
File: test/unit/test_smt.h Lines: 36 65 55.4 %
Date: 2021-03-23 Branches: 30 151 19.9 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file test_smt.h
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Aina Niemetz, Andrew Reynolds, Morgan Deters
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 Common header for unit tests that need an SmtEngine.
13
 **/
14
15
#ifndef CVC4__TEST__UNIT__TEST_SMT_H
16
#define CVC4__TEST__UNIT__TEST_SMT_H
17
18
#include "expr/dtype_cons.h"
19
#include "expr/node.h"
20
#include "expr/node_manager.h"
21
#include "smt/smt_engine.h"
22
#include "smt/smt_engine_scope.h"
23
#include "test.h"
24
#include "theory/output_channel.h"
25
#include "theory/rewriter.h"
26
#include "theory/theory.h"
27
#include "theory/theory_state.h"
28
#include "theory/valuation.h"
29
#include "util/resource_manager.h"
30
#include "util/unsafe_interrupt_exception.h"
31
32
namespace CVC4 {
33
namespace test {
34
35
/* -------------------------------------------------------------------------- */
36
/* Test fixtures.                                                             */
37
/* -------------------------------------------------------------------------- */
38
39
584
class TestSmt : public TestInternal
40
{
41
 protected:
42
292
  void SetUp() override
43
  {
44
292
    d_nodeManager.reset(new NodeManager());
45
292
    d_nmScope.reset(new NodeManagerScope(d_nodeManager.get()));
46
292
    d_smtEngine.reset(new SmtEngine(d_nodeManager.get()));
47
292
    d_smtEngine->finishInit();
48
292
  }
49
50
  std::unique_ptr<NodeManagerScope> d_nmScope;
51
  std::unique_ptr<NodeManager> d_nodeManager;
52
  std::unique_ptr<SmtEngine> d_smtEngine;
53
};
54
55
1064
class TestSmtNoFinishInit : public TestInternal
56
{
57
 protected:
58
532
  void SetUp() override
59
  {
60
532
    d_nodeManager.reset(new NodeManager());
61
532
    d_nmScope.reset(new NodeManagerScope(d_nodeManager.get()));
62
532
    d_smtEngine.reset(new SmtEngine(d_nodeManager.get()));
63
532
  }
64
65
  std::unique_ptr<NodeManagerScope> d_nmScope;
66
  std::unique_ptr<NodeManager> d_nodeManager;
67
  std::unique_ptr<SmtEngine> d_smtEngine;
68
};
69
70
/* -------------------------------------------------------------------------- */
71
/* Helpers.                                                                   */
72
/* -------------------------------------------------------------------------- */
73
74
/**
75
 * Very basic OutputChannel for testing simple Theory Behaviour.
76
 * Stores a call sequence for the output channel
77
 */
78
enum OutputChannelCallType
79
{
80
  CONFLICT,
81
  PROPAGATE,
82
  PROPAGATE_AS_DECISION,
83
  AUG_LEMMA,
84
  LEMMA,
85
  EXPLANATION
86
};
87
88
inline std::ostream& operator<<(std::ostream& out, OutputChannelCallType type)
89
{
90
  switch (type)
91
  {
92
    case CONFLICT: return out << "CONFLICT";
93
    case PROPAGATE: return out << "PROPAGATE";
94
    case PROPAGATE_AS_DECISION: return out << "PROPAGATE_AS_DECISION";
95
    case AUG_LEMMA: return out << "AUG_LEMMA";
96
    case LEMMA: return out << "LEMMA";
97
    case EXPLANATION: return out << "EXPLANATION";
98
    default: return out << "UNDEFINED-OutputChannelCallType!" << int(type);
99
  }
100
}
101
102
class DummyOutputChannel : public CVC4::theory::OutputChannel
103
{
104
 public:
105
6
  DummyOutputChannel() {}
106
6
  ~DummyOutputChannel() override {}
107
108
  void safePoint(ResourceManager::Resource r) override {}
109
  void conflict(TNode n) override { push(CONFLICT, n); }
110
111
  void trustedConflict(theory::TrustNode n) override
112
  {
113
    push(CONFLICT, n.getNode());
114
  }
115
116
  bool propagate(TNode n) override
117
  {
118
    push(PROPAGATE, n);
119
    return true;
120
  }
121
122
2
  void lemma(TNode n,
123
             theory::LemmaProperty p = theory::LemmaProperty::NONE) override
124
  {
125
2
    push(LEMMA, n);
126
2
  }
127
128
  void trustedLemma(theory::TrustNode n, theory::LemmaProperty p) override
129
  {
130
    push(LEMMA, n.getNode());
131
  }
132
133
  void requirePhase(TNode, bool) override {}
134
  void setIncomplete() override {}
135
  void handleUserAttribute(const char* attr, theory::Theory* t) override {}
136
137
2
  void splitLemma(TNode n, bool removable = false) override { push(LEMMA, n); }
138
139
6
  void clear() { d_callHistory.clear(); }
140
141
  Node getIthNode(int i) const
142
  {
143
    Node tmp = (d_callHistory[i]).second;
144
    return tmp;
145
  }
146
147
  OutputChannelCallType getIthCallType(int i) const
148
  {
149
    return (d_callHistory[i]).first;
150
  }
151
152
  unsigned getNumCalls() const { return d_callHistory.size(); }
153
154
  void printIth(std::ostream& os, int i) const
155
  {
156
    os << "[DummyOutputChannel " << i;
157
    os << " " << getIthCallType(i);
158
    os << " " << getIthNode(i) << "]";
159
  }
160
161
 private:
162
4
  void push(OutputChannelCallType call, TNode n)
163
  {
164
4
    d_callHistory.push_back(std::make_pair(call, n));
165
4
  }
166
167
  std::vector<std::pair<enum OutputChannelCallType, Node> > d_callHistory;
168
};
169
170
/* -------------------------------------------------------------------------- */
171
172
84
class DymmyTheoryRewriter : public theory::TheoryRewriter
173
{
174
 public:
175
48
  theory::RewriteResponse preRewrite(TNode n) override
176
  {
177
48
    return theory::RewriteResponse(theory::REWRITE_DONE, n);
178
  }
179
180
96
  theory::RewriteResponse postRewrite(TNode n) override
181
  {
182
96
    return theory::RewriteResponse(theory::REWRITE_DONE, n);
183
  }
184
};
185
186
/** Dummy Theory interface.  */
187
template <theory::TheoryId theoryId>
188
84
class DummyTheory : public theory::Theory
189
{
190
 public:
191
42
  DummyTheory(context::Context* ctxt,
192
              context::UserContext* uctxt,
193
              theory::OutputChannel& out,
194
              theory::Valuation valuation,
195
              const LogicInfo& logicInfo,
196
              ProofNodeManager* pnm)
197
      : Theory(theoryId, ctxt, uctxt, out, valuation, logicInfo, pnm),
198
42
        d_state(ctxt, uctxt, valuation)
199
  {
200
    // use a default theory state object
201
42
    d_theoryState = &d_state;
202
42
  }
203
204
36
  theory::TheoryRewriter* getTheoryRewriter() override { return &d_rewriter; }
205
206
  void registerTerm(TNode n)
207
  {
208
    // check that we registerTerm() a term only once
209
    ASSERT_TRUE(d_registered.find(n) == d_registered.end());
210
211
    for (TNode::iterator i = n.begin(); i != n.end(); ++i)
212
    {
213
      // check that registerTerm() is called in reverse topological order
214
      ASSERT_TRUE(d_registered.find(*i) != d_registered.end());
215
    }
216
217
    d_registered.insert(n);
218
  }
219
220
  void presolve() override { Unimplemented(); }
221
  void preRegisterTerm(TNode n) override { Unimplemented(); }
222
  void propagate(Effort level) override { Unimplemented(); }
223
4
  bool preNotifyFact(
224
      TNode atom, bool pol, TNode fact, bool isPrereg, bool isInternal) override
225
  {
226
    // do not assert to equality engine, since this theory does not use one
227
4
    return true;
228
  }
229
  theory::TrustNode explain(TNode n) override
230
  {
231
    return theory::TrustNode::null();
232
  }
233
  Node getValue(TNode n) { return Node::null(); }
234
  std::string identify() const override { return "DummyTheory" + d_id; }
235
236
  std::set<Node> d_registered;
237
238
 private:
239
  /** Default theory state object */
240
  theory::TheoryState d_state;
241
  /**
242
   * This fake theory class is equally useful for bool, uf, arith, etc.  It
243
   * keeps an identifier to identify itself.
244
   */
245
  std::string d_id;
246
  /** The theory rewriter for this theory. */
247
  DymmyTheoryRewriter d_rewriter;
248
};
249
250
/* -------------------------------------------------------------------------- */
251
}  // namespace test
252
}  // namespace CVC4
253
#endif