From 0da555cb481696efd78d9c5dc6293b6a95d1ffd5 Mon Sep 17 00:00:00 2001
From: Alan Mishchenko <alanmi@berkeley.edu>
Date: Wed, 20 Sep 2006 08:01:00 -0700
Subject: Version abc60920

---
 src/sat/fraig/fraigSat.c | 14 ++++++++++++++
 1 file changed, 14 insertions(+)

(limited to 'src/sat/fraig/fraigSat.c')

diff --git a/src/sat/fraig/fraigSat.c b/src/sat/fraig/fraigSat.c
index af0f13ce..53057fc3 100644
--- a/src/sat/fraig/fraigSat.c
+++ b/src/sat/fraig/fraigSat.c
@@ -300,6 +300,7 @@ int Fraig_NodeIsEquivalent( Fraig_Man_t * p, Fraig_Node_t * pOld, Fraig_Node_t *
 {
     int RetValue, RetValue1, i, fComp, clk;
     int fVerbose = 0;
+    int fSwitch = 0;
 
     // make sure the nodes are not complemented
     assert( !Fraig_IsComplement(pNew) );
@@ -318,6 +319,7 @@ int Fraig_NodeIsEquivalent( Fraig_Man_t * p, Fraig_Node_t * pOld, Fraig_Node_t *
         if ( nBTLimit <= 10 )
             return 0;
         nBTLimit = (int)sqrt(nBTLimit);
+//        fSwitch = 1;
     }
 
     p->nSatCalls++;
@@ -417,6 +419,8 @@ PRT( "time", clock() - clk );
 //        if ( pOld->fFailTfo || pNew->fFailTfo )
 //            printf( "*" );
 //        printf( "s(%d)", pNew->Level );
+        if ( fSwitch )
+             printf( "s(%d)", pNew->Level );
         p->nSatCounter++;
         return 0;
     }
@@ -433,6 +437,8 @@ p->time3 += clock() - clk;
             pOld->fFailTfo = 1;
         pNew->fFailTfo = 1;
 //        p->nSatFails++;
+        if ( fSwitch )
+             printf( "T(%d)", pNew->Level );
         p->nSatFailsReal++;
         return 0;
     }
@@ -491,6 +497,8 @@ PRT( "time", clock() - clk );
 //        if ( pOld->fFailTfo || pNew->fFailTfo )
 //            printf( "*" );
 //        printf( "s(%d)", pNew->Level );
+        if ( fSwitch )
+             printf( "s(%d)", pNew->Level );
         return 0;
     }
     else // if ( RetValue1 == MSAT_UNKNOWN )
@@ -500,6 +508,8 @@ p->time3 += clock() - clk;
 //        if ( pOld->fFailTfo || pNew->fFailTfo )
 //            printf( "*" );
 //        printf( "T(%d)", pNew->Level );
+        if ( fSwitch )
+             printf( "T(%d)", pNew->Level );
 
         // mark the node as the failed node
         pOld->fFailTfo = 1;
@@ -515,6 +525,10 @@ p->time3 += clock() - clk;
 //    if ( pOld->fFailTfo || pNew->fFailTfo )
 //        printf( "*" );
 //    printf( "u(%d)", pNew->Level );
+
+    if ( fSwitch )
+         printf( "u(%d)", pNew->Level );
+
     return 1;
 }
 
-- 
cgit v1.2.3