src/smt/preprocessor.h

   1 /*********************                                                        */
   2 /*! \file preprocessor.h
   3  ** \verbatim
   4  ** Top contributors (to current version):
   5  **   Andrew Reynolds
   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, context::UserContext* u, AbstractValues& abs);
  45   ~Preprocessor();
  46   /**
  47    * Finish initialization
  48    */
  49   void finishInit();
  50   /**
  51    * Process the assertions that have been asserted in argument as. Returns
  52    * true if no conflict was discovered while preprocessing them.
  53    */
  54   bool process(Assertions& as);
  55   /**
  56    * Postprocess assertions, called after the SmtEngine has finished
  57    * giving the assertions to the SMT solver and before the assertions are
  58    * cleared.
  59    */
  60   void postprocess(Assertions& as);
  61   /**
  62    * Clear learned literals from the Boolean propagator.
  63    */
  64   void clearLearnedLiterals();
  65   /**
  66    * Cleanup, which deletes the processing passes owned by this module. This
  67    * is required to be done explicitly so that passes are deleted before the
  68    * objects they refer to in the SmtEngine destructor.
  69    */
  70   void cleanup();
  71   /**
  72    * Simplify a formula without doing "much" work.  Does not involve
  73    * the SAT Engine in the simplification, but uses the current
  74    * definitions, assertions, and the current partial model, if one
  75    * has been constructed.  It also involves theory normalization.
  76    *
  77    * @param n The node to simplify
  78    * @param removeItes Whether to remove ITE (and other terms with formulas in
  79    * term positions) from the result.
  80    * @return The simplified term.
  81    */
  82   Node simplify(const Node& n, bool removeItes = false);
  83   /**
  84    * Expand the definitions in a term or formula n.  No other
  85    * simplification or normalization is done.
  86    *
  87    * @param n The node to expand
  88    * @param expandOnly if true, then the expandDefinitions function of
  89    * TheoryEngine is not called on subterms of n.
  90    * @return The expanded term.
  91    */
  92   Node expandDefinitions(const Node& n, bool expandOnly = false);
  93   /** Same as above, with a cache of previous results. */
  94   Node expandDefinitions(
  95       const Node& n,
  96       std::unordered_map<Node, Node, NodeHashFunction>& cache,
  97       bool expandOnly = false);
  98   /**
  99    * Get the underlying term formula remover utility.
 100    */
 101   RemoveTermFormulas& getTermFormulaRemover();
 102
 103  private:
 104   /**
 105    * Apply substitutions that have been inferred by preprocessing, return the
 106    * substituted form of node.
 107    */
 108   Node applySubstitutions(TNode node);
 109   /** Reference to the parent SmtEngine */
 110   SmtEngine& d_smt;
 111   /** Reference to the abstract values utility */
 112   AbstractValues& d_absValues;
 113   /**
 114    * A circuit propagator for non-clausal propositional deduction.
 115    */
 116   theory::booleans::CircuitPropagator d_propagator;
 117   /**
 118    * User-context-dependent flag of whether any assertions have been processed.
 119    */
 120   context::CDO<bool> d_assertionsProcessed;
 121   /** The preprocessing pass context */
 122   std::unique_ptr<preprocessing::PreprocessingPassContext> d_ppContext;
 123   /**
 124    * Process assertions module, responsible for implementing the preprocessing
 125    * passes.
 126    */
 127   ProcessAssertions d_processor;
 128   /**
 129    * The term formula remover, responsible for eliminating formulas that occur
 130    * in term contexts.
 131    */
 132   RemoveTermFormulas d_rtf;
 133 };
 134
 135 }  // namespace smt
 136 }  // namespace CVC4
 137
 138 #endif