diff options
author | Morgan Deters <mdeters@gmail.com> | 2011-04-14 20:41:19 +0000 |
---|---|---|
committer | Morgan Deters <mdeters@gmail.com> | 2011-04-14 20:41:19 +0000 |
commit | 068985035a64d556cbfc2e46af44566c01e0a5e0 (patch) | |
tree | 5c6a9c58eb0d740dec1f651bb7701028ae1beb73 /src/prop | |
parent | 7e289e28e54afa144032048443202a88fa124cb5 (diff) |
Three things:
1. Infrastructure for unit T-conflicts added to SAT proxy
(and also the theory output channel documentation);
previously theories could not communicate unit T-conflicts
with the SAT layer because that layer had an implicit
assumption (not asserted) that the conflict nodes were an AND.
2. UF now pre-rewrites trivial equalities to "true". These could
conceivably occur in artificial benchmarks in this form:
(let (?x BIG-HUGE-TERM) ... (= ?x ?x) ... )
3. The SMT-LIBv2 printer now properly prints Bool constants.
Diffstat (limited to 'src/prop')
-rw-r--r-- | src/prop/sat.cpp | 22 |
1 files changed, 15 insertions, 7 deletions
diff --git a/src/prop/sat.cpp b/src/prop/sat.cpp index 40c17e016..f34699e2b 100644 --- a/src/prop/sat.cpp +++ b/src/prop/sat.cpp @@ -28,6 +28,7 @@ namespace CVC4 { namespace prop { void SatSolver::theoryCheck(theory::Theory::Effort effort, SatClause& conflict) { + Assert(conflict.size() == 0); // Try theory propagation bool ok = d_theoryEngine->check(effort); // If in conflict construct the conflict clause @@ -35,15 +36,22 @@ void SatSolver::theoryCheck(theory::Theory::Effort effort, SatClause& conflict) // We have a conflict, get it Node conflictNode = d_theoryEngine->getConflict(); Debug("prop") << "SatSolver::theoryCheck() => conflict: " << conflictNode << std::endl; - // Go through the literals and construct the conflict clause - Node::const_iterator literal_it = conflictNode.begin(); - Node::const_iterator literal_end = conflictNode.end(); - while (literal_it != literal_end) { + if(conflictNode.getKind() == kind::AND) { + // Go through the literals and construct the conflict clause + Node::const_iterator literal_it = conflictNode.begin(); + Node::const_iterator literal_end = conflictNode.end(); + while (literal_it != literal_end) { + // Get the literal corresponding to the node + SatLiteral l = d_cnfStream->getLiteral(*literal_it); + // Add the negation to the conflict clause and continue + conflict.push(~l); + literal_it ++; + } + } else { // unit conflict // Get the literal corresponding to the node - SatLiteral l = d_cnfStream->getLiteral(*literal_it); - // Add the negation to the conflict clause and continue + SatLiteral l = d_cnfStream->getLiteral(conflictNode); + // construct the unit conflict clause conflict.push(~l); - literal_it ++; } } } |