Home
last modified time | relevance | path

Searched refs:satClauseToNodeSet (Results 1 – 2 of 2) sorted by relevance

/dports/math/cvc4/CVC4-1.7/src/proof/
H A Dproof_manager.cpp392 std::set<Node> lemma = satClauseToNodeSet(it->second); in getLemmasInUnsatCore()
414 std::set<Node> ProofManager::satClauseToNodeSet(prop::SatClause* clause) { in satClauseToNodeSet() function in CVC4::ProofManager
448 std::set<Node> currentLemma = satClauseToNodeSet(it->second); in getWeakestImplicantInUnsatCore()
477 std::set<Node> currentLemma = satClauseToNodeSet(it->second); in getWeakestImplicantInUnsatCore()
H A Dproof_manager.h305 std::set<Node> satClauseToNodeSet(prop::SatClause* clause);