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 "context/cdhashmap.h"
  23 #include "context/context.h"
  24 #include "expr/lazy_proof.h"
  25 #include "expr/node.h"
  26 #include "expr/tconv_seq_proof_generator.h"
  27 #include "expr/term_conversion_proof_generator.h"
  28 #include "theory/trust_node.h"
  29
  30 namespace CVC4 {
  31
  32 class LogicInfo;
  33 class TheoryEngine;
  34 class RemoveTermFormulas;
  35
  36 namespace theory {
  37
  38 /**
  39  * The preprocessor used in TheoryEngine.
  40  */
  41 class TheoryPreprocessor
  42 {
  43   typedef context::CDHashMap<Node, Node, NodeHashFunction> NodeMap;
  44
  45  public:
  46   /** Constructs a theory preprocessor */
  47   TheoryPreprocessor(TheoryEngine& engine,
  48                      RemoveTermFormulas& tfr,
  49                      context::UserContext* userContext,
  50                      ProofNodeManager* pnm = nullptr);
  51   /** Destroys a theory preprocessor */
  52   ~TheoryPreprocessor();
  53   /**
  54    * Preprocesses the given assertion node. It returns a TrustNode of kind
  55    * TrustNodeKind::REWRITE indicating the preprocessed form of node. It stores
  56    * additional lemmas in newLemmas, which are trust nodes of kind
  57    * TrustNodeKind::LEMMA. These correspond to e.g. lemmas corresponding to ITE
  58    * removal. For each lemma in newLemmas, we add the corresponding skolem that
  59    * the lemma defines. The flag doTheoryPreprocess is whether we should run
  60    * theory-specific preprocessing.
  61    *
  62    * @param node The assertion to preprocess,
  63    * @param newLemmas The lemmas to add to the set of assertions,
  64    * @param newSkolems The skolems that newLemmas correspond to,
  65    * @param doTheoryPreprocess whether to run theory-specific preprocessing.
  66    * @return The (REWRITE) trust node corresponding to rewritten node via
  67    * preprocessing.
  68    */
  69   TrustNode preprocess(TNode node,
  70                        std::vector<TrustNode>& newLemmas,
  71                        std::vector<Node>& newSkolems,
  72                        bool doTheoryPreprocess);
  73   /**
  74    * Same as above, but transforms the proof of node into a proof of the
  75    * preprocessed node.
  76    *
  77    * @param node The assertion to preprocess,
  78    * @param newLemmas The lemmas to add to the set of assertions,
  79    * @param newSkolems The skolems that newLemmas correspond to,
  80    * @param doTheoryPreprocess whether to run theory-specific preprocessing.
  81    * @return The (LEMMA) trust node corresponding to the proof of the rewritten
  82    * form of the proven field of node.
  83    */
  84   TrustNode preprocessLemma(TrustNode node,
  85                             std::vector<TrustNode>& newLemmas,
  86                             std::vector<Node>& newSkolems,
  87                             bool doTheoryPreprocess);
  88   /**
  89    * Runs theory specific preprocessing on the non-Boolean parts of
  90    * the formula.  This is only called on input assertions, after ITEs
  91    * have been removed.
  92    */
  93   TrustNode theoryPreprocess(TNode node);
  94
  95  private:
  96   /** Reference to owning theory engine */
  97   TheoryEngine& d_engine;
  98   /** Logic info of theory engine */
  99   const LogicInfo& d_logicInfo;
 100   /** Cache for theory-preprocessing of assertions */
 101   NodeMap d_ppCache;
 102   /** The term formula remover */
 103   RemoveTermFormulas& d_tfr;
 104   /** The term context, which computes hash values for term contexts. */
 105   InQuantTermContext d_iqtc;
 106   /**
 107    * A term conversion proof generator storing preprocessing and rewriting
 108    * steps.
 109    */
 110   std::unique_ptr<TConvProofGenerator> d_tpg;
 111   /**
 112    * A term conversion sequence generator, which applies theory preprocessing,
 113    * term formula removal, and rewriting in sequence.
 114    */
 115   std::unique_ptr<TConvSeqProofGenerator> d_tspg;
 116   /**
 117    * A term conversion proof generator storing rewriting steps, which is used
 118    * for calls to preprocess when doTheoryPreprocess is false. We store
 119    * (top-level) rewrite steps only. Notice this is intentionally separate
 120    * from d_tpg, which interleaves both preprocessing and rewriting.
 121    */
 122   std::unique_ptr<TConvProofGenerator> d_tpgRew;
 123   /**
 124    * A term conversion sequence generator, which applies term formula removal
 125    * and rewriting in sequence. This is used for reconstruct proofs of
 126    * calls to preprocess where doTheoryPreprocess is false.
 127    */
 128   std::unique_ptr<TConvSeqProofGenerator> d_tspgNoPp;
 129   /** A lazy proof, for additional lemmas. */
 130   std::unique_ptr<LazyCDProof> d_lp;
 131   /** Helper for theoryPreprocess */
 132   Node ppTheoryRewrite(TNode term);
 133   /**
 134    * Rewrite with proof, which stores a REWRITE step in d_tpg if necessary
 135    * and returns the rewritten form of term.
 136    */
 137   Node rewriteWithProof(Node term);
 138   /**
 139    * Preprocess with proof, which calls the appropriate ppRewrite method,
 140    * stores the corresponding rewrite step in d_tpg if necessary and returns
 141    * the preprocessed and rewritten form of term. It should be the case that
 142    * term is already in rewritten form.
 143    */
 144   Node preprocessWithProof(Node term);
 145   /** Proofs enabled */
 146   bool isProofEnabled() const;
 147 };
 148
 149 }  // namespace theory
 150 }  // namespace CVC4
 151
 152 #endif /* CVC4__THEORY__THEORY_PREPROCESSOR_H */