summaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
authorAlan Mishchenko <alanmi@berkeley.edu>2015-09-18 08:10:18 -0700
committerAlan Mishchenko <alanmi@berkeley.edu>2015-09-18 08:10:18 -0700
commit3b838b953d36c6293af51ddae55ec061e994b4c7 (patch)
treeaf8d6fdfbcdb53a1e3d5ae403d9e7523b1cbba45
parentc30a0af71c219dcdd42322c411b805bb674d14b7 (diff)
downloadabc-3b838b953d36c6293af51ddae55ec061e994b4c7.tar.gz
abc-3b838b953d36c6293af51ddae55ec061e994b4c7.tar.bz2
abc-3b838b953d36c6293af51ddae55ec061e994b4c7.zip
Tuning SAT solver for QBF instances.
-rw-r--r--src/base/abci/abc.c15
-rw-r--r--src/proof/fra/fraCec.c2
-rw-r--r--src/sat/cnf/cnfUtil.c12
3 files changed, 22 insertions, 7 deletions
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index 809995c4..47da5723 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -21828,7 +21828,8 @@ int Abc_CommandDSat( Abc_Frame_t * pAbc, int argc, char ** argv )
if ( argc == globalUtilOptind + 1 )
{
- extern int Cnf_DataSolveFromFile( char * pFileName, int nConfLimit, int fVerbose );
+ int * pModel = NULL;
+ extern int Cnf_DataSolveFromFile( char * pFileName, int nConfLimit, int nLearnedStart, int nLearnedDelta, int nLearnedPerce, int fVerbose, int ** ppModel );
// get the input file name
char * pFileName = argv[globalUtilOptind];
FILE * pFile = fopen( pFileName, "rb" );
@@ -21838,10 +21839,18 @@ int Abc_CommandDSat( Abc_Frame_t * pAbc, int argc, char ** argv )
return 0;
}
fclose( pFile );
- Cnf_DataSolveFromFile( pFileName, nConfLimit, fVerbose );
+ Cnf_DataSolveFromFile( pFileName, nConfLimit, nLearnedStart, nLearnedDelta, nLearnedPerce, fVerbose, &pModel );
+ if ( pModel && pNtk )
+ {
+ int * pSimInfo = Abc_NtkVerifySimulatePattern( pNtk, pModel );
+ if ( pSimInfo[0] != 1 )
+ Abc_Print( 1, "ERROR in Abc_NtkMiterSat(): Generated counter example is invalid.\n" );
+ ABC_FREE( pSimInfo );
+ pAbc->pCex = Abc_CexCreate( 0, Abc_NtkPiNum(pNtk), pNtk->pModel, 0, 0, 0 );
+ }
+ ABC_FREE( pModel );
return 0;
}
-
if ( pNtk == NULL )
{
Abc_Print( -1, "Empty network.\n" );
diff --git a/src/proof/fra/fraCec.c b/src/proof/fra/fraCec.c
index fe113367..130036a6 100644
--- a/src/proof/fra/fraCec.c
+++ b/src/proof/fra/fraCec.c
@@ -194,7 +194,7 @@ int Fra_FraigSat( Aig_Man_t * pMan, ABC_INT64_T nConfLimit, ABC_INT64_T nInsLimi
}
if ( nLearnedStart )
- pSat->nLearntStart = nLearnedStart;
+ pSat->nLearntStart = pSat->nLearntMax = nLearnedStart;
if ( nLearnedDelta )
pSat->nLearntDelta = nLearnedDelta;
if ( nLearnedPerce )
diff --git a/src/sat/cnf/cnfUtil.c b/src/sat/cnf/cnfUtil.c
index ed38e735..7900b08c 100644
--- a/src/sat/cnf/cnfUtil.c
+++ b/src/sat/cnf/cnfUtil.c
@@ -399,7 +399,7 @@ finish:
SeeAlso []
***********************************************************************/
-int Cnf_DataSolveFromFile( char * pFileName, int nConfLimit, int fVerbose )
+int Cnf_DataSolveFromFile( char * pFileName, int nConfLimit, int nLearnedStart, int nLearnedDelta, int nLearnedPerce, int fVerbose, int ** ppModel )
{
abctime clk = Abc_Clock();
Cnf_Dat_t * pCnf = Cnf_DataReadFromFile( pFileName );
@@ -420,9 +420,15 @@ int Cnf_DataSolveFromFile( char * pFileName, int nConfLimit, int fVerbose )
printf( "The problem is trivially UNSAT.\n" );
return 1;
}
+ if ( nLearnedStart )
+ pSat->nLearntStart = pSat->nLearntMax = nLearnedStart;
+ if ( nLearnedDelta )
+ pSat->nLearntDelta = nLearnedDelta;
+ if ( nLearnedPerce )
+ pSat->nLearntRatio = nLearnedPerce;
+ if ( fVerbose )
+ pSat->fVerbose = fVerbose;
// solve the miter
-// if ( fVerbose )
-// pSat->verbosity = 1;
status = sat_solver_solve( pSat, NULL, NULL, (ABC_INT64_T)nConfLimit, 0, (ABC_INT64_T)0, (ABC_INT64_T)0 );
if ( status == l_Undef )
RetValue = -1;