diff options
author | Dejan Jovanović <dejan.jovanovic@gmail.com> | 2011-08-24 21:03:19 +0000 |
---|---|---|
committer | Dejan Jovanović <dejan.jovanovic@gmail.com> | 2011-08-24 21:03:19 +0000 |
commit | 278cdeb360322c7e9ae4b102abd740d101f37c6d (patch) | |
tree | 4c6c79e73b1c9cb60b21c8ffb743c4218f61094f /src/theory/theory.h | |
parent | ad18245c092ea6e5b998b556aaec74ef9109bd8c (diff) |
Simplification of the preregister and register throught a NodeVisitor class. The theoryOf is not all in one place, theory::theoryOf. The uninterpreted sorts belong to the builtin theory and are dispatched to the apropriate theory (QF_UF, QF_AX) through theoryOf based on the setting in the Theory class.
Diffstat (limited to 'src/theory/theory.h')
-rw-r--r-- | src/theory/theory.h | 41 |
1 files changed, 28 insertions, 13 deletions
diff --git a/src/theory/theory.h b/src/theory/theory.h index 93d78f57c..1d8797d1f 100644 --- a/src/theory/theory.h +++ b/src/theory/theory.h @@ -40,11 +40,6 @@ class TheoryEngine; namespace theory { -/** Tag for the "newFact()-has-been-called-in-this-context" flag on Nodes */ -struct AssertedAttrTag {}; -/** The "newFact()-has-been-called-in-this-context" flag on Nodes */ -typedef CVC4::expr::CDAttribute<AssertedAttrTag, bool> Asserted; - /** * Base class for T-solvers. Abstract DPLL(T). * @@ -178,31 +173,51 @@ protected: return d_facts.end(); } + /** + * The theory that owns the uninterpreted sort. + */ + static TheoryId d_uninterpretedSortOwner; + public: /** * Return the ID of the theory responsible for the given type. */ static inline TheoryId theoryOf(TypeNode typeNode) { + TheoryId id; if (typeNode.getKind() == kind::TYPE_CONSTANT) { - return typeConstantToTheoryId(typeNode.getConst<TypeConstant>()); + id = typeConstantToTheoryId(typeNode.getConst<TypeConstant>()); } else { - return kindToTheoryId(typeNode.getKind()); + id = kindToTheoryId(typeNode.getKind()); + } + if (id == THEORY_BUILTIN) { + return d_uninterpretedSortOwner; } + return id; } + /** * Returns the ID of the theory responsible for the given node. */ static inline TheoryId theoryOf(TNode node) { - if (node.getMetaKind() == kind::metakind::VARIABLE || - node.getMetaKind() == kind::metakind::CONSTANT) { - // Constants, variables, 0-ary constructors + // Constants, variables, 0-ary constructors + if (node.getMetaKind() == kind::metakind::VARIABLE || node.getMetaKind() == kind::metakind::CONSTANT) { return theoryOf(node.getType()); - } else { - // Regular nodes - return kindToTheoryId(node.getKind()); } + // 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()); + } + + /** + * Set the owner of the uninterpreted sort. + */ + static void setUninterpretedSortOwner(TheoryId theory) { + d_uninterpretedSortOwner = theory; } /** |