From b1a913fb5e85ba04646632f3d771ad79bfd8a720 Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Tue, 23 Jan 2007 08:01:00 -0800 Subject: Version abc70123 --- src/base/abci/abc.c | 14 +-- src/base/abci/abcIvy.c | 2 +- src/base/abci/abcProve.c | 6 +- src/base/abci/abcSat.c | 229 ++++++++++++++++++---------------------------- src/base/abci/abcVerify.c | 4 +- 5 files changed, 98 insertions(+), 157 deletions(-) (limited to 'src/base/abci') diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index f6c180da..a6552951 100644 --- a/src/base/abci/abc.c +++ b/src/base/abci/abc.c @@ -9206,7 +9206,6 @@ int Abc_CommandSat( Abc_Frame_t * pAbc, int argc, char ** argv ) Abc_Ntk_t * pNtk; int c; int RetValue; - int fJFront; int fVerbose; int nConfLimit; int nInsLimit; @@ -9217,12 +9216,11 @@ int Abc_CommandSat( Abc_Frame_t * pAbc, int argc, char ** argv ) pErr = Abc_FrameReadErr(pAbc); // set defaults - fJFront = 0; fVerbose = 0; nConfLimit = 100000; nInsLimit = 0; Extra_UtilGetoptReset(); - while ( ( c = Extra_UtilGetopt( argc, argv, "CIvjh" ) ) != EOF ) + while ( ( c = Extra_UtilGetopt( argc, argv, "CIvh" ) ) != EOF ) { switch ( c ) { @@ -9248,9 +9246,6 @@ int Abc_CommandSat( Abc_Frame_t * pAbc, int argc, char ** argv ) if ( nInsLimit < 0 ) goto usage; break; - case 'j': - fJFront ^= 1; - break; case 'v': fVerbose ^= 1; break; @@ -9275,13 +9270,13 @@ int Abc_CommandSat( Abc_Frame_t * pAbc, int argc, char ** argv ) clk = clock(); if ( Abc_NtkIsStrash(pNtk) ) { - RetValue = Abc_NtkMiterSat( pNtk, (sint64)nConfLimit, (sint64)nInsLimit, fJFront, fVerbose, NULL, NULL ); + RetValue = Abc_NtkMiterSat( pNtk, (sint64)nConfLimit, (sint64)nInsLimit, fVerbose, NULL, NULL ); } else { assert( Abc_NtkIsLogic(pNtk) ); Abc_NtkLogicToBdd( pNtk ); - RetValue = Abc_NtkMiterSat( pNtk, (sint64)nConfLimit, (sint64)nInsLimit, fJFront, fVerbose, NULL, NULL ); + RetValue = Abc_NtkMiterSat( pNtk, (sint64)nConfLimit, (sint64)nInsLimit, fVerbose, NULL, NULL ); } // verify that the pattern is correct @@ -9316,12 +9311,11 @@ int Abc_CommandSat( Abc_Frame_t * pAbc, int argc, char ** argv ) return 0; usage: - fprintf( pErr, "usage: sat [-C num] [-I num] [-jvh]\n" ); + fprintf( pErr, "usage: sat [-C num] [-I num] [-vh]\n" ); fprintf( pErr, "\t solves the combinational miter using SAT solver MiniSat-1.14\n" ); fprintf( pErr, "\t derives CNF from the current network and leave it unchanged\n" ); fprintf( pErr, "\t-C num : limit on the number of conflicts [default = %d]\n", nConfLimit ); fprintf( pErr, "\t-I num : limit on the number of inspections [default = %d]\n", nInsLimit ); - fprintf( pErr, "\t-j : toggle the use of J-frontier [default = %s]\n", fJFront? "yes": "no" ); fprintf( pErr, "\t-v : prints verbose information [default = %s]\n", fVerbose? "yes": "no" ); fprintf( pErr, "\t-h : print the command usage\n"); return 1; diff --git a/src/base/abci/abcIvy.c b/src/base/abci/abcIvy.c index 610f5b5c..243067ce 100644 --- a/src/base/abci/abcIvy.c +++ b/src/base/abci/abcIvy.c @@ -491,7 +491,7 @@ int Abc_NtkIvyProve( Abc_Ntk_t ** ppNtk, void * pPars ) } // if SAT only, solve without iteration - RetValue = Abc_NtkMiterSat( pNtk, 2*(sint64)pParams->nMiteringLimitStart, (sint64)0, 0, 0, NULL, NULL ); + RetValue = Abc_NtkMiterSat( pNtk, 2*(sint64)pParams->nMiteringLimitStart, (sint64)0, 0, NULL, NULL ); if ( RetValue >= 0 ) return RetValue; diff --git a/src/base/abci/abcProve.c b/src/base/abci/abcProve.c index d206ae6e..6d1ed161 100644 --- a/src/base/abci/abcProve.c +++ b/src/base/abci/abcProve.c @@ -79,7 +79,7 @@ int Abc_NtkMiterProve( Abc_Ntk_t ** ppNtk, void * pPars ) if ( !pParams->fUseRewriting && !pParams->fUseFraiging ) { clk = clock(); - RetValue = Abc_NtkMiterSat( pNtk, (sint64)pParams->nMiteringLimitLast, (sint64)0, 0, 0, NULL, NULL ); + RetValue = Abc_NtkMiterSat( pNtk, (sint64)pParams->nMiteringLimitLast, (sint64)0, 0, NULL, NULL ); Abc_NtkMiterPrint( pNtk, "SAT solving", clk, pParams->fVerbose ); *ppNtk = pNtk; return RetValue; @@ -99,7 +99,7 @@ int Abc_NtkMiterProve( Abc_Ntk_t ** ppNtk, void * pPars ) // try brute-force SAT clk = clock(); nInspectLimit = pParams->nTotalInspectLimit? pParams->nTotalInspectLimit - pParams->nTotalInspectsMade : 0; - RetValue = Abc_NtkMiterSat( pNtk, (sint64)(pParams->nMiteringLimitStart * pow(pParams->nMiteringLimitMulti,nIter)), (sint64)nInspectLimit, 0, 0, &nSatConfs, &nSatInspects ); + RetValue = Abc_NtkMiterSat( pNtk, (sint64)(pParams->nMiteringLimitStart * pow(pParams->nMiteringLimitMulti,nIter)), (sint64)nInspectLimit, 0, &nSatConfs, &nSatInspects ); Abc_NtkMiterPrint( pNtk, "SAT solving", clk, pParams->fVerbose ); if ( RetValue >= 0 ) break; @@ -213,7 +213,7 @@ int Abc_NtkMiterProve( Abc_Ntk_t ** ppNtk, void * pPars ) } clk = clock(); nInspectLimit = pParams->nTotalInspectLimit? pParams->nTotalInspectLimit - pParams->nTotalInspectsMade : 0; - RetValue = Abc_NtkMiterSat( pNtk, (sint64)pParams->nMiteringLimitLast, (sint64)nInspectLimit, 0, 0, NULL, NULL ); + RetValue = Abc_NtkMiterSat( pNtk, (sint64)pParams->nMiteringLimitLast, (sint64)nInspectLimit, 0, NULL, NULL ); Abc_NtkMiterPrint( pNtk, "SAT solving", clk, pParams->fVerbose ); } 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 diff --git a/src/base/abci/abcVerify.c b/src/base/abci/abcVerify.c index f3a069f4..c891772f 100644 --- a/src/base/abci/abcVerify.c +++ b/src/base/abci/abcVerify.c @@ -86,7 +86,7 @@ void Abc_NtkCecSat( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nConfLimit, int nI } // solve the CNF using the SAT solver - RetValue = Abc_NtkMiterSat( pCnf, (sint64)nConfLimit, (sint64)nInsLimit, 0, 0, NULL, NULL ); + RetValue = Abc_NtkMiterSat( pCnf, (sint64)nConfLimit, (sint64)nInsLimit, 0, NULL, NULL ); if ( RetValue == -1 ) printf( "Networks are undecided (SAT solver timed out).\n" ); else if ( RetValue == 0 ) @@ -268,7 +268,7 @@ void Abc_NtkSecSat( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nConfLimit, int nI } // solve the CNF using the SAT solver - RetValue = Abc_NtkMiterSat( pCnf, (sint64)nConfLimit, (sint64)nInsLimit, 0, 0, NULL, NULL ); + RetValue = Abc_NtkMiterSat( pCnf, (sint64)nConfLimit, (sint64)nInsLimit, 0, NULL, NULL ); if ( RetValue == -1 ) printf( "Networks are undecided (SAT solver timed out).\n" ); else if ( RetValue == 0 ) -- cgit v1.2.3