Lines Matching refs:d_th
1324 d_th(th), in StrongSolverTheoryUF()
1352 return d_th->getQuantifiersEngine()->getTheoryEngine()->getSortInference(); in getSortInference()
1357 return d_th->getSatContext(); in getSatContext()
1362 return d_th->getOutputChannel(); in getOutputChannel()
1469 if( d_th->getQuantifiersEngine() ){ in assertNode()
1549 a = d_th->d_equalityEngine.getRepresentative( a ); in areDisequal()
1550 b = d_th->d_equalityEngine.getRepresentative( b ); in areDisequal()
1551 if( d_th->d_equalityEngine.areDisequal( a, b, false ) ){ in areDisequal()
1584 eq::EqClassesIterator eqcs_i(d_th->getEqualityEngine()); in check()
1594 if( !d_th->getEqualityEngine()->areDisequal( a, b, false ) ){ in check()
1659 rm = new SortModel( n, d_th->getSatContext(), d_th->getUserContext(), this ); in preRegisterTerm()
1768 d_th->getDecisionManager()->registerStrategy( in initializeCombinedCardinality()