1 /********************* */
2 /*! \file inst_strategy_cbqi.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-2016 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 counterexample-guided quantifier instantiation strategies
14 #include "theory/quantifiers/inst_strategy_cbqi.h"
16 #include "options/quantifiers_options.h"
17 #include "smt/ite_removal.h"
18 #include "theory/arith/partial_model.h"
19 #include "theory/arith/theory_arith.h"
20 #include "theory/arith/theory_arith_private.h"
21 #include "theory/quantifiers/first_order_model.h"
22 #include "theory/quantifiers/term_database.h"
23 #include "theory/quantifiers/trigger.h"
24 #include "theory/theory_engine.h"
28 using namespace CVC4::kind
;
29 using namespace CVC4::context
;
30 using namespace CVC4::theory
;
31 using namespace CVC4::theory::quantifiers
;
32 using namespace CVC4::theory::arith
;
34 #define ARITH_INSTANTIATOR_USE_MINUS_DELTA
36 InstStrategyCbqi::InstStrategyCbqi( QuantifiersEngine
* qe
)
37 : QuantifiersModule( qe
), d_added_cbqi_lemma( qe
->getUserContext() )
38 //, d_added_inst( qe->getUserContext() )
42 InstStrategyCbqi::~InstStrategyCbqi() throw(){}
44 bool InstStrategyCbqi::needsCheck( Theory::Effort e
) {
45 return e
>=Theory::EFFORT_LAST_CALL
;
48 unsigned InstStrategyCbqi::needsModel( Theory::Effort e
) {
49 for( unsigned i
=0; i
<d_quantEngine
->getModel()->getNumAssertedQuantifiers(); i
++ ){
50 Node q
= d_quantEngine
->getModel()->getAssertedQuantifier( i
);
51 if( doCbqi( q
) && d_quantEngine
->getModel()->isQuantifierActive( q
) ){
52 return QuantifiersEngine::QEFFORT_STANDARD
;
55 return QuantifiersEngine::QEFFORT_NONE
;
58 void InstStrategyCbqi::reset_round( Theory::Effort effort
) {
59 d_cbqi_set_quant_inactive
= false;
60 d_incomplete_check
= false;
61 //check if any cbqi lemma has not been added yet
62 for( unsigned i
=0; i
<d_quantEngine
->getModel()->getNumAssertedQuantifiers(); i
++ ){
63 Node q
= d_quantEngine
->getModel()->getAssertedQuantifier( i
);
64 //it is not active if it corresponds to a rewrite rule: we will process in rewrite engine
66 if( !hasAddedCbqiLemma( q
) ){
67 d_added_cbqi_lemma
.insert( q
);
68 Trace("cbqi") << "Do cbqi for " << q
<< std::endl
;
70 //get the counterexample literal
71 Node ceLit
= d_quantEngine
->getTermDatabase()->getCounterexampleLiteral( q
);
72 Node ceBody
= d_quantEngine
->getTermDatabase()->getInstConstantBody( q
);
73 if( !ceBody
.isNull() ){
74 //add counterexample lemma
75 Node lem
= NodeManager::currentNM()->mkNode( OR
, ceLit
.negate(), ceBody
.negate() );
76 //require any decision on cel to be phase=true
77 d_quantEngine
->addRequirePhase( ceLit
, true );
78 Debug("cbqi-debug") << "Require phase " << ceLit
<< " = true." << std::endl
;
79 //add counterexample lemma
80 lem
= Rewriter::rewrite( lem
);
81 Trace("cbqi") << "Counterexample lemma : " << lem
<< std::endl
;
82 registerCounterexampleLemma( q
, lem
);
84 //set inactive the quantified formulas whose CE literals are asserted false
85 }else if( d_quantEngine
->getModel()->isQuantifierActive( q
) ){
86 Debug("cbqi-debug") << "Check quantified formula " << q
<< "..." << std::endl
;
87 Node cel
= d_quantEngine
->getTermDatabase()->getCounterexampleLiteral( q
);
89 if( d_quantEngine
->getValuation().hasSatValue( cel
, value
) ){
90 Debug("cbqi-debug") << "...CE Literal has value " << value
<< std::endl
;
92 if( d_quantEngine
->getValuation().isDecision( cel
) ){
93 Trace("cbqi-warn") << "CBQI WARNING: Bad decision on CE Literal." << std::endl
;
95 d_quantEngine
->getModel()->setQuantifierActive( q
, false );
96 d_cbqi_set_quant_inactive
= true;
100 Debug("cbqi-debug") << "...CE Literal does not have value " << std::endl
;
105 processResetInstantiationRound( effort
);
108 void InstStrategyCbqi::check( Theory::Effort e
, unsigned quant_e
) {
109 if( quant_e
==QuantifiersEngine::QEFFORT_STANDARD
){
110 Assert( !d_quantEngine
->inConflict() );
112 if( Trace
.isOn("cbqi-engine") ){
113 clSet
= double(clock())/double(CLOCKS_PER_SEC
);
114 Trace("cbqi-engine") << "---Cbqi Engine Round, effort = " << e
<< "---" << std::endl
;
116 unsigned lastWaiting
= d_quantEngine
->getNumLemmasWaiting();
117 for( int ee
=0; ee
<=1; ee
++ ){
118 for( unsigned i
=0; i
<d_quantEngine
->getModel()->getNumAssertedQuantifiers(); i
++ ){
119 Node q
= d_quantEngine
->getModel()->getAssertedQuantifier( i
);
120 if( doCbqi( q
) && d_quantEngine
->getModel()->isQuantifierActive( q
) ){
122 if( d_quantEngine
->inConflict() ){
127 if( d_quantEngine
->inConflict() || d_quantEngine
->getNumLemmasWaiting()>lastWaiting
){
131 if( Trace
.isOn("cbqi-engine") ){
132 if( d_quantEngine
->getNumLemmasWaiting()>lastWaiting
){
133 Trace("cbqi-engine") << "Added lemmas = " << (d_quantEngine
->getNumLemmasWaiting()-lastWaiting
) << std::endl
;
135 double clSet2
= double(clock())/double(CLOCKS_PER_SEC
);
136 Trace("cbqi-engine") << "Finished cbqi engine, time = " << (clSet2
-clSet
) << std::endl
;
141 bool InstStrategyCbqi::checkComplete() {
142 if( ( !options::cbqiSat() && d_cbqi_set_quant_inactive
) || d_incomplete_check
){
149 void InstStrategyCbqi::preRegisterQuantifier( Node q
) {
150 if( d_quantEngine
->getOwner( q
)==NULL
&& doCbqi( q
) ){
151 if( !options::cbqiAll() && !options::cbqiSplx() ){
152 //take full ownership of the quantified formula
153 d_quantEngine
->setOwner( q
, this );
158 void InstStrategyCbqi::registerQuantifier( Node q
) {
162 void InstStrategyCbqi::registerCounterexampleLemma( Node q
, Node lem
){
163 Trace("cbqi-debug") << "Counterexample lemma : " << lem
<< std::endl
;
164 d_quantEngine
->addLemma( lem
, false );
167 bool InstStrategyCbqi::hasNonCbqiOperator( Node n
, std::map
< Node
, bool >& visited
){
168 if( visited
.find( n
)==visited
.end() ){
170 if( n
.getKind()!=BOUND_VARIABLE
&& TermDb::hasBoundVarAttr( n
) ){
171 if( !inst::Trigger::isCbqiKind( n
.getKind() ) ){
172 Trace("cbqi-debug2") << "Non-cbqi kind : " << n
.getKind() << " in " << n
<< std::endl
;
174 }else if( n
.getKind()==MULT
&& ( n
.getNumChildren()!=2 || !n
[0].isConst() ) ){
175 Trace("cbqi-debug2") << "Non-linear arithmetic : " << n
<< std::endl
;
177 }else if( n
.getKind()==FORALL
){
178 return hasNonCbqiOperator( n
[1], visited
);
180 for( unsigned i
=0; i
<n
.getNumChildren(); i
++ ){
181 if( hasNonCbqiOperator( n
[i
], visited
) ){
190 bool InstStrategyCbqi::hasNonCbqiVariable( Node q
){
191 for( unsigned i
=0; i
<q
[0].getNumChildren(); i
++ ){
192 TypeNode tn
= q
[0][i
].getType();
193 if( !tn
.isInteger() && !tn
.isReal() && !tn
.isBoolean() ){
194 if( options::cbqiSplx() ){
197 //datatypes supported in new implementation
198 if( !tn
.isDatatype() ){
207 bool InstStrategyCbqi::doCbqi( Node q
){
208 std::map
< Node
, bool >::iterator it
= d_do_cbqi
.find( q
);
209 if( it
==d_do_cbqi
.end() ){
211 if( d_quantEngine
->getTermDatabase()->isQAttrQuantElim( q
) ){
214 //if has an instantiation pattern, don't do it
215 if( q
.getNumChildren()==3 && options::eMatching() && options::userPatternsQuant()!=USER_PAT_MODE_IGNORE
){
218 if( options::cbqiAll() ){
221 //if quantifier has a non-arithmetic variable, then do not use cbqi
222 //if quantifier has an APPLY_UF term, then do not use cbqi
223 //Node cb = d_quantEngine->getTermDatabase()->getInstConstantBody( q );
224 std::map
< Node
, bool > visited
;
225 ret
= !hasNonCbqiVariable( q
) && !hasNonCbqiOperator( q
[1], visited
);
229 Trace("cbqi") << "doCbqi " << q
<< " returned " << ret
<< std::endl
;
237 Node
InstStrategyCbqi::getNextDecisionRequest(){
238 // all counterexample literals that are not asserted
239 for( unsigned i
=0; i
<d_quantEngine
->getModel()->getNumAssertedQuantifiers(); i
++ ){
240 Node q
= d_quantEngine
->getModel()->getAssertedQuantifier( i
);
241 if( hasAddedCbqiLemma( q
) ){
242 Node cel
= d_quantEngine
->getTermDatabase()->getCounterexampleLiteral( q
);
244 if( !d_quantEngine
->getValuation().hasSatValue( cel
, value
) ){
245 Trace("cbqi-debug2") << "CBQI: get next decision " << cel
<< std::endl
;
258 InstStrategySimplex::InstStrategySimplex( TheoryArith
* th
, QuantifiersEngine
* ie
) : InstStrategyCbqi( ie
), d_th( th
), d_counter( 0 ){
259 d_negOne
= NodeManager::currentNM()->mkConst( Rational(-1) );
260 d_zero
= NodeManager::currentNM()->mkConst( Rational(0) );
263 void getInstantiationConstants( Node n
, std::vector
< Node
>& ics
){
264 if( n
.getKind()==INST_CONSTANT
){
265 if( std::find( ics
.begin(), ics
.end(), n
)==ics
.end() ){
269 for( unsigned i
=0; i
<n
.getNumChildren(); i
++ ){
270 getInstantiationConstants( n
[i
], ics
);
276 void InstStrategySimplex::processResetInstantiationRound( Theory::Effort effort
){
277 Debug("quant-arith") << "Setting up simplex for instantiator... " << std::endl
;
278 d_quantActive
.clear();
280 d_tableaux_term
.clear();
282 d_ceTableaux
.clear();
283 //search for instantiation rows in simplex tableaux
284 ArithVariables
& avnm
= d_th
->d_internal
->d_partialModel
;
285 ArithVariables::var_iterator vi
, vend
;
286 for(vi
= avnm
.var_begin(), vend
= avnm
.var_end(); vi
!= vend
; ++vi
){
288 Node n
= avnm
.asNode(x
);
290 //collect instantiation constants
291 std::vector
< Node
> ics
;
292 getInstantiationConstants( n
, ics
);
293 for( unsigned i
=0; i
<ics
.size(); i
++ ){
294 NodeBuilder
<> t(kind::PLUS
);
295 if( n
.getKind()==PLUS
){
296 for( int j
=0; j
<(int)n
.getNumChildren(); j
++ ){
297 addTermToRow( ics
[i
], x
, n
[j
], t
);
300 addTermToRow( ics
[i
], x
, n
, t
);
302 d_instRows
[ics
[i
]].push_back( x
);
303 //this theory has constraints from f
304 Node f
= TermDb::getInstConstAttr(ics
[i
]);
305 Debug("quant-arith") << "Has constraints from " << f
<< std::endl
;
306 //set that we should process it
307 d_quantActive
[ f
] = true;
309 if( t
.getNumChildren()==0 ){
310 d_tableaux_term
[ics
[i
]][x
] = d_zero
;
311 }else if( t
.getNumChildren()==1 ){
312 d_tableaux_term
[ics
[i
]][x
] = t
.getChild( 0 );
314 d_tableaux_term
[ics
[i
]][x
] = t
;
319 if( Debug
.isOn("quant-arith-debug") ){
320 Debug("quant-arith-debug") << std::endl
;
321 debugPrint( "quant-arith-debug" );
326 void InstStrategySimplex::addTermToRow( Node i
, ArithVar x
, Node n
, NodeBuilder
<>& t
){
327 if( n
.getKind()==MULT
){
328 if( TermDb::hasInstConstAttr(n
[1]) && n
[0].getKind()==CONST_RATIONAL
){
330 d_ceTableaux
[i
][x
][ n
[1] ] = n
[0];
332 d_tableaux_ce_term
[i
][x
][ n
[1] ] = n
[0];
335 d_tableaux
[i
][x
][ n
[1] ] = n
[0];
339 if( TermDb::hasInstConstAttr(n
) ){
341 d_ceTableaux
[i
][x
][ n
] = Node::null();
343 d_tableaux_ce_term
[i
][x
][ n
] = NodeManager::currentNM()->mkConst( Rational(1) );
346 d_tableaux
[i
][x
][ n
] = NodeManager::currentNM()->mkConst( Rational(1) );
352 void InstStrategySimplex::process( Node f
, Theory::Effort effort
, int e
){
354 if( d_quantActive
.find( f
)!=d_quantActive
.end() ){
355 //the point instantiation
356 InstMatch
m_point( f
);
357 bool m_point_valid
= true;
359 //scan over all instantiation rows
360 for( unsigned i
=0; i
<d_quantEngine
->getTermDatabase()->getNumInstantiationConstants( f
); i
++ ){
361 Node ic
= d_quantEngine
->getTermDatabase()->getInstantiationConstant( f
, i
);
362 Debug("quant-arith-simplex") << "InstStrategySimplex check " << ic
<< ", rows = " << d_instRows
[ic
].size() << std::endl
;
363 for( unsigned j
=0; j
<d_instRows
[ic
].size(); j
++ ){
364 ArithVar x
= d_instRows
[ic
][j
];
365 if( !d_ceTableaux
[ic
][x
].empty() ){
366 if( Debug
.isOn("quant-arith-simplex") ){
367 Debug("quant-arith-simplex") << "--- Check row " << ic
<< " " << x
<< std::endl
;
368 Debug("quant-arith-simplex") << " ";
369 for( std::map
< Node
, Node
>::iterator it
= d_ceTableaux
[ic
][x
].begin(); it
!= d_ceTableaux
[ic
][x
].end(); ++it
){
370 if( it
!=d_ceTableaux
[ic
][x
].begin() ){ Debug("quant-arith-simplex") << " + "; }
371 Debug("quant-arith-simplex") << it
->first
<< " * " << it
->second
;
373 Debug("quant-arith-simplex") << " = ";
374 Node v
= getTableauxValue( x
, false );
375 Debug("quant-arith-simplex") << v
<< std::endl
;
376 Debug("quant-arith-simplex") << " term : " << d_tableaux_term
[ic
][x
] << std::endl
;
377 Debug("quant-arith-simplex") << " ce-term : ";
378 for( std::map
< Node
, Node
>::iterator it
= d_tableaux_ce_term
[ic
][x
].begin(); it
!= d_tableaux_ce_term
[ic
][x
].end(); it
++ ){
379 if( it
!=d_tableaux_ce_term
[ic
][x
].begin() ){ Debug("quant-arith-simplex") << " + "; }
380 Debug("quant-arith-simplex") << it
->first
<< " * " << it
->second
;
382 Debug("quant-arith-simplex") << std::endl
;
384 //instantiation row will be A*e + B*t = beta,
385 // where e is a vector of terms , and t is vector of ground terms.
386 // Say one term in A*e is coeff*e_i, where e_i is an instantiation constant
387 // We will construct the term ( beta - B*t)/coeff to use for e_i.
389 for( unsigned k
=0; k
<f
[0].getNumChildren(); k
++ ){
390 if( f
[0][k
].getType().isInteger() ){
391 m
.setValue( k
, d_zero
);
394 //By default, choose the first instantiation constant to be e_i.
395 Node var
= d_ceTableaux
[ic
][x
].begin()->first
;
396 //if it is integer, we need to find variable with coefficent +/- 1
397 if( var
.getType().isInteger() ){
398 std::map
< Node
, Node
>::iterator it
= d_ceTableaux
[ic
][x
].begin();
399 while( !var
.isNull() && !d_ceTableaux
[ic
][x
][var
].isNull() && d_ceTableaux
[ic
][x
][var
]!=d_negOne
){
401 if( it
==d_ceTableaux
[ic
][x
].end() ){
407 //Otherwise, try one that divides all ground term coefficients?
408 // Might be futile, if rewrite ensures gcd of coeffs is 1.
411 //add to point instantiation if applicable
412 if( d_tableaux_ce_term
[ic
][x
].empty() && d_tableaux_term
[ic
][x
]==d_zero
){
413 Debug("quant-arith-simplex") << "*** Row contributes to point instantiation." << std::endl
;
414 Node v
= getTableauxValue( x
, false );
415 if( !var
.getType().isInteger() || v
.getType().isInteger() ){
416 m_point
.setValue( i
, v
);
418 m_point_valid
= false;
421 Debug("quant-arith-simplex") << "Instantiate with var " << var
<< std::endl
;
422 if( doInstantiation( f
, ic
, d_tableaux_term
[ic
][x
], x
, m
, var
) ){
426 Debug("quant-arith-simplex") << "Could not find var." << std::endl
;
431 if( lem
==0 && m_point_valid
){
432 if( d_quantEngine
->addInstantiation( f
, m_point
) ){
433 Debug("quant-arith-simplex") << "...added point instantiation." << std::endl
;
441 void InstStrategySimplex::debugPrint( const char* c
){
442 ArithVariables
& avnm
= d_th
->d_internal
->d_partialModel
;
443 ArithVariables::var_iterator vi
, vend
;
444 for(vi
= avnm
.var_begin(), vend
= avnm
.var_end(); vi
!= vend
; ++vi
){
446 Node n
= avnm
.asNode(x
);
447 //if( ((TheoryArith*)getTheory())->d_partialModel.hasEitherBound( x ) ){
448 Debug(c
) << x
<< " : " << n
<< ", bounds = ";
449 if( d_th
->d_internal
->d_partialModel
.hasLowerBound( x
) ){
450 Debug(c
) << d_th
->d_internal
->d_partialModel
.getLowerBound( x
);
452 Debug(c
) << "-infty";
455 Debug(c
) << d_th
->d_internal
->d_partialModel
.getAssignment( x
);
457 if( d_th
->d_internal
->d_partialModel
.hasUpperBound( x
) ){
458 Debug(c
) << d_th
->d_internal
->d_partialModel
.getUpperBound( x
);
460 Debug(c
) << "+infty";
462 Debug(c
) << std::endl
;
463 //Debug(c) << " Term = " << d_tableaux_term[x] << std::endl;
465 //for( std::map< Node, Node >::iterator it2 = d_tableaux[x].begin(); it2 != d_tableaux[x].end(); ++it2 ){
466 // Debug(c) << "( " << it2->first << ", " << it2->second << " ) ";
468 //for( std::map< Node, Node >::iterator it2 = d_ceTableaux[x].begin(); it2 != d_ceTableaux[x].end(); ++it2 ){
469 // Debug(c) << "(CE)( " << it2->first << ", " << it2->second << " ) ";
471 //for( std::map< Node, Node >::iterator it2 = d_tableaux_ce_term[x].begin(); it2 != d_tableaux_ce_term[x].end(); ++it2 ){
472 // Debug(c) << "(CE-term)( " << it2->first << ", " << it2->second << " ) ";
474 //Debug(c) << std::endl;
477 Debug(c
) << std::endl
;
479 for( unsigned i
=0; i
<d_quantEngine
->getModel()->getNumAssertedQuantifiers(); i
++ ){
480 Node f
= d_quantEngine
->getModel()->getAssertedQuantifier( i
);
481 Debug(c
) << f
<< std::endl
;
482 Debug(c
) << " Inst constants: ";
483 for( unsigned j
=0; j
<d_quantEngine
->getTermDatabase()->getNumInstantiationConstants( f
); i
++ ){
487 Debug( c
) << d_quantEngine
->getTermDatabase()->getInstantiationConstant( f
, i
);
489 Debug(c
) << std::endl
;
490 for( unsigned j
=0; j
<d_quantEngine
->getTermDatabase()->getNumInstantiationConstants( f
); j
++ ){
491 Node ic
= d_quantEngine
->getTermDatabase()->getInstantiationConstant( f
, j
);
492 Debug(c
) << " Instantiation rows for " << ic
<< " : ";
493 for( unsigned k
=0; k
<d_instRows
[ic
].size(); k
++ ){
497 Debug(c
) << d_instRows
[ic
][k
];
499 Debug(c
) << std::endl
;
504 //say instantiation row x for quantifier f is coeff*var + A*t[e] + term = beta,
505 // where var is an instantiation constant from f,
506 // t[e] is a vector of terms containing instantiation constants from f,
507 // and term is a ground term (c1*t1 + ... + cn*tn).
508 // We construct the term ( beta - term )/coeff to use as an instantiation for var.
509 bool InstStrategySimplex::doInstantiation( Node f
, Node ic
, Node term
, ArithVar x
, InstMatch
& m
, Node var
){
511 if( doInstantiation2( f
, ic
, term
, x
, m
, var
) ){
512 ++(d_quantEngine
->d_statistics
.d_instantiations_cbqi_arith
);
515 #ifdef ARITH_INSTANTIATOR_USE_MINUS_DELTA
516 //otherwise try -delta
517 if( doInstantiation2( f
, ic
, term
, x
, m
, var
, true ) ){
518 ++(d_quantEngine
->d_statistics
.d_instantiations_cbqi_arith
);
529 bool InstStrategySimplex::doInstantiation2( Node f
, Node ic
, Node term
, ArithVar x
, InstMatch
& m
, Node var
, bool minus_delta
){
530 // make term ( beta - term )/coeff
531 bool vIsInteger
= var
.getType().isInteger();
532 Node beta
= getTableauxValue( x
, minus_delta
);
533 if( !vIsInteger
|| beta
.getType().isInteger() ){
534 Node instVal
= NodeManager::currentNM()->mkNode( MINUS
, beta
, term
);
535 if( !d_ceTableaux
[ic
][x
][var
].isNull() ){
537 Assert( d_ceTableaux
[ic
][x
][var
]==NodeManager::currentNM()->mkConst( Rational(-1) ) );
538 instVal
= NodeManager::currentNM()->mkNode( MULT
, d_ceTableaux
[ic
][x
][var
], instVal
);
540 Assert( d_ceTableaux
[ic
][x
][var
].getKind()==CONST_RATIONAL
);
541 Node coeff
= NodeManager::currentNM()->mkConst( Rational(1) / d_ceTableaux
[ic
][x
][var
].getConst
<Rational
>() );
542 instVal
= NodeManager::currentNM()->mkNode( MULT
, coeff
, instVal
);
545 instVal
= Rewriter::rewrite( instVal
);
546 //use as instantiation value for var
547 int vn
= var
.getAttribute(InstVarNumAttribute());
548 m
.setValue( vn
, instVal
);
549 Debug("quant-arith") << "Add instantiation " << m
<< std::endl
;
550 return d_quantEngine
->addInstantiation( f
, m
);
556 Node InstStrategySimplex::getTableauxValue( Node n, bool minus_delta ){
557 if( d_th->d_internal->d_partialModel.hasArithVar(n) ){
558 ArithVar v = d_th->d_internal->d_partialModel.asArithVar( n );
559 return getTableauxValue( v, minus_delta );
561 return NodeManager::currentNM()->mkConst( Rational(0) );
565 Node
InstStrategySimplex::getTableauxValue( ArithVar v
, bool minus_delta
){
566 const Rational
& delta
= d_th
->d_internal
->d_partialModel
.getDelta();
567 DeltaRational drv
= d_th
->d_internal
->d_partialModel
.getAssignment( v
);
568 Rational qmodel
= drv
.substituteDelta( minus_delta
? -delta
: delta
);
569 return mkRationalNode(qmodel
);
576 bool CegqiOutputInstStrategy::doAddInstantiation( std::vector
< Node
>& subs
) {
577 return d_out
->doAddInstantiation( subs
);
580 bool CegqiOutputInstStrategy::isEligibleForInstantiation( Node n
) {
581 return d_out
->isEligibleForInstantiation( n
);
584 bool CegqiOutputInstStrategy::addLemma( Node lem
) {
585 return d_out
->addLemma( lem
);
589 InstStrategyCegqi::InstStrategyCegqi( QuantifiersEngine
* qe
)
590 : InstStrategyCbqi( qe
) {
591 d_out
= new CegqiOutputInstStrategy( this );
592 d_small_const
= NodeManager::currentNM()->mkConst( Rational(1)/Rational(1000000) );
595 InstStrategyCegqi::~InstStrategyCegqi() throw () {
598 for(std::map
< Node
, CegInstantiator
* >::iterator i
= d_cinst
.begin(),
599 iend
= d_cinst
.end(); i
!= iend
; ++i
) {
600 CegInstantiator
* instantiator
= (*i
).second
;
606 void InstStrategyCegqi::processResetInstantiationRound( Theory::Effort effort
) {
607 d_check_vts_lemma_lc
= false;
610 void InstStrategyCegqi::process( Node q
, Theory::Effort effort
, int e
) {
612 CegInstantiator
* cinst
= getInstantiator( q
);
613 Trace("inst-alg") << "-> Run cegqi for " << q
<< std::endl
;
615 if( !cinst
->check() ){
616 d_incomplete_check
= true;
617 d_check_vts_lemma_lc
= true;
619 d_curr_quant
= Node::null();
621 //minimize the free delta heuristically on demand
622 if( d_check_vts_lemma_lc
){
623 Trace("inst-alg") << "-> Minimize delta heuristic, for " << q
<< std::endl
;
624 d_check_vts_lemma_lc
= false;
625 d_small_const
= NodeManager::currentNM()->mkNode( MULT
, d_small_const
, d_small_const
);
626 d_small_const
= Rewriter::rewrite( d_small_const
);
627 //heuristic for now, until we know how to do nested quantification
628 Node delta
= d_quantEngine
->getTermDatabase()->getVtsDelta( true, false );
629 if( !delta
.isNull() ){
630 Trace("quant-vts-debug") << "Delta lemma for " << d_small_const
<< std::endl
;
631 Node delta_lem_ub
= NodeManager::currentNM()->mkNode( LT
, delta
, d_small_const
);
632 d_quantEngine
->getOutputChannel().lemma( delta_lem_ub
);
634 std::vector
< Node
> inf
;
635 d_quantEngine
->getTermDatabase()->getVtsTerms( inf
, true, false, false );
636 for( unsigned i
=0; i
<inf
.size(); i
++ ){
637 Trace("quant-vts-debug") << "Infinity lemma for " << inf
[i
] << " " << d_small_const
<< std::endl
;
638 Node inf_lem_lb
= NodeManager::currentNM()->mkNode( GT
, inf
[i
], NodeManager::currentNM()->mkConst( Rational(1)/d_small_const
.getConst
<Rational
>() ) );
639 d_quantEngine
->getOutputChannel().lemma( inf_lem_lb
);
645 bool InstStrategyCegqi::doAddInstantiation( std::vector
< Node
>& subs
) {
646 Assert( !d_curr_quant
.isNull() );
647 //if doing partial quantifier elimination, record the instantiation and set the incomplete flag instead of sending instantiation lemma
648 if( d_quantEngine
->getTermDatabase()->isQAttrQuantElimPartial( d_curr_quant
) ){
649 d_cbqi_set_quant_inactive
= true;
650 d_incomplete_check
= true;
651 d_quantEngine
->recordInstantiationInternal( d_curr_quant
, subs
, false, false );
654 //check if we need virtual term substitution (if used delta or infinity)
655 bool used_vts
= d_quantEngine
->getTermDatabase()->containsVtsTerm( subs
, false );
656 if( d_quantEngine
->addInstantiation( d_curr_quant
, subs
, false, false, used_vts
) ){
657 //d_added_inst.insert( d_curr_quant );
665 bool InstStrategyCegqi::addLemma( Node lem
) {
666 return d_quantEngine
->addLemma( lem
);
669 bool InstStrategyCegqi::isEligibleForInstantiation( Node n
) {
670 if( n
.getKind()==INST_CONSTANT
|| n
.getKind()==SKOLEM
){
671 if( n
.getKind()==SKOLEM
&& d_quantEngine
->getTermDatabase()->containsVtsTerm( n
) ){
674 //only legal if current quantified formula contains n
675 return TermDb::containsTerm( d_curr_quant
, n
);
682 CegInstantiator
* InstStrategyCegqi::getInstantiator( Node q
) {
683 std::map
< Node
, CegInstantiator
* >::iterator it
= d_cinst
.find( q
);
684 if( it
==d_cinst
.end() ){
685 CegInstantiator
* cinst
= new CegInstantiator( d_quantEngine
, d_out
, true, true );
693 void InstStrategyCegqi::registerQuantifier( Node q
) {
694 if( options::cbqiPreRegInst() ){
695 //just get the instantiator
696 getInstantiator( q
);
700 void InstStrategyCegqi::registerCounterexampleLemma( Node q
, Node lem
) {
701 //must register with the instantiator
702 //must explicitly remove ITEs so that we record dependencies
703 std::vector
< Node
> ce_vars
;
704 for( unsigned i
=0; i
<d_quantEngine
->getTermDatabase()->getNumInstantiationConstants( q
); i
++ ){
705 ce_vars
.push_back( d_quantEngine
->getTermDatabase()->getInstantiationConstant( q
, i
) );
707 std::vector
< Node
> lems
;
708 lems
.push_back( lem
);
709 CegInstantiator
* cinst
= getInstantiator( q
);
710 cinst
->registerCounterexampleLemma( lems
, ce_vars
);
711 for( unsigned i
=0; i
<lems
.size(); i
++ ){
712 Trace("cbqi-debug") << "Counterexample lemma " << i
<< " : " << lems
[i
] << std::endl
;
713 d_quantEngine
->addLemma( lems
[i
], false );
717 void InstStrategyCegqi::presolve() {
718 if( options::cbqiPreRegInst() ){
719 for( std::map
< Node
, CegInstantiator
* >::iterator it
= d_cinst
.begin(); it
!= d_cinst
.end(); ++it
){
720 it
->second
->presolve( it
->first
);