From f96f3fa58355b1d78ade7c764882e4482e88daca Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Mon, 24 Oct 2011 18:05:45 +0800 Subject: Improvements to the QBF solver. --- src/base/abci/abcQbf.c | 7 ++++--- 1 file changed, 4 insertions(+), 3 deletions(-) (limited to 'src/base/abci/abcQbf.c') 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 ); -- cgit v1.2.3