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 Node::fromExpr(newD
[(*c
).getName() + "'"].getConstructor()).setAttribute(BooleanTermAttr(), Node::fromExpr((*c
).getConstructor()));// other attr?
286 Debug("boolean-terms") << "mapped " << newD
[(*c
).getName() + "'"].getConstructor() << " to " << (*c
).getConstructor() << endl
;
287 d_varCache
[Node::fromExpr((*c
).getConstructor())] = Node::fromExpr(newD
[(*c
).getName() + "'"].getConstructor());
288 d_varCache
[Node::fromExpr((*c
).getTester())] = Node::fromExpr(newD
[(*c
).getName() + "'"].getTester());
289 for(DatatypeConstructor::const_iterator a
= (*c
).begin(); a
!= (*c
).end(); ++a
) {
290 d_varCache
[Node::fromExpr((*a
).getSelector())] = Node::fromExpr(newD
[(*c
).getName() + "'"].getSelector((*a
).getName() + "'"));
294 d_datatypeReverseCache
[&newD
] = &dt
;
300 // this is identity; don't need the reverse cache
304 }/* BooleanTermConverter::convertDatatype() */
306 TypeNode
BooleanTermConverter::convertType(TypeNode type
, bool datatypesContext
) {
307 Debug("boolean-terms") << "CONVERT-TYPE[" << type
<< ":" << type
.getId() << ", " << datatypesContext
<< "]" << endl
;
308 // This function recursively converts the type.
309 if(type
.isBoolean()) {
310 return datatypesContext
? d_ttDt
.getType() : d_tt
.getType();
312 const pair
<TypeNode
, bool> cacheKey(type
, datatypesContext
);
313 if(d_typeCache
.find(cacheKey
) != d_typeCache
.end()) {
314 TypeNode out
= d_typeCache
[cacheKey
];
315 return out
.isNull() ? type
: out
;
317 TypeNode
& outNode
= d_typeCache
[cacheKey
];
318 if(type
.getKind() == kind::DATATYPE_TYPE
||
319 type
.getKind() == kind::PARAMETRIC_DATATYPE
) {
320 bool parametric
= (type
.getKind() == kind::PARAMETRIC_DATATYPE
);
321 const Datatype
& dt
= parametric
? type
[0].getConst
<Datatype
>() : type
.getConst
<Datatype
>();
322 TypeNode out
= TypeNode::fromType(convertDatatype(dt
).getDatatypeType());
323 Debug("boolean-terms") << "AFTER, got "<< out
<< " param:" << parametric
<< endl
;
325 // re-parameterize the translation
326 vector
<TypeNode
> params
= type
.getParamTypes();
327 for(size_t i
= 0; i
< params
.size(); ++i
) {
328 Debug("boolean-terms") << "in loop, got "<< params
[i
] << endl
;
329 params
[i
] = convertType(params
[i
], true);
330 Debug("boolean-terms") << "in loop, convert to "<< params
[i
] << endl
;
332 params
.insert(params
.begin(), out
[0]);
333 out
= NodeManager::currentNM()->mkTypeNode(kind::PARAMETRIC_DATATYPE
, params
);
334 Debug("boolean-terms") << "got OUT: " << out
<< endl
;
337 outNode
= out
;// cache it
338 Debug("boolean-terms") << "OUT is same as TYPE" << endl
;
339 } else Debug("boolean-terms") << "OUT is DIFFERENT FROM TYPE" << endl
;
342 if(type
.isRecord()) {
343 const Record
& rec
= type
.getConst
<Record
>();
344 vector
< pair
<string
, Type
> > flds
;
345 for(Record::const_iterator i
= rec
.begin(); i
!= rec
.end(); ++i
) {
346 TypeNode converted
= convertType(TypeNode::fromType((*i
).second
), true);
347 if(TypeNode::fromType((*i
).second
) != converted
) {
348 flds
.push_back(make_pair((*i
).first
, converted
.toType()));
353 TypeNode newRec
= NodeManager::currentNM()->mkRecordType(Record(flds
));
354 Debug("tuprec") << "converted " << type
<< " to " << newRec
<< endl
;
356 outNode
= newRec
;// cache it
360 if(!type
.isSort() && type
.getNumChildren() > 0) {
361 Debug("boolean-terms") << "here at A for " << type
<< ":" << type
.getId() << endl
;
362 // This should handle tuples and arrays ok.
363 // Might handle function types too, but they can't go
364 // in other types, so it doesn't matter.
365 NodeBuilder
<> b(type
.getKind());
366 if(type
.getMetaKind() == kind::metakind::PARAMETERIZED
) {
367 b
<< type
.getOperator();
369 for(TypeNode::iterator i
= type
.begin(); i
!= type
.end(); ++i
) {
370 b
<< convertType(*i
, false);
374 outNode
= out
;// cache it
376 Debug("boolean-terms") << "here at B, returning " << out
<< ":" << out
.getId() << endl
;
379 // leave the cache at Null
381 }/* BooleanTermConverter::convertType() */
383 // look for vars from "vars" that occur in a term-context in n; transfer them to output.
384 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
) {
388 const pair
<TNode
, bool> cacheKey(n
, boolParent
);
389 if(alreadySeen
.find(cacheKey
) != alreadySeen
.end()) {
392 alreadySeen
.insert(cacheKey
);
394 if(n
.isVar() && vars
.find(n
) != vars
.end() && !boolParent
) {
401 for(size_t i
= 0; i
< n
.getNumChildren(); ++i
) {
402 collectVarsInTermContext(n
[i
], vars
, output
, isBoolean(n
, i
), alreadySeen
);
409 Node
BooleanTermConverter::rewriteBooleanTermsRec(TNode top
, theory::TheoryId parentTheory
, std::map
<TNode
, Node
>& quantBoolVars
) throw() {
411 stack
< triple
<TNode
, theory::TheoryId
, bool> > worklist
;
412 worklist
.push(triple
<TNode
, theory::TheoryId
, bool>(top
, parentTheory
, false));
413 stack
< NodeBuilder
<> > result
;
414 result
.push(NodeBuilder
<>(kind::TUPLE
));
416 NodeManager
* nm
= NodeManager::currentNM();
418 while(!worklist
.empty()) {
419 top
= worklist
.top().first
;
420 parentTheory
= worklist
.top().second
;
421 bool& childrenPushed
= worklist
.top().third
;
423 Kind k
= top
.getKind();
424 kind::MetaKind mk
= top
.getMetaKind();
426 // we only distinguish between datatypes, booleans, and "other", and we
427 // don't even distinguish datatypes except when in "native" conversion
429 if(parentTheory
!= theory::THEORY_BOOL
) {
430 if(options::booleanTermConversionMode() != BOOLEAN_TERM_CONVERT_NATIVE
||
431 parentTheory
!= theory::THEORY_DATATYPES
) {
432 parentTheory
= theory::THEORY_BUILTIN
;
436 if(!childrenPushed
) {
437 Debug("boolean-terms") << "rewriteBooleanTermsRec: " << top
<< " - parentTheory=" << parentTheory
<< endl
;
439 BooleanTermVarCache::iterator i
= d_varCache
.find(top
);
440 if(i
!= d_varCache
.end()) {
441 result
.top() << ((*i
).second
.isNull() ? Node(top
) : (*i
).second
);
445 BooleanTermCache::iterator j
= d_termCache
.find(pair
<Node
, theory::TheoryId
>(top
, parentTheory
));
446 if(j
!= d_termCache
.end()) {
447 result
.top() << ((*j
).second
.isNull() ? Node(top
) : (*j
).second
);
452 if(quantBoolVars
.find(top
) != quantBoolVars
.end()) {
453 // this Bool variable is quantified over and we're changing it to a BitVector var
454 if(parentTheory
== theory::THEORY_BOOL
) {
455 result
.top() << quantBoolVars
[top
].eqNode(d_tt
);
457 result
.top() << quantBoolVars
[top
];
463 if(parentTheory
!= theory::THEORY_BOOL
&& top
.getType().isBoolean()) {
464 // still need to rewrite e.g. function applications over boolean
465 Node topRewritten
= rewriteBooleanTermsRec(top
, theory::THEORY_BOOL
, quantBoolVars
);
467 if(parentTheory
== theory::THEORY_DATATYPES
) {
468 n
= nm
->mkNode(kind::ITE
, topRewritten
, d_ttDt
, d_ffDt
);
470 n
= nm
->mkNode(kind::ITE
, topRewritten
, d_tt
, d_ff
);
472 Debug("boolean-terms") << "constructed ITE: " << n
<< endl
;
478 if(mk
== kind::metakind::CONSTANT
) {
479 if(k
== kind::STORE_ALL
) {
480 const ArrayStoreAll
& asa
= top
.getConst
<ArrayStoreAll
>();
481 ArrayType arrType
= asa
.getType();
482 TypeNode indexType
= TypeNode::fromType(arrType
.getIndexType());
483 Type constituentType
= arrType
.getConstituentType();
484 if(constituentType
.isBoolean()) {
485 // we have store_all(true) or store_all(false)
486 // just turn it into store_all(1) or store_all(0)
487 if(indexType
.isBoolean()) {
488 // change index type to BV(1) also
489 indexType
= d_tt
.getType();
491 ArrayStoreAll
asaRepl(nm
->mkArrayType(indexType
, d_tt
.getType()).toType(),
492 (asa
.getExpr().getConst
<bool>() ? d_tt
: d_ff
).toExpr());
493 Node n
= nm
->mkConst(asaRepl
);
494 Debug("boolean-terms") << " returning new store_all: " << n
<< endl
;
499 if(indexType
.isBoolean()) {
500 // must change index type to BV(1)
501 indexType
= d_tt
.getType();
502 ArrayStoreAll
asaRepl(nm
->mkArrayType(indexType
, TypeNode::fromType(constituentType
)).toType(), asa
.getExpr());
503 Node n
= nm
->mkConst(asaRepl
);
504 Debug("boolean-terms") << " returning new store_all: " << n
<< endl
;
513 } else if(mk
== kind::metakind::VARIABLE
) {
514 TypeNode t
= top
.getType();
516 for(unsigned i
= 0; i
< t
.getNumChildren(); ++i
) {
517 TypeNode newType
= convertType(t
[i
], false);
518 // is this the return type? (allowed to be Bool)
519 bool returnType
= (i
== t
.getNumChildren() - 1);
520 if(newType
!= t
[i
] && (!t
[i
].isBoolean() || !returnType
)) {
521 vector
<TypeNode
> argTypes
= t
.getArgTypes();
522 for(unsigned j
= 0; j
< argTypes
.size(); ++j
) {
523 argTypes
[j
] = convertType(argTypes
[j
], false);
525 TypeNode rangeType
= t
.getRangeType();
526 if(!rangeType
.isBoolean()) {
527 rangeType
= convertType(rangeType
, false);
529 TypeNode newType
= nm
->mkFunctionType(argTypes
, rangeType
);
530 Node n
= nm
->mkSkolem(top
.getAttribute(expr::VarNameAttr()) + "__boolterm__",
531 newType
, "a function introduced by Boolean-term conversion",
532 NodeManager::SKOLEM_EXACT_NAME
);
533 Debug("boolean-terms") << "constructed func: " << n
<< " of type " << newType
<< endl
;
534 top
.setAttribute(BooleanTermAttr(), n
);
535 NodeBuilder
<> boundVarsBuilder(kind::BOUND_VAR_LIST
);
536 NodeBuilder
<> bodyBuilder(kind::APPLY_UF
);
538 for(unsigned j
= 0; j
< t
.getNumChildren() - 1; ++j
) {
539 Node var
= nm
->mkBoundVar(t
[j
]);
540 boundVarsBuilder
<< var
;
541 if(t
[j
] != argTypes
[j
]) {
542 bodyBuilder
<< rewriteAs(var
, argTypes
[j
]);
547 Node boundVars
= boundVarsBuilder
;
548 Node body
= bodyBuilder
;
549 if(t
.getRangeType() != rangeType
) {
550 Node convbody
= rewriteAs(body
, t
.getRangeType());
553 Node lam
= nm
->mkNode(kind::LAMBDA
, boundVars
, body
);
554 Debug("boolean-terms") << "substituting " << top
<< " ==> " << lam
<< endl
;
555 d_smt
.d_theoryEngine
->getModel()->addSubstitution(top
, lam
);
562 } else if(t
.isArray()) {
563 TypeNode indexType
= convertType(t
.getArrayIndexType(), false);
564 TypeNode constituentType
= convertType(t
.getArrayConstituentType(), false);
565 if(indexType
!= t
.getArrayIndexType() && constituentType
== t
.getArrayConstituentType()) {
566 TypeNode newType
= nm
->mkArrayType(indexType
, constituentType
);
567 Node n
= nm
->mkSkolem(top
.getAttribute(expr::VarNameAttr()) + "'",
568 newType
, "an array variable introduced by Boolean-term conversion",
569 NodeManager::SKOLEM_EXACT_NAME
);
570 top
.setAttribute(BooleanTermAttr(), n
);
571 Debug("boolean-terms") << "constructed: " << n
<< " of type " << newType
<< endl
;
572 Node n_ff
= nm
->mkNode(kind::SELECT
, n
, d_ff
);
573 Node n_tt
= nm
->mkNode(kind::SELECT
, n
, d_tt
);
574 Node base
= nm
->mkConst(ArrayStoreAll(ArrayType(top
.getType().toType()), (*TypeEnumerator(n_ff
.getType())).toExpr()));
575 Node repl
= nm
->mkNode(kind::STORE
,
576 nm
->mkNode(kind::STORE
, base
, nm
->mkConst(true),
578 nm
->mkConst(false), n_ff
);
579 Debug("boolean-terms") << "array replacement: " << top
<< " => " << repl
<< endl
;
580 d_smt
.d_theoryEngine
->getModel()->addSubstitution(top
, repl
);
585 } else if(indexType
== t
.getArrayIndexType() && constituentType
!= t
.getArrayConstituentType()) {
586 TypeNode newType
= nm
->mkArrayType(indexType
, constituentType
);
587 Node n
= nm
->mkSkolem(top
.getAttribute(expr::VarNameAttr()) + "'",
588 newType
, "an array variable introduced by Boolean-term conversion",
589 NodeManager::SKOLEM_EXACT_NAME
);
590 top
.setAttribute(BooleanTermAttr(), n
);
591 Debug("boolean-terms") << "constructed: " << n
<< " of type " << newType
<< endl
;
592 d_smt
.d_theoryEngine
->getModel()->addSubstitution(top
, n
);
597 } else if(indexType
!= t
.getArrayIndexType() && constituentType
!= t
.getArrayConstituentType()) {
598 TypeNode newType
= nm
->mkArrayType(indexType
, constituentType
);
599 Node n
= nm
->mkSkolem(top
.getAttribute(expr::VarNameAttr()) + "'",
600 newType
, "an array variable introduced by Boolean-term conversion",
601 NodeManager::SKOLEM_EXACT_NAME
);
602 top
.setAttribute(BooleanTermAttr(), n
);
603 Debug("boolean-terms") << "constructed: " << n
<< " of type " << newType
<< endl
;
604 Node n_ff
= nm
->mkNode(kind::SELECT
, n
, d_ff
);
605 Node n_tt
= nm
->mkNode(kind::SELECT
, n
, d_tt
);
606 Node base
= nm
->mkConst(ArrayStoreAll(ArrayType(top
.getType().toType()), nm
->mkConst(false).toExpr()));
607 Node repl
= nm
->mkNode(kind::STORE
,
608 nm
->mkNode(kind::STORE
, base
, nm
->mkConst(false),
609 nm
->mkNode(kind::EQUAL
, n_ff
, d_tt
)), nm
->mkConst(true),
610 nm
->mkNode(kind::EQUAL
, n_tt
, d_tt
));
611 Debug("boolean-terms") << "array replacement: " << top
<< " => " << repl
<< endl
;
612 d_smt
.d_theoryEngine
->getModel()->addSubstitution(top
, repl
);
618 d_varCache
[top
] = Node::null();
622 } else if(t
.isTuple() || t
.isRecord()) {
623 TypeNode newType
= convertType(t
, true);
625 Node n
= nm
->mkSkolem(top
.getAttribute(expr::VarNameAttr()) + "'",
626 newType
, "a tuple/record variable introduced by Boolean-term conversion",
627 NodeManager::SKOLEM_EXACT_NAME
);
628 top
.setAttribute(BooleanTermAttr(), n
);
629 n
.setAttribute(BooleanTermAttr(), top
);
630 Debug("boolean-terms") << "adding subs: " << top
<< " :=> " << n
<< endl
;
631 d_smt
.d_theoryEngine
->getModel()->addSubstitution(top
, n
);
632 Debug("boolean-terms") << "constructed: " << n
<< " of type " << newType
<< endl
;
638 d_varCache
[top
] = Node::null();
642 } else if(t
.isDatatype() || t
.isParametricDatatype()) {
643 Debug("boolean-terms") << "found a var of datatype type" << endl
;
644 TypeNode newT
= convertType(t
, parentTheory
== theory::THEORY_DATATYPES
);
646 Assert(d_varCache
.find(top
) == d_varCache
.end(),
647 "Node `%s' already in cache ?!", top
.toString().c_str());
648 Node n
= nm
->mkSkolem(top
.getAttribute(expr::VarNameAttr()) + "'",
649 newT
, "a datatype variable introduced by Boolean-term conversion",
650 NodeManager::SKOLEM_EXACT_NAME
);
651 Debug("boolean-terms") << "adding subs: " << top
<< " :=> " << n
<< endl
;
652 top
.setAttribute(BooleanTermAttr(), n
);
653 d_smt
.d_theoryEngine
->getModel()->addSubstitution(top
, n
);
654 Debug("boolean-terms") << "constructed: " << n
<< " of type " << newT
<< endl
;
660 d_varCache
[top
] = Node::null();
665 } else if(t
.isConstructor()) {
666 Assert(parentTheory
!= theory::THEORY_BOOL
);
667 Assert(t
[t
.getNumChildren() - 1].getKind() == kind::DATATYPE_TYPE
||
668 t
[t
.getNumChildren() - 1].getKind() == kind::PARAMETRIC_DATATYPE
);
669 const Datatype
& dt
= t
[t
.getNumChildren() - 1].getKind() == kind::DATATYPE_TYPE
?
670 t
[t
.getNumChildren() - 1].getConst
<Datatype
>() :
671 t
[t
.getNumChildren() - 1][0].getConst
<Datatype
>();
672 TypeNode dt2type
= convertType(TypeNode::fromType(dt
.getDatatypeType()), parentTheory
== theory::THEORY_DATATYPES
);
673 const Datatype
& dt2
= (dt2type
.getKind() == kind::DATATYPE_TYPE
? dt2type
: dt2type
[0]).getConst
<Datatype
>();
675 Assert(d_varCache
.find(top
) != d_varCache
.end(),
676 "constructor `%s' not in cache", top
.toString().c_str());
677 result
.top() << d_varCache
[top
].get();
681 d_varCache
[top
] = Node::null();
685 } else if(t
.isTester() || t
.isSelector()) {
686 Assert(parentTheory
!= theory::THEORY_BOOL
);
687 const Datatype
& dt
= t
[0].getKind() == kind::DATATYPE_TYPE
?
688 t
[0].getConst
<Datatype
>() :
689 t
[0][0].getConst
<Datatype
>();
690 TypeNode dt2type
= convertType(TypeNode::fromType(dt
.getDatatypeType()), parentTheory
== theory::THEORY_DATATYPES
);
691 const Datatype
& dt2
= (dt2type
.getKind() == kind::DATATYPE_TYPE
? dt2type
: dt2type
[0]).getConst
<Datatype
>();
693 Assert(d_varCache
.find(top
) != d_varCache
.end(),
694 "tester or selector `%s' not in cache", top
.toString().c_str());
695 result
.top() << d_varCache
[top
].get();
699 d_varCache
[top
] = Node::null();
704 } else if(!t
.isSort() && t
.getNumChildren() > 0) {
705 for(TypeNode::iterator i
= t
.begin(); i
!= t
.end(); ++i
) {
706 if((*i
).isBoolean()) {
707 vector
<TypeNode
> argTypes(t
.begin(), t
.end());
708 replace(argTypes
.begin(), argTypes
.end(), *i
, d_tt
.getType());
709 TypeNode newType
= nm
->mkTypeNode(t
.getKind(), argTypes
);
710 Node n
= nm
->mkSkolem(top
.getAttribute(expr::VarNameAttr()),
711 newType
, "a variable introduced by Boolean-term conversion",
712 NodeManager::SKOLEM_EXACT_NAME
);
713 Debug("boolean-terms") << "constructed: " << n
<< " of type " << newType
<< endl
;
714 top
.setAttribute(BooleanTermAttr(), n
);
727 case kind::BOUND_VAR_LIST
:
732 case kind::REWRITE_RULE
:
733 case kind::RR_REWRITE
:
734 case kind::RR_DEDUCTION
:
735 case kind::RR_REDUCTION
:
743 Debug("bt") << "looking at quantifier -> " << top
<< endl
;
746 for(TNode::iterator i
= top
[0].begin(); i
!= top
[0].end(); ++i
) {
747 if((*i
).getType().isBoolean()) {
749 } else if(convertType((*i
).getType(), false) != (*i
).getType()) {
753 if(ourVars
.empty() && output
.empty()) {
754 // Simple case, quantifier doesn't quantify over Boolean vars,
755 // no special handling needed for quantifier. Fall through.
756 Debug("bt") << "- quantifier simple case (1), no Boolean vars bound" << endl
;
758 hash_set
< pair
<TNode
, bool>, PairHashFunction
<TNode
, bool, TNodeHashFunction
, BoolHashFunction
> > alreadySeen
;
759 collectVarsInTermContext(top
[1], ourVars
, output
, true, alreadySeen
);
761 // Simple case, quantifier quantifies over Boolean vars, but they
762 // don't occur in term context. Fall through.
763 Debug("bt") << "- quantifier simple case (2), Boolean vars bound but not used in term context" << endl
;
765 Debug("bt") << "- quantifier case (3), Boolean vars bound and used in term context" << endl
;
766 // We have Boolean vars appearing in term context. Convert their
767 // types in the quantifier.
768 for(set
<TNode
>::const_iterator i
= output
.begin(); i
!= output
.end(); ++i
) {
769 Node newVar
= nm
->mkBoundVar((*i
).toString(), convertType((*i
).getType(), false));
770 Assert(quantBoolVars
.find(*i
) == quantBoolVars
.end(), "bad quantifier: shares a bound var with another quantifier (don't do that!)");
771 quantBoolVars
[*i
] = newVar
;
773 vector
<TNode
> boundVars
;
774 for(TNode::iterator i
= top
[0].begin(); i
!= top
[0].end(); ++i
) {
775 map
<TNode
, Node
>::const_iterator j
= quantBoolVars
.find(*i
);
776 if(j
== quantBoolVars
.end()) {
777 boundVars
.push_back(*i
);
779 boundVars
.push_back((*j
).second
);
782 Node boundVarList
= nm
->mkNode(kind::BOUND_VAR_LIST
, boundVars
);
783 Node body
= rewriteBooleanTermsRec(top
[1], theory::THEORY_BOOL
, quantBoolVars
);
784 Node quant
= nm
->mkNode(top
.getKind(), boundVarList
, body
);
785 Debug("bt") << "rewrote quantifier to -> " << quant
<< endl
;
786 d_termCache
[make_pair(top
, theory::THEORY_BOOL
)] = quant
;
787 d_termCache
[make_pair(top
, theory::THEORY_BUILTIN
)] = quant
.iteNode(d_tt
, d_ff
);
788 d_termCache
[make_pair(top
, theory::THEORY_DATATYPES
)] = quant
.iteNode(d_tt
, d_ff
);
789 result
.top() << quant
;
794 /* intentional fall-through for some cases above */
798 result
.push(NodeBuilder
<>(k
));
799 Debug("bt") << "looking at: " << top
<< endl
;
800 // rewrite the operator, as necessary
801 if(mk
== kind::metakind::PARAMETERIZED
) {
802 if(k
== kind::RECORD
) {
803 result
.top() << convertType(top
.getType(), parentTheory
== theory::THEORY_DATATYPES
);
804 } else if(k
== kind::APPLY_TYPE_ASCRIPTION
) {
805 Node asc
= nm
->mkConst(AscriptionType(convertType(TypeNode::fromType(top
.getOperator().getConst
<AscriptionType
>().getType()), parentTheory
== theory::THEORY_DATATYPES
).toType()));
807 Debug("boolean-terms") << "setting " << top
.getOperator() << ":" << top
.getOperator().getId() << " to point to " << asc
<< ":" << asc
.getId() << endl
;
808 asc
.setAttribute(BooleanTermAttr(), top
.getOperator());
809 } else if(kindToTheoryId(k
) != THEORY_BV
&&
810 k
!= kind::TUPLE_SELECT
&&
811 k
!= kind::TUPLE_UPDATE
&&
812 k
!= kind::RECORD_SELECT
&&
813 k
!= kind::RECORD_UPDATE
&&
814 k
!= kind::DIVISIBLE
) {
815 Debug("bt") << "rewriting: " << top
.getOperator() << endl
;
816 result
.top() << rewriteBooleanTermsRec(top
.getOperator(), theory::THEORY_BUILTIN
, quantBoolVars
);
817 Debug("bt") << "got: " << result
.top().getOperator() << endl
;
819 result
.top() << top
.getOperator();
823 for(int i
= top
.getNumChildren() - 1; i
>= 0; --i
) {
824 Debug("bt") << "rewriting: " << top
[i
] << endl
;
825 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));
826 //b << rewriteBooleanTermsRec(top[i], isBoolean(top, i) ? , quantBoolVars);
827 //Debug("bt") << "got: " << b[b.getNumChildren() - 1] << endl;
829 childrenPushed
= true;
832 Node n
= result
.top();
834 Debug("boolean-terms") << "constructed: " << n
<< endl
;
835 if(parentTheory
== theory::THEORY_BOOL
) {
836 if(n
.getType().isBitVector() &&
837 n
.getType().getBitVectorSize() == 1) {
838 n
= nm
->mkNode(kind::EQUAL
, n
, d_tt
);
839 } else if(n
.getType().isDatatype() &&
840 n
.getType().hasAttribute(BooleanTermAttr())) {
841 n
= nm
->mkNode(kind::EQUAL
, n
, d_ttDt
);
844 d_termCache
[make_pair(top
, parentTheory
)] = n
;
854 Assert(worklist
.size() == 0);
855 Assert(result
.size() == 1);
856 Node retval
= result
.top()[0];
857 result
.top().clear();
861 }/* BooleanTermConverter::rewriteBooleanTermsRec() */
863 }/* CVC4::smt namespace */
864 }/* CVC4 namespace */