src/preprocessing/passes/non_clausal_simp.h

   1 /*********************                                                        */
   2 /*! \file non_clausal_simp.h
   3  ** \verbatim
   4  ** Top contributors (to current version):
   5  **   Andrew Reynolds, Aina Niemetz, Gereon Kremer
   6  ** This file is part of the CVC4 project.
   7  ** Copyright (c) 2009-2021 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 Non-clausal simplification preprocessing pass.
  13  **/
  14
  15 #include "cvc4_private.h"
  16
  17 #ifndef CVC4__PREPROCESSING__PASSES__NON_CLAUSAL_SIMP_H
  18 #define CVC4__PREPROCESSING__PASSES__NON_CLAUSAL_SIMP_H
  19
  20 #include "context/cdlist.h"
  21 #include "expr/node.h"
  22 #include "preprocessing/preprocessing_pass.h"
  23 #include "theory/trust_node.h"
  24
  25 namespace cvc5 {
  26
  27 class LazyCDProof;
  28 class ProofNodeManager;
  29
  30 namespace smt {
  31 class PreprocessProofGenerator;
  32 }
  33 namespace theory {
  34 class TrustSubstitutionMap;
  35 }
  36
  37 namespace preprocessing {
  38 namespace passes {
  39
  40 class NonClausalSimp : public PreprocessingPass
  41 {
  42  public:
  43   NonClausalSimp(PreprocessingPassContext* preprocContext);
  44
  45  protected:
  46   PreprocessingPassResult applyInternal(
  47       AssertionPipeline* assertionsToPreprocess) override;
  48
  49  private:
  50   struct Statistics
  51   {
  52     IntStat d_numConstantProps;
  53     Statistics();
  54     ~Statistics();
  55   };
  56
  57   Statistics d_statistics;
  58   /**
  59    * Transform learned literal lit. We apply substitutions in subs once and then
  60    * apply constant propagations cp to fixed point. Return the rewritten
  61    * form of lit.
  62    *
  63    * If proofs are enabled, then we require that the learned literal preprocess
  64    * proof generator (d_llpg) has a proof of lit when this method is called,
  65    * and ensure that the return literal also has a proof in d_llpg.
  66    */
  67   Node processLearnedLit(Node lit,
  68                          theory::TrustSubstitutionMap* subs,
  69                          theory::TrustSubstitutionMap* cp);
  70   /**
  71    * Process rewritten learned literal. This is called when we have a
  72    * learned literal lit that is rewritten to litr based on the proof generator
  73    * contained in trn (if it exists). The trust node trn should be of kind
  74    * REWRITE and proving (= lit litr).
  75    *
  76    * This tracks the proof in the learned literal preprocess proof generator
  77    * d_llpg below and returns the rewritten learned literal.
  78    */
  79   Node processRewrittenLearnedLit(theory::TrustNode trn);
  80   /** Is proof enabled? */
  81   bool isProofEnabled() const;
  82   /** The proof node manager */
  83   ProofNodeManager* d_pnm;
  84   /** the learned literal preprocess proof generator */
  85   std::unique_ptr<smt::PreprocessProofGenerator> d_llpg;
  86   /**
  87    * An lazy proof for learned literals that are reasserted into the assertions
  88    * pipeline by this class.
  89    */
  90   std::unique_ptr<LazyCDProof> d_llra;
  91   /**
  92    * A context-dependent list of trust substitution maps, which are required
  93    * for storing proofs.
  94    */
  95   context::CDList<std::shared_ptr<theory::TrustSubstitutionMap> > d_tsubsList;
  96 };
  97
  98 }  // namespace passes
  99 }  // namespace preprocessing
 100 }  // namespace cvc5
 101
 102 #endif