luke
/
abc
mirror of https://github.com/YosysHQ/abc.git
1
0
Fork 0
Code Issues Packages Projects Releases Wiki Activity

New command &genrel to generate relations for windows in the AIG.

This commit is contained in:
Alan Mishchenko 2024-05-14 22:35:43 -07:00
parent daf3313ce6
commit 6ad6539c0f
3 changed files with 185 additions and 0 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

94
src/aig/gia/giaQbf.c
View File

@ -24,6 +24,7 @@
#include "misc/extra/extra.h"
#include "sat/glucose/AbcGlucose.h"
#include "misc/util/utilTruth.h"
#include "base/io/ioResub.h"
ABC_NAMESPACE_IMPL_START
@ -945,6 +946,99 @@ int Gia_QbfSolve( Gia_Man_t * pGia, int nPars, int nIterLimit, int nConfLimit, i
return RetValue;
}
/**Function*************************************************************
Synopsis [Performs QBF solving using an improved algorithm.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Vec_Int_t * Gia_ManGenCombs( Gia_Man_t * p, Vec_Int_t * vInsOuts, int fVerbose )
{
int nTimeOut = 600, nConfLimit = 1000000;
int i, iObj, iSatVar, Iter, Mask, nSolutions = 0, RetValue = 0;
abctime clkStart = Abc_Clock();
Gia_Man_t * pCopy = Gia_ManDup(p);
Vec_IntForEachEntry( vInsOuts, iObj, i )
Gia_ManAppendCo( pCopy, Abc_Var2Lit(iObj, 0) );
Cnf_Dat_t * pCnf = (Cnf_Dat_t *)Mf_ManGenerateCnf( pCopy, 8, 0, 0, 0, 0 );
sat_solver * pSat = (sat_solver *)Cnf_DataWriteIntoSolver( pCnf, 1, 0 );
Vec_Int_t * vLits = Vec_IntAlloc( 100 );
Vec_Int_t * vRes = Vec_IntAlloc( 1000 );
//Gia_ManForEachCoId( pCopy, iObj, i )
// printf( "%d=%d ", i, pCnf->pVarNums[iObj] );
//printf( "\n" );
Cnf_DataFree( pCnf );
for ( Iter = 0; Iter < 1000000; Iter++ )
{
int status = sat_solver_solve( pSat, NULL, NULL, (ABC_INT64_T)nConfLimit, 0, 0, 0 );
if ( status == l_False ) { RetValue = 1; break; }
if ( status == l_Undef ) { RetValue = 0; break; }
nSolutions++;
// extract SAT assignment
Mask = 0;
Vec_IntClear( vLits );
for ( i = 0; i < Vec_IntSize(vInsOuts); i++ ) {
iSatVar = i + 1+Gia_ManCoNum(p);
Vec_IntPush( vLits, Abc_Var2Lit(iSatVar, sat_solver_var_value(pSat, iSatVar)) );
if ( sat_solver_var_value(pSat, iSatVar) )
Mask |= 1 << (Vec_IntSize(vInsOuts)-1-i);
}
Vec_IntPush( vRes, Mask );
if ( fVerbose )
{
printf( "%5d : ", Iter );
for ( i = Vec_IntSize(vInsOuts)-1; i >= 0; i-- )
printf( "%d", (Mask >> i) & 1 );
printf( "\n" );
}
// add clause
if ( !sat_solver_addclause( pSat, Vec_IntArray(vLits), Vec_IntArray(vLits) + Vec_IntSize(vLits) ) )
{ RetValue = 1; break; }
if ( nTimeOut && (Abc_Clock() - clkStart)/CLOCKS_PER_SEC >= nTimeOut ) { RetValue = 0; break; }
}
Vec_IntSort( vRes, 0 );
Gia_ManStop( pCopy );
Vec_IntFree( vLits );
sat_solver_delete( pSat );
if ( RetValue == 0 )
Vec_IntFreeP( &vRes );
if ( fVerbose )
Abc_PrintTime( 1, "Time", Abc_Clock() - clkStart );
return vRes;
}
void Gia_ManGenRel( Gia_Man_t * pGia, Vec_Int_t * vInsOuts, int nIns, char * pFileName, int fVerbose )
{
Vec_Int_t * vRes = Gia_ManGenCombs( pGia, vInsOuts, fVerbose ); int i, k, Mask;
if ( vRes == NULL ) {
printf( "Enumerating solutions did not succeed.\n" );
return;
}
Abc_RData_t * p = Abc_RDataStart( nIns, Vec_IntSize(vInsOuts)-nIns, Vec_IntSize(vRes) );
Vec_IntForEachEntry( vRes, Mask, i ) {
for ( k = 0; k < Vec_IntSize(vInsOuts); k++ )
if ( (Mask >> (Vec_IntSize(vInsOuts)-1-k)) & 1 ) { // the bit is 1
if ( k < nIns )
Abc_RDataSetIn( p, k, i );
else
Abc_RDataSetOut( p, 2*(k-nIns)+1, i );
}
else { // the bit is zero
if ( k >= nIns )
Abc_RDataSetOut( p, 2*(k-nIns), i );
}
}
Abc_WritePla( p, pFileName, 0 );
Abc_RDataStop( p );
Vec_IntFree( vRes );
}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////

85
src/base/abci/abc.c
View File

@ -607,6 +607,7 @@ static int Abc_CommandAbc9BRecover ( Abc_Frame_t * pAbc, int argc, cha
static int Abc_CommandAbc9StrEco ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandAbc9GenCex ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandAbc9Odc ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandAbc9GenRel ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandAbc9Test ( Abc_Frame_t * pAbc, int argc, char ** argv );
@ -1396,6 +1397,7 @@ void Abc_Init( Abc_Frame_t * pAbc )
Cmd_CommandAdd( pAbc, "ABC9", "&str_eco", Abc_CommandAbc9StrEco, 0 );
Cmd_CommandAdd( pAbc, "ABC9", "&gencex", Abc_CommandAbc9GenCex, 0 );
Cmd_CommandAdd( pAbc, "ABC9", "&odc", Abc_CommandAbc9Odc, 0 );
Cmd_CommandAdd( pAbc, "ABC9", "&genrel", Abc_CommandAbc9GenRel, 0 );
Cmd_CommandAdd( pAbc, "ABC9", "&test", Abc_CommandAbc9Test, 0 );
{
@ -53026,6 +53028,89 @@ usage:
return 1;
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Abc_CommandAbc9GenRel( Abc_Frame_t * pAbc, int argc, char ** argv )
{
extern void Gia_ManGenRel( Gia_Man_t * pGia, Vec_Int_t * vInsOuts, int nIns, char * pFileName, int fVerbose );
Vec_Int_t * vInsOuts = NULL;
int c, nIns = -1, fVerbose = 0;
Extra_UtilGetoptReset();
while ( ( c = Extra_UtilGetopt( argc, argv, "Ivh" ) ) != EOF )
{
switch ( c )
{
case 'I':
if ( globalUtilOptind >= argc )
{
Abc_Print( -1, "Command line switch \"-N\" should be followed by an integer.\n" );
goto usage;
}
nIns = atoi(argv[globalUtilOptind]);
globalUtilOptind++;
if ( nIns < 0 )
goto usage;
break;
case 'v':
fVerbose ^= 1;
break;
case 'h':
goto usage;
default:
goto usage;
}
}
if ( pAbc->pGia == NULL )
{
Abc_Print( -1, "Abc_CommandAbc9GenRel(): There is no AIG.\n" );
return 0;
}
if ( nIns < 2 )
{
Abc_Print( -1, "Abc_CommandAbc9GenRel(): The number of inputs should be given on the command line.\n" );
return 0;
}
if ( argc == globalUtilOptind )
{
Abc_Print( -1, "Abc_CommandAbc9GenRel(): Node IDs should be given on the command line.\n" );
return 0;
}
if ( argc-globalUtilOptind-nIns-1 < 1 )
{
Abc_Print( -1, "Abc_CommandAbc9GenRel(): The relation should have at least one output.\n" );
return 0;
}
vInsOuts = Vec_IntAlloc( 100 );
for ( c = globalUtilOptind; c < argc-1; c++ )
Vec_IntPush( vInsOuts, atoi(argv[c]) );
if ( fVerbose )
{
printf( "Deriving relation for %d inputs and %d outputs: ", nIns, Vec_IntSize(vInsOuts)-nIns );
Vec_IntPrint( vInsOuts );
}
Gia_ManGenRel( pAbc->pGia, vInsOuts, nIns, argv[argc-1], fVerbose );
Vec_IntFree( vInsOuts );
return 0;
usage:
Abc_Print( -2, "usage: &genrel [-I num] [-vh] <node1> <node2> ... <nodeN> <filename>\n" );
Abc_Print( -2, "\t generates Boolean relation for the given logic window\n" );
Abc_Print( -2, "\t-I num : the number of inputs of the relation [default = undefined]\n" );
Abc_Print( -2, "\t-v : toggles printing verbose information [default = %d]\n", fVerbose ? "yes": "no" );
Abc_Print( -2, "\t-h : print the command usage\n");
Abc_Print( -2, "\t<nodes> : the list of nodes for inputs and outputs\n");
Abc_Print( -2, "\t<file> : the output file name (extended PLA format)\n");
return 1;
}
/**Function*************************************************************
Synopsis []

6
src/base/io/ioResub.h
View File

@ -52,6 +52,12 @@ struct Abc_RData_t_
/// MACRO DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
static inline int Abc_RDataGetIn ( Abc_RData_t * p, int i, int b ) { return Abc_InfoHasBit((unsigned *)Vec_WrdEntryP(p->vSimsIn, i*p->nSimWords), b); }
static inline int Abc_RDataGetOut( Abc_RData_t * p, int i, int b ) { return Abc_InfoHasBit((unsigned *)Vec_WrdEntryP(p->vSimsOut, i*p->nSimWords), b); }
static inline void Abc_RDataSetIn ( Abc_RData_t * p, int i, int b ) { Abc_InfoSetBit((unsigned *)Vec_WrdEntryP(p->vSimsIn, i*p->nSimWords), b); }
static inline void Abc_RDataSetOut( Abc_RData_t * p, int i, int b ) { Abc_InfoSetBit((unsigned *)Vec_WrdEntryP(p->vSimsOut, i*p->nSimWords), b); }
////////////////////////////////////////////////////////////////////////
/// FUNCTION DECLARATIONS ///
////////////////////////////////////////////////////////////////////////