diff options
| -rw-r--r-- | abclib.dsp | 4 | ||||
| -rw-r--r-- | src/aig/gia/giaSatoko.c | 126 | ||||
| -rw-r--r-- | src/aig/gia/module.make | 1 | ||||
| -rw-r--r-- | src/base/abci/abc.c | 73 | ||||
| -rw-r--r-- | src/base/wlc/wlcShow.c | 4 |
5 files changed, 204 insertions, 4 deletions
@@ -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 diff --git a/src/aig/gia/giaSatoko.c b/src/aig/gia/giaSatoko.c new file mode 100644 index 00000000..62bc7713 --- /dev/null +++ b/src/aig/gia/giaSatoko.c @@ -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 + diff --git a/src/aig/gia/module.make b/src/aig/gia/module.make index 0066bfd2..0ddf9833 100644 --- a/src/aig/gia/module.make +++ b/src/aig/gia/module.make @@ -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 \ diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index 65974acb..1ecc5e68 100644 --- a/src/base/abci/abc.c +++ b/src/base/abci/abc.c @@ -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 [] diff --git a/src/base/wlc/wlcShow.c b/src/base/wlc/wlcShow.c index 7914cd7a..1601d602 100644 --- a/src/base/wlc/wlcShow.c +++ b/src/base/wlc/wlcShow.c @@ -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 ) |