Searched refs:removedDfs (Results 1 – 2 of 2) sorted by relevance
| /dports/math/cvc4/CVC4-1.7/src/proof/ |
| H A D | sat_proof.h | 277 void removedDfs(typename Solver::TLit lit, LitSet* removedSet,
|
| H A D | sat_proof_implementation.h | 629 void TSatProof<Solver>::removedDfs(typename Solver::TLit lit, in removedDfs() function
648 removedDfs(v, removedSet, removeStack, inClause, seen); in removedDfs()
672 removedDfs(*it, removed, removeStack, inClause, seen); in removeRedundantFromRes()
|