diff options
Diffstat (limited to 'src/aig')
-rw-r--r-- | src/aig/gia/giaIso.c | 2 | ||||
-rw-r--r-- | src/aig/gia/giaIso2.c | 2 | ||||
-rw-r--r-- | src/aig/gia/giaSat3.c | 136 | ||||
-rw-r--r-- | src/aig/gia/module.make | 1 | ||||
-rw-r--r-- | src/aig/saig/saigIsoSlow.c | 2 |
5 files changed, 140 insertions, 3 deletions
diff --git a/src/aig/gia/giaIso.c b/src/aig/gia/giaIso.c index baf7bc93..0e040b6c 100644 --- a/src/aig/gia/giaIso.c +++ b/src/aig/gia/giaIso.c @@ -24,7 +24,7 @@ ABC_NAMESPACE_IMPL_START #define ISO_MASK 0xFF -static int s_256Primes[ISO_MASK+1] = +static unsigned int s_256Primes[ISO_MASK+1] = { 0x984b6ad9,0x18a6eed3,0x950353e2,0x6222f6eb,0xdfbedd47,0xef0f9023,0xac932a26,0x590eaf55, 0x97d0a034,0xdc36cd2e,0x22736b37,0xdc9066b0,0x2eb2f98b,0x5d9c7baf,0x85747c9e,0x8aca1055, diff --git a/src/aig/gia/giaIso2.c b/src/aig/gia/giaIso2.c index e1ea7690..576b118f 100644 --- a/src/aig/gia/giaIso2.c +++ b/src/aig/gia/giaIso2.c @@ -27,7 +27,7 @@ ABC_NAMESPACE_IMPL_START #define ISO_MASK 0xFF -static int s_256Primes[ISO_MASK+1] = +static unsigned int s_256Primes[ISO_MASK+1] = { 0x984b6ad9,0x18a6eed3,0x950353e2,0x6222f6eb,0xdfbedd47,0xef0f9023,0xac932a26,0x590eaf55, 0x97d0a034,0xdc36cd2e,0x22736b37,0xdc9066b0,0x2eb2f98b,0x5d9c7baf,0x85747c9e,0x8aca1055, diff --git a/src/aig/gia/giaSat3.c b/src/aig/gia/giaSat3.c new file mode 100644 index 00000000..fe76b078 --- /dev/null +++ b/src/aig/gia/giaSat3.c @@ -0,0 +1,136 @@ +/**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/bsat/satSolver3.h" + +ABC_NAMESPACE_IMPL_START + + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +sat_solver3 * Gia_ManSat3Init( Cnf_Dat_t * pCnf ) +{ + sat_solver3 * pSat = sat_solver3_new(); + int i; + //sat_solver_setnvars( pSat, p->nVars ); + for ( i = 0; i < pCnf->nClauses; i++ ) + { + if ( !sat_solver3_addclause( pSat, pCnf->pClauses[i], pCnf->pClauses[i+1] ) ) + { + sat_solver3_delete( pSat ); + return NULL; + } + } + return pSat; +} +void Gia_ManSat3Report( int iOutput, int status, abctime clk ) +{ + if ( iOutput >= 0 ) + Abc_Print( 1, "Output %6d : ", iOutput ); + else + Abc_Print( 1, "Total: " ); + + if ( status == l_Undef ) + Abc_Print( 1, "UNDECIDED " ); + else if ( status == l_True ) + Abc_Print( 1, "SATISFIABLE " ); + else + Abc_Print( 1, "UNSATISFIABLE " ); + + Abc_PrintTime( 1, "Time", clk ); +} +sat_solver3 * Gia_ManSat3Create( Gia_Man_t * p ) +{ + Cnf_Dat_t * pCnf = (Cnf_Dat_t *)Mf_ManGenerateCnf( p, 8, 0, 1, 0, 0 ); + sat_solver3 * pSat = Gia_ManSat3Init( pCnf ); + int status = pSat ? sat_solver3_simplify(pSat) : 0; + Cnf_DataFree( pCnf ); + if ( status ) + return pSat; + if ( pSat ) + sat_solver3_delete( pSat ); + return NULL; +} +int Gia_ManSat3CallOne( Gia_Man_t * p, int iOutput ) +{ + abctime clk = Abc_Clock(); + sat_solver3 * pSat; + int status, Cost = 0; + + pSat = Gia_ManSat3Create( p ); + if ( pSat ) + { + status = sat_solver3_solve( pSat, NULL, NULL, 0, 0, 0, 0 ); + Cost = (unsigned)pSat->stats.conflicts; + sat_solver3_delete( pSat ); + } + else + status = l_False; + + Gia_ManSat3Report( iOutput, status, Abc_Clock() - clk ); + return Cost; +} +void Gia_ManSat3Call( Gia_Man_t * p, int fSplit ) +{ + Gia_Man_t * pOne; + Gia_Obj_t * pRoot; + int i; + if ( fSplit ) + { + abctime clk = Abc_Clock(); + Gia_ManForEachCo( p, pRoot, i ) + { + pOne = Gia_ManDupDfsCone( p, pRoot ); + Gia_ManSat3CallOne( pOne, i ); + Gia_ManStop( pOne ); + } + Abc_PrintTime( 1, "Total time", Abc_Clock() - clk ); + return; + } + Gia_ManSat3CallOne( p, -1 ); +} + + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + +ABC_NAMESPACE_IMPL_END + diff --git a/src/aig/gia/module.make b/src/aig/gia/module.make index 0ddf9833..82d5a123 100644 --- a/src/aig/gia/module.make +++ b/src/aig/gia/module.make @@ -60,6 +60,7 @@ SRC += src/aig/gia/giaAig.c \ src/aig/gia/giaSatLut.c \ src/aig/gia/giaSatMap.c \ src/aig/gia/giaSatoko.c \ + src/aig/gia/giaSat3.c \ src/aig/gia/giaScl.c \ src/aig/gia/giaScript.c \ src/aig/gia/giaShow.c \ diff --git a/src/aig/saig/saigIsoSlow.c b/src/aig/saig/saigIsoSlow.c index 58dc6596..a0e2d1d0 100644 --- a/src/aig/saig/saigIsoSlow.c +++ b/src/aig/saig/saigIsoSlow.c @@ -120,7 +120,7 @@ static int s_1kPrimes[ISO_MASK+1] = { */ #define ISO_MASK 0x3FF -static int s_1kPrimes[ISO_MASK+1] = +static unsigned int s_1kPrimes[ISO_MASK+1] = //#define ISO_MASK 0xFF //static int s_1kPrimes[0x3FF+1] = { |