diff options
author | Morgan Deters <mdeters@gmail.com> | 2011-09-16 21:32:37 +0000 |
---|---|---|
committer | Morgan Deters <mdeters@gmail.com> | 2011-09-16 21:32:37 +0000 |
commit | a7488622a5c3120899c6c6c6e6546fc706040312 (patch) | |
tree | bd33620169c1938a4c59fd812bef13ec277277ba /src/theory/uf | |
parent | c229389dbf99fa7a747a1bb713e41a3081b6d5fa (diff) |
fix up more documentation
Diffstat (limited to 'src/theory/uf')
-rw-r--r-- | src/theory/uf/symmetry_breaker.cpp | 32 | ||||
-rw-r--r-- | src/theory/uf/symmetry_breaker.h | 32 |
2 files changed, 32 insertions, 32 deletions
diff --git a/src/theory/uf/symmetry_breaker.cpp b/src/theory/uf/symmetry_breaker.cpp index cebabe23c..1855aa59b 100644 --- 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 76005ff03..ddbd50cbb 100644 --- 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" |