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.h | |
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.h')
-rw-r--r-- | src/theory/theory.h | 35 |
1 files changed, 23 insertions, 12 deletions
diff --git a/src/theory/theory.h b/src/theory/theory.h index 8c830f8a2..217972dce 100644 --- a/src/theory/theory.h +++ b/src/theory/theory.h @@ -28,6 +28,7 @@ #include "theory/substitutions.h" #include "theory/output_channel.h" #include "theory/logic_info.h" +#include "theory/theoryof_mode.h" #include "context/context.h" #include "context/cdlist.h" #include "context/cdo.h" @@ -122,6 +123,7 @@ typedef std::set<CarePair> CareGraph; * all calls to them.) */ class Theory { + private: friend class ::CVC4::TheoryEngine; @@ -291,6 +293,9 @@ protected: void printFacts(std::ostream& os) const; void debugPrintFacts() const; + /** Mode of the theoryOf operation */ + static TheoryOfMode s_theoryOfMode; + public: /** @@ -314,24 +319,23 @@ public: return id; } + /** + * Returns the ID of the theory responsible for the given node. + */ + static TheoryId theoryOf(TheoryOfMode mode, TNode node); /** * Returns the ID of the theory responsible for the given node. */ static inline TheoryId theoryOf(TNode node) { - Trace("theory::internal") << "theoryOf(" << node << ")" << std::endl; - // 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()); + return theoryOf(s_theoryOfMode, node); } - + + /** Set the theoryOf mode */ + static void setTheoryOfMode(TheoryOfMode mode) { + s_theoryOfMode = mode; + } + /** * Set the owner of the uninterpreted sort. */ @@ -340,6 +344,13 @@ public: } /** + * Set the owner of the uninterpreted sort. + */ + static TheoryId getUninterpretedSortOwner() { + return s_uninterpretedSortOwner; + } + + /** * Checks if the node is a leaf node of this theory */ inline bool isLeaf(TNode node) const { |