1 /********************* */
2 /*! \file boolean_terms.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
12 ** \brief [[ Add one-line brief description here ]]
14 ** [[ Add lengthier description here ]]
15 ** \todo document this file
18 #include "smt/boolean_terms.h"
19 #include "smt/smt_engine.h"
20 #include "theory/theory_engine.h"
21 #include "theory/theory_model.h"
22 #include "theory/booleans/boolean_term_conversion_mode.h"
23 #include "theory/booleans/options.h"
24 #include "expr/kind.h"
25 #include "expr/node_manager_attributes.h"
26 #include "util/ntuple.h"
34 using namespace CVC4::theory
;
35 using namespace CVC4::theory::booleans
;
40 BooleanTermConverter::BooleanTermConverter(SmtEngine
& smt
) :
46 d_varCache(smt
.d_userContext
),
47 d_termCache(smt
.d_userContext
),
50 d_datatypeReverseCache() {
52 // set up our "false" and "true" conversions based on command-line option
53 if(options::booleanTermConversionMode() == BOOLEAN_TERM_CONVERT_TO_BITVECTORS
||
54 options::booleanTermConversionMode() == BOOLEAN_TERM_CONVERT_NATIVE
) {
55 d_ff
= NodeManager::currentNM()->mkConst(BitVector(1u, 0u));
56 d_tt
= NodeManager::currentNM()->mkConst(BitVector(1u, 1u));
58 if(options::booleanTermConversionMode() == BOOLEAN_TERM_CONVERT_TO_BITVECTORS
) {
62 Datatype
spec("BooleanTerm");
63 // don't change the order; false is assumed to come first by the model postprocessor
64 spec
.addConstructor(DatatypeConstructor("BT_False"));
65 spec
.addConstructor(DatatypeConstructor("BT_True"));
66 const Datatype
& dt
= NodeManager::currentNM()->toExprManager()->mkDatatypeType(spec
).getDatatype();
67 d_ffDt
= NodeManager::currentNM()->mkNode(kind::APPLY_CONSTRUCTOR
, Node::fromExpr(dt
["BT_False"].getConstructor()));
68 d_ttDt
= NodeManager::currentNM()->mkNode(kind::APPLY_CONSTRUCTOR
, Node::fromExpr(dt
["BT_True"].getConstructor()));
69 // mark this datatype type as being special for Boolean term conversion
70 TypeNode::fromType(dt
.getDatatypeType()).setAttribute(BooleanTermAttr(), Node::null());
71 if(options::booleanTermConversionMode() == BOOLEAN_TERM_CONVERT_TO_DATATYPES
) {
72 Assert(d_ff
.isNull() && d_tt
.isNull());
78 // assert that we set it up correctly
79 Assert(!d_ff
.isNull() && !d_tt
.isNull());
80 Assert(!d_ffDt
.isNull() && !d_ttDt
.isNull());
82 Assert(d_ff
.getType() == d_tt
.getType());
83 Assert(d_ffDt
!= d_ttDt
);
84 Assert(d_ffDt
.getType() == d_ttDt
.getType());
86 }/* BooleanTermConverter::BooleanTermConverter() */
88 static inline bool isBoolean(TNode top
, unsigned i
) {
89 switch(top
.getKind()) {
98 case kind::REWRITE_RULE
:
99 case kind::RR_REWRITE
:
100 case kind::RR_DEDUCTION
:
101 case kind::RR_REDUCTION
:
102 case kind::INST_PATTERN
:
109 return top
.getType().isBoolean();
116 // This function rewrites "in" as an "as"---this is actually expected
117 // to be for model-substitution, so the "in" is a Boolean-term-converted
118 // node, and "as" is the original. See how it's used in function
121 // Note this isn't the case any longer, and parts of what's below have
122 // been repurposed for *forward* conversion, meaning this works in either
124 Node
BooleanTermConverter::rewriteAs(TNode in
, TypeNode as
) throw() {
125 if(in
.getType() == as
) {
128 if(in
.getType().isBoolean()) {
129 Assert(d_tt
.getType() == as
);
130 return NodeManager::currentNM()->mkNode(kind::ITE
, in
, d_tt
, d_ff
);
132 if(as
.isBoolean() && in
.getType().isBitVector() && in
.getType().getBitVectorSize() == 1) {
133 return NodeManager::currentNM()->mkNode(kind::EQUAL
, NodeManager::currentNM()->mkConst(BitVector(1u, 1u)), in
);
135 if(in
.getType().isDatatype()) {
136 if(as
.isBoolean() && in
.getType().hasAttribute(BooleanTermAttr())) {
137 return NodeManager::currentNM()->mkNode(kind::EQUAL
, d_ttDt
, in
);
139 Assert(as
.isDatatype());
140 const Datatype
* dt2
= &as
.getDatatype();
142 if(d_datatypeCache
.find(dt2
) != d_datatypeCache
.end()) {
143 dt1
= d_datatypeCache
[dt2
];
145 dt1
= d_datatypeReverseCache
[dt2
];
147 Assert(dt1
!= NULL
, "expected datatype in cache");
148 Assert(*dt1
== in
.getType().getDatatype(), "improper rewriteAs() between datatypes");
150 for(size_t i
= 0; i
< dt1
->getNumConstructors(); ++i
) {
151 DatatypeConstructor ctor
= (*dt1
)[i
];
152 NodeBuilder
<> appctorb(kind::APPLY_CONSTRUCTOR
);
153 appctorb
<< (*dt2
)[i
].getConstructor();
154 for(size_t j
= 0; j
< ctor
.getNumArgs(); ++j
) {
155 appctorb
<< rewriteAs(NodeManager::currentNM()->mkNode(kind::APPLY_SELECTOR_TOTAL
, ctor
[j
].getSelector(), in
), TypeNode::fromType(SelectorType((*dt2
)[i
][j
].getSelector().getType()).getRangeType()));
157 Node appctor
= appctorb
;
161 Node newOut
= NodeManager::currentNM()->mkNode(kind::ITE
, ctor
.getTester(), appctor
, out
);
167 if(in
.getType().isArray()) {
169 // e.g. in : (Array Int Bool)
170 // for in' : (Array Int (_ BitVec 1))
171 // then subs in |=> \array_lambda ( \lambda (x:Int) . [convert (read a' x) x]
172 Assert(as
.isArray());
173 Assert(as
.getArrayIndexType() == in
.getType().getArrayIndexType());
174 Assert(as
.getArrayConstituentType() != in
.getType().getArrayConstituentType());
175 Node x
= NodeManager::currentNM()->mkBoundVar(as
.getArrayIndexType());
176 Node boundvars
= NodeManager::currentNM()->mkNode(kind::BOUND_VAR_LIST
, x
);
177 Node sel
= NodeManager::currentNM()->mkNode(kind::SELECT
, in
, x
);
178 Node selprime
= rewriteAs(sel
, as
.getArrayConstituentType());
179 Node lam
= NodeManager::currentNM()->mkNode(kind::LAMBDA
, boundvars
, selprime
);
180 Node out
= NodeManager::currentNM()->mkNode(kind::ARRAY_LAMBDA
, lam
);
181 Assert(out
.getType() == as
);
184 if(in
.getType().isParametricDatatype() &&
185 in
.getType().isInstantiatedDatatype()) {
186 // We have something here like (Pair Bool Bool)---need to dig inside
187 // and make it (Pair BV1 BV1)
188 Assert(as
.isParametricDatatype() && as
.isInstantiatedDatatype());
189 const Datatype
* dt2
= &as
[0].getDatatype();
190 std::vector
<TypeNode
> fromParams
, toParams
;
191 for(unsigned i
= 0; i
< dt2
->getNumParameters(); ++i
) {
192 fromParams
.push_back(TypeNode::fromType(dt2
->getParameter(i
)));
193 toParams
.push_back(as
[i
+ 1]);
196 if(d_datatypeCache
.find(dt2
) != d_datatypeCache
.end()) {
197 dt1
= d_datatypeCache
[dt2
];
199 dt1
= d_datatypeReverseCache
[dt2
];
201 Assert(dt1
!= NULL
, "expected datatype in cache");
202 Assert(*dt1
== in
.getType()[0].getDatatype(), "improper rewriteAs() between datatypes");
204 for(size_t i
= 0; i
< dt1
->getNumConstructors(); ++i
) {
205 DatatypeConstructor ctor
= (*dt1
)[i
];
206 NodeBuilder
<> appctorb(kind::APPLY_CONSTRUCTOR
);
207 appctorb
<< (*dt2
)[i
].getConstructor();
208 for(size_t j
= 0; j
< ctor
.getNumArgs(); ++j
) {
209 TypeNode asType
= TypeNode::fromType(SelectorType((*dt2
)[i
][j
].getSelector().getType()).getRangeType());
210 asType
= asType
.substitute(fromParams
.begin(), fromParams
.end(), toParams
.begin(), toParams
.end());
211 appctorb
<< rewriteAs(NodeManager::currentNM()->mkNode(kind::APPLY_SELECTOR_TOTAL
, ctor
[j
].getSelector(), in
), asType
);
213 Node appctor
= appctorb
;
217 Node newOut
= NodeManager::currentNM()->mkNode(kind::ITE
, ctor
.getTester(), appctor
, out
);
227 const Datatype
& BooleanTermConverter::convertDatatype(const Datatype
& dt
) throw() {
228 const Datatype
*& out
= d_datatypeCache
[&dt
];
233 Debug("boolean-terms") << "convertDatatype: considering " << dt
.getName() << endl
;
234 for(Datatype::const_iterator c
= dt
.begin(); c
!= dt
.end(); ++c
) {
235 TypeNode t
= TypeNode::fromType((*c
).getConstructor().getType());
236 for(TypeNode::const_iterator a
= t
.begin(); a
!= t
.end(); ++a
) {
237 TypeNode converted
= convertType(*a
, true);
238 Debug("boolean-terms") << "GOT: " << converted
<< ":" << converted
.getId() << endl
;
239 if(*a
!= converted
) {
240 SortConstructorType mySelfType
;
241 set
<Type
> unresolvedTypes
;
242 if(dt
.isParametric()) {
243 mySelfType
= NodeManager::currentNM()->toExprManager()->mkSortConstructor(dt
.getName() + "'", dt
.getNumParameters());
244 unresolvedTypes
.insert(mySelfType
);
246 vector
<Datatype
> newDtVector
;
247 if(dt
.isParametric()) {
248 newDtVector
.push_back(Datatype(dt
.getName() + "'", dt
.getParameters(), false));
250 newDtVector
.push_back(Datatype(dt
.getName() + "'", false));
252 Datatype
& newDt
= newDtVector
.front();
253 Debug("boolean-terms") << "found a Boolean arg in constructor " << (*c
).getName() << endl
;
254 for(c
= dt
.begin(); c
!= dt
.end(); ++c
) {
255 DatatypeConstructor
ctor((*c
).getName() + "'", (*c
).getTesterName() + "'");
256 t
= TypeNode::fromType((*c
).getConstructor().getType());
257 for(DatatypeConstructor::const_iterator a
= (*c
).begin(); a
!= (*c
).end(); ++a
) {
258 Type argType
= (*a
).getType().getRangeType();
259 if(argType
.isDatatype() && DatatypeType(argType
).getDatatype() == dt
) {
260 Debug("boolean-terms") << "argtype " << argType
<< " is self" << endl
;
261 if(dt
.isParametric()) {
262 Debug("boolean-terms") << "is-parametric self is " << mySelfType
<< endl
;
263 ctor
.addArg((*a
).getName() + "'", mySelfType
.instantiate(DatatypeType(argType
).getDatatype().getParameters()));
265 ctor
.addArg((*a
).getName() + "'", DatatypeSelfType());
268 Debug("boolean-terms") << "argtype " << argType
<< " is NOT self" << endl
;
269 converted
= convertType(TypeNode::fromType(argType
), true);
270 if(TypeNode::fromType(argType
) != converted
) {
271 ctor
.addArg((*a
).getName() + "'", converted
.toType());
273 ctor
.addArg((*a
).getName() + "'", argType
);
277 newDt
.addConstructor(ctor
);
279 vector
<DatatypeType
> newDttVector
=
280 NodeManager::currentNM()->toExprManager()->mkMutualDatatypeTypes(newDtVector
, unresolvedTypes
);
281 DatatypeType
& newDtt
= newDttVector
.front();
282 const Datatype
& newD
= newDtt
.getDatatype();
283 for(c
= dt
.begin(); c
!= dt
.end(); ++c
) {
284 Debug("boolean-terms") << "constructor " << (*c
).getConstructor() << ":" << (*c
).getConstructor().getType() << " made into " << newD
[(*c
).getName() + "'"].getConstructor() << ":" << newD
[(*c
).getName() + "'"].getConstructor().getType() << endl
;
285 const DatatypeConstructor
*newC
;
286 Node::fromExpr((*(newC
= &newD
[(*c
).getName() + "'"])).getConstructor()).setAttribute(BooleanTermAttr(), Node::fromExpr((*c
).getConstructor()));// other attr?
287 Debug("boolean-terms") << "mapped " << newD
[(*c
).getName() + "'"].getConstructor() << " to " << (*c
).getConstructor() << endl
;
288 d_varCache
[Node::fromExpr((*c
).getConstructor())] = Node::fromExpr(newD
[(*c
).getName() + "'"].getConstructor());
289 d_varCache
[Node::fromExpr((*c
).getTester())] = Node::fromExpr(newD
[(*c
).getName() + "'"].getTester());
290 for(DatatypeConstructor::const_iterator a
= (*c
).begin(); a
!= (*c
).end(); ++a
) {
291 Node::fromExpr((*newC
)[(*a
).getName() + "'"].getSelector()).setAttribute(BooleanTermAttr(), Node::fromExpr((*a
).getSelector()));// other attr?
292 d_varCache
[Node::fromExpr((*a
).getSelector())] = Node::fromExpr(newD
[(*c
).getName() + "'"].getSelector((*a
).getName() + "'"));
296 d_datatypeReverseCache
[&newD
] = &dt
;
302 // this is identity; don't need the reverse cache
306 }/* BooleanTermConverter::convertDatatype() */
308 TypeNode
BooleanTermConverter::convertType(TypeNode type
, bool datatypesContext
) {
309 Debug("boolean-terms") << "CONVERT-TYPE[" << type
<< ":" << type
.getId() << ", " << datatypesContext
<< "]" << endl
;
310 // This function recursively converts the type.
311 if(type
.isBoolean()) {
312 return datatypesContext
? d_ttDt
.getType() : d_tt
.getType();
314 const pair
<TypeNode
, bool> cacheKey(type
, datatypesContext
);
315 if(d_typeCache
.find(cacheKey
) != d_typeCache
.end()) {
316 TypeNode out
= d_typeCache
[cacheKey
];
317 return out
.isNull() ? type
: out
;
319 TypeNode
& outNode
= d_typeCache
[cacheKey
];
320 if(type
.getKind() == kind::DATATYPE_TYPE
||
321 type
.getKind() == kind::PARAMETRIC_DATATYPE
) {
322 bool parametric
= (type
.getKind() == kind::PARAMETRIC_DATATYPE
);
323 const Datatype
& dt
= parametric
? type
[0].getConst
<Datatype
>() : type
.getConst
<Datatype
>();
324 TypeNode out
= TypeNode::fromType(convertDatatype(dt
).getDatatypeType());
325 Debug("boolean-terms") << "AFTER, got "<< out
<< " param:" << parametric
<< endl
;
327 // re-parameterize the translation
328 vector
<TypeNode
> params
= type
.getParamTypes();
329 for(size_t i
= 0; i
< params
.size(); ++i
) {
330 Debug("boolean-terms") << "in loop, got "<< params
[i
] << endl
;
331 params
[i
] = convertType(params
[i
], true);
332 Debug("boolean-terms") << "in loop, convert to "<< params
[i
] << endl
;
334 params
.insert(params
.begin(), out
[0]);
335 out
= NodeManager::currentNM()->mkTypeNode(kind::PARAMETRIC_DATATYPE
, params
);
336 Debug("boolean-terms") << "got OUT: " << out
<< endl
;
339 outNode
= out
;// cache it
340 Debug("boolean-terms") << "OUT is same as TYPE" << endl
;
341 } else Debug("boolean-terms") << "OUT is DIFFERENT FROM TYPE" << endl
;
344 if(type
.isRecord()) {
345 const Record
& rec
= type
.getConst
<Record
>();
346 vector
< pair
<string
, Type
> > flds
;
347 for(Record::const_iterator i
= rec
.begin(); i
!= rec
.end(); ++i
) {
348 TypeNode converted
= convertType(TypeNode::fromType((*i
).second
), true);
349 if(TypeNode::fromType((*i
).second
) != converted
) {
350 flds
.push_back(make_pair((*i
).first
, converted
.toType()));
355 TypeNode newRec
= NodeManager::currentNM()->mkRecordType(Record(flds
));
356 Debug("tuprec") << "converted " << type
<< " to " << newRec
<< endl
;
358 outNode
= newRec
;// cache it
362 if(!type
.isSort() && type
.getNumChildren() > 0) {
363 Debug("boolean-terms") << "here at A for " << type
<< ":" << type
.getId() << endl
;
364 // This should handle tuples and arrays ok.
365 // Might handle function types too, but they can't go
366 // in other types, so it doesn't matter.
367 NodeBuilder
<> b(type
.getKind());
368 if(type
.getMetaKind() == kind::metakind::PARAMETERIZED
) {
369 b
<< type
.getOperator();
371 for(TypeNode::iterator i
= type
.begin(); i
!= type
.end(); ++i
) {
372 b
<< convertType(*i
, false);
376 outNode
= out
;// cache it
378 Debug("boolean-terms") << "here at B, returning " << out
<< ":" << out
.getId() << endl
;
381 // leave the cache at Null
383 }/* BooleanTermConverter::convertType() */
385 // look for vars from "vars" that occur in a term-context in n; transfer them to output.
386 static void collectVarsInTermContext(TNode n
, std::set
<TNode
>& vars
, std::set
<TNode
>& output
, bool boolParent
, std::hash_set
< std::pair
<TNode
, bool>, PairHashFunction
<TNode
, bool, TNodeHashFunction
, BoolHashFunction
> >& alreadySeen
) {
390 const pair
<TNode
, bool> cacheKey(n
, boolParent
);
391 if(alreadySeen
.find(cacheKey
) != alreadySeen
.end()) {
394 alreadySeen
.insert(cacheKey
);
396 if(n
.isVar() && vars
.find(n
) != vars
.end() && !boolParent
) {
403 for(size_t i
= 0; i
< n
.getNumChildren(); ++i
) {
404 collectVarsInTermContext(n
[i
], vars
, output
, isBoolean(n
, i
), alreadySeen
);
411 Node
BooleanTermConverter::rewriteBooleanTermsRec(TNode top
, theory::TheoryId parentTheory
, std::map
<TNode
, Node
>& quantBoolVars
) throw() {
413 stack
< triple
<TNode
, theory::TheoryId
, bool> > worklist
;
414 worklist
.push(triple
<TNode
, theory::TheoryId
, bool>(top
, parentTheory
, false));
415 stack
< NodeBuilder
<> > result
;
416 result
.push(NodeBuilder
<>(kind::TUPLE
));
418 NodeManager
* nm
= NodeManager::currentNM();
420 while(!worklist
.empty()) {
421 top
= worklist
.top().first
;
422 parentTheory
= worklist
.top().second
;
423 bool& childrenPushed
= worklist
.top().third
;
425 Kind k
= top
.getKind();
426 kind::MetaKind mk
= top
.getMetaKind();
428 // we only distinguish between datatypes, booleans, and "other", and we
429 // don't even distinguish datatypes except when in "native" conversion
431 if(parentTheory
!= theory::THEORY_BOOL
) {
432 if(options::booleanTermConversionMode() != BOOLEAN_TERM_CONVERT_NATIVE
||
433 parentTheory
!= theory::THEORY_DATATYPES
) {
434 parentTheory
= theory::THEORY_BUILTIN
;
438 if(!childrenPushed
) {
439 Debug("boolean-terms") << "rewriteBooleanTermsRec: " << top
<< " - parentTheory=" << parentTheory
<< endl
;
441 BooleanTermVarCache::iterator i
= d_varCache
.find(top
);
442 if(i
!= d_varCache
.end()) {
443 result
.top() << ((*i
).second
.isNull() ? Node(top
) : (*i
).second
);
447 BooleanTermCache::iterator j
= d_termCache
.find(pair
<Node
, theory::TheoryId
>(top
, parentTheory
));
448 if(j
!= d_termCache
.end()) {
449 result
.top() << ((*j
).second
.isNull() ? Node(top
) : (*j
).second
);
454 if(quantBoolVars
.find(top
) != quantBoolVars
.end()) {
455 // this Bool variable is quantified over and we're changing it to a BitVector var
456 if(parentTheory
== theory::THEORY_BOOL
) {
457 result
.top() << quantBoolVars
[top
].eqNode(d_tt
);
459 result
.top() << quantBoolVars
[top
];
465 if(parentTheory
!= theory::THEORY_BOOL
&& top
.getType().isBoolean()) {
466 // still need to rewrite e.g. function applications over boolean
467 Node topRewritten
= rewriteBooleanTermsRec(top
, theory::THEORY_BOOL
, quantBoolVars
);
469 if(parentTheory
== theory::THEORY_DATATYPES
) {
470 n
= nm
->mkNode(kind::ITE
, topRewritten
, d_ttDt
, d_ffDt
);
472 n
= nm
->mkNode(kind::ITE
, topRewritten
, d_tt
, d_ff
);
474 Debug("boolean-terms") << "constructed ITE: " << n
<< endl
;
480 if(mk
== kind::metakind::CONSTANT
) {
481 if(k
== kind::STORE_ALL
) {
482 const ArrayStoreAll
& asa
= top
.getConst
<ArrayStoreAll
>();
483 ArrayType arrType
= asa
.getType();
484 TypeNode indexType
= TypeNode::fromType(arrType
.getIndexType());
485 Type constituentType
= arrType
.getConstituentType();
486 if(constituentType
.isBoolean()) {
487 // we have store_all(true) or store_all(false)
488 // just turn it into store_all(1) or store_all(0)
489 if(indexType
.isBoolean()) {
490 // change index type to BV(1) also
491 indexType
= d_tt
.getType();
493 ArrayStoreAll
asaRepl(nm
->mkArrayType(indexType
, d_tt
.getType()).toType(),
494 (asa
.getExpr().getConst
<bool>() ? d_tt
: d_ff
).toExpr());
495 Node n
= nm
->mkConst(asaRepl
);
496 Debug("boolean-terms") << " returning new store_all: " << n
<< endl
;
501 if(indexType
.isBoolean()) {
502 // must change index type to BV(1)
503 indexType
= d_tt
.getType();
504 ArrayStoreAll
asaRepl(nm
->mkArrayType(indexType
, TypeNode::fromType(constituentType
)).toType(), asa
.getExpr());
505 Node n
= nm
->mkConst(asaRepl
);
506 Debug("boolean-terms") << " returning new store_all: " << n
<< endl
;
515 } else if(mk
== kind::metakind::VARIABLE
) {
516 TypeNode t
= top
.getType();
518 for(unsigned i
= 0; i
< t
.getNumChildren(); ++i
) {
519 TypeNode newType
= convertType(t
[i
], false);
520 // is this the return type? (allowed to be Bool)
521 bool returnType
= (i
== t
.getNumChildren() - 1);
522 if(newType
!= t
[i
] && (!t
[i
].isBoolean() || !returnType
)) {
523 vector
<TypeNode
> argTypes
= t
.getArgTypes();
524 for(unsigned j
= 0; j
< argTypes
.size(); ++j
) {
525 argTypes
[j
] = convertType(argTypes
[j
], false);
527 TypeNode rangeType
= t
.getRangeType();
528 if(!rangeType
.isBoolean()) {
529 rangeType
= convertType(rangeType
, false);
531 TypeNode newType
= nm
->mkFunctionType(argTypes
, rangeType
);
532 Node n
= nm
->mkSkolem(top
.getAttribute(expr::VarNameAttr()) + "__boolterm__",
533 newType
, "a function introduced by Boolean-term conversion",
534 NodeManager::SKOLEM_EXACT_NAME
);
535 Debug("boolean-terms") << "constructed func: " << n
<< " of type " << newType
<< endl
;
536 top
.setAttribute(BooleanTermAttr(), n
);
537 NodeBuilder
<> boundVarsBuilder(kind::BOUND_VAR_LIST
);
538 NodeBuilder
<> bodyBuilder(kind::APPLY_UF
);
540 for(unsigned j
= 0; j
< t
.getNumChildren() - 1; ++j
) {
541 Node var
= nm
->mkBoundVar(t
[j
]);
542 boundVarsBuilder
<< var
;
543 if(t
[j
] != argTypes
[j
]) {
544 bodyBuilder
<< rewriteAs(var
, argTypes
[j
]);
549 Node boundVars
= boundVarsBuilder
;
550 Node body
= bodyBuilder
;
551 if(t
.getRangeType() != rangeType
) {
552 Node convbody
= rewriteAs(body
, t
.getRangeType());
555 Node lam
= nm
->mkNode(kind::LAMBDA
, boundVars
, body
);
556 Debug("boolean-terms") << "substituting " << top
<< " ==> " << lam
<< endl
;
557 d_smt
.d_theoryEngine
->getModel()->addSubstitution(top
, lam
);
564 } else if(t
.isArray()) {
565 TypeNode indexType
= convertType(t
.getArrayIndexType(), false);
566 TypeNode constituentType
= convertType(t
.getArrayConstituentType(), false);
567 if(indexType
!= t
.getArrayIndexType() && constituentType
== t
.getArrayConstituentType()) {
568 TypeNode newType
= nm
->mkArrayType(indexType
, constituentType
);
569 Node n
= nm
->mkSkolem(top
.getAttribute(expr::VarNameAttr()) + "'",
570 newType
, "an array variable introduced by Boolean-term conversion",
571 NodeManager::SKOLEM_EXACT_NAME
);
572 top
.setAttribute(BooleanTermAttr(), n
);
573 Debug("boolean-terms") << "constructed: " << n
<< " of type " << newType
<< endl
;
574 Node n_ff
= nm
->mkNode(kind::SELECT
, n
, d_ff
);
575 Node n_tt
= nm
->mkNode(kind::SELECT
, n
, d_tt
);
576 Node base
= nm
->mkConst(ArrayStoreAll(ArrayType(top
.getType().toType()), (*TypeEnumerator(n_ff
.getType())).toExpr()));
577 Node repl
= nm
->mkNode(kind::STORE
,
578 nm
->mkNode(kind::STORE
, base
, nm
->mkConst(true),
580 nm
->mkConst(false), n_ff
);
581 Debug("boolean-terms") << "array replacement: " << top
<< " => " << repl
<< endl
;
582 d_smt
.d_theoryEngine
->getModel()->addSubstitution(top
, repl
);
587 } else if(indexType
== t
.getArrayIndexType() && constituentType
!= t
.getArrayConstituentType()) {
588 TypeNode newType
= nm
->mkArrayType(indexType
, constituentType
);
589 Node n
= nm
->mkSkolem(top
.getAttribute(expr::VarNameAttr()) + "'",
590 newType
, "an array variable introduced by Boolean-term conversion",
591 NodeManager::SKOLEM_EXACT_NAME
);
592 top
.setAttribute(BooleanTermAttr(), n
);
593 Debug("boolean-terms") << "constructed: " << n
<< " of type " << newType
<< endl
;
594 d_smt
.d_theoryEngine
->getModel()->addSubstitution(top
, n
);
599 } else if(indexType
!= t
.getArrayIndexType() && constituentType
!= t
.getArrayConstituentType()) {
600 TypeNode newType
= nm
->mkArrayType(indexType
, constituentType
);
601 Node n
= nm
->mkSkolem(top
.getAttribute(expr::VarNameAttr()) + "'",
602 newType
, "an array variable introduced by Boolean-term conversion",
603 NodeManager::SKOLEM_EXACT_NAME
);
604 top
.setAttribute(BooleanTermAttr(), n
);
605 Debug("boolean-terms") << "constructed: " << n
<< " of type " << newType
<< endl
;
606 Node n_ff
= nm
->mkNode(kind::SELECT
, n
, d_ff
);
607 Node n_tt
= nm
->mkNode(kind::SELECT
, n
, d_tt
);
608 Node base
= nm
->mkConst(ArrayStoreAll(ArrayType(top
.getType().toType()), nm
->mkConst(false).toExpr()));
609 Node repl
= nm
->mkNode(kind::STORE
,
610 nm
->mkNode(kind::STORE
, base
, nm
->mkConst(false),
611 nm
->mkNode(kind::EQUAL
, n_ff
, d_tt
)), nm
->mkConst(true),
612 nm
->mkNode(kind::EQUAL
, n_tt
, d_tt
));
613 Debug("boolean-terms") << "array replacement: " << top
<< " => " << repl
<< endl
;
614 d_smt
.d_theoryEngine
->getModel()->addSubstitution(top
, repl
);
620 d_varCache
[top
] = Node::null();
624 } else if(t
.isTuple() || t
.isRecord()) {
625 TypeNode newType
= convertType(t
, true);
627 Node n
= nm
->mkSkolem(top
.getAttribute(expr::VarNameAttr()) + "'",
628 newType
, "a tuple/record variable introduced by Boolean-term conversion",
629 NodeManager::SKOLEM_EXACT_NAME
);
630 top
.setAttribute(BooleanTermAttr(), n
);
631 n
.setAttribute(BooleanTermAttr(), top
);
632 Debug("boolean-terms") << "adding subs: " << top
<< " :=> " << n
<< endl
;
633 d_smt
.d_theoryEngine
->getModel()->addSubstitution(top
, n
);
634 Debug("boolean-terms") << "constructed: " << n
<< " of type " << newType
<< endl
;
640 d_varCache
[top
] = Node::null();
644 } else if(t
.isDatatype() || t
.isParametricDatatype()) {
645 Debug("boolean-terms") << "found a var of datatype type" << endl
;
646 TypeNode newT
= convertType(t
, parentTheory
== theory::THEORY_DATATYPES
);
648 Assert(d_varCache
.find(top
) == d_varCache
.end(),
649 "Node `%s' already in cache ?!", top
.toString().c_str());
650 Node n
= nm
->mkSkolem(top
.getAttribute(expr::VarNameAttr()) + "'",
651 newT
, "a datatype variable introduced by Boolean-term conversion",
652 NodeManager::SKOLEM_EXACT_NAME
);
653 Debug("boolean-terms") << "adding subs: " << top
<< " :=> " << n
<< endl
;
654 top
.setAttribute(BooleanTermAttr(), n
);
655 d_smt
.d_theoryEngine
->getModel()->addSubstitution(top
, n
);
656 Debug("boolean-terms") << "constructed: " << n
<< " of type " << newT
<< endl
;
662 d_varCache
[top
] = Node::null();
667 } else if(t
.isConstructor()) {
668 Assert(parentTheory
!= theory::THEORY_BOOL
);
669 Assert(t
[t
.getNumChildren() - 1].getKind() == kind::DATATYPE_TYPE
||
670 t
[t
.getNumChildren() - 1].getKind() == kind::PARAMETRIC_DATATYPE
);
671 const Datatype
& dt
= t
[t
.getNumChildren() - 1].getKind() == kind::DATATYPE_TYPE
?
672 t
[t
.getNumChildren() - 1].getConst
<Datatype
>() :
673 t
[t
.getNumChildren() - 1][0].getConst
<Datatype
>();
674 TypeNode dt2type
= convertType(TypeNode::fromType(dt
.getDatatypeType()), parentTheory
== theory::THEORY_DATATYPES
);
675 const Datatype
& dt2
= (dt2type
.getKind() == kind::DATATYPE_TYPE
? dt2type
: dt2type
[0]).getConst
<Datatype
>();
677 Assert(d_varCache
.find(top
) != d_varCache
.end(),
678 "constructor `%s' not in cache", top
.toString().c_str());
679 result
.top() << d_varCache
[top
].get();
683 d_varCache
[top
] = Node::null();
687 } else if(t
.isTester() || t
.isSelector()) {
688 Assert(parentTheory
!= theory::THEORY_BOOL
);
689 const Datatype
& dt
= t
[0].getKind() == kind::DATATYPE_TYPE
?
690 t
[0].getConst
<Datatype
>() :
691 t
[0][0].getConst
<Datatype
>();
692 TypeNode dt2type
= convertType(TypeNode::fromType(dt
.getDatatypeType()), parentTheory
== theory::THEORY_DATATYPES
);
693 const Datatype
& dt2
= (dt2type
.getKind() == kind::DATATYPE_TYPE
? dt2type
: dt2type
[0]).getConst
<Datatype
>();
695 Assert(d_varCache
.find(top
) != d_varCache
.end(),
696 "tester or selector `%s' not in cache", top
.toString().c_str());
697 result
.top() << d_varCache
[top
].get();
701 d_varCache
[top
] = Node::null();
706 } else if(!t
.isSort() && t
.getNumChildren() > 0) {
707 for(TypeNode::iterator i
= t
.begin(); i
!= t
.end(); ++i
) {
708 if((*i
).isBoolean()) {
709 vector
<TypeNode
> argTypes(t
.begin(), t
.end());
710 replace(argTypes
.begin(), argTypes
.end(), *i
, d_tt
.getType());
711 TypeNode newType
= nm
->mkTypeNode(t
.getKind(), argTypes
);
712 Node n
= nm
->mkSkolem(top
.getAttribute(expr::VarNameAttr()),
713 newType
, "a variable introduced by Boolean-term conversion",
714 NodeManager::SKOLEM_EXACT_NAME
);
715 Debug("boolean-terms") << "constructed: " << n
<< " of type " << newType
<< endl
;
716 top
.setAttribute(BooleanTermAttr(), n
);
729 case kind::BOUND_VAR_LIST
:
734 case kind::REWRITE_RULE
:
735 case kind::RR_REWRITE
:
736 case kind::RR_DEDUCTION
:
737 case kind::RR_REDUCTION
:
745 Debug("bt") << "looking at quantifier -> " << top
<< endl
;
748 for(TNode::iterator i
= top
[0].begin(); i
!= top
[0].end(); ++i
) {
749 if((*i
).getType().isBoolean()) {
751 } else if(convertType((*i
).getType(), false) != (*i
).getType()) {
755 if(ourVars
.empty() && output
.empty()) {
756 // Simple case, quantifier doesn't quantify over Boolean vars,
757 // no special handling needed for quantifier. Fall through.
758 Debug("bt") << "- quantifier simple case (1), no Boolean vars bound" << endl
;
760 hash_set
< pair
<TNode
, bool>, PairHashFunction
<TNode
, bool, TNodeHashFunction
, BoolHashFunction
> > alreadySeen
;
761 collectVarsInTermContext(top
[1], ourVars
, output
, true, alreadySeen
);
763 // Simple case, quantifier quantifies over Boolean vars, but they
764 // don't occur in term context. Fall through.
765 Debug("bt") << "- quantifier simple case (2), Boolean vars bound but not used in term context" << endl
;
767 Debug("bt") << "- quantifier case (3), Boolean vars bound and used in term context" << endl
;
768 // We have Boolean vars appearing in term context. Convert their
769 // types in the quantifier.
770 for(set
<TNode
>::const_iterator i
= output
.begin(); i
!= output
.end(); ++i
) {
771 Node newVar
= nm
->mkBoundVar((*i
).toString(), convertType((*i
).getType(), false));
772 Assert(quantBoolVars
.find(*i
) == quantBoolVars
.end(), "bad quantifier: shares a bound var with another quantifier (don't do that!)");
773 quantBoolVars
[*i
] = newVar
;
775 vector
<TNode
> boundVars
;
776 for(TNode::iterator i
= top
[0].begin(); i
!= top
[0].end(); ++i
) {
777 map
<TNode
, Node
>::const_iterator j
= quantBoolVars
.find(*i
);
778 if(j
== quantBoolVars
.end()) {
779 boundVars
.push_back(*i
);
781 boundVars
.push_back((*j
).second
);
784 Node boundVarList
= nm
->mkNode(kind::BOUND_VAR_LIST
, boundVars
);
785 Node body
= rewriteBooleanTermsRec(top
[1], theory::THEORY_BOOL
, quantBoolVars
);
786 Node quant
= nm
->mkNode(top
.getKind(), boundVarList
, body
);
787 Debug("bt") << "rewrote quantifier to -> " << quant
<< endl
;
788 d_termCache
[make_pair(top
, theory::THEORY_BOOL
)] = quant
;
789 d_termCache
[make_pair(top
, theory::THEORY_BUILTIN
)] = quant
.iteNode(d_tt
, d_ff
);
790 d_termCache
[make_pair(top
, theory::THEORY_DATATYPES
)] = quant
.iteNode(d_tt
, d_ff
);
791 result
.top() << quant
;
796 /* intentional fall-through for some cases above */
800 result
.push(NodeBuilder
<>(k
));
801 Debug("bt") << "looking at: " << top
<< endl
;
802 // rewrite the operator, as necessary
803 if(mk
== kind::metakind::PARAMETERIZED
) {
804 if(k
== kind::RECORD
) {
805 result
.top() << convertType(top
.getType(), parentTheory
== theory::THEORY_DATATYPES
);
806 } else if(k
== kind::APPLY_TYPE_ASCRIPTION
) {
807 Node asc
= nm
->mkConst(AscriptionType(convertType(TypeNode::fromType(top
.getOperator().getConst
<AscriptionType
>().getType()), parentTheory
== theory::THEORY_DATATYPES
).toType()));
809 Debug("boolean-terms") << "setting " << top
.getOperator() << ":" << top
.getOperator().getId() << " to point to " << asc
<< ":" << asc
.getId() << endl
;
810 asc
.setAttribute(BooleanTermAttr(), top
.getOperator());
811 } else if(kindToTheoryId(k
) != THEORY_BV
&&
812 k
!= kind::TUPLE_SELECT
&&
813 k
!= kind::TUPLE_UPDATE
&&
814 k
!= kind::RECORD_SELECT
&&
815 k
!= kind::RECORD_UPDATE
&&
816 k
!= kind::DIVISIBLE
) {
817 Debug("bt") << "rewriting: " << top
.getOperator() << endl
;
818 result
.top() << rewriteBooleanTermsRec(top
.getOperator(), theory::THEORY_BUILTIN
, quantBoolVars
);
819 Debug("bt") << "got: " << result
.top().getOperator() << endl
;
821 result
.top() << top
.getOperator();
825 for(int i
= top
.getNumChildren() - 1; i
>= 0; --i
) {
826 Debug("bt") << "rewriting: " << top
[i
] << endl
;
827 worklist
.push(triple
<TNode
, theory::TheoryId
, bool>(top
[i
], top
.getKind() == kind::CHAIN
? parentTheory
: (isBoolean(top
, i
) ? theory::THEORY_BOOL
: (top
.getKind() == kind::APPLY_CONSTRUCTOR
? theory::THEORY_DATATYPES
: theory::THEORY_BUILTIN
)), false));
828 //b << rewriteBooleanTermsRec(top[i], isBoolean(top, i) ? , quantBoolVars);
829 //Debug("bt") << "got: " << b[b.getNumChildren() - 1] << endl;
831 childrenPushed
= true;
834 Node n
= result
.top();
836 Debug("boolean-terms") << "constructed: " << n
<< endl
;
837 if(parentTheory
== theory::THEORY_BOOL
) {
838 if(n
.getType().isBitVector() &&
839 n
.getType().getBitVectorSize() == 1) {
840 n
= nm
->mkNode(kind::EQUAL
, n
, d_tt
);
841 } else if(n
.getType().isDatatype() &&
842 n
.getType().hasAttribute(BooleanTermAttr())) {
843 n
= nm
->mkNode(kind::EQUAL
, n
, d_ttDt
);
846 d_termCache
[make_pair(top
, parentTheory
)] = n
;
856 Assert(worklist
.size() == 0);
857 Assert(result
.size() == 1);
858 Node retval
= result
.top()[0];
859 result
.top().clear();
863 }/* BooleanTermConverter::rewriteBooleanTermsRec() */
865 }/* CVC4::smt namespace */
866 }/* CVC4 namespace */