1 /********************* */
2 /*! \file theory_eq_notify.h
4 ** Top contributors (to current version):
5 ** Andrew Reynolds, Mathias Preiner, Tim King
6 ** This file is part of the CVC4 project.
7 ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
8 ** in the top-level source directory and their institutional affiliations.
9 ** All rights reserved. See the file COPYING in the top-level source
10 ** directory for licensing information.\endverbatim
12 ** \brief The theory equality notify utility.
15 #include "cvc4_private.h"
17 #ifndef CVC4__THEORY__THEORY_EQ_NOTIFY_H
18 #define CVC4__THEORY__THEORY_EQ_NOTIFY_H
20 #include "expr/node.h"
21 #include "theory/theory_inference_manager.h"
22 #include "theory/uf/equality_engine_notify.h"
28 * The default class for equality engine callbacks for a theory. This forwards
29 * calls for trigger predicates, trigger term equalities and conflicts due to
30 * constant merges to the provided theory inference manager.
32 class TheoryEqNotifyClass
: public eq::EqualityEngineNotify
35 TheoryEqNotifyClass(TheoryInferenceManager
& im
) : d_im(im
) {}
36 ~TheoryEqNotifyClass() {}
38 bool eqNotifyTriggerPredicate(TNode predicate
, bool value
) override
42 return d_im
.propagateLit(predicate
);
44 return d_im
.propagateLit(predicate
.notNode());
46 bool eqNotifyTriggerTermEquality(TheoryId tag
,
53 return d_im
.propagateLit(t1
.eqNode(t2
));
55 return d_im
.propagateLit(t1
.eqNode(t2
).notNode());
57 void eqNotifyConstantTermMerge(TNode t1
, TNode t2
) override
59 d_im
.conflictEqConstantMerge(t1
, t2
);
61 void eqNotifyNewClass(TNode t
) override
65 void eqNotifyMerge(TNode t1
, TNode t2
) override
69 void eqNotifyDisequal(TNode t1
, TNode t2
, TNode reason
) override
75 /** Reference to the theory inference manager */
76 TheoryInferenceManager
& d_im
;