1 /*********************                                                        */
2 /*! \file arith_ite_utils.h
3  ** \verbatim
4  ** Top contributors (to current version):
5  **   Tim King, Aina Niemetz
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 // 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_skolemsAdded;
73 
74   std::vector<Node> d_orBinEqs;
75 
76 public:
77  ArithIteUtils(preprocessing::util::ContainsTermITEVisitor& contains,
78                context::Context* userContext,
79                TheoryModel* model);
80  ~ArithIteUtils();
81 
82  //(ite ?v_2 ?v_1 (ite ?v_3 (- ?v_1 128) (- ?v_1 256)))
83 
84  /** removes common sums variables sums from term ites. */
85  Node reduceVariablesInItes(Node n);
86 
87  Node reduceConstantIteByGCD(Node n);
88 
89  void clear();
90 
91  Node applySubstitutions(TNode f);
92  unsigned getSubCount() const;
93 
94  void learnSubstitutions(const std::vector<Node>& assertions);
95 
96 private:
97   /* applies this to all children of n and constructs the result */
98   Node applyReduceVariablesInItes(Node n);
99 
100   const Integer& gcdIte(Node n);
101   Node reduceIteConstantIteByGCD_rec(Node n, const Rational& q);
102   Node reduceIteConstantIteByGCD(Node n);
103 
104   void addSubstitution(TNode f, TNode t);
105   Node selectForCmp(Node n) const;
106 
107   void collectAssertions(TNode assertion);
108   void addImplications(Node x, Node y);
109   Node findIteCnd(TNode tb, TNode fb) const;
110   bool solveBinOr(TNode binor);
111 
112 }; /* class ArithIteUtils */
113 
114 }/* CVC4::theory::arith namespace */
115 }/* CVC4::theory namespace */
116 }/* CVC4 namespace */
117 
118 #endif /* __CVC4__THEORY__ARITH__ARITH_ITE_UTILS_H */
119