Home
last modified time | relevance | path

Searched refs:containsVtsTerm (Results 1 – 4 of 4) sorted by relevance

/dports/math/cvc4/CVC4-1.7/src/theory/quantifiers/
H A Dterm_util.h219 bool containsVtsTerm( Node n, bool isFree = false );
221 bool containsVtsTerm( std::vector< Node >& n, bool isFree = false );
H A Dterm_util.cpp467 if( containsVtsTerm( slv ) ){ in rewriteVtsSymbols()
525 bool TermUtil::containsVtsTerm( Node n, bool isFree ) { in containsVtsTerm() function in CVC4::theory::quantifiers::TermUtil
531 bool TermUtil::containsVtsTerm( std::vector< Node >& n, bool isFree ) { in containsVtsTerm() function in CVC4::theory::quantifiers::TermUtil
/dports/math/cvc4/CVC4-1.7/src/theory/quantifiers/cegqi/
H A Dinst_strategy_cegqi.cpp633 bool used_vts = d_quantEngine->getTermUtil()->containsVtsTerm( subs, false ); in doAddInstantiation()
/dports/math/cvc4/CVC4-1.7/src/theory/quantifiers/sygus/
H A Dce_guided_single_inv.cpp422 if( d_qe->getTermUtil()->containsVtsTerm( lem ) ){ in doAddInstantiation()