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

New command &satoko.

This commit is contained in:
Alan Mishchenko 2017-02-08 14:10:08 -08:00
parent 80f5070dbe
commit de4bf41c53
5 changed files with 204 additions and 4 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

4
abclib.dsp
View File

@ -4639,6 +4639,10 @@ SOURCE=.\src\aig\gia\giaSatMap.c
# End Source File
# Begin Source File
SOURCE=.\src\aig\gia\giaSatoko.c
# End Source File
# Begin Source File
SOURCE=.\src\aig\gia\giaScl.c
# End Source File
# Begin Source File

126
src/aig/gia/giaSatoko.c Normal file
View File

@ -0,0 +1,126 @@
/**CFile****************************************************************
FileName [giaSatoko.c]
SystemName [ABC: Logic synthesis and verification system.]
PackageName [Scalable AIG package.]
Synopsis [Interface to Satoko solver.]
Author [Alan Mishchenko, Bruno Schmitt]
Affiliation [UC Berkeley]
Date [Ver. 1.0. Started - June 20, 2005.]
Revision [$Id: giaSatoko.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
***********************************************************************/
#include "gia.h"
#include "sat/cnf/cnf.h"
#include "sat/satoko/satoko.h"
ABC_NAMESPACE_IMPL_START
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
extern Cnf_Dat_t * Mf_ManGenerateCnf( Gia_Man_t * pGia, int nLutSize, int fCnfObjIds, int fAddOrCla, int fVerbose );
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
satoko_t * Gia_ManCreateSatoko( Gia_Man_t * p )
{
satoko_t * pSat = satoko_create();
Cnf_Dat_t * pCnf = Mf_ManGenerateCnf( p, 8, 0, 1, 0 );
int i, status;
//sat_solver_setnvars( pSat, p->nVars );
for ( i = 0; i < pCnf->nClauses; i++ )
{
if ( !satoko_add_clause( pSat, pCnf->pClauses[i], pCnf->pClauses[i+1]-pCnf->pClauses[i] ) )
{
Cnf_DataFree( pCnf );
satoko_destroy( pSat );
return NULL;
}
}
Cnf_DataFree( pCnf );
status = satoko_simplify(pSat);
if ( status == SATOKO_OK )
return pSat;
satoko_destroy( pSat );
return NULL;
}
void Gia_ManCallSatokoOne( Gia_Man_t * p, satoko_opts_t * opts, int iOutput )
{
abctime clk = Abc_Clock();
satoko_t * pSat;
int status;
pSat = Gia_ManCreateSatoko( p );
if ( pSat )
{
satoko_configure(pSat, opts);
status = satoko_solve( pSat );
satoko_destroy( pSat );
}
else
status = SATOKO_UNSAT;
if ( iOutput >= 0 )
Abc_Print( 1, "Output %6d : ", iOutput );
else
Abc_Print( 1, "Total: " );
if ( status == SATOKO_UNDEC )
Abc_Print( 1, "UNDECIDED " );
else if ( status == SATOKO_SAT )
Abc_Print( 1, "SATISFIABLE " );
else
Abc_Print( 1, "UNSATISFIABLE " );
Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
}
void Gia_ManCallSatoko( Gia_Man_t * p, satoko_opts_t * opts, int fSplit )
{
if ( fSplit )
{
Gia_Man_t * pOne;
Gia_Obj_t * pRoot;
int i;
Gia_ManForEachCo( p, pRoot, i )
{
pOne = Gia_ManDupDfsCone( p, pRoot );
Gia_ManCallSatokoOne( pOne, opts, i );
Gia_ManStop( pOne );
}
return;
}
Gia_ManCallSatokoOne( p, opts, -1 );
}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
ABC_NAMESPACE_IMPL_END

1
src/aig/gia/module.make
View File

@ -59,6 +59,7 @@ SRC += src/aig/gia/giaAig.c \
src/aig/gia/giaSatLE.c \
src/aig/gia/giaSatLut.c \
src/aig/gia/giaSatMap.c \
src/aig/gia/giaSatoko.c \
src/aig/gia/giaScl.c \
src/aig/gia/giaScript.c \
src/aig/gia/giaShow.c \

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

@ -310,6 +310,7 @@ static int Abc_CommandSat ( Abc_Frame_t * pAbc, int argc, cha
static int Abc_CommandDSat ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandXSat ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandSatoko ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandAbc9Satoko ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandPSat ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandProve ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandIProve ( Abc_Frame_t * pAbc, int argc, char ** argv );
@ -959,6 +960,7 @@ void Abc_Init( Abc_Frame_t * pAbc )
Cmd_CommandAdd( pAbc, "Verification", "dsat", Abc_CommandDSat, 0 );
Cmd_CommandAdd( pAbc, "Verification", "xsat", Abc_CommandXSat, 0 );
Cmd_CommandAdd( pAbc, "Verification", "satoko", Abc_CommandSatoko, 0 );
Cmd_CommandAdd( pAbc, "Verification", "&satoko", Abc_CommandAbc9Satoko, 0 );
Cmd_CommandAdd( pAbc, "Verification", "psat", Abc_CommandPSat, 0 );
Cmd_CommandAdd( pAbc, "Verification", "prove", Abc_CommandProve, 1 );
Cmd_CommandAdd( pAbc, "Verification", "iprove", Abc_CommandIProve, 1 );
@ -23356,11 +23358,12 @@ int Abc_CommandSatoko( Abc_Frame_t * pAbc, int argc, char ** argv )
satoko_t * p;
int status;
satoko_parse_dimacs( pFileName, &p );
status = satoko_parse_dimacs( pFileName, &p );
satoko_configure(p, &opts);
clk = Abc_Clock();
status = satoko_solve( p );
if ( status == SATOKO_OK )
status = satoko_solve( p );
if ( status == SATOKO_UNDEC )
Abc_Print( 1, "UNDECIDED " );
@ -23382,6 +23385,72 @@ usage:
Abc_Print( -2, "\t-h : print the command usage\n");
return 1;
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Abc_CommandAbc9Satoko( Abc_Frame_t * pAbc, int argc, char ** argv )
{
extern void Gia_ManCallSatoko( Gia_Man_t * p, satoko_opts_t * opts, int fSplit );
int c, fSplit = 0;
satoko_opts_t opts;
satoko_default_opts(&opts);
Extra_UtilGetoptReset();
while ( ( c = Extra_UtilGetopt( argc, argv, "Csvh" ) ) != EOF )
{
switch ( c )
{
case 'C':
if ( globalUtilOptind >= argc )
{
Abc_Print( -1, "Command line switch \"-C\" should be followed by an integer.\n" );
goto usage;
}
opts.conf_limit = atoi(argv[globalUtilOptind]);
globalUtilOptind++;
if ( opts.conf_limit < 0 )
goto usage;
break;
case 's':
fSplit ^= 1;
break;
case 'v':
opts.verbose ^= 1;
break;
case 'h':
goto usage;
default:
goto usage;
}
}
if ( pAbc->pGia == NULL )
{
Abc_Print( -1, "Abc_CommandAbc9Satoko(): There is no AIG.\n" );
return 1;
}
Gia_ManCallSatoko( pAbc->pGia, &opts, fSplit );
return 0;
usage:
Abc_Print( -2, "usage: &satoko [-C num] [-svh]\n" );
Abc_Print( -2, "\t-C num : limit on the number of conflicts [default = %d]\n", opts.conf_limit );
Abc_Print( -2, "\t-s : split multi-output miter into individual outputs [default = %s]\n", fSplit? "yes": "no" );
Abc_Print( -2, "\t-v : prints verbose information [default = %s]\n", opts.verbose? "yes": "no" );
Abc_Print( -2, "\t-h : print the command usage\n");
return 1;
}
/**Function*************************************************************
Synopsis []

4
src/base/wlc/wlcShow.c
View File

@ -49,9 +49,9 @@ void Wlc_NtkDumpDot( Wlc_Ntk_t * p, char * pFileName, Vec_Int_t * vBold )
Wlc_Obj_t * pNode;
int LevelMax, Prev, Level, i;
if ( Wlc_NtkObjNum(p) > 1000 )
if ( Wlc_NtkObjNum(p) > 2000 )
{
fprintf( stdout, "Cannot visualize WLC with more than %d nodes.\n", 1000 );
fprintf( stdout, "Cannot visualize WLC with more than %d nodes.\n", 2000 );
return;
}
if ( (pFile = fopen( pFileName, "w" )) == NULL )