diff options
author | Dejan Jovanović <dejan.jovanovic@gmail.com> | 2012-06-16 21:35:05 +0000 |
---|---|---|
committer | Dejan Jovanović <dejan.jovanovic@gmail.com> | 2012-06-16 21:35:05 +0000 |
commit | bc36750b551f1d0b571af1e2265b5dea42544e7d (patch) | |
tree | 4d8621cce48900fe3220d55b5fb451adeb125607 /src/theory/theory.cpp | |
parent | adae14a07b1019d092b4d5aa0cf809f9d0eca66d (diff) |
changing theoryOf in shared mode with arrays to move equalities to arrays
disabled in bitvectors due to non-stably infinite problems
the option to enable it is --theoryof-mode=term
Diffstat (limited to 'src/theory/theory.cpp')
-rw-r--r-- | src/theory/theory.cpp | 75 |
1 files changed, 75 insertions, 0 deletions
diff --git a/src/theory/theory.cpp b/src/theory/theory.cpp index 7555282d8..1dd0a1209 100644 --- a/src/theory/theory.cpp +++ b/src/theory/theory.cpp @@ -31,6 +31,9 @@ namespace theory { /** Default value for the uninterpreted sorts is the UF theory */ TheoryId Theory::s_uninterpretedSortOwner = THEORY_UF; +/** By default, we use the type based theoryOf */ +TheoryOfMode Theory::s_theoryOfMode = THEORY_OF_TYPE_BASED; + std::ostream& operator<<(std::ostream& os, Theory::Effort level){ switch(level){ case Theory::EFFORT_STANDARD: @@ -56,6 +59,78 @@ Theory::~Theory() { StatisticsRegistry::unregisterStat(&d_computeCareGraphTime); } +TheoryId Theory::theoryOf(TheoryOfMode mode, TNode node) { + + Trace("theory::internal") << "theoryOf(" << node << ")" << std::endl; + + switch(mode) { + case THEORY_OF_TYPE_BASED: + // Constants, variables, 0-ary constructors + if (node.getMetaKind() == kind::metakind::VARIABLE || node.getMetaKind() == kind::metakind::CONSTANT) { + return theoryOf(node.getType()); + } + // Equality is owned by the theory that owns the domain + if (node.getKind() == kind::EQUAL) { + return theoryOf(node[0].getType()); + } + // Regular nodes are owned by the kind + return kindToTheoryId(node.getKind()); + break; + case THEORY_OF_TERM_BASED: + // Variables + if (node.getMetaKind() == kind::metakind::VARIABLE) { + if (theoryOf(node.getType()) != theory::THEORY_BOOL) { + // We treat the varibables as uninterpreted + return s_uninterpretedSortOwner; + } else { + // Except for the Boolean ones, which we just ignore anyhow + return theory::THEORY_BOOL; + } + } + // Constants + if (node.getMetaKind() == kind::metakind::CONSTANT) { + // Constants go to the theory of the type + return theoryOf(node.getType()); + } + // Equality + if (node.getKind() == kind::EQUAL) { + // If one of them is an ITE, it's irelevant, since they will get replaced out anyhow + if (node[0].getKind() == kind::ITE) { + return theoryOf(node[0].getType()); + } + if (node[1].getKind() == kind::ITE) { + return theoryOf(node[1].getType()); + } + // If both sides belong to the same theory the choice is easy + TheoryId T1 = theoryOf(node[0]); + TheoryId T2 = theoryOf(node[1]); + if (T1 == T2) { + return T1; + } + TheoryId T3 = theoryOf(node[0].getType()); + // This is a case of + // * x*y = f(z) -> UF + // * x = c -> UF + // * f(x) = read(a, y) -> either UF or ARRAY + // at least one of the theories has to be parametric, i.e. theory of the type is different + // from the theory of the term + if (T1 == T3) { + return T2; + } + if (T2 == T3) { + return T1; + } + // If both are parametric, we take the smaller one (arbitraty) + return T1 < T2 ? T1 : T2; + } + // Regular nodes are owned by the kind + return kindToTheoryId(node.getKind()); + break; + default: + Unreachable(); + } +} + void Theory::addSharedTermInternal(TNode n) { Debug("sharing") << "Theory::addSharedTerm<" << getId() << ">(" << n << ")" << endl; Debug("theory::assertions") << "Theory::addSharedTerm<" << getId() << ">(" << n << ")" << endl; |