diff options
author | Alan Mishchenko <alanmi@berkeley.edu> | 2017-02-08 18:57:16 -0800 |
---|---|---|
committer | Alan Mishchenko <alanmi@berkeley.edu> | 2017-02-08 18:57:16 -0800 |
commit | 77e2b1ff53bd806a681c9a887cd5b026681d271b (patch) | |
tree | 836772eb3d0f29f9afa61cd2b4f8b181859baabb /src/aig/gia | |
parent | cf24a0eb0c630e19bf1d81622fc05327371c63cf (diff) | |
download | abc-77e2b1ff53bd806a681c9a887cd5b026681d271b.tar.gz abc-77e2b1ff53bd806a681c9a887cd5b026681d271b.tar.bz2 abc-77e2b1ff53bd806a681c9a887cd5b026681d271b.zip |
Autotuner for 'satoko'.
Diffstat (limited to 'src/aig/gia')
-rw-r--r-- | src/aig/gia/giaSatoko.c | 8 |
1 files changed, 6 insertions, 2 deletions
diff --git a/src/aig/gia/giaSatoko.c b/src/aig/gia/giaSatoko.c index 5506c7e4..fc8e5c28 100644 --- a/src/aig/gia/giaSatoko.c +++ b/src/aig/gia/giaSatoko.c @@ -21,6 +21,7 @@ #include "gia.h" #include "sat/cnf/cnf.h" #include "sat/satoko/satoko.h" +#include "sat/satoko/solver.h" ABC_NAMESPACE_IMPL_START @@ -68,17 +69,19 @@ satoko_t * Gia_ManCreateSatoko( Gia_Man_t * p ) satoko_destroy( pSat ); return NULL; } -void Gia_ManCallSatokoOne( Gia_Man_t * p, satoko_opts_t * opts, int iOutput ) +int Gia_ManCallSatokoOne( Gia_Man_t * p, satoko_opts_t * opts, int iOutput ) { abctime clk = Abc_Clock(); satoko_t * pSat; - int status; + 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 @@ -97,6 +100,7 @@ void Gia_ManCallSatokoOne( Gia_Man_t * p, satoko_opts_t * opts, int iOutput ) Abc_Print( 1, "UNSATISFIABLE " ); Abc_PrintTime( 1, "Time", Abc_Clock() - clk ); + return Cost; } void Gia_ManCallSatoko( Gia_Man_t * p, satoko_opts_t * opts, int fSplit ) { |