Searched refs:currentLemma (Results 1 – 1 of 1) sorted by relevance
448 std::set<Node> currentLemma = satClauseToNodeSet(it->second); in getWeakestImplicantInUnsatCore() local454 if (!getCnfProof()->haveProofRecipe(currentLemma)) in getWeakestImplicantInUnsatCore()457 recipe = getCnfProof()->getProofRecipe(currentLemma); in getWeakestImplicantInUnsatCore()459 for (lemmaIt = currentLemma.begin(); lemmaIt != currentLemma.end(); ++lemmaIt) { in getWeakestImplicantInUnsatCore()477 std::set<Node> currentLemma = satClauseToNodeSet(it->second); in getWeakestImplicantInUnsatCore() local483 if (!getCnfProof()->haveProofRecipe(currentLemma)) in getWeakestImplicantInUnsatCore()486 recipe = getCnfProof()->getProofRecipe(currentLemma); in getWeakestImplicantInUnsatCore()489 for (lemmaIt = currentLemma.begin(); lemmaIt != currentLemma.end(); ++lemmaIt) { in getWeakestImplicantInUnsatCore()