1 /********************* */
2 /*! \file ite_removal.cpp
4 ** Original author: Dejan Jovanovic
5 ** Major contributors: Tim King, Morgan Deters
6 ** Minor contributors (to current version): Kshitij Bansal, Andrew Reynolds, Clark Barrett
7 ** This file is part of the CVC4 project.
8 ** Copyright (c) 2009-2014 New York University and The University of Iowa
9 ** See the file COPYING in the top-level source directory for licensing
10 ** information.\endverbatim
12 ** \brief Removal of term ITEs
14 ** Removal of term ITEs.
19 #include "util/ite_removal.h"
20 #include "expr/command.h"
21 #include "theory/ite_utilities.h"
22 #include "proof/proof_manager.h"
29 RemoveITE::RemoveITE(context::UserContext
* u
)
32 d_containsVisitor
= new theory::ContainsTermITEVisitor();
35 RemoveITE::~RemoveITE(){
36 delete d_containsVisitor
;
39 void RemoveITE::garbageCollect(){
40 d_containsVisitor
->garbageCollect();
43 theory::ContainsTermITEVisitor
* RemoveITE::getContainsVisitor() {
44 return d_containsVisitor
;
47 size_t RemoveITE::collectedCacheSizes() const{
48 return d_containsVisitor
->cache_size() + d_iteCache
.size();
51 void RemoveITE::run(std::vector
<Node
>& output
, IteSkolemMap
& iteSkolemMap
, bool reportDeps
)
53 size_t n
= output
.size();
54 for (unsigned i
= 0, i_end
= output
.size(); i
< i_end
; ++ i
) {
55 // Do this in two steps to avoid Node problems(?)
56 // Appears related to bug 512, splitting this into two lines
57 // fixes the bug on clang on Mac OS
58 Node itesRemoved
= run(output
[i
], output
, iteSkolemMap
, false);
59 // In some calling contexts, not necessary to report dependence information.
60 if(reportDeps
&& options::unsatCores()) {
61 // new assertions have a dependence on the node
62 PROOF( ProofManager::currentPM()->addDependence(itesRemoved
, output
[i
]); )
63 while(n
< output
.size()) {
64 PROOF( ProofManager::currentPM()->addDependence(output
[n
], output
[i
]); )
68 output
[i
] = itesRemoved
;
72 bool RemoveITE::containsTermITE(TNode e
) const {
73 return d_containsVisitor
->containsTermITE(e
);
76 Node
RemoveITE::run(TNode node
, std::vector
<Node
>& output
,
77 IteSkolemMap
& iteSkolemMap
, bool inQuant
) {
79 Debug("ite") << "removeITEs(" << node
<< ")" << endl
;
81 if(node
.isVar() || node
.isConst() ||
82 (options::biasedITERemoval() && !containsTermITE(node
))){
86 // The result may be cached already
87 std::pair
<Node
, bool> cacheKey(node
, inQuant
);
88 NodeManager
*nodeManager
= NodeManager::currentNM();
89 ITECache::const_iterator i
= d_iteCache
.find(cacheKey
);
90 if(i
!= d_iteCache
.end()) {
91 Node cached
= (*i
).second
;
92 Debug("ite") << "removeITEs: in-cache: " << cached
<< endl
;
93 return cached
.isNull() ? Node(node
) : cached
;
96 // Remember that we're inside a quantifier
97 if(node
.getKind() == kind::FORALL
|| node
.getKind() == kind::EXISTS
) {
101 // If an ITE replace it
102 if(node
.getKind() == kind::ITE
) {
103 TypeNode nodeType
= node
.getType();
104 if(!nodeType
.isBoolean() && (!inQuant
|| !node
.hasBoundVar())) {
106 // Make the skolem to represent the ITE
107 skolem
= nodeManager
->mkSkolem("termITE", nodeType
, "a variable introduced due to term-level ITE removal");
111 nodeManager
->mkNode(kind::ITE
, node
[0], skolem
.eqNode(node
[1]),
112 skolem
.eqNode(node
[2]));
113 Debug("ite") << "removeITEs(" << node
<< ") => " << newAssertion
<< endl
;
116 d_iteCache
.insert(cacheKey
, skolem
);
118 // Remove ITEs from the new assertion, rewrite it and push it to the output
119 newAssertion
= run(newAssertion
, output
, iteSkolemMap
, inQuant
);
121 iteSkolemMap
[skolem
] = output
.size();
122 output
.push_back(newAssertion
);
124 // The representation is now the skolem
129 // If not an ITE, go deep
130 vector
<Node
> newChildren
;
131 bool somethingChanged
= false;
132 if(node
.getMetaKind() == kind::metakind::PARAMETERIZED
) {
133 newChildren
.push_back(node
.getOperator());
135 // Remove the ITEs from the children
136 for(TNode::const_iterator it
= node
.begin(), end
= node
.end(); it
!= end
; ++it
) {
137 Node newChild
= run(*it
, output
, iteSkolemMap
, inQuant
);
138 somethingChanged
|= (newChild
!= *it
);
139 newChildren
.push_back(newChild
);
142 // If changes, we rewrite
143 if(somethingChanged
) {
144 Node cached
= nodeManager
->mkNode(node
.getKind(), newChildren
);
145 d_iteCache
.insert(cacheKey
, cached
);
148 d_iteCache
.insert(cacheKey
, Node::null());
153 Node
RemoveITE::replace(TNode node
, bool inQuant
) const {
154 if(node
.isVar() || node
.isConst() ||
155 (options::biasedITERemoval() && !containsTermITE(node
))){
160 NodeManager
*nodeManager
= NodeManager::currentNM();
161 ITECache::const_iterator i
= d_iteCache
.find(make_pair(node
, inQuant
));
162 if(i
!= d_iteCache
.end()) {
163 Node cached
= (*i
).second
;
164 return cached
.isNull() ? Node(node
) : cached
;
167 // Remember that we're inside a quantifier
168 if(node
.getKind() == kind::FORALL
|| node
.getKind() == kind::EXISTS
) {
172 vector
<Node
> newChildren
;
173 bool somethingChanged
= false;
174 if(node
.getMetaKind() == kind::metakind::PARAMETERIZED
) {
175 newChildren
.push_back(node
.getOperator());
177 // Replace in children
178 for(TNode::const_iterator it
= node
.begin(), end
= node
.end(); it
!= end
; ++it
) {
179 Node newChild
= replace(*it
, inQuant
);
180 somethingChanged
|= (newChild
!= *it
);
181 newChildren
.push_back(newChild
);
184 // If changes, we rewrite
185 if(somethingChanged
) {
186 return nodeManager
->mkNode(node
.getKind(), newChildren
);
192 }/* CVC4 namespace */