From b732c86723668bd73094fa9a2719760a91cd9981 Mon Sep 17 00:00:00 2001 From: Alex Ozdemir Date: Mon, 18 Nov 2019 16:41:07 -0800 Subject: Signature documentation update (#3476) This comment was slightly out-of-date. --- proofs/signatures/drat.plf | 14 +++++++++----- 1 file changed, 9 insertions(+), 5 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. -- cgit v1.2.3 From 7ac4aac015e69a6f377c5254c600bea386d58577 Mon Sep 17 00:00:00 2001 From: Alex Ozdemir Date: Mon, 18 Nov 2019 17:07:52 -0800 Subject: Add a few comments to ProofManager (#3477) --- src/proof/proof_manager.cpp | 8 +++++++- 1 file changed, 7 insertions(+), 1 deletion(-) 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); -- cgit v1.2.3