1 /*********************                                                        */
2 /*! \file ite_simp.h
3  ** \verbatim
4  ** Top contributors (to current version):
5  **   Aina Niemetz
6  ** This file is part of the CVC4 project.
7  ** Copyright (c) 2009-2019 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
57