src/preprocessing/passes/pseudo_boolean_processor.h

   1 /*********************                                                        */
   2 /*! \file pseudo_boolean_processor.h
   3  ** \verbatim
   4  ** Top contributors (to current version):
   5  **   Tim King, Andres Noetzli
   6  ** This file is part of the CVC4 project.
   7  ** Copyright (c) 2009-2019 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 [[ Add one-line brief description here ]]
  13  **
  14  ** [[ Add lengthier description here ]]
  15  ** \todo document this file
  16  **/
  17
  18 #include "cvc4_private.h"
  19
  20 #ifndef CVC4__PREPROCESSING__PASSES__PSEUDO_BOOLEAN_PROCESSOR_H
  21 #define CVC4__PREPROCESSING__PASSES__PSEUDO_BOOLEAN_PROCESSOR_H
  22
  23 #include <unordered_set>
  24 #include <vector>
  25
  26 #include "context/cdhashmap.h"
  27 #include "context/cdo.h"
  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/substitutions.h"
  33 #include "util/maybe.h"
  34 #include "util/rational.h"
  35
  36 namespace CVC4 {
  37 namespace preprocessing {
  38 namespace passes {
  39
  40 class PseudoBooleanProcessor : public PreprocessingPass
  41 {
  42  public:
  43   PseudoBooleanProcessor(PreprocessingPassContext* preprocContext);
  44
  45  protected:
  46   PreprocessingPassResult applyInternal(
  47       AssertionPipeline* assertionsToPreprocess) override;
  48
  49  private:
  50   /** Assumes that the assertions have been rewritten. */
  51   void learn(const std::vector<Node>& assertions);
  52
  53   /** Assumes that the assertions have been rewritten. */
  54   void applyReplacements(AssertionPipeline* assertionsToPreprocess);
  55
  56   bool likelyToHelp() const;
  57
  58   bool isPseudoBoolean(Node v) const;
  59
  60   // Adds the fact the that integert typed variable v
  61   //   must be >= 0 to the context.
  62   // This is explained by the explanation exp.
  63   // exp cannot be null.
  64   void addGeqZero(Node v, Node exp);
  65
  66   // Adds the fact the that integert typed variable v
  67   //   must be <= 1 to the context.
  68   // This is explained by the explanation exp.
  69   // exp cannot be null.
  70   void addLeqOne(Node v, Node exp);
  71
  72   static inline bool isIntVar(Node v)
  73   {
  74     return v.isVar() && v.getType().isInteger();
  75   }
  76
  77   void clear();
  78
  79   /** Assumes that the assertion has been rewritten. */
  80   void learn(Node assertion);
  81
  82   /** Rewrites a node  */
  83   Node applyReplacements(Node pre);
  84
  85   void learnInternal(Node assertion, bool negated, Node orig);
  86   void learnRewrittenGeq(Node assertion, bool negated, Node orig);
  87
  88   void addSub(Node from, Node to);
  89   void learnGeqSub(Node geq);
  90
  91   static Node mkGeqOne(Node v);
  92
  93   // x ->  <geqZero, leqOne>
  94   typedef context::CDHashMap<Node, std::pair<Node, Node>, NodeHashFunction>
  95       CDNode2PairMap;
  96   CDNode2PairMap d_pbBounds;
  97   theory::SubstitutionMap d_subCache;
  98
  99   typedef std::unordered_set<Node, NodeHashFunction> NodeSet;
 100   NodeSet d_learningCache;
 101
 102   context::CDO<unsigned> d_pbs;
 103
 104   // decompose into \sum pos >= neg + off
 105   Maybe<Rational> d_off;
 106   std::vector<Node> d_pos;
 107   std::vector<Node> d_neg;
 108
 109   /** Returns true if successful. */
 110   bool decomposeAssertion(Node assertion, bool negated);
 111 };
 112
 113 }  // namespace passes
 114 }  // namespace preprocessing
 115 }  // namespace CVC4
 116
 117 #endif  // CVC4__PREPROCESSING__PASSES__PSEUDO_BOOLEAN_PROCESSOR_H