src/smt/preprocessor.h

   1 /*********************                                                        */
   2 /*! \file preprocessor.h
   3  ** \verbatim
   4  ** Top contributors (to current version):
   5  **   Andrew Reynolds, Morgan Deters, Haniel Barbosa
   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 preprocessor of the SmtEngine.
  13  **/
  14
  15 #include "cvc4_private.h"
  16
  17 #ifndef CVC4__SMT__PREPROCESSOR_H
  18 #define CVC4__SMT__PREPROCESSOR_H
  19
  20 #include <vector>
  21
  22 #include "preprocessing/preprocessing_pass_context.h"
  23 #include "smt/process_assertions.h"
  24 #include "smt/term_formula_removal.h"
  25 #include "theory/booleans/circuit_propagator.h"
  26
  27 namespace CVC4 {
  28 namespace smt {
  29
  30 class AbstractValues;
  31
  32 /**
  33  * The preprocessor module of an SMT engine.
  34  *
  35  * This class is responsible for:
  36  * (1) preprocessing the set of assertions from input before they are sent to
  37  * the SMT solver,
  38  * (2) implementing methods for expanding and simplifying formulas. The latter
  39  * takes into account the substitutions inferred by this class.
  40  */
  41 class Preprocessor
  42 {
  43  public:
  44   Preprocessor(SmtEngine& smt,
  45                context::UserContext* u,
  46                AbstractValues& abs,
  47                SmtEngineStatistics& stats);
  48   ~Preprocessor();
  49   /**
  50    * Finish initialization
  51    */
  52   void finishInit();
  53   /**
  54    * Process the assertions that have been asserted in argument as. Returns
  55    * true if no conflict was discovered while preprocessing them.
  56    */
  57   bool process(Assertions& as);
  58   /**
  59    * Postprocess assertions, called after the SmtEngine has finished
  60    * giving the assertions to the SMT solver and before the assertions are
  61    * cleared.
  62    */
  63   void postprocess(Assertions& as);
  64   /**
  65    * Clear learned literals from the Boolean propagator.
  66    */
  67   void clearLearnedLiterals();
  68   /**
  69    * Cleanup, which deletes the processing passes owned by this module. This
  70    * is required to be done explicitly so that passes are deleted before the
  71    * objects they refer to in the SmtEngine destructor.
  72    */
  73   void cleanup();
  74   /**
  75    * Simplify a formula without doing "much" work.  Does not involve
  76    * the SAT Engine in the simplification, but uses the current
  77    * definitions, assertions, and the current partial model, if one
  78    * has been constructed.  It also involves theory normalization.
  79    *
  80    * @param n The node to simplify
  81    * @param removeItes Whether to remove ITE (and other terms with formulas in
  82    * term positions) from the result.
  83    * @return The simplified term.
  84    */
  85   Node simplify(const Node& n, bool removeItes = false);
  86   /**
  87    * Expand the definitions in a term or formula n.  No other
  88    * simplification or normalization is done.
  89    *
  90    * @param n The node to expand
  91    * @param expandOnly if true, then the expandDefinitions function of
  92    * TheoryEngine is not called on subterms of n.
  93    * @return The expanded term.
  94    */
  95   Node expandDefinitions(const Node& n, bool expandOnly = false);
  96   /** Same as above, with a cache of previous results. */
  97   Node expandDefinitions(
  98       const Node& n,
  99       std::unordered_map<Node, Node, NodeHashFunction>& cache,
 100       bool expandOnly = false);
 101   /**
 102    * Get the underlying term formula remover utility.
 103    */
 104   RemoveTermFormulas& getTermFormulaRemover();
 105
 106   /**
 107    * Set proof node manager. Enables proofs in this preprocessor.
 108    */
 109   void setProofGenerator(PreprocessProofGenerator* pppg);
 110
 111  private:
 112   /** A copy of the current context */
 113   context::Context* d_context;
 114   /** Reference to the parent SmtEngine */
 115   SmtEngine& d_smt;
 116   /** Reference to the abstract values utility */
 117   AbstractValues& d_absValues;
 118   /**
 119    * A circuit propagator for non-clausal propositional deduction.
 120    */
 121   theory::booleans::CircuitPropagator d_propagator;
 122   /**
 123    * User-context-dependent flag of whether any assertions have been processed.
 124    */
 125   context::CDO<bool> d_assertionsProcessed;
 126   /** The preprocessing pass context */
 127   std::unique_ptr<preprocessing::PreprocessingPassContext> d_ppContext;
 128   /**
 129    * Process assertions module, responsible for implementing the preprocessing
 130    * passes.
 131    */
 132   ProcessAssertions d_processor;
 133   /**
 134    * The term formula remover, responsible for eliminating formulas that occur
 135    * in term contexts.
 136    */
 137   RemoveTermFormulas d_rtf;
 138   /** Proof node manager */
 139   ProofNodeManager* d_pnm;
 140 };
 141
 142 }  // namespace smt
 143 }  // namespace CVC4
 144
 145 #endif