diff options
Diffstat (limited to 'src')
-rw-r--r-- | src/aig/gia/giaSatoko.c | 112 | ||||
-rw-r--r-- | src/base/abci/abc.c | 20 | ||||
-rw-r--r-- | src/sat/glucose/AbcGlucoseCmd.cpp | 6 |
3 files changed, 108 insertions, 30 deletions
diff --git a/src/aig/gia/giaSatoko.c b/src/aig/gia/giaSatoko.c index aaf9daaa..dad3bcc4 100644 --- a/src/aig/gia/giaSatoko.c +++ b/src/aig/gia/giaSatoko.c @@ -20,6 +20,7 @@ #include "gia.h" #include "sat/cnf/cnf.h" +#include "misc/extra/extra.h" #include "sat/satoko/satoko.h" ABC_NAMESPACE_IMPL_START @@ -79,22 +80,6 @@ Vec_Int_t * Gia_ManCollectVars( int Root, Vec_Int_t * vMapping, int nVars ) SeeAlso [] ***********************************************************************/ -satoko_t * Gia_ManSatokoInit( Cnf_Dat_t * pCnf, satoko_opts_t * opts ) -{ - satoko_t * pSat = satoko_create(); - int i; - //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] ) ) - { - satoko_destroy( pSat ); - return NULL; - } - } - satoko_configure(pSat, opts); - return pSat; -} void Gia_ManSatokoReport( int iOutput, int status, abctime clk ) { if ( iOutput >= 0 ) @@ -111,6 +96,95 @@ void Gia_ManSatokoReport( int iOutput, int status, abctime clk ) Abc_PrintTime( 1, "Time", clk ); } +satoko_t * Gia_ManSatokoFromDimacs( char * pFileName, satoko_opts_t * opts ) +{ + satoko_t * pSat = satoko_create(); + char * pBuffer = Extra_FileReadContents( pFileName ); + Vec_Int_t * vLits = Vec_IntAlloc( 100 ); + char * pTemp; int fComp, Var, VarMax = 0; + for ( pTemp = pBuffer; *pTemp; pTemp++ ) + { + if ( *pTemp == 'c' || *pTemp == 'p' ) + { + while ( *pTemp != '\n' ) + pTemp++; + continue; + } + while ( *pTemp == ' ' || *pTemp == '\t' || *pTemp == '\r' || *pTemp == '\n' ) + pTemp++; + fComp = 0; + if ( *pTemp == '-' ) + fComp = 1, pTemp++; + if ( *pTemp == '+' ) + pTemp++; + Var = atoi( pTemp ); + if ( Var == 0 ) { + if ( Vec_IntSize(vLits) > 0 ) + { + satoko_setnvars( pSat, VarMax+1 ); + if ( !satoko_add_clause( pSat, Vec_IntArray(vLits), Vec_IntSize(vLits) ) ) + { + satoko_destroy(pSat); + Vec_IntFree( vLits ); + ABC_FREE( pBuffer ); + return NULL; + } + Vec_IntClear( vLits ); + } + } + else + { + Var--; + VarMax = Abc_MaxInt( VarMax, Var ); + Vec_IntPush( vLits, Abc_Var2Lit(Var, fComp) ); + } + while ( *pTemp >= '0' && *pTemp <= '9' ) + pTemp++; + } + ABC_FREE( pBuffer ); + Vec_IntFree( vLits ); + return pSat; +} +void Gia_ManSatokoDimacs( char * pFileName, satoko_opts_t * opts ) +{ + abctime clk = Abc_Clock(); + int status = SATOKO_UNSAT; + satoko_t * pSat = Gia_ManSatokoFromDimacs( pFileName, opts ); + if ( pSat ) + { + status = satoko_solve( pSat ); + satoko_destroy( pSat ); + } + Gia_ManSatokoReport( -1, status, Abc_Clock() - clk ); +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +satoko_t * Gia_ManSatokoInit( Cnf_Dat_t * pCnf, satoko_opts_t * opts ) +{ + satoko_t * pSat = satoko_create(); + int i; + //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] ) ) + { + satoko_destroy( pSat ); + return NULL; + } + } + satoko_configure(pSat, opts); + return pSat; +} satoko_t * Gia_ManSatokoCreate( Gia_Man_t * p, satoko_opts_t * opts ) { Cnf_Dat_t * pCnf = (Cnf_Dat_t *)Mf_ManGenerateCnf( p, 8, 0, 1, 0, 0 ); @@ -126,8 +200,7 @@ int Gia_ManSatokoCallOne( Gia_Man_t * p, satoko_opts_t * opts, int iOutput ) { abctime clk = Abc_Clock(); satoko_t * pSat; - int status, Cost = 0; - + int status = SATOKO_UNSAT, Cost = 0; pSat = Gia_ManSatokoCreate( p, opts ); if ( pSat ) { @@ -135,9 +208,6 @@ int Gia_ManSatokoCallOne( Gia_Man_t * p, satoko_opts_t * opts, int iOutput ) Cost = satoko_stats(pSat)->n_conflicts; satoko_destroy( pSat ); } - else - status = SATOKO_UNSAT; - Gia_ManSatokoReport( iOutput, status, Abc_Clock() - clk ); return Cost; } diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index 025d9963..520af9fd 100644 --- a/src/base/abci/abc.c +++ b/src/base/abci/abc.c @@ -23795,6 +23795,7 @@ usage: ***********************************************************************/ int Abc_CommandAbc9Satoko( Abc_Frame_t * pAbc, int argc, char ** argv ) { + extern void Gia_ManSatokoDimacs( char * pFileName, satoko_opts_t * opts ); extern void Gia_ManSatokoCall( Gia_Man_t * p, satoko_opts_t * opts, int fSplit, int fIncrem ); int c, fSplit = 0, fIncrem = 0; @@ -23832,6 +23833,11 @@ int Abc_CommandAbc9Satoko( Abc_Frame_t * pAbc, int argc, char ** argv ) goto usage; } } + if ( argc == globalUtilOptind + 1 ) + { + Gia_ManSatokoDimacs( argv[globalUtilOptind], &opts ); + return 0; + } if ( pAbc->pGia == NULL ) { Abc_Print( -1, "Abc_CommandAbc9Satoko(): There is no AIG.\n" ); @@ -23841,12 +23847,14 @@ int Abc_CommandAbc9Satoko( Abc_Frame_t * pAbc, int argc, char ** argv ) return 0; usage: - Abc_Print( -2, "usage: &satoko [-C num] [-sivh]\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-i : split multi-output miter and solve incrementally [default = %s]\n", fIncrem? "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"); + Abc_Print( -2, "usage: &satoko [-C num] [-sivh] <file.cnf>\n" ); + Abc_Print( -2, "\t run Satoko by Bruno Schmitt\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-i : split multi-output miter and solve incrementally [default = %s]\n", fIncrem? "yes": "no" ); + Abc_Print( -2, "\t-v : prints verbose information [default = %s]\n", opts.verbose? "yes": "no" ); + Abc_Print( -2, "\t<file.cnf> : (optional) CNF file to solve\n"); + Abc_Print( -2, "\t-h : print the command usage\n"); return 1; } diff --git a/src/sat/glucose/AbcGlucoseCmd.cpp b/src/sat/glucose/AbcGlucoseCmd.cpp index bcff4165..74a58c33 100644 --- a/src/sat/glucose/AbcGlucoseCmd.cpp +++ b/src/sat/glucose/AbcGlucoseCmd.cpp @@ -50,7 +50,7 @@ extern "C" { void Glucose_Init(Abc_Frame_t *pAbc) { - Cmd_CommandAdd( pAbc, "ABC9", "&gluco", Abc_CommandGlucose, 0 ); + Cmd_CommandAdd( pAbc, "ABC9", "&glucose", Abc_CommandGlucose, 0 ); } void Glucose_End( Abc_Frame_t * pAbc ) @@ -127,8 +127,8 @@ int Abc_CommandGlucose( Abc_Frame_t * pAbc, int argc, char ** argv ) return 0; usage: - Abc_Print( -2, "usage: &gluco [-C num] [-pvh] <file.cnf>\n" ); - Abc_Print( -2, "\t run glucose\n" ); + Abc_Print( -2, "usage: &glucose [-C num] [-pvh] <file.cnf>\n" ); + Abc_Print( -2, "\t run Glucose 3.0 by Gilles Audemard and Laurent Simon\n" ); Abc_Print( -2, "\t-C num : conflict limit [default = %d]\n", nConfls ); Abc_Print( -2, "\t-p : enable preprocessing [default = %d]\n",pre); Abc_Print( -2, "\t-v : verbosity [default = %d]\n",verb); |