Searched refs:subsRep (Results 1 – 2 of 2) sorted by relevance
| /dports/math/cvc4/CVC4-1.7/src/theory/quantifiers/ |
| H A D | term_database.cpp | 610 if( subsRep ){ in getEntailedTerm2()
621 if( isEntailed2( n[0], subs, subsRep, hasSubs, i==0, qy ) ){ in getEntailedTerm2()
660 return getEntailedTerm2( n, subs, subsRep, true, 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()
694 return isEntailed2( n[0], subs, subsRep, hasSubs, !pol, qy ); in isEntailed2()
698 if( isEntailed2( n[i], subs, subsRep, hasSubs, pol, qy ) ){ in isEntailed2()
712 if( isEntailed2( n[0], subs, subsRep, hasSubs, i==0, qy ) ){ in isEntailed2()
719 TNode n1 = getEntailedTerm2( n, subs, subsRep, hasSubs, qy ); in isEntailed2()
731 return isEntailed2( n[1], subs, subsRep, hasSubs, pol, qy ); in isEntailed2()
[all …]
|
| H A D | term_database.h | 216 bool subsRep,
234 bool subsRep,
312 …TNode getEntailedTerm2( TNode n, std::map< TNode, TNode >& subs, bool subsRep, bool hasSubs, Equal…
314 …bool isEntailed2( TNode n, std::map< TNode, TNode >& subs, bool subsRep, bool hasSubs, bool pol, E…
|