Searched refs:getEntailedTerm2 (Results 1 – 2 of 2) sorted by relevance
| /dports/math/cvc4/CVC4-1.7/src/theory/quantifiers/ |
| H A D | term_database.cpp | 599 TNode TermDb::getEntailedTerm2( TNode n, std::map< TNode, TNode >& subs, bool subsRep, bool hasSubs… in getEntailedTerm2() function in CVC4::theory::quantifiers::TermDb
615 return getEntailedTerm2( it->second, subs, subsRep, hasSubs, qy ); in getEntailedTerm2()
622 return getEntailedTerm2( n[ i==0 ? 1 : 2 ], subs, subsRep, hasSubs, qy ); in getEntailedTerm2()
631 TNode c = getEntailedTerm2( n[i], subs, subsRep, hasSubs, qy ); in getEntailedTerm2()
660 return getEntailedTerm2( n, subs, subsRep, true, qy ); in getEntailedTerm()
668 return getEntailedTerm2( n, subs, false, false, qy ); in getEntailedTerm()
676 TNode n1 = getEntailedTerm2( n[0], subs, subsRep, hasSubs, qy ); in isEntailed2()
678 TNode n2 = getEntailedTerm2( n[1], subs, subsRep, hasSubs, qy ); in isEntailed2()
719 TNode n1 = getEntailedTerm2( n, subs, subsRep, hasSubs, qy ); in isEntailed2()
|
| H A D | term_database.h | 312 …TNode getEntailedTerm2( TNode n, std::map< TNode, TNode >& subs, bool subsRep, bool hasSubs, Equal…
|