Home
last modified time | relevance | path

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

/dports/math/cvc4/CVC4-1.7/src/theory/quantifiers/
H A Dterm_database.h201 TNode getEntailedTerm(TNode n, EqualityQuery* qy = NULL);
214 TNode getEntailedTerm(TNode n,
H A Dterm_database.cpp656 TNode TermDb::getEntailedTerm( TNode n, std::map< TNode, TNode >& subs, bool subsRep, EqualityQuery… in getEntailedTerm() function in CVC4::theory::quantifiers::TermDb
663 TNode TermDb::getEntailedTerm( TNode n, EqualityQuery * qy ) { in getEntailedTerm() function in CVC4::theory::quantifiers::TermDb
H A Dquant_conflict_find.cpp1224 TNode t = tdb->getEntailedTerm(d_n[i]); in reset_round()
H A Dconjecture_generator.cpp1337 TNode grhs = getTermDatabase()->getEntailedTerm( rhs, subs, true ); in notifySubstitution()