Searched refs:registerUnitClause (Results 1 – 4 of 4) sorted by relevance
| /dports/math/cvc4/CVC4-1.7/src/proof/ |
| H A D | sat_proof_implementation.h | 539 ClauseId TSatProof<Solver>::registerUnitClause(typename Solver::TLit lit, in registerUnitClause() function
577 d_trueLit = registerUnitClause(lit, INPUT); in registerTrueLit()
583 d_falseLit = registerUnitClause(lit, INPUT); in registerFalseLit()
758 ClauseId id = registerUnitClause(lit, LEARNT); in endResChain()
821 ClauseId unit_id = registerUnitClause(lit, LEARNT); in resolveUnit()
831 d_unitConflictId.set(registerUnitClause(conflict_lit, kind)); in storeUnitConflict()
|
| H A D | sat_proof.h | 159 ClauseId registerUnitClause(const typename Solver::TLit lit, ClauseKind kind);
|
| /dports/math/cvc4/CVC4-1.7/src/prop/minisat/core/ |
| H A D | Solver.cc | 465 id = ProofManager::getSatProof()->registerUnitClause(ps[0], INPUT); in addClause_()
1815 ClauseId id = ProofManager::getSatProof()->registerUnitClause(lemma[0], THEORY_LEMMA); in updateLemmas()
|
| /dports/math/cvc4/CVC4-1.7/src/prop/bvminisat/core/ |
| H A D | Solver.cc | 245 if(d_bvp){ id = d_bvp->getSatProof()->registerUnitClause(ps[0], INPUT);} in addClause_()
|