Searched refs:qepr (Results 1 – 3 of 3) sorted by relevance
109 QuantEPR * qepr = d_quantEngine->getQuantEPR(); in registerCbqiLemma() local110 if( qepr!=NULL ){ in registerCbqiLemma()114 if( qepr->isEPR( tn ) ){ in registerCbqiLemma()116 std::map< TypeNode, std::vector< Node > >::iterator itc = qepr->d_consts.find( tn ); in registerCbqiLemma()117 if( itc!=qepr->d_consts.end() ){ in registerCbqiLemma()660 QuantEPR * qepr = d_quantEngine->getQuantEPR(); in isEligibleForInstantiation() local661 if( qepr!=NULL ){ in isEligibleForInstantiation()663 if( qepr->isEPRConstant( tn, n ) ){ in isEligibleForInstantiation()
263 QuantEPR* qepr = qe != nullptr ? qe->getQuantEPR() : nullptr; in isCbqiSort() local264 if (qepr != nullptr) in isCbqiSort()266 if (qepr->isEPR(tn)) in isCbqiSort()
1075 quantifiers::QuantEPR* qepr = getLogicInfo().isQuantified() in initializeBounds() local1081 if( qepr && qepr->isEPR( tn ) ){ in initializeBounds()1082 for( unsigned j=0; j<qepr->d_consts[tn].size(); j++ ){ in initializeBounds()1083 Node k = qepr->d_consts[tn][j]; in initializeBounds()1108 if( qepr && qepr->isEPR( tn ) ){ in initializeBounds()1109 qepr->addEPRConstant( tn, e ); in initializeBounds()1113 if( qepr && qepr->isEPR( tn ) ){ in initializeBounds()1115 if( !qepr->isEPRConstant( tn, nr ) ){ in initializeBounds()1116 qepr->addEPRConstant( tn, nr ); in initializeBounds()