1 /********************* */
2 /*! \file quantifiers_rewriter.cpp
4 ** Top contributors (to current version):
5 ** Andrew Reynolds, Morgan Deters, Tim King
6 ** This file is part of the CVC4 project.
7 ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS
8 ** in the top-level source directory) and their institutional affiliations.
9 ** All rights reserved. See the file COPYING in the top-level source
10 ** directory for licensing information.\endverbatim
12 ** \brief Implementation of QuantifiersRewriter class
15 #include "theory/quantifiers/quantifiers_rewriter.h"
17 #include "expr/dtype.h"
18 #include "expr/node_algorithm.h"
19 #include "options/quantifiers_options.h"
20 #include "theory/arith/arith_msum.h"
21 #include "theory/datatypes/theory_datatypes_utils.h"
22 #include "theory/quantifiers/bv_inverter.h"
23 #include "theory/quantifiers/ematching/trigger.h"
24 #include "theory/quantifiers/quantifiers_attributes.h"
25 #include "theory/quantifiers/skolemize.h"
26 #include "theory/quantifiers/term_database.h"
27 #include "theory/quantifiers/term_util.h"
28 #include "theory/strings/theory_strings_utils.h"
31 using namespace CVC4::kind
;
32 using namespace CVC4::context
;
36 namespace quantifiers
{
38 bool QuantifiersRewriter::isLiteral( Node n
){
39 switch( n
.getKind() ){
41 return n
[0].getKind()!=NOT
&& isLiteral( n
[0] );
52 return !n
[0].getType().isBoolean();
60 void QuantifiersRewriter::addNodeToOrBuilder( Node n
, NodeBuilder
<>& t
){
61 if( n
.getKind()==OR
){
62 for( int i
=0; i
<(int)n
.getNumChildren(); i
++ ){
70 void QuantifiersRewriter::computeArgs(const std::vector
<Node
>& args
,
71 std::map
<Node
, bool>& activeMap
,
73 std::map
<Node
, bool>& visited
)
75 if( visited
.find( n
)==visited
.end() ){
77 if( n
.getKind()==BOUND_VARIABLE
){
78 if( std::find( args
.begin(), args
.end(), n
)!=args
.end() ){
79 activeMap
[ n
] = true;
84 computeArgs(args
, activeMap
, n
.getOperator(), visited
);
86 for( int i
=0; i
<(int)n
.getNumChildren(); i
++ ){
87 computeArgs( args
, activeMap
, n
[i
], visited
);
93 void QuantifiersRewriter::computeArgVec(const std::vector
<Node
>& args
,
94 std::vector
<Node
>& activeArgs
,
97 Assert(activeArgs
.empty());
98 std::map
< Node
, bool > activeMap
;
99 std::map
< Node
, bool > visited
;
100 computeArgs( args
, activeMap
, n
, visited
);
101 if( !activeMap
.empty() ){
102 for( unsigned i
=0; i
<args
.size(); i
++ ){
103 if( activeMap
.find( args
[i
] )!=activeMap
.end() ){
104 activeArgs
.push_back( args
[i
] );
110 void QuantifiersRewriter::computeArgVec2(const std::vector
<Node
>& args
,
111 std::vector
<Node
>& activeArgs
,
115 Assert(activeArgs
.empty());
116 std::map
< Node
, bool > activeMap
;
117 std::map
< Node
, bool > visited
;
118 computeArgs( args
, activeMap
, n
, visited
);
119 if( !activeMap
.empty() ){
120 //collect variables in inst pattern list only if we cannot eliminate quantifier
121 computeArgs( args
, activeMap
, ipl
, visited
);
122 for( unsigned i
=0; i
<args
.size(); i
++ ){
123 if( activeMap
.find( args
[i
] )!=activeMap
.end() ){
124 activeArgs
.push_back( args
[i
] );
130 RewriteResponse
QuantifiersRewriter::preRewrite(TNode in
) {
131 if( in
.getKind()==kind::EXISTS
|| in
.getKind()==kind::FORALL
){
132 Trace("quantifiers-rewrite-debug") << "pre-rewriting " << in
<< std::endl
;
133 std::vector
< Node
> args
;
135 bool doRewrite
= false;
136 while( body
.getNumChildren()==2 && body
.getKind()==body
[1].getKind() ){
137 for( unsigned i
=0; i
<body
[0].getNumChildren(); i
++ ){
138 args
.push_back( body
[0][i
] );
144 std::vector
< Node
> children
;
145 for( unsigned i
=0; i
<body
[0].getNumChildren(); i
++ ){
146 args
.push_back( body
[0][i
] );
148 children
.push_back( NodeManager::currentNM()->mkNode(kind::BOUND_VAR_LIST
,args
) );
149 children
.push_back( body
[1] );
150 if( body
.getNumChildren()==3 ){
151 children
.push_back( body
[2] );
153 Node n
= NodeManager::currentNM()->mkNode( in
.getKind(), children
);
155 Trace("quantifiers-pre-rewrite") << "*** pre-rewrite " << in
<< std::endl
;
156 Trace("quantifiers-pre-rewrite") << " to " << std::endl
;
157 Trace("quantifiers-pre-rewrite") << n
<< std::endl
;
159 return RewriteResponse(REWRITE_DONE
, n
);
162 return RewriteResponse(REWRITE_DONE
, in
);
165 RewriteResponse
QuantifiersRewriter::postRewrite(TNode in
) {
166 Trace("quantifiers-rewrite-debug") << "post-rewriting " << in
<< std::endl
;
167 RewriteStatus status
= REWRITE_DONE
;
171 if( in
.getKind()==EXISTS
){
172 std::vector
< Node
> children
;
173 children
.push_back( in
[0] );
174 children
.push_back( in
[1].negate() );
175 if( in
.getNumChildren()==3 ){
176 children
.push_back( in
[2] );
178 ret
= NodeManager::currentNM()->mkNode( FORALL
, children
);
180 status
= REWRITE_AGAIN_FULL
;
181 }else if( in
.getKind()==FORALL
){
182 if( in
[1].isConst() && in
.getNumChildren()==2 ){
183 return RewriteResponse( status
, in
[1] );
187 QuantAttributes::computeQuantAttributes( in
, qa
);
188 if( !qa
.isRewriteRule() ){
189 for( int op
=0; op
<COMPUTE_LAST
; op
++ ){
190 if( doOperation( in
, op
, qa
) ){
191 ret
= computeOperation( in
, op
, qa
);
194 status
= REWRITE_AGAIN_FULL
;
204 Trace("quantifiers-rewrite") << "*** rewrite (op=" << rew_op
<< ") " << in
<< std::endl
;
205 Trace("quantifiers-rewrite") << " to " << std::endl
;
206 Trace("quantifiers-rewrite") << ret
<< std::endl
;
208 return RewriteResponse( status
, ret
);
211 bool QuantifiersRewriter::addCheckElimChild( std::vector
< Node
>& children
, Node c
, Kind k
, std::map
< Node
, bool >& lit_pol
, bool& childrenChanged
){
212 if( ( k
==OR
|| k
==AND
) && options::elimTautQuant() ){
213 Node lit
= c
.getKind()==NOT
? c
[0] : c
;
214 bool pol
= c
.getKind()!=NOT
;
215 std::map
< Node
, bool >::iterator it
= lit_pol
.find( lit
);
216 if( it
==lit_pol
.end() ){
218 children
.push_back( c
);
220 childrenChanged
= true;
221 if( it
->second
!=pol
){
226 children
.push_back( c
);
231 // eliminates IMPLIES/XOR, removes duplicates/infers tautologies of AND/OR, and computes NNF
232 Node
QuantifiersRewriter::computeElimSymbols( Node body
) {
233 Kind ok
= body
.getKind();
235 bool negAllCh
= false;
244 if( body
[0].getKind()==NOT
){
245 return computeElimSymbols( body
[0][0] );
246 }else if( body
[0].getKind()==OR
|| body
[0].getKind()==IMPLIES
){
249 negCh1
= body
[0].getKind()==IMPLIES
;
251 }else if( body
[0].getKind()==AND
){
255 }else if( body
[0].getKind()==XOR
|| ( body
[0].getKind()==EQUAL
&& body
[0][0].getType().isBoolean() ) ){
257 negCh1
= ( body
[0].getKind()==EQUAL
);
259 }else if( body
[0].getKind()==ITE
){
260 k
= body
[0].getKind();
267 }else if( ( ok
!=EQUAL
|| !body
[0].getType().isBoolean() ) && ok
!=ITE
&& ok
!=AND
&& ok
!=OR
){
271 bool childrenChanged
= false;
272 std::vector
< Node
> children
;
273 std::map
< Node
, bool > lit_pol
;
274 for( unsigned i
=0; i
<body
.getNumChildren(); i
++ ){
275 Node c
= computeElimSymbols( ( i
==0 && negCh1
)!=negAllCh
? body
[i
].negate() : body
[i
] );
277 if( c
.getKind()==k
&& ( k
==OR
|| k
==AND
) ){
279 childrenChanged
= true;
280 for( unsigned j
=0; j
<c
.getNumChildren(); j
++ ){
281 if( !addCheckElimChild( children
, c
[j
], k
, lit_pol
, childrenChanged
) ){
287 success
= addCheckElimChild( children
, c
, k
, lit_pol
, childrenChanged
);
291 Assert(k
== OR
|| k
== AND
);
292 return NodeManager::currentNM()->mkConst( k
==OR
);
294 childrenChanged
= childrenChanged
|| c
!=body
[i
];
296 if( childrenChanged
|| k
!=ok
){
297 return ( children
.size()==1 && k
!=NOT
) ? children
[0] : NodeManager::currentNM()->mkNode( k
, children
);
303 void QuantifiersRewriter::computeDtTesterIteSplit( Node n
, std::map
< Node
, Node
>& pcons
, std::map
< Node
, std::map
< int, Node
> >& ncons
,
304 std::vector
< Node
>& conj
){
305 if( n
.getKind()==ITE
&& n
[0].getKind()==APPLY_TESTER
&& n
[1].getType().isBoolean() ){
306 Trace("quantifiers-rewrite-ite-debug") << "Split tester condition : " << n
<< std::endl
;
308 std::map
< Node
, Node
>::iterator itp
= pcons
.find( x
);
309 if( itp
!=pcons
.end() ){
310 Trace("quantifiers-rewrite-ite-debug") << "...condition already set " << itp
->second
<< std::endl
;
311 computeDtTesterIteSplit( n
[ itp
->second
==n
[0] ? 1 : 2 ], pcons
, ncons
, conj
);
313 Node tester
= n
[0].getOperator();
314 int index
= datatypes::utils::indexOf(tester
);
315 std::map
< int, Node
>::iterator itn
= ncons
[x
].find( index
);
316 if( itn
!=ncons
[x
].end() ){
317 Trace("quantifiers-rewrite-ite-debug") << "...condition negated " << itn
->second
<< std::endl
;
318 computeDtTesterIteSplit( n
[ 2 ], pcons
, ncons
, conj
);
320 for( unsigned i
=0; i
<2; i
++ ){
325 ncons
[x
][index
] = n
[0].negate();
327 computeDtTesterIteSplit( n
[i
+1], pcons
, ncons
, conj
);
329 ncons
[x
].erase( index
);
333 NodeManager
* nm
= NodeManager::currentNM();
334 Trace("quantifiers-rewrite-ite-debug") << "Return value : " << n
<< std::endl
;
335 std::vector
< Node
> children
;
336 children
.push_back( n
);
337 std::vector
< Node
> vars
;
338 //add all positive testers
339 for( std::map
< Node
, Node
>::iterator it
= pcons
.begin(); it
!= pcons
.end(); ++it
){
340 children
.push_back( it
->second
.negate() );
341 vars
.push_back( it
->first
);
343 //add all negative testers
344 for( std::map
< Node
, std::map
< int, Node
> >::iterator it
= ncons
.begin(); it
!= ncons
.end(); ++it
){
346 //only if we haven't settled on a positive tester
347 if( std::find( vars
.begin(), vars
.end(), x
)==vars
.end() ){
348 //check if we have exhausted all options but one
349 const DType
& dt
= x
.getType().getDType();
350 std::vector
< Node
> nchildren
;
352 for( int i
=0; i
<(int)dt
.getNumConstructors(); i
++ ){
353 std::map
< int, Node
>::iterator itt
= it
->second
.find( i
);
354 if( itt
==it
->second
.end() ){
355 pos_cons
= pos_cons
==-1 ? i
: -2;
357 nchildren
.push_back( itt
->second
.negate() );
361 Node tester
= dt
[pos_cons
].getTester();
362 children
.push_back(nm
->mkNode(APPLY_TESTER
, tester
, x
).negate());
364 children
.insert( children
.end(), nchildren
.begin(), nchildren
.end() );
368 //make condition/output pair
369 Node c
= children
.size()==1 ? children
[0] : NodeManager::currentNM()->mkNode( OR
, children
);
374 int getEntailedCond( Node n
, std::map
< Node
, bool >& currCond
){
375 std::map
< Node
, bool >::iterator it
= currCond
.find( n
);
376 if( it
!=currCond
.end() ){
377 return it
->second
? 1 : -1;
378 }else if( n
.getKind()==NOT
){
379 return -getEntailedCond( n
[0], currCond
);
380 }else if( n
.getKind()==AND
|| n
.getKind()==OR
){
381 bool hasZero
= false;
382 for( unsigned i
=0; i
<n
.getNumChildren(); i
++ ){
383 int res
= getEntailedCond( n
[i
], currCond
);
386 }else if( n
.getKind()==AND
&& res
==-1 ){
388 }else if( n
.getKind()==OR
&& res
==1 ){
392 return hasZero
? 0 : ( n
.getKind()==AND
? 1 : -1 );
393 }else if( n
.getKind()==ITE
){
394 int res
= getEntailedCond( n
[0], currCond
);
396 return getEntailedCond( n
[1], currCond
);
398 return getEntailedCond( n
[2], currCond
);
400 }else if( ( n
.getKind()==EQUAL
&& n
[0].getType().isBoolean() ) || n
.getKind()==ITE
){
401 unsigned start
= n
.getKind()==EQUAL
? 0 : 1;
403 for( unsigned j
=start
; j
<=(start
+1); j
++ ){
404 int res
= getEntailedCond( n
[j
], currCond
);
407 }else if( j
==start
){
411 if( n
.getKind()==ITE
){
412 return res1
==res
? res
: 0;
413 }else if( n
.getKind()==EQUAL
){
414 return res1
==res
? 1 : -1;
419 else if (n
.isConst())
421 return n
.getConst
<bool>() ? 1 : -1;
426 bool addEntailedCond( Node n
, bool pol
, std::map
< Node
, bool >& currCond
, std::vector
< Node
>& new_cond
, bool& conflict
) {
429 Trace("quantifiers-rewrite-term-debug")
430 << "constant cond : " << n
<< " -> " << pol
<< std::endl
;
431 if (n
.getConst
<bool>() != pol
)
437 std::map
< Node
, bool >::iterator it
= currCond
.find( n
);
438 if( it
==currCond
.end() ){
439 Trace("quantifiers-rewrite-term-debug") << "cond : " << n
<< " -> " << pol
<< std::endl
;
440 new_cond
.push_back( n
);
444 else if (it
->second
!= pol
)
446 Trace("quantifiers-rewrite-term-debug")
447 << "CONFLICTING cond : " << n
<< " -> " << pol
<< std::endl
;
453 void setEntailedCond( Node n
, bool pol
, std::map
< Node
, bool >& currCond
, std::vector
< Node
>& new_cond
, bool& conflict
) {
454 if( ( n
.getKind()==AND
&& pol
) || ( n
.getKind()==OR
&& !pol
) ){
455 for( unsigned i
=0; i
<n
.getNumChildren(); i
++ ){
456 setEntailedCond( n
[i
], pol
, currCond
, new_cond
, conflict
);
461 }else if( n
.getKind()==NOT
){
462 setEntailedCond( n
[0], !pol
, currCond
, new_cond
, conflict
);
464 }else if( n
.getKind()==ITE
){
465 int pol
= getEntailedCond( n
, currCond
);
467 setEntailedCond( n
[1], pol
, currCond
, new_cond
, conflict
);
469 setEntailedCond( n
[2], pol
, currCond
, new_cond
, conflict
);
472 if( addEntailedCond( n
, pol
, currCond
, new_cond
, conflict
) ){
473 if( n
.getKind()==APPLY_TESTER
){
474 NodeManager
* nm
= NodeManager::currentNM();
475 const DType
& dt
= datatypes::utils::datatypeOf(n
.getOperator());
476 unsigned index
= datatypes::utils::indexOf(n
.getOperator());
477 Assert(dt
.getNumConstructors() > 1);
479 for( unsigned i
=0; i
<dt
.getNumConstructors(); i
++ ){
481 Node t
= nm
->mkNode(APPLY_TESTER
, dt
[i
].getTester(), n
[0]);
482 addEntailedCond( t
, false, currCond
, new_cond
, conflict
);
486 if( dt
.getNumConstructors()==2 ){
487 int oindex
= 1-index
;
488 Node t
= nm
->mkNode(APPLY_TESTER
, dt
[oindex
].getTester(), n
[0]);
489 addEntailedCond( t
, true, currCond
, new_cond
, conflict
);
496 void removeEntailedCond( std::map
< Node
, bool >& currCond
, std::vector
< Node
>& new_cond
, std::map
< Node
, Node
>& cache
) {
497 if( !new_cond
.empty() ){
498 for( unsigned j
=0; j
<new_cond
.size(); j
++ ){
499 currCond
.erase( new_cond
[j
] );
506 Node
QuantifiersRewriter::computeProcessTerms( Node body
, std::vector
< Node
>& new_vars
, std::vector
< Node
>& new_conds
, Node q
, QAttributes
& qa
){
507 std::map
< Node
, bool > curr_cond
;
508 std::map
< Node
, Node
> cache
;
509 std::map
< Node
, Node
> icache
;
511 Node h
= QuantAttributes::getFunDefHead( q
);
513 // if it is a function definition, rewrite the body independently
514 Node fbody
= QuantAttributes::getFunDefBody( q
);
515 Trace("quantifiers-rewrite-debug") << "Decompose " << h
<< " / " << fbody
<< " as function definition for " << q
<< "." << std::endl
;
518 Node r
= computeProcessTerms2(fbody
,
528 Assert(new_vars
.size() == h
.getNumChildren());
529 return Rewriter::rewrite(NodeManager::currentNM()->mkNode(EQUAL
, h
, r
));
531 // It can happen that we can't infer the shape of the function definition,
532 // for example: forall xy. f( x, y ) = 1 + f( x, y ), this is rewritten to
535 return computeProcessTerms2(body
,
544 options::elimExtArithQuant());
547 Node
QuantifiersRewriter::computeProcessTerms2( Node body
, bool hasPol
, bool pol
, std::map
< Node
, bool >& currCond
, int nCurrCond
,
548 std::map
< Node
, Node
>& cache
, std::map
< Node
, Node
>& icache
,
549 std::vector
< Node
>& new_vars
, std::vector
< Node
>& new_conds
, bool elimExtArith
) {
550 NodeManager
* nm
= NodeManager::currentNM();
551 Trace("quantifiers-rewrite-term-debug2") << "computeProcessTerms " << body
<< " " << hasPol
<< " " << pol
<< std::endl
;
553 std::map
< Node
, Node
>::iterator iti
= cache
.find( body
);
554 if( iti
!=cache
.end() ){
556 Trace("quantifiers-rewrite-term-debug2") << "Return (cached) " << ret
<< " for " << body
<< std::endl
;
558 //only do context dependent processing up to depth 8
559 bool doCD
= options::condRewriteQuant() && nCurrCond
< 8;
560 bool changed
= false;
561 std::vector
< Node
> children
;
562 //set entailed conditions based on OR/AND
563 std::map
< int, std::vector
< Node
> > new_cond_children
;
564 if( doCD
&& ( body
.getKind()==OR
|| body
.getKind()==AND
) ){
565 nCurrCond
= nCurrCond
+ 1;
566 bool conflict
= false;
567 bool use_pol
= body
.getKind()==AND
;
568 for( unsigned j
=0; j
<body
.getNumChildren(); j
++ ){
569 setEntailedCond( body
[j
], use_pol
, currCond
, new_cond_children
[j
], conflict
);
572 Trace("quantifiers-rewrite-term-debug") << "-------conflict, return " << !use_pol
<< std::endl
;
573 ret
= NodeManager::currentNM()->mkConst( !use_pol
);
577 for( size_t i
=0; i
<body
.getNumChildren(); i
++ ){
579 //set/update entailed conditions
580 std::vector
< Node
> new_cond
;
581 bool conflict
= false;
583 if( Trace
.isOn("quantifiers-rewrite-term-debug") ){
584 if( ( body
.getKind()==ITE
&& i
>0 ) || body
.getKind()==OR
|| body
.getKind()==AND
){
585 Trace("quantifiers-rewrite-term-debug") << "---rewrite " << body
[i
] << " under conditions:----" << std::endl
;
588 if( body
.getKind()==ITE
&& i
>0 ){
590 nCurrCond
= nCurrCond
+ 1;
592 setEntailedCond( children
[0], i
==1, currCond
, new_cond
, conflict
);
593 // should not conflict (entailment check failed)
596 if( body
.getKind()==OR
|| body
.getKind()==AND
){
597 bool use_pol
= body
.getKind()==AND
;
598 //remove the current condition
599 removeEntailedCond( currCond
, new_cond_children
[i
], cache
);
601 //add the previous condition
602 setEntailedCond( children
[i
-1], use_pol
, currCond
, new_cond_children
[i
-1], conflict
);
605 Trace("quantifiers-rewrite-term-debug") << "-------conflict, return " << !use_pol
<< std::endl
;
606 ret
= NodeManager::currentNM()->mkConst( !use_pol
);
609 if( !new_cond
.empty() ){
612 if( Trace
.isOn("quantifiers-rewrite-term-debug") ){
613 if( ( body
.getKind()==ITE
&& i
>0 ) || body
.getKind()==OR
|| body
.getKind()==AND
){
614 Trace("quantifiers-rewrite-term-debug") << "-------" << std::endl
;
619 //do the recursive call on children
623 QuantPhaseReq::getPolarity( body
, i
, hasPol
, pol
, newHasPol
, newPol
);
624 Node nn
= computeProcessTerms2( body
[i
], newHasPol
, newPol
, currCond
, nCurrCond
, cache
, icache
, new_vars
, new_conds
, elimExtArith
);
625 if( body
.getKind()==ITE
&& i
==0 ){
626 int res
= getEntailedCond( nn
, currCond
);
627 Trace("quantifiers-rewrite-term-debug") << "Condition for " << body
<< " is " << nn
<< ", entailment check=" << res
<< std::endl
;
629 ret
= computeProcessTerms2( body
[1], hasPol
, pol
, currCond
, nCurrCond
, cache
, icache
, new_vars
, new_conds
, elimExtArith
);
631 ret
= computeProcessTerms2( body
[2], hasPol
, pol
, currCond
, nCurrCond
, cache
, icache
, new_vars
, new_conds
, elimExtArith
);
634 children
.push_back( nn
);
635 changed
= changed
|| nn
!=body
[i
];
638 //clean up entailed conditions
639 removeEntailedCond( currCond
, new_cond
, cache
);
649 if( body
.getMetaKind() == kind::metakind::PARAMETERIZED
){
650 children
.insert( children
.begin(), body
.getOperator() );
652 ret
= NodeManager::currentNM()->mkNode( body
.getKind(), children
);
659 //clean up entailed conditions
660 if( body
.getKind()==OR
|| body
.getKind()==AND
){
661 for( unsigned j
=0; j
<body
.getNumChildren(); j
++ ){
662 removeEntailedCond( currCond
, new_cond_children
[j
], cache
);
666 Trace("quantifiers-rewrite-term-debug2") << "Returning " << ret
<< " for " << body
<< std::endl
;
670 //do context-independent rewriting
671 iti
= icache
.find( ret
);
672 if( iti
!=icache
.end() ){
676 if (ret
.getKind() == EQUAL
677 && options::iteLiftQuant() != options::IteLiftQuantMode::NONE
)
679 for( size_t i
=0; i
<2; i
++ ){
680 if( ret
[i
].getKind()==ITE
){
681 Node no
= i
==0 ? ret
[1] : ret
[0];
682 if( no
.getKind()!=ITE
){
684 options::iteLiftQuant() == options::IteLiftQuantMode::ALL
;
685 std::vector
< Node
> children
;
686 children
.push_back( ret
[i
][0] );
687 for( size_t j
=1; j
<=2; j
++ ){
688 //check if it rewrites to a constant
689 Node nn
= NodeManager::currentNM()->mkNode( EQUAL
, no
, ret
[i
][j
] );
690 nn
= Rewriter::rewrite( nn
);
691 children
.push_back( nn
);
697 ret
= NodeManager::currentNM()->mkNode( ITE
, children
);
704 else if (ret
.getKind() == SELECT
&& ret
[0].getKind() == STORE
)
708 std::vector
<Node
> iconds
;
709 std::vector
<Node
> elements
;
710 while (st
.getKind() == STORE
)
712 iconds
.push_back(index
.eqNode(st
[1]));
713 elements
.push_back(st
[2]);
716 ret
= nm
->mkNode(SELECT
, st
, index
);
718 for (int i
= (iconds
.size() - 1); i
>= 0; i
--)
720 ret
= nm
->mkNode(ITE
, iconds
[i
], elements
[i
], ret
);
723 else if( elimExtArith
)
725 if( ret
.getKind()==INTS_DIVISION_TOTAL
|| ret
.getKind()==INTS_MODULUS_TOTAL
){
729 const Rational
& rat
= den
.getConst
<Rational
>();
730 Assert(!num
.isConst());
732 Node intVar
= NodeManager::currentNM()->mkBoundVar(NodeManager::currentNM()->integerType());
733 new_vars
.push_back( intVar
);
736 cond
= NodeManager::currentNM()->mkNode(kind::AND
,
737 NodeManager::currentNM()->mkNode(kind::LEQ
, NodeManager::currentNM()->mkNode(kind::MULT
, den
, intVar
), num
),
738 NodeManager::currentNM()->mkNode(kind::LT
, num
,
739 NodeManager::currentNM()->mkNode(kind::MULT
, den
, NodeManager::currentNM()->mkNode(kind::PLUS
, intVar
, NodeManager::currentNM()->mkConst(Rational(1))))));
741 cond
= NodeManager::currentNM()->mkNode(kind::AND
,
742 NodeManager::currentNM()->mkNode(kind::LEQ
, NodeManager::currentNM()->mkNode(kind::MULT
, den
, intVar
), num
),
743 NodeManager::currentNM()->mkNode(kind::LT
, num
,
744 NodeManager::currentNM()->mkNode(kind::MULT
, den
, NodeManager::currentNM()->mkNode(kind::PLUS
, intVar
, NodeManager::currentNM()->mkConst(Rational(-1))))));
746 new_conds
.push_back( cond
.negate() );
747 if( ret
.getKind()==INTS_DIVISION_TOTAL
){
750 ret
= NodeManager::currentNM()->mkNode(kind::MINUS
, num
, NodeManager::currentNM()->mkNode(kind::MULT
, den
, intVar
));
754 }else if( ret
.getKind()==TO_INTEGER
|| ret
.getKind()==IS_INTEGER
){
755 Node intVar
= NodeManager::currentNM()->mkBoundVar(NodeManager::currentNM()->integerType());
756 new_vars
.push_back( intVar
);
757 new_conds
.push_back(NodeManager::currentNM()->mkNode(kind::AND
,
758 NodeManager::currentNM()->mkNode(kind::LT
,
759 NodeManager::currentNM()->mkNode(kind::MINUS
, ret
[0], NodeManager::currentNM()->mkConst(Rational(1))), intVar
),
760 NodeManager::currentNM()->mkNode(kind::LEQ
, intVar
, ret
[0])).negate());
761 if( ret
.getKind()==TO_INTEGER
){
764 ret
= ret
[0].eqNode( intVar
);
773 Node
QuantifiersRewriter::computeCondSplit(Node body
,
774 const std::vector
<Node
>& args
,
777 NodeManager
* nm
= NodeManager::currentNM();
778 Kind bk
= body
.getKind();
779 if (options::iteDtTesterSplitQuant() && bk
== ITE
780 && body
[0].getKind() == APPLY_TESTER
)
782 Trace("quantifiers-rewrite-ite-debug") << "DTT split : " << body
<< std::endl
;
783 std::map
< Node
, Node
> pcons
;
784 std::map
< Node
, std::map
< int, Node
> > ncons
;
785 std::vector
< Node
> conj
;
786 computeDtTesterIteSplit( body
, pcons
, ncons
, conj
);
787 Assert(!conj
.empty());
789 Trace("quantifiers-rewrite-ite") << "*** Split ITE (datatype tester) " << body
<< " into : " << std::endl
;
790 for( unsigned i
=0; i
<conj
.size(); i
++ ){
791 Trace("quantifiers-rewrite-ite") << " " << conj
[i
] << std::endl
;
793 return nm
->mkNode(AND
, conj
);
796 if (!options::condVarSplitQuant())
800 Trace("cond-var-split-debug")
801 << "Conditional var elim split " << body
<< "?" << std::endl
;
804 || (bk
== EQUAL
&& body
[0].getType().isBoolean()
805 && options::condVarSplitQuantAgg()))
807 Assert(!qa
.isFunDef());
808 bool do_split
= false;
809 unsigned index_max
= bk
== ITE
? 0 : 1;
810 std::vector
<Node
> tmpArgs
= args
;
811 for (unsigned index
= 0; index
<= index_max
; index
++)
813 if (hasVarElim(body
[index
], true, tmpArgs
)
814 || hasVarElim(body
[index
], false, tmpArgs
))
826 pos
= nm
->mkNode(OR
, body
[0].negate(), body
[1]);
827 neg
= nm
->mkNode(OR
, body
[0], body
[2]);
831 pos
= nm
->mkNode(OR
, body
[0].negate(), body
[1]);
832 neg
= nm
->mkNode(OR
, body
[0], body
[1].negate());
834 Trace("cond-var-split-debug") << "*** Split (conditional variable eq) "
835 << body
<< " into : " << std::endl
;
836 Trace("cond-var-split-debug") << " " << pos
<< std::endl
;
837 Trace("cond-var-split-debug") << " " << neg
<< std::endl
;
838 return nm
->mkNode(AND
, pos
, neg
);
844 unsigned size
= body
.getNumChildren();
845 bool do_split
= false;
846 unsigned split_index
= 0;
847 for (unsigned i
= 0; i
< size
; i
++)
849 // check if this child is a (conditional) variable elimination
851 if (b
.getKind() == AND
)
853 std::vector
<Node
> vars
;
854 std::vector
<Node
> subs
;
855 std::vector
<Node
> tmpArgs
= args
;
856 for (unsigned j
= 0, bsize
= b
.getNumChildren(); j
< bsize
; j
++)
858 if (getVarElimLit(b
[j
], false, tmpArgs
, vars
, subs
))
860 Trace("cond-var-split-debug") << "Variable elimination in child #"
861 << j
<< " under " << i
<< std::endl
;
862 // Figure out if we should split
863 // Currently we split if the aggressive option is set, or
864 // if the top-level OR is binary.
865 if (options::condVarSplitQuantAgg() || size
== 2)
869 // other splitting criteria go here
889 std::vector
<Node
> children
;
890 for (TNode bc
: body
)
892 children
.push_back(bc
);
894 std::vector
<Node
> split_children
;
895 for (TNode bci
: body
[split_index
])
897 children
[split_index
] = bci
;
898 split_children
.push_back(nm
->mkNode(OR
, children
));
900 // split the AND child, for example:
901 // ( x!=a ^ P(x) ) V Q(x) ---> ( x!=a V Q(x) ) ^ ( P(x) V Q(x) )
902 return nm
->mkNode(AND
, split_children
);
909 bool QuantifiersRewriter::isVarElim(Node v
, Node s
)
911 Assert(v
.getKind() == BOUND_VARIABLE
);
912 return !expr::hasSubterm(s
, v
) && s
.getType().isSubtypeOf(v
.getType());
915 Node
QuantifiersRewriter::getVarElimLitBv(Node lit
,
916 const std::vector
<Node
>& args
,
919 if (Trace
.isOn("quant-velim-bv"))
921 Trace("quant-velim-bv") << "Bv-Elim : " << lit
<< " varList = { ";
922 for (const Node
& v
: args
)
924 Trace("quant-velim-bv") << v
<< " ";
926 Trace("quant-velim-bv") << "} ?" << std::endl
;
928 Assert(lit
.getKind() == EQUAL
);
929 // TODO (#1494) : linearize the literal using utility
931 // compute a subset active_args of the bound variables args that occur in lit
932 std::vector
<Node
> active_args
;
933 computeArgVec(args
, active_args
, lit
);
936 for (const Node
& cvar
: active_args
)
938 // solve for the variable on this path using the inverter
939 std::vector
<unsigned> path
;
940 Node slit
= binv
.getPathToPv(lit
, cvar
, path
);
943 Node slv
= binv
.solveBvLit(cvar
, lit
, path
, nullptr);
944 Trace("quant-velim-bv") << "...solution : " << slv
<< std::endl
;
948 // if this is a proper variable elimination, that is, var = slv where
949 // var is not in the free variables of slv, then we can return this
950 // as the variable elimination for lit.
951 if (isVarElim(var
, slv
))
959 Trace("quant-velim-bv") << "...non-invertible path." << std::endl
;
966 Node
QuantifiersRewriter::getVarElimLitString(Node lit
,
967 const std::vector
<Node
>& args
,
970 Assert(lit
.getKind() == EQUAL
);
971 NodeManager
* nm
= NodeManager::currentNM();
972 for (unsigned i
= 0; i
< 2; i
++)
974 if (lit
[i
].getKind() == STRING_CONCAT
)
976 for (unsigned j
= 0, nchildren
= lit
[i
].getNumChildren(); j
< nchildren
;
979 if (std::find(args
.begin(), args
.end(), lit
[i
][j
]) != args
.end())
982 Node slv
= lit
[1 - i
];
983 std::vector
<Node
> preL(lit
[i
].begin(), lit
[i
].begin() + j
);
984 std::vector
<Node
> postL(lit
[i
].begin() + j
+ 1, lit
[i
].end());
985 Node tpre
= strings::utils::mkConcat(STRING_CONCAT
, preL
);
986 Node tpost
= strings::utils::mkConcat(STRING_CONCAT
, postL
);
987 Node slvL
= nm
->mkNode(STRING_LENGTH
, slv
);
988 Node tpreL
= nm
->mkNode(STRING_LENGTH
, tpre
);
989 Node tpostL
= nm
->mkNode(STRING_LENGTH
, tpost
);
994 nm
->mkNode(MINUS
, slvL
, nm
->mkNode(PLUS
, tpreL
, tpostL
)));
995 // forall x. r ++ x ++ t = s => P( x )
997 // r ++ s' ++ t = s => P( s' ) where
998 // s' = substr( s, |r|, |s|-(|t|+|r|) ).
999 // We apply this only if r,t,s do not contain free variables.
1000 if (!expr::hasFreeVar(slv
))
1009 return Node::null();
1012 bool QuantifiersRewriter::getVarElimLit(Node lit
,
1014 std::vector
<Node
>& args
,
1015 std::vector
<Node
>& vars
,
1016 std::vector
<Node
>& subs
)
1018 if (lit
.getKind() == NOT
)
1020 return getVarElimLit(lit
[0], !pol
, args
, vars
, subs
);
1022 NodeManager
* nm
= NodeManager::currentNM();
1023 Trace("var-elim-quant-debug")
1024 << "Eliminate : " << lit
<< ", pol = " << pol
<< "?" << std::endl
;
1025 if (lit
.getKind() == APPLY_TESTER
&& pol
&& lit
[0].getKind() == BOUND_VARIABLE
1026 && options::dtVarExpandQuant())
1028 Trace("var-elim-dt") << "Expand datatype variable based on : " << lit
1030 std::vector
<Node
>::iterator ita
=
1031 std::find(args
.begin(), args
.end(), lit
[0]);
1032 if (ita
!= args
.end())
1034 vars
.push_back(lit
[0]);
1035 Node tester
= lit
.getOperator();
1036 int index
= datatypes::utils::indexOf(tester
);
1037 const DType
& dt
= datatypes::utils::datatypeOf(tester
);
1038 const DTypeConstructor
& c
= dt
[index
];
1039 std::vector
<Node
> newChildren
;
1040 newChildren
.push_back(c
.getConstructor());
1041 std::vector
<Node
> newVars
;
1042 for (unsigned j
= 0, nargs
= c
.getNumArgs(); j
< nargs
; j
++)
1044 TypeNode tn
= c
[j
].getRangeType();
1045 Node v
= nm
->mkBoundVar(tn
);
1046 newChildren
.push_back(v
);
1047 newVars
.push_back(v
);
1049 subs
.push_back(nm
->mkNode(APPLY_CONSTRUCTOR
, newChildren
));
1050 Trace("var-elim-dt") << "...apply substitution " << subs
[0] << "/"
1051 << vars
[0] << std::endl
;
1053 args
.insert(args
.end(), newVars
.begin(), newVars
.end());
1057 // all eliminations below guarded by varElimQuant()
1058 if (!options::varElimQuant())
1063 if (lit
.getKind() == EQUAL
)
1065 if (pol
|| lit
[0].getType().isBoolean())
1067 for (unsigned i
= 0; i
< 2; i
++)
1070 Node v_slv
= lit
[i
];
1071 if (v_slv
.getKind() == NOT
)
1076 std::vector
<Node
>::iterator ita
=
1077 std::find(args
.begin(), args
.end(), v_slv
);
1078 if (ita
!= args
.end())
1080 if (isVarElim(v_slv
, lit
[1 - i
]))
1082 Node slv
= lit
[1 - i
];
1085 Assert(slv
.getType().isBoolean());
1088 Trace("var-elim-quant")
1089 << "Variable eliminate based on equality : " << v_slv
<< " -> "
1090 << slv
<< std::endl
;
1091 vars
.push_back(v_slv
);
1092 subs
.push_back(slv
);
1100 else if (lit
.getKind() == APPLY_TESTER
&& pol
1101 && lit
[0].getKind() == BOUND_VARIABLE
&& options::dtVarExpandQuant())
1103 Trace("var-elim-dt") << "Expand datatype variable based on : " << lit
1105 Node tester
= lit
.getOperator();
1106 unsigned index
= datatypes::utils::indexOf(tester
);
1107 Node s
= datatypeExpand(index
, lit
[0], args
);
1110 vars
.push_back(lit
[0]);
1112 Trace("var-elim-dt") << "...apply substitution " << s
<< "/" << lit
[0]
1117 if (lit
.getKind() == BOUND_VARIABLE
)
1119 std::vector
< Node
>::iterator ita
= std::find( args
.begin(), args
.end(), lit
);
1120 if( ita
!=args
.end() ){
1121 Trace("var-elim-bool") << "Variable eliminate : " << lit
<< std::endl
;
1122 vars
.push_back( lit
);
1123 subs
.push_back( NodeManager::currentNM()->mkConst( pol
) );
1128 if (lit
.getKind() == EQUAL
&& lit
[0].getType().isReal() && pol
)
1130 // for arithmetic, solve the equality
1131 std::map
< Node
, Node
> msum
;
1132 if (ArithMSum::getMonomialSumLit(lit
, msum
))
1134 for( std::map
< Node
, Node
>::iterator itm
= msum
.begin(); itm
!= msum
.end(); ++itm
){
1135 if( !itm
->first
.isNull() ){
1136 std::vector
< Node
>::iterator ita
= std::find( args
.begin(), args
.end(), itm
->first
);
1137 if( ita
!=args
.end() ){
1141 int ires
= ArithMSum::isolate(itm
->first
, msum
, veq_c
, val
, EQUAL
);
1142 if (ires
!= 0 && veq_c
.isNull() && isVarElim(itm
->first
, val
))
1144 Trace("var-elim-quant")
1145 << "Variable eliminate based on solved equality : "
1146 << itm
->first
<< " -> " << val
<< std::endl
;
1147 vars
.push_back(itm
->first
);
1148 subs
.push_back(val
);
1157 if (lit
.getKind() == EQUAL
&& pol
)
1161 TypeNode tt
= lit
[0].getType();
1162 if (tt
.isBitVector())
1164 slv
= getVarElimLitBv(lit
, args
, var
);
1166 else if (tt
.isString())
1168 slv
= getVarElimLitString(lit
, args
, var
);
1172 Assert(!var
.isNull());
1173 std::vector
<Node
>::iterator ita
=
1174 std::find(args
.begin(), args
.end(), var
);
1175 Assert(ita
!= args
.end());
1176 Trace("var-elim-quant")
1177 << "Variable eliminate based on theory-specific solving : " << var
1178 << " -> " << slv
<< std::endl
;
1179 Assert(!expr::hasSubterm(slv
, var
));
1180 Assert(slv
.getType().isSubtypeOf(var
.getType()));
1181 vars
.push_back(var
);
1182 subs
.push_back(slv
);
1190 Node
QuantifiersRewriter::datatypeExpand(unsigned index
,
1192 std::vector
<Node
>& args
)
1194 if (!v
.getType().isDatatype())
1196 return Node::null();
1198 std::vector
<Node
>::iterator ita
= std::find(args
.begin(), args
.end(), v
);
1199 if (ita
== args
.end())
1201 return Node::null();
1203 const DType
& dt
= v
.getType().getDType();
1204 Assert(index
< dt
.getNumConstructors());
1205 const DTypeConstructor
& c
= dt
[index
];
1206 std::vector
<Node
> newChildren
;
1207 newChildren
.push_back(c
.getConstructor());
1208 std::vector
<Node
> newVars
;
1209 for (unsigned j
= 0, nargs
= c
.getNumArgs(); j
< nargs
; j
++)
1211 TypeNode tn
= c
.getArgType(j
);
1212 Node vn
= NodeManager::currentNM()->mkBoundVar(tn
);
1213 newChildren
.push_back(vn
);
1214 newVars
.push_back(vn
);
1217 args
.insert(args
.end(), newVars
.begin(), newVars
.end());
1218 return NodeManager::currentNM()->mkNode(APPLY_CONSTRUCTOR
, newChildren
);
1221 bool QuantifiersRewriter::getVarElim(Node n
,
1223 std::vector
<Node
>& args
,
1224 std::vector
<Node
>& vars
,
1225 std::vector
<Node
>& subs
)
1227 Kind nk
= n
.getKind();
1230 return getVarElim(n
[0], !pol
, args
, vars
, subs
);
1232 else if ((nk
== AND
&& pol
) || (nk
== OR
&& !pol
))
1234 for (const Node
& cn
: n
)
1236 if (getVarElim(cn
, pol
, args
, vars
, subs
))
1243 return getVarElimLit(n
, pol
, args
, vars
, subs
);
1246 bool QuantifiersRewriter::hasVarElim(Node n
, bool pol
, std::vector
<Node
>& args
)
1248 std::vector
< Node
> vars
;
1249 std::vector
< Node
> subs
;
1250 return getVarElim(n
, pol
, args
, vars
, subs
);
1253 bool QuantifiersRewriter::getVarElimIneq(Node body
,
1254 std::vector
<Node
>& args
,
1255 std::vector
<Node
>& bounds
,
1256 std::vector
<Node
>& subs
,
1259 // elimination based on inequalities
1260 std::map
<Node
, std::map
<bool, std::map
<Node
, bool> > > num_bounds
;
1261 QuantPhaseReq
qpr(body
);
1262 for (const std::pair
<const Node
, bool>& pr
: qpr
.d_phase_reqs
)
1264 // an inequality that is entailed with a given polarity
1265 Node lit
= pr
.first
;
1266 if (lit
.getKind() != GEQ
)
1270 bool pol
= pr
.second
;
1271 Trace("var-elim-quant-debug") << "Process inequality bounds : " << lit
1272 << ", pol = " << pol
<< "..." << std::endl
;
1273 // solve the inequality
1274 std::map
<Node
, Node
> msum
;
1275 if (!ArithMSum::getMonomialSumLit(lit
, msum
))
1277 // not an inequality, cannot use
1280 for (const std::pair
<const Node
, Node
>& m
: msum
)
1282 if (!m
.first
.isNull())
1284 std::vector
<Node
>::iterator ita
=
1285 std::find(args
.begin(), args
.end(), m
.first
);
1286 if (ita
!= args
.end())
1288 // store that this literal is upper/lower bound for itm->first
1292 ArithMSum::isolate(m
.first
, msum
, veq_c
, val
, lit
.getKind());
1293 if (ires
!= 0 && veq_c
.isNull())
1295 bool is_upper
= pol
!= (ires
== 1);
1296 Trace("var-elim-ineq-debug")
1297 << lit
<< " is a " << (is_upper
? "upper" : "lower")
1298 << " bound for " << m
.first
<< std::endl
;
1299 Trace("var-elim-ineq-debug")
1300 << " pol/ires = " << pol
<< " " << ires
<< std::endl
;
1301 num_bounds
[m
.first
][is_upper
][lit
] = pol
;
1305 Trace("var-elim-ineq-debug")
1306 << "...ineligible " << m
.first
1307 << " since it cannot be solved for (" << ires
<< ", " << veq_c
1308 << ")." << std::endl
;
1309 num_bounds
[m
.first
][true].clear();
1310 num_bounds
[m
.first
][false].clear();
1315 // compute variables in itm->first, these are not eligible for
1317 std::unordered_set
<Node
, NodeHashFunction
> fvs
;
1318 expr::getFreeVariables(m
.first
, fvs
);
1319 for (const Node
& v
: fvs
)
1321 Trace("var-elim-ineq-debug")
1322 << "...ineligible " << v
1323 << " since it is contained in monomial." << std::endl
;
1324 num_bounds
[v
][true].clear();
1325 num_bounds
[v
][false].clear();
1332 // collect all variables that have only upper/lower bounds
1333 std::map
<Node
, bool> elig_vars
;
1334 for (const std::pair
<const Node
, std::map
<bool, std::map
<Node
, bool> > >& nb
:
1337 if (nb
.second
.find(true) == nb
.second
.end())
1339 Trace("var-elim-ineq-debug")
1340 << "Variable " << nb
.first
<< " has only lower bounds." << std::endl
;
1341 elig_vars
[nb
.first
] = false;
1343 else if (nb
.second
.find(false) == nb
.second
.end())
1345 Trace("var-elim-ineq-debug")
1346 << "Variable " << nb
.first
<< " has only upper bounds." << std::endl
;
1347 elig_vars
[nb
.first
] = true;
1350 if (elig_vars
.empty())
1354 std::vector
<Node
> inactive_vars
;
1355 std::map
<Node
, std::map
<int, bool> > visited
;
1356 std::map
<Node
, int> exclude
;
1357 for (const std::pair
<Node
, bool>& pr
: qpr
.d_phase_reqs
)
1359 if (pr
.first
.getKind() == GEQ
)
1361 exclude
[pr
.first
] = pr
.second
? -1 : 1;
1362 Trace("var-elim-ineq-debug")
1363 << "...exclude " << pr
.first
<< " at polarity " << exclude
[pr
.first
]
1367 // traverse the body, invalidate variables if they occur in places other than
1368 // the bounds they occur in
1369 std::unordered_map
<TNode
, std::unordered_set
<int>, TNodeHashFunction
>
1371 std::vector
<TNode
> evisit
;
1372 std::vector
<int> evisit_pol
;
1375 evisit
.push_back(body
);
1376 evisit_pol
.push_back(1);
1377 if (!qa
.d_ipl
.isNull())
1379 // do not eliminate variables that occur in the annotation
1380 evisit
.push_back(qa
.d_ipl
);
1381 evisit_pol
.push_back(0);
1385 ecur
= evisit
.back();
1387 ecur_pol
= evisit_pol
.back();
1388 evisit_pol
.pop_back();
1389 std::unordered_set
<int>& epp
= evisited
[ecur
];
1390 if (epp
.find(ecur_pol
) == epp
.end())
1392 epp
.insert(ecur_pol
);
1393 if (elig_vars
.find(ecur
) != elig_vars
.end())
1395 // variable contained in a place apart from bounds, no longer eligible
1397 elig_vars
.erase(ecur
);
1398 Trace("var-elim-ineq-debug") << "...found occurrence of " << ecur
1399 << ", mark ineligible" << std::endl
;
1404 bool pol
= ecur_pol
>= 0;
1405 bool hasPol
= ecur_pol
!= 0;
1408 std::map
<Node
, int>::iterator itx
= exclude
.find(ecur
);
1409 if (itx
!= exclude
.end() && itx
->second
== ecur_pol
)
1411 // already processed this literal as a bound
1417 for (unsigned j
= 0, size
= ecur
.getNumChildren(); j
< size
; j
++)
1421 QuantPhaseReq::getPolarity(ecur
, j
, hasPol
, pol
, newHasPol
, newPol
);
1422 evisit
.push_back(ecur
[j
]);
1423 evisit_pol
.push_back(newHasPol
? (newPol
? 1 : -1) : 0);
1428 } while (!evisit
.empty() && !elig_vars
.empty());
1431 for (const std::pair
<Node
, bool>& ev
: elig_vars
)
1434 Trace("var-elim-ineq-debug")
1435 << v
<< " is eligible for elimination." << std::endl
;
1436 // do substitution corresponding to infinite projection, all literals
1437 // involving unbounded variable go to true/false
1438 for (const std::pair
<const Node
, bool>& nb
: num_bounds
[v
][elig_vars
[v
]])
1440 Trace("var-elim-ineq-debug")
1441 << " subs : " << nb
.first
<< " -> " << nb
.second
<< std::endl
;
1442 bounds
.push_back(nb
.first
);
1443 subs
.push_back(NodeManager::currentNM()->mkConst(nb
.second
));
1445 // eliminate from args
1446 std::vector
<Node
>::iterator ita
= std::find(args
.begin(), args
.end(), v
);
1447 Assert(ita
!= args
.end());
1454 Node
QuantifiersRewriter::computeVarElimination( Node body
, std::vector
< Node
>& args
, QAttributes
& qa
){
1455 if (!options::varElimQuant() && !options::dtVarExpandQuant()
1456 && !options::varIneqElimQuant())
1461 while (prev
!= body
&& !args
.empty())
1465 std::vector
<Node
> vars
;
1466 std::vector
<Node
> subs
;
1467 // standard variable elimination
1468 if (options::varElimQuant())
1470 getVarElim(body
, false, args
, vars
, subs
);
1472 // variable elimination based on one-direction inequalities
1473 if (vars
.empty() && options::varIneqElimQuant())
1475 getVarElimIneq(body
, args
, vars
, subs
, qa
);
1477 // if we eliminated a variable, update body and reprocess
1480 Trace("var-elim-quant-debug")
1481 << "VE " << vars
.size() << "/" << args
.size() << std::endl
;
1482 Assert(vars
.size() == subs
.size());
1483 // remake with eliminated nodes
1485 body
.substitute(vars
.begin(), vars
.end(), subs
.begin(), subs
.end());
1486 body
= Rewriter::rewrite(body
);
1487 if (!qa
.d_ipl
.isNull())
1489 qa
.d_ipl
= qa
.d_ipl
.substitute(
1490 vars
.begin(), vars
.end(), subs
.begin(), subs
.end());
1492 Trace("var-elim-quant") << "Return " << body
<< std::endl
;
1498 Node
QuantifiersRewriter::computePrenex( Node body
, std::vector
< Node
>& args
, std::vector
< Node
>& nargs
, bool pol
, bool prenexAgg
){
1499 if( body
.getKind()==FORALL
){
1500 if( ( pol
|| prenexAgg
) && ( options::prenexQuantUser() || body
.getNumChildren()==2 ) ){
1501 std::vector
< Node
> terms
;
1502 std::vector
< Node
> subs
;
1503 //for doing prenexing of same-signed quantifiers
1504 //must rename each variable that already exists
1505 for( unsigned i
=0; i
<body
[0].getNumChildren(); i
++ ){
1506 terms
.push_back( body
[0][i
] );
1507 subs
.push_back( NodeManager::currentNM()->mkBoundVar( body
[0][i
].getType() ) );
1510 args
.insert( args
.end(), subs
.begin(), subs
.end() );
1512 nargs
.insert( nargs
.end(), subs
.begin(), subs
.end() );
1514 Node newBody
= body
[1];
1515 newBody
= newBody
.substitute( terms
.begin(), terms
.end(), subs
.begin(), subs
.end() );
1518 //must remove structure
1519 }else if( prenexAgg
&& body
.getKind()==kind::ITE
&& body
.getType().isBoolean() ){
1520 Node nn
= NodeManager::currentNM()->mkNode( kind::AND
,
1521 NodeManager::currentNM()->mkNode( kind::OR
, body
[0].notNode(), body
[1] ),
1522 NodeManager::currentNM()->mkNode( kind::OR
, body
[0], body
[2] ) );
1523 return computePrenex( nn
, args
, nargs
, pol
, prenexAgg
);
1524 }else if( prenexAgg
&& body
.getKind()==kind::EQUAL
&& body
[0].getType().isBoolean() ){
1525 Node nn
= NodeManager::currentNM()->mkNode( kind::AND
,
1526 NodeManager::currentNM()->mkNode( kind::OR
, body
[0].notNode(), body
[1] ),
1527 NodeManager::currentNM()->mkNode( kind::OR
, body
[0], body
[1].notNode() ) );
1528 return computePrenex( nn
, args
, nargs
, pol
, prenexAgg
);
1529 }else if( body
.getType().isBoolean() ){
1530 Assert(body
.getKind() != EXISTS
);
1531 bool childrenChanged
= false;
1532 std::vector
< Node
> newChildren
;
1533 for( unsigned i
=0; i
<body
.getNumChildren(); i
++ ){
1536 QuantPhaseReq::getPolarity( body
, i
, true, pol
, newHasPol
, newPol
);
1538 Node n
= computePrenex( body
[i
], args
, nargs
, newPol
, prenexAgg
);
1539 newChildren
.push_back( n
);
1541 childrenChanged
= true;
1544 newChildren
.push_back( body
[i
] );
1547 if( childrenChanged
){
1548 if( body
.getKind()==NOT
&& newChildren
[0].getKind()==NOT
){
1549 return newChildren
[0][0];
1551 return NodeManager::currentNM()->mkNode( body
.getKind(), newChildren
);
1558 Node
QuantifiersRewriter::computePrenexAgg( Node n
, bool topLevel
, std::map
< unsigned, std::map
< Node
, Node
> >& visited
){
1559 unsigned tindex
= topLevel
? 0 : 1;
1560 std::map
< Node
, Node
>::iterator itv
= visited
[tindex
].find( n
);
1561 if( itv
!=visited
[tindex
].end() ){
1564 if (expr::hasClosure(n
))
1568 && options::prenexQuant() == options::PrenexQuantMode::DISJ_NORMAL
1569 && (n
.getKind() == AND
|| (n
.getKind() == NOT
&& n
[0].getKind() == OR
)))
1571 std::vector
< Node
> children
;
1572 Node nc
= n
.getKind()==NOT
? n
[0] : n
;
1573 for( unsigned i
=0; i
<nc
.getNumChildren(); i
++ ){
1574 Node ncc
= computePrenexAgg( nc
[i
], true, visited
);
1575 if( n
.getKind()==NOT
){
1578 children
.push_back( ncc
);
1580 ret
= NodeManager::currentNM()->mkNode( AND
, children
);
1582 else if (n
.getKind() == NOT
)
1584 ret
= computePrenexAgg( n
[0], false, visited
).negate();
1586 else if (n
.getKind() == FORALL
)
1589 Node nn = computePrenexAgg( n[1], false );
1591 if( n.getNumChildren()==2 ){
1592 return NodeManager::currentNM()->mkNode( FORALL, n[0], nn );
1594 return NodeManager::currentNM()->mkNode( FORALL, n[0], nn, n[2] );
1598 std::vector
< Node
> children
;
1599 if (n
[1].getKind() == OR
1600 && options::prenexQuant() == options::PrenexQuantMode::DISJ_NORMAL
)
1602 for( unsigned i
=0; i
<n
[1].getNumChildren(); i
++ ){
1603 children
.push_back( computePrenexAgg( n
[1][i
], false, visited
) );
1608 children
.push_back( computePrenexAgg( n
[1], false, visited
) );
1610 std::vector
< Node
> args
;
1611 for( unsigned i
=0; i
<n
[0].getNumChildren(); i
++ ){
1612 args
.push_back( n
[0][i
] );
1614 std::vector
< Node
> nargs
;
1615 //for each child, strip top level quant
1616 for( unsigned i
=0; i
<children
.size(); i
++ ){
1617 if( children
[i
].getKind()==FORALL
){
1618 for( unsigned j
=0; j
<children
[i
][0].getNumChildren(); j
++ ){
1619 args
.push_back( children
[i
][0][j
] );
1621 children
[i
] = children
[i
][1];
1625 std::vector
< Node
> iplc
;
1626 if( n
.getNumChildren()==3 ){
1627 for( unsigned i
=0; i
<n
[2].getNumChildren(); i
++ ){
1628 iplc
.push_back( n
[2][i
] );
1631 Node nb
= children
.size()==1 ? children
[0] : NodeManager::currentNM()->mkNode( OR
, children
);
1632 ret
= mkForall( args
, nb
, iplc
, true );
1636 std::vector
< Node
> args
;
1637 std::vector
< Node
> nargs
;
1638 Node nn
= computePrenex( n
, args
, nargs
, true, true );
1640 Node nnn
= computePrenexAgg( nn
, false, visited
);
1642 if( nnn
.getKind()==FORALL
){
1643 for( unsigned i
=0; i
<nnn
[0].getNumChildren(); i
++ ){
1644 args
.push_back( nnn
[0][i
] );
1647 //pos polarity variables are inner
1648 if( !args
.empty() ){
1649 nnn
= mkForall( args
, nnn
, true );
1652 }else if( nnn
.getKind()==NOT
&& nnn
[0].getKind()==FORALL
){
1653 for( unsigned i
=0; i
<nnn
[0][0].getNumChildren(); i
++ ){
1654 nargs
.push_back( nnn
[0][0][i
] );
1656 nnn
= nnn
[0][1].negate();
1658 if( !nargs
.empty() ){
1659 nnn
= mkForall( nargs
, nnn
.negate(), true ).negate();
1661 if( !args
.empty() ){
1662 nnn
= mkForall( args
, nnn
, true );
1666 Assert(args
.empty());
1667 Assert(nargs
.empty());
1670 visited
[tindex
][n
] = ret
;
1676 Node
QuantifiersRewriter::computeSplit( std::vector
< Node
>& args
, Node body
, QAttributes
& qa
) {
1677 Assert(body
.getKind() == OR
);
1678 size_t var_found_count
= 0;
1679 size_t eqc_count
= 0;
1680 size_t eqc_active
= 0;
1681 std::map
< Node
, int > var_to_eqc
;
1682 std::map
< int, std::vector
< Node
> > eqc_to_var
;
1683 std::map
< int, std::vector
< Node
> > eqc_to_lit
;
1685 std::vector
<Node
> lits
;
1687 for( unsigned i
=0; i
<body
.getNumChildren(); i
++ ){
1688 //get variables contained in the literal
1690 std::vector
< Node
> lit_args
;
1691 computeArgVec( args
, lit_args
, n
);
1692 if( lit_args
.empty() ){
1693 lits
.push_back( n
);
1695 //collect the equivalence classes this literal belongs to, and the new variables it contributes
1696 std::vector
< int > eqcs
;
1697 std::vector
< Node
> lit_new_args
;
1698 //for each variable in literal
1699 for( unsigned j
=0; j
<lit_args
.size(); j
++) {
1700 //see if the variable has already been found
1701 if (var_to_eqc
.find(lit_args
[j
])!=var_to_eqc
.end()) {
1702 int eqc
= var_to_eqc
[lit_args
[j
]];
1703 if (std::find(eqcs
.begin(), eqcs
.end(), eqc
)==eqcs
.end()) {
1704 eqcs
.push_back(eqc
);
1708 lit_new_args
.push_back(lit_args
[j
]);
1712 eqcs
.push_back(eqc_count
);
1718 //merge equivalence classes with eqcz
1719 for (unsigned j
=1; j
<eqcs
.size(); j
++) {
1721 //move all variables from equivalence class
1722 for (unsigned k
=0; k
<eqc_to_var
[eqc
].size(); k
++) {
1723 Node v
= eqc_to_var
[eqc
][k
];
1724 var_to_eqc
[v
] = eqcz
;
1725 eqc_to_var
[eqcz
].push_back(v
);
1727 eqc_to_var
.erase(eqc
);
1728 //move all literals from equivalence class
1729 for (unsigned k
=0; k
<eqc_to_lit
[eqc
].size(); k
++) {
1730 Node l
= eqc_to_lit
[eqc
][k
];
1731 eqc_to_lit
[eqcz
].push_back(l
);
1733 eqc_to_lit
.erase(eqc
);
1736 //add variables to equivalence class
1737 for (unsigned j
=0; j
<lit_new_args
.size(); j
++) {
1738 var_to_eqc
[lit_new_args
[j
]] = eqcz
;
1739 eqc_to_var
[eqcz
].push_back(lit_new_args
[j
]);
1741 //add literal to equivalence class
1742 eqc_to_lit
[eqcz
].push_back(n
);
1745 if ( eqc_active
>1 || !lits
.empty() || var_to_eqc
.size()!=args
.size() ){
1746 Trace("clause-split-debug") << "Split quantified formula with body " << body
<< std::endl
;
1747 Trace("clause-split-debug") << " Ground literals: " << std::endl
;
1748 for( size_t i
=0; i
<lits
.size(); i
++) {
1749 Trace("clause-split-debug") << " " << lits
[i
] << std::endl
;
1751 Trace("clause-split-debug") << std::endl
;
1752 Trace("clause-split-debug") << "Equivalence classes: " << std::endl
;
1753 for (std::map
< int, std::vector
< Node
> >::iterator it
= eqc_to_lit
.begin(); it
!= eqc_to_lit
.end(); ++it
){
1754 Trace("clause-split-debug") << " Literals: " << std::endl
;
1755 for (size_t i
=0; i
<it
->second
.size(); i
++) {
1756 Trace("clause-split-debug") << " " << it
->second
[i
] << std::endl
;
1758 int eqc
= it
->first
;
1759 Trace("clause-split-debug") << " Variables: " << std::endl
;
1760 for (size_t i
=0; i
<eqc_to_var
[eqc
].size(); i
++) {
1761 Trace("clause-split-debug") << " " << eqc_to_var
[eqc
][i
] << std::endl
;
1763 Trace("clause-split-debug") << std::endl
;
1764 Node bvl
= NodeManager::currentNM()->mkNode( BOUND_VAR_LIST
, eqc_to_var
[eqc
]);
1765 Node body
= it
->second
.size()==1 ? it
->second
[0] : NodeManager::currentNM()->mkNode( OR
, it
->second
);
1766 Node fa
= NodeManager::currentNM()->mkNode( FORALL
, bvl
, body
);
1769 Assert(!lits
.empty());
1770 Node nf
= lits
.size()==1 ? lits
[0] : NodeManager::currentNM()->mkNode(OR
,lits
);
1771 Trace("clause-split-debug") << "Made node : " << nf
<< std::endl
;
1774 return mkForAll( args
, body
, qa
);
1778 Node
QuantifiersRewriter::mkForAll( std::vector
< Node
>& args
, Node body
, QAttributes
& qa
){
1782 std::vector
< Node
> children
;
1783 children
.push_back( NodeManager::currentNM()->mkNode(kind::BOUND_VAR_LIST
, args
) );
1784 children
.push_back( body
);
1785 if( !qa
.d_ipl
.isNull() ){
1786 children
.push_back( qa
.d_ipl
);
1788 return NodeManager::currentNM()->mkNode( kind::FORALL
, children
);
1792 Node
QuantifiersRewriter::mkForall( std::vector
< Node
>& args
, Node body
, bool marked
) {
1793 std::vector
< Node
> iplc
;
1794 return mkForall( args
, body
, iplc
, marked
);
1797 Node
QuantifiersRewriter::mkForall( std::vector
< Node
>& args
, Node body
, std::vector
< Node
>& iplc
, bool marked
) {
1801 std::vector
< Node
> children
;
1802 children
.push_back( NodeManager::currentNM()->mkNode(kind::BOUND_VAR_LIST
, args
) );
1803 children
.push_back( body
);
1805 Node avar
= NodeManager::currentNM()->mkSkolem( "id", NodeManager::currentNM()->booleanType() );
1806 QuantIdNumAttribute ida
;
1807 avar
.setAttribute(ida
,0);
1808 iplc
.push_back( NodeManager::currentNM()->mkNode( INST_ATTRIBUTE
, avar
) );
1810 if( !iplc
.empty() ){
1811 children
.push_back( NodeManager::currentNM()->mkNode( INST_PATTERN_LIST
, iplc
) );
1813 return NodeManager::currentNM()->mkNode( FORALL
, children
);
1817 //computes miniscoping, also eliminates variables that do not occur free in body
1818 Node
QuantifiersRewriter::computeMiniscoping( std::vector
< Node
>& args
, Node body
, QAttributes
& qa
){
1819 if( body
.getKind()==FORALL
){
1821 std::vector
< Node
> newArgs
;
1822 newArgs
.insert( newArgs
.end(), args
.begin(), args
.end() );
1823 for( unsigned i
=0; i
<body
[0].getNumChildren(); i
++ ){
1824 newArgs
.push_back( body
[0][i
] );
1826 return mkForAll( newArgs
, body
[1], qa
);
1827 }else if( body
.getKind()==AND
){
1828 if( options::miniscopeQuant() ){
1830 NodeBuilder
<> t(kind::AND
);
1831 for( unsigned i
=0; i
<body
.getNumChildren(); i
++ ){
1832 t
<< computeMiniscoping( args
, body
[i
], qa
);
1837 }else if( body
.getKind()==OR
){
1838 if( options::quantSplit() ){
1839 //splitting subsumes free variable miniscoping, apply it with higher priority
1840 return computeSplit( args
, body
, qa
);
1841 }else if( options::miniscopeQuantFreeVar() ){
1842 Node newBody
= body
;
1843 NodeBuilder
<> body_split(kind::OR
);
1844 NodeBuilder
<> tb(kind::OR
);
1845 for (const Node
& trm
: body
)
1847 if (expr::hasSubterm(trm
, args
))
1854 if( tb
.getNumChildren()==0 ){
1856 }else if( body_split
.getNumChildren()>0 ){
1857 newBody
= tb
.getNumChildren()==1 ? tb
.getChild( 0 ) : tb
;
1858 std::vector
< Node
> activeArgs
;
1859 computeArgVec2( args
, activeArgs
, newBody
, qa
.d_ipl
);
1860 body_split
<< mkForAll( activeArgs
, newBody
, qa
);
1861 return body_split
.getNumChildren()==1 ? body_split
.getChild( 0 ) : body_split
;
1864 }else if( body
.getKind()==NOT
){
1865 Assert(isLiteral(body
[0]));
1867 //remove variables that don't occur
1868 std::vector
< Node
> activeArgs
;
1869 computeArgVec2( args
, activeArgs
, body
, qa
.d_ipl
);
1870 return mkForAll( activeArgs
, body
, qa
);
1873 Node
QuantifiersRewriter::computeAggressiveMiniscoping( std::vector
< Node
>& args
, Node body
){
1874 std::map
<Node
, std::vector
<Node
> > varLits
;
1875 std::map
<Node
, std::vector
<Node
> > litVars
;
1876 if (body
.getKind() == OR
) {
1877 Trace("ag-miniscope") << "compute aggressive miniscoping on " << body
<< std::endl
;
1878 for (size_t i
= 0; i
< body
.getNumChildren(); i
++) {
1879 std::vector
<Node
> activeArgs
;
1880 computeArgVec(args
, activeArgs
, body
[i
]);
1881 for (unsigned j
= 0; j
< activeArgs
.size(); j
++) {
1882 varLits
[activeArgs
[j
]].push_back(body
[i
]);
1884 std::vector
<Node
>& lit_body_i
= litVars
[body
[i
]];
1885 std::vector
<Node
>::iterator lit_body_i_begin
= lit_body_i
.begin();
1886 std::vector
<Node
>::const_iterator active_begin
= activeArgs
.begin();
1887 std::vector
<Node
>::const_iterator active_end
= activeArgs
.end();
1888 lit_body_i
.insert(lit_body_i_begin
, active_begin
, active_end
);
1890 //find the variable in the least number of literals
1892 for( std::map
< Node
, std::vector
<Node
> >::iterator it
= varLits
.begin(); it
!= varLits
.end(); ++it
){
1893 if( bestVar
.isNull() || varLits
[bestVar
].size()>it
->second
.size() ){
1894 bestVar
= it
->first
;
1897 Trace("ag-miniscope-debug") << "Best variable " << bestVar
<< " occurs in " << varLits
[bestVar
].size() << "/ " << body
.getNumChildren() << " literals." << std::endl
;
1898 if( !bestVar
.isNull() && varLits
[bestVar
].size()<body
.getNumChildren() ){
1900 Trace("ag-miniscope") << "Miniscope on " << bestVar
<< std::endl
;
1902 std::vector
<Node
> qlit1
;
1903 qlit1
.insert( qlit1
.begin(), varLits
[bestVar
].begin(), varLits
[bestVar
].end() );
1904 std::vector
<Node
> qlitt
;
1905 //for all literals not containing bestVar
1906 for( size_t i
=0; i
<body
.getNumChildren(); i
++ ){
1907 if( std::find( qlit1
.begin(), qlit1
.end(), body
[i
] )==qlit1
.end() ){
1908 qlitt
.push_back( body
[i
] );
1911 //make the variable lists
1912 std::vector
<Node
> qvl1
;
1913 std::vector
<Node
> qvl2
;
1914 std::vector
<Node
> qvsh
;
1915 for( unsigned i
=0; i
<args
.size(); i
++ ){
1916 bool found1
= false;
1917 bool found2
= false;
1918 for( size_t j
=0; j
<varLits
[args
[i
]].size(); j
++ ){
1919 if( !found1
&& std::find( qlit1
.begin(), qlit1
.end(), varLits
[args
[i
]][j
] )!=qlit1
.end() ){
1921 }else if( !found2
&& std::find( qlitt
.begin(), qlitt
.end(), varLits
[args
[i
]][j
] )!=qlitt
.end() ){
1924 if( found1
&& found2
){
1930 qvsh
.push_back( args
[i
] );
1932 qvl1
.push_back( args
[i
] );
1936 qvl2
.push_back( args
[i
] );
1939 Assert(!qvl1
.empty());
1940 Assert(!qvl2
.empty() || !qvsh
.empty());
1941 //check for literals that only contain shared variables
1942 std::vector
<Node
> qlitsh
;
1943 std::vector
<Node
> qlit2
;
1944 for( size_t i
=0; i
<qlitt
.size(); i
++ ){
1945 bool hasVar2
= false;
1946 for( size_t j
=0; j
<litVars
[qlitt
[i
]].size(); j
++ ){
1947 if( std::find( qvl2
.begin(), qvl2
.end(), litVars
[qlitt
[i
]][j
] )!=qvl2
.end() ){
1953 qlit2
.push_back( qlitt
[i
] );
1955 qlitsh
.push_back( qlitt
[i
] );
1960 Trace("ag-miniscope-debug") << "Split into literals : " << qlit1
.size() << " / " << qlit2
.size() << " / " << qlitsh
.size();
1961 Trace("ag-miniscope-debug") << ", variables : " << qvl1
.size() << " / " << qvl2
.size() << " / " << qvsh
.size() << std::endl
;
1962 Node n1
= qlit1
.size()==1 ? qlit1
[0] : NodeManager::currentNM()->mkNode( OR
, qlit1
);
1963 n1
= computeAggressiveMiniscoping( qvl1
, n1
);
1964 qlitsh
.push_back( n1
);
1965 if( !qlit2
.empty() ){
1966 Node n2
= qlit2
.size()==1 ? qlit2
[0] : NodeManager::currentNM()->mkNode( OR
, qlit2
);
1967 n2
= computeAggressiveMiniscoping( qvl2
, n2
);
1968 qlitsh
.push_back( n2
);
1970 Node n
= NodeManager::currentNM()->mkNode( OR
, qlitsh
);
1971 if( !qvsh
.empty() ){
1972 Node bvl
= NodeManager::currentNM()->mkNode(kind::BOUND_VAR_LIST
, qvsh
);
1973 n
= NodeManager::currentNM()->mkNode( FORALL
, bvl
, n
);
1975 Trace("ag-miniscope") << "Return " << n
<< " for " << body
<< std::endl
;
1980 return mkForAll( args
, body
, qa
);
1983 bool QuantifiersRewriter::doOperation( Node q
, int computeOption
, QAttributes
& qa
){
1984 bool is_strict_trigger
=
1986 && options::userPatternsQuant() == options::UserPatMode::TRUST
;
1987 bool is_std
= qa
.isStandard() && !is_strict_trigger
;
1988 if (computeOption
== COMPUTE_ELIM_SYMBOLS
)
1992 else if (computeOption
== COMPUTE_MINISCOPING
)
1996 else if (computeOption
== COMPUTE_AGGRESSIVE_MINISCOPING
)
1998 return options::aggressiveMiniscopeQuant() && is_std
;
2000 else if (computeOption
== COMPUTE_PROCESS_TERMS
)
2002 return options::condRewriteQuant() || options::elimExtArithQuant()
2003 || options::iteLiftQuant() != options::IteLiftQuantMode::NONE
;
2005 else if (computeOption
== COMPUTE_COND_SPLIT
)
2007 return (options::iteDtTesterSplitQuant() || options::condVarSplitQuant())
2008 && !is_strict_trigger
;
2010 else if (computeOption
== COMPUTE_PRENEX
)
2012 return options::prenexQuant() != options::PrenexQuantMode::NONE
2013 && !options::aggressiveMiniscopeQuant() && is_std
;
2015 else if (computeOption
== COMPUTE_VAR_ELIMINATION
)
2017 return (options::varElimQuant() || options::dtVarExpandQuant()) && is_std
;
2025 //general method for computing various rewrites
2026 Node
QuantifiersRewriter::computeOperation( Node f
, int computeOption
, QAttributes
& qa
){
2027 Trace("quantifiers-rewrite-debug") << "Compute operation " << computeOption
<< " on " << f
<< " " << qa
.d_qid_num
<< std::endl
;
2028 std::vector
< Node
> args
;
2029 for( unsigned i
=0; i
<f
[0].getNumChildren(); i
++ ){
2030 args
.push_back( f
[0][i
] );
2033 if( computeOption
==COMPUTE_ELIM_SYMBOLS
){
2034 n
= computeElimSymbols( n
);
2035 }else if( computeOption
==COMPUTE_MINISCOPING
){
2036 if (options::prenexQuant() == options::PrenexQuantMode::DISJ_NORMAL
2037 || options::prenexQuant() == options::PrenexQuantMode::NORMAL
)
2039 if( !qa
.d_qid_num
.isNull() ){
2040 //already processed this, return self
2045 return computeMiniscoping( args
, n
, qa
);
2046 }else if( computeOption
==COMPUTE_AGGRESSIVE_MINISCOPING
){
2047 return computeAggressiveMiniscoping( args
, n
);
2048 }else if( computeOption
==COMPUTE_PROCESS_TERMS
){
2049 std::vector
< Node
> new_conds
;
2050 n
= computeProcessTerms( n
, args
, new_conds
, f
, qa
);
2051 if( !new_conds
.empty() ){
2052 new_conds
.push_back( n
);
2053 n
= NodeManager::currentNM()->mkNode( OR
, new_conds
);
2055 }else if( computeOption
==COMPUTE_COND_SPLIT
){
2056 n
= computeCondSplit(n
, args
, qa
);
2057 }else if( computeOption
==COMPUTE_PRENEX
){
2058 if (options::prenexQuant() == options::PrenexQuantMode::DISJ_NORMAL
2059 || options::prenexQuant() == options::PrenexQuantMode::NORMAL
)
2061 //will rewrite at preprocess time
2066 std::vector
< Node
> nargs
;
2067 n
= computePrenex( n
, args
, nargs
, true, false );
2068 Assert(nargs
.empty());
2070 }else if( computeOption
==COMPUTE_VAR_ELIMINATION
){
2071 n
= computeVarElimination( n
, args
, qa
);
2073 Trace("quantifiers-rewrite-debug") << "Compute Operation: return " << n
<< ", " << args
.size() << std::endl
;
2074 if( f
[1]==n
&& args
.size()==f
[0].getNumChildren() ){
2080 std::vector
< Node
> children
;
2081 children
.push_back( NodeManager::currentNM()->mkNode(kind::BOUND_VAR_LIST
, args
) );
2082 children
.push_back( n
);
2083 if( !qa
.d_ipl
.isNull() && args
.size()==f
[0].getNumChildren() ){
2084 children
.push_back( qa
.d_ipl
);
2086 return NodeManager::currentNM()->mkNode(kind::FORALL
, children
);
2092 Node
QuantifiersRewriter::rewriteRewriteRule( Node r
) {
2093 Kind rrkind
= r
[2].getKind();
2095 //guards, pattern, body
2097 // Replace variables by Inst_* variable and tag the terms that contain them
2098 std::vector
<Node
> vars
;
2099 vars
.reserve(r
[0].getNumChildren());
2100 for( Node::const_iterator v
= r
[0].begin(); v
!= r
[0].end(); ++v
){
2104 // Body/Remove_term/Guards/Triggers
2105 Node body
= r
[2][1];
2106 TNode new_terms
= r
[2][1];
2107 std::vector
<Node
> guards
;
2108 std::vector
<Node
> pattern
;
2109 Node true_node
= NodeManager::currentNM()->mkConst(true);
2111 TNode head
= r
[2][0];
2113 case kind::RR_REWRITE
:
2115 pattern
.push_back( head
);
2116 body
= head
.eqNode(body
);
2118 case kind::RR_REDUCTION
:
2119 case kind::RR_DEDUCTION
:
2120 // Add head to guards and pattern
2121 switch(head
.getKind()){
2123 for( unsigned i
= 0; i
<head
.getNumChildren(); i
++ ){
2124 guards
.push_back(head
[i
]);
2125 pattern
.push_back(head
[i
]);
2129 if( head
!=true_node
){
2130 guards
.push_back(head
);
2131 pattern
.push_back( head
);
2136 default: Unreachable() << "RewriteRules can be of only three kinds"; break;
2138 // Add the other guards
2140 switch(g
.getKind()){
2142 for( unsigned i
= 0; i
<g
.getNumChildren(); i
++ ){
2143 guards
.push_back(g
[i
]);
2147 if( g
!= true_node
){
2148 guards
.push_back( g
);
2152 // Add the other triggers
2153 if( r
[2].getNumChildren() >= 3 ){
2154 for( unsigned i
=0; i
<r
[2][2][0].getNumChildren(); i
++ ) {
2155 pattern
.push_back( r
[2][2][0][i
] );
2159 Trace("rr-rewrite") << "Rule is " << r
<< std::endl
;
2160 Trace("rr-rewrite") << "Head is " << head
<< std::endl
;
2161 Trace("rr-rewrite") << "Patterns are ";
2162 for( unsigned i
=0; i
<pattern
.size(); i
++ ){
2163 Trace("rr-rewrite") << pattern
[i
] << " ";
2165 Trace("rr-rewrite") << std::endl
;
2167 NodeBuilder
<> forallB(kind::FORALL
);
2169 Node gg
= guards
.size()==0 ? true_node
: ( guards
.size()==1 ? guards
[0] : NodeManager::currentNM()->mkNode( AND
, guards
) );
2170 gg
= NodeManager::currentNM()->mkNode( OR
, gg
.negate(), body
);
2171 gg
= Rewriter::rewrite( gg
);
2173 NodeBuilder
<> patternB(kind::INST_PATTERN
);
2174 patternB
.append(pattern
);
2175 NodeBuilder
<> patternListB(kind::INST_PATTERN_LIST
);
2176 //the entire rewrite rule is the first pattern
2177 if( options::quantRewriteRules() ){
2178 patternListB
<< NodeManager::currentNM()->mkNode( INST_ATTRIBUTE
, r
);
2180 patternListB
<< static_cast<Node
>(patternB
);
2181 forallB
<< static_cast<Node
>(patternListB
);
2182 Node rn
= (Node
) forallB
;
2187 bool QuantifiersRewriter::isPrenexNormalForm( Node n
) {
2188 if( n
.getKind()==FORALL
){
2189 return n
[1].getKind()!=FORALL
&& isPrenexNormalForm( n
[1] );
2190 }else if( n
.getKind()==NOT
){
2191 return n
[0].getKind()!=NOT
&& isPrenexNormalForm( n
[0] );
2193 return !expr::hasClosure(n
);
2197 Node
QuantifiersRewriter::preSkolemizeQuantifiers( Node n
, bool polarity
, std::vector
< TypeNode
>& fvTypes
, std::vector
< TNode
>& fvs
){
2198 Trace("pre-sk") << "Pre-skolem " << n
<< " " << polarity
<< " " << fvs
.size() << endl
;
2199 if( n
.getKind()==kind::NOT
){
2200 Node nn
= preSkolemizeQuantifiers( n
[0], !polarity
, fvTypes
, fvs
);
2202 }else if( n
.getKind()==kind::FORALL
){
2203 if (n
.getNumChildren() == 3)
2205 // Do not pre-skolemize quantified formulas with three children.
2206 // This includes non-standard quantified formulas
2207 // like recursive function definitions, or sygus conjectures, and
2208 // quantified formulas with triggers.
2213 if( options::preSkolemQuant() && options::preSkolemQuantNested() ){
2214 vector
< Node
> children
;
2215 children
.push_back( n
[0] );
2216 //add children to current scope
2217 std::vector
< TypeNode
> fvt
;
2218 std::vector
< TNode
> fvss
;
2219 fvt
.insert( fvt
.begin(), fvTypes
.begin(), fvTypes
.end() );
2220 fvss
.insert( fvss
.begin(), fvs
.begin(), fvs
.end() );
2221 for( int i
=0; i
<(int)n
[0].getNumChildren(); i
++ ){
2222 fvt
.push_back( n
[0][i
].getType() );
2223 fvss
.push_back( n
[0][i
] );
2226 children
.push_back( preSkolemizeQuantifiers( n
[1], polarity
, fvt
, fvss
) );
2227 //return processed quantifier
2228 return NodeManager::currentNM()->mkNode( kind::FORALL
, children
);
2232 Node nn
= preSkolemizeQuantifiers( n
[1], polarity
, fvTypes
, fvs
);
2233 std::vector
< Node
> sk
;
2235 std::vector
< unsigned > sub_vars
;
2236 //return skolemized body
2237 return Skolemize::mkSkolemizedBody(
2238 n
, nn
, fvTypes
, fvs
, sk
, sub
, sub_vars
);
2241 //check if it contains a quantifier as a subterm
2242 //if so, we will write this node
2243 if (expr::hasClosure(n
))
2245 if( ( n
.getKind()==kind::ITE
&& n
.getType().isBoolean() ) || ( n
.getKind()==kind::EQUAL
&& n
[0].getType().isBoolean() ) ){
2246 if( options::preSkolemQuantAgg() ){
2248 //must remove structure
2249 if( n
.getKind()==kind::ITE
){
2250 nn
= NodeManager::currentNM()->mkNode( kind::AND
,
2251 NodeManager::currentNM()->mkNode( kind::OR
, n
[0].notNode(), n
[1] ),
2252 NodeManager::currentNM()->mkNode( kind::OR
, n
[0], n
[2] ) );
2253 }else if( n
.getKind()==kind::EQUAL
){
2254 nn
= NodeManager::currentNM()->mkNode( kind::AND
,
2255 NodeManager::currentNM()->mkNode( kind::OR
, n
[0].notNode(), n
.getKind()==kind::XOR
? n
[1].notNode() : n
[1] ),
2256 NodeManager::currentNM()->mkNode( kind::OR
, n
[0], n
.getKind()==kind::XOR
? n
[1] : n
[1].notNode() ) );
2258 return preSkolemizeQuantifiers( nn
, polarity
, fvTypes
, fvs
);
2260 }else if( n
.getKind()==kind::AND
|| n
.getKind()==kind::OR
){
2261 vector
< Node
> children
;
2262 for( int i
=0; i
<(int)n
.getNumChildren(); i
++ ){
2263 children
.push_back( preSkolemizeQuantifiers( n
[i
], polarity
, fvTypes
, fvs
) );
2265 return NodeManager::currentNM()->mkNode( n
.getKind(), children
);
2273 Node
QuantifiersRewriter::preprocess( Node n
, bool isInst
) {
2275 if( n
.getKind() == kind::REWRITE_RULE
){
2276 n
= quantifiers::QuantifiersRewriter::rewriteRewriteRule( n
);
2278 if( options::preSkolemQuant() ){
2279 if( !isInst
|| !options::preSkolemQuantNested() ){
2280 Trace("quantifiers-preprocess-debug") << "Pre-skolemize " << n
<< "..." << std::endl
;
2281 //apply pre-skolemization to existential quantifiers
2282 std::vector
< TypeNode
> fvTypes
;
2283 std::vector
< TNode
> fvs
;
2284 n
= quantifiers::QuantifiersRewriter::preSkolemizeQuantifiers( prev
, true, fvTypes
, fvs
);
2288 //pull all quantifiers globally
2289 if (options::prenexQuant() == options::PrenexQuantMode::DISJ_NORMAL
2290 || options::prenexQuant() == options::PrenexQuantMode::NORMAL
)
2292 Trace("quantifiers-prenex") << "Prenexing : " << n
<< std::endl
;
2293 std::map
< unsigned, std::map
< Node
, Node
> > visited
;
2294 n
= quantifiers::QuantifiersRewriter::computePrenexAgg( n
, true, visited
);
2295 n
= Rewriter::rewrite( n
);
2296 Trace("quantifiers-prenex") << "Prenexing returned : " << n
<< std::endl
;
2297 //Assert( isPrenexNormalForm( n ) );
2300 Trace("quantifiers-preprocess") << "Preprocess " << prev
<< std::endl
;
2301 Trace("quantifiers-preprocess") << "..returned " << n
<< std::endl
;
2306 }/* CVC4::theory::quantifiers namespace */
2307 }/* CVC4::theory namespace */
2308 }/* CVC4 namespace */