diff options
Diffstat (limited to 'src/theory/uf/theory_uf.h')
-rw-r--r-- | src/theory/uf/theory_uf.h | 56 |
1 files changed, 38 insertions, 18 deletions
diff --git a/src/theory/uf/theory_uf.h b/src/theory/uf/theory_uf.h index 6956390f5..9017928b7 100644 --- a/src/theory/uf/theory_uf.h +++ b/src/theory/uf/theory_uf.h @@ -39,21 +39,46 @@ namespace uf { class TheoryUF : public Theory { public: - class NotifyClass { + class NotifyClass : public eq::EqualityEngineNotify { TheoryUF& d_uf; public: NotifyClass(TheoryUF& uf): d_uf(uf) {} - bool notify(TNode propagation) { - Debug("uf") << "NotifyClass::notify(" << propagation << ")" << std::endl; - // Just forward to uf - return d_uf.propagate(propagation); + bool eqNotifyTriggerEquality(TNode equality, bool value) { + Debug("uf") << "NotifyClass::eqNotifyTriggerEquality(" << equality << ", " << (value ? "true" : "false" )<< ")" << std::endl; + if (value) { + return d_uf.propagate(equality); + } else { + // We use only literal triggers so taking not is safe + return d_uf.propagate(equality.notNode()); + } } - - void notify(TNode t1, TNode t2) { - Debug("uf") << "NotifyClass::notify(" << t1 << ", " << t2 << ")" << std::endl; - Node equality = Rewriter::rewriteEquality(theory::THEORY_UF, t1.eqNode(t2)); - d_uf.propagate(equality); + + bool eqNotifyTriggerPredicate(TNode predicate, bool value) { + Debug("uf") << "NotifyClass::eqNotifyTriggerPredicate(" << predicate << ", " << (value ? "true" : "false" )<< ")" << std::endl; + if (value) { + return d_uf.propagate(predicate); + } else { + return d_uf.propagate(predicate.notNode()); + } + } + + bool eqNotifyTriggerTermEquality(TNode t1, TNode t2, bool value) { + Debug("uf") << "NotifyClass::eqNotifyTriggerTermMerge(" << t1 << ", " << t2 << std::endl; + if (value) { + return d_uf.propagate(t1.eqNode(t2)); + } else { + return d_uf.propagate(t1.eqNode(t2).notNode()); + } + } + + bool eqNotifyConstantTermMerge(TNode t1, TNode t2) { + Debug("uf") << "NotifyClass::eqNotifyConstantTermMerge(" << t1 << ", " << t2 << std::endl; + if (Theory::theoryOf(t1) == THEORY_BOOL) { + return d_uf.propagate(t1.iffNode(t2)); + } else { + return d_uf.propagate(t1.eqNode(t2)); + } } }; @@ -63,7 +88,7 @@ private: NotifyClass d_notify; /** Equaltity engine */ - EqualityEngine<NotifyClass> d_equalityEngine; + eq::EqualityEngine d_equalityEngine; /** Are we in conflict */ context::CDO<bool> d_conflict; @@ -72,7 +97,8 @@ private: Node d_conflictNode; /** - * Should be called to propagate the literal. + * Should be called to propagate the literal. We use a node here + * since some of the propagated literals are not kept anywhere. */ bool propagate(TNode literal); @@ -90,12 +116,6 @@ private: /** All the function terms that the theory has seen */ context::CDList<TNode> d_functionsTerms; - /** True node for predicates = true */ - Node d_true; - - /** True node for predicates = false */ - Node d_false; - /** Symmetry analyzer */ SymmetryBreaker d_symb; |