diff options
| -rw-r--r-- | src/printer/smt2/smt2_printer.cpp | 5 | ||||
| -rw-r--r-- | src/prop/sat.cpp | 22 | ||||
| -rw-r--r-- | src/theory/output_channel.h | 4 | ||||
| -rw-r--r-- | src/theory/uf/theory_uf_rewriter.h | 5 |
4 files changed, 28 insertions, 8 deletions
diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp index 91a529bc2..9bad4c7b5 100644 --- a/src/printer/smt2/smt2_printer.cpp +++ b/src/printer/smt2/smt2_printer.cpp @@ -74,6 +74,11 @@ void Smt2Printer::toStream(std::ostream& out, TNode n, } break; } + case kind::CONST_BOOLEAN: + // the default would print "1" or "0" for bool, that's not correct + // for our purposes + out << (n.getConst<bool>() ? "true" : "false"); + break; default: // fall back on whatever operator<< does on underlying type; we // might luck out and be SMT-LIB v2 compliant 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 ++; } } } diff --git a/src/theory/output_channel.h b/src/theory/output_channel.h index b25bf503d..a9722690b 100644 --- a/src/theory/output_channel.h +++ b/src/theory/output_channel.h @@ -72,7 +72,9 @@ public: * @param n - a conflict at the current decision level. This should * be an AND-kinded node of literals that are TRUE in the current * assignment and are in conflict (i.e., at least one must be - * assigned false). + * assigned false), or else a literal by itself (in the case of a + * unit conflict) which is assigned TRUE (and T-conflicting) in the + * current assignment. * * @param safe - whether it is safe to be interrupted */ diff --git a/src/theory/uf/theory_uf_rewriter.h b/src/theory/uf/theory_uf_rewriter.h index 744a3d966..ee88df126 100644 --- a/src/theory/uf/theory_uf_rewriter.h +++ b/src/theory/uf/theory_uf_rewriter.h @@ -51,6 +51,11 @@ public: } static RewriteResponse preRewrite(TNode node) { + if(node.getKind() == kind::EQUAL || node.getKind() == kind::IFF) { + if(node[0] == node[1]) { + return RewriteResponse(REWRITE_DONE, NodeManager::currentNM()->mkConst(true)); + } + } return RewriteResponse(REWRITE_DONE, node); } |