1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
|
/********************* */
/*! \file ite_removal.cpp
** \verbatim
** Original author: Dejan Jovanović <dejan.jovanovic@gmail.com>
** Major contributors: Andrew Reynolds <andrew.j.reynolds@gmail.com>, Morgan Deters <mdeters@cs.nyu.edu>
** Minor contributors (to current version): Clark Barrett <barrett@cs.nyu.edu>
** This file is part of the CVC4 project.
** Copyright (c) 2009-2013 New York University and The University of Iowa
** See the file COPYING in the top-level source directory for licensing
** information.\endverbatim
**
** \brief Removal of term ITEs
**
** Removal of term ITEs.
**/
#include <vector>
#include "util/ite_removal.h"
#include "theory/rewriter.h"
#include "expr/command.h"
#include "theory/quantifiers/options.h"
using namespace CVC4;
using namespace std;
namespace CVC4 {
void RemoveITE::run(std::vector<Node>& output, IteSkolemMap& iteSkolemMap)
{
for (unsigned i = 0, i_end = output.size(); i < i_end; ++ i) {
std::vector<Node> quantVar;
output[i] = run(output[i], output, iteSkolemMap, quantVar);
}
}
Node RemoveITE::run(TNode node, std::vector<Node>& output,
IteSkolemMap& iteSkolemMap, std::vector<Node>& quantVar) {
// Current node
Debug("ite") << "removeITEs(" << node << ")" << endl;
// The result may be cached already
NodeManager *nodeManager = NodeManager::currentNM();
ITECache::iterator i = d_iteCache.find(node);
if(i != d_iteCache.end()) {
Node cachedRewrite = (*i).second;
Debug("ite") << "removeITEs: in-cache: " << cachedRewrite << endl;
return cachedRewrite.isNull() ? Node(node) : cachedRewrite;
}
// If an ITE replace it
if(node.getKind() == kind::ITE) {
TypeNode nodeType = node.getType();
if(!nodeType.isBoolean()) {
Node skolem;
// Make the skolem to represent the ITE
if( quantVar.empty() ){
skolem = nodeManager->mkSkolem("termITE_$$", nodeType, "a variable introduced due to term-level ITE removal");
}else{
//if in the scope of free variables, make a skolem operator
vector< TypeNode > argTypes;
for( size_t i=0; i<quantVar.size(); i++ ){
argTypes.push_back( quantVar[i].getType() );
}
TypeNode typ = NodeManager::currentNM()->mkFunctionType( argTypes, nodeType );
Node op = NodeManager::currentNM()->mkSkolem( "termITEop_$$", typ, "a function variable introduced due to term-level ITE removal" );
vector< Node > funcArgs;
funcArgs.push_back( op );
funcArgs.insert( funcArgs.end(), quantVar.begin(), quantVar.end() );
skolem = NodeManager::currentNM()->mkNode( kind::APPLY_UF, funcArgs );
}
// The new assertion
Node newAssertion =
nodeManager->mkNode(kind::ITE, node[0], skolem.eqNode(node[1]),
skolem.eqNode(node[2]));
Debug("ite") << "removeITEs(" << node << ") => " << newAssertion << endl;
// Attach the skolem
d_iteCache[node] = skolem;
// Remove ITEs from the new assertion, rewrite it and push it to the output
newAssertion = run(newAssertion, output, iteSkolemMap, quantVar);
if( !quantVar.empty() ){
//if in the scope of free variables, it is a quantified assertion
vector< Node > children;
children.push_back( NodeManager::currentNM()->mkNode( kind::BOUND_VAR_LIST, quantVar ) );
children.push_back( newAssertion );
newAssertion = NodeManager::currentNM()->mkNode( kind::FORALL, children );
}
iteSkolemMap[skolem] = output.size();
output.push_back(newAssertion);
// The representation is now the skolem
return skolem;
}
}
// If not an ITE, go deep
if( ( node.getKind() != kind::FORALL || options::iteRemoveQuant() ) &&
node.getKind() != kind::EXISTS &&
node.getKind() != kind::REWRITE_RULE ) {
std::vector< Node > newQuantVar;
newQuantVar.insert( newQuantVar.end(), quantVar.begin(), quantVar.end() );
if( node.getKind()==kind::FORALL ){
for( size_t i=0; i<node[0].getNumChildren(); i++ ){
newQuantVar.push_back( node[0][i] );
}
}
vector<Node> newChildren;
bool somethingChanged = false;
if(node.getMetaKind() == kind::metakind::PARAMETERIZED) {
newChildren.push_back(node.getOperator());
}
// Remove the ITEs from the children
for(TNode::const_iterator it = node.begin(), end = node.end(); it != end; ++it) {
Node newChild = run(*it, output, iteSkolemMap, newQuantVar);
somethingChanged |= (newChild != *it);
newChildren.push_back(newChild);
}
// If changes, we rewrite
if(somethingChanged) {
Node cachedRewrite = nodeManager->mkNode(node.getKind(), newChildren);
d_iteCache[node] = cachedRewrite;
return cachedRewrite;
} else {
d_iteCache[node] = Node::null();
return node;
}
} else {
d_iteCache[node] = Node::null();
return node;
}
}
}/* CVC4 namespace */
|
