diff options
Diffstat (limited to 'src/base/abci/abcSat.c')
-rw-r--r-- | src/base/abci/abcSat.c | 229 |
1 files changed, 88 insertions, 141 deletions
diff --git a/src/base/abci/abcSat.c b/src/base/abci/abcSat.c index cf67db6d..96540269 100644 --- a/src/base/abci/abcSat.c +++ b/src/base/abci/abcSat.c @@ -6,7 +6,7 @@ PackageName [Network and node package.] - Synopsis [Procedures to solve the miter using the internal SAT solver.] + Synopsis [Procedures to solve the miter using the internal SAT sat_solver.] Author [Alan Mishchenko] @@ -19,12 +19,13 @@ ***********************************************************************/ #include "abc.h" +#include "satSolver.h" //////////////////////////////////////////////////////////////////////// /// DECLARATIONS /// //////////////////////////////////////////////////////////////////////// -static solver * Abc_NtkMiterSatCreateLogic( Abc_Ntk_t * pNtk, int fAllPrimes ); +static sat_solver * Abc_NtkMiterSatCreateLogic( Abc_Ntk_t * pNtk, int fAllPrimes ); extern Vec_Int_t * Abc_NtkGetCiSatVarNums( Abc_Ntk_t * pNtk ); static nMuxes; @@ -34,7 +35,7 @@ static nMuxes; /**Function************************************************************* - Synopsis [Attempts to solve the miter using an internal SAT solver.] + Synopsis [Attempts to solve the miter using an internal SAT sat_solver.] Description [Returns -1 if timed out; 0 if SAT; 1 if UNSAT.] @@ -43,9 +44,9 @@ static nMuxes; SeeAlso [] ***********************************************************************/ -int Abc_NtkMiterSat( Abc_Ntk_t * pNtk, sint64 nConfLimit, sint64 nInsLimit, int fJFront, int fVerbose, sint64 * pNumConfs, sint64 * pNumInspects ) +int Abc_NtkMiterSat( Abc_Ntk_t * pNtk, sint64 nConfLimit, sint64 nInsLimit, int fVerbose, sint64 * pNumConfs, sint64 * pNumInspects ) { - solver * pSat; + sat_solver * pSat; lbool status; int RetValue, clk; @@ -59,22 +60,22 @@ int Abc_NtkMiterSat( Abc_Ntk_t * pNtk, sint64 nConfLimit, sint64 nInsLimit, int // 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 + // load clauses into the sat_solver clk = clock(); - pSat = Abc_NtkMiterSatCreate( pNtk, fJFront, 0 ); + pSat = Abc_NtkMiterSatCreate( pNtk, 0 ); if ( pSat == NULL ) return 1; -// printf( "Created SAT problem with %d variable and %d clauses. ", solver_nvars(pSat), solver_nclauses(pSat) ); +// printf( "Created SAT problem with %d variable and %d clauses. ", sat_solver_nvars(pSat), sat_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) ); + status = sat_solver_simplify(pSat); +// printf( "Simplified the problem to %d variables and %d clauses. ", sat_solver_nvars(pSat), sat_solver_nclauses(pSat) ); // PRT( "Time", clock() - clk ); if ( status == 0 ) { - solver_delete( pSat ); + sat_solver_delete( pSat ); // printf( "The problem is UNSATISFIABLE after simplification.\n" ); return 1; } @@ -83,7 +84,7 @@ int Abc_NtkMiterSat( Abc_Ntk_t * pNtk, sint64 nConfLimit, sint64 nInsLimit, int clk = clock(); if ( fVerbose ) pSat->verbosity = 1; - status = solver_solve( pSat, NULL, NULL, (sint64)nConfLimit, (sint64)nInsLimit ); + status = sat_solver_solve( pSat, NULL, NULL, (sint64)nConfLimit, (sint64)nInsLimit, (sint64)0, (sint64)0 ); if ( status == l_Undef ) { // printf( "The problem timed out.\n" ); @@ -101,30 +102,30 @@ int Abc_NtkMiterSat( Abc_Ntk_t * pNtk, sint64 nConfLimit, sint64 nInsLimit, int } else assert( 0 ); -// PRT( "SAT solver time", clock() - clk ); -// printf( "The number of conflicts = %d.\n", (int)pSat->solver_stats.conflicts ); +// PRT( "SAT sat_solver time", clock() - clk ); +// printf( "The number of conflicts = %d.\n", (int)pSat->sat_solver_stats.conflicts ); // 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 ); + pNtk->pModel = Sat_SolverGetModel( pSat, vCiIds->pArray, vCiIds->nSize ); Vec_IntFree( vCiIds ); } - // free the solver + // free the sat_solver if ( fVerbose ) - Asat_SatPrintStats( stdout, pSat ); + Sat_SolverPrintStats( stdout, pSat ); if ( pNumConfs ) - *pNumConfs = (int)pSat->solver_stats.conflicts; + *pNumConfs = (int)pSat->stats.conflicts; if ( pNumInspects ) - *pNumInspects = (int)pSat->solver_stats.inspects; + *pNumInspects = (int)pSat->stats.inspects; -Sat_SolverTraceWrite( pSat, NULL, NULL, 0 ); -Sat_SolverTraceStop( pSat ); +sat_solver_store_write( pSat, "trace.cnf" ); +sat_solver_store_free( pSat ); - solver_delete( pSat ); + sat_solver_delete( pSat ); return RetValue; } @@ -163,13 +164,13 @@ Vec_Int_t * Abc_NtkGetCiSatVarNums( Abc_Ntk_t * pNtk ) SeeAlso [] ***********************************************************************/ -int Abc_NtkClauseTriv( solver * pSat, Abc_Obj_t * pNode, Vec_Int_t * vVars ) +int Abc_NtkClauseTriv( sat_solver * pSat, Abc_Obj_t * pNode, Vec_Int_t * vVars ) { -//printf( "Adding triv %d. %d\n", Abc_ObjRegular(pNode)->Id, (int)pSat->solver_stats.clauses ); +//printf( "Adding triv %d. %d\n", Abc_ObjRegular(pNode)->Id, (int)pSat->sat_solver_stats.clauses ); vVars->nSize = 0; Vec_IntPush( vVars, toLitCond( (int)Abc_ObjRegular(pNode)->pCopy, Abc_ObjIsComplement(pNode) ) ); // Vec_IntPush( vVars, toLitCond( (int)Abc_ObjRegular(pNode)->Id, Abc_ObjIsComplement(pNode) ) ); - return solver_addclause( pSat, vVars->pArray, vVars->pArray + vVars->nSize ); + return sat_solver_addclause( pSat, vVars->pArray, vVars->pArray + vVars->nSize ); } /**Function************************************************************* @@ -183,16 +184,16 @@ int Abc_NtkClauseTriv( solver * pSat, Abc_Obj_t * pNode, Vec_Int_t * vVars ) SeeAlso [] ***********************************************************************/ -int Abc_NtkClauseTop( solver * pSat, Vec_Ptr_t * vNodes, Vec_Int_t * vVars ) +int Abc_NtkClauseTop( sat_solver * pSat, Vec_Ptr_t * vNodes, Vec_Int_t * vVars ) { Abc_Obj_t * pNode; int i; -//printf( "Adding triv %d. %d\n", Abc_ObjRegular(pNode)->Id, (int)pSat->solver_stats.clauses ); +//printf( "Adding triv %d. %d\n", Abc_ObjRegular(pNode)->Id, (int)pSat->sat_solver_stats.clauses ); vVars->nSize = 0; Vec_PtrForEachEntry( vNodes, pNode, i ) Vec_IntPush( vVars, toLitCond( (int)Abc_ObjRegular(pNode)->pCopy, Abc_ObjIsComplement(pNode) ) ); // Vec_IntPush( vVars, toLitCond( (int)Abc_ObjRegular(pNode)->Id, Abc_ObjIsComplement(pNode) ) ); - return solver_addclause( pSat, vVars->pArray, vVars->pArray + vVars->nSize ); + return sat_solver_addclause( pSat, vVars->pArray, vVars->pArray + vVars->nSize ); } /**Function************************************************************* @@ -206,15 +207,15 @@ int Abc_NtkClauseTop( solver * pSat, Vec_Ptr_t * vNodes, Vec_Int_t * vVars ) SeeAlso [] ***********************************************************************/ -int Abc_NtkClauseAnd( solver * pSat, Abc_Obj_t * pNode, Vec_Ptr_t * vSuper, Vec_Int_t * vVars ) +int Abc_NtkClauseAnd( sat_solver * pSat, Abc_Obj_t * pNode, Vec_Ptr_t * vSuper, Vec_Int_t * vVars ) { int fComp1, Var, Var1, i; -//printf( "Adding AND %d. (%d) %d\n", pNode->Id, vSuper->nSize+1, (int)pSat->solver_stats.clauses ); +//printf( "Adding AND %d. (%d) %d\n", pNode->Id, vSuper->nSize+1, (int)pSat->sat_solver_stats.clauses ); assert( !Abc_ObjIsComplement( pNode ) ); assert( Abc_ObjIsNode( pNode ) ); -// nVars = solver_nvars(pSat); +// nVars = sat_solver_nvars(pSat); Var = (int)pNode->pCopy; // Var = pNode->Id; @@ -237,7 +238,7 @@ int Abc_NtkClauseAnd( solver * pSat, Abc_Obj_t * pNode, Vec_Ptr_t * vSuper, Vec_ vVars->nSize = 0; Vec_IntPush( vVars, toLitCond(Var1, fComp1) ); Vec_IntPush( vVars, toLitCond(Var, 1 ) ); - if ( !solver_addclause( pSat, vVars->pArray, vVars->pArray + vVars->nSize ) ) + if ( !sat_solver_addclause( pSat, vVars->pArray, vVars->pArray + vVars->nSize ) ) return 0; } @@ -256,7 +257,7 @@ int Abc_NtkClauseAnd( solver * pSat, Abc_Obj_t * pNode, Vec_Ptr_t * vSuper, Vec_ Vec_IntPush( vVars, toLitCond(Var1, !fComp1) ); } Vec_IntPush( vVars, toLitCond(Var, 0) ); - return solver_addclause( pSat, vVars->pArray, vVars->pArray + vVars->nSize ); + return sat_solver_addclause( pSat, vVars->pArray, vVars->pArray + vVars->nSize ); } /**Function************************************************************* @@ -270,10 +271,10 @@ int Abc_NtkClauseAnd( solver * pSat, Abc_Obj_t * pNode, Vec_Ptr_t * vSuper, Vec_ SeeAlso [] ***********************************************************************/ -int Abc_NtkClauseMux( solver * pSat, Abc_Obj_t * pNode, Abc_Obj_t * pNodeC, Abc_Obj_t * pNodeT, Abc_Obj_t * pNodeE, Vec_Int_t * vVars ) +int Abc_NtkClauseMux( sat_solver * pSat, Abc_Obj_t * pNode, Abc_Obj_t * pNodeC, Abc_Obj_t * pNodeT, Abc_Obj_t * pNodeE, Vec_Int_t * vVars ) { int VarF, VarI, VarT, VarE, fCompT, fCompE; -//printf( "Adding mux %d. %d\n", pNode->Id, (int)pSat->solver_stats.clauses ); +//printf( "Adding mux %d. %d\n", pNode->Id, (int)pSat->sat_solver_stats.clauses ); assert( !Abc_ObjIsComplement( pNode ) ); assert( Abc_NodeIsMuxType( pNode ) ); @@ -301,25 +302,25 @@ int Abc_NtkClauseMux( solver * pSat, Abc_Obj_t * pNode, Abc_Obj_t * pNodeC, Abc_ Vec_IntPush( vVars, toLitCond(VarI, 1) ); Vec_IntPush( vVars, toLitCond(VarT, 1^fCompT) ); Vec_IntPush( vVars, toLitCond(VarF, 0) ); - if ( !solver_addclause( pSat, vVars->pArray, vVars->pArray + vVars->nSize ) ) + if ( !sat_solver_addclause( pSat, vVars->pArray, vVars->pArray + vVars->nSize ) ) return 0; vVars->nSize = 0; Vec_IntPush( vVars, toLitCond(VarI, 1) ); Vec_IntPush( vVars, toLitCond(VarT, 0^fCompT) ); Vec_IntPush( vVars, toLitCond(VarF, 1) ); - if ( !solver_addclause( pSat, vVars->pArray, vVars->pArray + vVars->nSize ) ) + if ( !sat_solver_addclause( pSat, vVars->pArray, vVars->pArray + vVars->nSize ) ) return 0; vVars->nSize = 0; Vec_IntPush( vVars, toLitCond(VarI, 0) ); Vec_IntPush( vVars, toLitCond(VarE, 1^fCompE) ); Vec_IntPush( vVars, toLitCond(VarF, 0) ); - if ( !solver_addclause( pSat, vVars->pArray, vVars->pArray + vVars->nSize ) ) + if ( !sat_solver_addclause( pSat, vVars->pArray, vVars->pArray + vVars->nSize ) ) return 0; vVars->nSize = 0; Vec_IntPush( vVars, toLitCond(VarI, 0) ); Vec_IntPush( vVars, toLitCond(VarE, 0^fCompE) ); Vec_IntPush( vVars, toLitCond(VarF, 1) ); - if ( !solver_addclause( pSat, vVars->pArray, vVars->pArray + vVars->nSize ) ) + if ( !sat_solver_addclause( pSat, vVars->pArray, vVars->pArray + vVars->nSize ) ) return 0; if ( VarT == VarE ) @@ -335,13 +336,13 @@ int Abc_NtkClauseMux( solver * pSat, Abc_Obj_t * pNode, Abc_Obj_t * pNodeC, Abc_ Vec_IntPush( vVars, toLitCond(VarT, 0^fCompT) ); Vec_IntPush( vVars, toLitCond(VarE, 0^fCompE) ); Vec_IntPush( vVars, toLitCond(VarF, 1) ); - if ( !solver_addclause( pSat, vVars->pArray, vVars->pArray + vVars->nSize ) ) + if ( !sat_solver_addclause( pSat, vVars->pArray, vVars->pArray + vVars->nSize ) ) return 0; vVars->nSize = 0; Vec_IntPush( vVars, toLitCond(VarT, 1^fCompT) ); Vec_IntPush( vVars, toLitCond(VarE, 1^fCompE) ); Vec_IntPush( vVars, toLitCond(VarF, 0) ); - return solver_addclause( pSat, vVars->pArray, vVars->pArray + vVars->nSize ); + return sat_solver_addclause( pSat, vVars->pArray, vVars->pArray + vVars->nSize ); } /**Function************************************************************* @@ -442,7 +443,7 @@ int Abc_NtkNodeFactor( Abc_Obj_t * pObj, int nLevelMax ) /**Function************************************************************* - Synopsis [Sets up the SAT solver.] + Synopsis [Sets up the SAT sat_solver.] Description [] @@ -451,16 +452,14 @@ int Abc_NtkNodeFactor( Abc_Obj_t * pObj, int nLevelMax ) SeeAlso [] ***********************************************************************/ -int Abc_NtkMiterSatCreateInt( solver * pSat, Abc_Ntk_t * pNtk, int fJFront ) +int Abc_NtkMiterSatCreateInt( sat_solver * pSat, Abc_Ntk_t * pNtk ) { Abc_Obj_t * pNode, * pFanin, * pNodeC, * pNodeT, * pNodeE; Vec_Ptr_t * vNodes, * vSuper; - Vec_Flt_t * vFactors; - Vec_Int_t * vVars, * vFanio; - Vec_Vec_t * vCircuit; + Vec_Int_t * vVars; int i, k, fUseMuxes = 1; - int clk1 = clock(), clk; - int fOrderCiVarsFirst = 0; + int clk1 = clock(); +// int fOrderCiVarsFirst = 0; int nLevelsMax = Abc_AigLevel(pNtk); int RetValue = 0; @@ -471,12 +470,9 @@ int Abc_NtkMiterSatCreateInt( solver * pSat, Abc_Ntk_t * pNtk, int fJFront ) pNode->pCopy = NULL; // start the data structures - vNodes = Vec_PtrAlloc( 1000 ); // the nodes corresponding to vars in the solver + vNodes = Vec_PtrAlloc( 1000 ); // the nodes corresponding to vars in the sat_solver vSuper = Vec_PtrAlloc( 100 ); // the nodes belonging to the given implication supergate vVars = Vec_IntAlloc( 100 ); // the temporary array for variables in the clause - if ( fJFront ) - vCircuit = Vec_VecAlloc( 1000 ); -// vCircuit = Vec_VecStart( 184 ); // add the clause for the constant node pNode = Abc_AigConst1(pNtk); @@ -574,23 +570,8 @@ int Abc_NtkMiterSatCreateInt( solver * pSat, Abc_Ntk_t * pNtk, int fJFront ) goto Quits; } } - // add the variables to the J-frontier - if ( !fJFront ) - continue; - // make sure that the fanin entries go first - assert( pNode->pCopy ); - Vec_VecExpand( vCircuit, (int)pNode->pCopy ); - vFanio = Vec_VecEntry( vCircuit, (int)pNode->pCopy ); - Vec_PtrForEachEntryReverse( vSuper, pFanin, k ) -// Vec_PtrForEachEntry( vSuper, pFanin, k ) - { - pFanin = Abc_ObjRegular( pFanin ); - assert( pFanin->pCopy && pFanin->pCopy != pNode->pCopy ); - Vec_IntPushFirst( vFanio, (int)pFanin->pCopy ); - Vec_VecPush( vCircuit, (int)pFanin->pCopy, pNode->pCopy ); - } } - +/* // set preferred variables if ( fOrderCiVarsFirst ) { @@ -603,45 +584,8 @@ int Abc_NtkMiterSatCreateInt( solver * pSat, Abc_Ntk_t * pNtk, int fJFront ) pPrefVars[nVars++] = (int)pNode->pCopy; } nVars = ABC_MIN( nVars, 10 ); - Asat_SolverSetPrefVars( pSat, pPrefVars, nVars ); - } - - // create the variable order - if ( fJFront ) - { - clk = clock(); - Asat_JManStart( pSat, vCircuit ); - Vec_VecFree( vCircuit ); - PRT( "Setup", clock() - clk ); -// Asat_JManStop( pSat ); -// PRT( "Total", clock() - clk1 ); + ASat_SolverSetPrefVars( pSat, pPrefVars, nVars ); } - - Abc_NtkStartReverseLevels( pNtk ); - vFactors = Vec_FltStart( solver_nvars(pSat) ); - Abc_NtkForEachNode( pNtk, pNode, i ) - if ( pNode->fMarkA ) - Vec_FltWriteEntry( vFactors, (int)pNode->pCopy, (float)pow(0.97, Abc_NodeReadReverseLevel(pNode)) ); - Abc_NtkForEachCi( pNtk, pNode, i ) - if ( pNode->fMarkA ) - Vec_FltWriteEntry( vFactors, (int)pNode->pCopy, (float)pow(0.97, nLevelsMax+1) ); - // set the PI levels -// Abc_NtkForEachObj( pNtk, pNode, i ) -// if ( pNode->fMarkA ) -// printf( "(%d) %.3f ", Abc_NodeReadReverseLevel(pNode), Vec_FltEntry(vFactors, (int)pNode->pCopy) ); -// printf( "\n" ); - Asat_SolverSetFactors( pSat, Vec_FltReleaseArray(vFactors) ); - Vec_FltFree( vFactors ); - -/* - // create factors - vLevels = Vec_IntStart( Vec_PtrSize(vNodes) ); // the reverse levels of the nodes - Abc_NtkForEachObj( pNtk, pNode, i ) - if ( pNode->fMarkA ) - Vec_IntWriteEntry( vLevels, (int)pNode->pCopy, Abc_NtkNodeFactor(pNode, nLevelsMax) ); - assert( Vec_PtrSize(vNodes) == Vec_IntSize(vLevels) ); - Asat_SolverSetFactors( pSat, Vec_IntReleaseArray(vLevels) ); - Vec_IntFree( vLevels ); */ RetValue = 1; Quits : @@ -654,7 +598,7 @@ Quits : /**Function************************************************************* - Synopsis [Sets up the SAT solver.] + Synopsis [Sets up the SAT sat_solver.] Description [] @@ -663,9 +607,9 @@ Quits : SeeAlso [] ***********************************************************************/ -solver * Abc_NtkMiterSatCreate( Abc_Ntk_t * pNtk, int fJFront, int fAllPrimes ) +void * Abc_NtkMiterSatCreate( Abc_Ntk_t * pNtk, int fAllPrimes ) { - solver * pSat; + sat_solver * pSat; Abc_Obj_t * pNode; int RetValue, i, clk = clock(); @@ -674,18 +618,21 @@ solver * Abc_NtkMiterSatCreate( Abc_Ntk_t * pNtk, int fJFront, int fAllPrimes ) return Abc_NtkMiterSatCreateLogic(pNtk, fAllPrimes); nMuxes = 0; - pSat = solver_new(); - RetValue = Abc_NtkMiterSatCreateInt( pSat, pNtk, fJFront ); + pSat = sat_solver_new(); +sat_solver_store_alloc( pSat ); + RetValue = Abc_NtkMiterSatCreateInt( pSat, pNtk ); +sat_solver_store_mark_roots( pSat ); + Abc_NtkForEachObj( pNtk, pNode, i ) pNode->fMarkA = 0; -// Asat_SolverWriteDimacs( pSat, "temp_sat.cnf", NULL, NULL, 1 ); +// ASat_SolverWriteDimacs( pSat, "temp_sat.cnf", NULL, NULL, 1 ); if ( RetValue == 0 ) { - solver_delete(pSat); + sat_solver_delete(pSat); return NULL; } // printf( "Ands = %6d. Muxes = %6d (%5.2f %%). ", Abc_NtkNodeNum(pNtk), nMuxes, 300.0*nMuxes/Abc_NtkNodeNum(pNtk) ); -// PRT( "Creating solver", clock() - clk ); +// PRT( "Creating sat_solver", clock() - clk ); return pSat; } @@ -703,7 +650,7 @@ solver * Abc_NtkMiterSatCreate( Abc_Ntk_t * pNtk, int fJFront, int fAllPrimes ) SeeAlso [] ***********************************************************************/ -int Abc_NodeAddClauses( solver * pSat, char * pSop0, char * pSop1, Abc_Obj_t * pNode, Vec_Int_t * vVars ) +int Abc_NodeAddClauses( sat_solver * pSat, char * pSop0, char * pSop1, Abc_Obj_t * pNode, Vec_Int_t * vVars ) { Abc_Obj_t * pFanin; int i, c, nFanins; @@ -721,8 +668,8 @@ int Abc_NodeAddClauses( solver * pSat, char * pSop0, char * pSop1, Abc_Obj_t * p if ( !Cudd_IsComplement(pNode->pData) ) Vec_IntPush( vVars, toLit(pNode->Id) ); else - Vec_IntPush( vVars, neg(toLit(pNode->Id)) ); - RetValue = solver_addclause( pSat, vVars->pArray, vVars->pArray + vVars->nSize ); + Vec_IntPush( vVars, lit_neg(toLit(pNode->Id)) ); + RetValue = sat_solver_addclause( pSat, vVars->pArray, vVars->pArray + vVars->nSize ); if ( !RetValue ) { printf( "The CNF is trivially UNSAT.\n" ); @@ -745,10 +692,10 @@ int Abc_NodeAddClauses( solver * pSat, char * pSop0, char * pSop1, Abc_Obj_t * p 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, lit_neg(toLit(pFanin->Id)) ); } - Vec_IntPush( vVars, neg(toLit(pNode->Id)) ); - RetValue = solver_addclause( pSat, vVars->pArray, vVars->pArray + vVars->nSize ); + Vec_IntPush( vVars, lit_neg(toLit(pNode->Id)) ); + RetValue = sat_solver_addclause( pSat, vVars->pArray, vVars->pArray + vVars->nSize ); if ( !RetValue ) { printf( "The CNF is trivially UNSAT.\n" ); @@ -770,10 +717,10 @@ int Abc_NodeAddClauses( solver * pSat, char * pSop0, char * pSop1, Abc_Obj_t * p 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, lit_neg(toLit(pFanin->Id)) ); } Vec_IntPush( vVars, toLit(pNode->Id) ); - RetValue = solver_addclause( pSat, vVars->pArray, vVars->pArray + vVars->nSize ); + RetValue = sat_solver_addclause( pSat, vVars->pArray, vVars->pArray + vVars->nSize ); if ( !RetValue ) { printf( "The CNF is trivially UNSAT.\n" ); @@ -794,7 +741,7 @@ int Abc_NodeAddClauses( solver * pSat, char * pSop0, char * pSop1, Abc_Obj_t * p SeeAlso [] ***********************************************************************/ -int Abc_NodeAddClausesTop( solver * pSat, Abc_Obj_t * pNode, Vec_Int_t * vVars ) +int Abc_NodeAddClausesTop( sat_solver * pSat, Abc_Obj_t * pNode, Vec_Int_t * vVars ) { Abc_Obj_t * pFanin; int RetValue; @@ -805,7 +752,7 @@ int Abc_NodeAddClausesTop( solver * pSat, Abc_Obj_t * pNode, Vec_Int_t * vVars ) vVars->nSize = 0; Vec_IntPush( vVars, toLit(pFanin->Id) ); Vec_IntPush( vVars, toLit(pNode->Id) ); - RetValue = solver_addclause( pSat, vVars->pArray, vVars->pArray + vVars->nSize ); + RetValue = sat_solver_addclause( pSat, vVars->pArray, vVars->pArray + vVars->nSize ); if ( !RetValue ) { printf( "The CNF is trivially UNSAT.\n" ); @@ -813,9 +760,9 @@ int Abc_NodeAddClausesTop( solver * pSat, Abc_Obj_t * pNode, Vec_Int_t * vVars ) } vVars->nSize = 0; - Vec_IntPush( vVars, neg(toLit(pFanin->Id)) ); - Vec_IntPush( vVars, neg(toLit(pNode->Id)) ); - RetValue = solver_addclause( pSat, vVars->pArray, vVars->pArray + vVars->nSize ); + Vec_IntPush( vVars, lit_neg(toLit(pFanin->Id)) ); + Vec_IntPush( vVars, lit_neg(toLit(pNode->Id)) ); + RetValue = sat_solver_addclause( pSat, vVars->pArray, vVars->pArray + vVars->nSize ); if ( !RetValue ) { printf( "The CNF is trivially UNSAT.\n" ); @@ -825,9 +772,9 @@ int Abc_NodeAddClausesTop( solver * pSat, Abc_Obj_t * pNode, Vec_Int_t * vVars ) else { vVars->nSize = 0; - Vec_IntPush( vVars, neg(toLit(pFanin->Id)) ); + Vec_IntPush( vVars, lit_neg(toLit(pFanin->Id)) ); Vec_IntPush( vVars, toLit(pNode->Id) ); - RetValue = solver_addclause( pSat, vVars->pArray, vVars->pArray + vVars->nSize ); + RetValue = sat_solver_addclause( pSat, vVars->pArray, vVars->pArray + vVars->nSize ); if ( !RetValue ) { printf( "The CNF is trivially UNSAT.\n" ); @@ -836,8 +783,8 @@ int Abc_NodeAddClausesTop( solver * pSat, Abc_Obj_t * pNode, Vec_Int_t * vVars ) vVars->nSize = 0; Vec_IntPush( vVars, toLit(pFanin->Id) ); - Vec_IntPush( vVars, neg(toLit(pNode->Id)) ); - RetValue = solver_addclause( pSat, vVars->pArray, vVars->pArray + vVars->nSize ); + Vec_IntPush( vVars, lit_neg(toLit(pNode->Id)) ); + RetValue = sat_solver_addclause( pSat, vVars->pArray, vVars->pArray + vVars->nSize ); if ( !RetValue ) { printf( "The CNF is trivially UNSAT.\n" ); @@ -847,7 +794,7 @@ int Abc_NodeAddClausesTop( solver * pSat, Abc_Obj_t * pNode, Vec_Int_t * vVars ) vVars->nSize = 0; Vec_IntPush( vVars, toLit(pNode->Id) ); - RetValue = solver_addclause( pSat, vVars->pArray, vVars->pArray + vVars->nSize ); + RetValue = sat_solver_addclause( pSat, vVars->pArray, vVars->pArray + vVars->nSize ); if ( !RetValue ) { printf( "The CNF is trivially UNSAT.\n" ); @@ -858,7 +805,7 @@ int Abc_NodeAddClausesTop( solver * pSat, Abc_Obj_t * pNode, Vec_Int_t * vVars ) /**Function************************************************************* - Synopsis [Sets up the SAT solver.] + Synopsis [Sets up the SAT sat_solver.] Description [] @@ -867,9 +814,9 @@ int Abc_NodeAddClausesTop( solver * pSat, Abc_Obj_t * pNode, Vec_Int_t * vVars ) SeeAlso [] ***********************************************************************/ -solver * Abc_NtkMiterSatCreateLogic( Abc_Ntk_t * pNtk, int fAllPrimes ) +sat_solver * Abc_NtkMiterSatCreateLogic( Abc_Ntk_t * pNtk, int fAllPrimes ) { - solver * pSat; + sat_solver * pSat; Extra_MmFlex_t * pMmFlex; Abc_Obj_t * pNode; Vec_Str_t * vCube; @@ -884,22 +831,21 @@ solver * Abc_NtkMiterSatCreateLogic( Abc_Ntk_t * pNtk, int fAllPrimes ) pNode->pCopy = (void *)pNode->Id; // start the data structures - pSat = solver_new(); + pSat = sat_solver_new(); +sat_solver_store_alloc( pSat ); pMmFlex = Extra_MmFlexStart(); vCube = Vec_StrAlloc( 100 ); vVars = Vec_IntAlloc( 100 ); -Sat_SolverTraceStart( pSat, "trace.cnf" ); - // add clauses for each internal nodes Abc_NtkForEachNode( pNtk, pNode, i ) { // derive SOPs for both phases of the node Abc_NodeBddToCnf( pNode, pMmFlex, vCube, fAllPrimes, &pSop0, &pSop1 ); - // add the clauses to the solver + // add the clauses to the sat_solver if ( !Abc_NodeAddClauses( pSat, pSop0, pSop1, pNode, vVars ) ) { - solver_delete( pSat ); + sat_solver_delete( pSat ); pSat = NULL; goto finish; } @@ -909,11 +855,12 @@ Sat_SolverTraceStart( pSat, "trace.cnf" ); { if ( !Abc_NodeAddClausesTop( pSat, pNode, vVars ) ) { - solver_delete( pSat ); + sat_solver_delete( pSat ); pSat = NULL; goto finish; } } +sat_solver_store_mark_roots( pSat ); finish: // delete |