1 files changed, 0 insertions, 109 deletions
diff --git a/src/preprocessing/passes/symmetry_breaker.h b/src/preprocessing/passes/symmetry_breaker.h
deleted file mode 100644
index 6bb10ebb8..000000000
--- a/src/preprocessing/passes/symmetry_breaker.h
+++ /dev/null
@@ -1,109 +0,0 @@
-/*********************                                                        */
-/*! \file symmetry_breaker.h
- ** \verbatim
- ** Top contributors (to current version):
- **   Paul Meng, Andrew Reynolds
- ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2019 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 Symmetry breaker for theories
- **/
-
-#ifndef CVC4__PREPROCESSING__PASSES__SYMMETRY_BREAKER_H_
-#define CVC4__PREPROCESSING__PASSES__SYMMETRY_BREAKER_H_
-
-#include <map>
-#include <string>
-#include <vector>
-#include "expr/node.h"
-
-#include "preprocessing/preprocessing_pass.h"
-#include "preprocessing/preprocessing_pass_context.h"
-
-namespace CVC4 {
-namespace preprocessing {
-namespace passes {
-
-/**
- * Given a vector of partitions {{v_{11}, ... , v_{1n}}, {v_{m1}, ... , v_{mk}}},
- * the symmetry breaker will generate symmetry breaking constraints for each
- * partition {v_{i1}, ... , v_{ij}} depending on the type of variables
- * in each partition.
- *
- * For a partition of integer, real and bit-vectors variables {v1, ..., vn},
- * we generate ordered constraints: {v1 <= v2, ..., v{n-1} <= vn}.
- * For a partition of variables of other types {v1, ..., vn}, we generate
- * the following two kinds of constraints.
- *
- * 1. Consecutive constraints ensure that equivalence classes over v_1...v_n are
- *    in consecutive segments
- *    v_i = v_j => v_i = v_{j-1} for all 0 <= i < j-1 < j < n
- * 2. Length order constraints ensure that the length of segments occur in
- *    descending order
- *    v_i = v_j => (v_{i} = v_{i-1} OR v_{i-1} = x_{(i-1)-(j-i)})
- *    for all 1 <= i < j < part.size() and (i-1)-(j-i) >= 0
- * */
-
-class SymmetryBreaker
-{
- public:
-  /**
-   * Constructor
-   * */
-  SymmetryBreaker()
-  {
-    d_trueNode = NodeManager::currentNM()->mkConst<bool>(true);
-    d_falseNode = NodeManager::currentNM()->mkConst<bool>(false);
-  }
-
-  /**
-   * Destructor
-   * */
-  ~SymmetryBreaker() {}
-
-  /**
-   * This is to generate symmetry breaking constraints for partitions in parts.
-   * Since parts are symmetries of the original assertions C,
-   * the symmetry breaking constraints SB for parts returned by this function
-   * conjuncted with the original assertions SB ^ C is equisatisfiable to C.
-   * */
-  Node generateSymBkConstraints(const std::vector<std::vector<Node> >& parts);
-
- private:
-
-  /** True and false constant nodes */
-  Node d_trueNode;
-  Node d_falseNode;
-
-  /**
-   * Get the order kind depending on the type of node.
-   * For example, if node is a integer or real, this function would return
-   * the operator less than or equal to (<=) so that we can use it to build
-   * ordered constraints.
-   * */
-  Kind getOrderKind(Node node);
-};
-
-/**
- * This class detects symmetries in the input assertions in the form of a
- * partition (see symmetry_detect.h), and subsequently adds symmetry breaking
- * constraints that correspond to this partition, using the above class.
- */
-class SymBreakerPass : public PreprocessingPass
-{
- public:
-  SymBreakerPass(PreprocessingPassContext* preprocContext);
-
- protected:
-  PreprocessingPassResult applyInternal(
-      AssertionPipeline* assertionsToPreprocess) override;
-};
-
-}  // namespace passes
-}  // namespace preprocessing
-}  // namespace CVC4
-
-#endif /* CVC4__PREPROCESSING__PASSES__SYMMETRY_BREAKER_H_ */