diff options
| author | Alan Mishchenko <alanmi@berkeley.edu> | 2016-04-12 19:44:21 -0700 |
|---|---|---|
| committer | Alan Mishchenko <alanmi@berkeley.edu> | 2016-04-12 19:44:21 -0700 |
| commit | 89d4ac502908d4b41edaccfb858fef584374728d (patch) | |
| tree | e2aeb4d99256e4106900d25066400f99cd8410b1 /src/sat/bmc/bmcClp.c | |
| parent | 8de7383edd3ef28875d6ccb4b992776cf906a405 (diff) | |
| download | abc-89d4ac502908d4b41edaccfb858fef584374728d.tar.gz abc-89d4ac502908d4b41edaccfb858fef584374728d.tar.bz2 abc-89d4ac502908d4b41edaccfb858fef584374728d.zip | |
Adding new implementation of LEXSAT.
Diffstat (limited to 'src/sat/bmc/bmcClp.c')
| -rw-r--r-- | src/sat/bmc/bmcClp.c | 7 |
1 files changed, 6 insertions, 1 deletions
diff --git a/src/sat/bmc/bmcClp.c b/src/sat/bmc/bmcClp.c index eb924123..8a69fe56 100644 --- a/src/sat/bmc/bmcClp.c +++ b/src/sat/bmc/bmcClp.c @@ -592,7 +592,7 @@ int Bmc_CollapseExpand2( sat_solver * pSat, sat_solver * pSatOn, Vec_Int_t * vLi SeeAlso [] ***********************************************************************/ -int Bmc_ComputeCanonical( sat_solver * pSat, Vec_Int_t * vLits, Vec_Int_t * vTemp, int nBTLimit ) +int Bmc_ComputeCanonical2( sat_solver * pSat, Vec_Int_t * vLits, Vec_Int_t * vTemp, int nBTLimit ) { int i, k, iLit, status = l_Undef; for ( i = 0; i < Vec_IntSize(vLits); i++ ) @@ -621,6 +621,11 @@ int Bmc_ComputeCanonical( sat_solver * pSat, Vec_Int_t * vLits, Vec_Int_t * vTem assert( status == l_True ); return status; } +int Bmc_ComputeCanonical( sat_solver * pSat, Vec_Int_t * vLits, Vec_Int_t * vTemp, int nBTLimit ) +{ + sat_solver_set_resource_limits( pSat, nBTLimit, 0, 0, 0 ); + return sat_solver_solve_lexsat( pSat, Vec_IntArray(vLits), Vec_IntSize(vLits) ); +} /**Function************************************************************* |