From: Morgan Deters <mdeters@gmail.com>
Date: Thu, 14 Apr 2011 20:41:19 +0000 (+0000)
Subject: Three things:
X-Git-Tag: cvc5-1.0.0~8598
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=068985035a64d556cbfc2e46af44566c01e0a5e0;p=cvc5.git

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.
---

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);
   }