diff options
author | Morgan Deters <mdeters@gmail.com> | 2012-06-11 16:28:23 +0000 |
---|---|---|
committer | Morgan Deters <mdeters@gmail.com> | 2012-06-11 16:28:23 +0000 |
commit | 3378e253fcdb34c753407bb16d08929da06b3aaa (patch) | |
tree | db7c7118dd0d1594175b56866f845b42426ae0a7 /src/theory/shared_terms_database.h | |
parent | 42794501e81c44dce5c2f7687af288af030ef63e (diff) |
Merge from quantifiers2-trunkmerge branch.
Adds TheoryQuantifiers and TheoryRewriteRules, QuantifiersEngine, and other infrastructure.
Adds theory instantiators to many theories.
Adds the UF strong solver.
Diffstat (limited to 'src/theory/shared_terms_database.h')
-rw-r--r-- | src/theory/shared_terms_database.h | 21 |
1 files changed, 13 insertions, 8 deletions
diff --git a/src/theory/shared_terms_database.h b/src/theory/shared_terms_database.h index fccd2e6bc..c7da8a463 100644 --- a/src/theory/shared_terms_database.h +++ b/src/theory/shared_terms_database.h @@ -2,7 +2,7 @@ /*! \file node_visitor.h ** \verbatim ** Original author: dejan - ** Major contributors: + ** Major contributors: ** Minor contributors (to current version): ** This file is part of the CVC4 prototype. ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys) @@ -40,7 +40,7 @@ private: /** The context */ context::Context* d_context; - + /** Some statistics */ IntStat d_statSharedTerms; @@ -49,13 +49,13 @@ private: /** A map from atoms to a list of shared terms */ SharedTermsMap d_atomsToTerms; - + /** Each time we add a shared term, we add it's parent to this list */ std::vector<TNode> d_addedSharedTerms; - + /** Context-dependent size of the d_addedSharedTerms list */ context::CDO<unsigned> d_addedSharedTermsSize; - + /** A map from atoms and subterms to the theories that use it */ typedef context::CDHashMap<std::pair<Node, TNode>, theory::Theory::Set, TNodePairHashFunction> SharedTermsTheoriesMap; SharedTermsTheoriesMap d_termsToTheories; @@ -95,6 +95,11 @@ private: void eqNotifyConstantTermMerge(TNode t1, TNode t2) { d_sharedTerms.conflict(t1, t2, true); } + + void eqNotifyNewClass(TNode t) { } + void eqNotifyPreMerge(TNode t1, TNode t2) { } + void eqNotifyPostMerge(TNode t1, TNode t2) { } + void eqNotifyDisequal(TNode t1, TNode t2, TNode reason) { } }; /** The notify class for d_equalityEngine */ @@ -147,7 +152,7 @@ public: SharedTermsDatabase(TheoryEngine* theoryEngine, context::Context* context); ~SharedTermsDatabase() throw(AssertionException); - + /** * Asserts the equality to the shared terms database, */ @@ -185,12 +190,12 @@ public: bool hasSharedTerms(TNode atom) const; /** - * Iterator pointing to the first shared term belonging to the given atom. + * Iterator pointing to the first shared term belonging to the given atom. */ shared_terms_iterator begin(TNode atom) const; /** - * Iterator pointing to the end of the list of shared terms belonging to the given atom. + * Iterator pointing to the end of the list of shared terms belonging to the given atom. */ shared_terms_iterator end(TNode atom) const; |