diff options
author | Morgan Deters <mdeters@gmail.com> | 2011-09-16 20:53:00 +0000 |
---|---|---|
committer | Morgan Deters <mdeters@gmail.com> | 2011-09-16 20:53:00 +0000 |
commit | 55820808b55999c27ee1a66df0e674318302d5a6 (patch) | |
tree | 58a9b59e7216d7f39c8b72b9e92b7441389d7742 /src/theory | |
parent | 6df0b6f2ac842b0407232fcee72ff68b7e9deee5 (diff) |
fix numerous documentation issues; doxygen complains much less, now
Diffstat (limited to 'src/theory')
-rw-r--r-- | src/theory/arith/arith_utilities.h | 6 | ||||
-rw-r--r-- | src/theory/arith/normal_form.h | 2 | ||||
-rw-r--r-- | src/theory/arith/tableau.h | 2 | ||||
-rw-r--r-- | src/theory/theory_engine.cpp | 2 | ||||
-rw-r--r-- | src/theory/uf/symmetry_breaker.cpp | 6 | ||||
-rw-r--r-- | src/theory/uf/symmetry_breaker.h | 6 |
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" |