summaryrefslogtreecommitdiffstats
path: root/src/base
diff options
context:
space:
mode:
authorAlan Mishchenko <alanmi@berkeley.edu>2015-11-06 13:49:23 -0800
committerAlan Mishchenko <alanmi@berkeley.edu>2015-11-06 13:49:23 -0800
commite50fc467fd54420cf262bf5266959f6c02a65bf7 (patch)
tree925906416cae4d923544269d106b74644a7a72ad /src/base
parentdd365cbaf36fad4675bb116a8e7e80dbfdd0205a (diff)
downloadabc-e50fc467fd54420cf262bf5266959f6c02a65bf7.tar.gz
abc-e50fc467fd54420cf262bf5266959f6c02a65bf7.tar.bz2
abc-e50fc467fd54420cf262bf5266959f6c02a65bf7.zip
Improvements to 'satclp' (unfinished).
Diffstat (limited to 'src/base')
-rw-r--r--src/base/abci/abcCollapse.c46
1 files changed, 31 insertions, 15 deletions
diff --git a/src/base/abci/abcCollapse.c b/src/base/abci/abcCollapse.c
index f9b02fda..653618c5 100644
--- a/src/base/abci/abcCollapse.c
+++ b/src/base/abci/abcCollapse.c
@@ -643,12 +643,15 @@ int Abc_NtkCollapseCountVars( Vec_Str_t * vSop, Vec_Int_t * vSupp )
SeeAlso []
***********************************************************************/
-sat_solver * Abc_NtkClpDeriveSatSolver( Cnf_Dat_t * pCnf, int iCoObjId, Vec_Int_t * vSupp, Vec_Int_t * vAnds, Vec_Int_t * vMap, sat_solver ** ppSat )
+sat_solver * Abc_NtkClpDeriveSatSolver( Cnf_Dat_t * pCnf, int iCoObjId, Vec_Int_t * vSupp, Vec_Int_t * vAnds, Vec_Int_t * vMap, sat_solver ** ppSat1, sat_solver ** ppSat2, sat_solver ** ppSat3 )
{
int i, k, iObj, status, nVars = 2;
+// int i, k, iObj, status, nVars = 1;
Vec_Int_t * vLits = Vec_IntAlloc( 16 );
sat_solver * pSat = sat_solver_new();
- if ( ppSat ) *ppSat = sat_solver_new();
+ if ( ppSat1 ) *ppSat1 = sat_solver_new();
+ if ( ppSat2 ) *ppSat2 = sat_solver_new();
+ if ( ppSat3 ) *ppSat3 = sat_solver_new();
// assign SAT variable numbers
Vec_IntWriteEntry( vMap, iCoObjId, nVars++ );
Vec_IntForEachEntry( vSupp, iObj, k )
@@ -656,9 +659,13 @@ sat_solver * Abc_NtkClpDeriveSatSolver( Cnf_Dat_t * pCnf, int iCoObjId, Vec_Int_
Vec_IntForEachEntry( vAnds, iObj, k )
if ( pCnf->pObj2Clause[iObj] != -1 )
Vec_IntWriteEntry( vMap, iObj, nVars++ );
+// Vec_IntForEachEntry( vSupp, iObj, k )
+// Vec_IntWriteEntry( vMap, iObj, nVars++ );
// create clauses for the internal nodes and for the output
sat_solver_setnvars( pSat, nVars );
- if ( ppSat ) sat_solver_setnvars( *ppSat, nVars );
+ if ( ppSat1 ) sat_solver_setnvars( *ppSat1, nVars );
+ if ( ppSat2 ) sat_solver_setnvars( *ppSat2, nVars );
+ if ( ppSat3 ) sat_solver_setnvars( *ppSat3, nVars );
Vec_IntPush( vAnds, iCoObjId );
Vec_IntForEachEntry( vAnds, iObj, k )
{
@@ -676,7 +683,9 @@ sat_solver * Abc_NtkClpDeriveSatSolver( Cnf_Dat_t * pCnf, int iCoObjId, Vec_Int_
status = sat_solver_addclause( pSat, Vec_IntArray(vLits), Vec_IntArray(vLits)+Vec_IntSize(vLits) );
assert( status );
(void) status;
- if ( ppSat ) sat_solver_addclause( *ppSat, Vec_IntArray(vLits), Vec_IntArray(vLits)+Vec_IntSize(vLits) );
+ if ( ppSat1 ) sat_solver_addclause( *ppSat1, Vec_IntArray(vLits), Vec_IntArray(vLits)+Vec_IntSize(vLits) );
+ if ( ppSat2 ) sat_solver_addclause( *ppSat2, Vec_IntArray(vLits), Vec_IntArray(vLits)+Vec_IntSize(vLits) );
+ if ( ppSat3 ) sat_solver_addclause( *ppSat3, Vec_IntArray(vLits), Vec_IntArray(vLits)+Vec_IntSize(vLits) );
}
}
Vec_IntPop( vAnds );
@@ -696,15 +705,15 @@ sat_solver * Abc_NtkClpDeriveSatSolver( Cnf_Dat_t * pCnf, int iCoObjId, Vec_Int_
SeeAlso []
***********************************************************************/
-Vec_Str_t * Abc_NtkClpGiaOne( Gia_Man_t * p, int iCo, int nCubeLim, int nBTLimit, int fVerbose, int fCanon, int fReverse, Vec_Int_t * vSupp )
+Vec_Str_t * Abc_NtkClpGiaOne( Gia_Man_t * p, int iCo, int nCubeLim, int nBTLimit, int fCanon, int fReverse, Vec_Int_t * vSupp, int fVerbose )
{
Vec_Str_t * vSop;
abctime clk = Abc_Clock();
- extern Vec_Str_t * Bmc_CollapseOne( Gia_Man_t * p, int nCubeLim, int nBTLimit, int fCanon, int fReverse, int fVerbose );
+ extern Vec_Str_t * Bmc_CollapseOneOld( Gia_Man_t * p, int nCubeLim, int nBTLimit, int fCanon, int fReverse, int fVerbose );
Gia_Man_t * pGia = Gia_ManDupCones( p, &iCo, 1, 1 );
if ( fVerbose )
printf( "Output %4d: Supp = %4d. Cone =%6d.\n", iCo, Vec_IntSize(vSupp), Gia_ManAndNum(pGia) );
- vSop = Bmc_CollapseOne( pGia, nCubeLim, nBTLimit, fCanon, fReverse, fVerbose );
+ vSop = Bmc_CollapseOneOld( pGia, nCubeLim, nBTLimit, fCanon, fReverse, fVerbose );
Gia_ManStop( pGia );
if ( vSop == NULL )
return NULL;
@@ -718,13 +727,15 @@ Vec_Str_t * Abc_NtkClpGiaOne( Gia_Man_t * p, int iCo, int nCubeLim, int nBTLimit
Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
return vSop;
}
-Vec_Str_t * Abc_NtkClpGiaOne2( Cnf_Dat_t * pCnf, Gia_Man_t * p, int iCo, int nCubeLim, int nBTLimit, int fVerbose, int fCanon, int fReverse, Vec_Int_t * vSupp, Vec_Int_t * vMap )
+Vec_Str_t * Abc_NtkClpGiaOne2( Cnf_Dat_t * pCnf, Gia_Man_t * p, int iCo, int nCubeLim, int nBTLimit, int fCanon, int fReverse, Vec_Int_t * vSupp, Vec_Int_t * vMap, int fVerbose )
{
Vec_Str_t * vSop;
- sat_solver * pSat, * pSat2 = NULL;
+ sat_solver * pSat, * pSat1 = NULL, * pSat2 = NULL, * pSat3 = NULL;
Gia_Obj_t * pObj;
abctime clk = Abc_Clock();
- extern Vec_Str_t * Bmc_CollapseOne_int( sat_solver * pSat, sat_solver * pSat2, int nVars, int nCubeLim, int nBTLimit, int fCanon, int fReverse, int fVerbose );
+ extern Vec_Str_t * Bmc_CollapseOne_int( sat_solver * pSat, int nVars, int nCubeLim, int nBTLimit, int fCanon, int fReverse, int fVerbose );
+ extern Vec_Str_t * Bmc_CollapseOne_int2( sat_solver * pSat, sat_solver * pSat2, int nVars, int nCubeLim, int nBTLimit, int fCanon, int fReverse, int fVerbose );
+ extern Vec_Str_t * Bmc_CollapseOne_int3( sat_solver * pSat, sat_solver * pSat1, sat_solver * pSat2, sat_solver * pSat3, int nVars, int nCubeLim, int nBTLimit, int fCanon, int fReverse, int fVerbose );
int i, iCoObjId = Gia_ObjId( p, Gia_ManCo(p, iCo) );
Vec_Int_t * vAnds = Vec_IntAlloc( 100 );
Vec_Int_t * vSuppObjs = Vec_IntAlloc( 100 );
@@ -733,13 +744,18 @@ Vec_Str_t * Abc_NtkClpGiaOne2( Cnf_Dat_t * pCnf, Gia_Man_t * p, int iCo, int nCu
Gia_ManIncrementTravId( p );
Gia_ManCollectAnds( p, &iCoObjId, 1, vAnds );
assert( Vec_IntSize(vAnds) > 0 );
- pSat = Abc_NtkClpDeriveSatSolver( pCnf, iCoObjId, vSuppObjs, vAnds, vMap, &pSat2 );
+// pSat = Abc_NtkClpDeriveSatSolver( pCnf, iCoObjId, vSuppObjs, vAnds, vMap, &pSat1, &pSat2, &pSat3 );
+ pSat = Abc_NtkClpDeriveSatSolver( pCnf, iCoObjId, vSuppObjs, vAnds, vMap, NULL, NULL, NULL );
Vec_IntFree( vSuppObjs );
if ( fVerbose )
printf( "Output %4d: Supp = %4d. Cone =%6d.\n", iCo, Vec_IntSize(vSupp), Vec_IntSize(vAnds) );
- vSop = Bmc_CollapseOne_int( pSat, pSat2, Vec_IntSize(vSupp), nCubeLim, nBTLimit, fCanon, fReverse, fVerbose );
+// vSop = Bmc_CollapseOne_int3( pSat, pSat1, pSat2, pSat3, Vec_IntSize(vSupp), nCubeLim, nBTLimit, fCanon, fReverse, fVerbose );
+// vSop = Bmc_CollapseOne_int2( pSat, pSat1, Vec_IntSize(vSupp), nCubeLim, nBTLimit, fCanon, fReverse, fVerbose );
+ vSop = Bmc_CollapseOne_int( pSat, Vec_IntSize(vSupp), nCubeLim, nBTLimit, fCanon, fReverse, fVerbose );
sat_solver_delete( pSat );
- sat_solver_delete( pSat2 );
+ if ( pSat1 ) sat_solver_delete( pSat1 );
+ if ( pSat2 ) sat_solver_delete( pSat2 );
+ if ( pSat3 ) sat_solver_delete( pSat3 );
Vec_IntFree( vAnds );
if ( vSop == NULL )
return NULL;
@@ -794,8 +810,8 @@ Vec_Ptr_t * Abc_GiaDeriveSops( Abc_Ntk_t * pNtkNew, Gia_Man_t * p, Vec_Wec_t * v
Vec_PtrWriteEntry( vSopsRepr, iEntry, (void *)(ABC_PTRINT_T)1 );
continue;
}
-// vSop = Abc_NtkClpGiaOne( p, iCoThis, nCubeLim, nBTLimit, i ? 0 : fVerbose, fCanon, fReverse, vSupp );
- vSop = Abc_NtkClpGiaOne2( pCnf, p, iCoThis, nCubeLim, nBTLimit, i ? 0 : fVerbose, fCanon, fReverse, vSupp, vMap );
+ vSop = Abc_NtkClpGiaOne( p, iCoThis, nCubeLim, nBTLimit, fCanon, fReverse, vSupp, i ? 0 : fVerbose );
+// vSop = Abc_NtkClpGiaOne2( pCnf, p, iCoThis, nCubeLim, nBTLimit, fCanon, fReverse, vSupp, vMap, i ? 0 : fVerbose );
if ( vSop == NULL )
goto finish;
assert( Vec_IntSize( Vec_WecEntry(vSupps, iCoThis) ) == Abc_SopGetVarNum(Vec_StrArray(vSop)) );