src/theory/theory_preprocessor.h

   1 /*********************                                                        */
   2 /*! \file theory_preprocessor.h
   3  ** \verbatim
   4  ** Top contributors (to current version):
   5  **   Andrew Reynolds, Morgan Deters, Dejan Jovanovic
   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 theory preprocessor.
  13  **/
  14
  15 #include "cvc4_private.h"
  16
  17 #ifndef CVC4__THEORY__THEORY_PREPROCESSOR_H
  18 #define CVC4__THEORY__THEORY_PREPROCESSOR_H
  19
  20 #include <unordered_map>
  21
  22 #include "expr/node.h"
  23 #include "preprocessing/assertion_pipeline.h"
  24
  25 namespace CVC4 {
  26
  27 class LogicInfo;
  28 class TheoryEngine;
  29 class RemoveTermFormulas;
  30 class LazyCDProof;
  31
  32 namespace theory {
  33
  34 /**
  35  * The preprocessor used in TheoryEngine.
  36  */
  37 class TheoryPreprocessor
  38 {
  39   typedef std::unordered_map<Node, Node, NodeHashFunction> NodeMap;
  40
  41  public:
  42   /** Constructs a theory preprocessor */
  43   TheoryPreprocessor(TheoryEngine& engine, RemoveTermFormulas& tfr);
  44   /** Destroys a theory preprocessor */
  45   ~TheoryPreprocessor();
  46   /** Clear the cache of this class */
  47   void clearCache();
  48   /**
  49    * Preprocesses node and stores it along with lemmas generated by
  50    * preprocessing into the assertion pipeline lemmas. The (optional) argument
  51    * lcp is the proof that stores a proof of all top-level formulas in lemmas,
  52    * assuming that lcp initially contains a proof of node. The flag
  53    * doTheoryPreprocess is whether we should run theory-specific preprocessing.
  54    */
  55   void preprocess(TNode node,
  56                   preprocessing::AssertionPipeline& lemmas,
  57                   bool doTheoryPreprocess);
  58   /**
  59    * Runs theory specific preprocessing on the non-Boolean parts of
  60    * the formula.  This is only called on input assertions, after ITEs
  61    * have been removed.
  62    */
  63   Node theoryPreprocess(TNode node);
  64
  65  private:
  66   /** Reference to owning theory engine */
  67   TheoryEngine& d_engine;
  68   /** Logic info of theory engine */
  69   const LogicInfo& d_logicInfo;
  70   /** Cache for theory-preprocessing of assertions */
  71   NodeMap d_ppCache;
  72   /** The term formula remover */
  73   RemoveTermFormulas& d_tfr;
  74   /** Helper for theoryPreprocess */
  75   Node ppTheoryRewrite(TNode term);
  76 };
  77
  78 }  // namespace theory
  79 }  // namespace CVC4
  80
  81 #endif /* CVC4__THEORY__THEORY_PREPROCESSOR_H */