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 | |
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')
-rw-r--r-- | src/theory/Makefile.am | 1 | ||||
-rw-r--r-- | src/theory/arrays/theory_arrays.cpp | 2 | ||||
-rw-r--r-- | src/theory/rewriter.cpp | 18 | ||||
-rw-r--r-- | src/theory/theory.cpp | 75 | ||||
-rw-r--r-- | src/theory/theory.h | 35 | ||||
-rw-r--r-- | src/theory/theory_engine.cpp | 2 | ||||
-rw-r--r-- | src/theory/theoryof_mode.h | 36 | ||||
-rw-r--r-- | src/theory/uf/theory_uf.cpp | 2 |
8 files changed, 149 insertions, 22 deletions
diff --git a/src/theory/Makefile.am b/src/theory/Makefile.am index 19e7d588a..84af80035 100644 --- a/src/theory/Makefile.am +++ b/src/theory/Makefile.am @@ -18,6 +18,7 @@ libtheory_la_SOURCES = \ theory_test_utils.h \ theory.h \ theory.cpp \ + theoryof_mode.h \ theory_registrar.h \ rewriter.h \ rewriter_attributes.h \ diff --git a/src/theory/arrays/theory_arrays.cpp b/src/theory/arrays/theory_arrays.cpp index 9717f6286..041a5924a 100644 --- a/src/theory/arrays/theory_arrays.cpp +++ b/src/theory/arrays/theory_arrays.cpp @@ -1315,7 +1315,7 @@ void TheoryArrays::dischargeLemmas() } void TheoryArrays::conflict(TNode a, TNode b) { - if (Theory::theoryOf(a) == theory::THEORY_BOOL) { + if (a.getKind() == kind::CONST_BOOLEAN) { d_conflictNode = explain(a.iffNode(b)); } else { d_conflictNode = explain(a.eqNode(b)); diff --git a/src/theory/rewriter.cpp b/src/theory/rewriter.cpp index 8c20c84c1..a91243343 100644 --- a/src/theory/rewriter.cpp +++ b/src/theory/rewriter.cpp @@ -26,6 +26,10 @@ using namespace std; namespace CVC4 { namespace theory { +static TheoryId theoryOf(TNode node) { + return Theory::theoryOf(THEORY_OF_TYPE_BASED, node); +} + std::hash_set<Node, NodeHashFunction> d_rewriteStack; /** @@ -61,7 +65,7 @@ struct RewriteStackElement { }; Node Rewriter::rewrite(TNode node) { - return rewriteTo(theory::Theory::theoryOf(node), node); + return rewriteTo(theoryOf(node), node); } Node Rewriter::rewriteTo(theory::TheoryId theoryId, Node node) { @@ -102,7 +106,7 @@ Node Rewriter::rewriteTo(theory::TheoryId theoryId, Node node) { RewriteResponse response = Rewriter::callPreRewrite((TheoryId) rewriteStackTop.theoryId, rewriteStackTop.node); // Put the rewritten node to the top of the stack rewriteStackTop.node = response.node; - TheoryId newTheory = Theory::theoryOf(rewriteStackTop.node); + TheoryId newTheory = theoryOf(rewriteStackTop.node); // In the pre-rewrite, if changing theories, we just call the other theories pre-rewrite if (newTheory == (TheoryId) rewriteStackTop.theoryId && response.status == REWRITE_DONE) { break; @@ -116,7 +120,7 @@ Node Rewriter::rewriteTo(theory::TheoryId theoryId, Node node) { else { // Continue with the cached version rewriteStackTop.node = cached; - rewriteStackTop.theoryId = Theory::theoryOf(cached); + rewriteStackTop.theoryId = theoryOf(cached); } } @@ -145,7 +149,7 @@ Node Rewriter::rewriteTo(theory::TheoryId theoryId, Node node) { // The child node Node childNode = rewriteStackTop.node[child]; // Push the rewrite request to the stack (NOTE: rewriteStackTop might be a bad reference now) - rewriteStack.push_back(RewriteStackElement(childNode, Theory::theoryOf(childNode))); + rewriteStack.push_back(RewriteStackElement(childNode, theoryOf(childNode))); // Go on with the rewriting continue; } @@ -153,7 +157,7 @@ Node Rewriter::rewriteTo(theory::TheoryId theoryId, Node node) { // Incorporate the children if necessary if (rewriteStackTop.node.getNumChildren() > 0) { rewriteStackTop.node = rewriteStackTop.builder; - rewriteStackTop.theoryId = Theory::theoryOf(rewriteStackTop.node); + rewriteStackTop.theoryId = theoryOf(rewriteStackTop.node); } // Done with all pre-rewriting, so let's do the post rewrite @@ -161,7 +165,7 @@ Node Rewriter::rewriteTo(theory::TheoryId theoryId, Node node) { // Do the post-rewrite RewriteResponse response = Rewriter::callPostRewrite((TheoryId) rewriteStackTop.theoryId, rewriteStackTop.node); // We continue with the response we got - TheoryId newTheoryId = Theory::theoryOf(response.node); + TheoryId newTheoryId = theoryOf(response.node); if (newTheoryId != (TheoryId) rewriteStackTop.theoryId || response.status == REWRITE_AGAIN_FULL) { // In the post rewrite if we've changed theories, we must do a full rewrite Assert(response.node != rewriteStackTop.node); @@ -194,7 +198,7 @@ Node Rewriter::rewriteTo(theory::TheoryId theoryId, Node node) { } else { // We were already in cache, so just remember it rewriteStackTop.node = cached; - rewriteStackTop.theoryId = Theory::theoryOf(cached); + rewriteStackTop.theoryId = theoryOf(cached); } // If this is the last node, just return 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; 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 { diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp index 30b9cd098..0c0d65d74 100644 --- a/src/theory/theory_engine.cpp +++ b/src/theory/theory_engine.cpp @@ -904,7 +904,7 @@ void TheoryEngine::assertToTheory(TNode assertion, theory::TheoryId toTheoryId, // Try and assert (note that we assert the non-normalized one) if (markPropagation(normalizedAssertion, assertion, toTheoryId, fromTheoryId)) { // Check if has been pre-registered with the theory - bool preregistered = d_propEngine->isSatLiteral(normalizedAssertion) && Theory::theoryOf(normalizedAssertion) == toTheoryId; + bool preregistered = d_propEngine->isSatLiteral(normalizedAssertion) && Theory::theoryOf(normalizedAtom) == toTheoryId; // Assert away theoryOf(toTheoryId)->assertFact(normalizedAssertion, preregistered); d_factsAsserted = true; diff --git a/src/theory/theoryof_mode.h b/src/theory/theoryof_mode.h new file mode 100644 index 000000000..533704a39 --- /dev/null +++ b/src/theory/theoryof_mode.h @@ -0,0 +1,36 @@ +/********************* */ +/*! \file theory.h + ** \verbatim + ** Original author: mdeters + ** Major contributors: dejan + ** Minor contributors (to current version): taking, barrett + ** This file is part of the CVC4 prototype. + ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys) + ** Courant Institute of Mathematical Sciences + ** New York University + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** \brief Base of the theory interface. + ** + ** Base of the theory interface. + **/ + +#pragma once + +#include "cvc4_public.h" + +namespace CVC4 { +namespace theory { + +/** How do we associate theories with the terms */ +enum TheoryOfMode { + /** Equality, variables and constants are associated with the types */ + THEORY_OF_TYPE_BASED, + /** Variables are uninterpreted, constants are with the type, equalities prefer parametric */ + THEORY_OF_TERM_BASED +}; + +} +} + diff --git a/src/theory/uf/theory_uf.cpp b/src/theory/uf/theory_uf.cpp index dc7bb7c92..5d36cd082 100644 --- a/src/theory/uf/theory_uf.cpp +++ b/src/theory/uf/theory_uf.cpp @@ -418,7 +418,7 @@ void TheoryUF::computeCareGraph() { }/* TheoryUF::computeCareGraph() */ void TheoryUF::conflict(TNode a, TNode b) { - if (Theory::theoryOf(a) == theory::THEORY_BOOL) { + if (a.getKind() == kind::CONST_BOOLEAN) { d_conflictNode = explain(a.iffNode(b)); } else { d_conflictNode = explain(a.eqNode(b)); |