1 /********************* */
2 /*! \file quantifiers_rewriter.cpp
4 ** Original author: Morgan Deters
5 ** Major contributors: Andrew Reynolds
6 ** Minor contributors (to current version): Tim King
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 Implementation of QuantifiersRewriter class
15 #include "theory/quantifiers/quantifiers_rewriter.h"
16 #include "theory/quantifiers/options.h"
17 #include "theory/quantifiers/term_database.h"
18 #include "theory/datatypes/datatypes_rewriter.h"
22 using namespace CVC4::kind
;
23 using namespace CVC4::context
;
24 using namespace CVC4::theory
;
25 using namespace CVC4::theory::quantifiers
;
27 bool QuantifiersRewriter::isClause( Node n
){
30 }else if( n
.getKind()==NOT
){
31 return isCube( n
[0] );
32 }else if( n
.getKind()==OR
){
33 for( int i
=0; i
<(int)n
.getNumChildren(); i
++ ){
34 if( !isClause( n
[i
] ) ){
39 }else if( n
.getKind()==IMPLIES
){
40 return isCube( n
[0] ) && isClause( n
[1] );
46 bool QuantifiersRewriter::isLiteral( Node n
){
47 switch( n
.getKind() ){
49 return isLiteral( n
[0] );
60 return n
[0].getType()!=NodeManager::currentNM()->booleanType();
68 bool QuantifiersRewriter::isCube( Node n
){
71 }else if( n
.getKind()==NOT
){
72 return isClause( n
[0] );
73 }else if( n
.getKind()==AND
){
74 for( int i
=0; i
<(int)n
.getNumChildren(); i
++ ){
75 if( !isCube( n
[i
] ) ){
85 void QuantifiersRewriter::addNodeToOrBuilder( Node n
, NodeBuilder
<>& t
){
86 if( n
.getKind()==OR
){
87 for( int i
=0; i
<(int)n
.getNumChildren(); i
++ ){
95 void QuantifiersRewriter::computeArgs( std::vector
< Node
>& args
, std::map
< Node
, bool >& activeMap
, Node n
){
96 if( n
.getKind()==BOUND_VARIABLE
){
97 if( std::find( args
.begin(), args
.end(), n
)!=args
.end() ){
98 activeMap
[ n
] = true;
101 for( int i
=0; i
<(int)n
.getNumChildren(); i
++ ){
102 computeArgs( args
, activeMap
, n
[i
] );
107 void QuantifiersRewriter::computeArgVec( std::vector
< Node
>& args
, std::vector
< Node
>& activeArgs
, Node n
) {
108 std::map
< Node
, bool > activeMap
;
109 computeArgs( args
, activeMap
, n
);
110 for( unsigned i
=0; i
<args
.size(); i
++ ){
111 if( activeMap
[args
[i
]] ){
112 activeArgs
.push_back( args
[i
] );
118 bool QuantifiersRewriter::hasArg( std::vector
< Node
>& args
, Node n
){
119 if( std::find( args
.begin(), args
.end(), n
)!=args
.end() ){
122 for( int i
=0; i
<(int)n
.getNumChildren(); i
++ ){
123 if( hasArg( args
, n
[i
] ) ){
131 void QuantifiersRewriter::setNestedQuantifiers( Node n
, Node q
){
132 std::vector
< Node
> processed
;
133 setNestedQuantifiers2( n
, q
, processed
);
136 void QuantifiersRewriter::setNestedQuantifiers2( Node n
, Node q
, std::vector
< Node
>& processed
) {
137 if( std::find( processed
.begin(), processed
.end(), n
)==processed
.end() ){
138 processed
.push_back( n
);
139 if( n
.getKind()==FORALL
|| n
.getKind()==EXISTS
){
140 Trace("quantifiers-rewrite-debug") << "Set nested quant attribute " << n
<< std::endl
;
141 NestedQuantAttribute nqai
;
142 n
[0].setAttribute(nqai
,q
);
144 for( int i
=0; i
<(int)n
.getNumChildren(); i
++ ){
145 setNestedQuantifiers2( n
[i
], q
, processed
);
150 RewriteResponse
QuantifiersRewriter::preRewrite(TNode in
) {
151 if( in
.getKind()==kind::EXISTS
|| in
.getKind()==kind::FORALL
){
152 Trace("quantifiers-rewrite-debug") << "pre-rewriting " << in
<< " " << in
[0].hasAttribute(NestedQuantAttribute()) << std::endl
;
153 if( !in
.hasAttribute(NestedQuantAttribute()) ){
154 setNestedQuantifiers( in
[ 1 ], in
);
156 std::vector
< Node
> args
;
157 for( int i
=0; i
<(int)in
[0].getNumChildren(); i
++ ){
158 args
.push_back( in
[0][i
] );
161 bool doRewrite
= false;
162 std::vector
< Node
> ipl
;
163 while( body
.getNumChildren()>=2 && body
.getKind()==in
.getKind() ){
164 if( body
.getNumChildren()==3 ){
165 for( unsigned i
=0; i
<body
[2].getNumChildren(); i
++ ){
166 ipl
.push_back( body
[2][i
] );
169 for( int i
=0; i
<(int)body
[0].getNumChildren(); i
++ ){
170 args
.push_back( body
[0][i
] );
176 std::vector
< Node
> children
;
177 children
.push_back( NodeManager::currentNM()->mkNode(kind::BOUND_VAR_LIST
,args
) );
178 children
.push_back( body
);
179 if( in
.getNumChildren()==3 ){
180 for( unsigned i
=0; i
<in
[2].getNumChildren(); i
++ ){
181 ipl
.push_back( in
[2][i
] );
185 children
.push_back( NodeManager::currentNM()->mkNode( INST_PATTERN_LIST
, ipl
) );
187 Node n
= NodeManager::currentNM()->mkNode( in
.getKind(), children
);
189 setAttributes( in
, n
);
190 Trace("quantifiers-pre-rewrite") << "*** pre-rewrite " << in
<< std::endl
;
191 Trace("quantifiers-pre-rewrite") << " to " << std::endl
;
192 Trace("quantifiers-pre-rewrite") << n
<< std::endl
;
194 return RewriteResponse(REWRITE_DONE
, n
);
197 return RewriteResponse(REWRITE_DONE
, in
);
200 RewriteResponse
QuantifiersRewriter::postRewrite(TNode in
) {
201 Trace("quantifiers-rewrite-debug") << "post-rewriting " << in
<< std::endl
;
202 Trace("quantifiers-rewrite-debug") << "Attributes : " << in
[0].hasAttribute(NestedQuantAttribute()) << std::endl
;
203 if( !options::quantRewriteRules() || !TermDb::isRewriteRule( in
) ){
204 RewriteStatus status
= REWRITE_DONE
;
207 std::vector
< Node
> args
;
208 for( int i
=0; i
<(int)in
[0].getNumChildren(); i
++ ){
209 args
.push_back( in
[0][i
] );
211 //get the instantiation pattern list
213 if( in
.getNumChildren()==3 ){
217 if( in
.getKind()==EXISTS
){
218 std::vector
< Node
> children
;
219 children
.push_back( in
[0] );
220 children
.push_back( in
[1].negate() );
221 if( in
.getNumChildren()==3 ){
222 children
.push_back( in
[2] );
224 ret
= NodeManager::currentNM()->mkNode( FORALL
, children
);
226 status
= REWRITE_AGAIN_FULL
;
228 bool isNested
= in
[0].hasAttribute(NestedQuantAttribute());
229 for( int op
=0; op
<COMPUTE_LAST
; op
++ ){
230 if( doOperation( in
, isNested
, op
) ){
231 ret
= computeOperation( in
, isNested
, op
);
233 status
= REWRITE_AGAIN_FULL
;
241 setAttributes( in
, ret
);
242 Trace("quantifiers-rewrite") << "*** rewrite " << in
<< std::endl
;
243 Trace("quantifiers-rewrite") << " to " << std::endl
;
244 Trace("quantifiers-rewrite") << ret
<< std::endl
;
245 //Trace("quantifiers-rewrite-debug") << "Attributes : " << ret[0].hasAttribute(NestedQuantAttribute()) << std::endl;
247 return RewriteResponse( status
, ret
);
249 return RewriteResponse(REWRITE_DONE
, in
);
252 Node
QuantifiersRewriter::computeElimSymbols( Node body
) {
253 if( isLiteral( body
) ){
256 bool childrenChanged
= false;
257 std::vector
< Node
> children
;
258 for( unsigned i
=0; i
<body
.getNumChildren(); i
++ ){
259 Node c
= computeElimSymbols( body
[i
] );
260 if( i
==0 && ( body
.getKind()==IMPLIES
|| body
.getKind()==XOR
) ){
263 children
.push_back( c
);
264 childrenChanged
= childrenChanged
|| c
!=body
[i
];
266 if( body
.getKind()==IMPLIES
){
267 return NodeManager::currentNM()->mkNode( OR
, children
);
268 }else if( body
.getKind()==XOR
){
269 return NodeManager::currentNM()->mkNode( IFF
, children
);
270 }else if( childrenChanged
){
271 return NodeManager::currentNM()->mkNode( body
.getKind(), children
);
278 Node
QuantifiersRewriter::computeNNF( Node body
){
279 if( body
.getKind()==NOT
){
280 if( body
[0].getKind()==NOT
){
281 return computeNNF( body
[0][0] );
282 }else if( isLiteral( body
[0] ) ){
285 std::vector
< Node
> children
;
286 Kind k
= body
[0].getKind();
287 if( body
[0].getKind()==OR
|| body
[0].getKind()==AND
){
288 for( int i
=0; i
<(int)body
[0].getNumChildren(); i
++ ){
289 children
.push_back( computeNNF( body
[0][i
].notNode() ) );
291 k
= body
[0].getKind()==AND
? OR
: AND
;
292 }else if( body
[0].getKind()==IFF
){
293 for( int i
=0; i
<2; i
++ ){
294 Node nn
= i
==0 ? body
[0][i
] : body
[0][i
].notNode();
295 children
.push_back( computeNNF( nn
) );
297 }else if( body
[0].getKind()==ITE
){
298 for( int i
=0; i
<3; i
++ ){
299 Node nn
= i
==0 ? body
[0][i
] : body
[0][i
].notNode();
300 children
.push_back( computeNNF( nn
) );
303 Notice() << "Unhandled Quantifiers NNF: " << body
<< std::endl
;
306 return NodeManager::currentNM()->mkNode( k
, children
);
308 }else if( isLiteral( body
) ){
311 std::vector
< Node
> children
;
312 bool childrenChanged
= false;
313 for( int i
=0; i
<(int)body
.getNumChildren(); i
++ ){
314 Node nc
= computeNNF( body
[i
] );
315 children
.push_back( nc
);
316 childrenChanged
= childrenChanged
|| nc
!=body
[i
];
318 if( childrenChanged
){
319 return NodeManager::currentNM()->mkNode( body
.getKind(), children
);
326 Node
QuantifiersRewriter::computeSimpleIteLift( Node body
) {
327 if( body
.getKind()==EQUAL
){
328 for( size_t i
=0; i
<2; i
++ ){
329 if( body
[i
].getKind()==ITE
){
330 Node no
= i
==0 ? body
[1] : body
[0];
331 bool doRewrite
= false;
332 std::vector
< Node
> children
;
333 children
.push_back( body
[i
][0] );
334 for( size_t j
=1; j
<=2; j
++ ){
335 //check if it rewrites to a constant
336 Node nn
= NodeManager::currentNM()->mkNode( EQUAL
, no
, body
[i
][j
] );
337 nn
= Rewriter::rewrite( nn
);
338 children
.push_back( nn
);
344 return NodeManager::currentNM()->mkNode( ITE
, children
);
348 }else if( body
.getKind()!=APPLY_UF
&& body
.getType()==NodeManager::currentNM()->booleanType() ){
349 bool changed
= false;
350 std::vector
< Node
> children
;
351 for( size_t i
=0; i
<body
.getNumChildren(); i
++ ){
352 Node nn
= computeSimpleIteLift( body
[i
] );
353 children
.push_back( nn
);
354 changed
= changed
|| nn
!=body
[i
];
357 return NodeManager::currentNM()->mkNode( body
.getKind(), children
);
363 Node
QuantifiersRewriter::computeVarElimination( Node body
, std::vector
< Node
>& args
, Node
& ipl
){
364 Trace("var-elim-quant-debug") << "Compute var elimination for " << body
<< std::endl
;
365 QuantPhaseReq
qpr( body
);
366 std::vector
< Node
> vars
;
367 std::vector
< Node
> subs
;
368 for( std::map
< Node
, bool >::iterator it
= qpr
.d_phase_reqs
.begin(); it
!= qpr
.d_phase_reqs
.end(); ++it
){
369 //Notice() << " " << it->first << " -> " << ( it->second ? "true" : "false" ) << std::endl;
370 if( it
->first
.getKind()==EQUAL
){
371 if( it
->second
&& options::varElimQuant() ){
372 for( int i
=0; i
<2; i
++ ){
373 int j
= i
==0 ? 1 : 0;
374 std::vector
< Node
>::iterator ita
= std::find( args
.begin(), args
.end(), it
->first
[i
] );
375 if( ita
!=args
.end() ){
376 std::vector
< Node
> temp
;
377 temp
.push_back( it
->first
[i
] );
378 if( !hasArg( temp
, it
->first
[j
] ) ){
379 vars
.push_back( it
->first
[i
] );
380 subs
.push_back( it
->first
[j
] );
391 else if( it
->first
.getKind()==APPLY_TESTER
){
392 if( options::dtVarExpandQuant() && it
->second
&& it
->first
[0].getKind()==BOUND_VARIABLE
){
393 Trace("dt-var-expand") << "Expand datatype variable based on : " << it
->first
<< std::endl
;
394 std::vector
< Node
>::iterator ita
= std::find( args
.begin(), args
.end(), it
->first
[0] );
395 if( ita
!=args
.end() ){
396 vars
.push_back( it
->first
[0] );
397 Expr testerExpr
= it
->first
.getOperator().toExpr();
398 int index
= Datatype::indexOf( testerExpr
);
399 const Datatype
& dt
= Datatype::datatypeOf(testerExpr
);
400 const DatatypeConstructor
& c
= dt
[index
];
401 std::vector
< Node
> newChildren
;
402 newChildren
.push_back( Node::fromExpr( c
.getConstructor() ) );
403 std::vector
< Node
> newVars
;
404 for( unsigned j
=0; j
<c
.getNumArgs(); j
++ ){
405 TypeNode tn
= TypeNode::fromType( c
[j
].getSelector().getType() );
407 Node v
= NodeManager::currentNM()->mkBoundVar( tn
);
408 newChildren
.push_back( v
);
409 newVars
.push_back( v
);
411 subs
.push_back( NodeManager::currentNM()->mkNode( APPLY_CONSTRUCTOR
, newChildren
) );
412 Trace("dt-var-expand") << "...apply substitution " << subs
[0] << "/" << vars
[0] << std::endl
;
414 args
.insert( args
.end(), newVars
.begin(), newVars
.end() );
420 Trace("var-elim-quant") << "VE " << vars
.size() << "/" << args
.size() << std::endl
;
421 //remake with eliminated nodes
422 body
= body
.substitute( vars
.begin(), vars
.end(), subs
.begin(), subs
.end() );
423 body
= Rewriter::rewrite( body
);
425 ipl
= ipl
.substitute( vars
.begin(), vars
.end(), subs
.begin(), subs
.end() );
427 Trace("var-elim-quant") << "Return " << body
<< std::endl
;
432 Node
QuantifiersRewriter::computeClause( Node n
){
433 Assert( isClause( n
) );
434 if( isLiteral( n
) ){
438 if( n
.getKind()==NOT
){
439 if( n
[0].getKind()==NOT
){
440 return computeClause( n
[0][0] );
443 Assert( n
[0].getKind()==AND
);
444 for( int i
=0; i
<(int)n
[0].getNumChildren(); i
++ ){
445 Node nn
= computeClause( n
[0][i
].notNode() );
446 addNodeToOrBuilder( nn
, t
);
450 for( int i
=0; i
<(int)n
.getNumChildren(); i
++ ){
451 Node nn
= computeClause( n
[i
] );
452 addNodeToOrBuilder( nn
, t
);
455 return t
.constructNode();
459 void QuantifiersRewriter::setAttributes( Node in
, Node n
) {
460 if( n
.getKind()==FORALL
&& in
.getKind()==FORALL
){
461 if( in
[0].hasAttribute(NestedQuantAttribute()) ){
462 setNestedQuantifiers( n
[0], in
[0].getAttribute(NestedQuantAttribute()) );
467 Node
QuantifiersRewriter::computeCNF( Node n
, std::vector
< Node
>& args
, NodeBuilder
<>& defs
, bool forcePred
){
468 if( isLiteral( n
) ){
470 }else if( !forcePred
&& isClause( n
) ){
471 return computeClause( n
);
473 Kind k
= n
.getKind();
475 for( int i
=0; i
<(int)n
.getNumChildren(); i
++ ){
477 Node ncnf
= computeCNF( nc
, args
, defs
, k
!=OR
);
479 addNodeToOrBuilder( ncnf
, t
);
484 if( !forcePred
&& k
==OR
){
485 return t
.constructNode();
487 //compute the free variables
489 std::vector
< Node
> activeArgs
;
490 computeArgVec( args
, activeArgs
, nt
);
491 std::vector
< TypeNode
> argTypes
;
492 for( int i
=0; i
<(int)activeArgs
.size(); i
++ ){
493 argTypes
.push_back( activeArgs
[i
].getType() );
495 //create the predicate
496 Assert( argTypes
.size()>0 );
497 TypeNode typ
= NodeManager::currentNM()->mkFunctionType( argTypes
, NodeManager::currentNM()->booleanType() );
498 std::stringstream ss
;
499 ss
<< "cnf_" << n
.getKind() << "_" << n
.getId();
500 Node op
= NodeManager::currentNM()->mkSkolem( ss
.str(), typ
, "was created by the quantifiers rewriter" );
501 std::vector
< Node
> predArgs
;
502 predArgs
.push_back( op
);
503 predArgs
.insert( predArgs
.end(), activeArgs
.begin(), activeArgs
.end() );
504 Node pred
= NodeManager::currentNM()->mkNode( APPLY_UF
, predArgs
);
505 Trace("quantifiers-rewrite-cnf-debug") << "Made predicate " << pred
<< " for " << nt
<< std::endl
;
506 //create the bound var list
507 Node bvl
= NodeManager::currentNM()->mkNode( BOUND_VAR_LIST
, activeArgs
);
508 //now, look at the structure of nt
509 if( nt
.getKind()==NOT
){
511 for( int i
=0; i
<2; i
++ ){
512 NodeBuilder
<> tt(OR
);
513 tt
<< ( i
==0 ? nt
[0].notNode() : nt
[0] );
514 tt
<< ( i
==0 ? pred
.notNode() : pred
);
515 defs
<< NodeManager::currentNM()->mkNode( FORALL
, bvl
, tt
.constructNode() );
517 }else if( nt
.getKind()==OR
){
519 for( int i
=0; i
<(int)nt
.getNumChildren(); i
++ ){
520 NodeBuilder
<> tt(OR
);
521 tt
<< nt
[i
].notNode() << pred
;
522 defs
<< NodeManager::currentNM()->mkNode( FORALL
, bvl
, tt
.constructNode() );
524 NodeBuilder
<> tt(OR
);
525 for( int i
=0; i
<(int)nt
.getNumChildren(); i
++ ){
528 tt
<< pred
.notNode();
529 defs
<< NodeManager::currentNM()->mkNode( FORALL
, bvl
, tt
.constructNode() );
530 }else if( nt
.getKind()==AND
){
532 for( int i
=0; i
<(int)nt
.getNumChildren(); i
++ ){
533 NodeBuilder
<> tt(OR
);
534 tt
<< nt
[i
] << pred
.notNode();
535 defs
<< NodeManager::currentNM()->mkNode( FORALL
, bvl
, tt
.constructNode() );
537 NodeBuilder
<> tt(OR
);
538 for( int i
=0; i
<(int)nt
.getNumChildren(); i
++ ){
539 tt
<< nt
[i
].notNode();
542 defs
<< NodeManager::currentNM()->mkNode( FORALL
, bvl
, tt
.constructNode() );
543 }else if( nt
.getKind()==IFF
){
545 for( int i
=0; i
<4; i
++ ){
546 NodeBuilder
<> tt(OR
);
547 tt
<< ( ( i
==0 || i
==3 ) ? nt
[0].notNode() : nt
[0] );
548 tt
<< ( ( i
==1 || i
==3 ) ? nt
[1].notNode() : nt
[1] );
549 tt
<< ( ( i
==0 || i
==1 ) ? pred
.notNode() : pred
);
550 defs
<< NodeManager::currentNM()->mkNode( FORALL
, bvl
, tt
.constructNode() );
552 }else if( nt
.getKind()==ITE
){
554 for( int j
=1; j
<=2; j
++ ){
555 for( int i
=0; i
<2; i
++ ){
556 NodeBuilder
<> tt(OR
);
557 tt
<< ( ( j
==1 ) ? nt
[0].notNode() : nt
[0] );
558 tt
<< ( ( i
==1 ) ? nt
[j
].notNode() : nt
[j
] );
559 tt
<< ( ( i
==0 ) ? pred
.notNode() : pred
);
560 defs
<< NodeManager::currentNM()->mkNode( FORALL
, bvl
, tt
.constructNode() );
563 for( int i
=0; i
<2; i
++ ){
564 NodeBuilder
<> tt(OR
);
565 tt
<< ( i
==0 ? nt
[1].notNode() : nt
[1] );
566 tt
<< ( i
==0 ? nt
[2].notNode() : nt
[2] );
567 tt
<< ( i
==1 ? pred
.notNode() : pred
);
568 defs
<< NodeManager::currentNM()->mkNode( FORALL
, bvl
, tt
.constructNode() );
571 Notice() << "Unhandled Quantifiers CNF: " << nt
<< std::endl
;
578 Node
QuantifiersRewriter::computePrenex( Node body
, std::vector
< Node
>& args
, bool pol
){
579 if( body
.getKind()==FORALL
){
581 std::vector
< Node
> terms
;
582 std::vector
< Node
> subs
;
583 //for doing prenexing of same-signed quantifiers
584 //must rename each variable that already exists
585 for( int i
=0; i
<(int)body
[0].getNumChildren(); i
++ ){
586 //if( std::find( args.begin(), args.end(), body[0][i] )!=args.end() ){
587 terms
.push_back( body
[0][i
] );
588 subs
.push_back( NodeManager::currentNM()->mkBoundVar( body
[0][i
].getType() ) );
590 args
.insert( args
.end(), subs
.begin(), subs
.end() );
591 Node newBody
= body
[1];
592 newBody
= newBody
.substitute( terms
.begin(), terms
.end(), subs
.begin(), subs
.end() );
593 Debug("quantifiers-substitute-debug") << "Did substitute have an effect" << (body
[1] != newBody
) << body
[1] << " became " << newBody
<< endl
;
598 }else if( body
.getKind()==ITE
|| body
.getKind()==XOR
|| body
.getKind()==IFF
){
601 Assert( body
.getKind()!=EXISTS
);
602 bool childrenChanged
= false;
603 std::vector
< Node
> newChildren
;
604 for( int i
=0; i
<(int)body
.getNumChildren(); i
++ ){
605 bool newPol
= body
.getKind()==NOT
? !pol
: pol
;
606 Node n
= computePrenex( body
[i
], args
, newPol
);
607 newChildren
.push_back( n
);
609 childrenChanged
= true;
612 if( childrenChanged
){
613 if( body
.getKind()==NOT
&& newChildren
[0].getKind()==NOT
){
614 return newChildren
[0][0];
616 return NodeManager::currentNM()->mkNode( body
.getKind(), newChildren
);
624 Node
QuantifiersRewriter::computeSplit( Node f
, Node body
, std::vector
< Node
>& vars
) {
625 if( body
.getKind()==OR
){
626 size_t var_found_count
= 0;
627 size_t eqc_count
= 0;
628 size_t eqc_active
= 0;
629 std::map
< Node
, int > var_to_eqc
;
630 std::map
< int, std::vector
< Node
> > eqc_to_var
;
631 std::map
< int, std::vector
< Node
> > eqc_to_lit
;
633 std::vector
<Node
> lits
;
635 for( size_t i
=0; i
<body
.getNumChildren(); i
++ ){
636 //get variables contained in the literal
638 std::vector
<Node
> lit_vars
;
639 computeArgVec( vars
, lit_vars
, n
);
640 //collectVars( n, vars, lit_vars );
641 if (lit_vars
.empty()) {
644 std::vector
<int> eqcs
;
645 std::vector
<Node
> lit_new_vars
;
646 //for each variable in literal
647 for( size_t j
=0; j
<lit_vars
.size(); j
++) {
648 //see if the variable has already been found
649 if (var_to_eqc
.find(lit_vars
[j
])!=var_to_eqc
.end()) {
650 int eqc
= var_to_eqc
[lit_vars
[j
]];
651 if (std::find(eqcs
.begin(), eqcs
.end(), eqc
)==eqcs
.end()) {
657 lit_new_vars
.push_back(lit_vars
[j
]);
661 eqcs
.push_back(eqc_count
);
667 //merge equivalence classes with eqcz
668 for (unsigned j
=1; j
<eqcs
.size(); j
++) {
670 //move all variables from equivalence class
671 for (unsigned k
=0; k
<eqc_to_var
[eqc
].size(); k
++) {
672 Node v
= eqc_to_var
[eqc
][k
];
673 var_to_eqc
[v
] = eqcz
;
674 eqc_to_var
[eqcz
].push_back(v
);
676 eqc_to_var
.erase(eqc
);
677 //move all literals from equivalence class
678 for (unsigned k
=0; k
<eqc_to_lit
[eqc
].size(); k
++) {
679 Node l
= eqc_to_lit
[eqc
][k
];
680 eqc_to_lit
[eqcz
].push_back(l
);
682 eqc_to_lit
.erase(eqc
);
685 if (eqc_active
==1 && var_found_count
==vars
.size()) {
688 //add variables to equivalence class
689 for (size_t j
=0; j
<lit_new_vars
.size(); j
++) {
690 var_to_eqc
[lit_new_vars
[j
]] = eqcz
;
691 eqc_to_var
[eqcz
].push_back(lit_new_vars
[j
]);
693 //add literal to equivalence class
694 eqc_to_lit
[eqcz
].push_back(n
);
698 Trace("clause-split-debug") << "Split clause " << f
<< std::endl
;
699 Trace("clause-split-debug") << " Ground literals: " << std::endl
;
700 for( size_t i
=0; i
<lits
.size(); i
++) {
701 Trace("clause-split-debug") << " " << lits
[i
] << std::endl
;
703 Trace("clause-split-debug") << std::endl
;
704 Trace("clause-split-debug") << "Equivalence classes: " << std::endl
;
705 for (std::map
< int, std::vector
< Node
> >::iterator it
= eqc_to_lit
.begin(); it
!= eqc_to_lit
.end(); ++it
){
706 Trace("clause-split-debug") << " Literals: " << std::endl
;
707 for (size_t i
=0; i
<it
->second
.size(); i
++) {
708 Trace("clause-split-debug") << " " << it
->second
[i
] << std::endl
;
711 Trace("clause-split-debug") << " Variables: " << std::endl
;
712 for (size_t i
=0; i
<eqc_to_var
[eqc
].size(); i
++) {
713 Trace("clause-split-debug") << " " << eqc_to_var
[eqc
][i
] << std::endl
;
715 Trace("clause-split-debug") << std::endl
;
716 Node bvl
= NodeManager::currentNM()->mkNode( BOUND_VAR_LIST
, eqc_to_var
[eqc
]);
717 Node body
= it
->second
.size()==1 ? it
->second
[0] : NodeManager::currentNM()->mkNode(OR
,it
->second
);
718 Node fa
= NodeManager::currentNM()->mkNode( FORALL
, bvl
, body
);
721 Node nf
= NodeManager::currentNM()->mkNode(OR
,lits
);
722 Trace("clause-split-debug") << "Made node : " << nf
<< std::endl
;
729 Node
QuantifiersRewriter::mkForAll( std::vector
< Node
>& args
, Node body
, Node ipl
){
730 std::vector
< Node
> activeArgs
;
731 computeArgVec( args
, activeArgs
, body
);
732 if( activeArgs
.empty() ){
735 std::vector
< Node
> children
;
736 children
.push_back( NodeManager::currentNM()->mkNode(kind::BOUND_VAR_LIST
, activeArgs
) );
737 children
.push_back( body
);
739 children
.push_back( ipl
);
741 return NodeManager::currentNM()->mkNode( kind::FORALL
, children
);
745 Node
QuantifiersRewriter::computeMiniscoping( Node f
, std::vector
< Node
>& args
, Node body
, Node ipl
, bool isNested
){
746 //Notice() << "rewrite quant " << body << std::endl;
747 if( body
.getKind()==FORALL
){
749 std::vector
< Node
> newArgs
;
750 for( int i
=0; i
<(int)body
[0].getNumChildren(); i
++ ){
751 newArgs
.push_back( body
[0][i
] );
753 newArgs
.insert( newArgs
.end(), args
.begin(), args
.end() );
754 return mkForAll( newArgs
, body
[ 1 ], ipl
);
755 }else if( !isNested
){
756 if( body
.getKind()==NOT
){
758 if( body
[0].getKind()==NOT
){
759 return computeMiniscoping( f
, args
, body
[0][0], ipl
);
760 }else if( body
[0].getKind()==AND
){
761 if( doMiniscopingNoFreeVar() ){
762 NodeBuilder
<> t(kind::OR
);
763 for( int i
=0; i
<(int)body
[0].getNumChildren(); i
++ ){
764 t
<< ( body
[0][i
].getKind()==NOT
? body
[0][i
][0] : body
[0][i
].notNode() );
766 return computeMiniscoping( f
, args
, t
.constructNode(), ipl
);
768 }else if( body
[0].getKind()==OR
){
769 if( doMiniscopingAnd() ){
770 NodeBuilder
<> t(kind::AND
);
771 for( int i
=0; i
<(int)body
[0].getNumChildren(); i
++ ){
772 Node trm
= body
[0][i
].negate();
773 t
<< computeMiniscoping( f
, args
, trm
, ipl
);
775 return t
.constructNode();
778 }else if( body
.getKind()==AND
){
779 if( doMiniscopingAnd() ){
781 NodeBuilder
<> t(kind::AND
);
782 for( int i
=0; i
<(int)body
.getNumChildren(); i
++ ){
783 t
<< computeMiniscoping( f
, args
, body
[i
], ipl
);
788 }else if( body
.getKind()==OR
){
789 if( doMiniscopingNoFreeVar() ){
791 NodeBuilder
<> body_split(kind::OR
);
792 NodeBuilder
<> tb(kind::OR
);
793 for( int i
=0; i
<(int)body
.getNumChildren(); i
++ ){
795 if( hasArg( args
, body
[i
] ) ){
801 if( tb
.getNumChildren()==0 ){
803 }else if( body_split
.getNumChildren()>0 ){
804 newBody
= tb
.getNumChildren()==1 ? tb
.getChild( 0 ) : tb
;
805 body_split
<< mkForAll( args
, newBody
, ipl
);
806 return body_split
.getNumChildren()==1 ? body_split
.getChild( 0 ) : body_split
;
814 return mkForAll( args
, body
, ipl
);
818 Node
QuantifiersRewriter::computeAggressiveMiniscoping( std::vector
< Node
>& args
, Node body
, bool isNested
){
820 std::map
< Node
, std::vector
< Node
> > varLits
;
821 std::map
< Node
, std::vector
< Node
> > litVars
;
822 if( body
.getKind()==OR
){
823 Trace("ag-miniscope") << "compute aggressive miniscoping on " << body
<< std::endl
;
824 for( size_t i
=0; i
<body
.getNumChildren(); i
++ ){
825 std::vector
< Node
> activeArgs
;
826 computeArgVec( args
, activeArgs
, body
[i
] );
827 for (unsigned j
=0; j
<activeArgs
.size(); j
++ ){
828 varLits
[activeArgs
[j
]].push_back( body
[i
] );
830 litVars
[body
[i
]].insert( litVars
[body
[i
]].begin(), activeArgs
.begin(), activeArgs
.end() );
832 //find the variable in the least number of literals
834 for( std::map
< Node
, std::vector
< Node
> >::iterator it
= varLits
.begin(); it
!= varLits
.end(); ++it
){
835 if( bestVar
.isNull() || varLits
[bestVar
].size()>it
->second
.size() ){
839 Trace("ag-miniscope-debug") << "Best variable " << bestVar
<< " occurs in " << varLits
[bestVar
].size() << "/ " << body
.getNumChildren() << " literals." << std::endl
;
840 if( !bestVar
.isNull() && varLits
[bestVar
].size()<body
.getNumChildren() ){
842 Trace("ag-miniscope") << "Miniscope on " << bestVar
<< std::endl
;
844 std::vector
< Node
> qlit1
;
845 qlit1
.insert( qlit1
.begin(), varLits
[bestVar
].begin(), varLits
[bestVar
].end() );
846 std::vector
< Node
> qlitt
;
847 //for all literals not containing bestVar
848 for( size_t i
=0; i
<body
.getNumChildren(); i
++ ){
849 if( std::find( qlit1
.begin(), qlit1
.end(), body
[i
] )==qlit1
.end() ){
850 qlitt
.push_back( body
[i
] );
853 //make the variable lists
854 std::vector
< Node
> qvl1
;
855 std::vector
< Node
> qvl2
;
856 std::vector
< Node
> qvsh
;
857 for( unsigned i
=0; i
<args
.size(); i
++ ){
860 for( size_t j
=0; j
<varLits
[args
[i
]].size(); j
++ ){
861 if( !found1
&& std::find( qlit1
.begin(), qlit1
.end(), varLits
[args
[i
]][j
] )!=qlit1
.end() ){
863 }else if( !found2
&& std::find( qlitt
.begin(), qlitt
.end(), varLits
[args
[i
]][j
] )!=qlitt
.end() ){
866 if( found1
&& found2
){
872 qvsh
.push_back( args
[i
] );
874 qvl1
.push_back( args
[i
] );
878 qvl2
.push_back( args
[i
] );
881 Assert( !qvl1
.empty() );
882 Assert( !qvl2
.empty() || !qvsh
.empty() );
883 //check for literals that only contain shared variables
884 std::vector
< Node
> qlitsh
;
885 std::vector
< Node
> qlit2
;
886 for( size_t i
=0; i
<qlitt
.size(); i
++ ){
887 bool hasVar2
= false;
888 for( size_t j
=0; j
<litVars
[qlitt
[i
]].size(); j
++ ){
889 if( std::find( qvl2
.begin(), qvl2
.end(), litVars
[qlitt
[i
]][j
] )!=qvl2
.end() ){
895 qlit2
.push_back( qlitt
[i
] );
897 qlitsh
.push_back( qlitt
[i
] );
902 Trace("ag-miniscope-debug") << "Split into literals : " << qlit1
.size() << " / " << qlit2
.size() << " / " << qlitsh
.size();
903 Trace("ag-miniscope-debug") << ", variables : " << qvl1
.size() << " / " << qvl2
.size() << " / " << qvsh
.size() << std::endl
;
904 Node n1
= qlit1
.size()==1 ? qlit1
[0] : NodeManager::currentNM()->mkNode( OR
, qlit1
);
905 n1
= computeAggressiveMiniscoping( qvl1
, n1
);
906 qlitsh
.push_back( n1
);
907 if( !qlit2
.empty() ){
908 Node n2
= qlit2
.size()==1 ? qlit2
[0] : NodeManager::currentNM()->mkNode( OR
, qlit2
);
909 n2
= computeAggressiveMiniscoping( qvl2
, n2
);
910 qlitsh
.push_back( n2
);
912 Node n
= NodeManager::currentNM()->mkNode( OR
, qlitsh
);
914 Node bvl
= NodeManager::currentNM()->mkNode(kind::BOUND_VAR_LIST
, qvsh
);
915 n
= NodeManager::currentNM()->mkNode( FORALL
, bvl
, n
);
917 Trace("ag-miniscope") << "Return " << n
<< " for " << body
<< std::endl
;
922 return mkForAll( args
, body
, Node::null() );
925 bool QuantifiersRewriter::doMiniscopingNoFreeVar(){
926 return options::miniscopeQuantFreeVar();
929 bool QuantifiersRewriter::doMiniscopingAnd(){
930 if( options::miniscopeQuant() ){
933 if( options::cbqi() ){
941 bool QuantifiersRewriter::doOperation( Node f
, bool isNested
, int computeOption
){
942 if( computeOption
==COMPUTE_ELIM_SYMBOLS
){
944 }else if( computeOption
==COMPUTE_MINISCOPING
){
946 }else if( computeOption
==COMPUTE_AGGRESSIVE_MINISCOPING
){
947 return options::aggressiveMiniscopeQuant();
948 }else if( computeOption
==COMPUTE_NNF
){
949 return options::nnfQuant();
950 }else if( computeOption
==COMPUTE_SIMPLE_ITE_LIFT
){
951 return options::simpleIteLiftQuant();
952 }else if( computeOption
==COMPUTE_PRENEX
){
953 return options::prenexQuant() && !options::aggressiveMiniscopeQuant();
954 }else if( computeOption
==COMPUTE_VAR_ELIMINATION
){
955 return options::varElimQuant() || options::dtVarExpandQuant();
956 }else if( computeOption
==COMPUTE_CNF
){
957 return false;//return options::cnfQuant() ; FIXME
958 }else if( computeOption
==COMPUTE_SPLIT
){
959 return options::clauseSplit();
965 //general method for computing various rewrites
966 Node
QuantifiersRewriter::computeOperation( Node f
, bool isNested
, int computeOption
){
967 if( f
.getKind()==FORALL
){
968 Trace("quantifiers-rewrite-debug") << "Compute operation " << computeOption
<< " on " << f
<< ", nested = " << isNested
<< std::endl
;
969 std::vector
< Node
> args
;
970 for( int i
=0; i
<(int)f
[0].getNumChildren(); i
++ ){
971 args
.push_back( f
[0][i
] );
973 NodeBuilder
<> defs(kind::AND
);
976 if( f
.getNumChildren()==3 ){
979 if( computeOption
==COMPUTE_ELIM_SYMBOLS
){
980 n
= computeElimSymbols( n
);
981 }else if( computeOption
==COMPUTE_MINISCOPING
){
983 return computeMiniscoping( f
, args
, n
, ipl
, isNested
);
984 }else if( computeOption
==COMPUTE_AGGRESSIVE_MINISCOPING
){
985 return computeAggressiveMiniscoping( args
, n
, isNested
);
986 }else if( computeOption
==COMPUTE_NNF
){
988 }else if( computeOption
==COMPUTE_SIMPLE_ITE_LIFT
){
989 n
= computeSimpleIteLift( n
);
990 }else if( computeOption
==COMPUTE_PRENEX
){
991 n
= computePrenex( n
, args
, true );
992 }else if( computeOption
==COMPUTE_VAR_ELIMINATION
){
996 n
= computeVarElimination( n
, args
, ipl
);
997 }while( prev
!=n
&& !args
.empty() );
998 }else if( computeOption
==COMPUTE_CNF
){
999 //n = computeNNF( n );
1000 n
= computeCNF( n
, args
, defs
, false );
1002 }else if( computeOption
==COMPUTE_SPLIT
) {
1003 return computeSplit(f
, n
, args
);
1005 Trace("quantifiers-rewrite-debug") << "Compute Operation: return " << n
<< ", " << args
.size() << std::endl
;
1006 if( f
[1]==n
&& args
.size()==f
[0].getNumChildren() ){
1012 std::vector
< Node
> children
;
1013 children
.push_back( NodeManager::currentNM()->mkNode(kind::BOUND_VAR_LIST
, args
) );
1014 children
.push_back( n
);
1015 if( !ipl
.isNull() ){
1016 children
.push_back( ipl
);
1018 defs
<< NodeManager::currentNM()->mkNode(kind::FORALL
, children
);
1020 return defs
.getNumChildren()==1 ? defs
.getChild( 0 ) : defs
.constructNode();
1028 Node
QuantifiersRewriter::rewriteRewriteRule( Node r
) {
1029 Kind rrkind
= r
[2].getKind();
1031 //guards, pattern, body
1033 // Replace variables by Inst_* variable and tag the terms that contain them
1034 std::vector
<Node
> vars
;
1035 vars
.reserve(r
[0].getNumChildren());
1036 for( Node::const_iterator v
= r
[0].begin(); v
!= r
[0].end(); ++v
){
1040 // Body/Remove_term/Guards/Triggers
1041 Node body
= r
[2][1];
1042 TNode new_terms
= r
[2][1];
1043 std::vector
<Node
> guards
;
1044 std::vector
<Node
> pattern
;
1045 Node true_node
= NodeManager::currentNM()->mkConst(true);
1047 TNode head
= r
[2][0];
1049 case kind::RR_REWRITE
:
1051 pattern
.push_back( head
);
1052 if( head
.getType().isBoolean() ){
1053 body
= head
.iffNode(body
);
1055 body
= head
.eqNode(body
);
1058 case kind::RR_REDUCTION
:
1059 case kind::RR_DEDUCTION
:
1060 // Add head to guards and pattern
1061 switch(head
.getKind()){
1063 for( unsigned i
= 0; i
<head
.getNumChildren(); i
++ ){
1064 guards
.push_back(head
[i
]);
1065 pattern
.push_back(head
[i
]);
1069 if( head
!=true_node
){
1070 guards
.push_back(head
);
1071 pattern
.push_back( head
);
1077 Unreachable("RewriteRules can be of only three kinds");
1080 // Add the other guards
1082 switch(g
.getKind()){
1084 for( unsigned i
= 0; i
<g
.getNumChildren(); i
++ ){
1085 guards
.push_back(g
[i
]);
1089 if( g
!= true_node
){
1090 guards
.push_back( g
);
1094 // Add the other triggers
1095 if( r
[2].getNumChildren() >= 3 ){
1096 for( unsigned i
=0; i
<r
[2][2][0].getNumChildren(); i
++ ) {
1097 pattern
.push_back( r
[2][2][0][i
] );
1101 Trace("rr-rewrite") << "Rule is " << r
<< std::endl
;
1102 Trace("rr-rewrite") << "Head is " << head
<< std::endl
;
1103 Trace("rr-rewrite") << "Patterns are ";
1104 for( unsigned i
=0; i
<pattern
.size(); i
++ ){
1105 Trace("rr-rewrite") << pattern
[i
] << " ";
1107 Trace("rr-rewrite") << std::endl
;
1109 NodeBuilder
<> forallB(kind::FORALL
);
1111 Node gg
= guards
.size()==0 ? true_node
: ( guards
.size()==1 ? guards
[0] : NodeManager::currentNM()->mkNode( AND
, guards
) );
1112 gg
= NodeManager::currentNM()->mkNode( OR
, gg
.negate(), body
);
1113 gg
= Rewriter::rewrite( gg
);
1115 NodeBuilder
<> patternB(kind::INST_PATTERN
);
1116 patternB
.append(pattern
);
1117 NodeBuilder
<> patternListB(kind::INST_PATTERN_LIST
);
1118 //the entire rewrite rule is the first pattern
1119 if( options::quantRewriteRules() ){
1120 patternListB
<< NodeManager::currentNM()->mkNode( INST_PATTERN
, r
);
1122 patternListB
<< static_cast<Node
>(patternB
);
1123 forallB
<< static_cast<Node
>(patternListB
);
1124 Node rn
= (Node
) forallB
;
1129 struct ContainsQuantAttributeId
{};
1130 typedef expr::Attribute
<ContainsQuantAttributeId
, uint64_t> ContainsQuantAttribute
;
1132 // check if the given node contains a universal quantifier
1133 bool QuantifiersRewriter::containsQuantifiers(Node n
) {
1134 if( n
.hasAttribute(ContainsQuantAttribute()) ){
1135 return n
.getAttribute(ContainsQuantAttribute())==1;
1136 } else if(n
.getKind() == kind::FORALL
) {
1140 for( unsigned i
= 0; i
< n
.getNumChildren(); ++i
){
1141 if( containsQuantifiers(n
[i
]) ){
1146 ContainsQuantAttribute cqa
;
1147 n
.setAttribute(cqa
, cq
? 1 : 0);
1152 Node
QuantifiersRewriter::preSkolemizeQuantifiers( Node n
, bool polarity
, std::vector
< TypeNode
>& fvTypes
, std::vector
< TNode
>& fvs
){
1153 Trace("pre-sk") << "Pre-skolem " << n
<< " " << polarity
<< " " << fvs
.size() << endl
;
1154 if( n
.getKind()==kind::NOT
){
1155 Node nn
= preSkolemizeQuantifiers( n
[0], !polarity
, fvTypes
, fvs
);
1157 }else if( n
.getKind()==kind::FORALL
){
1159 if( options::preSkolemQuant() ){
1160 vector
< Node
> children
;
1161 children
.push_back( n
[0] );
1162 //add children to current scope
1163 std::vector
< TypeNode
> fvt
;
1164 std::vector
< TNode
> fvss
;
1165 fvt
.insert( fvt
.begin(), fvTypes
.begin(), fvTypes
.end() );
1166 fvss
.insert( fvss
.begin(), fvs
.begin(), fvs
.end() );
1167 for( int i
=0; i
<(int)n
[0].getNumChildren(); i
++ ){
1168 fvt
.push_back( n
[0][i
].getType() );
1169 fvss
.push_back( n
[0][i
] );
1172 children
.push_back( preSkolemizeQuantifiers( n
[1], polarity
, fvt
, fvss
) );
1173 if( n
.getNumChildren()==3 ){
1174 children
.push_back( n
[2] );
1176 //return processed quantifier
1177 return NodeManager::currentNM()->mkNode( kind::FORALL
, children
);
1181 Node nn
= preSkolemizeQuantifiers( n
[1], polarity
, fvTypes
, fvs
);
1182 std::vector
< Node
> sk
;
1184 std::vector
< unsigned > sub_vars
;
1185 //return skolemized body
1186 return TermDb::mkSkolemizedBody( n
, nn
, fvTypes
, fvs
, sk
, sub
, sub_vars
);
1189 //check if it contains a quantifier as a subterm
1190 //if so, we will write this node
1191 if( containsQuantifiers( n
) ){
1192 if( n
.getType().isBoolean() ){
1193 if( n
.getKind()==kind::ITE
|| n
.getKind()==kind::IFF
|| n
.getKind()==kind::XOR
|| n
.getKind()==kind::IMPLIES
){
1195 //must remove structure
1196 if( n
.getKind()==kind::ITE
){
1197 nn
= NodeManager::currentNM()->mkNode( kind::AND
,
1198 NodeManager::currentNM()->mkNode( kind::OR
, n
[0].notNode(), n
[1] ),
1199 NodeManager::currentNM()->mkNode( kind::OR
, n
[0], n
[2] ) );
1200 }else if( n
.getKind()==kind::IFF
|| n
.getKind()==kind::XOR
){
1201 nn
= NodeManager::currentNM()->mkNode( kind::AND
,
1202 NodeManager::currentNM()->mkNode( kind::OR
, n
[0].notNode(), n
.getKind()==kind::XOR
? n
[1].notNode() : n
[1] ),
1203 NodeManager::currentNM()->mkNode( kind::OR
, n
[0], n
.getKind()==kind::XOR
? n
[1] : n
[1].notNode() ) );
1204 }else if( n
.getKind()==kind::IMPLIES
){
1205 nn
= NodeManager::currentNM()->mkNode( kind::OR
, n
[0].notNode(), n
[1] );
1207 return preSkolemizeQuantifiers( nn
, polarity
, fvTypes
, fvs
);
1208 }else if( n
.getKind()==kind::AND
|| n
.getKind()==kind::OR
){
1209 vector
< Node
> children
;
1210 for( int i
=0; i
<(int)n
.getNumChildren(); i
++ ){
1211 children
.push_back( preSkolemizeQuantifiers( n
[i
], polarity
, fvTypes
, fvs
) );
1213 return NodeManager::currentNM()->mkNode( n
.getKind(), children
);
1221 bool QuantifiersRewriter::isDtStrInductionQuantifier( Node q
){
1222 Assert( q
.getKind()==FORALL
);
1223 return q
[0].getNumChildren()==1 && datatypes::DatatypesRewriter::isTermDatatype( q
[0][0] );