src/preprocessing/passes/unconstrained_simplifier.h

   1 /*********************                                                        */
   2 /*! \file unconstrained_simplifier.h
   3  ** \verbatim
   4  ** Top contributors (to current version):
   5  **   Clark Barrett, Andres Noetzli, 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 Simplifications based on unconstrained variables
  13  **
  14  ** This module implements a preprocessing phase which replaces certain
  15  ** "unconstrained" expressions by variables.  Based on Roberto
  16  ** Bruttomesso's PhD thesis.
  17  **/
  18
  19 #include "cvc4_private.h"
  20
  21 #ifndef CVC4__PREPROCESSING_PASSES_UNCONSTRAINED_SIMPLIFIER_H
  22 #define CVC4__PREPROCESSING_PASSES_UNCONSTRAINED_SIMPLIFIER_H
  23
  24 #include <unordered_map>
  25 #include <unordered_set>
  26 #include <vector>
  27
  28 #include "context/context.h"
  29 #include "expr/node.h"
  30 #include "preprocessing/preprocessing_pass.h"
  31 #include "preprocessing/preprocessing_pass_context.h"
  32 #include "theory/logic_info.h"
  33 #include "theory/substitutions.h"
  34 #include "util/statistics_registry.h"
  35
  36 namespace CVC4 {
  37 namespace preprocessing {
  38 namespace passes {
  39
  40 class UnconstrainedSimplifier : public PreprocessingPass
  41 {
  42  public:
  43   UnconstrainedSimplifier(PreprocessingPassContext* preprocContext);
  44   ~UnconstrainedSimplifier() override;
  45
  46   PreprocessingPassResult applyInternal(
  47       AssertionPipeline* assertionsToPreprocess) override;
  48
  49  private:
  50   /** number of expressions eliminated due to unconstrained simplification */
  51   IntStat d_numUnconstrainedElim;
  52
  53   using TNodeCountMap = std::unordered_map<TNode, unsigned, TNodeHashFunction>;
  54   using TNodeMap = std::unordered_map<TNode, TNode, TNodeHashFunction>;
  55   using TNodeSet = std::unordered_set<TNode, TNodeHashFunction>;
  56
  57   TNodeCountMap d_visited;
  58   TNodeMap d_visitedOnce;
  59   TNodeSet d_unconstrained;
  60
  61   context::Context* d_context;
  62   theory::SubstitutionMap d_substitutions;
  63
  64   /**
  65    * Visit all subterms in assertion. This method throws a LogicException if
  66    * there is a subterm that is unhandled by this preprocessing pass (e.g. a
  67    * quantified formula).
  68    */
  69   void visitAll(TNode assertion);
  70   Node newUnconstrainedVar(TypeNode t, TNode var);
  71   void processUnconstrained();
  72 };
  73
  74 }  // namespace passes
  75 }  // namespace preprocessing
  76 }  // namespace CVC4
  77
  78 #endif