diff options
author | Dejan Jovanović <dejan.jovanovic@gmail.com> | 2012-06-06 06:12:40 +0000 |
---|---|---|
committer | Dejan Jovanović <dejan.jovanovic@gmail.com> | 2012-06-06 06:12:40 +0000 |
commit | fd9e22c4a2e57c3dfeda4de3842a3fb3ca4776ba (patch) | |
tree | 047e4d27f725e9157ed5bef5357d0d72560218ae /src/theory/shared_terms_database.h | |
parent | 2799ae1cf57ed2b98387a1de1325bccd89bd2a30 (diff) |
Changes to the combination mechanism, lots of details. Not done yet, there are still the AUFBV wrong results, but it seems better.
http://church.cims.nyu.edu/regress-results/compare_jobs.php?job_id=4382&reference_id=4359&p=5
Diffstat (limited to 'src/theory/shared_terms_database.h')
-rw-r--r-- | src/theory/shared_terms_database.h | 158 |
1 files changed, 96 insertions, 62 deletions
diff --git a/src/theory/shared_terms_database.h b/src/theory/shared_terms_database.h index c044097ff..1a38d7332 100644 --- a/src/theory/shared_terms_database.h +++ b/src/theory/shared_terms_database.h @@ -18,12 +18,14 @@ #include "expr/node.h" #include "theory/theory.h" -#include "context/context.h" -#include "util/stats.h" #include "theory/uf/equality_engine.h" +#include "util/stats.h" +#include "context/cdhashset.h" namespace CVC4 { +class TheoryEngine; + class SharedTermsDatabase : public context::ContextNotifyObj { public: @@ -54,51 +56,20 @@ private: /** Context-dependent size of the d_addedSharedTerms list */ context::CDO<unsigned> d_addedSharedTermsSize; - typedef context::CDHashMap<std::pair<Node, TNode>, theory::Theory::Set, TNodePairHashFunction> SharedTermsTheoriesMap; - /** 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; - typedef context::CDHashMap<TNode, theory::Theory::Set, TNodeHashFunction> AlreadyNotifiedMap; - /** Map from term to theories that have already been notified about the shared term */ + typedef context::CDHashMap<TNode, theory::Theory::Set, TNodeHashFunction> AlreadyNotifiedMap; AlreadyNotifiedMap d_alreadyNotifiedMap; -public: - - /** Class for notifications about new shared term equalities */ - class SharedTermsNotifyClass { - public: - SharedTermsNotifyClass() {} - virtual ~SharedTermsNotifyClass() {} - virtual void notify(TNode literal, TNode original, theory::TheoryId theory) = 0; - }; + /** The registered equalities for propagation */ + typedef context::CDHashSet<TNode, TNodeHashFunction> RegisteredEqualitiesSet; + RegisteredEqualitiesSet d_registeredEqualities; private: - // Instance of class to send shared term notifications to - SharedTermsNotifyClass& d_sharedNotify; - - // Type for list of theory, node pairs: theory is theory to be notified, - // node is the representative for this equivalence class known to the - // theory that will be notified - typedef context::CDHashMap<theory::TheoryId, TNode, __gnu_cxx::hash<unsigned> > NotifyList; - typedef context::CDHashMap<TNode, NotifyList*, TNodeHashFunction> TermToNotifyList; - - // Map from terms (only valid for reps) to their notify lists - // Note that theory, term pairs only need to be in the notify list if the - // representative term is not a valid shared term for the theory. - TermToNotifyList d_termToNotifyList; - - // List of allocated NotifyList* objects - std::vector<NotifyList*> d_allocatedNL; - - // Total number of allocated NotifyList* objects - unsigned d_allocatedNLSize; - - // Size of portion of d_allocatedNL that is currently in use - context::CDO<unsigned> d_allocatedNLNext; - /** This method removes all the un-necessary stuff from the maps */ void backtrack(); @@ -108,7 +79,7 @@ private: public: EENotifyClass(SharedTermsDatabase& shared): d_sharedTerms(shared) {} bool eqNotifyTriggerEquality(TNode equality, bool value) { - Unreachable(); + d_sharedTerms.propagateEquality(equality, value); return true; } @@ -118,14 +89,12 @@ private: } bool eqNotifyTriggerTermEquality(theory::TheoryId tag, TNode t1, TNode t2, bool value) { - if (value) { - d_sharedTerms.mergeSharedTerms(t1, t2); - } - return true; + return d_sharedTerms.propagateSharedEquality(tag, t1, t2, value); } bool eqNotifyConstantTermMerge(TNode t1, TNode t2) { - return true; + d_sharedTerms.conflict(t1, t2, true); + return false; } }; @@ -135,24 +104,83 @@ private: /** Equality engine */ theory::eq::EqualityEngine d_equalityEngine; - /** Attach a new notify list to an equivalence class representative */ - NotifyList* getNewNotifyList(); + /** + * Method called by equalityEngine when a becomes (dis-)equal to b and a and b are shared with + * the theory. Returns false if there is a direct conflict (via rewrite for example). + */ + bool propagateSharedEquality(theory::TheoryId theory, TNode a, TNode b, bool value); + + /** + * Called from the equality engine when a trigger equality is deduced. + */ + bool propagateEquality(TNode equality, bool polarity); + + /** Theory engine */ + TheoryEngine* d_theoryEngine; + + /** Are we in conflict */ + context::CDO<bool> d_inConflict; + + /** Conflicting terms, if any */ + Node d_conflictLHS, d_conflictRHS; + + /** Polarity of the conflict */ + bool d_conflictPolarity; + + /** Called by the equality engine notify to mark the conflict */ + void conflict(TNode lhs, TNode rhs, bool polarity) { + if (!d_inConflict) { + // Only remember it if we're not already in conflict + d_inConflict = true; + d_conflictLHS = lhs; + d_conflictRHS = rhs; + d_conflictPolarity = polarity; + } + } - /** Method called by equalityEngine when a becomes equal to b */ - void mergeSharedTerms(TNode a, TNode b); + /** + * Should be called before any public non-const method in order to + * enqueue the conflict to the theory engine. + */ + void checkForConflict(); public: - SharedTermsDatabase(SharedTermsNotifyClass& notify, context::Context* context); + SharedTermsDatabase(TheoryEngine* theoryEngine, context::Context* context); ~SharedTermsDatabase() throw(AssertionException); /** + * Asserts the equality to the shared terms database, + */ + void assertEquality(TNode equality, bool polarity, TNode reason); + + /** + * Return whether the equality is alreday known to the engine + */ + bool isKnown(TNode literal) const; + + /** + * Returns an explanation of the propagation that came from the database. + */ + Node explain(TNode literal) const; + + /** + * Add an equality to propagate. + */ + void addEqualityToPropagate(TNode equality); + + /** * Add a shared term to the database. The shared term is a subterm of the atom and * should be associated with the given theory. */ void addSharedTerm(TNode atom, TNode term, theory::Theory::Set theories); /** + * Mark that the given theories have been notified of the given shared term. + */ + void markNotified(TNode term, theory::Theory::Set theories); + + /** * Returns true if the atom contains any shared terms, false otherwise. */ bool hasSharedTerms(TNode atom) const; @@ -176,26 +204,32 @@ public: * Get the theories that share the term and have been notified already. */ theory::Theory::Set getNotifiedTheories(TNode term) const; - - // Notify theory about a new equality between shared terms - void assertEq(TNode equality, theory::TheoryId theory); - + /** - * Mark that the given theories have been notified of the given shared term. + * Returns true if the term is currently registered as shared with some theory. */ - void markNotified(TNode term, theory::Theory::Set theories); - bool isShared(TNode term) const { - return d_alreadyNotifiedMap.find(term) != d_alreadyNotifiedMap.end(); + return term.isConst() || d_alreadyNotifiedMap.find(term) != d_alreadyNotifiedMap.end(); } - bool areEqual(TNode a, TNode b); - - bool areDisequal(TNode a, TNode b); + /** + * Returns true if the literal is an (dis-)equality with both sides registered as shared with + * some theory. + */ + bool isSharedEquality(TNode literal) const { + TNode atom = literal.getKind() == kind::NOT ? literal[0] : literal; + return atom.getKind() == kind::EQUAL && isShared(atom[0]) && isShared(atom[1]); + } - void processSharedLiteral(TNode literal, TNode reason); + /** + * Returns true if the shared terms a and b are known to be equal. + */ + bool areEqual(TNode a, TNode b) const; - Node explain(TNode literal); + /** + * Retursn true if the shared terms a and b are known to be dis-equal. + */ + bool areDisequal(TNode a, TNode b) const; protected: |