summaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
Diffstat
-rw-r--r--src/base/main/mainFrame.c4
-rw-r--r--src/base/main/mainInt.h2
-rw-r--r--src/base/wlc/wlcAbc.c151
-rw-r--r--src/base/wlc/wlcCom.c338
-rw-r--r--src/proof/pdr/pdrCore.c4
-rw-r--r--src/proof/pdr/pdrInv.c228
-rw-r--r--src/proof/pdr/pdrUtil.c2
7 files changed, 625 insertions, 104 deletions
diff --git a/src/base/main/mainFrame.c b/src/base/main/mainFrame.c
index 05cb09c1..9647d020 100644
--- a/src/base/main/mainFrame.c
+++ b/src/base/main/mainFrame.c
@@ -95,8 +95,6 @@ void Abc_FrameSetStatus( int Status ) { ABC_FREE( s_Globa
void Abc_FrameSetManDsd( void * pMan ) { if (s_GlobalFrame->pManDsd && s_GlobalFrame->pManDsd != pMan) If_DsdManFree((If_DsdMan_t *)s_GlobalFrame->pManDsd, 0); s_GlobalFrame->pManDsd = pMan; }
void Abc_FrameSetManDsd2( void * pMan ) { if (s_GlobalFrame->pManDsd2 && s_GlobalFrame->pManDsd2 != pMan) If_DsdManFree((If_DsdMan_t *)s_GlobalFrame->pManDsd2, 0); s_GlobalFrame->pManDsd2 = pMan; }
void Abc_FrameSetInv( Vec_Int_t * vInv ) { Vec_IntFreeP(&s_GlobalFrame->pAbcWlcInv); s_GlobalFrame->pAbcWlcInv = vInv; }
-void Abc_FrameSetCnf( Vec_Int_t * vCnf ) { Vec_IntFreeP(&s_GlobalFrame->pAbcWlcCnf); s_GlobalFrame->pAbcWlcCnf = vCnf; }
-void Abc_FrameSetStr( Vec_Str_t * vStr ) { Vec_StrFreeP(&s_GlobalFrame->pAbcWlcStr); s_GlobalFrame->pAbcWlcStr = vStr; }
void Abc_FrameSetJsonStrs( Abc_Nam_t * pStrs ) { Abc_NamDeref( s_GlobalFrame->pJsonStrs ); s_GlobalFrame->pJsonStrs = pStrs; }
void Abc_FrameSetJsonObjs( Vec_Wec_t * vObjs ) { Vec_WecFreeP(&s_GlobalFrame->vJsonObjs ); s_GlobalFrame->vJsonObjs = vObjs; }
@@ -227,8 +225,6 @@ void Abc_FrameDeallocate( Abc_Frame_t * p )
ABC_FREE( p->pCex2 );
ABC_FREE( p->pCex );
Vec_IntFreeP( &p->pAbcWlcInv );
- Vec_IntFreeP( &p->pAbcWlcCnf );
- Vec_StrFreeP( &p->pAbcWlcStr );
Abc_NamDeref( s_GlobalFrame->pJsonStrs );
Vec_WecFreeP(&s_GlobalFrame->vJsonObjs );
ABC_FREE( p );
diff --git a/src/base/main/mainInt.h b/src/base/main/mainInt.h
index ff59b81a..278a9191 100644
--- a/src/base/main/mainInt.h
+++ b/src/base/main/mainInt.h
@@ -129,8 +129,6 @@ struct Abc_Frame_t_
void * pAbc85Delay;
void * pAbcWlc;
Vec_Int_t * pAbcWlcInv;
- Vec_Int_t * pAbcWlcCnf;
- Vec_Str_t * pAbcWlcStr;
void * pAbcBac;
void * pAbcCba;
void * pAbcPla;
diff --git a/src/base/wlc/wlcAbc.c b/src/base/wlc/wlcAbc.c
index 0bf27f7b..1a98fb71 100644
--- a/src/base/wlc/wlcAbc.c
+++ b/src/base/wlc/wlcAbc.c
@@ -42,7 +42,7 @@ ABC_NAMESPACE_IMPL_START
SeeAlso []
***********************************************************************/
-void Wlc_NtkPrintInvStats( Wlc_Ntk_t * pNtk, Vec_Int_t * vInv, int fVerbose )
+void Wlc_NtkPrintInvStats( Wlc_Ntk_t * pNtk, Vec_Int_t * vCounts, int fVerbose )
{
Wlc_Obj_t * pObj;
int i, k, nNum, nRange, nBits = 0;
@@ -53,7 +53,7 @@ void Wlc_NtkPrintInvStats( Wlc_Ntk_t * pNtk, Vec_Int_t * vInv, int fVerbose )
nRange = Wlc_ObjRange(pObj);
for ( k = 0; k < nRange; k++ )
{
- nNum = Vec_IntEntry(vInv, nBits + k);
+ nNum = Vec_IntEntry(vCounts, nBits + k);
if ( nNum )
break;
}
@@ -65,7 +65,7 @@ void Wlc_NtkPrintInvStats( Wlc_Ntk_t * pNtk, Vec_Int_t * vInv, int fVerbose )
printf( "%s[%d:%d] : ", Wlc_ObjName(pNtk, Wlc_ObjId(pNtk, pObj)), pObj->End, pObj->Beg );
for ( k = 0; k < nRange; k++ )
{
- nNum = Vec_IntEntry( vInv, nBits + k );
+ nNum = Vec_IntEntry( vCounts, nBits + k );
if ( nNum == 0 )
continue;
printf( " [%d] -> %d", k, nNum );
@@ -73,8 +73,8 @@ void Wlc_NtkPrintInvStats( Wlc_Ntk_t * pNtk, Vec_Int_t * vInv, int fVerbose )
printf( "\n");
nBits += nRange;
}
- //printf( "%d %d\n", Vec_IntSize(vInv), nBits );
- assert( Vec_IntSize(vInv) == nBits );
+ //printf( "%d %d\n", Vec_IntSize(vCounts), nBits );
+ assert( Vec_IntSize(vCounts) == nBits );
}
/**Function*************************************************************
@@ -88,8 +88,14 @@ void Wlc_NtkPrintInvStats( Wlc_Ntk_t * pNtk, Vec_Int_t * vInv, int fVerbose )
SeeAlso []
***********************************************************************/
-Abc_Ntk_t * Wlc_NtkGetInv( Wlc_Ntk_t * pNtk, Vec_Int_t * vInv, Vec_Str_t * vSop, int fVerbose )
+Abc_Ntk_t * Wlc_NtkGetInv( Wlc_Ntk_t * pNtk, Vec_Int_t * vInv )
{
+ extern Vec_Int_t * Pdr_InvCounts( Vec_Int_t * vInv );
+ extern Vec_Str_t * Pdr_InvPrintStr( Vec_Int_t * vInv, Vec_Int_t * vCounts );
+
+ Vec_Int_t * vCounts = Pdr_InvCounts( vInv );
+ Vec_Str_t * vSop = Pdr_InvPrintStr( vInv, vCounts );
+
Wlc_Obj_t * pObj;
int i, k, nNum, nRange, nBits = 0;
Abc_Ntk_t * pMainNtk = NULL;
@@ -98,46 +104,69 @@ Abc_Ntk_t * Wlc_NtkGetInv( Wlc_Ntk_t * pNtk, Vec_Int_t * vInv, Vec_Str_t * vSop,
// start the network
pMainNtk = Abc_NtkAlloc( ABC_NTK_LOGIC, ABC_FUNC_SOP, 1 );
// duplicate the name and the spec
- pMainNtk->pName = Extra_UtilStrsav(pNtk->pName);
+ pMainNtk->pName = Extra_UtilStrsav(pNtk ? pNtk->pName : "inv");
// create primary inputs
- Wlc_NtkForEachCi( pNtk, pObj, i )
+ if ( pNtk == NULL )
{
- if ( pObj->Type != WLC_OBJ_FO )
- continue;
- nRange = Wlc_ObjRange(pObj);
- for ( k = 0; k < nRange; k++ )
+ int Entry, nInputs = Abc_SopGetVarNum( Vec_StrArray(vSop) );
+ Vec_IntForEachEntry( vCounts, Entry, i )
{
- nNum = Vec_IntEntry(vInv, nBits + k);
- if ( nNum )
- break;
+ if ( Entry == 0 )
+ continue;
+ pMainObj = Abc_NtkCreatePi( pMainNtk );
+ sprintf( Buffer, "pi%d", i );
+ Abc_ObjAssignName( pMainObj, Buffer, NULL );
}
- if ( k == nRange )
+ if ( Abc_NtkPiNum(pMainNtk) != nInputs )
{
- nBits += nRange;
- continue;
+ printf( "Mismatch between number of inputs and the number of literals in the invariant.\n" );
+ Abc_NtkDelete( pMainNtk );
+ return NULL;
}
- //printf( "%s[%d:%d] : ", Wlc_ObjName(pNtk, Wlc_ObjId(pNtk, pObj)), pObj->End, pObj->Beg );
- for ( k = 0; k < nRange; k++ )
+ }
+ else
+ {
+ Wlc_NtkForEachCi( pNtk, pObj, i )
{
- nNum = Vec_IntEntry( vInv, nBits + k );
- if ( nNum == 0 )
+ if ( pObj->Type != WLC_OBJ_FO )
continue;
- //printf( " [%d] -> %d", k, nNum );
- pMainObj = Abc_NtkCreatePi( pMainNtk );
- sprintf( Buffer, "%s[%d]", Wlc_ObjName(pNtk, Wlc_ObjId(pNtk, pObj)), k );
- Abc_ObjAssignName( pMainObj, Buffer, NULL );
-
+ nRange = Wlc_ObjRange(pObj);
+ for ( k = 0; k < nRange; k++ )
+ {
+ nNum = Vec_IntEntry(vCounts, nBits + k);
+ if ( nNum )
+ break;
+ }
+ if ( k == nRange )
+ {
+ nBits += nRange;
+ continue;
+ }
+ //printf( "%s[%d:%d] : ", Wlc_ObjName(pNtk, Wlc_ObjId(pNtk, pObj)), pObj->End, pObj->Beg );
+ for ( k = 0; k < nRange; k++ )
+ {
+ nNum = Vec_IntEntry( vCounts, nBits + k );
+ if ( nNum == 0 )
+ continue;
+ //printf( " [%d] -> %d", k, nNum );
+ pMainObj = Abc_NtkCreatePi( pMainNtk );
+ sprintf( Buffer, "%s[%d]", Wlc_ObjName(pNtk, Wlc_ObjId(pNtk, pObj)), k );
+ Abc_ObjAssignName( pMainObj, Buffer, NULL );
+
+ }
+ //printf( "\n");
+ nBits += nRange;
}
- //printf( "\n");
- nBits += nRange;
}
- //printf( "%d %d\n", Vec_IntSize(vInv), nBits );
- assert( Vec_IntSize(vInv) == nBits );
+ //printf( "%d %d\n", Vec_IntSize(vCounts), nBits );
+ assert( pNtk == NULL || Vec_IntSize(vCounts) == nBits );
// create node
pMainObj = Abc_NtkCreateNode( pMainNtk );
Abc_NtkForEachPi( pMainNtk, pMainTemp, i )
Abc_ObjAddFanin( pMainObj, pMainTemp );
pMainObj->pData = Abc_SopRegister( (Mem_Flex_t *)pMainNtk->pManFunc, Vec_StrArray(vSop) );
+ Vec_IntFree( vCounts );
+ Vec_StrFree( vSop );
// create PO
pMainTemp = Abc_NtkCreatePo( pMainNtk );
Abc_ObjAddFanin( pMainTemp, pMainObj );
@@ -145,6 +174,66 @@ Abc_Ntk_t * Wlc_NtkGetInv( Wlc_Ntk_t * pNtk, Vec_Int_t * vInv, Vec_Str_t * vSop,
return pMainNtk;
}
+/**Function*************************************************************
+
+ Synopsis [Translate current network into an interpolant.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Vec_Int_t * Wlc_NtkGetPut( Abc_Ntk_t * pNtk, int nRegs )
+{
+ Vec_Int_t * vRes = NULL;
+ if ( Abc_NtkPoNum(pNtk) != 1 )
+ printf( "The number of outputs is other than 1.\n" );
+ else if ( Abc_NtkNodeNum(pNtk) != 1 )
+ printf( "The number of internal nodes is other than 1.\n" );
+ else
+ {
+ Abc_Obj_t * pNode = Abc_ObjFanin0( Abc_NtkCo(pNtk, 0) );
+ char * pName, * pCube, * pSop = (char *)pNode->pData;
+ Vec_Int_t * vFanins = Vec_IntAlloc( Abc_ObjFaninNum(pNode) );
+ Abc_Obj_t * pFanin; int i, k, Value, nLits;
+ Abc_ObjForEachFanin( pNode, pFanin, i )
+ {
+ assert( Abc_ObjIsCi(pFanin) );
+ pName = Abc_ObjName(pFanin);
+ for ( k = (int)strlen(pName)-1; k >= 0; k-- )
+ if ( pName[k] < '0' || pName[k] > '9' )
+ break;
+ if ( k == (int)strlen(pName)-1 )
+ {
+ printf( "Cannot read input name of fanin %d.\n", i );
+ Value = i;
+ }
+ else
+ Value = atoi(pName + k + 1);
+ Vec_IntPush( vFanins, Value );
+ }
+ assert( Vec_IntSize(vFanins) == Abc_ObjFaninNum(pNode) );
+ vRes = Vec_IntAlloc( 1000 );
+ Vec_IntPush( vRes, Abc_SopGetCubeNum(pSop) );
+ Abc_SopForEachCube( pSop, Abc_ObjFaninNum(pNode), pCube )
+ {
+ nLits = 0;
+ Abc_CubeForEachVar( pCube, Value, k )
+ if ( Value != '-' )
+ nLits++;
+ Vec_IntPush( vRes, nLits );
+ Abc_CubeForEachVar( pCube, Value, k )
+ if ( Value != '-' )
+ Vec_IntPush( vRes, Abc_Var2Lit(Vec_IntEntry(vFanins, k), (int)Value == '0') );
+ }
+ Vec_IntPush( vRes, nRegs );
+ Vec_IntFree( vFanins );
+ }
+ return vRes;
+}
+
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
diff --git a/src/base/wlc/wlcCom.c b/src/base/wlc/wlcCom.c
index f3eb6dd7..93614938 100644
--- a/src/base/wlc/wlcCom.c
+++ b/src/base/wlc/wlcCom.c
@@ -32,18 +32,21 @@ static int Abc_CommandReadWlc ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandWriteWlc ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandPs ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandBlast ( Abc_Frame_t * pAbc, int argc, char ** argv );
-static int Abc_CommandPsInv ( Abc_Frame_t * pAbc, int argc, char ** argv );
-static int Abc_CommandGetInv ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandProfile ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandTest ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandInvPs ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandInvPrint ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandInvCheck ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandInvGet ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandInvPut ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandInvMin ( Abc_Frame_t * pAbc, int argc, char ** argv );
+
static inline Wlc_Ntk_t * Wlc_AbcGetNtk( Abc_Frame_t * pAbc ) { return (Wlc_Ntk_t *)pAbc->pAbcWlc; }
static inline void Wlc_AbcFreeNtk( Abc_Frame_t * pAbc ) { if ( pAbc->pAbcWlc ) Wlc_NtkFree(Wlc_AbcGetNtk(pAbc)); }
static inline void Wlc_AbcUpdateNtk( Abc_Frame_t * pAbc, Wlc_Ntk_t * pNtk ) { Wlc_AbcFreeNtk(pAbc); pAbc->pAbcWlc = pNtk; }
static inline Vec_Int_t * Wlc_AbcGetInv( Abc_Frame_t * pAbc ) { return pAbc->pAbcWlcInv; }
-static inline Vec_Int_t * Wlc_AbcGetCnf( Abc_Frame_t * pAbc ) { return pAbc->pAbcWlcCnf; }
-static inline Vec_Str_t * Wlc_AbcGetStr( Abc_Frame_t * pAbc ) { return pAbc->pAbcWlcStr; }
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS ///
@@ -66,10 +69,15 @@ void Wlc_Init( Abc_Frame_t * pAbc )
Cmd_CommandAdd( pAbc, "Word level", "%write", Abc_CommandWriteWlc, 0 );
Cmd_CommandAdd( pAbc, "Word level", "%ps", Abc_CommandPs, 0 );
Cmd_CommandAdd( pAbc, "Word level", "%blast", Abc_CommandBlast, 0 );
- Cmd_CommandAdd( pAbc, "Word level", "%psinv", Abc_CommandPsInv, 0 );
- Cmd_CommandAdd( pAbc, "Word level", "%getinv", Abc_CommandGetInv, 0 );
Cmd_CommandAdd( pAbc, "Word level", "%profile", Abc_CommandProfile, 0 );
Cmd_CommandAdd( pAbc, "Word level", "%test", Abc_CommandTest, 0 );
+
+ Cmd_CommandAdd( pAbc, "Word level", "inv_ps", Abc_CommandInvPs, 0 );
+ Cmd_CommandAdd( pAbc, "Word level", "inv_print", Abc_CommandInvPrint, 0 );
+ Cmd_CommandAdd( pAbc, "Word level", "inv_check", Abc_CommandInvCheck, 0 );
+ Cmd_CommandAdd( pAbc, "Word level", "inv_get", Abc_CommandInvGet, 0 );
+ Cmd_CommandAdd( pAbc, "Word level", "inv_put", Abc_CommandInvPut, 0 );
+ Cmd_CommandAdd( pAbc, "Word level", "inv_min", Abc_CommandInvMin, 0 );
}
/**Function********************************************************************
@@ -440,10 +448,108 @@ usage:
SeeAlso []
******************************************************************************/
-int Abc_CommandPsInv( Abc_Frame_t * pAbc, int argc, char ** argv )
+int Abc_CommandProfile( Abc_Frame_t * pAbc, int argc, char ** argv )
{
+ Wlc_Ntk_t * pNtk = Wlc_AbcGetNtk(pAbc);
+ int c, fVerbose = 0;
+ Extra_UtilGetoptReset();
+ while ( ( c = Extra_UtilGetopt( argc, argv, "vh" ) ) != EOF )
+ {
+ switch ( c )
+ {
+ case 'v':
+ fVerbose ^= 1;
+ break;
+ case 'h':
+ goto usage;
+ default:
+ goto usage;
+ }
+ }
+ if ( pNtk == NULL )
+ {
+ Abc_Print( 1, "Abc_CommandProfile(): There is no current design.\n" );
+ return 0;
+ }
+ Wlc_WinProfileArith( pNtk );
+ return 0;
+usage:
+ Abc_Print( -2, "usage: %%profile [-vh]\n" );
+ Abc_Print( -2, "\t profiles arithmetic components in the word-level networks\n" );
+ Abc_Print( -2, "\t-v : toggle printing verbose information [default = %s]\n", fVerbose? "yes": "no" );
+ Abc_Print( -2, "\t-h : print the command usage\n");
+ return 1;
+}
+
+/**Function********************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+******************************************************************************/
+int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv )
+{
+ extern void Wlc_NtkSimulateTest( Wlc_Ntk_t * p );
+ Wlc_Ntk_t * pNtk = Wlc_AbcGetNtk(pAbc);
+ int c, fVerbose = 0;
+ Extra_UtilGetoptReset();
+ while ( ( c = Extra_UtilGetopt( argc, argv, "vh" ) ) != EOF )
+ {
+ switch ( c )
+ {
+ case 'v':
+ fVerbose ^= 1;
+ break;
+ case 'h':
+ goto usage;
+ default:
+ goto usage;
+ }
+ }
+ if ( pNtk == NULL )
+ {
+ Abc_Print( 1, "Abc_CommandTest(): There is no current design.\n" );
+ return 0;
+ }
+ // transform
+ //pNtk = Wlc_NtkUifNodePairs( pNtk, NULL );
+ //pNtk = Wlc_NtkAbstractNodes( pNtk, NULL );
+ //Wlc_AbcUpdateNtk( pAbc, pNtk );
+ //Wlc_GenerateSmtStdout( pAbc );
+ //Wlc_NtkSimulateTest( (Wlc_Ntk_t *)pAbc->pAbcWlc );
+ pNtk = Wlc_NtkDupSingleNodes( pNtk );
+ Wlc_AbcUpdateNtk( pAbc, pNtk );
+ return 0;
+usage:
+ Abc_Print( -2, "usage: %%test [-vh]\n" );
+ Abc_Print( -2, "\t experiments with word-level networks\n" );
+ Abc_Print( -2, "\t-v : toggle printing verbose information [default = %s]\n", fVerbose? "yes": "no" );
+ Abc_Print( -2, "\t-h : print the command usage\n");
+ return 1;
+}
+
+/**Function********************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+******************************************************************************/
+int Abc_CommandInvPs( Abc_Frame_t * pAbc, int argc, char ** argv )
+{
+ extern Vec_Int_t * Pdr_InvCounts( Vec_Int_t * vInv );
extern void Wlc_NtkPrintInvStats( Wlc_Ntk_t * pNtk, Vec_Int_t * vInv, int fVerbose );
Wlc_Ntk_t * pNtk = Wlc_AbcGetNtk(pAbc);
+ Vec_Int_t * vCounts;
int c, fVerbose = 0;
Extra_UtilGetoptReset();
while ( ( c = Extra_UtilGetopt( argc, argv, "vh" ) ) != EOF )
@@ -461,24 +567,66 @@ int Abc_CommandPsInv( Abc_Frame_t * pAbc, int argc, char ** argv )
}
if ( pNtk == NULL )
{
- Abc_Print( 1, "Abc_CommandPsInv(): There is no current design.\n" );
+ Abc_Print( 1, "Abc_CommandInvPs(): There is no current design.\n" );
return 0;
}
- if ( Wlc_AbcGetNtk(pAbc) == NULL )
+ if ( Wlc_AbcGetInv(pAbc) == NULL )
{
- Abc_Print( 1, "Abc_CommandPsInv(): There is no saved invariant.\n" );
+ Abc_Print( 1, "Abc_CommandInvPs(): Invariant is not available.\n" );
return 0;
}
+ vCounts = Pdr_InvCounts( Wlc_AbcGetInv(pAbc) );
+ Wlc_NtkPrintInvStats( pNtk, vCounts, fVerbose );
+ Vec_IntFree( vCounts );
+ return 0;
+usage:
+ Abc_Print( -2, "usage: inv_ps [-vh]\n" );
+ Abc_Print( -2, "\t prints statistics for inductive invariant\n" );
+ Abc_Print( -2, "\t (in the case of \'sat\' or \'undecided\', inifity clauses are used)\n" );
+ Abc_Print( -2, "\t-v : toggle printing verbose information [default = %s]\n", fVerbose? "yes": "no" );
+ Abc_Print( -2, "\t-h : print the command usage\n");
+ return 1;
+}
+
+/**Function********************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+******************************************************************************/
+int Abc_CommandInvPrint( Abc_Frame_t * pAbc, int argc, char ** argv )
+{
+ extern void Pdr_InvPrint( Vec_Int_t * vInv );
+ int c, fVerbose = 0;
+ Extra_UtilGetoptReset();
+ while ( ( c = Extra_UtilGetopt( argc, argv, "vh" ) ) != EOF )
+ {
+ switch ( c )
+ {
+ case 'v':
+ fVerbose ^= 1;
+ break;
+ case 'h':
+ goto usage;
+ default:
+ goto usage;
+ }
+ }
if ( Wlc_AbcGetInv(pAbc) == NULL )
{
- Abc_Print( 1, "Abc_CommandPsInv(): Invariant is not available.\n" );
+ Abc_Print( 1, "Abc_CommandInvPs(): Invariant is not available.\n" );
return 0;
}
- Wlc_NtkPrintInvStats( pNtk, Wlc_AbcGetInv(pAbc), fVerbose );
+ Pdr_InvPrint( Wlc_AbcGetInv(pAbc) );
return 0;
- usage:
- Abc_Print( -2, "usage: %%psinv [-vh]\n" );
- Abc_Print( -2, "\t prints statistics for inductive invariant\n" );
+usage:
+ Abc_Print( -2, "usage: inv_print [-vh]\n" );
+ Abc_Print( -2, "\t prints the current inductive invariant\n" );
Abc_Print( -2, "\t (in the case of \'sat\' or \'undecided\', inifity clauses are used)\n" );
Abc_Print( -2, "\t-v : toggle printing verbose information [default = %s]\n", fVerbose? "yes": "no" );
Abc_Print( -2, "\t-h : print the command usage\n");
@@ -496,11 +644,9 @@ int Abc_CommandPsInv( Abc_Frame_t * pAbc, int argc, char ** argv )
SeeAlso []
******************************************************************************/
-int Abc_CommandGetInv( Abc_Frame_t * pAbc, int argc, char ** argv )
+int Abc_CommandInvCheck( Abc_Frame_t * pAbc, int argc, char ** argv )
{
- extern Abc_Ntk_t * Wlc_NtkGetInv( Wlc_Ntk_t * pNtk, Vec_Int_t * vInv, Vec_Str_t * vSop, int fVerbose );
- Abc_Ntk_t * pMainNtk;
- Wlc_Ntk_t * pNtk = Wlc_AbcGetNtk(pAbc);
+ extern Vec_Int_t * Pdr_InvCheck( Gia_Man_t * p, Vec_Int_t * vInv );
int c, fVerbose = 0;
Extra_UtilGetoptReset();
while ( ( c = Extra_UtilGetopt( argc, argv, "vh" ) ) != EOF )
@@ -516,28 +662,76 @@ int Abc_CommandGetInv( Abc_Frame_t * pAbc, int argc, char ** argv )
goto usage;
}
}
- if ( pNtk == NULL )
+ if ( pAbc->pGia == NULL )
+ {
+ Abc_Print( 1, "Abc_CommandInvMin(): There is no current design.\n" );
+ return 0;
+ }
+ if ( Wlc_AbcGetInv(pAbc) == NULL )
{
- Abc_Print( 1, "Abc_CommandGetInv(): There is no current design.\n" );
+ Abc_Print( 1, "Abc_CommandInvMin(): There is no saved invariant.\n" );
return 0;
}
- if ( Wlc_AbcGetNtk(pAbc) == NULL )
+ if ( Gia_ManRegNum(pAbc->pGia) != Vec_IntEntryLast(Wlc_AbcGetInv(pAbc)) )
{
- Abc_Print( 1, "Abc_CommandGetInv(): There is no saved invariant.\n" );
+ Abc_Print( 1, "Abc_CommandInvMin(): The number of flops in the invariant and in GIA should be the same.\n" );
return 0;
}
+ Pdr_InvCheck( pAbc->pGia, Wlc_AbcGetInv(pAbc) );
+ return 0;
+usage:
+ Abc_Print( -2, "usage: inv_check [-vh]\n" );
+ Abc_Print( -2, "\t checks that the invariant is indeed an inductive invariant\n" );
+ Abc_Print( -2, "\t (AIG representing the design should be in the &-space)\n" );
+ Abc_Print( -2, "\t-v : toggle printing verbose information [default = %s]\n", fVerbose? "yes": "no" );
+ Abc_Print( -2, "\t-h : print the command usage\n");
+ return 1;
+}
+
+/**Function********************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+******************************************************************************/
+int Abc_CommandInvGet( Abc_Frame_t * pAbc, int argc, char ** argv )
+{
+ extern Abc_Ntk_t * Wlc_NtkGetInv( Wlc_Ntk_t * pNtk, Vec_Int_t * vInv );
+ Abc_Ntk_t * pMainNtk;
+ Wlc_Ntk_t * pNtk = Wlc_AbcGetNtk(pAbc);
+ int c, fVerbose = 0;
+ Extra_UtilGetoptReset();
+ while ( ( c = Extra_UtilGetopt( argc, argv, "vh" ) ) != EOF )
+ {
+ switch ( c )
+ {
+ case 'v':
+ fVerbose ^= 1;
+ break;
+ case 'h':
+ goto usage;
+ default:
+ goto usage;
+ }
+ }
if ( Wlc_AbcGetInv(pAbc) == NULL )
{
- Abc_Print( 1, "Abc_CommandGetInv(): Invariant is not available.\n" );
+ Abc_Print( 1, "Abc_CommandInvGet(): Invariant is not available.\n" );
return 0;
}
// derive the network
- pMainNtk = Wlc_NtkGetInv( pNtk, Wlc_AbcGetInv(pAbc), Wlc_AbcGetStr(pAbc), fVerbose );
+ pMainNtk = Wlc_NtkGetInv( pNtk, Wlc_AbcGetInv(pAbc) );
// replace the current network
- Abc_FrameReplaceCurrentNetwork( pAbc, pMainNtk );
+ if ( pMainNtk )
+ Abc_FrameReplaceCurrentNetwork( pAbc, pMainNtk );
return 0;
- usage:
- Abc_Print( -2, "usage: %%getinv [-vh]\n" );
+usage:
+ Abc_Print( -2, "usage: inv_get [-vh]\n" );
Abc_Print( -2, "\t places invariant found by PDR as the current network in the main-space\n" );
Abc_Print( -2, "\t (in the case of \'sat\' or \'undecided\', inifity clauses are used)\n" );
Abc_Print( -2, "\t-v : toggle printing verbose information [default = %s]\n", fVerbose? "yes": "no" );
@@ -556,34 +750,45 @@ int Abc_CommandGetInv( Abc_Frame_t * pAbc, int argc, char ** argv )
SeeAlso []
******************************************************************************/
-int Abc_CommandProfile( Abc_Frame_t * pAbc, int argc, char ** argv )
+int Abc_CommandInvPut( Abc_Frame_t * pAbc, int argc, char ** argv )
{
- Wlc_Ntk_t * pNtk = Wlc_AbcGetNtk(pAbc);
+ extern Vec_Int_t * Wlc_NtkGetPut( Abc_Ntk_t * pNtk, int nRegs );
+ Vec_Int_t * vInv = NULL;
+ Abc_Ntk_t * pNtk = Abc_FrameReadNtk(pAbc);
int c, fVerbose = 0;
Extra_UtilGetoptReset();
while ( ( c = Extra_UtilGetopt( argc, argv, "vh" ) ) != EOF )
{
switch ( c )
{
- case 'v':
- fVerbose ^= 1;
- break;
- case 'h':
- goto usage;
- default:
- goto usage;
+ case 'v':
+ fVerbose ^= 1;
+ break;
+ case 'h':
+ goto usage;
+ default:
+ goto usage;
}
}
if ( pNtk == NULL )
{
- Abc_Print( 1, "Abc_CommandProfile(): There is no current design.\n" );
+ Abc_Print( 1, "Abc_CommandInvPut(): There is no current design.\n" );
return 0;
}
- Wlc_WinProfileArith( pNtk );
+ if ( pAbc->pGia == NULL )
+ {
+ Abc_Print( 1, "Abc_CommandInvPut(): There is no current AIG.\n" );
+ return 0;
+ }
+ // derive the network
+ vInv = Wlc_NtkGetPut( pNtk, Gia_ManRegNum(pAbc->pGia) );
+ if ( vInv )
+ Abc_FrameSetInv( vInv );
return 0;
usage:
- Abc_Print( -2, "usage: %%profile [-vh]\n" );
- Abc_Print( -2, "\t profiles arithmetic components in the word-level networks\n" );
+ Abc_Print( -2, "usage: inv_put [-vh]\n" );
+ Abc_Print( -2, "\t inputs the current network in the main-space as an invariant\n" );
+ Abc_Print( -2, "\t (AIG representing the design should be in the &-space)\n" );
Abc_Print( -2, "\t-v : toggle printing verbose information [default = %s]\n", fVerbose? "yes": "no" );
Abc_Print( -2, "\t-h : print the command usage\n");
return 1;
@@ -600,42 +805,49 @@ usage:
SeeAlso []
******************************************************************************/
-int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv )
+int Abc_CommandInvMin( Abc_Frame_t * pAbc, int argc, char ** argv )
{
- extern void Wlc_NtkSimulateTest( Wlc_Ntk_t * p );
- Wlc_Ntk_t * pNtk = Wlc_AbcGetNtk(pAbc);
+ extern Vec_Int_t * Pdr_InvMinimize( Gia_Man_t * p, Vec_Int_t * vInv );
+ Vec_Int_t * vInv, * vInv2;
int c, fVerbose = 0;
Extra_UtilGetoptReset();
while ( ( c = Extra_UtilGetopt( argc, argv, "vh" ) ) != EOF )
{
switch ( c )
{
- case 'v':
- fVerbose ^= 1;
- break;
- case 'h':
- goto usage;
- default:
- goto usage;
+ case 'v':
+ fVerbose ^= 1;
+ break;
+ case 'h':
+ goto usage;
+ default:
+ goto usage;
}
}
- if ( pNtk == NULL )
+ if ( pAbc->pGia == NULL )
{
- Abc_Print( 1, "Abc_CommandTest(): There is no current design.\n" );
+ Abc_Print( 1, "Abc_CommandInvMin(): There is no current design.\n" );
return 0;
}
- // transform
- //pNtk = Wlc_NtkUifNodePairs( pNtk, NULL );
- //pNtk = Wlc_NtkAbstractNodes( pNtk, NULL );
- //Wlc_AbcUpdateNtk( pAbc, pNtk );
- //Wlc_GenerateSmtStdout( pAbc );
- //Wlc_NtkSimulateTest( (Wlc_Ntk_t *)pAbc->pAbcWlc );
- pNtk = Wlc_NtkDupSingleNodes( pNtk );
- Wlc_AbcUpdateNtk( pAbc, pNtk );
+ if ( Wlc_AbcGetInv(pAbc) == NULL )
+ {
+ Abc_Print( 1, "Abc_CommandInvMin(): Invariant is not available.\n" );
+ return 0;
+ }
+ vInv = Wlc_AbcGetInv(pAbc);
+ if ( Gia_ManRegNum(pAbc->pGia) != Vec_IntEntryLast(vInv) )
+ {
+ Abc_Print( 1, "Abc_CommandInvMin(): The number of flops in the invariant and in GIA should be the same.\n" );
+ return 0;
+ }
+ vInv2 = Pdr_InvMinimize( pAbc->pGia, vInv );
+ if ( vInv2 )
+ Abc_FrameSetInv( vInv2 );
return 0;
usage:
- Abc_Print( -2, "usage: %%test [-vh]\n" );
- Abc_Print( -2, "\t experiments with word-level networks\n" );
+ Abc_Print( -2, "usage: inv_min [-vh]\n" );
+ Abc_Print( -2, "\t minimizes the number of clauses in the current invariant\n" );
+ Abc_Print( -2, "\t (AIG representing the design should be in the &-space)\n" );
Abc_Print( -2, "\t-v : toggle printing verbose information [default = %s]\n", fVerbose? "yes": "no" );
Abc_Print( -2, "\t-h : print the command usage\n");
return 1;
diff --git a/src/proof/pdr/pdrCore.c b/src/proof/pdr/pdrCore.c
index 66cae36e..c625e366 100644
--- a/src/proof/pdr/pdrCore.c
+++ b/src/proof/pdr/pdrCore.c
@@ -923,9 +923,7 @@ int Pdr_ManSolve( Aig_Man_t * pAig, Pdr_Par_t * pPars )
if ( p->pPars->fDumpInv )
{
char * pFileName = Extra_FileNameGenericAppend(p->pAig->pName, "_inv.pla");
- Abc_FrameSetCnf( Pdr_ManDeriveInfinityClauses( p, RetValue!=1 ) );
- Abc_FrameSetStr( Pdr_ManDumpString(p) );
- Abc_FrameSetInv( Pdr_ManCountFlopsInv(p) );
+ Abc_FrameSetInv( Pdr_ManDeriveInfinityClauses( p, RetValue!=1 ) );
Pdr_ManDumpClauses( p, pFileName, RetValue==1 );
}
p->tTotal += Abc_Clock() - clk;
diff --git a/src/proof/pdr/pdrInv.c b/src/proof/pdr/pdrInv.c
index 02b90a36..f29b792c 100644
--- a/src/proof/pdr/pdrInv.c
+++ b/src/proof/pdr/pdrInv.c
@@ -605,9 +605,237 @@ Vec_Int_t * Pdr_ManDeriveInfinityClauses( Pdr_Man_t * p, int fReduce )
//Vec_PtrFree( vCubes );
Vec_PtrFreeP( &p->vInfCubes );
p->vInfCubes = vCubes;
+ Vec_IntPush( vResult, Aig_ManRegNum(p->pAig) );
return vResult;
}
+
+
+/**Function*************************************************************
+
+ Synopsis [Remove clauses while maintaining the invariant.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+#define Pdr_ForEachCube( pList, pCut, i ) for ( i = 0, pCut = pList + 1; i < pList[0]; i++, pCut += pCut[0] + 1 )
+
+extern Cnf_Dat_t * Mf_ManGenerateCnf( Gia_Man_t * pGia, int nLutSize, int fCnfObjIds, int fAddOrCla, int fVerbose );
+
+Vec_Int_t * Pdr_InvMap( Vec_Int_t * vCounts )
+{
+ int i, k = 0, Count;
+ Vec_Int_t * vMap = Vec_IntStart( Vec_IntSize(vCounts) );
+ Vec_IntForEachEntry( vCounts, Count, i )
+ if ( Count )
+ Vec_IntWriteEntry( vMap, i, k++ );
+ return vMap;
+}
+Vec_Int_t * Pdr_InvCounts( Vec_Int_t * vInv )
+{
+ int i, k, * pCube, * pList = Vec_IntArray(vInv);
+ Vec_Int_t * vCounts = Vec_IntStart( Vec_IntEntryLast(vInv) );
+ Pdr_ForEachCube( pList, pCube, i )
+ for ( k = 0; k < pCube[0]; k++ )
+ Vec_IntAddToEntry( vCounts, Abc_Lit2Var(pCube[k+1]), 1 );
+ return vCounts;
+}
+int Pdr_InvUsedFlopNum( Vec_Int_t * vInv )
+{
+ Vec_Int_t * vCounts = Pdr_InvCounts( vInv );
+ int nZeros = Vec_IntCountZero( vCounts );
+ Vec_IntFree( vCounts );
+ return Vec_IntEntryLast(vInv) - nZeros;
+}
+
+Vec_Str_t * Pdr_InvPrintStr( Vec_Int_t * vInv, Vec_Int_t * vCounts )
+{
+ Vec_Str_t * vStr = Vec_StrAlloc( 1000 );
+ Vec_Int_t * vMap = Pdr_InvMap( vCounts );
+ int nVars = Vec_IntSize(vCounts) - Vec_IntCountZero(vCounts);
+ int i, k, * pCube, * pList = Vec_IntArray(vInv);
+ char * pBuffer = ABC_ALLOC( char, nVars );
+ for ( i = 0; i < nVars; i++ )
+ pBuffer[i] = '-';
+ Pdr_ForEachCube( pList, pCube, i )
+ {
+ for ( k = 0; k < pCube[0]; k++ )
+ pBuffer[Vec_IntEntry(vMap, Abc_Lit2Var(pCube[k+1]))] = '0' + !Abc_LitIsCompl(pCube[k+1]);
+ for ( k = 0; k < nVars; k++ )
+ Vec_StrPush( vStr, pBuffer[k] );
+ Vec_StrPush( vStr, ' ' );
+ Vec_StrPush( vStr, '1' );
+ Vec_StrPush( vStr, '\n' );
+ for ( k = 0; k < pCube[0]; k++ )
+ pBuffer[Vec_IntEntry(vMap, Abc_Lit2Var(pCube[k+1]))] = '-';
+ }
+ Vec_StrPush( vStr, '\0' );
+ ABC_FREE( pBuffer );
+ Vec_IntFree( vMap );
+ return vStr;
+}
+void Pdr_InvPrint( Vec_Int_t * vInv )
+{
+ Vec_Int_t * vCounts = Pdr_InvCounts( vInv );
+ Vec_Str_t * vStr = Pdr_InvPrintStr( vInv, vCounts );
+ printf( "Invariant contains %d clauses with %d literals and %d flops (out of %d).\n", Vec_IntEntry(vInv, 0), Vec_IntSize(vInv)-Vec_IntEntry(vInv, 0)-2, Pdr_InvUsedFlopNum(vInv), Vec_IntEntryLast(vInv) );
+ printf( "%s", Vec_StrArray( vStr ) );
+ Vec_IntFree( vCounts );
+ Vec_StrFree( vStr );
+}
+
+void Pdr_InvCheck( Gia_Man_t * p, Vec_Int_t * vInv )
+{
+ int nBTLimit = 0;
+ int i, k, status, nFailed = 0;
+ // create SAT solver
+ Cnf_Dat_t * pCnf = Mf_ManGenerateCnf( p, 8, 0, 0, 0 );
+ sat_solver * pSat = (sat_solver *)Cnf_DataWriteIntoSolver( pCnf, 1, 0 );
+ // collect cubes
+ int * pCube, * pList = Vec_IntArray(vInv), nCubes = pList[0];
+ // create variables
+ Vec_Int_t * vLits = Vec_IntAlloc(100);
+ int nVars = Gia_ManRegNum(p);
+ int iFoVarBeg = pCnf->nVars - Gia_ManRegNum(p);
+ int iFiVarBeg = 1 + Gia_ManPoNum(p);
+ assert( Gia_ManPoNum(p) == 1 );
+ // add cubes
+ Pdr_ForEachCube( pList, pCube, i )
+ {
+ // collect literals
+ Vec_IntClear( vLits );
+ for ( k = 0; k < pCube[0]; k++ )
+ Vec_IntPush( vLits, Abc_Var2Lit(iFoVarBeg + Abc_Lit2Var(pCube[k+1]), !Abc_LitIsCompl(pCube[k+1])) );
+ // add it to the solver
+ status = sat_solver_addclause( pSat, Vec_IntArray(vLits), Vec_IntLimit(vLits) );
+ assert( status == 1 );
+ }
+ // iterate through cubes in the direct order
+ Pdr_ForEachCube( pList, pCube, i )
+ {
+ // collect cube
+ Vec_IntClear( vLits );
+ for ( k = 0; k < pCube[0]; k++ )
+ Vec_IntPush( vLits, Abc_Var2Lit(iFiVarBeg + Abc_Lit2Var(pCube[k+1]), Abc_LitIsCompl(pCube[k+1])) );
+ // check if this cube intersects with the complement of other cubes in the solver
+ // if it does not intersect, then it is redundant and can be skipped
+ status = sat_solver_solve( pSat, Vec_IntArray(vLits), Vec_IntLimit(vLits), nBTLimit, 0, 0, 0 );
+ if ( status == l_Undef ) // timeout
+ break;
+ if ( status == l_False ) // unsat -- correct
+ continue;
+ assert( status == l_True );
+ nFailed++;
+ }
+ if ( nFailed )
+ printf( "Invariant verification failed for %d clauses (out of %d).\n", nFailed, nCubes );
+ else
+ printf( "Invariant verification passes.\n" );
+ Cnf_DataFree( pCnf );
+ sat_solver_delete( pSat );
+ Vec_IntFree( vLits );
+}
+
+Vec_Int_t * Pdr_InvMinimize( Gia_Man_t * p, Vec_Int_t * vInv )
+{
+ int nBTLimit = 0;
+ int n, i, k, status, nLits, fFailed = 0, fCannot = 0, nRemoved = 0;
+ Vec_Int_t * vRes = NULL;
+ // create SAT solver
+ Cnf_Dat_t * pCnf = Mf_ManGenerateCnf( p, 8, 0, 0, 0 );
+ sat_solver * pSat = (sat_solver *)Cnf_DataWriteIntoSolver( pCnf, 1, 0 );
+ int * pCube, * pList = Vec_IntArray(vInv), nCubes = pList[0];
+ // create variables
+ Vec_Int_t * vLits = Vec_IntAlloc(100);
+ Vec_Bit_t * vRemoved = Vec_BitStart( nCubes );
+ int nVars = Gia_ManRegNum(p);
+ int iFoVarBeg = pCnf->nVars - Gia_ManRegNum(p);
+ int iFiVarBeg = 1 + Gia_ManPoNum(p);
+ int iAuxVarBeg = sat_solver_nvars(pSat);
+ assert( Gia_ManPoNum(p) == 1 );
+ // allocate auxiliary variables
+ sat_solver_setnvars( pSat, sat_solver_nvars(pSat) + nCubes );
+ // add clauses
+ Pdr_ForEachCube( pList, pCube, i )
+ {
+ // collect literals
+ Vec_IntFill( vLits, 1, Abc_Var2Lit(iAuxVarBeg + i, 1) ); // neg aux literal
+ for ( k = 0; k < pCube[0]; k++ )
+ Vec_IntPush( vLits, Abc_Var2Lit(iFoVarBeg + Abc_Lit2Var(pCube[k+1]), !Abc_LitIsCompl(pCube[k+1])) );
+ // add it to the solver
+ status = sat_solver_addclause( pSat, Vec_IntArray(vLits), Vec_IntLimit(vLits) );
+ assert( status == 1 );
+ }
+ // iterate through clauses
+ Pdr_ForEachCube( pList, pCube, i )
+ {
+ if ( Vec_BitEntry(vRemoved, i) )
+ continue;
+ // collect aux literals for remaining clauses
+ Vec_IntClear( vLits );
+ for ( k = 0; k < nCubes; k++ )
+ if ( k != i && !Vec_BitEntry(vRemoved, k) ) // skip this cube and already removed cubes
+ Vec_IntPush( vLits, Abc_Var2Lit(iAuxVarBeg + k, 0) ); // pos aux literal
+ nLits = Vec_IntSize( vLits );
+ // try removing other clauses
+ fCannot = 0;
+ Pdr_ForEachCube( pList, pCube, n )
+ {
+ if ( Vec_BitEntry(vRemoved, n) || n == i )
+ continue;
+ // collect cube
+ Vec_IntShrink( vLits, nLits );
+ for ( k = 0; k < pCube[0]; k++ )
+ Vec_IntPush( vLits, Abc_Var2Lit(iFiVarBeg + Abc_Lit2Var(pCube[k+1]), Abc_LitIsCompl(pCube[k+1])) );
+ // check if this cube intersects with the complement of other cubes in the solver
+ // if it does not intersect, then it is redundant and can be skipped
+ status = sat_solver_solve( pSat, Vec_IntArray(vLits), Vec_IntLimit(vLits), nBTLimit, 0, 0, 0 );
+ if ( status == l_Undef ) // timeout
+ {
+ fFailed = 1;
+ break;
+ }
+ if ( status == l_False ) // unsat -- correct
+ continue;
+ assert( status == l_True );
+ // cannot remove
+ fCannot = 1;
+ break;
+ }
+ if ( fFailed )
+ break;
+ if ( fCannot )
+ continue;
+ printf( "Removing clause %d.\n", i );
+ Vec_BitWriteEntry( vRemoved, i, 1 );
+ nRemoved++;
+ }
+ if ( nRemoved )
+ printf( "Invariant minimization reduced %d clauses (out of %d).\n", nRemoved, nCubes );
+ else
+ printf( "Invariant minimization did not change the invariant.\n" );
+ // cleanup cover
+ if ( !fFailed && nRemoved > 0 ) // finished without timeout and removed some cubes
+ {
+ vRes = Vec_IntAlloc( 1000 );
+ Vec_IntPush( vRes, nCubes-nRemoved );
+ Pdr_ForEachCube( pList, pCube, i )
+ if ( !Vec_BitEntry(vRemoved, i) )
+ for ( k = 0; k <= pCube[0]; k++ )
+ Vec_IntPush( vRes, pCube[k] );
+ Vec_IntPush( vRes, Vec_IntEntryLast(vInv) );
+ }
+ Cnf_DataFree( pCnf );
+ sat_solver_delete( pSat );
+ Vec_BitFree( vRemoved );
+ Vec_IntFree( vLits );
+ return vRes;
+}
+
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
diff --git a/src/proof/pdr/pdrUtil.c b/src/proof/pdr/pdrUtil.c
index 53a8a54a..32e97772 100644
--- a/src/proof/pdr/pdrUtil.c
+++ b/src/proof/pdr/pdrUtil.c
@@ -284,7 +284,7 @@ void Pdr_SetPrintStr( Vec_Str_t * vStr, Pdr_Set_t * p, int nRegs, Vec_Int_t * vF
}
Vec_StrPushBuffer( vStr, pBuff, k );
Vec_StrPush( vStr, ' ' );
- Vec_StrPush( vStr, '0' );
+ Vec_StrPush( vStr, '1' );
Vec_StrPush( vStr, '\n' );
ABC_FREE( pBuff );
}
generated by cgit v1.2.3 (git 2.25.1) at 2024-12-27 12:34:44 +0000