src/preprocessing/passes/bv_abstraction.h

   1 /*********************                                                        */
   2 /*! \file bv_abstraction.h
   3  ** \verbatim
   4  ** Top contributors (to current version):
   5  **   Mathias Preiner
   6  ** This file is part of the CVC4 project.
   7  ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
   8  ** in the top-level source directory) and their institutional affiliations.
   9  ** All rights reserved.  See the file COPYING in the top-level source
  10  ** directory for licensing information.\endverbatim
  11  **
  12  ** \brief The BvAbstraction preprocessing pass
  13  **
  14  ** Abstract common structures over small domains to UF. This preprocessing
  15  ** is particularly useful on QF_BV/mcm benchmarks and can be enabled via
  16  ** option `--bv-abstraction`.
  17  ** For more information see 3.4 Refactoring Isomorphic Circuits in [1].
  18  **
  19  ** [1] Liana Hadarean, An Efficient and Trustworthy Theory Solver for
  20  **     Bit-vectors in Satisfiability Modulo Theories
  21  **     https://cs.nyu.edu/media/publications/hadarean_liana.pdf
  22  **/
  23
  24 #include "cvc4_private.h"
  25
  26 #ifndef CVC4__PREPROCESSING__PASSES__BV_ABSTRACTION_H
  27 #define CVC4__PREPROCESSING__PASSES__BV_ABSTRACTION_H
  28
  29 #include "preprocessing/preprocessing_pass.h"
  30 #include "preprocessing/preprocessing_pass_context.h"
  31
  32 namespace CVC4 {
  33 namespace preprocessing {
  34 namespace passes {
  35
  36 class BvAbstraction : public PreprocessingPass
  37 {
  38  public:
  39   BvAbstraction(PreprocessingPassContext* preprocContext);
  40
  41  protected:
  42   PreprocessingPassResult applyInternal(
  43       AssertionPipeline* assertionsToPreprocess) override;
  44 };
  45
  46 }  // namespace passes
  47 }  // namespace preprocessing
  48 }  // namespace CVC4
  49
  50 #endif /* CVC4__PREPROCESSING__PASSES__BV_ABSTRACTION_H */