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