summaryrefslogtreecommitdiffstats
path: root/src/base/abci/abcSat.c
diff options
context:
space:
mode:
Diffstat (limited to 'src/base/abci/abcSat.c')
-rw-r--r--src/base/abci/abcSat.c294
1 files changed, 8 insertions, 286 deletions
diff --git a/src/base/abci/abcSat.c b/src/base/abci/abcSat.c
index 9c650aa9..5376444b 100644
--- a/src/base/abci/abcSat.c
+++ b/src/base/abci/abcSat.c
@@ -24,13 +24,7 @@
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
-static int Abc_NodeAddClauses( solver * pSat, char * pSop0, char * pSop1, Abc_Obj_t * pNode, Vec_Int_t * vVars );
-static int Abc_NodeAddClausesTop( solver * pSat, Abc_Obj_t * pNode, Vec_Int_t * vVars );
-
-static solver * Abc_NtkMiterSatCreate2( Abc_Ntk_t * pNtk );
-
static Vec_Int_t * Abc_NtkGetCiSatVarNums( Abc_Ntk_t * pNtk );
-
static nMuxes;
////////////////////////////////////////////////////////////////////////
@@ -48,13 +42,13 @@ static nMuxes;
SeeAlso []
***********************************************************************/
-int Abc_NtkMiterSat_OldAndRusty( Abc_Ntk_t * pNtk, int nSeconds, int fVerbose )
+int Abc_NtkMiterSat( Abc_Ntk_t * pNtk, int nConfLimit, int nImpLimit, int fVerbose )
{
solver * pSat;
lbool status;
int RetValue, clk;
- assert( Abc_NtkIsBddLogic(pNtk) );
+ assert( Abc_NtkIsStrash(pNtk) );
assert( Abc_NtkLatchNum(pNtk) == 0 );
if ( Abc_NtkPoNum(pNtk) > 1 )
@@ -84,7 +78,7 @@ int Abc_NtkMiterSat_OldAndRusty( Abc_Ntk_t * pNtk, int nSeconds, int fVerbose )
clk = clock();
if ( fVerbose )
pSat->verbosity = 1;
- status = solver_solve( pSat, NULL, NULL, nSeconds );
+ status = solver_solve( pSat, NULL, NULL, nConfLimit, nImpLimit );
if ( status == l_Undef )
{
// printf( "The problem timed out.\n" );
@@ -107,277 +101,6 @@ int Abc_NtkMiterSat_OldAndRusty( Abc_Ntk_t * pNtk, int nSeconds, int fVerbose )
// if the problem is SAT, get the counterexample
if ( status == l_True )
{
- Vec_Int_t * vCiIds = Abc_NtkGetCiIds( pNtk );
- pNtk->pModel = solver_get_model( pSat, vCiIds->pArray, vCiIds->nSize );
- Vec_IntFree( vCiIds );
- }
- // free the solver
- solver_delete( pSat );
- return RetValue;
-}
-
-/**Function*************************************************************
-
- Synopsis [Sets up the SAT solver.]
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-solver * Abc_NtkMiterSatCreate( Abc_Ntk_t * pNtk )
-{
- solver * pSat;
- Extra_MmFlex_t * pMmFlex;
- Abc_Obj_t * pNode;
- Vec_Str_t * vCube;
- Vec_Int_t * vVars;
- char * pSop0, * pSop1;
- int i, clk = clock();
-
- assert( Abc_NtkIsBddLogic(pNtk) );
-
- // start the data structures
- pSat = solver_new();
- pMmFlex = Extra_MmFlexStart();
- vCube = Vec_StrAlloc( 100 );
- vVars = Vec_IntAlloc( 100 );
-
- // add clauses for each internal nodes
- Abc_NtkForEachNode( pNtk, pNode, i )
- {
- // derive SOPs for both phases of the node
- Abc_NodeBddToCnf( pNode, pMmFlex, vCube, &pSop0, &pSop1 );
- // add the clauses to the solver
- if ( !Abc_NodeAddClauses( pSat, pSop0, pSop1, pNode, vVars ) )
- {
- solver_delete( pSat );
- return NULL;
- }
- }
- // add clauses for the POs
- if ( !Abc_NodeAddClausesTop( pSat, Abc_NtkPo(pNtk, Abc_NtkPoNum(pNtk)-1), vVars ) )
- {
- solver_delete( pSat );
- return NULL;
- }
-// Asat_SolverWriteDimacs( pSat, "test.cnf", NULL, NULL, 0 );
-
- PRT( "Creating solver", clock() - clk );
-
- // delete
- Vec_StrFree( vCube );
- Vec_IntFree( vVars );
- Extra_MmFlexStop( pMmFlex, 0 );
- return pSat;
-}
-
-/**Function*************************************************************
-
- Synopsis [Adds clauses for the internal node.]
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-int Abc_NodeAddClauses( solver * pSat, char * pSop0, char * pSop1, Abc_Obj_t * pNode, Vec_Int_t * vVars )
-{
- Abc_Obj_t * pFanin;
- int i, c, nFanins;
- char * pCube;
-
- nFanins = Abc_ObjFaninNum( pNode );
- assert( nFanins == Abc_SopGetVarNum( pSop0 ) );
-
- if ( nFanins == 0 )
- {
- vVars->nSize = 0;
- if ( Abc_SopIsConst1(pSop1) )
- Vec_IntPush( vVars, toLit(pNode->Id) );
- else
- Vec_IntPush( vVars, neg(toLit(pNode->Id)) );
- return solver_addclause( pSat, vVars->pArray, vVars->pArray + vVars->nSize );
- }
-
- // add clauses for the negative phase
- for ( c = 0; ; c++ )
- {
- // get the cube
- pCube = pSop0 + c * (nFanins + 3);
- if ( *pCube == 0 )
- break;
- // add the clause
- vVars->nSize = 0;
- Abc_ObjForEachFanin( pNode, pFanin, i )
- {
- if ( pCube[i] == '0' )
- Vec_IntPush( vVars, toLit(pFanin->Id) );
- else if ( pCube[i] == '1' )
- Vec_IntPush( vVars, neg(toLit(pFanin->Id)) );
- }
- Vec_IntPush( vVars, neg(toLit(pNode->Id)) );
- if ( !solver_addclause( pSat, vVars->pArray, vVars->pArray + vVars->nSize ) )
- return 0;
- }
-
- // add clauses for the positive phase
- for ( c = 0; ; c++ )
- {
- // get the cube
- pCube = pSop1 + c * (nFanins + 3);
- if ( *pCube == 0 )
- break;
- // add the clause
- vVars->nSize = 0;
- Abc_ObjForEachFanin( pNode, pFanin, i )
- {
- if ( pCube[i] == '0' )
- Vec_IntPush( vVars, toLit(pFanin->Id) );
- else if ( pCube[i] == '1' )
- Vec_IntPush( vVars, neg(toLit(pFanin->Id)) );
- }
- Vec_IntPush( vVars, toLit(pNode->Id) );
- if ( !solver_addclause( pSat, vVars->pArray, vVars->pArray + vVars->nSize ) )
- return 0;
- }
- return 1;
-}
-
-/**Function*************************************************************
-
- Synopsis [Adds clauses for the PO node.]
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-int Abc_NodeAddClausesTop( solver * pSat, Abc_Obj_t * pNode, Vec_Int_t * vVars )
-{
- Abc_Obj_t * pFanin;
-
- pFanin = Abc_ObjFanin0(pNode);
- if ( Abc_ObjFaninC0(pNode) )
- {
- vVars->nSize = 0;
- Vec_IntPush( vVars, toLit(pFanin->Id) );
- Vec_IntPush( vVars, toLit(pNode->Id) );
- if ( !solver_addclause( pSat, vVars->pArray, vVars->pArray + vVars->nSize ) )
- return 0;
-
- vVars->nSize = 0;
- Vec_IntPush( vVars, neg(toLit(pFanin->Id)) );
- Vec_IntPush( vVars, neg(toLit(pNode->Id)) );
- if ( !solver_addclause( pSat, vVars->pArray, vVars->pArray + vVars->nSize ) )
- return 0;
- }
- else
- {
- vVars->nSize = 0;
- Vec_IntPush( vVars, neg(toLit(pFanin->Id)) );
- Vec_IntPush( vVars, toLit(pNode->Id) );
- if ( !solver_addclause( pSat, vVars->pArray, vVars->pArray + vVars->nSize ) )
- return 0;
-
- vVars->nSize = 0;
- Vec_IntPush( vVars, toLit(pFanin->Id) );
- Vec_IntPush( vVars, neg(toLit(pNode->Id)) );
- if ( !solver_addclause( pSat, vVars->pArray, vVars->pArray + vVars->nSize ) )
- return 0;
- }
-
- vVars->nSize = 0;
- Vec_IntPush( vVars, toLit(pNode->Id) );
- return solver_addclause( pSat, vVars->pArray, vVars->pArray + vVars->nSize );
-}
-
-
-
-
-
-
-
-
-
-
-
-/**Function*************************************************************
-
- Synopsis [Attempts to solve the miter using an internal SAT solver.]
-
- Description [Returns -1 if timed out; 0 if SAT; 1 if UNSAT.]
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-int Abc_NtkMiterSat( Abc_Ntk_t * pNtk, int nSeconds, int fVerbose )
-{
- solver * pSat;
- lbool status;
- int RetValue, clk;
-
- assert( Abc_NtkIsStrash(pNtk) );
- assert( Abc_NtkLatchNum(pNtk) == 0 );
-
- if ( Abc_NtkPoNum(pNtk) > 1 )
- fprintf( stdout, "Warning: The miter has %d outputs. SAT will try to prove all of them.\n", Abc_NtkPoNum(pNtk) );
-
- // load clauses into the solver
- clk = clock();
- pSat = Abc_NtkMiterSatCreate2( pNtk );
- if ( pSat == NULL )
- return 1;
-// printf( "Created SAT problem with %d variable and %d clauses. ", solver_nvars(pSat), solver_nclauses(pSat) );
-// PRT( "Time", clock() - clk );
-
- // simplify the problem
- clk = clock();
- status = solver_simplify(pSat);
-// printf( "Simplified the problem to %d variables and %d clauses. ", solver_nvars(pSat), solver_nclauses(pSat) );
-// PRT( "Time", clock() - clk );
- if ( status == 0 )
- {
- solver_delete( pSat );
-// printf( "The problem is UNSATISFIABLE after simplification.\n" );
- return 1;
- }
-
- // solve the miter
- clk = clock();
- if ( fVerbose )
- pSat->verbosity = 1;
- status = solver_solve( pSat, NULL, NULL, nSeconds );
- if ( status == l_Undef )
- {
-// printf( "The problem timed out.\n" );
- RetValue = -1;
- }
- else if ( status == l_True )
- {
-// printf( "The problem is SATISFIABLE.\n" );
- RetValue = 0;
- }
- else if ( status == l_False )
- {
-// printf( "The problem is UNSATISFIABLE.\n" );
- RetValue = 1;
- }
- else
- assert( 0 );
- PRT( "SAT solver time", clock() - clk );
-
- // if the problem is SAT, get the counterexample
- if ( status == l_True )
- {
// Vec_Int_t * vCiIds = Abc_NtkGetCiIds( pNtk );
Vec_Int_t * vCiIds = Abc_NtkGetCiSatVarNums( pNtk );
pNtk->pModel = solver_get_model( pSat, vCiIds->pArray, vCiIds->nSize );
@@ -411,7 +134,6 @@ Vec_Int_t * Abc_NtkGetCiSatVarNums( Abc_Ntk_t * pNtk )
}
-
/**Function*************************************************************
@@ -669,7 +391,7 @@ void Abc_NtkCollectSupergate( Abc_Obj_t * pNode, int fStopAtMux, Vec_Ptr_t * vNo
SeeAlso []
***********************************************************************/
-int Abc_NtkMiterSatCreate2Int( solver * pSat, Abc_Ntk_t * pNtk )
+int Abc_NtkMiterSatCreateInt( solver * pSat, Abc_Ntk_t * pNtk )
{
Abc_Obj_t * pNode, * pFanin, * pNodeC, * pNodeT, * pNodeE;
Vec_Ptr_t * vNodes, * vSuper;
@@ -787,7 +509,7 @@ int Abc_NtkMiterSatCreate2Int( solver * pSat, Abc_Ntk_t * pNtk )
SeeAlso []
***********************************************************************/
-solver * Abc_NtkMiterSatCreate2( Abc_Ntk_t * pNtk )
+solver * Abc_NtkMiterSatCreate( Abc_Ntk_t * pNtk )
{
solver * pSat;
Abc_Obj_t * pNode;
@@ -796,7 +518,7 @@ solver * Abc_NtkMiterSatCreate2( Abc_Ntk_t * pNtk )
nMuxes = 0;
pSat = solver_new();
- RetValue = Abc_NtkMiterSatCreate2Int( pSat, pNtk );
+ RetValue = Abc_NtkMiterSatCreateInt( pSat, pNtk );
Abc_NtkForEachObj( pNtk, pNode, i )
pNode->fMarkA = 0;
// Asat_SolverWriteDimacs( pSat, "temp_sat.cnf", NULL, NULL, 1 );
@@ -805,8 +527,8 @@ solver * Abc_NtkMiterSatCreate2( Abc_Ntk_t * pNtk )
solver_delete(pSat);
return NULL;
}
- printf( "The number of MUXes detected = %d (%5.2f %% of logic). ", nMuxes, 300.0*nMuxes/Abc_NtkNodeNum(pNtk) );
- PRT( "Creating solver", clock() - clk );
+// printf( "Ands = %6d. Muxes = %6d (%5.2f %%). ", Abc_NtkNodeNum(pNtk), nMuxes, 300.0*nMuxes/Abc_NtkNodeNum(pNtk) );
+// PRT( "Creating solver", clock() - clk );
return pSat;
}
generated by cgit v1.2.3 (git 2.25.1) at 2024-06-30 18:53:15 +0000