src/preprocessing/assertion_pipeline.h

   1 /*********************                                                        */
   2 /*! \file assertion_pipeline.h
   3  ** \verbatim
   4  ** Top contributors (to current version):
   5  **   Andres Noetzli, Andrew Reynolds, Justin Xu
   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 AssertionPipeline stores a list of assertions modified by
  13  ** preprocessing passes
  14  **/
  15
  16 #include "cvc4_private.h"
  17
  18 #ifndef CVC4__PREPROCESSING__ASSERTION_PIPELINE_H
  19 #define CVC4__PREPROCESSING__ASSERTION_PIPELINE_H
  20
  21 #include <vector>
  22
  23 #include "expr/node.h"
  24 #include "expr/proof_generator.h"
  25 #include "expr/proof_node_manager.h"
  26 #include "smt/preprocess_proof_generator.h"
  27 #include "smt/term_formula_removal.h"
  28 #include "theory/trust_node.h"
  29
  30 namespace CVC4 {
  31 namespace preprocessing {
  32
  33 /**
  34  * Assertion Pipeline stores a list of assertions modified by preprocessing
  35  * passes. It is assumed that all assertions after d_realAssertionsEnd were
  36  * generated by ITE removal. Hence, d_iteSkolemMap maps into only these.
  37  */
  38 class AssertionPipeline
  39 {
  40  public:
  41   AssertionPipeline();
  42
  43   size_t size() const { return d_nodes.size(); }
  44
  45   void resize(size_t n) { d_nodes.resize(n); }
  46
  47   /**
  48    * Clear the list of assertions and assumptions.
  49    */
  50   void clear();
  51
  52   const Node& operator[](size_t i) const { return d_nodes[i]; }
  53
  54   /**
  55    * Adds an assertion/assumption to be preprocessed.
  56    *
  57    * @param n The assertion/assumption
  58    * @param isAssumption If true, records that \p n is an assumption. Note that
  59    * all assumptions have to be added contiguously.
  60    * @param isInput If true, n is an input formula (an assumption in the main
  61    * body of the overall proof).
  62    * @param pg The proof generator who can provide a proof of n. The proof
  63    * generator is not required and is ignored if isInput is true.
  64    */
  65   void push_back(Node n,
  66                  bool isAssumption = false,
  67                  bool isInput = false,
  68                  ProofGenerator* pg = nullptr);
  69   /** Same as above, with TrustNode */
  70   void pushBackTrusted(theory::TrustNode trn);
  71
  72   /**
  73    * Get the constant reference to the underlying assertions. It is only
  74    * possible to modify these via the replace methods below.
  75    */
  76   const std::vector<Node>& ref() const { return d_nodes; }
  77
  78   std::vector<Node>::const_iterator begin() const { return d_nodes.cbegin(); }
  79   std::vector<Node>::const_iterator end() const { return d_nodes.cend(); }
  80
  81   /*
  82    * Replaces assertion i with node n and records the dependency between the
  83    * original assertion and its replacement.
  84    *
  85    * @param i The position of the assertion to replace.
  86    * @param n The replacement assertion.
  87    * @param pg The proof generator who can provide a proof of d_nodes[i] == n,
  88    * where d_nodes[i] is the assertion at position i prior to this call.
  89    */
  90   void replace(size_t i, Node n, ProofGenerator* pg = nullptr);
  91   /** Same as above, with TrustNode */
  92   void replaceTrusted(size_t i, theory::TrustNode trn);
  93
  94   IteSkolemMap& getIteSkolemMap() { return d_iteSkolemMap; }
  95   const IteSkolemMap& getIteSkolemMap() const { return d_iteSkolemMap; }
  96
  97   size_t getRealAssertionsEnd() const { return d_realAssertionsEnd; }
  98
  99   /** @return The index of the first assumption */
 100   size_t getAssumptionsStart() const { return d_assumptionsStart; }
 101
 102   /** @return The number of assumptions */
 103   size_t getNumAssumptions() const { return d_numAssumptions; }
 104
 105   void updateRealAssertionsEnd() { d_realAssertionsEnd = d_nodes.size(); }
 106
 107   /**
 108    * Returns true if substitutions must be stored as assertions. This is for
 109    * example the case when we do incremental solving.
 110    */
 111   bool storeSubstsInAsserts() { return d_storeSubstsInAsserts; }
 112
 113   /**
 114    * Enables storing substitutions as assertions.
 115    */
 116   void enableStoreSubstsInAsserts();
 117
 118   /**
 119    * Disables storing substitutions as assertions.
 120    */
 121   void disableStoreSubstsInAsserts();
 122
 123   /**
 124    * Adds a substitution node of the form (= lhs rhs) to the assertions.
 125    * This conjoins n to assertions at a distinguished index given by
 126    * d_substsIndex.
 127    *
 128    * @param n The substitution node
 129    * @param pg The proof generator that can provide a proof of n.
 130    */
 131   void addSubstitutionNode(Node n, ProofGenerator* pg = nullptr);
 132
 133   /**
 134    * Conjoin n to the assertion vector at position i. This replaces
 135    * d_nodes[i] with the rewritten form of (AND d_nodes[i] n).
 136    *
 137    * @param i The assertion to replace
 138    * @param n The formula to conjoin at position i
 139    * @param pg The proof generator that can provide a proof of n
 140    */
 141   void conjoin(size_t i, Node n, ProofGenerator* pg = nullptr);
 142
 143   /**
 144    * Checks whether the assertion at a given index represents substitutions.
 145    *
 146    * @param i The index in question
 147    */
 148   bool isSubstsIndex(size_t i)
 149   {
 150     return d_storeSubstsInAsserts && i == d_substsIndex;
 151   }
 152   //------------------------------------ for proofs
 153   /** Set proof generator */
 154   void setProofGenerator(smt::PreprocessProofGenerator* pppg);
 155   /** Is proof enabled? */
 156   bool isProofEnabled() const;
 157   //------------------------------------ end for proofs
 158  private:
 159   /** The list of current assertions */
 160   std::vector<Node> d_nodes;
 161
 162   /**
 163    * Map from skolem variables to index in d_assertions containing
 164    * corresponding introduced Boolean ite
 165    */
 166   IteSkolemMap d_iteSkolemMap;
 167
 168   /** Size of d_nodes when preprocessing starts */
 169   size_t d_realAssertionsEnd;
 170
 171   /**
 172    * If true, we store the substitutions as assertions. This is necessary when
 173    * doing incremental solving because we cannot apply them to existing
 174    * assertions while preprocessing new assertions.
 175    */
 176   bool d_storeSubstsInAsserts;
 177
 178   /**
 179    * The index of the assertions that holds the substitutions.
 180    *
 181    * TODO(#2473): replace by separate vector of substitution assertions.
 182    */
 183   size_t d_substsIndex;
 184
 185   /** Index of the first assumption */
 186   size_t d_assumptionsStart;
 187   /** The number of assumptions */
 188   size_t d_numAssumptions;
 189   /** The proof generator, if one is provided */
 190   smt::PreprocessProofGenerator* d_pppg;
 191 }; /* class AssertionPipeline */
 192
 193 }  // namespace preprocessing
 194 }  // namespace CVC4
 195
 196 #endif /* CVC4__PREPROCESSING__ASSERTION_PIPELINE_H */