diff options
author | Dejan Jovanović <dejan.jovanovic@gmail.com> | 2012-06-07 07:11:24 +0000 |
---|---|---|
committer | Dejan Jovanović <dejan.jovanovic@gmail.com> | 2012-06-07 07:11:24 +0000 |
commit | 49dd14da8d872403b4d772a2d49224e4d6bda227 (patch) | |
tree | 5abbd246c8a1bb797e97d4b9754a4f850e1dc1b5 /src/theory/uf/equality_engine.h | |
parent | 67903280f8fe6946a36ef9fc08bfc747f74bfbd7 (diff) |
fixing some bugs in propagation of disequalities
still doesnt fix the wrong answers thought :(
Diffstat (limited to 'src/theory/uf/equality_engine.h')
-rw-r--r-- | src/theory/uf/equality_engine.h | 42 |
1 files changed, 41 insertions, 1 deletions
diff --git a/src/theory/uf/equality_engine.h b/src/theory/uf/equality_engine.h index f40c79df3..5935ddc1f 100644 --- a/src/theory/uf/equality_engine.h +++ b/src/theory/uf/equality_engine.h @@ -520,8 +520,48 @@ private: */ std::vector<EqualityPair> d_deducedDisequalityReasons; - + /** + * Stores a propagated disequality for explanation purpooses and remembers the reasons. + */ bool storePropagatedDisequality(TNode lhs, TNode rhs, unsigned reasonsCount) const; + + /** + * An equality tagged with a set of tags. + */ + struct TaggedEquality { + /** Id of the equality */ + EqualityNodeId equalityId; + /** TriggerSet reference for the class of one of the sides */ + TriggerTermSetRef triggerSetRef; + /** Is trigger equivalent to the lhs (rhs otherwise) */ + bool lhs; + + TaggedEquality(EqualityNodeId equalityId = null_id, TriggerTermSetRef triggerSetRef = null_set_id, bool lhs = true) + : equalityId(equalityId), triggerSetRef(triggerSetRef), lhs(lhs) {} + }; + + /** A map from equivalence class id's to tagged equalities */ + typedef std::vector<TaggedEquality> TaggedEqualitiesSet; + + /** + * Returns a set of equalities that have been asserted false where one side of the equality + * belongs to the given equivalence class. The equalities are restricted to the ones where + * one side of the equality is in the tags set, but the other one isn't. Each returned + * dis-equality is associated with the tags that are the subset of the input tags, such that + * exactly one side of the equality is not in the set yet. + * + * @param classId the equivalence class to search + * @param inputTags the tags to filter the equalities + * @param out the output equalities, as described above + */ + void getDisequalities(bool allowConstants, EqualityNodeId classId, Theory::Set inputTags, TaggedEqualitiesSet& out); + + /** + * Propagates the remembered disequalities with given tags the original triggers for those tags, + * and the set of disequalities produced by above. + */ + bool propagateTriggerTermDisequalities(Theory::Set tags, + TriggerTermSetRef triggerSetRef, const TaggedEqualitiesSet& disequalitiesToNotify); public: |