summaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
Diffstat
-rw-r--r--src/base/abc/abcDfs.c2
-rw-r--r--src/base/abci/abcCollapse.c2
-rw-r--r--src/sat/bmc/bmcClp.c172
-rw-r--r--src/sat/bsat/satSolver.c2
-rw-r--r--src/sat/bsat/satSolver.h7
5 files changed, 132 insertions, 53 deletions
diff --git a/src/base/abc/abcDfs.c b/src/base/abc/abcDfs.c
index bb960ddc..e1b042b8 100644
--- a/src/base/abc/abcDfs.c
+++ b/src/base/abc/abcDfs.c
@@ -970,7 +970,7 @@ Vec_Int_t * Abc_NtkNodeSupportInt( Abc_Ntk_t * pNtk, int iCo )
int Abc_NtkFunctionalIsoGia_rec( Gia_Man_t * pNew, Abc_Obj_t * pNode )
{
int iLit0, iLit1;
- if ( Abc_NodeIsTravIdCurrent(pNode) || Abc_ObjFaninNum(pNode) == 0 )
+ if ( Abc_NodeIsTravIdCurrent(pNode) || Abc_ObjFaninNum(pNode) == 0 || Abc_ObjIsCi(pNode) )
return pNode->iTemp;
assert( Abc_ObjIsNode( pNode ) );
Abc_NodeSetTravIdCurrent( pNode );
diff --git a/src/base/abci/abcCollapse.c b/src/base/abci/abcCollapse.c
index e8ab3f7a..1536fe0c 100644
--- a/src/base/abci/abcCollapse.c
+++ b/src/base/abci/abcCollapse.c
@@ -256,7 +256,7 @@ Abc_Ntk_t * Abc_NtkCollapse( Abc_Ntk_t * pNtk, int fBddSizeMax, int fDualRail, i
int Abc_NtkClpOneGia_rec( Gia_Man_t * pNew, Abc_Obj_t * pNode )
{
int iLit0, iLit1;
- if ( Abc_NodeIsTravIdCurrent(pNode) || Abc_ObjFaninNum(pNode) == 0 )
+ if ( Abc_NodeIsTravIdCurrent(pNode) || Abc_ObjFaninNum(pNode) == 0 || Abc_ObjIsCi(pNode) )
return pNode->iTemp;
assert( Abc_ObjIsNode( pNode ) );
Abc_NodeSetTravIdCurrent( pNode );
diff --git a/src/sat/bmc/bmcClp.c b/src/sat/bmc/bmcClp.c
index d0948176..15cac4bb 100644
--- a/src/sat/bmc/bmcClp.c
+++ b/src/sat/bmc/bmcClp.c
@@ -38,7 +38,7 @@ extern Cnf_Dat_t * Mf_ManGenerateCnf( Gia_Man_t * pGia, int nLutSize, int fCnfOb
/**Function*************************************************************
- Synopsis []
+ Synopsis [Performs one round of removing literals.]
Description []
@@ -47,7 +47,7 @@ extern Cnf_Dat_t * Mf_ManGenerateCnf( Gia_Man_t * pGia, int nLutSize, int fCnfOb
SeeAlso []
***********************************************************************/
-int Bmc_CollapseExpandCanon( sat_solver * pSat, Vec_Int_t * vLits, Vec_Int_t * vNums, Vec_Int_t * vTemp, int nBTLimit )
+int Bmc_CollapseExpandRound( sat_solver * pSat, sat_solver * pSatOn, Vec_Int_t * vLits, Vec_Int_t * vNums, Vec_Int_t * vTemp, int nBTLimit, int fCanon )
{
int k, n, iLit, status;
// try removing one literal at a time
@@ -56,6 +56,26 @@ int Bmc_CollapseExpandCanon( sat_solver * pSat, Vec_Int_t * vLits, Vec_Int_t * v
int Save = Vec_IntEntry( vLits, k );
if ( Save == -1 )
continue;
+ // check if this literal when expanded overlaps with the on-set
+ if ( pSatOn )
+ {
+ // it is ok to skip the first round if the literal is positive
+ if ( fCanon && !Abc_LitIsCompl(Save) )
+ continue;
+ // put into new array
+ Vec_IntClear( vTemp );
+ Vec_IntForEachEntry( vLits, iLit, n )
+ if ( iLit != -1 )
+ Vec_IntPush( vTemp, Abc_LitNotCond(iLit, k==n) );
+ // check against onset
+ status = sat_solver_solve( pSatOn, Vec_IntArray(vTemp), Vec_IntLimit(vTemp), nBTLimit, 0, 0, 0 );
+ if ( status == l_Undef )
+ return -1;
+ //printf( "%d", status == l_True );
+ if ( status == l_False )
+ continue;
+ // otherwise keep trying to remove it
+ }
Vec_IntWriteEntry( vLits, k, -1 );
// put into new array
Vec_IntClear( vTemp );
@@ -69,6 +89,8 @@ int Bmc_CollapseExpandCanon( sat_solver * pSat, Vec_Int_t * vLits, Vec_Int_t * v
if ( status == l_True )
Vec_IntWriteEntry( vLits, k, Save );
}
+// if ( pSatOn )
+// printf( "\n" );
// put into new array
Vec_IntClear( vNums );
Vec_IntForEachEntry( vLits, iLit, n )
@@ -79,7 +101,7 @@ int Bmc_CollapseExpandCanon( sat_solver * pSat, Vec_Int_t * vLits, Vec_Int_t * v
/**Function*************************************************************
- Synopsis []
+ Synopsis [Expends minterm into a cube.]
Description []
@@ -88,44 +110,73 @@ int Bmc_CollapseExpandCanon( sat_solver * pSat, Vec_Int_t * vLits, Vec_Int_t * v
SeeAlso []
***********************************************************************/
-int Bmc_CollapseExpand( sat_solver * pSat, Vec_Int_t * vLits, Vec_Int_t * vNums, Vec_Int_t * vTemp, int nBTLimit )
+int Bmc_CollapseExpand( sat_solver * pSat, sat_solver * pSatOn, Vec_Int_t * vLits, Vec_Int_t * vNums, Vec_Int_t * vTemp, int nBTLimit, int fCanon )
{
- int i, k, iLit, status, nFinal, * pFinal;
- // check against offset
- status = sat_solver_solve( pSat, Vec_IntArray(vLits), Vec_IntLimit(vLits), nBTLimit, 0, 0, 0 );
- if ( status == l_Undef )
- return -1;
- assert( status == l_False );
- // get subset of literals
- nFinal = sat_solver_final( pSat, &pFinal );
-/*
- // collect literals
- Vec_IntClear( vNums );
- for ( i = 0; i < nFinal; i++ )
+ // perform one quick reduction if it is non-canonical
+ if ( !fCanon )
{
- iLit = Vec_IntFind( vLits, Abc_LitNot(pFinal[i]) );
- assert( iLit >= 0 );
- Vec_IntPush( vNums, iLit );
- }
-*/
- // mark unused literals
- Vec_IntForEachEntry( vLits, iLit, i )
- {
- for ( k = 0; k < nFinal; k++ )
- if ( iLit == Abc_LitNot(pFinal[k]) )
- break;
- if ( k == nFinal )
- Vec_IntWriteEntry( vLits, i, -1 );
+ int i, k, iLit, status, nFinal, * pFinal;
+ // check against offset
+ status = sat_solver_solve( pSat, Vec_IntArray(vLits), Vec_IntLimit(vLits), nBTLimit, 0, 0, 0 );
+ if ( status == l_Undef )
+ return -1;
+ assert( status == l_False );
+ // get subset of literals
+ nFinal = sat_solver_final( pSat, &pFinal );
+ // mark unused literals
+ Vec_IntForEachEntry( vLits, iLit, i )
+ {
+ for ( k = 0; k < nFinal; k++ )
+ if ( iLit == Abc_LitNot(pFinal[k]) )
+ break;
+ if ( k == nFinal )
+ Vec_IntWriteEntry( vLits, i, -1 );
+ }
}
- Bmc_CollapseExpandCanon( pSat, vLits, vNums, vTemp, nBTLimit );
+ Bmc_CollapseExpandRound( pSat, pSatOn, vLits, vNums, vTemp, nBTLimit, fCanon );
+ Bmc_CollapseExpandRound( pSat, NULL, vLits, vNums, vTemp, nBTLimit, fCanon );
+ return 0;
+}
-/*
- int i;
- Vec_IntClear( vNums );
+/**Function*************************************************************
+
+ Synopsis [Returns SAT solver in the 'sat' state with the given assignment.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Bmc_ComputeCanonical( 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++ )
- Vec_IntPush( vNums, i );
-*/
- return 0;
+ {
+ // copy the first i+1 literals
+ Vec_IntClear( vTemp );
+ Vec_IntForEachEntryStop( vLits, iLit, k, i+1 )
+ Vec_IntPush( vTemp, iLit );
+ // check if it satisfies the on-set
+ status = sat_solver_solve( pSat, Vec_IntArray(vTemp), Vec_IntLimit(vTemp), nBTLimit, 0, 0, 0 );
+ if ( status == l_Undef )
+ return l_Undef;
+ if ( status == l_True )
+ continue;
+ // if it is UNSAT, try the opposite literal
+ iLit = Vec_IntEntry( vLits, i );
+ // if literal is positive, there is no way to flip it
+ if ( !Abc_LitIsCompl(iLit) )
+ return l_False;
+ Vec_IntWriteEntry( vLits, i, Abc_LitNot(iLit) );
+ Vec_IntForEachEntryStart( vLits, iLit, k, i+1 )
+ Vec_IntWriteEntry( vLits, k, Abc_LitNot(Abc_LitRegular(iLit)) );
+ // recheck
+ i--;
+ }
+ assert( status == l_True );
+ return status;
}
/**Function*************************************************************
@@ -145,6 +196,7 @@ Vec_Str_t * Bmc_CollapseOneInt( Gia_Man_t * p, int nCubeLim, int nBTLimit, int f
int nVars = Gia_ManCiNum(p);
Vec_Int_t * vVars = Vec_IntAlloc( nVars );
Vec_Int_t * vLits = Vec_IntAlloc( nVars );
+ Vec_Int_t * vLitsC= Vec_IntAlloc( nVars );
Vec_Int_t * vNums = Vec_IntAlloc( nVars );
Vec_Int_t * vCube = Vec_IntAlloc( nVars );
Vec_Str_t * vSop = Vec_StrAlloc( 100 );
@@ -152,9 +204,10 @@ Vec_Str_t * Bmc_CollapseOneInt( Gia_Man_t * p, int nCubeLim, int nBTLimit, int f
// create SAT solver
Cnf_Dat_t * pCnf = Mf_ManGenerateCnf( p, 8, 0, 0, 0 );
- sat_solver * pSat[2] = {
+ sat_solver * pSat[3] = {
(sat_solver *)Cnf_DataWriteIntoSolver(pCnf, 1, 0),
- (sat_solver *)Cnf_DataWriteIntoSolver(pCnf, 1, 0)
+ (sat_solver *)Cnf_DataWriteIntoSolver(pCnf, 1, 0),
+ fCanon ? (sat_solver *)Cnf_DataWriteIntoSolver(pCnf, 1, 0) : NULL
};
// collect CI variables
@@ -162,14 +215,18 @@ Vec_Str_t * Bmc_CollapseOneInt( Gia_Man_t * p, int nCubeLim, int nBTLimit, int f
for ( n = 0; n < nVars; n++ )
Vec_IntPush( vVars, iCiVarBeg + n );
+ // start with all negative literals
+ Vec_IntForEachEntry( vVars, iVar, n )
+ Vec_IntPush( vLitsC, Abc_Var2Lit(iVar, 1) );
+
// check that on-set/off-set is sat
- for ( n = 0; n < 2; n++ )
+ for ( n = 0; n < 2 + fCanon; n++ )
{
- iLit = Abc_Var2Lit( iOut + 1, n ); // n=0 => F=1 n=1 => F=0
+ iLit = Abc_Var2Lit( iOut + 1, n&1 ); // n=0 => F=1 n=1 => F=0
status = sat_solver_addclause( pSat[n], &iLit, &iLit + 1 );
if ( status == 0 )
{
- Vec_StrPrintStr( vSop, (n ^ fCompl) ? " 1\n" : " 0\n" );
+ Vec_StrPrintStr( vSop, ((n&1) ^ fCompl) ? " 1\n" : " 0\n" );
Vec_StrPush( vSop, '\0' );
goto cleanup; // const0/1
}
@@ -181,7 +238,7 @@ Vec_Str_t * Bmc_CollapseOneInt( Gia_Man_t * p, int nCubeLim, int nBTLimit, int f
}
if ( status == l_False )
{
- Vec_StrPrintStr( vSop, (n ^ fCompl) ? " 1\n" : " 0\n" );
+ Vec_StrPrintStr( vSop, ((n&1) ^ fCompl) ? " 1\n" : " 0\n" );
Vec_StrPush( vSop, '\0' );
goto cleanup; // const0/1
}
@@ -189,13 +246,19 @@ Vec_Str_t * Bmc_CollapseOneInt( Gia_Man_t * p, int nCubeLim, int nBTLimit, int f
Vec_StrPush( vSop, '\0' );
// prepare on-set for solving
- if ( fCanon )
- sat_solver_prepare_enum( pSat[0], Vec_IntArray(vVars), Vec_IntSize(vVars) );
+// if ( fCanon )
+// sat_solver_prepare_enum( pSat[0], Vec_IntArray(vVars), Vec_IntSize(vVars) );
Count = 0;
while ( 1 )
{
// get the assignment
- status = sat_solver_solve( pSat[0], NULL, NULL, 0, 0, 0, 0 );
+ if ( fCanon )
+ status = Bmc_ComputeCanonical( pSat[0], vLitsC, vCube, nBTLimit );
+ else
+ {
+ sat_solver_clean_polarity( pSat[0], Vec_IntArray(vVars), Vec_IntSize(vVars) );
+ status = sat_solver_solve( pSat[0], NULL, NULL, 0, 0, 0, 0 );
+ }
if ( status == l_Undef )
{
Vec_StrFreeP( &vSop );
@@ -212,8 +275,13 @@ Vec_Str_t * Bmc_CollapseOneInt( Gia_Man_t * p, int nCubeLim, int nBTLimit, int f
}
// collect values
Vec_IntClear( vLits );
+ Vec_IntClear( vLitsC );
Vec_IntForEachEntry( vVars, iVar, n )
- Vec_IntPush( vLits, Abc_Var2Lit(iVar, !sat_solver_var_value(pSat[0], iVar)) );
+ {
+ iLit = Abc_Var2Lit(iVar, !sat_solver_var_value(pSat[0], iVar));
+ Vec_IntPush( vLits, iLit );
+ Vec_IntPush( vLitsC, iLit );
+ }
// print minterm
if ( fPrintMinterm )
{
@@ -223,10 +291,7 @@ Vec_Str_t * Bmc_CollapseOneInt( Gia_Man_t * p, int nCubeLim, int nBTLimit, int f
printf( "\n" );
}
// expand the values
- if ( fCanon )
- status = Bmc_CollapseExpandCanon( pSat[1], vLits, vNums, vCube, nBTLimit );
- else
- status = Bmc_CollapseExpand( pSat[1], vLits, vNums, vCube, nBTLimit );
+ status = Bmc_CollapseExpand( pSat[1], fCanon ? pSat[2] : pSat[0], vLits, vNums, vCube, nBTLimit, fCanon );
if ( status < 0 )
{
Vec_StrFreeP( &vSop );
@@ -254,15 +319,22 @@ Vec_Str_t * Bmc_CollapseOneInt( Gia_Man_t * p, int nCubeLim, int nBTLimit, int f
status = sat_solver_addclause( pSat[0], Vec_IntArray(vCube), Vec_IntLimit(vCube) );
if ( status == 0 )
break;
+ // add cube
+ if ( fCanon )
+ status = sat_solver_addclause( pSat[2], Vec_IntArray(vCube), Vec_IntLimit(vCube) );
+ assert( status == 1 );
}
//printf( "Finished enumerating %d assignments.\n", Count );
cleanup:
Vec_IntFree( vVars );
Vec_IntFree( vLits );
+ Vec_IntFree( vLitsC );
Vec_IntFree( vNums );
Vec_IntFree( vCube );
sat_solver_delete( pSat[0] );
sat_solver_delete( pSat[1] );
+ if ( fCanon )
+ sat_solver_delete( pSat[2] );
Cnf_DataFree( pCnf );
return vSop;
}
diff --git a/src/sat/bsat/satSolver.c b/src/sat/bsat/satSolver.c
index 053b0587..24c60dac 100644
--- a/src/sat/bsat/satSolver.c
+++ b/src/sat/bsat/satSolver.c
@@ -1861,7 +1861,7 @@ int sat_solver_solve(sat_solver* s, lit* begin, lit* end, ABC_INT64_T nConfLimit
int fConfl = sat_solver_propagate(s);
if (fConfl){
sat_solver_analyze_final(s, fConfl, 0);
- assert(s->conf_final.size > 0);
+ //assert(s->conf_final.size > 0);
sat_solver_canceluntil(s, 0);
return l_False; }
}
diff --git a/src/sat/bsat/satSolver.h b/src/sat/bsat/satSolver.h
index 8e171031..89391d2d 100644
--- a/src/sat/bsat/satSolver.h
+++ b/src/sat/bsat/satSolver.h
@@ -234,6 +234,13 @@ static void sat_solver_prepare_enum(sat_solver* s, int * pVars, int nVars )
for ( v = 0; v < nVars; v++ )
veci_push(&s->vDeciVars,pVars[v]);
}
+static void sat_solver_clean_polarity(sat_solver* s, int * pVars, int nVars )
+{
+ int i;
+ assert( veci_size(&s->vDeciVars) == 0 );
+ for ( i = 0; i < nVars; i++ )
+ s->polarity[pVars[i]] = 0;
+}
static int sat_solver_final(sat_solver* s, int ** ppArray)
{
generated by cgit v1.2.3 (git 2.25.1) at 2025-11-04 05:14:25 +0000