diff options
Diffstat (limited to 'src/theory/uf')
| -rw-r--r-- | src/theory/uf/equality_engine.h | 22 |
1 files changed, 11 insertions, 11 deletions
diff --git a/src/theory/uf/equality_engine.h b/src/theory/uf/equality_engine.h index 7f216d634..1e3b276a4 100644 --- a/src/theory/uf/equality_engine.h +++ b/src/theory/uf/equality_engine.h @@ -58,7 +58,7 @@ public: /** * Notifies about a trigger equality that became true or false. * - * @param eq the equality that became true or false + * @param equality the equality that became true or false * @param value the value of the equality */ virtual bool eqNotifyTriggerEquality(TNode equality, bool value) = 0; @@ -680,13 +680,13 @@ public: /** * Adds a predicate p with given polarity. The predicate asserted - * should be in the congruence closure kinds (otherwise it's + * should be in the congruence closure kinds (otherwise it's * useless. * * @param p the (non-negated) predicate - * @param polarity true if asserting the predicate, false if + * @param polarity true if asserting the predicate, false if * asserting the negated predicate - * @param the reason to keep for building explanations + * @param reason the reason to keep for building explanations */ void assertPredicate(TNode p, bool polarity, TNode reason); @@ -694,9 +694,9 @@ public: * Adds an equality eq with the given polarity to the database. * * @param eq the (non-negated) equality - * @param polarity true if asserting the equality, false if + * @param polarity true if asserting the equality, false if * asserting the negated equality - * @param the reason to keep for building explanations + * @param reason the reason to keep for building explanations */ void assertEquality(TNode eq, bool polarity, TNode reason); @@ -706,20 +706,20 @@ public: TNode getRepresentative(TNode t) const; /** - * Add all the terms where the given term appears as a first child + * Add all the terms where the given term appears as a first child * (directly or implicitly). */ void getUseListTerms(TNode t, std::set<TNode>& output); /** - * Get an explanation of the equality t1 = t2 begin true of false. + * Get an explanation of the equality t1 = t2 begin true of false. * Returns the reasons (added when asserting) that imply it * in the assertions vector. */ void explainEquality(TNode t1, TNode t2, bool polarity, std::vector<TNode>& assertions) const; /** - * Get an explanation of the predicate being true or false. + * Get an explanation of the predicate being true or false. * Returns the reasons (added when asserting) that imply imply it * in the assertions vector. */ @@ -733,12 +733,12 @@ public: * it's own notification. * * @param t the trigger term - * @param tag tag for this trigger (do NOT use THEORY_LAST) + * @param theoryTag tag for this trigger (do NOT use THEORY_LAST) */ void addTriggerTerm(TNode t, TheoryId theoryTag); /** - * Returns true if t is a trigger term or in the same equivalence + * Returns true if t is a trigger term or in the same equivalence * class as some other trigger term. */ bool isTriggerTerm(TNode t, TheoryId theoryTag) const; |