Home
last modified time | relevance | path

Searched defs:getInstantiatedQuantifiedFormulas (Results 1 – 4 of 4) sorted by relevance

/dports/math/cvc4/CVC4-1.7/src/theory/quantifiers/
H A Dinstantiate.cpp539 void Instantiate::getInstantiatedQuantifiedFormulas(std::vector<Node>& qs) in getInstantiatedQuantifiedFormulas() function in CVC4::theory::quantifiers::Instantiate
/dports/math/cvc4/CVC4-1.7/src/theory/
H A Dquantifiers_engine.cpp1152 void QuantifiersEngine::getInstantiatedQuantifiedFormulas( std::vector< Node >& qs ) { in getInstantiatedQuantifiedFormulas() function in QuantifiersEngine
H A Dtheory_engine.cpp1524 void TheoryEngine::getInstantiatedQuantifiedFormulas( std::vector< Node >& qs ) { in getInstantiatedQuantifiedFormulas() function in CVC4::TheoryEngine
/dports/math/cvc4/CVC4-1.7/src/smt/
H A Dsmt_engine.cpp4988 void SmtEngine::getInstantiatedQuantifiedFormulas( std::vector< Expr >& qs ) { in getInstantiatedQuantifiedFormulas() function in CVC4::SmtEngine