From 89d4ac502908d4b41edaccfb858fef584374728d Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Tue, 12 Apr 2016 19:44:21 -0700 Subject: Adding new implementation of LEXSAT. --- src/sat/bmc/bmcClp.c | 7 ++++++- 1 file changed, 6 insertions(+), 1 deletion(-) (limited to 'src/sat/bmc/bmcClp.c') 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************************************************************* -- cgit v1.2.3