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 "smt/term_formula_removal.h"
  29 #include "theory/trust_node.h"
  30
  31 namespace CVC4 {
  32
  33 class LogicInfo;
  34 class TheoryEngine;
  35 class RemoveTermFormulas;
  36
  37 namespace theory {
  38
  39 /**
  40  * The preprocessor used in TheoryEngine.
  41  */
  42 class TheoryPreprocessor
  43 {
  44   typedef context::CDHashMap<Node, Node, NodeHashFunction> NodeMap;
  45
  46  public:
  47   /** Constructs a theory preprocessor */
  48   TheoryPreprocessor(TheoryEngine& engine,
  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 and returns the LEMMA trust 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  private:
  90   /**
  91    * Runs theory specific preprocessing (Theory::ppRewrite) on the non-Boolean
  92    * parts of the node.
  93    */
  94   TrustNode theoryPreprocess(TNode node);
  95   /** Reference to owning theory engine */
  96   TheoryEngine& d_engine;
  97   /** Logic info of theory engine */
  98   const LogicInfo& d_logicInfo;
  99   /** Cache for theory-preprocessing of assertions */
 100   NodeMap d_ppCache;
 101   /** The term formula remover */
 102   RemoveTermFormulas d_tfr;
 103   /** The term context, which computes hash values for term contexts. */
 104   InQuantTermContext d_iqtc;
 105   /**
 106    * A term conversion proof generator storing preprocessing and rewriting
 107    * steps.
 108    */
 109   std::unique_ptr<TConvProofGenerator> d_tpg;
 110   /**
 111    * A term conversion sequence generator, which applies theory preprocessing,
 112    * term formula removal, and rewriting in sequence.
 113    */
 114   std::unique_ptr<TConvSeqProofGenerator> d_tspg;
 115   /**
 116    * A term conversion proof generator storing rewriting steps, which is used
 117    * for calls to preprocess when doTheoryPreprocess is false. We store
 118    * (top-level) rewrite steps only. Notice this is intentionally separate
 119    * from d_tpg, which interleaves both preprocessing and rewriting.
 120    */
 121   std::unique_ptr<TConvProofGenerator> d_tpgRew;
 122   /**
 123    * A term conversion sequence generator, which applies term formula removal
 124    * and rewriting in sequence. This is used for reconstruct proofs of
 125    * calls to preprocess where doTheoryPreprocess is false.
 126    */
 127   std::unique_ptr<TConvSeqProofGenerator> d_tspgNoPp;
 128   /** A lazy proof, for additional lemmas. */
 129   std::unique_ptr<LazyCDProof> d_lp;
 130   /** Helper for theoryPreprocess */
 131   Node ppTheoryRewrite(TNode term);
 132   /**
 133    * Rewrite with proof, which stores a REWRITE step in d_tpg if necessary
 134    * and returns the rewritten form of term.
 135    */
 136   Node rewriteWithProof(Node term);
 137   /**
 138    * Preprocess with proof, which calls the appropriate ppRewrite method,
 139    * stores the corresponding rewrite step in d_tpg if necessary and returns
 140    * the preprocessed and rewritten form of term. It should be the case that
 141    * term is already in rewritten form.
 142    */
 143   Node preprocessWithProof(Node term);
 144   /** Proofs enabled */
 145   bool isProofEnabled() const;
 146 };
 147
 148 }  // namespace theory
 149 }  // namespace CVC4
 150
 151 #endif /* CVC4__THEORY__THEORY_PREPROCESSOR_H */