1 files changed, 38 insertions, 40 deletions
diff --git a/src/theory/uf/symmetry_breaker.h b/src/theory/uf/symmetry_breaker.h
index 169794f3d..f2dd9c5f1 100644
--- a/src/theory/uf/symmetry_breaker.h
+++ b/src/theory/uf/symmetry_breaker.h
@@ -1,43 +1,41 @@
-/*********************                                                        */
-/*! \file symmetry_breaker.h
- ** \verbatim
- ** Top contributors (to current version):
- **   Morgan Deters, Liana Hadarean, Tim King
- ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
- ** in the top-level source directory and their institutional affiliations.
- ** All rights reserved.  See the file COPYING in the top-level source
- ** directory for licensing information.\endverbatim
- **
- ** \brief Implementation of algorithm suggested by Deharbe, Fontaine,
- ** Merz, and Paleo, "Exploiting symmetry in SMT problems," CADE 2011
- **
- ** Implementation of algorithm suggested by Deharbe, Fontaine, Merz,
- ** and Paleo, "Exploiting symmetry in SMT problems," CADE 2011.
- **
- ** From the paper:
- **
- ** <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$ \emptyset \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 \f$ \phi \f$
- ** </pre>
- **/
+/******************************************************************************
+ * Top contributors (to current version):
+ *   Morgan Deters, Liana Hadarean, Tim King
+ *
+ * This file is part of the cvc5 project.
+ *
+ * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
+ * in the top-level source directory and their institutional affiliations.
+ * All rights reserved.  See the file COPYING in the top-level source
+ * directory for licensing information.
+ * ****************************************************************************
+ *
+ * Implementation of algorithm suggested by Deharbe, Fontaine, Merz,
+ * and Paleo, "Exploiting symmetry in SMT problems," CADE 2011.
+ *
+ * From the paper:
+ *
+ * <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$ \emptyset \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 \f$ \phi \f$
+ * </pre>
+ */
 
 #include "cvc4_private.h"