fix numerous documentation issues; doxygen complains much less, now

9 files changed, 15 insertions, 17 deletions

diff --git a/src/expr/attribute_internals.h b/src/expr/attribute_internals.h
index 1df8da63e..b359b1666 100644
--- a/src/expr/attribute_internals.h
+++ b/src/expr/attribute_internals.h
@@ -69,7 +69,7 @@ namespace attr {
  * convert "attribute value types" into "table value types" and back
  * again.
  *
- * Each instantiation <T> is expected to have three members:
+ * Each instantiation < T > is expected to have three members:
  *
  *   typename table_value_type
  *
diff --git a/src/prop/prop_engine.h b/src/prop/prop_engine.h
index af7067130..bb8ed86e1 100644
--- a/src/prop/prop_engine.h
+++ b/src/prop/prop_engine.h
@@ -98,6 +98,8 @@ public:
    * than the (SAT and SMT) level at which it was asserted.
    *
    * @param node the formula to assert
+   * @param negated whether the node should be considered to be negated at the top level (or not)
+   * @param removable whether this lemma can be quietly removed based on an activity heuristic (or not)
    */
   void assertLemma(TNode node, bool negated, bool removable);
 
diff --git a/src/theory/arith/arith_utilities.h b/src/theory/arith/arith_utilities.h
index 3a1135f74..838285f42 100644
--- a/src/theory/arith/arith_utilities.h
+++ b/src/theory/arith/arith_utilities.h
@@ -89,7 +89,7 @@ inline Node coerceToRationalNode(TNode constant){
 
 
 
-/** is k \in {LT, LEQ, EQ, GEQ, GT} */
+/** \f$ k \in {LT, LEQ, EQ, GEQ, GT} \f$ */
 inline bool isRelationOperator(Kind k){
   using namespace kind;
 
@@ -145,8 +145,8 @@ inline bool evaluateConstantPredicate(Kind k, const Rational& left, const Ration
 /**
  * Returns the appropriate coefficient for the infinitesimal given the kind
  * for an arithmetic atom inorder to represent strict inequalities as inequalities.
- *   x < c  becomes  x <= c + (-1) * \delta
- *   x > c  becomes  x >= x + ( 1) * \delta
+ *   x < c  becomes  x <= c + (-1) * \f$ \delta \f$
+ *   x > c  becomes  x >= x + ( 1) * \f$ \delta \f$
  * Non-strict inequalities have a coefficient of zero.
  */
 inline int deltaCoeff(Kind k){
diff --git a/src/theory/arith/normal_form.h b/src/theory/arith/normal_form.h
index 6e2d706cc..a182bc3b0 100644
--- a/src/theory/arith/normal_form.h
+++ b/src/theory/arith/normal_form.h
@@ -62,7 +62,7 @@ namespace arith {
  *
  * monomial := constant | var_list | (* constant' var_list')
  *   where
- *     constant' \not\in {0,1}
+ *     \f$ constant' \not\in {0,1} \f$
  *
  * polynomial := monomial' | (+ [monomial])
  *   where
diff --git a/src/theory/arith/tableau.h b/src/theory/arith/tableau.h
index 3da3d68a5..f143b36c4 100644
--- a/src/theory/arith/tableau.h
+++ b/src/theory/arith/tableau.h
@@ -314,7 +314,7 @@ public:
   /**
    * Adds a row to the tableau.
    * The new row is equivalent to:
-   *   basicVar = \sum_i coeffs[i] * variables[i]
+   *   basicVar = \f$\sum_i\f$ coeffs[i] * variables[i]
    * preconditions:
    *   basicVar is already declared to be basic
    *   basicVar does not have a row associated with it in the tableau.
diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp
index d5ac8ddbb..5bb71532c 100644
--- a/src/theory/theory_engine.cpp
+++ b/src/theory/theory_engine.cpp
@@ -491,7 +491,7 @@ void TheoryEngine::assertFact(TNode node)
   }
 }
 
-void TheoryEngine::propagate(TNode literal, TheoryId theory) {
+void TheoryEngine::propagate(TNode literal, theory::TheoryId theory) {
       
   Debug("theory") << "EngineOutputChannel::propagate(" << literal << ")" << std::endl;
       
diff --git a/src/theory/uf/symmetry_breaker.cpp b/src/theory/uf/symmetry_breaker.cpp
index 1c2e8cd0d..cebabe23c 100644
--- a/src/theory/uf/symmetry_breaker.cpp
+++ b/src/theory/uf/symmetry_breaker.cpp
@@ -19,13 +19,13 @@
  **
  ** From the paper:
  **
- ** <pre>
+ ** <pre>\f[
  **   P := guess_permutations(phi)
  **   foreach {c_0, ..., c_n} \in P do
  **     if invariant_by_permutations(phi, {c_0, ..., c_n}) then
  **       T := select_terms(phi, {c_0, ..., c_n})
  **       cts := \empty
- **       while T != \empty && |cts| <= n do
+ **       while T != \empty \land |cts| <= n do
  **         t := select_most_promising_term(T, phi)
  **         T := T \ {t}
  **         cts := cts \cup used_in(t, {c_0, ..., c_n})
@@ -38,7 +38,7 @@
  **     end
  **   end
  **   return phi
- ** </pre>
+ ** \f]</pre>
  **/
 
 #include "theory/uf/symmetry_breaker.h"
diff --git a/src/theory/uf/symmetry_breaker.h b/src/theory/uf/symmetry_breaker.h
index 1b2680cf3..76005ff03 100644
--- a/src/theory/uf/symmetry_breaker.h
+++ b/src/theory/uf/symmetry_breaker.h
@@ -19,13 +19,13 @@
  **
  ** From the paper:
  **
- ** <pre>
+ ** <pre>\f[
  **   P := guess_permutations(phi)
  **   foreach {c_0, ..., c_n} \in P do
  **     if invariant_by_permutations(phi, {c_0, ..., c_n}) then
  **       T := select_terms(phi, {c_0, ..., c_n})
  **       cts := \empty
- **       while T != \empty && |cts| <= n do
+ **       while T != \empty \land |cts| <= n do
  **         t := select_most_promising_term(T, phi)
  **         T := T \ {t}
  **         cts := cts \cup used_in(t, {c_0, ..., c_n})
@@ -38,7 +38,7 @@
  **     end
  **   end
  **   return phi
- ** </pre>
+ ** \f]</pre>
  **/
 
 #include "cvc4_private.h"
diff --git a/src/util/propositional_query.h b/src/util/propositional_query.h
index 2d269e801..32ceff26b 100644
--- a/src/util/propositional_query.h
+++ b/src/util/propositional_query.h
@@ -41,8 +41,6 @@ public:
    * Returns whether a node q is propositionally satisfiable.
    *
    * @param q Node to be checked for satisfiability.
-   * @param e A number representing the effort to use between 0 (minimum effort),
-   *  and 1 (maximum effort).
    * @pre q is a ground formula.
    * @pre effort is between 0 and 1.
    */
@@ -52,8 +50,6 @@ public:
    * Returns whether a node q is a propositional tautology.
    *
    * @param q Node to be checked for satisfiability.
-   * @param e A number representing the effort to use between 0 (minimum effort),
-   *  and 1 (maximum effort).
    * @pre q is a ground formula.
    * @pre effort is between 0 and 1.
    */