diff options
| -rw-r--r-- | proofs/signatures/drat.plf | 14 | ||||
| -rw-r--r-- | src/proof/proof_manager.cpp | 8 |
2 files changed, 16 insertions, 6 deletions
diff --git a/proofs/signatures/drat.plf b/proofs/signatures/drat.plf index 9f1ec00a9..2f70bbfbd 100644 --- a/proofs/signatures/drat.plf +++ b/proofs/signatures/drat.plf @@ -11,7 +11,8 @@ ; Both are detailed in this paper, along with their differences: ; http://fmv.jku.at/papers/RebolaPardoBiere-POS18.pdf ; -; This signature checks **Specified DRAT**. +; This signature contains implementations for a checker for each. +; **Specified DRAT** is first. ; A DRAT proof itself: a list of addition or deletion instructions. (declare DRATProof type) @@ -23,7 +24,8 @@ ; Functional Programs ; ; ==================== ; -; Are two clauses equal (in the set sense) +; Are two clauses equal (i.e., if interpretted as sets of literals, are those +; sets equal?) ; ; Assumes that marks 1,2,3,4 are clear for the constituent variables, and ; leaves them clear afterwards. @@ -44,9 +46,11 @@ ; the mark 2 means (seen as - in c1, but not yet in c2) ; the mark 4 means (seen as - in c1) ; -; This implementation is robust to literal order, repeated literals, and -; literals of opposite polarity in the same clause. It is true equality on sets -; literals. +; This implementation **does not**: +; 1. assume that clauses do not have duplicates +; (so the clause [x v x v ~y] is an accceptable input) +; 2. assume that clauses are non-tautological +; (so the clause [x v ~x] is an acceptable input) ; ; TODO(aozdemir) This implementation could be further optimized b/c once c1 is ; drained, we need not continue to pattern match on it. diff --git a/src/proof/proof_manager.cpp b/src/proof/proof_manager.cpp index fa4c1ecb5..bbf5b0064 100644 --- a/src/proof/proof_manager.cpp +++ b/src/proof/proof_manager.cpp @@ -579,9 +579,13 @@ void LFSCProof::toStream(std::ostream& out) const CodeTimer skeletonProofTimer{ ProofManager::currentPM()->getStats().d_skeletonProofTraceTime}; Assert(!d_satProof->proofConstructed()); + + // Here we give our SAT solver a chance to flesh out the resolution proof. + // It proves bottom from a set of clauses. d_satProof->constructProof(); - // collecting leaf clauses in resolution proof + // We ask the SAT solver which clauses are used in that proof. + // For a resolution proof, these are the leaves of the tree. d_satProof->collectClausesUsed(used_inputs, used_lemmas); IdToSatClause::iterator it2; @@ -672,6 +676,8 @@ void LFSCProof::toStream(std::ostream& out) const } } + // From the clauses, compute the atoms (atomic theory predicates in + // assertions and lemmas). d_cnfProof->collectAtomsForClauses(used_inputs, atoms); d_cnfProof->collectAtomsForClauses(used_lemmas, atoms); |