1 /********************* */
4 ** Original author: Morgan Deters
5 ** Major contributors: Clark Barrett, Dejan Jovanovic
6 ** Minor contributors (to current version): Andrew Reynolds, Tim King
7 ** This file is part of the CVC4 project.
8 ** Copyright (c) 2009-2013 New York University and The University of Iowa
9 ** See the file COPYING in the top-level source directory for licensing
10 ** information.\endverbatim
12 ** \brief Base for theory interface.
14 ** Base for theory interface.
17 #include "theory/theory.h"
18 #include "util/cvc4_assert.h"
19 #include "theory/quantifiers_engine.h"
20 #include "theory/substitutions.h"
29 /** Default value for the uninterpreted sorts is the UF theory */
30 TheoryId
Theory::s_uninterpretedSortOwner
= THEORY_UF
;
32 std::ostream
& operator<<(std::ostream
& os
, Theory::Effort level
){
34 case Theory::EFFORT_STANDARD
:
35 os
<< "EFFORT_STANDARD"; break;
36 case Theory::EFFORT_FULL
:
37 os
<< "EFFORT_FULL"; break;
38 case Theory::EFFORT_COMBINATION
:
39 os
<< "EFFORT_COMBINATION"; break;
40 case Theory::EFFORT_LAST_CALL
:
41 os
<< "EFFORT_LAST_CALL"; break;
46 }/* ostream& operator<<(ostream&, Theory::Effort) */
49 StatisticsRegistry::unregisterStat(&d_computeCareGraphTime
);
52 TheoryId
Theory::theoryOf(TheoryOfMode mode
, TNode node
) {
54 Trace("theory::internal") << "theoryOf(" << node
<< ")" << std::endl
;
57 case THEORY_OF_TYPE_BASED
:
58 // Constants, variables, 0-ary constructors
59 if (node
.isVar() || node
.isConst()) {
60 return theoryOf(node
.getType());
62 // Equality is owned by the theory that owns the domain
63 if (node
.getKind() == kind::EQUAL
) {
64 return theoryOf(node
[0].getType());
66 // Regular nodes are owned by the kind
67 return kindToTheoryId(node
.getKind());
69 case THEORY_OF_TERM_BASED
:
72 if (theoryOf(node
.getType()) != theory::THEORY_BOOL
) {
73 // We treat the variables as uninterpreted
74 return s_uninterpretedSortOwner
;
76 // Except for the Boolean ones, which we just ignore anyhow
77 return theory::THEORY_BOOL
;
82 // Constants go to the theory of the type
83 return theoryOf(node
.getType());
86 if (node
.getKind() == kind::EQUAL
) {
87 // If one of them is an ITE, it's irelevant, since they will get replaced out anyhow
88 if (node
[0].getKind() == kind::ITE
) {
89 return theoryOf(node
[0].getType());
91 if (node
[1].getKind() == kind::ITE
) {
92 return theoryOf(node
[1].getType());
94 // If both sides belong to the same theory the choice is easy
95 TheoryId T1
= theoryOf(node
[0]);
96 TheoryId T2
= theoryOf(node
[1]);
100 TheoryId T3
= theoryOf(node
[0].getType());
102 // * x*y = f(z) -> UF
104 // * f(x) = read(a, y) -> either UF or ARRAY
105 // at least one of the theories has to be parametric, i.e. theory of the type is different
106 // from the theory of the term
113 // If both are parametric, we take the smaller one (arbitraty)
114 return T1
< T2
? T1
: T2
;
116 // Regular nodes are owned by the kind
117 return kindToTheoryId(node
.getKind());
124 void Theory::addSharedTermInternal(TNode n
) {
125 Debug("sharing") << "Theory::addSharedTerm<" << getId() << ">(" << n
<< ")" << endl
;
126 Debug("theory::assertions") << "Theory::addSharedTerm<" << getId() << ">(" << n
<< ")" << endl
;
127 d_sharedTerms
.push_back(n
);
131 void Theory::computeCareGraph() {
132 Debug("sharing") << "Theory::computeCareGraph<" << getId() << ">()" << endl
;
133 for (unsigned i
= 0; i
< d_sharedTerms
.size(); ++ i
) {
134 TNode a
= d_sharedTerms
[i
];
135 TypeNode aType
= a
.getType();
136 for (unsigned j
= i
+ 1; j
< d_sharedTerms
.size(); ++ j
) {
137 TNode b
= d_sharedTerms
[j
];
138 if (b
.getType() != aType
) {
139 // We don't care about the terms of different types
142 switch (d_valuation
.getEqualityStatus(a
, b
)) {
143 case EQUALITY_TRUE_AND_PROPAGATED
:
144 case EQUALITY_FALSE_AND_PROPAGATED
:
145 // If we know about it, we should have propagated it, so we can skip
156 void Theory::printFacts(std::ostream
& os
) const {
157 unsigned i
, n
= d_facts
.size();
158 for(i
= 0; i
< n
; i
++){
159 const Assertion
& a_i
= d_facts
[i
];
160 Node assertion
= a_i
;
161 os
<< d_id
<< '[' << i
<< ']' << " " << assertion
<< endl
;
165 void Theory::debugPrintFacts() const{
166 DebugChannel
.getStream() << "Theory::debugPrintFacts()" << endl
;
167 printFacts(DebugChannel
.getStream());
170 std::hash_set
<TNode
, TNodeHashFunction
> Theory::currentlySharedTerms() const{
171 std::hash_set
<TNode
, TNodeHashFunction
> currentlyShared
;
172 for(shared_terms_iterator i
= shared_terms_begin(), i_end
= shared_terms_end(); i
!= i_end
; ++i
){
173 currentlyShared
.insert (*i
);
175 return currentlyShared
;
179 void Theory::collectTerms(TNode n
, set
<Node
>& termSet
) const
181 if (termSet
.find(n
) != termSet
.end()) {
184 Trace("theory::collectTerms") << "Theory::collectTerms: adding " << n
<< endl
;
186 if (n
.getKind() == kind::NOT
|| n
.getKind() == kind::EQUAL
|| !isLeaf(n
)) {
187 for(TNode::iterator child_it
= n
.begin(); child_it
!= n
.end(); ++child_it
) {
188 collectTerms(*child_it
, termSet
);
194 void Theory::computeRelevantTerms(set
<Node
>& termSet
) const
196 // Collect all terms appearing in assertions
197 context::CDList
<Assertion
>::const_iterator assert_it
= facts_begin(), assert_it_end
= facts_end();
198 for (; assert_it
!= assert_it_end
; ++assert_it
) {
199 collectTerms(*assert_it
, termSet
);
202 // Add terms that are shared terms
203 context::CDList
<TNode
>::const_iterator shared_it
= shared_terms_begin(), shared_it_end
= shared_terms_end();
204 for (; shared_it
!= shared_it_end
; ++shared_it
) {
205 collectTerms(*shared_it
, termSet
);
210 Theory::PPAssertStatus
Theory::ppAssert(TNode in
, SubstitutionMap
& outSubstitutions
)
212 if (in
.getKind() == kind::EQUAL
) {
213 if (in
[0].isVar() && !in
[1].hasSubterm(in
[0])) {
214 outSubstitutions
.addSubstitution(in
[0], in
[1]);
215 return PP_ASSERT_STATUS_SOLVED
;
217 if (in
[1].isVar() && !in
[0].hasSubterm(in
[1])) {
218 outSubstitutions
.addSubstitution(in
[1], in
[0]);
219 return PP_ASSERT_STATUS_SOLVED
;
221 if (in
[0].isConst() && in
[1].isConst()) {
222 if (in
[0] != in
[1]) {
223 return PP_ASSERT_STATUS_CONFLICT
;
228 return PP_ASSERT_STATUS_UNSOLVED
;
231 std::pair
<bool, Node
> Theory::entailmentCheck(TNode lit
,
232 const EntailmentCheckParameters
* params
,
233 EntailmentCheckSideEffects
* out
){
234 return make_pair(false, Node::null());
237 EntailmentCheckParameters::EntailmentCheckParameters(TheoryId tid
)
241 EntailmentCheckParameters::~EntailmentCheckParameters(){}
243 TheoryId
EntailmentCheckParameters::getTheoryId() const {
247 EntailmentCheckSideEffects::EntailmentCheckSideEffects(TheoryId tid
)
251 TheoryId
EntailmentCheckSideEffects::getTheoryId() const {
255 EntailmentCheckSideEffects::~EntailmentCheckSideEffects() {
258 }/* CVC4::theory namespace */
259 }/* CVC4 namespace */