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/lazy_proof.h"
  23 #include "expr/node.h"
  24 #include "expr/term_conversion_proof_generator.h"
  25 #include "theory/trust_node.h"
  26
  27 namespace CVC4 {
  28
  29 class LogicInfo;
  30 class TheoryEngine;
  31 class RemoveTermFormulas;
  32
  33 namespace theory {
  34
  35 /**
  36  * The preprocessor used in TheoryEngine.
  37  */
  38 class TheoryPreprocessor
  39 {
  40   typedef std::unordered_map<Node, Node, NodeHashFunction> NodeMap;
  41
  42  public:
  43   /** Constructs a theory preprocessor */
  44   TheoryPreprocessor(TheoryEngine& engine,
  45                      RemoveTermFormulas& tfr,
  46                      ProofNodeManager* pnm = nullptr);
  47   /** Destroys a theory preprocessor */
  48   ~TheoryPreprocessor();
  49   /** Clear the cache of this class */
  50   void clearCache();
  51   /**
  52    * Preprocesses the given assertion node. It returns a TrustNode of kind
  53    * TrustNodeKind::REWRITE indicating the preprocessed form of node. It stores
  54    * additional lemmas in newLemmas, which are trust nodes of kind
  55    * TrustNodeKind::LEMMA. These correspond to e.g. lemmas corresponding to ITE
  56    * removal. For each lemma in newLemmas, we add the corresponding skolem that
  57    * the lemma defines. The flag doTheoryPreprocess is whether we should run
  58    * theory-specific preprocessing.
  59    *
  60    * @param node The assertion to preprocess,
  61    * @param newLemmas The lemmas to add to the set of assertions,
  62    * @param newSkolems The skolems that newLemmas correspond to,
  63    * @param doTheoryPreprocess whether to run theory-specific preprocessing.
  64    * @return The trust node corresponding to rewriting node via preprocessing.
  65    */
  66   TrustNode preprocess(TNode node,
  67                        std::vector<TrustNode>& newLemmas,
  68                        std::vector<Node>& newSkolems,
  69                        bool doTheoryPreprocess);
  70   /**
  71    * Runs theory specific preprocessing on the non-Boolean parts of
  72    * the formula.  This is only called on input assertions, after ITEs
  73    * have been removed.
  74    */
  75   TrustNode theoryPreprocess(TNode node);
  76
  77  private:
  78   /** Reference to owning theory engine */
  79   TheoryEngine& d_engine;
  80   /** Logic info of theory engine */
  81   const LogicInfo& d_logicInfo;
  82   /** Cache for theory-preprocessing of assertions */
  83   NodeMap d_ppCache;
  84   /** The term formula remover */
  85   RemoveTermFormulas& d_tfr;
  86   /** The context for the proof generator below */
  87   context::Context d_pfContext;
  88   /** A term conversion proof generator */
  89   std::unique_ptr<TConvProofGenerator> d_tpg;
  90   /** A lazy proof, for additional lemmas. */
  91   std::unique_ptr<LazyCDProof> d_lp;
  92   /** Helper for theoryPreprocess */
  93   Node ppTheoryRewrite(TNode term);
  94   /**
  95    * Rewrite with proof, which stores a REWRITE step in d_tpg if necessary
  96    * and returns the rewritten form of term.
  97    */
  98   Node rewriteWithProof(Node term);
  99   /**
 100    * Preprocess with proof, which calls the appropriate ppRewrite method,
 101    * stores the corresponding rewrite step in d_tpg if necessary and returns
 102    * the preprocessed and rewritten form of term. It should be the case that
 103    * term is already in rewritten form.
 104    */
 105   Node preprocessWithProof(Node term);
 106   /** Proofs enabled */
 107   bool isProofEnabled() const;
 108 };
 109
 110 }  // namespace theory
 111 }  // namespace CVC4
 112
 113 #endif /* CVC4__THEORY__THEORY_PREPROCESSOR_H */