Home
last modified time | relevance | path

Searched refs:isTermActive (Results 1 – 5 of 5) sorted by relevance

/dports/math/cvc4/CVC4-1.7/src/theory/quantifiers/
H A Dterm_database.h248 bool isTermActive(Node n);
H A Dterm_database.cpp271 if (hasTermCurrent(n) && isTermActive(n)) in computeUfEqcTerms()
322 if (!isTermActive(n)) in computeUfTerms()
753 bool TermDb::isTermActive( Node n ) { in isTermActive() function in CVC4::theory::quantifiers::TermDb
H A Drelevant_domain.cpp128 if( db->isTermActive( n ) ){ in compute()
H A Dconjecture_generator.cpp313 …return d_quantEngine->getTermDatabase()->isTermActive( n ) && inst::Trigger::isAtomicTrigger( n ) … in isHandledTerm()
461 …if( getTermDatabase()->hasTermCurrent( n ) && getTermDatabase()->isTermActive( n ) && ( n.getKind(… in check()
/dports/math/cvc4/CVC4-1.7/src/theory/quantifiers/ematching/
H A Dcandidate_generator.cpp33 …return d_qe->getTermDatabase()->isTermActive( n ) && ( !options::cbqi() || !quantifiers::TermUtil:… in isLegalCandidate()