c0c865b9849056548647acc1d88180769683b144
1 /********************* */
2 /*! \file model_postprocessor.cpp
4 ** Original author: Morgan Deters
5 ** Major contributors: none
6 ** Minor contributors (to current version): Andrew Reynolds
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
17 #include "smt/model_postprocessor.h"
18 #include "smt/boolean_terms.h"
19 #include "expr/node_manager_attributes.h"
23 using namespace CVC4::smt
;
25 Node
ModelPostprocessor::rewriteAs(TNode n
, TypeNode asType
) {
26 if(n
.getType().isSubtypeOf(asType
)) {
27 // good to go, we have the right type
30 if(n
.getKind() == kind::LAMBDA
) {
31 Assert(asType
.isFunction());
32 Node rhs
= rewriteAs(n
[1], asType
[1]);
33 Node out
= NodeManager::currentNM()->mkNode(kind::LAMBDA
, n
[0], rhs
);
34 Debug("boolean-terms") << "rewrote " << n
<< " as " << out
<< std::endl
;
35 Debug("boolean-terms") << "need type " << asType
<< endl
;
36 Assert(out
.getType() == asType
);
40 // we don't handle non-const right now
43 if(asType
.isBoolean()) {
44 if(n
.getType().isBitVector(1u)) {
45 // type mismatch: should only happen for Boolean-term conversion under
46 // datatype constructor applications; rewrite from BV(1) back to Boolean
47 bool tf
= (n
.getConst
<BitVector
>().getValue() == 1);
48 return NodeManager::currentNM()->mkConst(tf
);
50 if(n
.getType().isDatatype() && n
.getType().hasAttribute(BooleanTermAttr())) {
51 // type mismatch: should only happen for Boolean-term conversion under
52 // datatype constructor applications; rewrite from datatype back to Boolean
53 Assert(n
.getKind() == kind::APPLY_CONSTRUCTOR
);
54 Assert(n
.getNumChildren() == 0);
55 // we assume (by construction) false is first; see boolean_terms.cpp
56 bool tf
= (Datatype::indexOf(n
.getOperator().toExpr()) == 1);
57 Debug("boolean-terms") << "+++ rewriteAs " << n
<< " : " << asType
<< " ==> " << tf
<< endl
;
58 return NodeManager::currentNM()->mkConst(tf
);
61 if(n
.getType().isBoolean()) {
62 bool tf
= n
.getConst
<bool>();
63 if(asType
.isBitVector(1u)) {
64 return NodeManager::currentNM()->mkConst(BitVector(1u, tf
? 1u : 0u));
66 if(asType
.isDatatype() && asType
.hasAttribute(BooleanTermAttr())) {
67 const Datatype
& asDatatype
= asType
.getConst
<Datatype
>();
68 return NodeManager::currentNM()->mkNode(kind::APPLY_CONSTRUCTOR
, (tf
? asDatatype
[0] : asDatatype
[1]).getConstructor());
71 if(n
.getType().isRecord() && asType
.isRecord()) {
72 Debug("boolean-terms") << "+++ got a record - rewriteAs " << n
<< " : " << asType
<< endl
;
73 const Record
& rec CVC4_UNUSED
= n
.getType().getConst
<Record
>();
74 const Record
& asRec
= asType
.getConst
<Record
>();
75 Assert(rec
.getNumFields() == asRec
.getNumFields());
76 Assert(n
.getNumChildren() == asRec
.getNumFields());
77 NodeBuilder
<> b(n
.getKind());
79 for(size_t i
= 0; i
< n
.getNumChildren(); ++i
) {
80 b
<< rewriteAs(n
[i
], TypeNode::fromType(asRec
[i
].second
));
83 Debug("boolean-terms") << "+++ returning record " << out
<< endl
;
86 Debug("boolean-terms") << "+++ rewriteAs " << n
<< " : " << asType
<< endl
;
87 if(n
.getType().isArray()) {
88 Assert(asType
.isArray());
89 if(n
.getKind() == kind::STORE
) {
90 return NodeManager::currentNM()->mkNode(kind::STORE
,
91 rewriteAs(n
[0], asType
),
92 rewriteAs(n
[1], asType
[0]),
93 rewriteAs(n
[2], asType
[1]));
95 Assert(n
.getKind() == kind::STORE_ALL
);
96 const ArrayStoreAll
& asa
= n
.getConst
<ArrayStoreAll
>();
97 Node val
= rewriteAs(asa
.getExpr(), asType
[1]);
98 return NodeManager::currentNM()->mkConst(ArrayStoreAll(asType
.toType(), val
.toExpr()));
100 if(n
.getType().isParametricDatatype() &&
101 n
.getType().isInstantiatedDatatype() &&
102 asType
.isParametricDatatype() &&
103 asType
.isInstantiatedDatatype() &&
104 n
.getType()[0] == asType
[0]) {
105 // Here, we're doing something like rewriting a (Pair BV1 BV1) as a
107 const Datatype
* dt2
= &asType
[0].getDatatype();
108 std::vector
<TypeNode
> fromParams
, toParams
;
109 for(unsigned i
= 0; i
< dt2
->getNumParameters(); ++i
) {
110 fromParams
.push_back(TypeNode::fromType(dt2
->getParameter(i
)));
111 toParams
.push_back(asType
[i
+ 1]);
113 Assert(dt2
== &Datatype::datatypeOf(n
.getOperator().toExpr()));
114 size_t ctor_ix
= Datatype::indexOf(n
.getOperator().toExpr());
115 NodeBuilder
<> appctorb(kind::APPLY_CONSTRUCTOR
);
116 appctorb
<< (*dt2
)[ctor_ix
].getConstructor();
117 for(size_t j
= 0; j
< n
.getNumChildren(); ++j
) {
118 TypeNode asType
= TypeNode::fromType(SelectorType((*dt2
)[ctor_ix
][j
].getSelector().getType()).getRangeType());
119 asType
= asType
.substitute(fromParams
.begin(), fromParams
.end(), toParams
.begin(), toParams
.end());
120 appctorb
<< rewriteAs(n
[j
], asType
);
125 if(asType
.getNumChildren() != n
.getNumChildren() ||
126 n
.getMetaKind() == kind::metakind::CONSTANT
) {
129 NodeBuilder
<> b(n
.getKind());
130 if (n
.getMetaKind() == kind::metakind::PARAMETERIZED
) {
131 b
<< n
.getOperator();
133 TypeNode::iterator t
= asType
.begin();
134 for(TNode::iterator i
= n
.begin(); i
!= n
.end(); ++i
, ++t
) {
135 Assert(t
!= asType
.end());
136 b
<< rewriteAs(*i
, *t
);
138 Assert(t
== asType
.end());
139 Debug("boolean-terms") << "+++ constructing " << b
<< endl
;
144 void ModelPostprocessor::visit(TNode current
, TNode parent
) {
145 Debug("tuprec") << "visiting " << current
<< endl
;
146 Assert(!alreadyVisited(current
, TNode::null()));
147 if(current
.getType().hasAttribute(expr::DatatypeTupleAttr())) {
148 Assert(current
.getKind() == kind::APPLY_CONSTRUCTOR
);
149 TypeNode expectType
= current
.getType().getAttribute(expr::DatatypeTupleAttr());
150 NodeBuilder
<> b(kind::TUPLE
);
151 TypeNode::iterator t
= expectType
.begin();
152 for(TNode::iterator i
= current
.begin(); i
!= current
.end(); ++i
, ++t
) {
153 Assert(alreadyVisited(*i
, TNode::null()));
154 Assert(t
!= expectType
.end());
155 TNode n
= d_nodes
[*i
];
156 n
= n
.isNull() ? *i
: n
;
157 if(!n
.getType().isSubtypeOf(*t
)) {
158 Assert(n
.getType().isBitVector(1u) ||
159 (n
.getType().isDatatype() && n
.getType().hasAttribute(BooleanTermAttr())));
161 Assert((*t
).isBoolean());
162 if(n
.getType().isBitVector(1u)) {
163 b
<< NodeManager::currentNM()->mkConst(bool(n
.getConst
<BitVector
>().getValue() == 1));
165 // we assume (by construction) false is first; see boolean_terms.cpp
166 b
<< NodeManager::currentNM()->mkConst(bool(Datatype::indexOf(n
.getOperator().toExpr()) == 1));
172 Assert(t
== expectType
.end());
173 d_nodes
[current
] = b
;
174 Debug("tuprec") << "returning " << d_nodes
[current
] << endl
;
175 // The assert below is too strong---we might be returning a model value but
176 // expect a type that still uses datatypes for tuples/records. If it's
177 // really not the right type we should catch it in SmtEngine anyway.
178 // Assert(d_nodes[current].getType() == expectType);
179 } else if(current
.getType().hasAttribute(expr::DatatypeRecordAttr())) {
180 Assert(current
.getKind() == kind::APPLY_CONSTRUCTOR
);
181 TypeNode expectType
= current
.getType().getAttribute(expr::DatatypeRecordAttr());
182 const Record
& expectRec
= expectType
.getConst
<Record
>();
183 NodeBuilder
<> b(kind::RECORD
);
184 b
<< current
.getType().getAttribute(expr::DatatypeRecordAttr());
185 Record::const_iterator t
= expectRec
.begin();
186 for(TNode::iterator i
= current
.begin(); i
!= current
.end(); ++i
, ++t
) {
187 Assert(alreadyVisited(*i
, TNode::null()));
188 Assert(t
!= expectRec
.end());
189 TNode n
= d_nodes
[*i
];
190 n
= n
.isNull() ? *i
: n
;
191 if(!n
.getType().isSubtypeOf(TypeNode::fromType((*t
).second
))) {
192 Assert(n
.getType().isBitVector(1u) ||
193 (n
.getType().isDatatype() && n
.getType().hasAttribute(BooleanTermAttr())));
195 Assert((*t
).second
.isBoolean());
196 if(n
.getType().isBitVector(1u)) {
197 b
<< NodeManager::currentNM()->mkConst(bool(n
.getConst
<BitVector
>().getValue() == 1));
199 // we assume (by construction) false is first; see boolean_terms.cpp
200 b
<< NodeManager::currentNM()->mkConst(bool(Datatype::indexOf(n
.getOperator().toExpr()) == 1));
206 Assert(t
== expectRec
.end());
207 d_nodes
[current
] = b
;
208 Debug("tuprec") << "returning " << d_nodes
[current
] << endl
;
209 Assert(d_nodes
[current
].getType() == expectType
);
210 } else if(current
.getKind() == kind::APPLY_CONSTRUCTOR
&&
211 ( current
.getOperator().hasAttribute(BooleanTermAttr()) ||
212 ( current
.getOperator().getKind() == kind::APPLY_TYPE_ASCRIPTION
&&
213 current
.getOperator()[0].hasAttribute(BooleanTermAttr()) ) )) {
214 NodeBuilder
<> b(kind::APPLY_CONSTRUCTOR
);
216 if(current
.getOperator().getKind() == kind::APPLY_TYPE_ASCRIPTION
) {
217 TNode oldAsc
= current
.getOperator().getOperator();
218 Debug("boolean-terms") << "old asc: " << oldAsc
<< endl
;
219 Node newCons
= current
.getOperator()[0].getAttribute(BooleanTermAttr());
220 Node newAsc
= NodeManager::currentNM()->mkConst(AscriptionType(newCons
.getType().toType()));
221 Debug("boolean-terms") << "new asc: " << newAsc
<< endl
;
222 if(newCons
.getType().getRangeType().isParametricDatatype()) {
223 vector
<TypeNode
> oldParams
= TypeNode::fromType(oldAsc
.getConst
<AscriptionType
>().getType()).getRangeType().getParamTypes();
224 vector
<TypeNode
> newParams
= newCons
.getType().getRangeType().getParamTypes();
225 Assert(oldParams
.size() == newParams
.size() && oldParams
.size() > 0);
226 newAsc
= NodeManager::currentNM()->mkConst(AscriptionType(newCons
.getType().substitute(newParams
.begin(), newParams
.end(), oldParams
.begin(), oldParams
.end()).toType()));
228 realOp
= NodeManager::currentNM()->mkNode(kind::APPLY_TYPE_ASCRIPTION
, newAsc
, newCons
);
230 realOp
= current
.getOperator().getAttribute(BooleanTermAttr());
233 Debug("boolean-terms") << "+ op " << b
.getOperator() << endl
;
234 TypeNode::iterator j
= realOp
.getType().begin();
235 for(TNode::iterator i
= current
.begin(); i
!= current
.end(); ++i
, ++j
) {
236 Assert(j
!= realOp
.getType().end());
237 Assert(alreadyVisited(*i
, TNode::null()));
238 TNode repl
= d_nodes
[*i
];
239 repl
= repl
.isNull() ? *i
: repl
;
240 Debug("boolean-terms") << "+ adding " << repl
<< " expecting " << *j
<< endl
;
241 b
<< rewriteAs(repl
, *j
);
244 Debug("boolean-terms") << "model-post: " << current
<< endl
245 << "- returning " << n
<< endl
;
246 d_nodes
[current
] = n
;
248 // rewrite based on children
250 for(size_t i
= 0; i
< current
.getNumChildren(); ++i
) {
251 Assert(d_nodes
.find(current
[i
]) != d_nodes
.end());
252 if(!d_nodes
[current
[i
]].isNull()) {
258 Debug("tuprec") << "returning self for kind " << current
.getKind() << endl
;
260 d_nodes
[current
] = Node::null();
262 // rewrite based on children
263 NodeBuilder
<> nb(current
.getKind());
264 for(size_t i
= 0; i
< current
.getNumChildren(); ++i
) {
265 Assert(d_nodes
.find(current
[i
]) != d_nodes
.end());
266 TNode rw
= d_nodes
[current
[i
]];
272 d_nodes
[current
] = nb
;
273 Debug("tuprec") << "rewrote children for kind " << current
.getKind() << " got " << d_nodes
[current
] << endl
;
276 }/* ModelPostprocessor::visit() */