1 /********************* */
2 /*! \file theory.cpp
3 ** \verbatim
4 ** Top contributors (to current version):
5 ** Tim King, Dejan Jovanovic, Andrew Reynolds
6 ** This file is part of the CVC4 project.
7 ** Copyright (c) 2009-2019 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 Base for theory interface.
13 **
14 ** Base for theory interface.
15 **/
16
17 #include "theory/theory.h"
18
19 #include <vector>
20 #include <sstream>
21 #include <iostream>
22 #include <string>
23
24 #include "base/cvc4_assert.h"
25 #include "expr/node_algorithm.h"
26 #include "smt/smt_statistics_registry.h"
27 #include "theory/ext_theory.h"
28 #include "theory/quantifiers_engine.h"
29 #include "theory/substitutions.h"
30
31 using namespace std;
32
33 namespace CVC4 {
34 namespace theory {
35
36 /** Default value for the uninterpreted sorts is the UF theory */
37 TheoryId Theory::s_uninterpretedSortOwner = THEORY_UF;
38
operator <<(std::ostream & os,Theory::Effort level)39 std::ostream& operator<<(std::ostream& os, Theory::Effort level){
40 switch(level){
41 case Theory::EFFORT_STANDARD:
42 os << "EFFORT_STANDARD"; break;
43 case Theory::EFFORT_FULL:
44 os << "EFFORT_FULL"; break;
45 case Theory::EFFORT_COMBINATION:
46 os << "EFFORT_COMBINATION"; break;
47 case Theory::EFFORT_LAST_CALL:
48 os << "EFFORT_LAST_CALL"; break;
49 default:
50 Unreachable();
51 }
52 return os;
53 }/* ostream& operator<<(ostream&, Theory::Effort) */
54
Theory(TheoryId id,context::Context * satContext,context::UserContext * userContext,OutputChannel & out,Valuation valuation,const LogicInfo & logicInfo,std::string name)55 Theory::Theory(TheoryId id,
56 context::Context* satContext,
57 context::UserContext* userContext,
58 OutputChannel& out,
59 Valuation valuation,
60 const LogicInfo& logicInfo,
61 std::string name)
62 : d_id(id),
63 d_instanceName(name),
64 d_satContext(satContext),
65 d_userContext(userContext),
66 d_logicInfo(logicInfo),
67 d_facts(satContext),
68 d_factsHead(satContext, 0),
69 d_sharedTermsIndex(satContext, 0),
70 d_careGraph(NULL),
71 d_quantEngine(NULL),
72 d_decManager(nullptr),
73 d_extTheory(NULL),
74 d_checkTime(getStatsPrefix(id) + name + "::checkTime"),
75 d_computeCareGraphTime(getStatsPrefix(id) + name
76 + "::computeCareGraphTime"),
77 d_sharedTerms(satContext),
78 d_out(&out),
79 d_valuation(valuation),
80 d_proofsEnabled(false)
81 {
82 smtStatisticsRegistry()->registerStat(&d_checkTime);
83 smtStatisticsRegistry()->registerStat(&d_computeCareGraphTime);
84 }
85
~Theory()86 Theory::~Theory() {
87 smtStatisticsRegistry()->unregisterStat(&d_checkTime);
88 smtStatisticsRegistry()->unregisterStat(&d_computeCareGraphTime);
89
90 delete d_extTheory;
91 }
92
theoryOf(TheoryOfMode mode,TNode node)93 TheoryId Theory::theoryOf(TheoryOfMode mode, TNode node) {
94 TheoryId tid = THEORY_BUILTIN;
95 switch(mode) {
96 case THEORY_OF_TYPE_BASED:
97 // Constants, variables, 0-ary constructors
98 if (node.isVar()) {
99 if( node.getKind() == kind::BOOLEAN_TERM_VARIABLE ){
100 tid = THEORY_UF;
101 }else{
102 tid = Theory::theoryOf(node.getType());
103 }
104 }else if (node.isConst()) {
105 tid = Theory::theoryOf(node.getType());
106 } else if (node.getKind() == kind::EQUAL) {
107 // Equality is owned by the theory that owns the domain
108 tid = Theory::theoryOf(node[0].getType());
109 } else {
110 // Regular nodes are owned by the kind
111 tid = kindToTheoryId(node.getKind());
112 }
113 break;
114 case THEORY_OF_TERM_BASED:
115 // Variables
116 if (node.isVar()) {
117 if (Theory::theoryOf(node.getType()) != theory::THEORY_BOOL) {
118 // We treat the variables as uninterpreted
119 tid = s_uninterpretedSortOwner;
120 } else {
121 if( node.getKind() == kind::BOOLEAN_TERM_VARIABLE ){
122 //Boolean vars go to UF
123 tid = THEORY_UF;
124 }else{
125 // Except for the Boolean ones
126 tid = THEORY_BOOL;
127 }
128 }
129 } else if (node.isConst()) {
130 // Constants go to the theory of the type
131 tid = Theory::theoryOf(node.getType());
132 } else if (node.getKind() == kind::EQUAL) { // Equality
133 // If one of them is an ITE, it's irelevant, since they will get replaced out anyhow
134 if (node[0].getKind() == kind::ITE) {
135 tid = Theory::theoryOf(node[0].getType());
136 } else if (node[1].getKind() == kind::ITE) {
137 tid = Theory::theoryOf(node[1].getType());
138 } else {
139 TNode l = node[0];
140 TNode r = node[1];
141 TypeNode ltype = l.getType();
142 TypeNode rtype = r.getType();
143 if( ltype != rtype ){
144 tid = Theory::theoryOf(l.getType());
145 }else {
146 // If both sides belong to the same theory the choice is easy
147 TheoryId T1 = Theory::theoryOf(l);
148 TheoryId T2 = Theory::theoryOf(r);
149 if (T1 == T2) {
150 tid = T1;
151 } else {
152 TheoryId T3 = Theory::theoryOf(ltype);
153 // This is a case of
154 // * x*y = f(z) -> UF
155 // * x = c -> UF
156 // * f(x) = read(a, y) -> either UF or ARRAY
157 // at least one of the theories has to be parametric, i.e. theory of the type is different
158 // from the theory of the term
159 if (T1 == T3) {
160 tid = T2;
161 } else if (T2 == T3) {
162 tid = T1;
163 } else {
164 // If both are parametric, we take the smaller one (arbitrary)
165 tid = T1 < T2 ? T1 : T2;
166 }
167 }
168 }
169 }
170 } else {
171 // Regular nodes are owned by the kind
172 tid = kindToTheoryId(node.getKind());
173 }
174 break;
175 default:
176 Unreachable();
177 }
178 Trace("theory::internal") << "theoryOf(" << mode << ", " << node << ") -> " << tid << std::endl;
179 return tid;
180 }
181
addSharedTermInternal(TNode n)182 void Theory::addSharedTermInternal(TNode n) {
183 Debug("sharing") << "Theory::addSharedTerm<" << getId() << ">(" << n << ")" << endl;
184 Debug("theory::assertions") << "Theory::addSharedTerm<" << getId() << ">(" << n << ")" << endl;
185 d_sharedTerms.push_back(n);
186 addSharedTerm(n);
187 }
188
computeCareGraph()189 void Theory::computeCareGraph() {
190 Debug("sharing") << "Theory::computeCareGraph<" << getId() << ">()" << endl;
191 for (unsigned i = 0; i < d_sharedTerms.size(); ++ i) {
192 TNode a = d_sharedTerms[i];
193 TypeNode aType = a.getType();
194 for (unsigned j = i + 1; j < d_sharedTerms.size(); ++ j) {
195 TNode b = d_sharedTerms[j];
196 if (b.getType() != aType) {
197 // We don't care about the terms of different types
198 continue;
199 }
200 switch (d_valuation.getEqualityStatus(a, b)) {
201 case EQUALITY_TRUE_AND_PROPAGATED:
202 case EQUALITY_FALSE_AND_PROPAGATED:
203 // If we know about it, we should have propagated it, so we can skip
204 break;
205 default:
206 // Let's split on it
207 addCarePair(a, b);
208 break;
209 }
210 }
211 }
212 }
213
printFacts(std::ostream & os) const214 void Theory::printFacts(std::ostream& os) const {
215 unsigned i, n = d_facts.size();
216 for(i = 0; i < n; i++){
217 const Assertion& a_i = d_facts[i];
218 Node assertion = a_i;
219 os << d_id << '[' << i << ']' << " " << assertion << endl;
220 }
221 }
222
debugPrintFacts() const223 void Theory::debugPrintFacts() const{
224 DebugChannel.getStream() << "Theory::debugPrintFacts()" << endl;
225 printFacts(DebugChannel.getStream());
226 }
227
currentlySharedTerms() const228 std::unordered_set<TNode, TNodeHashFunction> Theory::currentlySharedTerms() const{
229 std::unordered_set<TNode, TNodeHashFunction> currentlyShared;
230 for (shared_terms_iterator i = shared_terms_begin(),
231 i_end = shared_terms_end(); i != i_end; ++i) {
232 currentlyShared.insert (*i);
233 }
234 return currentlyShared;
235 }
236
collectTerms(TNode n,set<Kind> & irrKinds,set<Node> & termSet) const237 void Theory::collectTerms(TNode n,
238 set<Kind>& irrKinds,
239 set<Node>& termSet) const
240 {
241 if (termSet.find(n) != termSet.end()) {
242 return;
243 }
244 Kind nk = n.getKind();
245 if (irrKinds.find(nk) == irrKinds.end())
246 {
247 Trace("theory::collectTerms")
248 << "Theory::collectTerms: adding " << n << endl;
249 termSet.insert(n);
250 }
251 if (nk == kind::NOT || nk == kind::EQUAL || !isLeaf(n))
252 {
253 for(TNode::iterator child_it = n.begin(); child_it != n.end(); ++child_it) {
254 collectTerms(*child_it, irrKinds, termSet);
255 }
256 }
257 }
258
259
computeRelevantTerms(set<Node> & termSet,bool includeShared) const260 void Theory::computeRelevantTerms(set<Node>& termSet, bool includeShared) const
261 {
262 set<Kind> irrKinds;
263 computeRelevantTerms(termSet, irrKinds, includeShared);
264 }
265
computeRelevantTerms(set<Node> & termSet,set<Kind> & irrKinds,bool includeShared) const266 void Theory::computeRelevantTerms(set<Node>& termSet,
267 set<Kind>& irrKinds,
268 bool includeShared) const
269 {
270 // Collect all terms appearing in assertions
271 irrKinds.insert(kind::EQUAL);
272 irrKinds.insert(kind::NOT);
273 context::CDList<Assertion>::const_iterator assert_it = facts_begin(), assert_it_end = facts_end();
274 for (; assert_it != assert_it_end; ++assert_it) {
275 collectTerms(*assert_it, irrKinds, termSet);
276 }
277
278 if (!includeShared) return;
279
280 // Add terms that are shared terms
281 set<Kind> kempty;
282 context::CDList<TNode>::const_iterator shared_it = shared_terms_begin(), shared_it_end = shared_terms_end();
283 for (; shared_it != shared_it_end; ++shared_it) {
284 collectTerms(*shared_it, kempty, termSet);
285 }
286 }
287
ppAssert(TNode in,SubstitutionMap & outSubstitutions)288 Theory::PPAssertStatus Theory::ppAssert(TNode in,
289 SubstitutionMap& outSubstitutions)
290 {
291 if (in.getKind() == kind::EQUAL)
292 {
293 // (and (= x t) phi) can be replaced by phi[x/t] if
294 // 1) x is a variable
295 // 2) x is not in the term t
296 // 3) x : T and t : S, then S <: T
297 if (in[0].isVar() && !expr::hasSubterm(in[1], in[0])
298 && (in[1].getType()).isSubtypeOf(in[0].getType()))
299 {
300 outSubstitutions.addSubstitution(in[0], in[1]);
301 return PP_ASSERT_STATUS_SOLVED;
302 }
303 if (in[1].isVar() && !expr::hasSubterm(in[0], in[1])
304 && (in[0].getType()).isSubtypeOf(in[1].getType()))
305 {
306 outSubstitutions.addSubstitution(in[1], in[0]);
307 return PP_ASSERT_STATUS_SOLVED;
308 }
309 if (in[0].isConst() && in[1].isConst())
310 {
311 if (in[0] != in[1])
312 {
313 return PP_ASSERT_STATUS_CONFLICT;
314 }
315 }
316 }
317
318 return PP_ASSERT_STATUS_UNSOLVED;
319 }
320
entailmentCheck(TNode lit,const EntailmentCheckParameters * params,EntailmentCheckSideEffects * out)321 std::pair<bool, Node> Theory::entailmentCheck(
322 TNode lit,
323 const EntailmentCheckParameters* params,
324 EntailmentCheckSideEffects* out) {
325 return make_pair(false, Node::null());
326 }
327
getExtTheory()328 ExtTheory* Theory::getExtTheory() {
329 Assert(d_extTheory != NULL);
330 return d_extTheory;
331 }
332
addCarePair(TNode t1,TNode t2)333 void Theory::addCarePair(TNode t1, TNode t2) {
334 if (d_careGraph) {
335 d_careGraph->insert(CarePair(t1, t2, d_id));
336 }
337 }
338
getCareGraph(CareGraph * careGraph)339 void Theory::getCareGraph(CareGraph* careGraph) {
340 Assert(careGraph != NULL);
341
342 Trace("sharing") << "Theory<" << getId() << ">::getCareGraph()" << std::endl;
343 TimerStat::CodeTimer computeCareGraphTime(d_computeCareGraphTime);
344 d_careGraph = careGraph;
345 computeCareGraph();
346 d_careGraph = NULL;
347 }
348
setQuantifiersEngine(QuantifiersEngine * qe)349 void Theory::setQuantifiersEngine(QuantifiersEngine* qe) {
350 Assert(d_quantEngine == NULL);
351 Assert(qe != NULL);
352 d_quantEngine = qe;
353 }
354
setDecisionManager(DecisionManager * dm)355 void Theory::setDecisionManager(DecisionManager* dm)
356 {
357 Assert(d_decManager == nullptr);
358 Assert(dm != nullptr);
359 d_decManager = dm;
360 }
361
setupExtTheory()362 void Theory::setupExtTheory() {
363 Assert(d_extTheory == NULL);
364 d_extTheory = new ExtTheory(this);
365 }
366
367
EntailmentCheckParameters(TheoryId tid)368 EntailmentCheckParameters::EntailmentCheckParameters(TheoryId tid)
369 : d_tid(tid) {
370 }
371
~EntailmentCheckParameters()372 EntailmentCheckParameters::~EntailmentCheckParameters(){}
373
getTheoryId() const374 TheoryId EntailmentCheckParameters::getTheoryId() const {
375 return d_tid;
376 }
377
EntailmentCheckSideEffects(TheoryId tid)378 EntailmentCheckSideEffects::EntailmentCheckSideEffects(TheoryId tid)
379 : d_tid(tid)
380 {}
381
getTheoryId() const382 TheoryId EntailmentCheckSideEffects::getTheoryId() const {
383 return d_tid;
384 }
385
~EntailmentCheckSideEffects()386 EntailmentCheckSideEffects::~EntailmentCheckSideEffects() {
387 }
388
389 }/* CVC4::theory namespace */
390 }/* CVC4 namespace */
391