src/theory/arith/arith_ite_utils.h

   1 /*********************                                                        */
   2 /*! \file arith_ite_utils.h
   3  ** \verbatim
   4  ** Top contributors (to current version):
   5  **   Tim King, Mathias Preiner, Aina Niemetz
   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 [[ Add one-line brief description here ]]
  13  **
  14  ** [[ Add lengthier description here ]]
  15  ** \todo document this file
  16  **/
  17
  18 // Pass 1: label the ite as (constant) or (+ constant variable)
  19
  20 #include "cvc4_private.h"
  21
  22 #ifndef CVC4__THEORY__ARITH__ARITH_ITE_UTILS_H
  23 #define CVC4__THEORY__ARITH__ARITH_ITE_UTILS_H
  24
  25 #include <unordered_map>
  26
  27 #include "expr/node.h"
  28 #include "context/cdo.h"
  29 #include "context/cdinsert_hashmap.h"
  30
  31 namespace CVC4 {
  32 namespace preprocessing {
  33 namespace util {
  34 class ContainsTermITEVisitor;
  35 }
  36 }  // namespace preprocessing
  37
  38 namespace theory {
  39
  40 class SubstitutionMap;
  41 class TheoryModel;
  42
  43 namespace arith {
  44
  45 class ArithIteUtils {
  46   preprocessing::util::ContainsTermITEVisitor& d_contains;
  47   SubstitutionMap* d_subs;
  48   TheoryModel* d_model;
  49
  50   typedef std::unordered_map<Node, Node, NodeHashFunction> NodeMap;
  51   // cache for reduce vars
  52   NodeMap d_reduceVar; // if reduceVars[n].isNull(), treat reduceVars[n] == n
  53
  54   // reduceVars[n] = d_constants[n] + d_varParts[n]
  55   NodeMap d_constants; // d_constants[n] is a constant ite tree
  56   NodeMap d_varParts; // d_varParts[n] is a polynomial
  57
  58
  59   NodeMap d_reduceGcd;
  60   typedef std::unordered_map<Node, Integer, NodeHashFunction> NodeIntegerMap;
  61   NodeIntegerMap d_gcds;
  62
  63   Integer d_one;
  64
  65   context::CDO<unsigned> d_subcount;
  66   typedef context::CDInsertHashMap<Node, Node, NodeHashFunction> CDNodeMap;
  67   CDNodeMap d_skolems;
  68
  69   typedef std::map<Node, std::set<Node> > ImpMap;
  70   ImpMap d_implies;
  71
  72   std::vector<Node> d_orBinEqs;
  73
  74 public:
  75  ArithIteUtils(preprocessing::util::ContainsTermITEVisitor& contains,
  76                context::Context* userContext,
  77                TheoryModel* model);
  78  ~ArithIteUtils();
  79
  80  //(ite ?v_2 ?v_1 (ite ?v_3 (- ?v_1 128) (- ?v_1 256)))
  81
  82  /** removes common sums variables sums from term ites. */
  83  Node reduceVariablesInItes(Node n);
  84
  85  Node reduceConstantIteByGCD(Node n);
  86
  87  void clear();
  88
  89  Node applySubstitutions(TNode f);
  90  unsigned getSubCount() const;
  91
  92  void learnSubstitutions(const std::vector<Node>& assertions);
  93
  94 private:
  95   /* applies this to all children of n and constructs the result */
  96   Node applyReduceVariablesInItes(Node n);
  97
  98   const Integer& gcdIte(Node n);
  99   Node reduceIteConstantIteByGCD_rec(Node n, const Rational& q);
 100   Node reduceIteConstantIteByGCD(Node n);
 101
 102   void addSubstitution(TNode f, TNode t);
 103   Node selectForCmp(Node n) const;
 104
 105   void collectAssertions(TNode assertion);
 106   void addImplications(Node x, Node y);
 107   Node findIteCnd(TNode tb, TNode fb) const;
 108   bool solveBinOr(TNode binor);
 109
 110 }; /* class ArithIteUtils */
 111
 112 }/* CVC4::theory::arith namespace */
 113 }/* CVC4::theory namespace */
 114 }/* CVC4 namespace */
 115
 116 #endif /* CVC4__THEORY__ARITH__ARITH_ITE_UTILS_H */