Searched refs:getCongruentTerm (Results 1 – 7 of 7) sorted by relevance
/dports/math/cvc4/CVC4-1.7/src/theory/quantifiers/ |
H A D | term_database.h | 164 TNode getCongruentTerm(Node f, Node n); 171 TNode getCongruentTerm(Node f, std::vector<TNode>& args);
|
H A D | equality_query.h | 83 TNode getCongruentTerm(Node f, std::vector<TNode>& args) override;
|
H A D | equality_query.cpp | 233 TNode EqualityQueryQuantifiersEngine::getCongruentTerm( Node f, std::vector< TNode >& args ) { in getCongruentTerm() function in CVC4::theory::quantifiers::EqualityQueryQuantifiersEngine 234 return d_qe->getTermDatabase()->getCongruentTerm( f, args ); in getCongruentTerm()
|
H A D | quant_util.h | 234 virtual TNode getCongruentTerm( Node f, std::vector< TNode >& args ) = 0;
|
H A D | inst_propagator.cpp | 103 TNode EqualityQueryInstProp::getCongruentTerm( Node f, std::vector< TNode >& args ) { in getCongruentTerm() function in EqualityQueryInstProp 104 TNode t = d_qe->getTermDatabase()->getCongruentTerm( f, args ); in getCongruentTerm() 174 TNode t = d_qe->getTermDatabase()->getCongruentTerm( f, args ); in getCongruentTermExp() 515 TNode nn = getCongruentTerm( f, t_args ); in evaluateTermExp()
|
H A D | term_database.cpp | 553 TNode nn = qy->getCongruentTerm( f, args ); in evaluateTerm2() 639 TNode nn = qy->getCongruentTerm( f, args ); in getEntailedTerm2() 1054 TNode TermDb::getCongruentTerm( Node f, Node n ) { in getCongruentTerm() function in CVC4::theory::quantifiers::TermDb 1068 TNode TermDb::getCongruentTerm( Node f, std::vector< TNode >& args ) { in getCongruentTerm() function in CVC4::theory::quantifiers::TermDb
|
H A D | inst_propagator.h | 62 TNode getCongruentTerm(Node f, std::vector<TNode>& args) override;
|