diff options
Diffstat (limited to 'src/theory/theory.cpp')
-rw-r--r-- | src/theory/theory.cpp | 186 |
1 files changed, 114 insertions, 72 deletions
diff --git a/src/theory/theory.cpp b/src/theory/theory.cpp index 719239806..a159787f9 100644 --- a/src/theory/theory.cpp +++ b/src/theory/theory.cpp @@ -16,13 +16,14 @@ #include "theory/theory.h" -#include <vector> -#include <sstream> #include <iostream> +#include <sstream> #include <string> +#include <vector> #include "base/check.h" #include "expr/node_algorithm.h" +#include "options/theory_options.h" #include "smt/smt_statistics_registry.h" #include "theory/ext_theory.h" #include "theory/quantifiers_engine.h" @@ -90,87 +91,128 @@ Theory::~Theory() { delete d_extTheory; } -TheoryId Theory::theoryOf(TheoryOfMode mode, TNode node) { +TheoryId Theory::theoryOf(options::TheoryOfMode mode, TNode node) +{ TheoryId tid = THEORY_BUILTIN; switch(mode) { - case THEORY_OF_TYPE_BASED: - // Constants, variables, 0-ary constructors - if (node.isVar()) { - if( node.getKind() == kind::BOOLEAN_TERM_VARIABLE ){ - tid = THEORY_UF; - }else{ - tid = Theory::theoryOf(node.getType()); - } - }else if (node.isConst()) { - 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()); - } - break; - case THEORY_OF_TERM_BASED: - // Variables - if (node.isVar()) { - if (Theory::theoryOf(node.getType()) != theory::THEORY_BOOL) { - // We treat the variables as uninterpreted - tid = s_uninterpretedSortOwner; - } else { - if( node.getKind() == kind::BOOLEAN_TERM_VARIABLE ){ - //Boolean vars go to UF + case options::TheoryOfMode::THEORY_OF_TYPE_BASED: + // Constants, variables, 0-ary constructors + if (node.isVar()) + { + if (node.getKind() == kind::BOOLEAN_TERM_VARIABLE) + { tid = THEORY_UF; - }else{ - // Except for the Boolean ones - tid = THEORY_BOOL; } + else + { + tid = Theory::theoryOf(node.getType()); + } + } + else if (node.isConst()) + { + tid = Theory::theoryOf(node.getType()); } - } else if (node.isConst()) { - // Constants go to the theory of the type - 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) { + else if (node.getKind() == kind::EQUAL) + { + // Equality is owned by the theory that owns the domain 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) { + } + else + { + // Regular nodes are owned by the kind + tid = kindToTheoryId(node.getKind()); + } + break; + case options::TheoryOfMode::THEORY_OF_TERM_BASED: + // Variables + if (node.isVar()) + { + if (Theory::theoryOf(node.getType()) != theory::THEORY_BOOL) + { + // We treat the variables as uninterpreted + tid = s_uninterpretedSortOwner; + } + else + { + if (node.getKind() == kind::BOOLEAN_TERM_VARIABLE) + { + // Boolean vars go to UF + tid = THEORY_UF; + } + else + { + // Except for the Boolean ones + tid = THEORY_BOOL; + } + } + } + else if (node.isConst()) + { + // Constants go to the theory of the type + 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) + { + 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 { - // If both are parametric, we take the smaller one (arbitrary) - tid = T1 < T2 ? T1 : T2; + } + 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; + } } } } } - } else { - // Regular nodes are owned by the kind - tid = kindToTheoryId(node.getKind()); - } + else + { + // Regular nodes are owned by the kind + tid = kindToTheoryId(node.getKind()); + } break; default: Unreachable(); |