1 /*********************                                                        */
2 /*! \file preprocessing_pass.h
3  ** \verbatim
4  ** Top contributors (to current version):
5  **   Justin Xu
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 The preprocessing pass super class
13  **
14  ** Implementation of the preprocessing pass super class. Preprocessing passes
15  ** that inherit from this class, need to pass their name to the constructor to
16  ** register the pass appropriately. The core of a preprocessing pass lives
17  ** in applyInternal(), which operates on a list of assertions and is called
18  ** from apply() in the super class. The apply() method automatically takes
19  ** care of the following:
20  **
21  ** - Dumping assertions before and after the pass
22  ** - Initializing the timer
23  ** - Tracing and chatting
24  **
25  ** Optionally, preprocessing passes can overwrite the initInteral() method to
26  ** do work that only needs to be done once.
27  **/
28 
29 #include "cvc4_private.h"
30 
31 #ifndef __CVC4__PREPROCESSING__PREPROCESSING_PASS_H
32 #define __CVC4__PREPROCESSING__PREPROCESSING_PASS_H
33 
34 #include <string>
35 
36 #include "preprocessing/assertion_pipeline.h"
37 #include "preprocessing/preprocessing_pass_context.h"
38 #include "smt/smt_engine_scope.h"
39 #include "theory/logic_info.h"
40 
41 namespace CVC4 {
42 namespace preprocessing {
43 
44 /**
45  * Preprocessing passes return a result which indicates whether a conflict has
46  * been detected during preprocessing.
47  */
48 enum PreprocessingPassResult { CONFLICT, NO_CONFLICT };
49 
50 class PreprocessingPass {
51  public:
52   /* Preprocesses a list of assertions assertionsToPreprocess */
53   PreprocessingPassResult apply(AssertionPipeline* assertionsToPreprocess);
54 
55   PreprocessingPass(PreprocessingPassContext* preprocContext,
56                     const std::string& name);
57   virtual ~PreprocessingPass();
58 
59  protected:
60   /*
61    * Method for dumping assertions within a pass. Also called before and after
62    * applying the pass.
63    */
64   void dumpAssertions(const char* key, const AssertionPipeline& assertionList);
65 
66   /*
67    * Abstract method that each pass implements to do the actual preprocessing.
68    */
69   virtual PreprocessingPassResult applyInternal(
70       AssertionPipeline* assertionsToPreprocess) = 0;
71 
72   /* Context for Preprocessing Passes that initializes necessary variables */
73   PreprocessingPassContext* d_preprocContext;
74 
75  private:
76   /* Name of pass */
77   std::string d_name;
78   /* Timer for registering the preprocessing time of this pass */
79   TimerStat d_timer;
80 };
81 
82 }  // namespace preprocessing
83 }  // namespace CVC4
84 
85 #endif /* __CVC4__PREPROCESSING__PREPROCESSING_PASS_H */
86