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

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

8 files changed, 19 insertions, 23 deletions

diff --git a/src/theory/bv/bitblast_strategies.cpp b/src/theory/bv/bitblast_strategies.cpp
index 8cfdab5af..80b689b8c 100644
--- a/src/theory/bv/bitblast_strategies.cpp
+++ b/src/theory/bv/bitblast_strategies.cpp
@@ -100,7 +100,7 @@ void inline makeZero(Bits& bits, unsigned width) {
  * 
  * @param a first term to be added
  * @param b second term to be added
- * @param sum the sum 
+ * @param res the result
  * @param carry the carry-in bit 
  * 
  * @return the carry-out
diff --git a/src/theory/bv/bitblast_strategies.h b/src/theory/bv/bitblast_strategies.h
index 826b61d4f..5b53678dd 100644
--- a/src/theory/bv/bitblast_strategies.h
+++ b/src/theory/bv/bitblast_strategies.h
@@ -41,7 +41,6 @@ typedef std::vector<Node>    Bits;
  * Default Atom Bitblasting strategies: 
  * 
  * @param node the atom to be bitblasted
- * @param markerLit the marker literal corresponding to the atom
  * @param bb the bitblaster
  */
 
@@ -68,9 +67,8 @@ Node SleBB(TNode node, Bitblaster* bb);
  * Default Term Bitblasting strategies
  * 
  * @param node the term to be bitblasted
+ * @param bits [output parameter] bits representing the new term 
  * @param bb the bitblaster in which the clauses are added
- * 
- * @return the bits representing the new term 
  */
 
 void UndefinedTermBBStrategy(TNode node, Bits& bits, Bitblaster* bb); 
diff --git a/src/theory/bv/bitblaster.cpp b/src/theory/bv/bitblaster.cpp
index c86f14398..eb5f3e155 100644
--- a/src/theory/bv/bitblaster.cpp
+++ b/src/theory/bv/bitblaster.cpp
@@ -170,7 +170,7 @@ void Bitblaster::explain(TNode atom, std::vector<TNode>& explanation) {
 /** 
  * Asserts the clauses corresponding to the atom to the Sat Solver
  * by turning on the marker literal (i.e. setting it to false)
- * @param node the atom to be aserted
+ * @param node the atom to be asserted
  * 
  */
  
diff --git a/src/theory/instantiator_tables_template.cpp b/src/theory/instantiator_tables_template.cpp
index 7a78c3aae..7234993fa 100644
--- a/src/theory/instantiator_tables_template.cpp
+++ b/src/theory/instantiator_tables_template.cpp
@@ -1,5 +1,5 @@
 /*********************                                                        */
-/*! \file instantiator_tables_template.cpp
+/*! \file instantiator_tables.cpp
  ** \verbatim
  ** Original author: mdeters
  ** Major contributors: none
diff --git a/src/theory/rewriter_tables_template.h b/src/theory/rewriter_tables_template.h
index 9ab98168e..6533e9335 100644
--- a/src/theory/rewriter_tables_template.h
+++ b/src/theory/rewriter_tables_template.h
@@ -1,5 +1,5 @@
 /*********************                                                        */
-/*! \file rewriter_tables_template.h
+/*! \file rewriter_tables.h
  ** \verbatim
  ** Original author: dejan
  ** Major contributors: mdeters
diff --git a/src/theory/theory_traits_template.h b/src/theory/theory_traits_template.h
index bbf13b425..4522af568 100644
--- a/src/theory/theory_traits_template.h
+++ b/src/theory/theory_traits_template.h
@@ -1,5 +1,5 @@
 /*********************                                                        */
-/*! \file theory_traits_template.h
+/*! \file theory_traits.h
  ** \verbatim
  ** Original author: dejan
  ** Major contributors: mdeters
@@ -27,7 +27,6 @@
 ${theory_includes}
 
 namespace CVC4 {
-
 namespace theory {
 
 template <TheoryId theoryId>
@@ -37,5 +36,5 @@ ${theory_traits}
 
 ${theory_for_each_macro}
 
-}/* theory namespace */
+}/* CVC4::theory namespace */
 }/* CVC4 namespace */
diff --git a/src/theory/type_enumerator_template.cpp b/src/theory/type_enumerator_template.cpp
index 426bf52a0..0619a900f 100644
--- a/src/theory/type_enumerator_template.cpp
+++ b/src/theory/type_enumerator_template.cpp
@@ -1,5 +1,5 @@
 /*********************                                                        */
-/*! \file type_enumerator_template.cpp
+/*! \file type_enumerator.cpp
  ** \verbatim
  ** Original author: mdeters
  ** Major contributors: none
@@ -58,4 +58,3 @@ ${mk_type_enumerator_cases}
 
 }/* CVC4::theory namespace */
 }/* CVC4 namespace */
-
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;