From 068985035a64d556cbfc2e46af44566c01e0a5e0 Mon Sep 17 00:00:00 2001
From: Morgan Deters <mdeters@gmail.com>
Date: Thu, 14 Apr 2011 20:41:19 +0000
Subject: [PATCH] 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.

---
 src/printer/smt2/smt2_printer.cpp  |  5 +++++
 src/prop/sat.cpp                   | 22 +++++++++++++++-------
 src/theory/output_channel.h        |  4 +++-
 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);
   }
 
-- 
2.30.2