src/preprocessing/passes/ite_simp.h

   1 /*********************                                                        */
   2 /*! \file ite_simp.h
   3  ** \verbatim
   4  ** Top contributors (to current version):
   5  **   Aina Niemetz, 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 ITE simplification preprocessing pass.
  13  **/
  14
  15 #include "cvc4_private.h"
  16
  17 #ifndef CVC4__PREPROCESSING__PASSES__ITE_SIMP_H
  18 #define CVC4__PREPROCESSING__PASSES__ITE_SIMP_H
  19
  20 #include "preprocessing/preprocessing_pass.h"
  21 #include "preprocessing/preprocessing_pass_context.h"
  22
  23 namespace CVC4 {
  24 namespace preprocessing {
  25 namespace passes {
  26
  27 class ITESimp : public PreprocessingPass
  28 {
  29  public:
  30    ITESimp(PreprocessingPassContext* preprocContext);
  31
  32  protected:
  33    PreprocessingPassResult applyInternal(
  34        AssertionPipeline* assertionsToPreprocess) override;
  35
  36  private:
  37   struct Statistics
  38   {
  39     IntStat d_arithSubstitutionsAdded;
  40     Statistics();
  41     ~Statistics();
  42   };
  43
  44   bool doneSimpITE(AssertionPipeline *assertionsToPreprocesss);
  45
  46   /** A collection of ite preprocessing passes. */
  47   util::ITEUtilities d_iteUtilities;
  48
  49   Statistics d_statistics;
  50 };
  51
  52 }  // namespace passes
  53 }  // namespace preprocessing
  54 }  // namespace CVC4
  55
  56 #endif