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

Adding APIs to mark cones. Creating test-bench for incremental solving &satoko -i.

This commit is contained in:
Alan Mishchenko 2017-02-11 17:28:37 -08:00
parent 7b7ebf91e4
commit 2a5fa67d36
7 changed files with 187 additions and 46 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

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

@ -45,46 +45,59 @@ ABC_NAMESPACE_IMPL_START
SeeAlso []
***********************************************************************/
satoko_t * Gia_ManCreateSatoko( Gia_Man_t * p )
void Gia_ManCollectVars_rec( int Var, Vec_Int_t * vMapping, Vec_Int_t * vRes, Vec_Bit_t * vVisit )
{
int * pCut, i;
if ( Vec_BitEntry(vVisit, Var) )
return;
Vec_BitWriteEntry(vVisit, Var, 1);
if ( Vec_IntEntry(vMapping, Var) ) // primary input or constant 0
{
pCut = Vec_IntEntryP( vMapping, Vec_IntEntry(vMapping, Var) );
for ( i = 1; i <= pCut[0]; i++ )
Gia_ManCollectVars_rec( pCut[i], vMapping, vRes, vVisit );
}
Vec_IntPush( vRes, Var );
}
Vec_Int_t * Gia_ManCollectVars( int Root, Vec_Int_t * vMapping, int nVars )
{
Vec_Int_t * vRes = Vec_IntAlloc( 100 );
Vec_Bit_t * vVisit = Vec_BitStart( nVars );
assert( Vec_IntEntry(vMapping, Root) );
Gia_ManCollectVars_rec( Root, vMapping, vRes, vVisit );
Vec_BitFree( vVisit );
return vRes;
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
satoko_t * Gia_ManSatokoInit( Cnf_Dat_t * pCnf, satoko_opts_t * opts )
{
satoko_t * pSat = satoko_create();
Cnf_Dat_t * pCnf = (Cnf_Dat_t *)Mf_ManGenerateCnf( p, 8, 0, 1, 0, 0 );
int i, status;
int i;
//sat_solver_setnvars( pSat, p->nVars );
for ( i = 0; i < pCnf->nClauses; i++ )
{
if ( !satoko_add_clause( pSat, (unsigned *)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;
satoko_configure(pSat, opts);
return pSat;
}
int Gia_ManCallSatokoOne( Gia_Man_t * p, satoko_opts_t * opts, int iOutput )
void Gia_ManSatokoReport( int iOutput, int status, abctime clk )
{
abctime clk = Abc_Clock();
satoko_t * pSat;
int status, Cost = 0;
pSat = Gia_ManCreateSatoko( p );
if ( pSat )
{
satoko_configure(pSat, opts);
status = satoko_solve( pSat );
Cost = (unsigned)pSat->stats.n_conflicts;
satoko_destroy( pSat );
}
else
status = SATOKO_UNSAT;
if ( iOutput >= 0 )
Abc_Print( 1, "Output %6d : ", iOutput );
else
@ -97,25 +110,89 @@ int Gia_ManCallSatokoOne( Gia_Man_t * p, satoko_opts_t * opts, int iOutput )
else
Abc_Print( 1, "UNSATISFIABLE " );
Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
Abc_PrintTime( 1, "Time", clk );
}
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 );
satoko_t * pSat = Gia_ManSatokoInit( pCnf, opts );
int status = pSat ? satoko_simplify(pSat) : SATOKO_OK;
Cnf_DataFree( pCnf );
if ( status == SATOKO_OK )
return pSat;
satoko_destroy( pSat );
return NULL;
}
int Gia_ManSatokoCallOne( Gia_Man_t * p, satoko_opts_t * opts, int iOutput )
{
abctime clk = Abc_Clock();
satoko_t * pSat;
int status, Cost = 0;
pSat = Gia_ManSatokoCreate( p, opts );
if ( pSat )
{
status = satoko_solve( pSat );
Cost = (unsigned)pSat->stats.n_conflicts;
satoko_destroy( pSat );
}
else
status = SATOKO_UNSAT;
Gia_ManSatokoReport( iOutput, status, Abc_Clock() - clk );
return Cost;
}
void Gia_ManCallSatoko( Gia_Man_t * p, satoko_opts_t * opts, int fSplit )
void Gia_ManSatokoCall( Gia_Man_t * p, satoko_opts_t * opts, int fSplit, int fIncrem )
{
int fUseCone = 1;
Gia_Man_t * pOne;
Gia_Obj_t * pRoot;
Vec_Int_t * vCone;
int i, iLit, status;
if ( fIncrem )
{
abctime clk = Abc_Clock();
Cnf_Dat_t * pCnf = (Cnf_Dat_t *)Mf_ManGenerateCnf( p, 8, 0, 0, fUseCone, 0 );
satoko_t * pSat = Gia_ManSatokoInit( pCnf, opts );
Gia_ManForEachCo( p, pRoot, i )
{
abctime clk = Abc_Clock();
iLit = Abc_Var2Lit( i+1, 0 );
satoko_assump_push( pSat, iLit );
if ( fUseCone )
{
vCone = Gia_ManCollectVars( i+1, pCnf->vMapping, pCnf->nVars );
satoko_mark_cone( pSat, Vec_IntArray(vCone), Vec_IntSize(vCone) );
printf( "Cone has %6d vars (out of %6d). ", Vec_IntSize(vCone), pCnf->nVars );
status = satoko_solve( pSat );
satoko_unmark_cone( pSat, Vec_IntArray(vCone), Vec_IntSize(vCone) );
Vec_IntFree( vCone );
}
else
{
status = satoko_solve( pSat );
}
satoko_assump_pop( pSat );
Gia_ManSatokoReport( i, status, Abc_Clock() - clk );
}
Cnf_DataFree( pCnf );
satoko_destroy( pSat );
Abc_PrintTime( 1, "Total time", Abc_Clock() - clk );
return;
}
if ( fSplit )
{
Gia_Man_t * pOne;
Gia_Obj_t * pRoot;
int i;
abctime clk = Abc_Clock();
Gia_ManForEachCo( p, pRoot, i )
{
pOne = Gia_ManDupDfsCone( p, pRoot );
Gia_ManCallSatokoOne( pOne, opts, i );
Gia_ManSatokoCallOne( pOne, opts, i );
Gia_ManStop( pOne );
}
Abc_PrintTime( 1, "Total time", Abc_Clock() - clk );
return;
}
Gia_ManCallSatokoOne( p, opts, -1 );
Gia_ManSatokoCallOne( p, opts, -1 );
}

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

@ -23410,13 +23410,13 @@ usage:
***********************************************************************/
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;
extern void Gia_ManSatokoCall( Gia_Man_t * p, satoko_opts_t * opts, int fSplit, int fIncrem );
int c, fSplit = 0, fIncrem = 0;
satoko_opts_t opts;
satoko_default_opts(&opts);
Extra_UtilGetoptReset();
while ( ( c = Extra_UtilGetopt( argc, argv, "Csvh" ) ) != EOF )
while ( ( c = Extra_UtilGetopt( argc, argv, "Csivh" ) ) != EOF )
{
switch ( c )
{
@ -23434,6 +23434,9 @@ int Abc_CommandAbc9Satoko( Abc_Frame_t * pAbc, int argc, char ** argv )
case 's':
fSplit ^= 1;
break;
case 'i':
fIncrem ^= 1;
break;
case 'v':
opts.verbose ^= 1;
break;
@ -23449,13 +23452,14 @@ int Abc_CommandAbc9Satoko( Abc_Frame_t * pAbc, int argc, char ** argv )
Abc_Print( -1, "Abc_CommandAbc9Satoko(): There is no AIG.\n" );
return 1;
}
Gia_ManCallSatoko( pAbc->pGia, &opts, fSplit );
Gia_ManSatokoCall( pAbc->pGia, &opts, fSplit, fIncrem );
return 0;
usage:
Abc_Print( -2, "usage: &satoko [-C num] [-svh]\n" );
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");
return 1;

6
src/base/cmd/cmdAuto.c
View File

@ -47,7 +47,7 @@ ABC_NAMESPACE_IMPL_START
#define CMD_AUTO_LINE_MAX 1000 // max number of chars in the string
#define CMD_AUTO_ARG_MAX 100 // max number of arguments in the call
extern int Gia_ManCallSatokoOne( Gia_Man_t * p, satoko_opts_t * opts, int iOutput );
extern int Gia_ManSatokoCallOne( Gia_Man_t * p, satoko_opts_t * opts, int iOutput );
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS ///
@ -92,7 +92,7 @@ int Cmd_RunAutoTunerEvalSimple( Vec_Ptr_t * vAigs, satoko_opts_t * pOpts )
//printf( "Tuning with options: " );
//Cmd_RunAutoTunerPrintOptions( pOpts );
Vec_PtrForEachEntry( Gia_Man_t *, vAigs, pGia, i )
TotalCost += Gia_ManCallSatokoOne( pGia, pOpts, -1 );
TotalCost += Gia_ManSatokoCallOne( pGia, pOpts, -1 );
return TotalCost;
}
@ -142,7 +142,7 @@ void * Cmd_RunAutoTunerEvalWorkerThread( void * pArg )
assert( 0 );
return NULL;
}
pThData->Result = Gia_ManCallSatokoOne( pThData->pGia, pThData->pOpts, -1 );
pThData->Result = Gia_ManSatokoCallOne( pThData->pGia, pThData->pOpts, -1 );
pThData->fWorking = 0;
}
assert( 0 );

2
src/sat/satoko/satoko.h
View File

@ -89,6 +89,8 @@ extern void satoko_assump_push(satoko_t *s, unsigned);
extern void satoko_assump_pop(satoko_t *s);
extern int satoko_simplify(satoko_t *);
extern int satoko_solve(satoko_t *);
extern void satoko_mark_cone(satoko_t *s, int * pvars, int nvars);
extern void satoko_unmark_cone(satoko_t *s, int * pvars, int nvars);
/* If problem is unsatisfiable under assumptions, this function is used to
* obtain the final conflict clause expressed in the assumptions.

16
src/sat/satoko/solver.c
View File

@ -190,14 +190,18 @@ static inline unsigned solver_decide(solver_t *s)
if (heap_size(s->var_order) == 0) {
next_var = UNDEF;
return UNDEF;
} else
next_var = heap_remove_min(s->var_order);
}
next_var = heap_remove_min(s->var_order);
if (solver_has_marks(s) && !var_mark(s, next_var))
next_var = UNDEF;
}
return var2lit(next_var, vec_char_at(s->polarity, next_var));
}
static inline void solver_new_decision(solver_t *s, unsigned lit)
{
if (solver_has_marks(s) && !var_mark(s, lit2var(lit)))
return;
assert(var_value(s, lit2var(lit)) == VAR_UNASSING);
vec_uint_push_back(s->trail_lim, vec_uint_size(s->trail));
solver_enqueue(s, lit, UNDEF);
@ -538,6 +542,8 @@ unsigned solver_propagate(solver_t *s)
n_propagations++;
watch_list_foreach(s->bin_watches, i, p) {
if (solver_has_marks(s) && !var_mark(s, lit2var(i->blocker)))
continue;
if (var_value(s, lit2var(i->blocker)) == VAR_UNASSING)
solver_enqueue(s, i->blocker, i->cref);
else if (lit_value(s, i->blocker) == LIT_FALSE)
@ -551,6 +557,12 @@ unsigned solver_propagate(solver_t *s)
struct clause *clause;
struct watcher w;
if (solver_has_marks(s) && !var_mark(s, lit2var(i->blocker)))
{
*j++ = *i++;
continue;
}
if (lit_value(s, i->blocker) == LIT_TRUE) {
*j++ = *i++;
continue;

23
src/sat/satoko/solver.h
View File

@ -93,6 +93,9 @@ struct solver_t_ {
vec_uint_t *stamps; /* Multipurpose stamp used to calculate LBD and
* clauses minimization with binary resolution */
/* Temporary data used for solving cones */
vec_char_t *marks;
struct satoko_stats stats;
struct satoko_opts opts;
};
@ -133,6 +136,18 @@ static inline unsigned var_reason(solver_t *s, unsigned var)
{
return vec_uint_at(s->reasons, var);
}
static inline int var_mark(solver_t *s, unsigned var)
{
return (int)vec_char_at(s->marks, var);
}
static inline void var_set_mark(solver_t *s, unsigned var)
{
vec_char_assign(s->marks, var, 1);
}
static inline void var_clean_mark(solver_t *s, unsigned var)
{
vec_char_assign(s->marks, var, 0);
}
//===------------------------------------------------------------------------===
// Inline lit functions
//===------------------------------------------------------------------------===
@ -185,6 +200,14 @@ static inline int solver_enqueue(solver_t *s, unsigned lit, unsigned reason)
vec_uint_push_back(s->trail, lit);
return SATOKO_OK;
}
static inline int solver_varnum(solver_t *s)
{
return vec_char_size(s->assigns);
}
static inline int solver_has_marks(solver_t *s)
{
return (int)(s->marks != NULL);
}
//===------------------------------------------------------------------------===
// Inline clause functions

27
src/sat/satoko/solver_api.c
View File

@ -145,11 +145,13 @@ void satoko_destroy(solver_t *s)
vec_uint_free(s->stack);
vec_uint_free(s->last_dlevel);
vec_uint_free(s->stamps);
if (s->marks) vec_char_free(s->marks);
satoko_free(s);
}
void satoko_default_opts(satoko_opts_t *opts)
{
memset(opts, 0, sizeof(satoko_opts_t));
opts->verbose = 0;
/* Limits */
opts->conf_limit = 0;
@ -232,6 +234,7 @@ void satoko_add_variable(solver_t *s, char sign)
vec_uint_push_back(s->stamps, 0);
vec_char_push_back(s->seen, 0);
heap_insert(s->var_order, var);
if (s->marks) vec_char_push_back(s->marks, 0);
}
int satoko_add_clause(solver_t *s, unsigned *lits, unsigned size)
@ -287,8 +290,8 @@ int satoko_solve(solver_t *s)
char status = SATOKO_UNDEC;
assert(s);
if (s->opts.verbose)
print_opts(s);
//if (s->opts.verbose)
// print_opts(s);
while (status == SATOKO_UNDEC) {
status = solver_search(s);
@ -317,4 +320,24 @@ satoko_stats_t satoko_stats(satoko_t *s)
return s->stats;
}
void satoko_mark_cone(satoko_t *s, int * pvars, int nvars)
{
int i;
if (!solver_has_marks(s))
s->marks = vec_char_init(solver_varnum(s), 0);
for (i = 0; i < nvars; i++)
{
var_set_mark(s, pvars[i]);
if (!heap_in_heap(s->var_order, pvars[i]))
heap_insert(s->var_order, pvars[i]);
}
}
void satoko_unmark_cone(satoko_t *s, int * pvars, int nvars)
{
int i;
assert(solver_has_marks(s));
for (i = 0; i < nvars; i++)
var_clean_mark(s, pvars[i]);
}
ABC_NAMESPACE_IMPL_END