diff options
author | Tim King <taking@cs.nyu.edu> | 2014-06-06 11:45:16 -0400 |
---|---|---|
committer | Tim King <taking@cs.nyu.edu> | 2014-06-06 16:26:40 -0400 |
commit | 6ec8f46e9a7315057ac8fb5c58a6b44cf5a5159e (patch) | |
tree | 9afae28a572c91b4c9f93ca137c84d1fa1808aef /src/theory/theory.cpp | |
parent | 0dce010bea47bc6a318eece2bd92ed2305b64c21 (diff) |
Patch for the subtype theoryof mode to make the equalities over disequal types get sent to the theory of the type.
Adding a new test case for bug 569.
Fixes to the normal form of arithmetic so that real terms are before integer terms.
Diffstat (limited to 'src/theory/theory.cpp')
-rw-r--r-- | src/theory/theory.cpp | 100 |
1 files changed, 53 insertions, 47 deletions
diff --git a/src/theory/theory.cpp b/src/theory/theory.cpp index 2dd474a19..d9281e8ba 100644 --- a/src/theory/theory.cpp +++ b/src/theory/theory.cpp @@ -50,75 +50,81 @@ Theory::~Theory() { } TheoryId Theory::theoryOf(TheoryOfMode mode, TNode node) { - - Trace("theory::internal") << "theoryOf(" << node << ")" << std::endl; - + TheoryId tid = THEORY_BUILTIN; switch(mode) { case THEORY_OF_TYPE_BASED: // Constants, variables, 0-ary constructors if (node.isVar() || node.isConst()) { - return theoryOf(node.getType()); - } - // Equality is owned by the theory that owns the domain - if (node.getKind() == kind::EQUAL) { - return theoryOf(node[0].getType()); + tid = Theory::theoryOf(node.getType()); + } else if (node.getKind() == kind::EQUAL) { + // Equality is owned by the theory that owns the domain + tid = Theory::theoryOf(node[0].getType()); + } else { + // Regular nodes are owned by the kind + tid = kindToTheoryId(node.getKind()); } - // Regular nodes are owned by the kind - return kindToTheoryId(node.getKind()); break; case THEORY_OF_TERM_BASED: // Variables if (node.isVar()) { - if (theoryOf(node.getType()) != theory::THEORY_BOOL) { + if (Theory::theoryOf(node.getType()) != theory::THEORY_BOOL) { // We treat the variables as uninterpreted - return s_uninterpretedSortOwner; + tid = s_uninterpretedSortOwner; } else { // Except for the Boolean ones, which we just ignore anyhow - return theory::THEORY_BOOL; + tid = theory::THEORY_BOOL; } - } - // Constants - if (node.isConst()) { + } else if (node.isConst()) { // Constants go to the theory of the type - return theoryOf(node.getType()); - } - // Equality - if (node.getKind() == kind::EQUAL) { + tid = Theory::theoryOf(node.getType()); + } else if (node.getKind() == kind::EQUAL) { // Equality // 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; + tid = Theory::theoryOf(node[0].getType()); + } else if (node[1].getKind() == kind::ITE) { + tid = Theory::theoryOf(node[1].getType()); + } else { + TNode l = node[0]; + TNode r = node[1]; + TypeNode ltype = l.getType(); + TypeNode rtype = r.getType(); + if( ltype != rtype ){ + tid = Theory::theoryOf(l.getType()); + }else { + // If both sides belong to the same theory the choice is easy + TheoryId T1 = Theory::theoryOf(l); + TheoryId T2 = Theory::theoryOf(r); + if (T1 == T2) { + tid = T1; + } else { + TheoryId T3 = Theory::theoryOf(ltype); + // 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) { + tid = T2; + } else if (T2 == T3) { + tid = T1; + } else { + // If both are parametric, we take the smaller one (arbitrary) + tid = T1 < T2 ? T1 : T2; + } + } + } } - // If both are parametric, we take the smaller one (arbitraty) - return T1 < T2 ? T1 : T2; + } else { + // Regular nodes are owned by the kind + tid = kindToTheoryId(node.getKind()); } - // Regular nodes are owned by the kind - return kindToTheoryId(node.getKind()); break; default: Unreachable(); } + Trace("theory::internal") << "theoryOf(" << mode << ", " << node << ") -> " << tid << std::endl; + return tid; } void Theory::addSharedTermInternal(TNode n) { |