* Numerous documentation fixes (fix doxygen warnings, add missing documentation, etc.).

* Remove sat_module.cpp, which was no longer used (was previously refactored?)

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;