From c4446189a9ca5a187a2ede26a7102866d2c5ae8e Mon Sep 17 00:00:00 2001
From: Alan Mishchenko <alanmi@berkeley.edu>
Date: Thu, 14 Jan 2016 20:42:22 -0800
Subject: Changes to PDR to compute f-inf clauses and import invariant (or
 clauses) as a network.

---
 src/proof/pdr/pdrUtil.c | 40 ++++++++++++++++++++++++++++++++++++++++
 1 file changed, 40 insertions(+)

(limited to 'src/proof/pdr/pdrUtil.c')

diff --git a/src/proof/pdr/pdrUtil.c b/src/proof/pdr/pdrUtil.c
index 1536c1cc..53a8a54a 100644
--- a/src/proof/pdr/pdrUtil.c
+++ b/src/proof/pdr/pdrUtil.c
@@ -249,6 +249,46 @@ void Pdr_SetPrint( FILE * pFile, Pdr_Set_t * p, int nRegs, Vec_Int_t * vFlopCoun
     ABC_FREE( pBuff );
 }
 
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Pdr_SetPrintStr( Vec_Str_t * vStr, Pdr_Set_t * p, int nRegs, Vec_Int_t * vFlopCounts )
+{
+    char * pBuff;
+    int i, k = 0, Entry;
+    pBuff = ABC_ALLOC( char, nRegs + 1 );
+    for ( i = 0; i < nRegs; i++ )
+        pBuff[i] = '-';
+    pBuff[i] = 0;
+    for ( i = 0; i < p->nLits; i++ )
+    {
+        if ( p->Lits[i] == -1 )
+            continue;
+        pBuff[lit_var(p->Lits[i])] = (lit_sign(p->Lits[i])? '0':'1');
+    }
+    if ( vFlopCounts )
+    {
+        // skip some literals
+        Vec_IntForEachEntry( vFlopCounts, Entry, i )
+            if ( Entry ) 
+                pBuff[k++] = pBuff[i];
+        pBuff[k] = 0;
+    }
+    Vec_StrPushBuffer( vStr, pBuff, k );
+    Vec_StrPush( vStr, ' ' );
+    Vec_StrPush( vStr, '0' );
+    Vec_StrPush( vStr, '\n' );
+    ABC_FREE( pBuff );
+}
+
 /**Function*************************************************************
 
   Synopsis    [Return 1 if pOld set-theoretically contains pNew.]
-- 
cgit v1.2.3