From 7d7ce3ecd03059602f70f26612aabd4a2ec49422 Mon Sep 17 00:00:00 2001
From: Alan Mishchenko <alanmi@berkeley.edu>
Date: Thu, 28 Dec 2017 23:04:24 -0800
Subject: New exact synthesis command 'allexact'.

---
 src/sat/glucose/Glucose.cpp | 6 ++++++
 1 file changed, 6 insertions(+)

(limited to 'src/sat/glucose')

diff --git a/src/sat/glucose/Glucose.cpp b/src/sat/glucose/Glucose.cpp
index 3ca372a8..0f2d2fce 100644
--- a/src/sat/glucose/Glucose.cpp
+++ b/src/sat/glucose/Glucose.cpp
@@ -253,6 +253,12 @@ bool Solver::addClause_(vec<Lit>& ps)
       else if (value(ps[i]) != l_False && ps[i] != p)
         ps[j++] = p = ps[i];
     ps.shrink(i - j);
+
+    if ( 0 ) {
+        for ( int i = 0; i < ps.size(); i++ )
+            printf( "%s%d ", (toInt(ps[i]) & 1) ? "-":"", toInt(ps[i]) >> 1 );
+        printf( "\n" );
+    }
     
     if (flag && (certifiedUNSAT)) {
       for (i = j = 0, p = lit_Undef; i < ps.size(); i++)
-- 
cgit v1.2.3