diff options
author | Morgan Deters <mdeters@cs.nyu.edu> | 2014-08-22 16:59:28 -0400 |
---|---|---|
committer | Morgan Deters <mdeters@cs.nyu.edu> | 2014-08-22 17:58:14 -0400 |
commit | 2dbe1f150d30f0fb0c8522f891104270ce09db4c (patch) | |
tree | 1305f3de890f4353c3b5695a93ab7e2419760617 /src/prop/cnf_stream.cpp | |
parent | 4ec2c8eb8b8a50dc743119100767e101f19305f6 (diff) |
Unsat core infrastruture and API (SMT-LIB compliance to come).
Diffstat (limited to 'src/prop/cnf_stream.cpp')
-rw-r--r-- | src/prop/cnf_stream.cpp | 28 |
1 files changed, 21 insertions, 7 deletions
diff --git a/src/prop/cnf_stream.cpp b/src/prop/cnf_stream.cpp index e0697735f..0d133aa13 100644 --- a/src/prop/cnf_stream.cpp +++ b/src/prop/cnf_stream.cpp @@ -44,7 +44,6 @@ using namespace CVC4::kind; namespace CVC4 { namespace prop { - CnfStream::CnfStream(SatSolver *satSolver, Registrar* registrar, context::Context* context, bool fullLitToNodeMap) : d_satSolver(satSolver), d_booleanVariables(context), @@ -52,6 +51,7 @@ CnfStream::CnfStream(SatSolver *satSolver, Registrar* registrar, context::Contex d_literalToNodeMap(context), d_fullLitToNodeMap(fullLitToNodeMap), d_registrar(registrar), + d_assertionTable(context), d_removable(false) { } @@ -74,7 +74,7 @@ void CnfStream::assertClause(TNode node, SatClause& c) { Dump("clauses") << AssertCommand(Expr(n.toExpr())); } } - d_satSolver->addClause(c, d_removable); + d_satSolver->addClause(c, d_removable, d_proofId); } void CnfStream::assertClause(TNode node, SatLiteral a) { @@ -104,9 +104,9 @@ bool CnfStream::hasLiteral(TNode n) const { } void TseitinCnfStream::ensureLiteral(TNode n) { - - // These are not removable + // These are not removable and have no proof ID d_removable = false; + d_proofId = uint64_t(-1); Debug("cnf") << "ensureLiteral(" << n << ")" << endl; if(hasLiteral(n)) { @@ -188,9 +188,12 @@ SatLiteral CnfStream::newLiteral(TNode node, bool isTheoryAtom, bool preRegister // If a theory literal, we pre-register it if (preRegister) { - bool backup = d_removable; + // In case we are re-entered due to lemmas, save our state + bool backupRemovable = d_removable; + uint64_t backupProofId= d_proofId; d_registrar->preRegister(node); - d_removable = backup; + d_removable = backupRemovable; + d_proofId = backupProofId; } // Here, you can have it @@ -642,9 +645,20 @@ void TseitinCnfStream::convertAndAssertIte(TNode node, bool negated) { // At the top level we must ensure that all clauses that are asserted are // not unit, except for the direct assertions. This allows us to remove the // clauses later when they are not needed anymore (lemmas for example). -void TseitinCnfStream::convertAndAssert(TNode node, bool removable, bool negated) { +void TseitinCnfStream::convertAndAssert(TNode node, bool removable, bool negated, ProofRule proof_id, TNode from) { Debug("cnf") << "convertAndAssert(" << node << ", removable = " << (removable ? "true" : "false") << ", negated = " << (negated ? "true" : "false") << ")" << endl; d_removable = removable; + if(options::proof() || options::unsatCores()) { + // Encode the assertion ID in the proof_id to store with generated clauses. + uint64_t assertionTableIndex = d_assertionTable.size(); + Assert((uint64_t(proof_id) & 0xffffffff00000000) == 0 && (assertionTableIndex & 0xffffffff00000000) == 0, "proof_id/table_index collision"); + d_proofId = assertionTableIndex | (uint64_t(proof_id) << 32); + d_assertionTable.push_back(from.isNull() ? node : from); + Debug("cores") << "cnf ix " << assertionTableIndex << " asst " << node << " proof_id " << proof_id << " from " << from << endl; + } else { + // We aren't producing proofs or unsat cores; use an invalid proof id. + d_proofId = uint64_t(-1); + } convertAndAssert(node, negated); } |