diff options
Diffstat (limited to 'src/theory/uf/symmetry_breaker.h')
-rw-r--r-- | src/theory/uf/symmetry_breaker.h | 78 |
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" |