Home
last modified time | relevance | path

Searched refs:getCongruentTerm (Results 1 – 7 of 7) sorted by relevance

/dports/math/cvc4/CVC4-1.7/src/theory/quantifiers/
H A Dterm_database.h164 TNode getCongruentTerm(Node f, Node n);
171 TNode getCongruentTerm(Node f, std::vector<TNode>& args);
H A Dequality_query.h83 TNode getCongruentTerm(Node f, std::vector<TNode>& args) override;
H A Dequality_query.cpp233 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 Dquant_util.h234 virtual TNode getCongruentTerm( Node f, std::vector< TNode >& args ) = 0;
H A Dinst_propagator.cpp103 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 Dterm_database.cpp553 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 Dinst_propagator.h62 TNode getCongruentTerm(Node f, std::vector<TNode>& args) override;