fix numerous documentation issues; doxygen complains much less, now

6 files changed, 12 insertions, 12 deletions

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"