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

Adding support for Dimacs input to &satoko.

This commit is contained in:
Alan Mishchenko 2017-09-16 13:13:30 -07:00
parent 6d2efdf28f
commit b5d42e8bf3
3 changed files with 108 additions and 30 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

112
src/aig/gia/giaSatoko.c
View File

@ -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;
}

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

@ -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;
}

6
src/sat/glucose/AbcGlucoseCmd.cpp
View File

@ -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);