fix up more documentation

diff --git a/src/theory/uf/symmetry_breaker.cpp b/src/theory/uf/symmetry_breaker.cpp
index cebabe23c0f93d5c564f3764e319d8d521ea8b58..1855aa59bdfae1164a89656543de876f6ca8fb20 100644 (file)
--- a/src/theory/uf/symmetry_breaker.cpp
+++ b/src/theory/uf/symmetry_breaker.cpp
@@ -19,26 +19,26 @@
  **
  ** From the paper:
  **
- ** <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 \land |cts| <= n do
- **         t := select_most_promising_term(T, phi)
- **         T := T \ {t}
- **         cts := cts \cup used_in(t, {c_0, ..., c_n})
- **         let c \in {c_0, ..., c_n} \ cts
- **         cts := cts \cup {c}
- **         if cts != {c_0, ..., c_n} then
- **           phi := phi /\ ( \vee_{c_i \in cts} t = c_i )
+ ** <pre>
+ **   \f$ P := guess\_permutations(\phi) \f$
+ **   foreach \f$ {c_0, ..., c_n} \in P \f$ do
+ **     if \f$ invariant\_by\_permutations(\phi, {c_0, ..., c_n}) \f$ then
+ **       T := \f$ select\_terms(\phi, {c_0, ..., c_n}) \f$
+ **       cts := \f$ \empty \f$
+ **       while T != \f$ \empty \wedge |cts| <= n \f$ do
+ **         \f$ t := select\_most\_promising\_term(T, \phi) \f$
+ **         \f$ T := T \setminus {t} \f$
+ **         cts := cts \f$ \cup used\_in(t, {c_0, ..., c_n}) \f$
+ **         let \f$ c \in {c_0, ..., c_n} \setminus cts \f$
+ **         cts := cts \f$ \cup {c} \f$
+ **         if cts != \f$ {c_0, ..., c_n} \f$ then
+ **           \f$ \phi := \phi \wedge ( \vee_{c_i \in cts} t = c_i ) \f$
  **         end
  **       end
  **     end
  **   end
- **   return phi
- ** \f]</pre>
+ **   return \f$ \phi \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 76005ff03a5a05ff79b38db292135096bf8332ff..ddbd50cbbaa46ae8fa1aa49c40682196f9b70950 100644 (file)
--- a/src/theory/uf/symmetry_breaker.h
+++ b/src/theory/uf/symmetry_breaker.h
@@ -19,26 +19,26 @@
  **
  ** From the paper:
  **
- ** <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 \land |cts| <= n do
- **         t := select_most_promising_term(T, phi)
- **         T := T \ {t}
- **         cts := cts \cup used_in(t, {c_0, ..., c_n})
- **         let c \in {c_0, ..., c_n} \ cts
- **         cts := cts \cup {c}
- **         if cts != {c_0, ..., c_n} then
- **           phi := phi /\ ( \vee_{c_i \in cts} t = c_i )
+ ** <pre>
+ **   \f$ P := guess\_permutations(\phi) \f$
+ **   foreach \f$ {c_0, ..., c_n} \in P \f$ do
+ **     if \f$ invariant\_by\_permutations(\phi, {c_0, ..., c_n}) \f$ then
+ **       T := \f$ select\_terms(\phi, {c_0, ..., c_n}) \f$
+ **       cts := \f$ \empty \f$
+ **       while T != \f$ \empty \wedge |cts| <= n \f$ do
+ **         \f$ t := select\_most\_promising\_term(T, \phi) \f$
+ **         \f$ T := T \setminus {t} \f$
+ **         cts := cts \f$ \cup used\_in(t, {c_0, ..., c_n}) \f$
+ **         let \f$ c \in {c_0, ..., c_n} \setminus cts \f$
+ **         cts := cts \f$ \cup {c} \f$
+ **         if cts != \f$ {c_0, ..., c_n} \f$ then
+ **           \f$ \phi := \phi \wedge ( \vee_{c_i \in cts} t = c_i ) \f$
  **         end
  **       end
  **     end
  **   end
- **   return phi
- ** \f]</pre>
+ **   return \f$ \phi \f$
+ ** </pre>
  **/
 
 #include "cvc4_private.h"