1 /********************* */
2 /*! \file arith_ite_utils.h
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
12 ** \brief [[ Add one-line brief description here ]]
14 ** [[ Add lengthier description here ]]
15 ** \todo document this file
18 // Pass 1: label the ite as (constant) or (+ constant variable)
20 #include "cvc4_private.h"
22 #ifndef CVC4__THEORY__ARITH__ARITH_ITE_UTILS_H
23 #define CVC4__THEORY__ARITH__ARITH_ITE_UTILS_H
25 #include <unordered_map>
27 #include "expr/node.h"
28 #include "context/cdo.h"
29 #include "context/cdinsert_hashmap.h"
32 namespace preprocessing
{
34 class ContainsTermITEVisitor
;
36 } // namespace preprocessing
40 class SubstitutionMap
;
46 preprocessing::util::ContainsTermITEVisitor
& d_contains
;
47 SubstitutionMap
* d_subs
;
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
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
60 typedef std::unordered_map
<Node
, Integer
, NodeHashFunction
> NodeIntegerMap
;
61 NodeIntegerMap d_gcds
;
65 context::CDO
<unsigned> d_subcount
;
66 typedef context::CDInsertHashMap
<Node
, Node
, NodeHashFunction
> CDNodeMap
;
69 typedef std::map
<Node
, std::set
<Node
> > ImpMap
;
72 std::vector
<Node
> d_orBinEqs
;
75 ArithIteUtils(preprocessing::util::ContainsTermITEVisitor
& contains
,
76 context::Context
* userContext
,
80 //(ite ?v_2 ?v_1 (ite ?v_3 (- ?v_1 128) (- ?v_1 256)))
82 /** removes common sums variables sums from term ites. */
83 Node
reduceVariablesInItes(Node n
);
85 Node
reduceConstantIteByGCD(Node n
);
89 Node
applySubstitutions(TNode f
);
90 unsigned getSubCount() const;
92 void learnSubstitutions(const std::vector
<Node
>& assertions
);
95 /* applies this to all children of n and constructs the result */
96 Node
applyReduceVariablesInItes(Node n
);
98 const Integer
& gcdIte(Node n
);
99 Node
reduceIteConstantIteByGCD_rec(Node n
, const Rational
& q
);
100 Node
reduceIteConstantIteByGCD(Node n
);
102 void addSubstitution(TNode f
, TNode t
);
103 Node
selectForCmp(Node n
) const;
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
);
110 }; /* class ArithIteUtils */
112 }/* CVC4::theory::arith namespace */
113 }/* CVC4::theory namespace */
114 }/* CVC4 namespace */
116 #endif /* CVC4__THEORY__ARITH__ARITH_ITE_UTILS_H */