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