Searched refs:evaluateTerm2 (Results 1 – 2 of 2) sorted by relevance
| /dports/math/cvc4/CVC4-1.7/src/theory/quantifiers/ |
| H A D | term_database.cpp | 514 Node TermDb::evaluateTerm2( TNode n, std::map< TNode, Node >& visited, EqualityQuery * qy, bool use… in evaluateTerm2() function in CVC4::theory::quantifiers::TermDb
530 TNode c = evaluateTerm2( n[i], visited, qy, useEntailmentTests ); in evaluateTerm2()
542 ret = evaluateTerm2( n[ c==d_true ? 1 : 2], visited, qy, useEntailmentTests ); in evaluateTerm2()
653 return evaluateTerm2( n, visited, qy, useEntailmentTests ); in evaluateTerm()
|
| H A D | term_database.h | 310 …Node evaluateTerm2( TNode n, std::map< TNode, Node >& visited, EqualityQuery * qy, bool useEntailm…
|