Home
last modified time | relevance | path

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

/dports/math/cvc4/CVC4-1.7/src/proof/
H A Dbitvector_proof.cpp211 if (ProofManager::getSkolemizationManager()->isSkolem(term)) { in printOwnedTerm()
366 …if ((it->isVariable() || it->isConst()) && !ProofManager::getSkolemizationManager()->isSkolem(*it)… in printTermDeclarations()
H A Dproof_manager.h198 static SkolemizationManager *getSkolemizationManager();
H A Darray_proof.cpp1269 if (ProofManager::getSkolemizationManager()->isSkolem(*it)) { in printTermDeclarations()
1290 Node equality = ProofManager::getSkolemizationManager()->getDisequality(*it); in printDeferredDeclarations()
H A Dproof_manager.cpp139 SkolemizationManager* ProofManager::getSkolemizationManager() { in getSkolemizationManager() function in CVC4::ProofManager
H A Darith_proof.cpp662 if (term.isVariable() && !ProofManager::getSkolemizationManager()->isSkolem(term)) { in registerTerm()
H A Dtheory_proof.cpp207 …if (ProofManager::getSkolemizationManager()->isSkolem(term) && theory_id != theory::THEORY_ARRAYS)… in registerTerm()
/dports/math/cvc4/CVC4-1.7/src/theory/arrays/
H A Dtheory_arrays.cpp1370 PROOF(ProofManager::getSkolemizationManager()->registerSkolem(fact, k)); in check()
1372 if (!ProofManager::getSkolemizationManager()->hasSkolem(fact)) { in check()
1379 k = ProofManager::getSkolemizationManager()->getSkolem(fact); in check()