diff options
author | Alex Ozdemir <aozdemir@hmc.edu> | 2019-03-15 18:51:47 -0700 |
---|---|---|
committer | Andres Noetzli <andres.noetzli@gmail.com> | 2019-03-16 01:51:47 +0000 |
commit | 5d0a5a729680a1db3f44e31037955390e86440ce (patch) | |
tree | d2f85ff47f75935439a14f514a5133d1dd6d5cad /src/proof/cnf_proof.cpp | |
parent | 2989780f0242d14712927bd4c01c4a521a8fe399 (diff) |
Enable CryptoMiniSat-backed BV proofs (#2847)
* Connect the plumbing so that BV proofs are enabled when using
CryptoMiniSat
* Also fixed a bug in CNF-proof generation
* Specifically, CNF proofs broke when proving tautological clauses.
Now they don't.
Diffstat (limited to 'src/proof/cnf_proof.cpp')
-rw-r--r-- | src/proof/cnf_proof.cpp | 173 |
1 files changed, 122 insertions, 51 deletions
diff --git a/src/proof/cnf_proof.cpp b/src/proof/cnf_proof.cpp index 4e8d20162..aed889e33 100644 --- a/src/proof/cnf_proof.cpp +++ b/src/proof/cnf_proof.cpp @@ -349,6 +349,39 @@ void CnfProof::collectAssertionsForClauses(const IdToSatClause& clauses, } } +// Detects whether a clause has x v ~x for some x +// If so, returns the positive occurence's idx first, then the negative's +Maybe<std::pair<size_t, size_t>> CnfProof::detectTrivialTautology( + const prop::SatClause& clause) +{ + // a map from a SatVariable to its previous occurence's polarity and location + std::map<prop::SatVariable, std::pair<bool, size_t>> varsToPolsAndIndices; + for (size_t i = 0; i < clause.size(); ++i) + { + prop::SatLiteral lit = clause[i]; + prop::SatVariable var = lit.getSatVariable(); + bool polarity = !lit.isNegated(); + + // Check if this var has already occured w/ opposite polarity + auto iter = varsToPolsAndIndices.find(var); + if (iter != varsToPolsAndIndices.end() && iter->second.first != polarity) + { + if (iter->second.first) + { + return Maybe<std::pair<size_t, size_t>>{ + std::make_pair(iter->second.second, i)}; + } + else + { + return Maybe<std::pair<size_t, size_t>>{ + std::make_pair(i, iter->second.second)}; + } + } + varsToPolsAndIndices[var] = std::make_pair(polarity, i); + } + return Maybe<std::pair<size_t, size_t>>{}; +} + void LFSCCnfProof::printAtomMapping(const std::set<Node>& atoms, std::ostream& os, std::ostream& paren) { @@ -431,61 +464,98 @@ void LFSCCnfProof::printCnfProofForClause(ClauseId id, Assert( clause->size()>0 ); - Node base_assertion = getDefinitionForClause(id); - - //get the assertion for the clause id - std::map<Node, unsigned > childIndex; - std::map<Node, bool > childPol; - Node assertion = clauseToNode( *clause, childIndex, childPol ); - //if there is no reason, construct assertion directly. This can happen for unit clauses. - if( base_assertion.isNull() ){ - base_assertion = assertion; + // If the clause contains x v ~x, it's easy! + // + // It's important to check for this case, because our other logic for + // recording the location of variables in the clause assumes the clause is + // not tautological + Maybe<std::pair<size_t, size_t>> isTrivialTaut = + detectTrivialTautology(*clause); + if (isTrivialTaut.just()) + { + size_t posIndexInClause = isTrivialTaut.value().first; + size_t negIndexInClause = isTrivialTaut.value().second; + Trace("cnf-pf") << "; Indices " << posIndexInClause << " (+) and " + << negIndexInClause << " (-) make this clause a tautology" + << std::endl; + + std::string proofOfPos = + ProofManager::getLitName((*clause)[negIndexInClause], d_name); + std::string proofOfNeg = + ProofManager::getLitName((*clause)[posIndexInClause], d_name); + os << "(contra _ " << proofOfPos << " " << proofOfNeg << ")"; } - //os_base is proof of base_assertion - std::stringstream os_base; - - // checks if tautological definitional clause or top-level clause - // and prints the proof of the top-level formula - bool is_input = printProofTopLevel(base_assertion, os_base); + else + { + Node base_assertion = getDefinitionForClause(id); + + // get the assertion for the clause id + std::map<Node, unsigned> childIndex; + std::map<Node, bool> childPol; + Node assertion = clauseToNode(*clause, childIndex, childPol); + // if there is no reason, construct assertion directly. This can happen + // for unit clauses. + if (base_assertion.isNull()) + { + base_assertion = assertion; + } + // os_base is proof of base_assertion + std::stringstream os_base; + + // checks if tautological definitional clause or top-level clause + // and prints the proof of the top-level formula + bool is_input = printProofTopLevel(base_assertion, os_base); + + if (is_input) + { + Debug("cnf-pf") << std::endl + << "; base assertion is input. proof: " << os_base.str() + << std::endl; + } - if (is_input) { - Debug("cnf-pf") << std::endl << "; base assertion is input. proof: " << os_base.str() << std::endl; - } + // get base assertion with polarity + bool base_pol = base_assertion.getKind() != kind::NOT; + base_assertion = base_assertion.getKind() == kind::NOT ? base_assertion[0] + : base_assertion; - //get base assertion with polarity - bool base_pol = base_assertion.getKind()!=kind::NOT; - base_assertion = base_assertion.getKind()==kind::NOT ? base_assertion[0] : base_assertion; - - std::map< Node, unsigned >::iterator itci = childIndex.find( base_assertion ); - bool is_in_clause = itci!=childIndex.end(); - unsigned base_index = is_in_clause ? itci->second : 0; - Trace("cnf-pf") << std::endl; - Trace("cnf-pf") << "; input = " << is_input << ", is_in_clause = " << is_in_clause << ", id = " << id << ", assertion = " << assertion << ", base assertion = " << base_assertion << std::endl; - if (!is_input){ - Assert(is_in_clause); - prop::SatLiteral blit = (*clause)[ base_index ]; - os_base << ProofManager::getLitName(blit, d_name); - base_pol = !childPol[base_assertion]; // WHY? if the case is => - } - Trace("cnf-pf") << "; polarity of base assertion = " << base_pol << std::endl; - Trace("cnf-pf") << "; proof of base : " << os_base.str() << std::endl; - - bool success = false; - if( is_input && - is_in_clause && - childPol[base_assertion]==base_pol ){ - //if both in input and in clause, the proof is trivial. this is the case for unit clauses. - Trace("cnf-pf") << "; trivial" << std::endl; - os << "(contra _ "; - success = true; - prop::SatLiteral lit = (*clause)[itci->second]; - if( base_pol ){ - os << os_base.str() << " " << ProofManager::getLitName(lit, d_name); - }else{ - os << ProofManager::getLitName(lit, d_name) << " " << os_base.str(); + std::map<Node, unsigned>::iterator itci = childIndex.find(base_assertion); + bool is_in_clause = itci != childIndex.end(); + unsigned base_index = is_in_clause ? itci->second : 0; + Trace("cnf-pf") << std::endl; + Trace("cnf-pf") << "; input = " << is_input + << ", is_in_clause = " << is_in_clause << ", id = " << id + << ", assertion = " << assertion + << ", base assertion = " << base_assertion << std::endl; + if (!is_input) + { + Assert(is_in_clause); + prop::SatLiteral blit = (*clause)[base_index]; + os_base << ProofManager::getLitName(blit, d_name); + base_pol = !childPol[base_assertion]; // WHY? if the case is => } - os << ")"; - } else if ((base_assertion.getKind()==kind::AND && !base_pol) || + Trace("cnf-pf") << "; polarity of base assertion = " << base_pol + << std::endl; + Trace("cnf-pf") << "; proof of base : " << os_base.str() << std::endl; + + bool success = false; + if (is_input && is_in_clause && childPol[base_assertion] == base_pol) + { + // if both in input and in clause, the proof is trivial. this is the case + // for unit clauses. + Trace("cnf-pf") << "; trivial" << std::endl; + os << "(contra _ "; + success = true; + prop::SatLiteral lit = (*clause)[itci->second]; + if (base_pol) + { + os << os_base.str() << " " << ProofManager::getLitName(lit, d_name); + } + else + { + os << ProofManager::getLitName(lit, d_name) << " " << os_base.str(); + } + os << ")"; + } else if ((base_assertion.getKind()==kind::AND && !base_pol) || ((base_assertion.getKind()==kind::OR || base_assertion.getKind()==kind::IMPLIES) && base_pol)) { Trace("cnf-pf") << "; and/or case 1" << std::endl; @@ -776,6 +846,7 @@ void LFSCCnfProof::printCnfProofForClause(ClauseId id, Trace("cnf-pf") << std::endl; os << "trust-bad"; } + } os << ")" << clause_paren.str() << " (\\ " << ProofManager::getInputClauseName(id, d_name) << "\n"; |