summaryrefslogtreecommitdiff
path: root/src
diff options
context:
space:
mode:
Diffstat (limited to 'src')
-rw-r--r--src/prop/proof_cnf_stream.cpp47
-rw-r--r--src/prop/proof_cnf_stream.h13
-rw-r--r--src/prop/sat_proof_manager.cpp33
-rw-r--r--src/prop/sat_proof_manager.h3
4 files changed, 60 insertions, 36 deletions
diff --git a/src/prop/proof_cnf_stream.cpp b/src/prop/proof_cnf_stream.cpp
index b5542ab35..8aaa68b9a 100644
--- a/src/prop/proof_cnf_stream.cpp
+++ b/src/prop/proof_cnf_stream.cpp
@@ -20,8 +20,6 @@
#include "theory/builtin/proof_checker.h"
#include "util/rational.h"
-using namespace cvc5::kind;
-
namespace cvc5 {
namespace prop {
@@ -58,7 +56,7 @@ bool ProofCnfStream::hasProofFor(Node f)
std::string ProofCnfStream::identify() const { return "ProofCnfStream"; }
-void ProofCnfStream::normalizeAndRegister(TNode clauseNode)
+Node ProofCnfStream::normalizeAndRegister(TNode clauseNode)
{
Node normClauseNode = d_psb.factorReorderElimDoubleNeg(clauseNode);
if (Trace.isOn("cnf") && normClauseNode != clauseNode)
@@ -69,6 +67,7 @@ void ProofCnfStream::normalizeAndRegister(TNode clauseNode)
<< pop;
}
d_satPM->registerSatAssumptions({normClauseNode});
+ return normClauseNode;
}
void ProofCnfStream::convertAndAssert(TNode node,
@@ -104,7 +103,8 @@ void ProofCnfStream::convertAndAssert(TNode node,
void ProofCnfStream::convertAndAssert(TNode node, bool negated)
{
Trace("cnf") << "ProofCnfStream::convertAndAssert(" << node
- << ", negated = " << (negated ? "true" : "false") << ")\n";
+ << ", negated = " << (negated ? "true" : "false") << ")\n"
+ << push;
switch (node.getKind())
{
case kind::AND: convertAndAssertAnd(node, negated); break;
@@ -159,12 +159,14 @@ void ProofCnfStream::convertAndAssert(TNode node, bool negated)
}
}
}
+ Trace("cnf") << pop;
}
void ProofCnfStream::convertAndAssertAnd(TNode node, bool negated)
{
Trace("cnf") << "ProofCnfStream::convertAndAssertAnd(" << node
- << ", negated = " << (negated ? "true" : "false") << ")\n";
+ << ", negated = " << (negated ? "true" : "false") << ")\n"
+ << push;
Assert(node.getKind() == kind::AND);
if (!negated)
{
@@ -205,12 +207,14 @@ void ProofCnfStream::convertAndAssertAnd(TNode node, bool negated)
normalizeAndRegister(clauseNode);
}
}
+ Trace("cnf") << pop;
}
void ProofCnfStream::convertAndAssertOr(TNode node, bool negated)
{
Trace("cnf") << "ProofCnfStream::convertAndAssertOr(" << node
- << ", negated = " << (negated ? "true" : "false") << ")\n";
+ << ", negated = " << (negated ? "true" : "false") << ")\n"
+ << push;
Assert(node.getKind() == kind::OR);
if (!negated)
{
@@ -240,12 +244,14 @@ void ProofCnfStream::convertAndAssertOr(TNode node, bool negated)
convertAndAssert(node[i], true);
}
}
+ Trace("cnf") << pop;
}
void ProofCnfStream::convertAndAssertXor(TNode node, bool negated)
{
Trace("cnf") << "ProofCnfStream::convertAndAssertXor(" << node
- << ", negated = " << (negated ? "true" : "false") << ")\n";
+ << ", negated = " << (negated ? "true" : "false") << ")\n"
+ << push;
if (!negated)
{
// p XOR q
@@ -317,12 +323,14 @@ void ProofCnfStream::convertAndAssertXor(TNode node, bool negated)
normalizeAndRegister(clauseNode);
}
}
+ Trace("cnf") << pop;
}
void ProofCnfStream::convertAndAssertIff(TNode node, bool negated)
{
Trace("cnf") << "ProofCnfStream::convertAndAssertIff(" << node
- << ", negated = " << (negated ? "true" : "false") << ")\n";
+ << ", negated = " << (negated ? "true" : "false") << ")\n"
+ << push;
if (!negated)
{
// p <=> q
@@ -400,12 +408,14 @@ void ProofCnfStream::convertAndAssertIff(TNode node, bool negated)
normalizeAndRegister(clauseNode);
}
}
+ Trace("cnf") << pop;
}
void ProofCnfStream::convertAndAssertImplies(TNode node, bool negated)
{
Trace("cnf") << "ProofCnfStream::convertAndAssertImplies(" << node
- << ", negated = " << (negated ? "true" : "false") << ")\n";
+ << ", negated = " << (negated ? "true" : "false") << ")\n"
+ << push;
if (!negated)
{
// ~p v q
@@ -444,12 +454,14 @@ void ProofCnfStream::convertAndAssertImplies(TNode node, bool negated)
<< "ProofCnfStream::convertAndAssertImplies: NOT_IMPLIES_ELIM2 added "
<< node[1].notNode() << "\n";
}
+ Trace("cnf") << pop;
}
void ProofCnfStream::convertAndAssertIte(TNode node, bool negated)
{
Trace("cnf") << "ProofCnfStream::convertAndAssertIte(" << node
- << ", negated = " << (negated ? "true" : "false") << ")\n";
+ << ", negated = " << (negated ? "true" : "false") << ")\n"
+ << push;
// ITE(p, q, r)
SatLiteral p = toCNF(node[0], false);
SatLiteral q = toCNF(node[1], negated);
@@ -515,6 +527,7 @@ void ProofCnfStream::convertAndAssertIte(TNode node, bool negated)
normalizeAndRegister(clauseNode);
}
}
+ Trace("cnf") << pop;
}
void ProofCnfStream::convertPropagation(TrustNode trn)
@@ -590,6 +603,20 @@ void ProofCnfStream::convertPropagation(TrustNode trn)
}
}
+
+Node ProofCnfStream::getClauseNode(const SatClause& clause)
+{
+ std::vector<Node> clauseNodes;
+ for (size_t i = 0, size = clause.size(); i < size; ++i)
+ {
+ SatLiteral satLit = clause[i];
+ clauseNodes.push_back(d_cnfStream.getNode(satLit));
+ }
+ // order children by node id
+ std::sort(clauseNodes.begin(), clauseNodes.end());
+ return NodeManager::currentNM()->mkNode(kind::OR, clauseNodes);
+}
+
void ProofCnfStream::ensureLiteral(TNode n)
{
Trace("cnf") << "ProofCnfStream::ensureLiteral(" << n << ")\n";
diff --git a/src/prop/proof_cnf_stream.h b/src/prop/proof_cnf_stream.h
index af131c2c3..b79b3098f 100644
--- a/src/prop/proof_cnf_stream.h
+++ b/src/prop/proof_cnf_stream.h
@@ -148,8 +148,19 @@ class ProofCnfStream : public ProofGenerator
* resulting clauses of the clausification process are synchronized with the
* clauses used in the underlying SAT solver, which automatically performs the
* above normalizations on all added clauses.
+ *
+ * @param clauseNode The clause node to be normalized.
+ * @return The normalized clause node.
+ */
+ Node normalizeAndRegister(TNode clauseNode);
+
+ /** Gets node equivalent to SAT clause.
+ *
+ * To avoid generating different nodes for the same clause, modulo ordering,
+ * an invariant assumed throughout this class, the OR node generated by this
+ * method always has its children ordered.
*/
- void normalizeAndRegister(TNode clauseNode);
+ Node getClauseNode(const SatClause& clause);
/** Reference to the underlying cnf stream. */
CnfStream& d_cnfStream;
diff --git a/src/prop/sat_proof_manager.cpp b/src/prop/sat_proof_manager.cpp
index fb37b1d01..fd57fb13c 100644
--- a/src/prop/sat_proof_manager.cpp
+++ b/src/prop/sat_proof_manager.cpp
@@ -42,33 +42,20 @@ SatProofManager::SatProofManager(Minisat::Solver* solver,
void SatProofManager::printClause(const Minisat::Clause& clause)
{
- for (unsigned i = 0, size = clause.size(); i < size; ++i)
+ for (size_t i = 0, size = clause.size(); i < size; ++i)
{
SatLiteral satLit = MinisatSatSolver::toSatLiteral(clause[i]);
Trace("sat-proof") << satLit << " ";
}
}
-Node SatProofManager::getClauseNode(SatLiteral satLit)
-{
- Assert(d_cnfStream->getNodeCache().find(satLit)
- != d_cnfStream->getNodeCache().end())
- << "SatProofManager::getClauseNode: literal " << satLit
- << " undefined.\n";
- return d_cnfStream->getNodeCache()[satLit];
-}
-
Node SatProofManager::getClauseNode(const Minisat::Clause& clause)
{
std::vector<Node> clauseNodes;
- for (unsigned i = 0, size = clause.size(); i < size; ++i)
+ for (size_t i = 0, size = clause.size(); i < size; ++i)
{
SatLiteral satLit = MinisatSatSolver::toSatLiteral(clause[i]);
- Assert(d_cnfStream->getNodeCache().find(satLit)
- != d_cnfStream->getNodeCache().end())
- << "SatProofManager::getClauseNode: literal " << satLit
- << " undefined\n";
- clauseNodes.push_back(d_cnfStream->getNodeCache()[satLit]);
+ clauseNodes.push_back(d_cnfStream->getNode(satLit));
}
// order children by node id
std::sort(clauseNodes.begin(), clauseNodes.end());
@@ -140,7 +127,7 @@ void SatProofManager::endResChain(Minisat::Lit lit)
SatLiteral satLit = MinisatSatSolver::toSatLiteral(lit);
Trace("sat-proof") << "SatProofManager::endResChain: chain_res for "
<< satLit;
- endResChain(getClauseNode(satLit), {satLit});
+ endResChain(d_cnfStream->getNode(satLit), {satLit});
}
void SatProofManager::endResChain(const Minisat::Clause& clause)
@@ -346,7 +333,7 @@ void SatProofManager::explainLit(SatLiteral lit,
std::unordered_set<TNode>& premises)
{
Trace("sat-proof") << push << "SatProofManager::explainLit: Lit: " << lit;
- Node litNode = getClauseNode(lit);
+ Node litNode = d_cnfStream->getNode(lit);
Trace("sat-proof") << " [" << litNode << "]\n";
// We don't need to explain nodes who are inputs. Note that it's *necessary*
// to avoid attempting such explanations because they can introduce cycles at
@@ -723,7 +710,7 @@ void SatProofManager::finalizeProof()
Trace("sat-proof")
<< "SatProofManager::finalizeProof: conflicting (lazy) satLit: "
<< d_conflictLit << "\n";
- finalizeProof(getClauseNode(d_conflictLit), {d_conflictLit});
+ finalizeProof(d_cnfStream->getNode(d_conflictLit), {d_conflictLit});
// reset since if in incremental mode this may be used again
d_conflictLit = undefSatVariable;
}
@@ -733,7 +720,7 @@ void SatProofManager::finalizeProof(Minisat::Lit inConflict, bool adding)
SatLiteral satLit = MinisatSatSolver::toSatLiteral(inConflict);
Trace("sat-proof") << "SatProofManager::finalizeProof: conflicting satLit: "
<< satLit << "\n";
- Node clauseNode = getClauseNode(satLit);
+ Node clauseNode = d_cnfStream->getNode(satLit);
if (adding)
{
registerSatAssumptions({clauseNode});
@@ -777,9 +764,11 @@ std::shared_ptr<ProofNode> SatProofManager::getProof()
void SatProofManager::registerSatLitAssumption(Minisat::Lit lit)
{
Trace("sat-proof") << "SatProofManager::registerSatLitAssumption: - "
- << getClauseNode(MinisatSatSolver::toSatLiteral(lit))
+ << d_cnfStream->getNode(
+ MinisatSatSolver::toSatLiteral(lit))
<< "\n";
- d_assumptions.insert(getClauseNode(MinisatSatSolver::toSatLiteral(lit)));
+ d_assumptions.insert(
+ d_cnfStream->getNode(MinisatSatSolver::toSatLiteral(lit)));
}
void SatProofManager::registerSatAssumptions(const std::vector<Node>& assumps)
diff --git a/src/prop/sat_proof_manager.h b/src/prop/sat_proof_manager.h
index a224f3a28..98d125591 100644
--- a/src/prop/sat_proof_manager.h
+++ b/src/prop/sat_proof_manager.h
@@ -568,14 +568,11 @@ class SatProofManager
/** All clauses added to the SAT solver, kept in a context-dependent manner.
*/
context::CDHashSet<Node> d_assumptions;
-
/**
* A placeholder that may be used to store the literal with the final
* conflict.
*/
SatLiteral d_conflictLit;
- /** Gets node equivalent to literal */
- Node getClauseNode(SatLiteral satLit);
/** Gets node equivalent to clause.
*
* To avoid generating different nodes for the same clause, modulo ordering,
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback