diff options
| author | Alan Mishchenko <alanmi@berkeley.edu> | 2011-10-24 18:05:45 +0800 |
|---|---|---|
| committer | Alan Mishchenko <alanmi@berkeley.edu> | 2011-10-24 18:05:45 +0800 |
| commit | f96f3fa58355b1d78ade7c764882e4482e88daca (patch) | |
| tree | e38e748614864cb7af5d226f99d4835638691fdf /src/base/abci/abcQbf.c | |
| parent | 88c36d9d657f478cd9cd736eeed91a186cb73815 (diff) | |
| download | abc-f96f3fa58355b1d78ade7c764882e4482e88daca.tar.gz abc-f96f3fa58355b1d78ade7c764882e4482e88daca.tar.bz2 abc-f96f3fa58355b1d78ade7c764882e4482e88daca.zip | |
Improvements to the QBF solver.
Diffstat (limited to 'src/base/abci/abcQbf.c')
| -rw-r--r-- | src/base/abci/abcQbf.c | 7 |
1 files changed, 4 insertions, 3 deletions
diff --git a/src/base/abci/abcQbf.c b/src/base/abci/abcQbf.c index d246f039..a243c7d5 100644 --- a/src/base/abci/abcQbf.c +++ b/src/base/abci/abcQbf.c @@ -89,7 +89,8 @@ void Abc_NtkQbf( Abc_Ntk_t * pNtk, int nPars, int fVerbose ) { // solve the synthesis instance clkS = clock(); - RetValue = Abc_NtkMiterSat( pNtkSyn, 0, 0, 0, NULL, NULL ); +// RetValue = Abc_NtkMiterSat( pNtkSyn, 0, 0, 0, NULL, NULL ); + RetValue = Abc_NtkDSat( pNtkSyn, (ABC_INT64_T)0, (ABC_INT64_T)0, 1, 0, 0 ); clkS = clock() - clkS; if ( RetValue == 0 ) Abc_NtkModelToVector( pNtkSyn, vPiValues ); @@ -143,8 +144,8 @@ clkV = clock() - clkV; printf( "AIG = %6d ", Abc_NtkNodeNum(pNtkSyn) ); Abc_NtkVectorPrintVars( pNtk, vPiValues, nPars ); printf( " " ); -// ABC_PRTn( "Syn", clkS ); - ABC_PRT( "Ver", clkV ); + ABC_PRT( "Syn", clkS ); +// ABC_PRT( "Ver", clkV ); } } Abc_NtkDelete( pNtkSyn ); |