fix numerous documentation issues; doxygen complains much less, now

diff --git a/src/expr/attribute_internals.h b/src/expr/attribute_internals.h
index 1df8da63ec88802e982c8bcbca0d36e73d21b375..b359b166612d0c1d7f08915782c1f5e009a6eaeb 100644 (file)
--- 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 af7067130df1b086adaff7be29a0486c03c62f12..bb8ed86e16a55a7387c4f50ab640e7b118dbe252 100644 (file)
--- 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 3a1135f74bcbde7a2f9651c3f0b1387f7711f09b..838285f426abd6e686f96d5b562d3c82f47e9bbd 100644 (file)
--- 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 6e2d706ccf1be662c4d2bd8b77c6fcfa750cb40d..a182bc3b0c6cfce4cd83ad8ae28efdb70d1ce6de 100644 (file)
--- 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 3da3d68a58a8d970fd94ecd638ab27a3342c69e0..f143b36c4f516db2789368990adba0224eaeceda 100644 (file)
--- 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 d5ac8ddbbf0751381e4fbcad18a02b1ccb421918..5bb71532c9c809911de2ee3cf3ef407fe11847c0 100644 (file)
--- 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 1c2e8cd0dfa06229853f3f892be8366fb14b76f9..cebabe23c0f93d5c564f3764e319d8d521ea8b58 100644 (file)
--- 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 1b2680cf3cf15b5446e68ad5de14f7dd803f328e..76005ff03a5a05ff79b38db292135096bf8332ff 100644 (file)
--- 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 2d269e801dd2cff1bc632f13e1db102bedb9b2bf..32ceff26b94c2c0db889241a147b8ece256685fa 100644 (file)
--- 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.
    */