diff options
Diffstat (limited to 'src')
32 files changed, 2095 insertions, 3398 deletions
diff --git a/src/base/abc/abc.h b/src/base/abc/abc.h index 849a888a..d843bca6 100644 --- a/src/base/abc/abc.h +++ b/src/base/abc/abc.h @@ -38,7 +38,6 @@ extern "C" { #include "cuddInt.h" #include "hop.h" #include "extra.h" -#include "solver.h" #include "vec.h" #include "stmm.h" #include "nm.h" @@ -118,6 +117,12 @@ typedef enum { #endif #endif +#ifdef _WIN32 +typedef signed __int64 sint64; // compatible with MS VS 6.0 +#else +typedef long long sint64; +#endif + typedef struct Abc_Lib_t_ Abc_Lib_t; typedef struct Abc_Ntk_t_ Abc_Ntk_t; typedef struct Abc_Obj_t_ Abc_Obj_t; @@ -725,8 +730,8 @@ extern int Abc_NtkRefactor( Abc_Ntk_t * pNtk, int nNodeSizeMax, i /*=== abcRewrite.c ==========================================================*/ extern int Abc_NtkRewrite( Abc_Ntk_t * pNtk, int fUpdateLevel, int fUseZeros, int fVerbose, int fVeryVerbose ); /*=== abcSat.c ==========================================================*/ -extern int Abc_NtkMiterSat( Abc_Ntk_t * pNtk, sint64 nConfLimit, sint64 nInsLimit, int fJFront, int fVerbose, sint64 * pNumConfs, sint64 * pNumInspects ); -extern solver * Abc_NtkMiterSatCreate( Abc_Ntk_t * pNtk, int fJFront, int fAllPrimes ); +extern int Abc_NtkMiterSat( Abc_Ntk_t * pNtk, sint64 nConfLimit, sint64 nInsLimit, int fVerbose, sint64 * pNumConfs, sint64 * pNumInspects ); +extern void * Abc_NtkMiterSatCreate( Abc_Ntk_t * pNtk, int fAllPrimes ); /*=== abcSop.c ==========================================================*/ extern char * Abc_SopRegister( Extra_MmFlex_t * pMan, char * pName ); extern char * Abc_SopStart( Extra_MmFlex_t * pMan, int nCubes, int nVars ); @@ -761,8 +766,6 @@ extern bool Abc_SopIsAndType( char * pSop ); extern bool Abc_SopIsOrType( char * pSop ); extern int Abc_SopIsExorType( char * pSop ); extern bool Abc_SopCheck( char * pSop, int nFanins ); -extern void Abc_SopWriteCnf( FILE * pFile, char * pClauses, Vec_Int_t * vVars ); -extern void Abc_SopAddCnfToSolver( solver * pSat, char * pClauses, Vec_Int_t * vVars, Vec_Int_t * vTemp ); extern char * Abc_SopFromTruthBin( char * pTruth ); extern char * Abc_SopFromTruthHex( char * pTruth ); /*=== abcStrash.c ==========================================================*/ diff --git a/src/base/abc/abcSop.c b/src/base/abc/abcSop.c index ffef42c9..4e9a6548 100644 --- a/src/base/abc/abcSop.c +++ b/src/base/abc/abcSop.c @@ -799,77 +799,6 @@ bool Abc_SopCheck( char * pSop, int nFanins ) return 1; } -/**Function************************************************************* - - Synopsis [Writes the CNF of the SOP into file.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Abc_SopWriteCnf( FILE * pFile, char * pClauses, Vec_Int_t * vVars ) -{ - char * pChar; - int i; - // check the logic function of the node - for ( pChar = pClauses; *pChar; pChar++ ) - { - // write the clause - for ( i = 0; i < vVars->nSize; i++, pChar++ ) - if ( *pChar == '0' ) - fprintf( pFile, "%d ", vVars->pArray[i] ); - else if ( *pChar == '1' ) - fprintf( pFile, "%d ", -vVars->pArray[i] ); - fprintf( pFile, "0\n" ); - // check that the remainig part is fine - assert( *pChar == ' ' ); - pChar++; - assert( *pChar == '1' ); - pChar++; - assert( *pChar == '\n' ); - } -} - -/**Function************************************************************* - - Synopsis [Adds the clauses of for the CNF to the solver.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Abc_SopAddCnfToSolver( solver * pSat, char * pClauses, Vec_Int_t * vVars, Vec_Int_t * vTemp ) -{ - char * pChar; - int i, RetValue; - // check the logic function of the node - for ( pChar = pClauses; *pChar; pChar++ ) - { - // add the clause - vTemp->nSize = 0; - for ( i = 0; i < vVars->nSize; i++, pChar++ ) - if ( *pChar == '0' ) - Vec_IntPush( vTemp, toLit(vVars->pArray[i]) ); - else if ( *pChar == '1' ) - Vec_IntPush( vTemp, neg(toLit(vVars->pArray[i])) ); - // add the clause to the solver - RetValue = solver_addclause( pSat, vTemp->pArray, vTemp->pArray + vTemp->nSize ); - assert( RetValue != 1 ); - // check that the remainig part is fine - assert( *pChar == ' ' ); - pChar++; - assert( *pChar == '1' ); - pChar++; - assert( *pChar == '\n' ); - } -} - /**Function************************************************************* 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 ) diff --git a/src/base/io/ioWriteCnf.c b/src/base/io/ioWriteCnf.c index f12a1297..88695668 100644 --- a/src/base/io/ioWriteCnf.c +++ b/src/base/io/ioWriteCnf.c @@ -19,6 +19,7 @@ ***********************************************************************/ #include "io.h" +#include "satSolver.h" //////////////////////////////////////////////////////////////////////// /// DECLARATIONS /// @@ -43,7 +44,7 @@ static Abc_Ntk_t * s_pNtk = NULL; ***********************************************************************/ int Io_WriteCnf( Abc_Ntk_t * pNtk, char * pFileName, int fAllPrimes ) { - solver * pSat; + sat_solver * pSat; if ( Abc_NtkIsStrash(pNtk) ) printf( "Io_WriteCnf() warning: Generating CNF by applying heuristic AIG to CNF conversion.\n" ); else @@ -67,7 +68,7 @@ int Io_WriteCnf( Abc_Ntk_t * pNtk, char * pFileName, int fAllPrimes ) if ( Abc_NtkIsLogic(pNtk) ) Abc_NtkLogicToBdd( pNtk ); // create solver with clauses - pSat = Abc_NtkMiterSatCreate( pNtk, 0, fAllPrimes ); + pSat = Abc_NtkMiterSatCreate( pNtk, fAllPrimes ); if ( pSat == NULL ) { fprintf( stdout, "The problem is trivially UNSAT. No CNF file is generated.\n" ); @@ -75,10 +76,10 @@ int Io_WriteCnf( Abc_Ntk_t * pNtk, char * pFileName, int fAllPrimes ) } // write the clauses s_pNtk = pNtk; - Asat_SolverWriteDimacs( pSat, pFileName, 0, 0, 1 ); + Sat_SolverWriteDimacs( pSat, pFileName, 0, 0, 1 ); s_pNtk = NULL; // free the solver - solver_delete( pSat ); + sat_solver_delete( pSat ); return 1; } diff --git a/src/opt/res/res.h b/src/opt/res/res.h index 91171d3b..4a887741 100644 --- a/src/opt/res/res.h +++ b/src/opt/res/res.h @@ -93,9 +93,9 @@ static inline void Res_WinAddNode( Res_Win_t * p, Abc_Obj_t * pObj ) extern void Res_WinDivisors( Res_Win_t * p, int nLevDivMax ); extern int Res_WinVisitMffc( Res_Win_t * p ); /*=== resFilter.c ==========================================================*/ -extern Vec_Ptr_t * Res_FilterCandidates( Res_Win_t * pWin, Res_Sim_t * pSim ); +extern Vec_Vec_t * Res_FilterCandidates( Res_Win_t * pWin, Res_Sim_t * pSim ); /*=== resSat.c ==========================================================*/ -extern Hop_Obj_t * Res_SatFindFunction( Hop_Man_t * pMan, Res_Win_t * pWin, Vec_Ptr_t * vFanins, Abc_Ntk_t * pAig ); +extern void * Res_SatProveUnsat( Abc_Ntk_t * pAig, Vec_Ptr_t * vFanins ); /*=== resSim.c ==========================================================*/ extern Res_Sim_t * Res_SimAlloc( int nWords ); extern void Res_SimFree( Res_Sim_t * p ); diff --git a/src/opt/res/resCore.c b/src/opt/res/resCore.c index 0335712d..17d1c62e 100644 --- a/src/opt/res/resCore.c +++ b/src/opt/res/resCore.c @@ -20,6 +20,8 @@ #include "abc.h" #include "res.h" +#include "kit.h" +#include "satStore.h" //////////////////////////////////////////////////////////////////////// /// DECLARATIONS /// @@ -42,15 +44,24 @@ ***********************************************************************/ int Abc_NtkResynthesize( Abc_Ntk_t * pNtk, int nWindow, int nSimWords, int fVerbose, int fVeryVerbose ) { + Int_Man_t * pMan; + Sto_Man_t * pCnf; Res_Win_t * pWin; Res_Sim_t * pSim; Abc_Ntk_t * pAig; Abc_Obj_t * pObj; Hop_Obj_t * pFunc; + Kit_Graph_t * pGraph; + Vec_Vec_t * vResubs; Vec_Ptr_t * vFanins; - int i, nNodesOld; + Vec_Int_t * vMemory; + unsigned * puTruth; + int i, k, nNodesOld, nFanins; assert( Abc_NtkHasAig(pNtk) ); assert( nWindow > 0 && nWindow < 100 ); + vMemory = Vec_IntAlloc(0); + // start the interpolation manager + pMan = Int_ManAlloc( 512 ); // start the window pWin = Res_WinAlloc(); pSim = Res_SimAlloc( nSimWords ); @@ -72,20 +83,44 @@ int Abc_NtkResynthesize( Abc_Ntk_t * pNtk, int nWindow, int nSimWords, int fVerb // create the AIG for the window pAig = Res_WndStrash( pWin ); // prepare simulation info - if ( Res_SimPrepare( pSim, pAig ) ) + if ( !Res_SimPrepare( pSim, pAig ) ) { - // find resub candidates for the node - vFanins = Res_FilterCandidates( pWin, pSim ); - // check using SAT - pFunc = Res_SatFindFunction( pNtk->pManFunc, pWin, vFanins, pAig ); - // update the network - if ( pFunc == NULL ) - Res_UpdateNetwork( pObj, vFanins, pFunc, pWin->vLevels ); + Abc_NtkDelete( pAig ); + continue; + } + // find resub candidates for the node + vResubs = Res_FilterCandidates( pWin, pSim ); + if ( vResubs ) + { + // iterate through the resubstitutions + Vec_VecForEachLevel( vResubs, vFanins, k ) + { + extern Hop_Obj_t * Kit_GraphToHop( Hop_Man_t * pMan, Kit_Graph_t * pGraph ); + pCnf = Res_SatProveUnsat( pAig, vFanins ); + if ( pCnf == NULL ) + continue; + // interplate this proof + nFanins = Int_ManInterpolate( pMan, pCnf, fVerbose, &puTruth ); + assert( nFanins == Vec_PtrSize(vFanins) - 2 ); + Sto_ManFree( pCnf ); + // transform interpolant into the AIG + pGraph = Kit_TruthToGraph( puTruth, nFanins, vMemory ); + // derive the AIG for the decomposition tree + pFunc = Kit_GraphToHop( pNtk->pManFunc, pGraph ); + Kit_GraphFree( pGraph ); + // update the network + if ( pFunc == NULL ) + Res_UpdateNetwork( pObj, vFanins, pFunc, pWin->vLevels ); + break; + } + Vec_VecFree( vResubs ); } Abc_NtkDelete( pAig ); } Res_WinFree( pWin ); Res_SimFree( pSim ); + Int_ManFree( pMan ); + Vec_IntFree( vMemory ); // check the resulting network if ( !Abc_NtkCheck( pNtk ) ) { diff --git a/src/opt/res/resFilter.c b/src/opt/res/resFilter.c index e2e295a0..65e9953f 100644 --- a/src/opt/res/resFilter.c +++ b/src/opt/res/resFilter.c @@ -40,7 +40,7 @@ SeeAlso [] ***********************************************************************/ -Vec_Ptr_t * Res_FilterCandidates( Res_Win_t * pWin, Res_Sim_t * pSim ) +Vec_Vec_t * Res_FilterCandidates( Res_Win_t * pWin, Res_Sim_t * pSim ) { unsigned * pInfo; Abc_Obj_t * pFanin; diff --git a/src/opt/res/resSat.c b/src/opt/res/resSat.c index 39ca9ad6..770152cf 100644 --- a/src/opt/res/resSat.c +++ b/src/opt/res/resSat.c @@ -21,19 +21,116 @@ #include "abc.h" #include "res.h" #include "hop.h" -//#include "bf.h" +#include "satSolver.h" //////////////////////////////////////////////////////////////////////// /// DECLARATIONS /// //////////////////////////////////////////////////////////////////////// +extern int Res_SatAddConst1( sat_solver * pSat, int iVar ); +extern int Res_SatAddEqual( sat_solver * pSat, int iVar0, int iVar1, int fCompl ); +extern int Res_SatAddAnd( sat_solver * pSat, int iVar, int iVar0, int iVar1, int fCompl0, int fCompl1 ); + //////////////////////////////////////////////////////////////////////// /// FUNCTION DEFINITIONS /// //////////////////////////////////////////////////////////////////////// /**Function************************************************************* - Synopsis [] + Synopsis [Loads AIG into the SAT solver.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void * Res_SatProveUnsat( Abc_Ntk_t * pAig, Vec_Ptr_t * vFanins ) +{ + void * pCnf; + sat_solver * pSat; + Vec_Ptr_t * vNodes; + Abc_Obj_t * pObj; + int i, nNodes, status; + + // make sure the constant node is not involved + assert( Abc_ObjFanoutNum(Abc_AigConst1(pAig)) == 0 ); + + // collect reachable nodes + vNodes = Abc_NtkDfsNodes( pAig, (Abc_Obj_t **)vFanins->pArray, vFanins->nSize ); + // assign unique numbers to each node + nNodes = 0; + Abc_NtkForEachPi( pAig, pObj, i ) + pObj->pCopy = (void *)nNodes++; + Vec_PtrForEachEntry( vNodes, pObj, i ) + pObj->pCopy = (void *)nNodes++; + Vec_PtrForEachEntry( vFanins, pObj, i ) + pObj->pCopy = (void *)nNodes++; + + // start the solver + pSat = sat_solver_new(); + sat_solver_store_alloc( pSat ); + + // add clause for AND gates + Vec_PtrForEachEntry( vNodes, pObj, i ) + Res_SatAddAnd( pSat, (int)pObj->pCopy, + (int)Abc_ObjFanin0(pObj)->pCopy, (int)Abc_ObjFanin1(pObj)->pCopy, Abc_ObjFaninC0(pObj), Abc_ObjFaninC1(pObj) ); + // add clauses for the POs + Vec_PtrForEachEntry( vFanins, pObj, i ) + Res_SatAddEqual( pSat, (int)pObj->pCopy, + (int)Abc_ObjFanin0(pObj)->pCopy, Abc_ObjFaninC0(pObj) ); + // add trivial clauses + pObj = Vec_PtrEntry(vFanins, 0); + Res_SatAddConst1( pSat, (int)pObj->pCopy ); + pObj = Vec_PtrEntry(vFanins, 1); + Res_SatAddConst1( pSat, (int)pObj->pCopy ); + // bookmark the clauses of A + sat_solver_store_mark_clauses_a( pSat ); + // duplicate the clauses + pObj = Vec_PtrEntry(vFanins, 1); + Sat_SolverDoubleClauses( pSat, (int)pObj->pCopy ); + // add the equality clauses + Vec_PtrForEachEntryStart( vFanins, pObj, i, 2 ) + Res_SatAddEqual( pSat, (int)pObj->pCopy, ((int)pObj->pCopy) + nNodes, 0 ); + // bookmark the roots + sat_solver_store_mark_roots( pSat ); + Vec_PtrFree( vNodes ); + + // solve the problem + status = sat_solver_solve( pSat, NULL, NULL, (sint64)10000, (sint64)0, (sint64)0, (sint64)0 ); + if ( status == l_False ) + pCnf = sat_solver_store_release( pSat ); + else if ( status == l_True ) + pCnf = NULL; + else + pCnf = NULL; + sat_solver_delete( pSat ); + return pCnf; +} + +/**Function************************************************************* + + Synopsis [Loads two-input AND-gate.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Res_SatAddConst1( sat_solver * pSat, int iVar ) +{ + lit Lit = lit_var(iVar); + if ( !sat_solver_addclause( pSat, &Lit, &Lit + 1 ) ) + return 0; + return 1; +} + +/**Function************************************************************* + + Synopsis [Loads two-input AND-gate.] Description [] @@ -42,11 +139,56 @@ SeeAlso [] ***********************************************************************/ -Hop_Obj_t * Res_SatFindFunction( Hop_Man_t * pMan, Res_Win_t * pWin, Vec_Ptr_t * vFanins, Abc_Ntk_t * pAig ) +int Res_SatAddEqual( sat_solver * pSat, int iVar0, int iVar1, int fCompl ) { - return NULL; + lit Lits[2]; + + Lits[0] = toLitCond( iVar0, 0 ); + Lits[1] = toLitCond( iVar1, !fCompl ); + if ( !sat_solver_addclause( pSat, Lits, Lits + 2 ) ) + return 0; + + Lits[0] = toLitCond( iVar0, 1 ); + Lits[1] = toLitCond( iVar1, fCompl ); + if ( !sat_solver_addclause( pSat, Lits, Lits + 2 ) ) + return 0; + + return 1; } +/**Function************************************************************* + + Synopsis [Loads two-input AND-gate.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Res_SatAddAnd( sat_solver * pSat, int iVar, int iVar0, int iVar1, int fCompl0, int fCompl1 ) +{ + lit Lits[3]; + + Lits[0] = toLitCond( iVar, 1 ); + Lits[1] = toLitCond( iVar0, fCompl0 ); + if ( !sat_solver_addclause( pSat, Lits, Lits + 2 ) ) + return 0; + + Lits[0] = toLitCond( iVar, 1 ); + Lits[1] = toLitCond( iVar1, fCompl1 ); + if ( !sat_solver_addclause( pSat, Lits, Lits + 2 ) ) + return 0; + + Lits[0] = toLitCond( iVar, 0 ); + Lits[1] = toLitCond( iVar0, !fCompl0 ); + Lits[2] = toLitCond( iVar1, !fCompl1 ); + if ( !sat_solver_addclause( pSat, Lits, Lits + 3 ) ) + return 0; + + return 1; +} //////////////////////////////////////////////////////////////////////// /// END OF FILE /// diff --git a/src/opt/ret/retInit.c b/src/opt/ret/retInit.c index b53ceeae..156df0dc 100644 --- a/src/opt/ret/retInit.c +++ b/src/opt/ret/retInit.c @@ -57,7 +57,7 @@ Vec_Int_t * Abc_NtkRetimeInitialValues( Abc_Ntk_t * pNtkCone, Vec_Int_t * vValue printf( "The miter for initial state computation has %d AIG nodes. ", Abc_NtkNodeNum(pNtkMiter) ); // solve the miter clk = clock(); - RetValue = Abc_NtkMiterSat( pNtkMiter, (sint64)500000, (sint64)50000000, 0, 0, NULL, NULL ); + RetValue = Abc_NtkMiterSat( pNtkMiter, (sint64)500000, (sint64)50000000, 0, NULL, NULL ); if ( fVerbose ) { PRT( "SAT solving time", clock() - clk ); } // analyze the result diff --git a/src/sat/asat/added.c b/src/sat/asat/added.c deleted file mode 100644 index 222693ad..00000000 --- a/src/sat/asat/added.c +++ /dev/null @@ -1,234 +0,0 @@ -/**CFile**************************************************************** - - FileName [added.c] - - SystemName [ABC: Logic synthesis and verification system.] - - PackageName [C-language MiniSat solver.] - - Synopsis [Additional SAT solver procedures.] - - Author [Alan Mishchenko] - - Affiliation [UC Berkeley] - - Date [Ver. 1.0. Started - June 20, 2005.] - - Revision [$Id: added.c,v 1.4 2005/09/16 22:55:03 casem Exp $] - -***********************************************************************/ - -#include <stdio.h> -#include <assert.h> -#include "solver.h" -#include "extra.h" - -//////////////////////////////////////////////////////////////////////// -/// DECLARATIONS /// -//////////////////////////////////////////////////////////////////////// - -struct clause_t -{ - int size_learnt; - lit lits[0]; -}; - -static inline int clause_size (clause* c) { return c->size_learnt >> 1; } -static inline lit* clause_begin (clause* c) { return c->lits; } - -static inline int lit_var(lit l) { return l >> 1; } -static inline int lit_sign(lit l) { return (l & 1); } - -static void Asat_ClauseWriteDimacs( FILE * pFile, clause * pC, bool fIncrement ); - -extern void Io_WriteCnfOutputPiMapping( FILE * pFile, int incrementVars ); - -//////////////////////////////////////////////////////////////////////// -/// FUNCTION DEFINITIONS /// -//////////////////////////////////////////////////////////////////////// - -/**Function************************************************************* - - Synopsis [Write the clauses in the solver into a file in DIMACS format.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Asat_SolverWriteDimacs( solver * p, char * pFileName, lit* assumptionsBegin, lit* assumptionsEnd, int incrementVars ) -{ - FILE * pFile; - void ** pClauses; - int nClauses, i; - - // count the number of clauses - nClauses = p->clauses.size + p->learnts.size; - for ( i = 0; i < p->size; i++ ) - if ( p->levels[i] == 0 && p->assigns[i] != l_Undef ) - nClauses++; - - // start the file - pFile = fopen( pFileName, "wb" ); - if ( pFile == NULL ) - { - printf( "Asat_SolverWriteDimacs(): Cannot open the ouput file.\n" ); - return; - } - fprintf( pFile, "c CNF generated by ABC on %s\n", Extra_TimeStamp() ); -// Io_WriteCnfOutputPiMapping( pFile, incrementVars ); - fprintf( pFile, "p cnf %d %d\n", p->size, nClauses ); - - // write the original clauses - nClauses = p->clauses.size; - pClauses = p->clauses.ptr; - for ( i = 0; i < nClauses; i++ ) - Asat_ClauseWriteDimacs( pFile, pClauses[i], incrementVars ); - - // write the learned clauses - nClauses = p->learnts.size; - pClauses = p->learnts.ptr; - for ( i = 0; i < nClauses; i++ ) - Asat_ClauseWriteDimacs( pFile, pClauses[i], incrementVars ); - - // write zero-level assertions - for ( i = 0; i < p->size; i++ ) - if ( p->levels[i] == 0 && p->assigns[i] != l_Undef ) - fprintf( pFile, "%s%d%s\n", - (p->assigns[i] == l_False)? "-": "", - i + (int)(incrementVars>0), - (incrementVars) ? " 0" : ""); - - // write the assumptions - if (assumptionsBegin) { - for (; assumptionsBegin != assumptionsEnd; assumptionsBegin++) { - fprintf( pFile, "%s%d%s\n", - lit_sign(*assumptionsBegin)? "-": "", - lit_var(*assumptionsBegin) + (int)(incrementVars>0), - (incrementVars) ? " 0" : ""); - } - } - - fprintf( pFile, "\n" ); - fclose( pFile ); -} - -/**Function************************************************************* - - Synopsis [Writes the given clause in a file in DIMACS format.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Asat_ClauseWriteDimacs( FILE * pFile, clause * pC, bool fIncrement ) -{ - lit * pLits = clause_begin(pC); - int nLits = clause_size(pC); - int i; - - for ( i = 0; i < nLits; i++ ) - fprintf( pFile, "%s%d ", (lit_sign(pLits[i])? "-": ""), lit_var(pLits[i]) + (int)(fIncrement>0) ); - if ( fIncrement ) - fprintf( pFile, "0" ); - fprintf( pFile, "\n" ); -} - -/**Function************************************************************* - - Synopsis [Returns a counter-example.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -int * solver_get_model( solver * p, int * pVars, int nVars ) -{ - int * pModel; - int i; - pModel = ALLOC( int, nVars ); - for ( i = 0; i < nVars; i++ ) - { - assert( pVars[i] >= 0 && pVars[i] < p->size ); - pModel[i] = (int)(p->model.ptr[pVars[i]] == l_True); - } - return pModel; -} - -/**Function************************************************************* - - Synopsis [Writes the given clause in a file in DIMACS format.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Asat_SatPrintStats( FILE * pFile, solver * p ) -{ - printf( "Start = %4d. Conf = %6d. Dec = %6d. Prop = %7d. Insp = %8d.\n", - (int)p->solver_stats.starts, - (int)p->solver_stats.conflicts, - (int)p->solver_stats.decisions, - (int)p->solver_stats.propagations, - (int)p->solver_stats.inspects ); - printf( "Total runtime = %7.2f sec. Var select = %7.2f sec. Var update = %7.2f sec.\n", - (float)(p->timeTotal)/(float)(CLOCKS_PER_SEC), - (float)(p->timeSelect)/(float)(CLOCKS_PER_SEC), - (float)(p->timeUpdate)/(float)(CLOCKS_PER_SEC) ); -} - -/**Function************************************************************* - - Synopsis [Sets the preferred variables.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Asat_SolverSetPrefVars(solver * s, int * pPrefVars, int nPrefVars) -{ - int i; - assert( s->pPrefVars == NULL ); - for ( i = 0; i < nPrefVars; i++ ) - assert( pPrefVars[i] < s->size ); - s->pPrefVars = pPrefVars; - s->nPrefVars = nPrefVars; -} - -/**Function************************************************************* - - Synopsis [Sets the preferred variables.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Asat_SolverSetFactors(solver * s, float * pFactors) -{ - assert( s->factors == NULL ); - s->factors = pFactors; -} - - -//////////////////////////////////////////////////////////////////////// -/// END OF FILE /// -//////////////////////////////////////////////////////////////////////// - - diff --git a/src/sat/asat/asatmem.c b/src/sat/asat/asatmem.c deleted file mode 100644 index 24c1b1a8..00000000 --- a/src/sat/asat/asatmem.c +++ /dev/null @@ -1,527 +0,0 @@ -/**CFile**************************************************************** - - FileName [asatmem.c] - - PackageName [SAT solver.] - - Synopsis [Memory management.] - - Author [Alan Mishchenko <alanmi@eecs.berkeley.edu>] - - Affiliation [UC Berkeley] - - Date [Ver. 1.0. Started - January 1, 2004.] - - Revision [$Id: asatmem.c,v 1.0 2004/01/01 1:00:00 alanmi Exp $] - -***********************************************************************/ - -#include "asatmem.h" -#include "extra.h" - -//////////////////////////////////////////////////////////////////////// -/// DECLARATIONS /// -//////////////////////////////////////////////////////////////////////// - -struct Asat_MmFixed_t_ -{ - // information about individual entries - int nEntrySize; // the size of one entry - int nEntriesAlloc; // the total number of entries allocated - int nEntriesUsed; // the number of entries in use - int nEntriesMax; // the max number of entries in use - char * pEntriesFree; // the linked list of free entries - - // this is where the memory is stored - int nChunkSize; // the size of one chunk - int nChunksAlloc; // the maximum number of memory chunks - int nChunks; // the current number of memory chunks - char ** pChunks; // the allocated memory - - // statistics - int nMemoryUsed; // memory used in the allocated entries - int nMemoryAlloc; // memory allocated -}; - -struct Asat_MmFlex_t_ -{ - // information about individual entries - int nEntriesUsed; // the number of entries allocated - char * pCurrent; // the current pointer to free memory - char * pEnd; // the first entry outside the free memory - - // this is where the memory is stored - int nChunkSize; // the size of one chunk - int nChunksAlloc; // the maximum number of memory chunks - int nChunks; // the current number of memory chunks - char ** pChunks; // the allocated memory - - // statistics - int nMemoryUsed; // memory used in the allocated entries - int nMemoryAlloc; // memory allocated -}; - -struct Asat_MmStep_t_ -{ - int nMems; // the number of fixed memory managers employed - Asat_MmFixed_t ** pMems; // memory managers: 2^1 words, 2^2 words, etc - int nMapSize; // the size of the memory array - Asat_MmFixed_t ** pMap; // maps the number of bytes into its memory manager -}; - -//////////////////////////////////////////////////////////////////////// -/// FUNCTION DEFINITIONS /// -//////////////////////////////////////////////////////////////////////// - -/**Function************************************************************* - - Synopsis [Allocates memory pieces of fixed size.] - - Description [The size of the chunk is computed as the minimum of - 1024 entries and 64K. Can only work with entry size at least 4 byte long.] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -Asat_MmFixed_t * Asat_MmFixedStart( int nEntrySize ) -{ - Asat_MmFixed_t * p; - - p = ALLOC( Asat_MmFixed_t, 1 ); - memset( p, 0, sizeof(Asat_MmFixed_t) ); - - p->nEntrySize = nEntrySize; - p->nEntriesAlloc = 0; - p->nEntriesUsed = 0; - p->pEntriesFree = NULL; - - if ( nEntrySize * (1 << 10) < (1<<16) ) - p->nChunkSize = (1 << 10); - else - p->nChunkSize = (1<<16) / nEntrySize; - if ( p->nChunkSize < 8 ) - p->nChunkSize = 8; - - p->nChunksAlloc = 64; - p->nChunks = 0; - p->pChunks = ALLOC( char *, p->nChunksAlloc ); - - p->nMemoryUsed = 0; - p->nMemoryAlloc = 0; - return p; -} - -/**Function************************************************************* - - Synopsis [] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Asat_MmFixedStop( Asat_MmFixed_t * p, int fVerbose ) -{ - int i; - if ( p == NULL ) - return; - if ( fVerbose ) - { - printf( "Fixed memory manager: Entry = %5d. Chunk = %5d. Chunks used = %5d.\n", - p->nEntrySize, p->nChunkSize, p->nChunks ); - printf( " Entries used = %8d. Entries peak = %8d. Memory used = %8d. Memory alloc = %8d.\n", - p->nEntriesUsed, p->nEntriesMax, p->nEntrySize * p->nEntriesUsed, p->nMemoryAlloc ); - } - for ( i = 0; i < p->nChunks; i++ ) - free( p->pChunks[i] ); - free( p->pChunks ); - free( p ); -} - -/**Function************************************************************* - - Synopsis [] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -char * Asat_MmFixedEntryFetch( Asat_MmFixed_t * p ) -{ - char * pTemp; - int i; - - // check if there are still free entries - if ( p->nEntriesUsed == p->nEntriesAlloc ) - { // need to allocate more entries - assert( p->pEntriesFree == NULL ); - if ( p->nChunks == p->nChunksAlloc ) - { - p->nChunksAlloc *= 2; - p->pChunks = REALLOC( char *, p->pChunks, p->nChunksAlloc ); - } - p->pEntriesFree = ALLOC( char, p->nEntrySize * p->nChunkSize ); - p->nMemoryAlloc += p->nEntrySize * p->nChunkSize; - // transform these entries into a linked list - pTemp = p->pEntriesFree; - for ( i = 1; i < p->nChunkSize; i++ ) - { - *((char **)pTemp) = pTemp + p->nEntrySize; - pTemp += p->nEntrySize; - } - // set the last link - *((char **)pTemp) = NULL; - // add the chunk to the chunk storage - p->pChunks[ p->nChunks++ ] = p->pEntriesFree; - // add to the number of entries allocated - p->nEntriesAlloc += p->nChunkSize; - } - // incrememt the counter of used entries - p->nEntriesUsed++; - if ( p->nEntriesMax < p->nEntriesUsed ) - p->nEntriesMax = p->nEntriesUsed; - // return the first entry in the free entry list - pTemp = p->pEntriesFree; - p->pEntriesFree = *((char **)pTemp); - return pTemp; -} - -/**Function************************************************************* - - Synopsis [] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Asat_MmFixedEntryRecycle( Asat_MmFixed_t * p, char * pEntry ) -{ - // decrement the counter of used entries - p->nEntriesUsed--; - // add the entry to the linked list of free entries - *((char **)pEntry) = p->pEntriesFree; - p->pEntriesFree = pEntry; -} - -/**Function************************************************************* - - Synopsis [] - - Description [Relocates all the memory except the first chunk.] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Asat_MmFixedRestart( Asat_MmFixed_t * p ) -{ - int i; - char * pTemp; - - // deallocate all chunks except the first one - for ( i = 1; i < p->nChunks; i++ ) - free( p->pChunks[i] ); - p->nChunks = 1; - // transform these entries into a linked list - pTemp = p->pChunks[0]; - for ( i = 1; i < p->nChunkSize; i++ ) - { - *((char **)pTemp) = pTemp + p->nEntrySize; - pTemp += p->nEntrySize; - } - // set the last link - *((char **)pTemp) = NULL; - // set the free entry list - p->pEntriesFree = p->pChunks[0]; - // set the correct statistics - p->nMemoryAlloc = p->nEntrySize * p->nChunkSize; - p->nMemoryUsed = 0; - p->nEntriesAlloc = p->nChunkSize; - p->nEntriesUsed = 0; -} - -/**Function************************************************************* - - Synopsis [] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -int Asat_MmFixedReadMemUsage( Asat_MmFixed_t * p ) -{ - return p->nMemoryAlloc; -} - - - -/**Function************************************************************* - - Synopsis [Allocates entries of flexible size.] - - Description [Can only work with entry size at least 4 byte long.] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -Asat_MmFlex_t * Asat_MmFlexStart() -{ - Asat_MmFlex_t * p; - - p = ALLOC( Asat_MmFlex_t, 1 ); - memset( p, 0, sizeof(Asat_MmFlex_t) ); - - p->nEntriesUsed = 0; - p->pCurrent = NULL; - p->pEnd = NULL; - - p->nChunkSize = (1 << 12); - p->nChunksAlloc = 64; - p->nChunks = 0; - p->pChunks = ALLOC( char *, p->nChunksAlloc ); - - p->nMemoryUsed = 0; - p->nMemoryAlloc = 0; - return p; -} - -/**Function************************************************************* - - Synopsis [] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Asat_MmFlexStop( Asat_MmFlex_t * p, int fVerbose ) -{ - int i; - if ( p == NULL ) - return; - if ( fVerbose ) - { - printf( "Flexible memory manager: Chunk size = %d. Chunks used = %d.\n", - p->nChunkSize, p->nChunks ); - printf( " Entries used = %d. Memory used = %d. Memory alloc = %d.\n", - p->nEntriesUsed, p->nMemoryUsed, p->nMemoryAlloc ); - } - for ( i = 0; i < p->nChunks; i++ ) - free( p->pChunks[i] ); - free( p->pChunks ); - free( p ); -} - -/**Function************************************************************* - - Synopsis [] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -char * Asat_MmFlexEntryFetch( Asat_MmFlex_t * p, int nBytes ) -{ - char * pTemp; - // check if there are still free entries - if ( p->pCurrent == NULL || p->pCurrent + nBytes > p->pEnd ) - { // need to allocate more entries - if ( p->nChunks == p->nChunksAlloc ) - { - p->nChunksAlloc *= 2; - p->pChunks = REALLOC( char *, p->pChunks, p->nChunksAlloc ); - } - if ( nBytes > p->nChunkSize ) - { - // resize the chunk size if more memory is requested than it can give - // (ideally, this should never happen) - p->nChunkSize = 2 * nBytes; - } - p->pCurrent = ALLOC( char, p->nChunkSize ); - p->pEnd = p->pCurrent + p->nChunkSize; - p->nMemoryAlloc += p->nChunkSize; - // add the chunk to the chunk storage - p->pChunks[ p->nChunks++ ] = p->pCurrent; - } - assert( p->pCurrent + nBytes <= p->pEnd ); - // increment the counter of used entries - p->nEntriesUsed++; - // keep track of the memory used - p->nMemoryUsed += nBytes; - // return the next entry - pTemp = p->pCurrent; - p->pCurrent += nBytes; - return pTemp; -} - -/**Function************************************************************* - - Synopsis [] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -int Asat_MmFlexReadMemUsage( Asat_MmFlex_t * p ) -{ - return p->nMemoryAlloc; -} - - - - - -/**Function************************************************************* - - Synopsis [Starts the hierarchical memory manager.] - - Description [This manager can allocate entries of any size. - Iternally they are mapped into the entries with the number of bytes - equal to the power of 2. The smallest entry size is 8 bytes. The - next one is 16 bytes etc. So, if the user requests 6 bytes, he gets - 8 byte entry. If we asks for 25 bytes, he gets 32 byte entry etc. - The input parameters "nSteps" says how many fixed memory managers - are employed internally. Calling this procedure with nSteps equal - to 10 results in 10 hierarchically arranged internal memory managers, - which can allocate up to 4096 (1Kb) entries. Requests for larger - entries are handed over to malloc() and then free()ed.] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -Asat_MmStep_t * Asat_MmStepStart( int nSteps ) -{ - Asat_MmStep_t * p; - int i, k; - p = ALLOC( Asat_MmStep_t, 1 ); - p->nMems = nSteps; - // start the fixed memory managers - p->pMems = ALLOC( Asat_MmFixed_t *, p->nMems ); - for ( i = 0; i < p->nMems; i++ ) - p->pMems[i] = Asat_MmFixedStart( (8<<i) ); - // set up the mapping of the required memory size into the corresponding manager - p->nMapSize = (4<<p->nMems); - p->pMap = ALLOC( Asat_MmFixed_t *, p->nMapSize+1 ); - p->pMap[0] = NULL; - for ( k = 1; k <= 4; k++ ) - p->pMap[k] = p->pMems[0]; - for ( i = 0; i < p->nMems; i++ ) - for ( k = (4<<i)+1; k <= (8<<i); k++ ) - p->pMap[k] = p->pMems[i]; -//for ( i = 1; i < 100; i ++ ) -//printf( "%10d: size = %10d\n", i, p->pMap[i]->nEntrySize ); - return p; -} - -/**Function************************************************************* - - Synopsis [Stops the memory manager.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Asat_MmStepStop( Asat_MmStep_t * p, int fVerbose ) -{ - int i; - for ( i = 0; i < p->nMems; i++ ) - Asat_MmFixedStop( p->pMems[i], fVerbose ); - free( p->pMems ); - free( p->pMap ); - free( p ); -} - -/**Function************************************************************* - - Synopsis [Creates the entry.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -char * Asat_MmStepEntryFetch( Asat_MmStep_t * p, int nBytes ) -{ - if ( nBytes == 0 ) - return NULL; - if ( nBytes > p->nMapSize ) - { -// printf( "Allocating %d bytes.\n", nBytes ); - return ALLOC( char, nBytes ); - } - return Asat_MmFixedEntryFetch( p->pMap[nBytes] ); -} - - -/**Function************************************************************* - - Synopsis [Recycles the entry.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Asat_MmStepEntryRecycle( Asat_MmStep_t * p, char * pEntry, int nBytes ) -{ - if ( nBytes == 0 ) - return; - if ( nBytes > p->nMapSize ) - { - free( pEntry ); - return; - } - Asat_MmFixedEntryRecycle( p->pMap[nBytes], pEntry ); -} - -/**Function************************************************************* - - Synopsis [] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -int Asat_MmStepReadMemUsage( Asat_MmStep_t * p ) -{ - int i, nMemTotal = 0; - for ( i = 0; i < p->nMems; i++ ) - nMemTotal += p->pMems[i]->nMemoryAlloc; - return nMemTotal; -} diff --git a/src/sat/asat/asatmem.h b/src/sat/asat/asatmem.h deleted file mode 100644 index 7351d77b..00000000 --- a/src/sat/asat/asatmem.h +++ /dev/null @@ -1,78 +0,0 @@ -/**CFile**************************************************************** - - FileName [asatmem.h] - - PackageName [SAT solver.] - - Synopsis [Memory management.] - - Author [Alan Mishchenko <alanmi@eecs.berkeley.edu>] - - Affiliation [UC Berkeley] - - Date [Ver. 1.0. Started - January 1, 2004.] - - Revision [$Id: asatmem.h,v 1.0 2004/01/01 1:00:00 alanmi Exp $] - -***********************************************************************/ - -#ifndef __ASAT_MEM_H__ -#define __ASAT_MEM_H__ - -//////////////////////////////////////////////////////////////////////// -/// INCLUDES /// -//////////////////////////////////////////////////////////////////////// - -//#include "leaks.h" -#include <stdio.h> -#include <stdlib.h> - -//////////////////////////////////////////////////////////////////////// -/// PARAMETERS /// -//////////////////////////////////////////////////////////////////////// - -//////////////////////////////////////////////////////////////////////// -/// STRUCTURE DEFINITIONS /// -//////////////////////////////////////////////////////////////////////// - -typedef struct Asat_MmFixed_t_ Asat_MmFixed_t; -typedef struct Asat_MmFlex_t_ Asat_MmFlex_t; -typedef struct Asat_MmStep_t_ Asat_MmStep_t; - -//////////////////////////////////////////////////////////////////////// -/// GLOBAL VARIABLES /// -//////////////////////////////////////////////////////////////////////// - -//////////////////////////////////////////////////////////////////////// -/// MACRO DEFINITIONS /// -//////////////////////////////////////////////////////////////////////// - -//////////////////////////////////////////////////////////////////////// -/// FUNCTION DECLARATIONS /// -//////////////////////////////////////////////////////////////////////// - -// fixed-size-block memory manager -extern Asat_MmFixed_t * Asat_MmFixedStart( int nEntrySize ); -extern void Asat_MmFixedStop( Asat_MmFixed_t * p, int fVerbose ); -extern char * Asat_MmFixedEntryFetch( Asat_MmFixed_t * p ); -extern void Asat_MmFixedEntryRecycle( Asat_MmFixed_t * p, char * pEntry ); -extern void Asat_MmFixedRestart( Asat_MmFixed_t * p ); -extern int Asat_MmFixedReadMemUsage( Asat_MmFixed_t * p ); -// flexible-size-block memory manager -extern Asat_MmFlex_t * Asat_MmFlexStart(); -extern void Asat_MmFlexStop( Asat_MmFlex_t * p, int fVerbose ); -extern char * Asat_MmFlexEntryFetch( Asat_MmFlex_t * p, int nBytes ); -extern int Asat_MmFlexReadMemUsage( Asat_MmFlex_t * p ); -// hierarchical memory manager -extern Asat_MmStep_t * Asat_MmStepStart( int nSteps ); -extern void Asat_MmStepStop( Asat_MmStep_t * p, int fVerbose ); -extern char * Asat_MmStepEntryFetch( Asat_MmStep_t * p, int nBytes ); -extern void Asat_MmStepEntryRecycle( Asat_MmStep_t * p, char * pEntry, int nBytes ); -extern int Asat_MmStepReadMemUsage( Asat_MmStep_t * p ); - -#endif - -//////////////////////////////////////////////////////////////////////// -/// END OF FILE /// -//////////////////////////////////////////////////////////////////////// - diff --git a/src/sat/asat/jfront.c b/src/sat/asat/jfront.c deleted file mode 100644 index efbe7883..00000000 --- a/src/sat/asat/jfront.c +++ /dev/null @@ -1,514 +0,0 @@ -/**CFile**************************************************************** - - FileName [jfront.c] - - SystemName [ABC: Logic synthesis and verification system.] - - PackageName [C-language MiniSat solver.] - - Synopsis [Implementation of J-frontier.] - - Author [Alan Mishchenko] - - Affiliation [UC Berkeley] - - Date [Ver. 1.0. Started - June 20, 2005.] - - Revision [$Id: jfront.c,v 1.4 2005/09/16 22:55:03 casem Exp $] - -***********************************************************************/ - -#include <stdio.h> -#include <assert.h> -#include "solver.h" -#include "extra.h" -#include "vec.h" - -/* - At any time during the solving process, the J-frontier is the set of currently - unassigned variables, each of which has at least one fanin/fanout variable that - is currently assigned. In the context of a CNF-based solver, default decisions - based on variable activity are modified to choose the most active variable among - those currently on the J-frontier. -*/ - -//////////////////////////////////////////////////////////////////////// -/// DECLARATIONS /// -//////////////////////////////////////////////////////////////////////// - -// variable on the J-frontier -typedef struct Asat_JVar_t_ Asat_JVar_t; -struct Asat_JVar_t_ -{ - unsigned int Num; // variable number - unsigned int nRefs; // the number of adjacent assigned vars - unsigned int Prev; // the previous variable - unsigned int Next; // the next variable - unsigned int nFans; // the number of fanins/fanouts - unsigned int Fans[0]; // the fanin/fanout variables -}; - -// the J-frontier as a ring of variables -// (ring is used instead of list because it allows to control the insertion point) -typedef struct Asat_JRing_t_ Asat_JRing_t; -struct Asat_JRing_t_ -{ - Asat_JVar_t * pRoot; // the pointer to the root - int nItems; // the number of variables in the ring -}; - -// the J-frontier manager -struct Asat_JMan_t_ -{ - solver * pSat; // the SAT solver - Asat_JRing_t rVars; // the ring of variables - Vec_Ptr_t * vVars; // the pointers to variables - Extra_MmFlex_t * pMem; // the memory manager for variables -}; - -// getting hold of the given variable -static inline Asat_JVar_t * Asat_JManVar( Asat_JMan_t * p, int Num ) { return !Num? NULL : Vec_PtrEntry(p->vVars, Num); } -static inline Asat_JVar_t * Asat_JVarPrev( Asat_JMan_t * p, Asat_JVar_t * pVar ) { return Asat_JManVar(p, pVar->Prev); } -static inline Asat_JVar_t * Asat_JVarNext( Asat_JMan_t * p, Asat_JVar_t * pVar ) { return Asat_JManVar(p, pVar->Next); } - -//The solver can communicate to the variable order the following parts: -//- the array of current assignments (pSat->pAssigns) -//- the array of variable activities (pSat->pdActivity) -//- the array of variables currently in the cone -//- the array of arrays of variables adjacent to each other - -static inline int Asat_JVarIsInBoundary( Asat_JMan_t * p, Asat_JVar_t * pVar ) { return pVar->Next > 0; } -static inline int Asat_JVarIsAssigned( Asat_JMan_t * p, Asat_JVar_t * pVar ) { return p->pSat->assigns[pVar->Num] != l_Undef; } -//static inline int Asat_JVarIsUsedInCone( Asat_JMan_t * p, int Var ) { return p->pSat->vVarsUsed->pArray[i]; } - -// manipulating the ring of variables -static void Asat_JRingAddLast( Asat_JMan_t * p, Asat_JVar_t * pVar ); -static void Asat_JRingRemove( Asat_JMan_t * p, Asat_JVar_t * pVar ); - -// iterator through the entries in J-boundary -#define Asat_JRingForEachEntry( p, pVar, pNext ) \ - for ( pVar = p->rVars.pRoot, \ - pNext = pVar? Asat_JVarNext(p, pVar) : NULL; \ - pVar; \ - pVar = (pNext != p->rVars.pRoot)? pNext : NULL, \ - pNext = pVar? Asat_JVarNext(p, pVar) : NULL ) - -// iterator through the adjacent variables -#define Asat_JVarForEachFanio( p, pVar, pFan, i ) \ - for ( i = 0; (i < (int)pVar->nFans) && (((pFan) = Asat_JManVar(p, pVar->Fans[i])), 1); i++ ) - -extern void Asat_JManAssign( Asat_JMan_t * p, int Var ); - -//////////////////////////////////////////////////////////////////////// -/// FUNCTION DEFINITIONS /// -//////////////////////////////////////////////////////////////////////// - -/**Function************************************************************* - - Synopsis [Start the J-frontier.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -Asat_JMan_t * Asat_JManStart( solver * pSat, void * pCircuit ) -{ - Vec_Vec_t * vCircuit = pCircuit; - Asat_JMan_t * p; - Asat_JVar_t * pVar; - Vec_Int_t * vConnect; - int i, nBytes, Entry, k; - // make sure the number of variables is less than sizeof(unsigned int) - assert( Vec_VecSize(vCircuit) < (1 << 16) ); - assert( Vec_VecSize(vCircuit) == pSat->size ); - // allocate the manager - p = ALLOC( Asat_JMan_t, 1 ); - memset( p, 0, sizeof(Asat_JMan_t) ); - p->pSat = pSat; - p->pMem = Extra_MmFlexStart(); - // fill in the variables - p->vVars = Vec_PtrAlloc( Vec_VecSize(vCircuit) ); - for ( i = 0; i < Vec_VecSize(vCircuit); i++ ) - { - vConnect = Vec_VecEntry( vCircuit, i ); - nBytes = sizeof(Asat_JVar_t) + sizeof(int) * Vec_IntSize(vConnect); - nBytes = sizeof(void *) * (nBytes / sizeof(void *) + ((nBytes % sizeof(void *)) != 0)); - pVar = (Asat_JVar_t *)Extra_MmFlexEntryFetch( p->pMem, nBytes ); - memset( pVar, 0, nBytes ); - pVar->Num = i; - // add fanins/fanouts - pVar->nFans = Vec_IntSize( vConnect ); - Vec_IntForEachEntry( vConnect, Entry, k ) - pVar->Fans[k] = Entry; - // add the variable - Vec_PtrPush( p->vVars, pVar ); - } - // set the current assignments - Vec_PtrForEachEntryStart( p->vVars, pVar, i, 1 ) - { -// if ( !Asat_JVarIsUsedInCone(p, pVar) ) -// continue; - // skip assigned vars, vars in the boundary, and vars not used in the cone - if ( Asat_JVarIsAssigned(p, pVar) ) - Asat_JManAssign( p, pVar->Num ); - } - - pSat->pJMan = p; - return p; -} - -/**Function************************************************************* - - Synopsis [Stops the J-frontier.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Asat_JManStop( solver * pSat ) -{ - Asat_JMan_t * p = pSat->pJMan; - if ( p == NULL ) - return; - pSat->pJMan = NULL; - Extra_MmFlexStop( p->pMem ); - Vec_PtrFree( p->vVars ); - free( p ); -} - - -/**Function************************************************************* - - Synopsis [] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -int Asat_JManCheck( Asat_JMan_t * p ) -{ - Asat_JVar_t * pVar, * pNext, * pFan; -// Msat_IntVec_t * vRound; -// int * pRound, nRound; -// int * pVars, nVars, i, k; - int i, k; - int Counter = 0; - - // go through all the variables in the boundary - Asat_JRingForEachEntry( p, pVar, pNext ) - { - assert( !Asat_JVarIsAssigned(p, pVar) ); - // go though all the variables in the neighborhood - // and check that it is true that there is least one assigned -// vRound = (Msat_IntVec_t *)Msat_ClauseVecReadEntry( p->pSat->vAdjacents, pVar->Num ); -// nRound = Msat_IntVecReadSize( vRound ); -// pRound = Msat_IntVecReadArray( vRound ); -// for ( i = 0; i < nRound; i++ ) - Asat_JVarForEachFanio( p, pVar, pFan, i ) - { -// if ( !Asat_JVarIsUsedInCone(p, pFan) ) -// continue; - if ( Asat_JVarIsAssigned(p, pFan) ) - break; - } -// assert( i != pVar->nFans ); -// if ( i == pVar->nFans ) -// return 0; - if ( i == (int)pVar->nFans ) - Counter++; - } - if ( Counter > 0 ) - printf( "%d(%d) ", Counter, p->rVars.nItems ); - - // we may also check other unassigned variables in the cone - // to make sure that if they are not in J-boundary, - // then they do not have an assigned neighbor -// nVars = Msat_IntVecReadSize( p->pSat->vConeVars ); -// pVars = Msat_IntVecReadArray( p->pSat->vConeVars ); -// for ( i = 0; i < nVars; i++ ) - Vec_PtrForEachEntry( p->vVars, pVar, i ) - { -// assert( Asat_JVarIsUsedInCone(p, pVar) ); - // skip assigned vars, vars in the boundary, and vars not used in the cone - if ( Asat_JVarIsAssigned(p, pVar) || Asat_JVarIsInBoundary(p, pVar) ) - continue; - // make sure, it does not have assigned neighbors -// vRound = (Msat_IntVec_t *)Msat_ClauseVecReadEntry( p->pSat->vAdjacents, pVars[i] ); -// nRound = Msat_IntVecReadSize( vRound ); -// pRound = Msat_IntVecReadArray( vRound ); -// for ( i = 0; i < nRound; i++ ) - Asat_JVarForEachFanio( p, pVar, pFan, k ) - { -// if ( !Asat_JVarIsUsedInCone(p, pFan) ) -// continue; - if ( Asat_JVarIsAssigned(p, pFan) ) - break; - } -// assert( k == pVar->nFans ); -// if ( k != pVar->nFans ) -// return 0; - } - return 1; -} - -/**Function************************************************************* - - Synopsis [] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Asat_JManAssign( Asat_JMan_t * p, int Var ) -{ -// Msat_IntVec_t * vRound; - Asat_JVar_t * pVar, * pFan; - int i, clk = clock(); - - // make sure the variable is in the boundary - assert( Var < Vec_PtrSize(p->vVars) ); - // if it is not in the boundary (initial decision, random decision), do not remove - pVar = Asat_JManVar( p, Var ); - if ( Asat_JVarIsInBoundary( p, pVar ) ) - Asat_JRingRemove( p, pVar ); - // add to the boundary those neighbors that are (1) unassigned, (2) not in boundary - // because for them we know that there is a variable (Var) which is assigned -// vRound = (Msat_IntVec_t *)p->pSat->vAdjacents->pArray[Var]; -// for ( i = 0; i < vRound->nSize; i++ ) - Asat_JVarForEachFanio( p, pVar, pFan, i ) - { -// if ( !Asat_JVarIsUsedInCone(p, pFan) ) -// continue; - pFan->nRefs++; - if ( Asat_JVarIsAssigned(p, pFan) || Asat_JVarIsInBoundary(p, pFan) ) - continue; - Asat_JRingAddLast( p, pFan ); - } -//timeSelect += clock() - clk; -// Asat_JManCheck( p ); - p->pSat->timeUpdate += clock() - clk; -} - -/**Function************************************************************* - - Synopsis [] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Asat_JManUnassign( Asat_JMan_t * p, int Var ) -{ -// Msat_IntVec_t * vRound, * vRound2; - Asat_JVar_t * pVar, * pFan; - int i, clk = clock();//, k - - // make sure the variable is not in the boundary - assert( Var < Vec_PtrSize(p->vVars) ); - pVar = Asat_JManVar( p, Var ); - assert( !Asat_JVarIsInBoundary( p, pVar ) ); - // go through its neigbors - if one of them is assigned add this var - // add to the boundary those neighbors that are not there already - // this will also get rid of variable outside of the current cone - // because they are unassigned in Msat_SolverPrepare() -// vRound = (Msat_IntVec_t *)p->pSat->vAdjacents->pArray[Var]; -// for ( i = 0; i < vRound->nSize; i++ ) -// if ( Asat_JVarIsAssigned(p, vRound->pArray[i]) ) -// break; -// if ( i != vRound->nSize ) -// Asat_JRingAddLast( &p->rVars, &p->pVars[Var] ); - if ( pVar->nRefs != 0 ) - Asat_JRingAddLast( p, pVar ); - -/* - // unassigning a variable may lead to its adjacents dropping from the boundary - for ( i = 0; i < vRound->nSize; i++ ) - if ( Asat_JVarIsInBoundary(p, vRound->pArray[i]) ) - { // the neighbor is in the J-boundary (and unassigned) - assert( !Asat_JVarIsAssigned(p, vRound->pArray[i]) ); - vRound2 = (Msat_IntVec_t *)p->pSat->vAdjacents->pArray[vRound->pArray[i]]; - // go through its neighbors and determine if there is at least one assigned - for ( k = 0; k < vRound2->nSize; k++ ) - if ( Asat_JVarIsAssigned(p, vRound2->pArray[k]) ) - break; - if ( k == vRound2->nSize ) // there is no assigned vars, delete this one - Asat_JRingRemove( &p->rVars, &p->pVars[vRound->pArray[i]] ); - } -*/ - Asat_JVarForEachFanio( p, pVar, pFan, i ) - { -// if ( !Asat_JVarIsUsedInCone(p, pFan) ) -// continue; - assert( pFan->nRefs > 0 ); - pFan->nRefs--; - if ( !Asat_JVarIsInBoundary(p, pFan) ) - continue; - // the neighbor is in the J-boundary (and unassigned) - assert( !Asat_JVarIsAssigned(p, pFan) ); - // if there is no assigned vars, delete this one - if ( pFan->nRefs == 0 ) - Asat_JRingRemove( p, pFan ); - } - -//timeSelect += clock() - clk; -// Asat_JManCheck( p ); - p->pSat->timeUpdate += clock() - clk; -} - -/**Function************************************************************* - - Synopsis [] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -int Asat_JManSelect( Asat_JMan_t * p ) -{ - Asat_JVar_t * pVar, * pNext, * pVarBest; - double * pdActs = p->pSat->activity; - double dfActBest; - int clk = clock(); - - pVarBest = NULL; - dfActBest = -1.0; - Asat_JRingForEachEntry( p, pVar, pNext ) - { - if ( dfActBest <= pdActs[pVar->Num] )//+ 0.00001 ) - { - dfActBest = pdActs[pVar->Num]; - pVarBest = pVar; - } - } -//timeSelect += clock() - clk; -//timeAssign += clock() - clk; -//if ( pVarBest && pVarBest->Num % 1000 == 0 ) -//printf( "%d ", p->rVars.nItems ); - -// Asat_JManCheck( p ); - p->pSat->timeSelect += clock() - clk; - if ( pVarBest ) - { -// assert( Asat_JVarIsUsedInCone(p, pVarBest) ); - return pVarBest->Num; - } - return var_Undef; -} - - - -/**Function************************************************************* - - Synopsis [Adds node to the end of the ring.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Asat_JRingAddLast( Asat_JMan_t * p, Asat_JVar_t * pVar ) -{ - Asat_JRing_t * pRing = &p->rVars; -//printf( "adding %d\n", pVar->Num ); - // check that the node is not in a ring - assert( pVar->Prev == 0 ); - assert( pVar->Next == 0 ); - // if the ring is empty, make the node point to itself - pRing->nItems++; - if ( pRing->pRoot == NULL ) - { - pRing->pRoot = pVar; -// pVar->pPrev = pVar; - pVar->Prev = pVar->Num; -// pVar->pNext = pVar; - pVar->Next = pVar->Num; - return; - } - // if the ring is not empty, add it as the last entry -// pVar->pPrev = pRing->pRoot->pPrev; - pVar->Prev = pRing->pRoot->Prev; -// pVar->pNext = pRing->pRoot; - pVar->Next = pRing->pRoot->Num; -// pVar->pPrev->pNext = pVar; - Asat_JVarPrev(p, pVar)->Next = pVar->Num; -// pVar->pNext->pPrev = pVar; - Asat_JVarNext(p, pVar)->Prev = pVar->Num; - - // move the root so that it points to the new entry -// pRing->pRoot = pRing->pRoot->pPrev; - pRing->pRoot = Asat_JVarPrev(p, pRing->pRoot); -} - -/**Function************************************************************* - - Synopsis [Removes the node from the ring.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Asat_JRingRemove( Asat_JMan_t * p, Asat_JVar_t * pVar ) -{ - Asat_JRing_t * pRing = &p->rVars; -//printf( "removing %d\n", pVar->Num ); - // check that the var is in a ring - assert( pVar->Prev ); - assert( pVar->Next ); - pRing->nItems--; - if ( pRing->nItems == 0 ) - { - assert( pRing->pRoot == pVar ); -// pVar->pPrev = NULL; - pVar->Prev = 0; -// pVar->pNext = NULL; - pVar->Next = 0; - pRing->pRoot = NULL; - return; - } - // move the root if needed - if ( pRing->pRoot == pVar ) -// pRing->pRoot = pVar->pNext; - pRing->pRoot = Asat_JVarNext(p, pVar); - // move the root to the next entry after pVar - // this way all the additions to the list will be traversed first -// pRing->pRoot = pVar->pNext; - pRing->pRoot = Asat_JVarPrev(p, pVar); - // delete the node -// pVar->pPrev->pNext = pVar->pNext; - Asat_JVarPrev(p, pVar)->Next = Asat_JVarNext(p, pVar)->Num; -// pVar->pNext->pPrev = pVar->pPrev; - Asat_JVarNext(p, pVar)->Prev = Asat_JVarPrev(p, pVar)->Num; -// pVar->pPrev = NULL; - pVar->Prev = 0; -// pVar->pNext = NULL; - pVar->Next = 0; -} - -//////////////////////////////////////////////////////////////////////// -/// END OF FILE /// -//////////////////////////////////////////////////////////////////////// - - diff --git a/src/sat/asat/main.c b/src/sat/asat/main.c deleted file mode 100644 index cbad5ba1..00000000 --- a/src/sat/asat/main.c +++ /dev/null @@ -1,195 +0,0 @@ -/************************************************************************************************** -MiniSat -- Copyright (c) 2005, Niklas Sorensson -http://www.cs.chalmers.se/Cs/Research/FormalMethods/MiniSat/ - -Permission is hereby granted, free of charge, to any person obtaining a copy of this software and -associated documentation files (the "Software"), to deal in the Software without restriction, -including without limitation the rights to use, copy, modify, merge, publish, distribute, -sublicense, and/or sell copies of the Software, and to permit persons to whom the Software is -furnished to do so, subject to the following conditions: - -The above copyright notice and this permission notice shall be included in all copies or -substantial portions of the Software. - -THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR IMPLIED, INCLUDING BUT -NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND -NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, -DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT -OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE. -**************************************************************************************************/ -// Modified to compile with MS Visual Studio 6.0 by Alan Mishchenko - -#include "solver.h" - -#include <stdio.h> -#include <stdlib.h> -#include <time.h> -//#include <unistd.h> -//#include <signal.h> -//#include <zlib.h> -//#include <sys/time.h> -//#include <sys/resource.h> - -//================================================================================================= -// Helpers: - - -// Reads an input stream to end-of-file and returns the result as a 'char*' terminated by '\0' -// (dynamic allocation in case 'in' is standard input). -// -char* readFile(FILE * in) -{ - char* data = malloc(65536); - int cap = 65536; - int size = 0; - - while (!feof(in)){ - if (size == cap){ - cap *= 2; - data = realloc(data, cap); } - size += fread(&data[size], 1, 65536, in); - } - data = realloc(data, size+1); - data[size] = '\0'; - - return data; -} - -//static inline double cpuTime(void) { -// struct rusage ru; -// getrusage(RUSAGE_SELF, &ru); -// return (double)ru.ru_utime.tv_sec + (double)ru.ru_utime.tv_usec / 1000000; } - - -//================================================================================================= -// DIMACS Parser: - - -static inline void skipWhitespace(char** in) { - while ((**in >= 9 && **in <= 13) || **in == 32) - (*in)++; } - -static inline void skipLine(char** in) { - for (;;){ - if (**in == 0) return; - if (**in == '\n') { (*in)++; return; } - (*in)++; } } - -static inline int parseInt(char** in) { - int val = 0; - int _neg = 0; - skipWhitespace(in); - if (**in == '-') _neg = 1, (*in)++; - else if (**in == '+') (*in)++; - if (**in < '0' || **in > '9') fprintf(stderr, "PARSE ERROR! Unexpected char: %c\n", **in), exit(1); - while (**in >= '0' && **in <= '9') - val = val*10 + (**in - '0'), - (*in)++; - return _neg ? -val : val; } - -static void readClause(char** in, solver* s, vec* lits) { - int parsed_lit, var; - vec_resize(lits,0); - for (;;){ - parsed_lit = parseInt(in); - if (parsed_lit == 0) break; - var = abs(parsed_lit)-1; - vec_push(lits, (void*)(parsed_lit > 0 ? toLit(var) : neg(toLit(var)))); - } -} - -static lbool parse_DIMACS_main(char* in, solver* s) { - vec lits; - vec_new(&lits); - - for (;;){ - skipWhitespace(&in); - if (*in == 0) - break; - else if (*in == 'c' || *in == 'p') - skipLine(&in); - else{ - lit* begin; - readClause(&in, s, &lits); - begin = (lit*)vec_begin(&lits); - if (solver_addclause(s, begin, begin+vec_size(&lits)) == l_False){ - vec_delete(&lits); - return l_False; - } - } - } - vec_delete(&lits); - return solver_simplify(s); -} - - -// Inserts problem into solver. Returns FALSE upon immediate conflict. -// -static lbool parse_DIMACS(FILE * in, solver* s) { - char* text = readFile(in); - lbool ret = parse_DIMACS_main(text, s); - free(text); - return ret; } - - -//================================================================================================= - - -void printStats(stats* stats, int cpu_time) -{ - double Time = (float)(cpu_time)/(float)(CLOCKS_PER_SEC); - printf("restarts : %12d\n", stats->starts); - printf("conflicts : %12.0f (%9.0f / sec )\n", (double)stats->conflicts , (double)stats->conflicts /Time); - printf("decisions : %12.0f (%9.0f / sec )\n", (double)stats->decisions , (double)stats->decisions /Time); - printf("propagations : %12.0f (%9.0f / sec )\n", (double)stats->propagations, (double)stats->propagations/Time); - printf("inspects : %12.0f (%9.0f / sec )\n", (double)stats->inspects , (double)stats->inspects /Time); - printf("conflict literals : %12.0f (%9.2f %% deleted )\n", (double)stats->tot_literals, (double)(stats->max_literals - stats->tot_literals) * 100.0 / (double)stats->max_literals); - printf("CPU time : %12.2f sec\n", Time); -} - -//solver* slv; -//static void SIGINT_handler(int signum) { -// printf("\n"); printf("*** INTERRUPTED ***\n"); -// printStats(&slv->stats, cpuTime()); -// printf("\n"); printf("*** INTERRUPTED ***\n"); -// exit(0); } - - -//================================================================================================= - - -int main(int argc, char** argv) -{ - solver* s = solver_new(); - lbool st; - FILE * in; - int clk = clock(); - - if (argc != 2) - fprintf(stderr, "ERROR! Not enough command line arguments.\n"), - exit(1); - - in = fopen(argv[1], "rb"); - if (in == NULL) - fprintf(stderr, "ERROR! Could not open file: %s\n", argc == 1 ? "<stdin>" : argv[1]), - exit(1); - st = parse_DIMACS(in, s); - fclose(in); - - if (st == l_False){ - solver_delete(s); - printf("Trivial problem\nUNSATISFIABLE\n"); - exit(20); - } - - s->verbosity = 1; -// slv = s; -// signal(SIGINT,SIGINT_handler); - st = solver_solve(s,0,0); - printStats(&s->stats, clock() - clk); - printf("\n"); - printf(st == l_True ? "SATISFIABLE\n" : "UNSATISFIABLE\n"); - - solver_delete(s); - return 0; -} diff --git a/src/sat/asat/module.make b/src/sat/asat/module.make deleted file mode 100644 index 26489191..00000000 --- a/src/sat/asat/module.make +++ /dev/null @@ -1,4 +0,0 @@ -SRC += src/sat/asat/added.c \ - src/sat/asat/asatmem.c \ - src/sat/asat/jfront.c \ - src/sat/asat/solver.c diff --git a/src/sat/asat/solver.c b/src/sat/asat/solver.c deleted file mode 100644 index b9851a54..00000000 --- a/src/sat/asat/solver.c +++ /dev/null @@ -1,1290 +0,0 @@ -/************************************************************************************************** -MiniSat -- Copyright (c) 2005, Niklas Sorensson -http://www.cs.chalmers.se/Cs/Research/FormalMethods/MiniSat/ - -Permission is hereby granted, free of charge, to any person obtaining a copy of this software and -associated documentation files (the "Software"), to deal in the Software without restriction, -including without limitation the rights to use, copy, modify, merge, publish, distribute, -sublicense, and/or sell copies of the Software, and to permit persons to whom the Software is -furnished to do so, subject to the following conditions: - -The above copyright notice and this permission notice shall be included in all copies or -substantial portions of the Software. - -THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR IMPLIED, INCLUDING BUT -NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND -NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, -DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT -OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE. -**************************************************************************************************/ -// Modified to compile with MS Visual Studio 6.0 by Alan Mishchenko - -#include <stdio.h> -#include <string.h> -#include <assert.h> -#include <math.h> -#include <time.h> - -#include "solver.h" - -#define ASAT_USE_SYSTEM_MEMORY_MANAGEMENT - -//================================================================================================= -// Simple (var/literal) helpers: - -static inline int lit_var(lit l) { return l >> 1; } -static inline int lit_sign(lit l) { return (l & 1); } - -//================================================================================================= -// Debug: - -//#define VERBOSEDEBUG - -// For derivation output (verbosity level 2) -#define L_IND "%-*d" -#define L_ind solver_dlevel(s)*3+3,solver_dlevel(s) -#define L_LIT "%sx%d" -#define L_lit(p) lit_sign(p)?"~":"", (lit_var(p)) - -// Just like 'assert()' but expression will be evaluated in the release version as well. -static inline void check(int expr) { assert(expr); } - -static void printlits(lit* begin, lit* end) -{ - int i; - for (i = 0; i < end - begin; i++) - printf(L_LIT" ",L_lit(begin[i])); -} - -//================================================================================================= -// Random numbers: - - -// Returns a random float 0 <= x < 1. Seed must never be 0. -static inline double drand(double* seed) { - int q; - *seed *= 1389796; - q = (int)(*seed / 2147483647); - *seed -= (double)q * 2147483647; - return *seed / 2147483647; } - - -// Returns a random integer 0 <= x < size. Seed must never be 0. -static inline int irand(double* seed, int size) { - return (int)(drand(seed) * size); } - - -//================================================================================================= -// Predeclarations: - -void sort(void** array, int size, int(*comp)(const void *, const void *)); - -//================================================================================================= -// Clause datatype + minor functions: - -struct clause_t -{ - int size_learnt; - lit lits[0]; -}; - -static inline int clause_size (clause* c) { return c->size_learnt >> 1; } -static inline lit* clause_begin (clause* c) { return c->lits; } -static inline int clause_learnt (clause* c) { return c->size_learnt & 1; } -static inline float clause_activity (clause* c) { return *((float*)&c->lits[c->size_learnt>>1]); } -static inline void clause_setactivity(clause* c, float a) { *((float*)&c->lits[c->size_learnt>>1]) = a; } - -//================================================================================================= -// Encode literals in clause pointers: - -clause* clause_from_lit (lit l) { return (clause*)(((unsigned long)l) + ((unsigned long)l) + 1); } -bool clause_is_lit (clause* c) { return ((unsigned long)c & 1); } -lit clause_read_lit (clause* c) { return (lit)((unsigned long)c >> 1); } - -//================================================================================================= -// Simple helpers: - -static inline int solver_dlevel(solver* s) { return veci_size(&s->trail_lim); } -static inline vec* solver_read_wlist (solver* s, lit l){ return &s->wlists[l]; } -static inline void vec_remove(vec* v, void* e) -{ - void** ws = vec_begin(v); - int j = 0; - - for (; ws[j] != e ; j++); - assert(j < vec_size(v)); - for (; j < vec_size(v)-1; j++) ws[j] = ws[j+1]; - vec_resize(v,vec_size(v)-1); -} - -//================================================================================================= -// Variable order functions: - -static inline void order_update(solver* s, int v) // updateorder -{ -// int clk = clock(); - int* orderpos = s->orderpos; - double* activity = s->activity; - int* heap = veci_begin(&s->order); - int i = orderpos[v]; - int x = heap[i]; - int parent = (i - 1) / 2; - - assert(s->orderpos[v] != -1); - - while (i != 0 && activity[x] > activity[heap[parent]]){ - heap[i] = heap[parent]; - orderpos[heap[i]] = i; - i = parent; - parent = (i - 1) / 2; - } - heap[i] = x; - orderpos[x] = i; -// s->timeUpdate += clock() - clk; -} - -static inline void order_assigned(solver* s, int v) -{ -} - -static inline void order_unassigned(solver* s, int v) // undoorder -{ -// int clk = clock(); - int* orderpos = s->orderpos; - if (orderpos[v] == -1){ - orderpos[v] = veci_size(&s->order); - veci_push(&s->order,v); - order_update(s,v); - } -// s->timeUpdate += clock() - clk; -} - -static int order_select(solver* s, float random_var_freq) // selectvar -{ -// int clk = clock(); - static int Counter = 0; - int* heap; - double* activity; - int* orderpos; - - lbool* values = s->assigns; - - // The first decisions - if ( s->pPrefVars && s->nPrefDecNum < s->nPrefVars ) - { - int i; - s->nPrefDecNum++; - for ( i = 0; i < s->nPrefVars; i++ ) - if ( values[s->pPrefVars[i]] == l_Undef ) - return s->pPrefVars[i]; - } - - // Random decision: - if (drand(&s->random_seed) < random_var_freq){ - int next = irand(&s->random_seed,s->size); - assert(next >= 0 && next < s->size); - if (values[next] == l_Undef) - return next; - } - - // Activity based decision: - - heap = veci_begin(&s->order); - activity = s->activity; - orderpos = s->orderpos; - - - while (veci_size(&s->order) > 0){ - int next = heap[0]; - int size = veci_size(&s->order)-1; - int x = heap[size]; - - veci_resize(&s->order,size); - - orderpos[next] = -1; - - if (size > 0){ - double act = activity[x]; - - int i = 0; - int child = 1; - - - while (child < size){ - if (child+1 < size && activity[heap[child]] < activity[heap[child+1]]) - child++; - - assert(child < size); - - if (act >= activity[heap[child]]) - break; - - heap[i] = heap[child]; - orderpos[heap[i]] = i; - i = child; - child = 2 * child + 1; - } - heap[i] = x; - orderpos[heap[i]] = i; - } - - if (values[next] == l_Undef) - return next; - } - -// s->timeSelect += clock() - clk; - return var_Undef; -} - -// J-frontier -extern void Asat_JManAssign( Asat_JMan_t * p, int Var ); -extern void Asat_JManUnassign( Asat_JMan_t * p, int Var ); -extern int Asat_JManSelect( Asat_JMan_t * p ); - -//================================================================================================= -// Activity functions: - -static inline void act_var_rescale(solver* s) { - double* activity = s->activity; - int i; - for (i = 0; i < s->size; i++) - activity[i] *= 1e-100; - s->var_inc *= 1e-100; -} - -static inline void act_var_bump(solver* s, int v) { - double* activity = s->activity; - activity[v] += s->var_inc; -// activity[v] += s->var_inc * s->factors[v]; - if (activity[v] > 1e100) - act_var_rescale(s); - //printf("bump %d %f\n", v-1, activity[v]); - if ( s->pJMan == NULL && s->orderpos[v] != -1 ) - order_update(s,v); - -} - -static inline void act_var_decay(solver* s) { s->var_inc *= s->var_decay; } - -static inline void act_clause_rescale(solver* s) { - clause** cs = (clause**)vec_begin(&s->learnts); - int i; - for (i = 0; i < vec_size(&s->learnts); i++){ - float a = clause_activity(cs[i]); - clause_setactivity(cs[i], a * (float)1e-20); - } - s->cla_inc *= (float)1e-20; -} - - -static inline void act_clause_bump(solver* s, clause *c) { - float a = clause_activity(c) + s->cla_inc; - clause_setactivity(c,a); - if (a > 1e20) act_clause_rescale(s); -} - -static inline void act_clause_decay(solver* s) { s->cla_inc *= s->cla_decay; } - - -//================================================================================================= -// Clause functions: - -/* pre: size > 1 && no variable occurs twice - */ -static clause* clause_new(solver* s, lit* begin, lit* end, int learnt) -{ - int size; - clause* c; - int i; - - assert(end - begin > 1); - assert(learnt >= 0 && learnt < 2); - size = end - begin; - -// c = (clause*)malloc(sizeof(clause) + sizeof(lit) * size + learnt * sizeof(float)); -#ifdef ASAT_USE_SYSTEM_MEMORY_MANAGEMENT - c = (clause*)malloc(sizeof(clause) + sizeof(lit) * size + learnt * sizeof(float)); -#else - c = (clause*)Asat_MmStepEntryFetch( s->pMem, sizeof(clause) + sizeof(lit) * size + learnt * sizeof(float) ); -#endif - - c->size_learnt = (size << 1) | learnt; - assert(((unsigned int)c & 1) == 0); - - for (i = 0; i < size; i++) - { - assert(begin[i] >= 0); - c->lits[i] = begin[i]; - } - - if (learnt) - *((float*)&c->lits[size]) = 0.0; - - assert(begin[0] >= 0); - assert(begin[0] < s->size*2); - assert(begin[1] >= 0); - assert(begin[1] < s->size*2); - - assert(neg(begin[0]) < s->size*2); - assert(neg(begin[1]) < s->size*2); - - //vec_push(solver_read_wlist(s,neg(begin[0])),(void*)c); - //vec_push(solver_read_wlist(s,neg(begin[1])),(void*)c); - - vec_push(solver_read_wlist(s,neg(begin[0])),(void*)(size > 2 ? c : clause_from_lit(begin[1]))); - vec_push(solver_read_wlist(s,neg(begin[1])),(void*)(size > 2 ? c : clause_from_lit(begin[0]))); - - return c; -} - - -static void clause_remove(solver* s, clause* c) -{ - lit* lits = clause_begin(c); - assert(neg(lits[0]) < s->size*2); - assert(neg(lits[1]) < s->size*2); - assert(lits[0] < s->size*2); - - //vec_remove(solver_read_wlist(s,neg(lits[0])),(void*)c); - //vec_remove(solver_read_wlist(s,neg(lits[1])),(void*)c); - - vec_remove(solver_read_wlist(s,neg(lits[0])),(void*)(clause_size(c) > 2 ? c : clause_from_lit(lits[1]))); - vec_remove(solver_read_wlist(s,neg(lits[1])),(void*)(clause_size(c) > 2 ? c : clause_from_lit(lits[0]))); - - if (clause_learnt(c)){ - s->solver_stats.learnts--; - s->solver_stats.learnts_literals -= clause_size(c); - }else{ - s->solver_stats.clauses--; - s->solver_stats.clauses_literals -= clause_size(c); - } - -#ifdef ASAT_USE_SYSTEM_MEMORY_MANAGEMENT - free(c); -#else - Asat_MmStepEntryRecycle( s->pMem, (char *)c, sizeof(clause) + sizeof(lit) * clause_size(c) + clause_learnt(c) * sizeof(float) ); -#endif - -} - - -static lbool clause_simplify(solver* s, clause* c) -{ - lit* lits = clause_begin(c); - lbool* values = s->assigns; - int i; - - assert(solver_dlevel(s) == 0); - - for (i = 0; i < clause_size(c); i++){ - lbool sig = !lit_sign(lits[i]); sig += sig - 1; - if (values[lit_var(lits[i])] == sig) - return l_True; - } - return l_False; -} - -//================================================================================================= -// Minor (solver) functions: - -static void solver_setnvars(solver* s,int n) -{ - int var; - if (s->cap < n){ - - while (s->cap < n) s->cap = s->cap*2+1; - - s->wlists = (vec*) realloc(s->wlists, sizeof(vec)*s->cap*2); - s->activity = (double*) realloc(s->activity, sizeof(double)*s->cap); - s->assigns = (lbool*) realloc(s->assigns, sizeof(lbool)*s->cap); - s->orderpos = (int*) realloc(s->orderpos, sizeof(int)*s->cap); - s->reasons = (clause**)realloc(s->reasons, sizeof(clause*)*s->cap); - s->levels = (int*) realloc(s->levels, sizeof(int)*s->cap); - s->tags = (lbool*) realloc(s->tags, sizeof(lbool)*s->cap); - s->trail = (lit*) realloc(s->trail, sizeof(lit)*s->cap); - } - - for (var = s->size; var < n; var++){ - vec_new(&s->wlists[2*var]); - vec_new(&s->wlists[2*var+1]); - s->activity [var] = 0; - s->assigns [var] = l_Undef; - s->orderpos [var] = var; - s->reasons [var] = (clause*)0; - s->levels [var] = 0; - s->tags [var] = l_Undef; - - assert(veci_size(&s->order) == var); - veci_push(&s->order,var); - order_update(s,var); - } - - s->size = n > s->size ? n : s->size; -} - - -static inline bool enqueue(solver* s, lit l, clause* from) -{ - lbool* values = s->assigns; - int v = lit_var(l); - lbool val = values[v]; - lbool sig = !lit_sign(l); sig += sig - 1; -#ifdef VERBOSEDEBUG - printf(L_IND"enqueue("L_LIT")\n", L_ind, L_lit(l)); -#endif - if (val != l_Undef){ - return val == sig; - }else{ - // New fact -- store it. - int* levels = s->levels; - clause** reasons = s->reasons; -#ifdef VERBOSEDEBUG - printf(L_IND"bind("L_LIT")\n", L_ind, L_lit(l)); -#endif - - values [v] = sig; - levels [v] = solver_dlevel(s); - reasons[v] = from; - s->trail[s->qtail++] = l; - - if ( s->pJMan ) - Asat_JManAssign( s->pJMan, v ); - else - order_assigned(s, v); - return 1; - } -} - - -static inline void assume(solver* s, lit l){ - assert(s->qtail == s->qhead); - assert(s->assigns[lit_var(l)] == l_Undef); -#ifdef VERBOSEDEBUG - printf(L_IND"assume("L_LIT")\n", L_ind, L_lit(l)); -#endif - veci_push(&s->trail_lim,s->qtail); - enqueue(s,l,(clause*)0); -} - - -static inline void solver_canceluntil(solver* s, int level) { - lit* trail; - lbool* values; - clause** reasons; - int bound; - int c; - - if (solver_dlevel(s) <= level) - return; - - trail = s->trail; - values = s->assigns; - reasons = s->reasons; - bound = veci_begin(&s->trail_lim)[level]; - - for (c = s->qtail-1; c >= bound; c--) { - int x = lit_var(trail[c]); - values [x] = l_Undef; - reasons[x] = (clause*)0; - } - - if ( s->pJMan ) - for (c = s->qtail-1; c >= bound; c--) - Asat_JManUnassign( s->pJMan, lit_var(trail[c]) ); - else - for (c = s->qhead-1; c >= bound; c--) - order_unassigned( s, lit_var(trail[c]) ); - - s->qhead = s->qtail = bound; - veci_resize(&s->trail_lim,level); -} - -static void solver_record(solver* s, veci* cls) -{ - lit* begin = veci_begin(cls); - lit* end = begin + veci_size(cls); - clause* c = (veci_size(cls) > 1) ? clause_new(s,begin,end,1) : (clause*)0; - enqueue(s,*begin,c); - -Sat_SolverTraceWrite( s, begin, end, 0 ); - - assert(veci_size(cls) > 0); - - if (c != 0) { - vec_push(&s->learnts,(void*)c); - act_clause_bump(s,c); - s->solver_stats.learnts++; - s->solver_stats.learnts_literals += veci_size(cls); - } -} - - -static double solver_progress(solver* s) -{ - lbool* values = s->assigns; - int* levels = s->levels; - int i; - - double progress = 0; - double F = 1.0 / s->size; - for (i = 0; i < s->size; i++) - if (values[i] != l_Undef) - progress += pow(F, levels[i]); - return progress / s->size; -} - -//================================================================================================= -// Major methods: - -static bool solver_lit_removable(solver* s, lit l, int minl) -{ - lbool* tags = s->tags; - clause** reasons = s->reasons; - int* levels = s->levels; - int top = veci_size(&s->tagged); - - assert(lit_var(l) >= 0 && lit_var(l) < s->size); - assert(reasons[lit_var(l)] != 0); - veci_resize(&s->stack,0); - veci_push(&s->stack,lit_var(l)); - - while (veci_size(&s->stack) > 0){ - clause* c; - int v = veci_begin(&s->stack)[veci_size(&s->stack)-1]; - assert(v >= 0 && v < s->size); - veci_resize(&s->stack,veci_size(&s->stack)-1); - assert(reasons[v] != 0); - c = reasons[v]; - - if (clause_is_lit(c)){ - int v = lit_var(clause_read_lit(c)); - if (tags[v] == l_Undef && levels[v] != 0){ - if (reasons[v] != 0 && ((1 << (levels[v] & 31)) & minl)){ - veci_push(&s->stack,v); - tags[v] = l_True; - veci_push(&s->tagged,v); - }else{ - int* tagged = veci_begin(&s->tagged); - int j; - for (j = top; j < veci_size(&s->tagged); j++) - tags[tagged[j]] = l_Undef; - veci_resize(&s->tagged,top); - return 0; - } - } - }else{ - lit* lits = clause_begin(c); - int i, j; - - for (i = 1; i < clause_size(c); i++){ - int v = lit_var(lits[i]); - if (tags[v] == l_Undef && levels[v] != 0){ - if (reasons[v] != 0 && ((1 << (levels[v] & 31)) & minl)){ - - veci_push(&s->stack,lit_var(lits[i])); - tags[v] = l_True; - veci_push(&s->tagged,v); - }else{ - int* tagged = veci_begin(&s->tagged); - for (j = top; j < veci_size(&s->tagged); j++) - tags[tagged[j]] = l_Undef; - veci_resize(&s->tagged,top); - return 0; - } - } - } - } - } - - return 1; -} - -static void solver_analyze(solver* s, clause* c, veci* learnt) -{ - lit* trail = s->trail; - lbool* tags = s->tags; - clause** reasons = s->reasons; - int* levels = s->levels; - int cnt = 0; - lit p = lit_Undef; - int ind = s->qtail-1; - lit* lits; - int i, j, minl; - int* tagged; - - veci_push(learnt,lit_Undef); - - do{ - assert(c != 0); - - if (clause_is_lit(c)){ - lit q = clause_read_lit(c); - assert(lit_var(q) >= 0 && lit_var(q) < s->size); - if (tags[lit_var(q)] == l_Undef && levels[lit_var(q)] > 0){ - tags[lit_var(q)] = l_True; - veci_push(&s->tagged,lit_var(q)); - act_var_bump(s,lit_var(q)); - if (levels[lit_var(q)] == solver_dlevel(s)) - cnt++; - else - veci_push(learnt,q); - } - }else{ - - if (clause_learnt(c)) - act_clause_bump(s,c); - - lits = clause_begin(c); - //printlits(lits,lits+clause_size(c)); printf("\n"); - for (j = (p == lit_Undef ? 0 : 1); j < clause_size(c); j++){ - lit q = lits[j]; - assert(lit_var(q) >= 0 && lit_var(q) < s->size); - if (tags[lit_var(q)] == l_Undef && levels[lit_var(q)] > 0){ - tags[lit_var(q)] = l_True; - veci_push(&s->tagged,lit_var(q)); - act_var_bump(s,lit_var(q)); - if (levels[lit_var(q)] == solver_dlevel(s)) - cnt++; - else - veci_push(learnt,q); - } - } - } - - while (tags[lit_var(trail[ind--])] == l_Undef); - - p = trail[ind+1]; - c = reasons[lit_var(p)]; - cnt--; - - }while (cnt > 0); - -// *veci_begin(learnt) = neg(p); - - lits = veci_begin(learnt); - lits[0] = neg(p); - - minl = 0; - for (i = 1; i < veci_size(learnt); i++){ - int lev = levels[lit_var(lits[i])]; - minl |= 1 << (lev & 31); - } - - // simplify (full) - for (i = j = 1; i < veci_size(learnt); i++){ - if (reasons[lit_var(lits[i])] == 0 || !solver_lit_removable(s,lits[i],minl)) - lits[j++] = lits[i]; - } -// j = veci_size(learnt); - - // update size of learnt + statistics - s->solver_stats.max_literals += veci_size(learnt); - veci_resize(learnt,j); - s->solver_stats.tot_literals += j; - - // clear tags - tagged = veci_begin(&s->tagged); - for (i = 0; i < veci_size(&s->tagged); i++) - tags[tagged[i]] = l_Undef; - veci_resize(&s->tagged,0); - -#ifdef DEBUG - for (i = 0; i < s->size; i++) - assert(tags[i] == l_Undef); -#endif - -#ifdef VERBOSEDEBUG - printf(L_IND"Learnt {", L_ind); - for (i = 0; i < veci_size(learnt); i++) printf(" "L_LIT, L_lit(lits[i])); -#endif - if (veci_size(learnt) > 1){ - int max_i = 1; - int max = levels[lit_var(lits[1])]; - lit tmp; - - for (i = 2; i < veci_size(learnt); i++) - if (levels[lit_var(lits[i])] > max){ - max = levels[lit_var(lits[i])]; - max_i = i; - } - - tmp = lits[1]; - lits[1] = lits[max_i]; - lits[max_i] = tmp; - } -#ifdef VERBOSEDEBUG - { - int lev = veci_size(learnt) > 1 ? levels[lit_var(lits[1])] : 0; - printf(" } at level %d\n", lev); - } -#endif -} - - -clause* solver_propagate(solver* s) -{ - lbool* values = s->assigns; - clause* confl = (clause*)0; - lit* lits; - - //printf("solver_propagate\n"); - while (confl == 0 && s->qtail - s->qhead > 0){ - lit p = s->trail[s->qhead++]; - vec* ws = solver_read_wlist(s,p); - clause **begin = (clause**)vec_begin(ws); - clause **end = begin + vec_size(ws); - clause **i, **j; - - s->solver_stats.propagations++; - s->simpdb_props--; - - //printf("checking lit %d: "L_LIT"\n", vec_size(ws), L_lit(p)); - for (i = j = begin; i < end; ){ - if (clause_is_lit(*i)){ - *j++ = *i; - if (!enqueue(s,clause_read_lit(*i),clause_from_lit(p))){ - confl = s->binary; - (clause_begin(confl))[1] = neg(p); - (clause_begin(confl))[0] = clause_read_lit(*i++); - - // Copy the remaining watches: - while (i < end) - *j++ = *i++; - } - }else{ - lit false_lit; - lbool sig; - - lits = clause_begin(*i); - - // Make sure the false literal is data[1]: - false_lit = neg(p); - if (lits[0] == false_lit){ - lits[0] = lits[1]; - lits[1] = false_lit; - } - assert(lits[1] == false_lit); - //printf("checking clause: "); printlits(lits, lits+clause_size(*i)); printf("\n"); - - // If 0th watch is true, then clause is already satisfied. - sig = !lit_sign(lits[0]); sig += sig - 1; - if (values[lit_var(lits[0])] == sig){ - *j++ = *i; - }else{ - // Look for new watch: - lit* stop = lits + clause_size(*i); - lit* k; - for (k = lits + 2; k < stop; k++){ - lbool sig = lit_sign(*k); sig += sig - 1; - if (values[lit_var(*k)] != sig){ - lits[1] = *k; - *k = false_lit; - vec_push(solver_read_wlist(s,neg(lits[1])),*i); - goto next; } - } - - *j++ = *i; - // Clause is unit under assignment: - if (!enqueue(s,lits[0], *i)){ - confl = *i++; - // Copy the remaining watches: - while (i < end) - *j++ = *i++; - } - } - } - next: - i++; - } - - s->solver_stats.inspects += j - (clause**)vec_begin(ws); - vec_resize(ws,j - (clause**)vec_begin(ws)); - } - - return confl; -} - -static inline int clause_cmp (const void* x, const void* y) { - return clause_size((clause*)x) > 2 && (clause_size((clause*)y) == 2 || clause_activity((clause*)x) < clause_activity((clause*)y)) ? -1 : 1; } - -void solver_reducedb(solver* s) -{ - int i, j; - double extra_lim = s->cla_inc / vec_size(&s->learnts); // Remove any clause below this activity - clause** learnts = (clause**)vec_begin(&s->learnts); - clause** reasons = s->reasons; - - sort(vec_begin(&s->learnts), vec_size(&s->learnts), &clause_cmp); - - for (i = j = 0; i < vec_size(&s->learnts) / 2; i++){ - if (clause_size(learnts[i]) > 2 && reasons[lit_var(*clause_begin(learnts[i]))] != learnts[i]) - clause_remove(s,learnts[i]); - else - learnts[j++] = learnts[i]; - } - for (; i < vec_size(&s->learnts); i++){ - if (clause_size(learnts[i]) > 2 && reasons[lit_var(*clause_begin(learnts[i]))] != learnts[i] && clause_activity(learnts[i]) < extra_lim) - clause_remove(s,learnts[i]); - else - learnts[j++] = learnts[i]; - } - - //printf("reducedb deleted %d\n", vec_size(&s->learnts) - j); - - - vec_resize(&s->learnts,j); -} - -static lbool solver_search(solver* s, int nof_conflicts, int nof_learnts) -{ - int* levels = s->levels; - double var_decay = 0.95; - double clause_decay = 0.999; - double random_var_freq = 0.0;//0.02; - - int conflictC = 0; - veci learnt_clause; - int i; - - assert(s->root_level == solver_dlevel(s)); - - s->solver_stats.starts++; - s->var_decay = (float)(1 / var_decay ); - s->cla_decay = (float)(1 / clause_decay); - veci_resize(&s->model,0); - veci_new(&learnt_clause); - - // reset the activities - if ( s->factors ) - { - s->var_inc = 1.0; - for ( i = 0; i < s->size; i++ ) - { - s->activity[i] = (double)s->factors[i]; -// if ( s->orderpos[i] != -1 ) -// order_update(s, i ); - } -// s->activity[i] = 1.0; - } - - for (;;){ - clause* confl = solver_propagate(s); - if (confl != 0){ - // CONFLICT - int blevel; - -#ifdef VERBOSEDEBUG - printf(L_IND"**CONFLICT**\n", L_ind); -#endif - s->solver_stats.conflicts++; conflictC++; - if (solver_dlevel(s) == s->root_level){ - veci_delete(&learnt_clause); - return l_False; - } - - veci_resize(&learnt_clause,0); - solver_analyze(s, confl, &learnt_clause); - blevel = veci_size(&learnt_clause) > 1 ? levels[lit_var(veci_begin(&learnt_clause)[1])] : s->root_level; - solver_canceluntil(s,blevel); - solver_record(s,&learnt_clause); - act_var_decay(s); - act_clause_decay(s); - - }else{ - // NO CONFLICT - int next; - - if (nof_conflicts >= 0 && conflictC >= nof_conflicts) - { - // Reached bound on number of conflicts: - s->progress_estimate = solver_progress(s); - solver_canceluntil(s,s->root_level); - veci_delete(&learnt_clause); - return l_Undef; - } - - if ( s->nConfLimit && s->solver_stats.conflicts > s->nConfLimit || - s->nInsLimit && s->solver_stats.inspects > s->nInsLimit ) - { - // Reached bound on number of conflicts: - s->progress_estimate = solver_progress(s); - solver_canceluntil(s,s->root_level); - veci_delete(&learnt_clause); - return l_Undef; - } - - if (solver_dlevel(s) == 0) - // Simplify the set of problem clauses: - solver_simplify(s); - - if (nof_learnts >= 0 && vec_size(&s->learnts) - s->qtail >= nof_learnts) - // Reduce the set of learnt clauses: - solver_reducedb(s); - - // New variable decision: - s->solver_stats.decisions++; - if ( s->pJMan ) - next = Asat_JManSelect( s->pJMan ); - else - next = order_select(s,(float)random_var_freq); - - if (next == var_Undef){ - // Model found: - lbool* values = s->assigns; - int i; - for (i = 0; i < s->size; i++) veci_push(&s->model,(int)values[i]); - solver_canceluntil(s,s->root_level); - veci_delete(&learnt_clause); - return l_True; - } - - assume(s,neg(toLit(next))); - } - } - - return l_Undef; // cannot happen -} - -//================================================================================================= -// External solver functions: - -solver* solver_new(void) -{ - solver* s = (solver*)malloc(sizeof(solver)); - memset( s, 0, sizeof(solver) ); - - // initialize vectors - vec_new(&s->clauses); - vec_new(&s->learnts); - veci_new(&s->order); - veci_new(&s->trail_lim); - veci_new(&s->tagged); - veci_new(&s->stack); - veci_new(&s->model); - - // initialize arrays - s->wlists = 0; - s->activity = 0; - s->factors = 0; - s->assigns = 0; - s->orderpos = 0; - s->reasons = 0; - s->levels = 0; - s->tags = 0; - s->trail = 0; - - - // initialize other vars - s->size = 0; - s->cap = 0; - s->qhead = 0; - s->qtail = 0; - s->cla_inc = 1; - s->cla_decay = 1; - s->var_inc = 1; - s->var_decay = 1; - s->root_level = 0; - s->simpdb_assigns = 0; - s->simpdb_props = 0; - s->random_seed = 91648253; - s->progress_estimate = 0; - s->binary = (clause*)malloc(sizeof(clause) + sizeof(lit)*2); - s->binary->size_learnt = (2 << 1); - s->verbosity = 0; - - s->solver_stats.starts = 0; - s->solver_stats.decisions = 0; - s->solver_stats.propagations = 0; - s->solver_stats.inspects = 0; - s->solver_stats.conflicts = 0; - s->solver_stats.clauses = 0; - s->solver_stats.clauses_literals = 0; - s->solver_stats.learnts = 0; - s->solver_stats.learnts_literals = 0; - s->solver_stats.max_literals = 0; - s->solver_stats.tot_literals = 0; - -#ifdef ASAT_USE_SYSTEM_MEMORY_MANAGEMENT - s->pMem = NULL; -#else - s->pMem = Asat_MmStepStart( 10 ); -#endif - s->pJMan = NULL; - s->pPrefVars = NULL; - s->nPrefVars = 0; - s->timeTotal = clock(); - s->timeSelect = 0; - s->timeUpdate = 0; - return s; -} - - -void solver_delete(solver* s) -{ - -#ifdef ASAT_USE_SYSTEM_MEMORY_MANAGEMENT - int i; - for (i = 0; i < vec_size(&s->clauses); i++) - free(vec_begin(&s->clauses)[i]); - for (i = 0; i < vec_size(&s->learnts); i++) - free(vec_begin(&s->learnts)[i]); -#else - Asat_MmStepStop( s->pMem, 0 ); -#endif - - // delete vectors - vec_delete(&s->clauses); - vec_delete(&s->learnts); - veci_delete(&s->order); - veci_delete(&s->trail_lim); - veci_delete(&s->tagged); - veci_delete(&s->stack); - veci_delete(&s->model); - free(s->binary); - - // delete arrays - if (s->wlists != 0){ - int i; - for (i = 0; i < s->size*2; i++) - vec_delete(&s->wlists[i]); - - // if one is different from null, all are - free(s->wlists); - free(s->activity ); - free(s->assigns ); - free(s->orderpos ); - free(s->reasons ); - free(s->levels ); - free(s->trail ); - free(s->tags ); - } - if ( s->pJMan ) Asat_JManStop( s ); - if ( s->pPrefVars ) free( s->pPrefVars ); - if ( s->factors ) free( s->factors ); - free(s); -} - - -bool solver_addclause(solver* s, lit* begin, lit* end) -{ - lit *i,*j; - int maxvar; - lbool* values; - lit last; - - if (begin == end) return 0; - - //printlits(begin,end); printf("\n"); - // insertion sort - maxvar = lit_var(*begin); - for (i = begin + 1; i < end; i++){ - lit l = *i; - maxvar = lit_var(l) > maxvar ? lit_var(l) : maxvar; - for (j = i; j > begin && *(j-1) > l; j--) - *j = *(j-1); - *j = l; - } - solver_setnvars(s,maxvar+1); - - //printlits(begin,end); printf("\n"); - values = s->assigns; - - // delete duplicates - last = lit_Undef; - for (i = j = begin; i < end; i++){ - //printf("lit: "L_LIT", value = %d\n", L_lit(*i), (lit_sign(*i) ? -values[lit_var(*i)] : values[lit_var(*i)])); - lbool sig = !lit_sign(*i); sig += sig - 1; - if (*i == neg(last) || sig == values[lit_var(*i)]) - return 1; // tautology - else if (*i != last && values[lit_var(*i)] == l_Undef) - last = *j++ = *i; - } - - //printf("final: "); printlits(begin,j); printf("\n"); - - if (j == begin) // empty clause - return 0; - -Sat_SolverTraceWrite( s, begin, end, 1 ); - - if (j - begin == 1) // unit clause - return enqueue(s,*begin,(clause*)0); - - // create new clause - vec_push(&s->clauses,clause_new(s,begin,j,0)); - - - s->solver_stats.clauses++; - s->solver_stats.clauses_literals += j - begin; - - return 1; -} - - -bool solver_simplify(solver* s) -{ - clause** reasons; - int type; - - assert(solver_dlevel(s) == 0); - - if (solver_propagate(s) != 0) - return 0; - - if (s->qhead == s->simpdb_assigns || s->simpdb_props > 0) - return 1; - - reasons = s->reasons; - for (type = 0; type < 2; type++){ - vec* cs = type ? &s->learnts : &s->clauses; - clause** cls = (clause**)vec_begin(cs); - - int i, j; - for (j = i = 0; i < vec_size(cs); i++){ - if (reasons[lit_var(*clause_begin(cls[i]))] != cls[i] && - clause_simplify(s,cls[i]) == l_True) - clause_remove(s,cls[i]); - else - cls[j++] = cls[i]; - } - vec_resize(cs,j); - } - - s->simpdb_assigns = s->qhead; - // (shouldn't depend on 'stats' really, but it will do for now) - s->simpdb_props = (int)(s->solver_stats.clauses_literals + s->solver_stats.learnts_literals); - - return 1; -} - - -bool solver_solve(solver* s, lit* begin, lit* end, sint64 nConfLimit, sint64 nInsLimit ) -{ - double nof_conflicts = 100; -// double nof_conflicts = 1000000; - double nof_learnts = solver_nclauses(s) / 3; - lbool status = l_Undef; - lbool* values = s->assigns; - lit* i; - - // set the external limits - s->nConfLimit = nConfLimit; // external limit on the number of conflicts - s->nInsLimit = nInsLimit; // external limit on the number of implications - - - for (i = begin; i < end; i++) - if ((lit_sign(*i) ? -values[lit_var(*i)] : values[lit_var(*i)]) == l_False || (assume(s,*i), solver_propagate(s) != 0)){ - solver_canceluntil(s,0); - return l_False; } - - s->root_level = solver_dlevel(s); - - if (s->verbosity >= 1){ - printf("==================================[MINISAT]===================================\n"); - printf("| Conflicts | ORIGINAL | LEARNT | Progress |\n"); - printf("| | Clauses Literals | Limit Clauses Literals Lit/Cl | |\n"); - printf("==============================================================================\n"); - } - - while (status == l_Undef){ - double Ratio = (s->solver_stats.learnts == 0)? 0.0 : - s->solver_stats.learnts_literals / (double)s->solver_stats.learnts; - - if (s->verbosity >= 1){ - printf("| %9.0f | %7.0f %8.0f | %7.0f %7.0f %8.0f %7.1f | %6.3f %% |\n", - (double)s->solver_stats.conflicts, - (double)s->solver_stats.clauses, - (double)s->solver_stats.clauses_literals, - (double)nof_learnts, - (double)s->solver_stats.learnts, - (double)s->solver_stats.learnts_literals, - Ratio, - s->progress_estimate*100); - fflush(stdout); - } - s->nPrefDecNum = 0; - status = solver_search(s,(int)nof_conflicts, (int)nof_learnts); - nof_conflicts *= 1.5; - nof_learnts *= 1.1; - - // quit the loop if reached an external limit - if ( s->nConfLimit && s->solver_stats.conflicts > s->nConfLimit ) - { -// printf( "Reached the limit on the number of conflicts (%d).\n", s->nConfLimit ); - break; - } - if ( s->nInsLimit && s->solver_stats.inspects > s->nInsLimit ) - { -// printf( "Reached the limit on the number of implications (%d).\n", s->nInsLimit ); - break; - } - } - if (s->verbosity >= 1) - printf("==============================================================================\n"); - - solver_canceluntil(s,0); - s->timeTotal = clock() - s->timeTotal; - return status; -} - - -int solver_nvars(solver* s) -{ - return s->size; -} - - -int solver_nclauses(solver* s) -{ - return vec_size(&s->clauses); -} - -//================================================================================================= -// Sorting functions (sigh): - -static inline void selectionsort(void** array, int size, int(*comp)(const void *, const void *)) -{ - int i, j, best_i; - void* tmp; - - for (i = 0; i < size-1; i++){ - best_i = i; - for (j = i+1; j < size; j++){ - if (comp(array[j], array[best_i]) < 0) - best_i = j; - } - tmp = array[i]; array[i] = array[best_i]; array[best_i] = tmp; - } -} - - -static void sortrnd(void** array, int size, int(*comp)(const void *, const void *), double* seed) -{ - if (size <= 15) - selectionsort(array, size, comp); - - else{ - void* pivot = array[irand(seed, size)]; - void* tmp; - int i = -1; - int j = size; - - for(;;){ - do i++; while(comp(array[i], pivot)<0); - do j--; while(comp(pivot, array[j])<0); - - if (i >= j) break; - - tmp = array[i]; array[i] = array[j]; array[j] = tmp; - } - - sortrnd(array , i , comp, seed); - sortrnd(&array[i], size-i, comp, seed); - } -} - -void sort(void** array, int size, int(*comp)(const void *, const void *)) -{ - double seed = 91648253; - sortrnd(array,size,comp,&seed); -} diff --git a/src/sat/asat/solver.h b/src/sat/asat/solver.h deleted file mode 100644 index 83066f41..00000000 --- a/src/sat/asat/solver.h +++ /dev/null @@ -1,189 +0,0 @@ -/************************************************************************************************** -MiniSat -- Copyright (c) 2005, Niklas Sorensson -http://www.cs.chalmers.se/Cs/Research/FormalMethods/MiniSat/ - -Permission is hereby granted, free of charge, to any person obtaining a copy of this software and -associated documentation files (the "Software"), to deal in the Software without restriction, -including without limitation the rights to use, copy, modify, merge, publish, distribute, -sublicense, and/or sell copies of the Software, and to permit persons to whom the Software is -furnished to do so, subject to the following conditions: - -The above copyright notice and this permission notice shall be included in all copies or -substantial portions of the Software. - -THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR IMPLIED, INCLUDING BUT -NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND -NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, -DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT -OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE. -**************************************************************************************************/ -// Modified to compile with MS Visual Studio 6.0 by Alan Mishchenko - -#ifndef solver_h -#define solver_h - -#ifdef __cplusplus -extern "C" { -#endif - -#ifdef _WIN32 -#define inline __inline // compatible with MS VS 6.0 -#endif - -#include "solver_vec.h" -#include "asatmem.h" - -//================================================================================================= -// Simple types: - -//typedef int bool; -#ifndef __cplusplus -#ifndef bool -#define bool int -#endif -#endif - -typedef int lit; -typedef char lbool; - -#ifdef _WIN32 -typedef signed __int64 sint64; // compatible with MS VS 6.0 -#else -typedef long long sint64; -#endif - -static const int var_Undef = -1; -static const lit lit_Undef = -2; - -static const lbool l_Undef = 0; -static const lbool l_True = 1; -static const lbool l_False = -1; - -static inline lit neg (lit l) { return l ^ 1; } -static inline lit toLit (int v) { return v + v; } -static inline lit toLitCond (int v, int c) { return v + v + (int)(c != 0); } - -//================================================================================================= -// Public interface: - -typedef struct Asat_JMan_t_ Asat_JMan_t; - -struct solver_t; -typedef struct solver_t solver; - -extern solver* solver_new(void); -extern void solver_delete(solver* s); - -extern bool solver_addclause(solver* s, lit* begin, lit* end); -extern bool solver_simplify(solver* s); -extern int solver_solve(solver* s, lit* begin, lit* end, sint64 nConfLimit, sint64 nInsLimit); -extern int * solver_get_model( solver * p, int * pVars, int nVars ); - -extern int solver_nvars(solver* s); -extern int solver_nclauses(solver* s); - - -// additional procedures -extern void Asat_SolverWriteDimacs( solver * pSat, char * pFileName, - lit* assumptionsBegin, lit* assumptionsEnd, - int incrementVars); -extern void Asat_SatPrintStats( FILE * pFile, solver * p ); -extern void Asat_SolverSetPrefVars( solver * s, int * pPrefVars, int nPrefVars ); -extern void Asat_SolverSetFactors( solver * s, float * pFactors ); - -// trace recording -extern void Sat_SolverTraceStart( solver * pSat, char * pName ); -extern void Sat_SolverTraceStop( solver * pSat ); -extern void Sat_SolverTraceWrite( solver * pSat, int * pBeg, int * pEnd, int fRoot ); - -// J-frontier support -extern Asat_JMan_t * Asat_JManStart( solver * pSat, void * vCircuit ); -extern void Asat_JManStop( solver * pSat ); - - -struct stats_t -{ - sint64 starts, decisions, propagations, inspects, conflicts; - sint64 clauses, clauses_literals, learnts, learnts_literals, max_literals, tot_literals; -}; -typedef struct stats_t stats; - -//================================================================================================= -// Solver representation: - -struct clause_t; -typedef struct clause_t clause; - -struct solver_t -{ - int size; // nof variables - int cap; // size of varmaps - int qhead; // Head index of queue. - int qtail; // Tail index of queue. - - // clauses - vec clauses; // List of problem constraints. (contains: clause*) - vec learnts; // List of learnt clauses. (contains: clause*) - - // activities - double var_inc; // Amount to bump next variable with. - double var_decay; // INVERSE decay factor for variable activity: stores 1/decay. - float cla_inc; // Amount to bump next clause with. - float cla_decay; // INVERSE decay factor for clause activity: stores 1/decay. - - vec* wlists; // - double* activity; // A heuristic measurement of the activity of a variable. - float * factors; // the factor of variable activity - lbool* assigns; // Current values of variables. - int* orderpos; // Index in variable order. - clause** reasons; // - int* levels; // - lit* trail; - - clause* binary; // A temporary binary clause - lbool* tags; // - veci tagged; // (contains: var) - veci stack; // (contains: var) - - veci order; // Variable order. (heap) (contains: var) - veci trail_lim; // Separator indices for different decision levels in 'trail'. (contains: int) - veci model; // If problem is solved, this vector contains the model (contains: lbool). - - int root_level; // Level of first proper decision. - int simpdb_assigns;// Number of top-level assignments at last 'simplifyDB()'. - int simpdb_props; // Number of propagations before next 'simplifyDB()'. - double random_seed; - double progress_estimate; - int verbosity; // Verbosity level. 0=silent, 1=some progress report, 2=everything - - sint64 nConfLimit; // external limit on the number of conflicts - sint64 nInsLimit; // external limit on the number of implications - - // the memory manager - Asat_MmStep_t * pMem; - - // J-frontier - Asat_JMan_t * pJMan; - - // for making decisions on some variables first - int nPrefDecNum; - int * pPrefVars; - int nPrefVars; - - // solver statistics - stats solver_stats; - int timeTotal; - int timeSelect; - int timeUpdate; - - // trace recording - FILE * pFile; - int nClauses; - int nRoots; -}; - -#ifdef __cplusplus -} -#endif - -#endif diff --git a/src/sat/asat/solver_vec.h b/src/sat/asat/solver_vec.h deleted file mode 100644 index 1ae30b0a..00000000 --- a/src/sat/asat/solver_vec.h +++ /dev/null @@ -1,83 +0,0 @@ -/************************************************************************************************** -MiniSat -- Copyright (c) 2005, Niklas Sorensson -http://www.cs.chalmers.se/Cs/Research/FormalMethods/MiniSat/ - -Permission is hereby granted, free of charge, to any person obtaining a copy of this software and -associated documentation files (the "Software"), to deal in the Software without restriction, -including without limitation the rights to use, copy, modify, merge, publish, distribute, -sublicense, and/or sell copies of the Software, and to permit persons to whom the Software is -furnished to do so, subject to the following conditions: - -The above copyright notice and this permission notice shall be included in all copies or -substantial portions of the Software. - -THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR IMPLIED, INCLUDING BUT -NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND -NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, -DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT -OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE. -**************************************************************************************************/ -// Modified to compile with MS Visual Studio 6.0 by Alan Mishchenko - -#ifndef vec_h -#define vec_h - -#include <stdlib.h> - -// vector of 32-bit intergers (added for 64-bit portability) -struct veci_t { - int size; - int cap; - int* ptr; -}; -typedef struct veci_t veci; - -static inline void veci_new (veci* v) { - v->size = 0; - v->cap = 4; - v->ptr = (int*)malloc(sizeof(int)*v->cap); -} - -static inline void veci_delete (veci* v) { free(v->ptr); } -static inline int* veci_begin (veci* v) { return v->ptr; } -static inline int veci_size (veci* v) { return v->size; } -static inline void veci_resize (veci* v, int k) { v->size = k; } // only safe to shrink !! -static inline void veci_push (veci* v, int e) -{ - if (v->size == v->cap) { - int newsize = v->cap * 2+1; - v->ptr = (int*)realloc(v->ptr,sizeof(int)*newsize); - v->cap = newsize; } - v->ptr[v->size++] = e; -} - - -// vector of 32- or 64-bit pointers -struct vec_t { - int size; - int cap; - void** ptr; -}; -typedef struct vec_t vec; - -static inline void vec_new (vec* v) { - v->size = 0; - v->cap = 4; - v->ptr = (void**)malloc(sizeof(void*)*v->cap); -} - -static inline void vec_delete (vec* v) { free(v->ptr); } -static inline void** vec_begin (vec* v) { return v->ptr; } -static inline int vec_size (vec* v) { return v->size; } -static inline void vec_resize (vec* v, int k) { v->size = k; } // only safe to shrink !! -static inline void vec_push (vec* v, void* e) -{ - if (v->size == v->cap) { - int newsize = v->cap * 2+1; - v->ptr = (void**)realloc(v->ptr,sizeof(void*)*newsize); - v->cap = newsize; } - v->ptr[v->size++] = e; -} - - -#endif diff --git a/src/sat/bsat/satInter.c b/src/sat/bsat/satInter.c new file mode 100644 index 00000000..e22b309c --- /dev/null +++ b/src/sat/bsat/satInter.c @@ -0,0 +1,980 @@ +/**CFile**************************************************************** + + FileName [satInter.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [SAT sat_solver.] + + Synopsis [Interpolation package.] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - June 20, 2005.] + + Revision [$Id: satInter.c,v 1.4 2005/09/16 22:55:03 casem Exp $] + +***********************************************************************/ + +#include <stdio.h> +#include <stdlib.h> +#include <string.h> +#include <assert.h> +#include <time.h> +#include "satStore.h" + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +// variable assignments +static const lit LIT_UNDEF = 0xffffffff; + +// interpolation manager +struct Int_Man_t_ +{ + // clauses of the problems + Sto_Man_t * pCnf; // the set of CNF clauses for A and B + // various parameters + int fVerbose; // verbosiness flag + int fProofVerif; // verifies the proof + int fProofWrite; // writes the proof file + int nVarsAlloc; // the allocated size of var arrays + int nClosAlloc; // the allocated size of clause arrays + // internal BCP + int nRootSize; // the number of root level assignments + int nTrailSize; // the number of assignments made + lit * pTrail; // chronological order of assignments (size nVars) + lit * pAssigns; // assignments by variable (size nVars) + char * pSeens; // temporary mark (size nVars) + Sto_Cls_t ** pReasons; // reasons for each assignment (size nVars) + Sto_Cls_t ** pWatches; // watched clauses for each literal (size 2*nVars) + // interpolation data + int nVarsAB; // the number of global variables + char * pVarTypes; // variable type (size nVars) [1=A, 0=B, <0=AB] + unsigned * pInters; // storage for interpolants as truth tables (size nClauses) + int nIntersAlloc; // the allocated size of truth table array + int nWords; // the number of words in the truth table + // proof recording + int Counter; // counter of resolved clauses + int * pProofNums; // the proof numbers for each clause (size nClauses) + FILE * pFile; // the file for proof recording + // internal verification + lit * pResLits; // the literals of the resolvent + int nResLits; // the number of literals of the resolvent + int nResLitsAlloc;// the number of literals of the resolvent + // runtime stats + int timeBcp; // the runtime for BCP + int timeTrace; // the runtime of trace construction + int timeTotal; // the total runtime of interpolation +}; + +// procedure to get hold of the clauses' truth table +static inline unsigned * Int_ManTruthRead( Int_Man_t * p, Sto_Cls_t * pCls ) { return p->pInters + pCls->Id * p->nWords; } +static inline void Int_ManTruthClear( unsigned * p, int nWords ) { int i; for ( i = nWords - 1; i >= 0; i-- ) p[i] = 0; } +static inline void Int_ManTruthFill( unsigned * p, int nWords ) { int i; for ( i = nWords - 1; i >= 0; i-- ) p[i] = ~0; } +static inline void Int_ManTruthCopy( unsigned * p, unsigned * q, int nWords ) { int i; for ( i = nWords - 1; i >= 0; i-- ) p[i] = q[i]; } +static inline void Int_ManTruthAnd( unsigned * p, unsigned * q, int nWords ) { int i; for ( i = nWords - 1; i >= 0; i-- ) p[i] &= q[i]; } +static inline void Int_ManTruthOr( unsigned * p, unsigned * q, int nWords ) { int i; for ( i = nWords - 1; i >= 0; i-- ) p[i] |= q[i]; } +static inline void Int_ManTruthOrNot( unsigned * p, unsigned * q, int nWords ) { int i; for ( i = nWords - 1; i >= 0; i-- ) p[i] |= ~q[i]; } + +// reading/writing the proof for a clause +static inline int Int_ManProofRead( Int_Man_t * p, Sto_Cls_t * pCls ) { return p->pProofNums[pCls->Id]; } +static inline void Int_ManProofWrite( Int_Man_t * p, Sto_Cls_t * pCls, int n ) { p->pProofNums[pCls->Id] = n; } + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [Allocate proof manager.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Int_Man_t * Int_ManAlloc( int nVarsAlloc ) +{ + Int_Man_t * p; + // allocate the manager + p = (Int_Man_t *)malloc( sizeof(Int_Man_t) ); + memset( p, 0, sizeof(Int_Man_t) ); + // verification + p->nResLitsAlloc = (1<<16); + p->pResLits = malloc( sizeof(lit) * p->nResLitsAlloc ); + // parameters + p->fProofWrite = 0; + p->fProofVerif = 0; + return p; +} + +/**Function************************************************************* + + Synopsis [Count common variables in the clauses of A and B.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Int_ManCommonVars( Int_Man_t * p ) +{ + Sto_Cls_t * pClause; + int Var, nVarsAB, v; + + // mark the variable encountered in the clauses of A + Sto_ManForEachClauseRoot( p->pCnf, pClause ) + { + if ( !pClause->fA ) + break; + for ( v = 0; v < (int)pClause->nLits; v++ ) + p->pVarTypes[lit_var(pClause->pLits[v])] = 1; + } + + // check variables that appear in clauses of B + nVarsAB = 0; + Sto_ManForEachClauseRoot( p->pCnf, pClause ) + { + if ( pClause->fA ) + continue; + for ( v = 0; v < (int)pClause->nLits; v++ ) + { + Var = lit_var(pClause->pLits[v]); + if ( p->pVarTypes[Var] == 1 ) // var of A + { + // change it into a global variable + nVarsAB++; + p->pVarTypes[Var] = -1; + } + } + } + + // order global variables + nVarsAB = 0; + for ( v = 0; v < p->pCnf->nVars; v++ ) + if ( p->pVarTypes[v] == -1 ) + p->pVarTypes[v] -= p->nVarsAB++; +printf( "There are %d global variables.\n", nVarsAB ); + return nVarsAB; +} + +/**Function************************************************************* + + Synopsis [Resize proof manager.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Int_ManResize( Int_Man_t * p ) +{ + // check if resizing is needed + if ( p->nVarsAlloc < p->pCnf->nVars ) + { + int nVarsAllocOld = p->nVarsAlloc; + // find the new size + if ( p->nVarsAlloc == 0 ) + p->nVarsAlloc = 1; + while ( p->nVarsAlloc < p->pCnf->nVars ) + p->nVarsAlloc *= 2; + // resize the arrays + p->pTrail = (lit *) realloc( p->pTrail, sizeof(lit) * p->nVarsAlloc ); + p->pAssigns = (lit *) realloc( p->pAssigns, sizeof(lit) * p->nVarsAlloc ); + p->pSeens = (char *) realloc( p->pSeens, sizeof(char) * p->nVarsAlloc ); + p->pVarTypes = (char *) realloc( p->pVarTypes, sizeof(char) * p->nVarsAlloc ); + p->pReasons = (Sto_Cls_t **)realloc( p->pReasons, sizeof(Sto_Cls_t *) * p->nVarsAlloc ); + p->pWatches = (Sto_Cls_t **)realloc( p->pWatches, sizeof(Sto_Cls_t *) * p->nVarsAlloc*2 ); + } + + // clean the free space + memset( p->pAssigns , 0xff, sizeof(lit) * p->pCnf->nVars ); + memset( p->pSeens , 0, sizeof(char) * p->pCnf->nVars ); + memset( p->pVarTypes, 0, sizeof(char) * p->pCnf->nVars ); + memset( p->pReasons , 0, sizeof(Sto_Cls_t *) * p->pCnf->nVars ); + memset( p->pWatches , 0, sizeof(Sto_Cls_t *) * p->pCnf->nVars*2 ); + + // compute the number of common variables + p->nVarsAB = Int_ManCommonVars( p ); + // compute the number of words in the truth table + p->nWords = (p->nVarsAB <= 5 ? 1 : (1 << (p->nVarsAB - 5))); + + // check if resizing of clauses is needed + if ( p->nClosAlloc < p->pCnf->nClauses ) + { + // find the new size + if ( p->nClosAlloc == 0 ) + p->nClosAlloc = 1; + while ( p->nClosAlloc < p->pCnf->nClauses ) + p->nClosAlloc *= 2; + // resize the arrays + p->pProofNums = (int *) realloc( p->pProofNums, sizeof(int) * p->nClosAlloc ); + } + memset( p->pProofNums, 0, sizeof(int) * p->pCnf->nClauses ); + + // check if resizing of truth tables is needed + if ( p->nIntersAlloc < p->nWords * p->pCnf->nClauses ) + { + p->nIntersAlloc = p->nWords * p->pCnf->nClauses; + p->pInters = (unsigned *) realloc( p->pInters, sizeof(unsigned) * p->nIntersAlloc ); + } + memset( p->pInters, 0, sizeof(unsigned) * p->nIntersAlloc ); +} + +/**Function************************************************************* + + Synopsis [Deallocate proof manager.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Int_ManFree( Int_Man_t * p ) +{ + printf( "Runtime stats:\n" ); +PRT( "BCP ", p->timeBcp ); +PRT( "Trace ", p->timeTrace ); +PRT( "TOTAL ", p->timeTotal ); + + free( p->pInters ); + free( p->pProofNums ); + free( p->pTrail ); + free( p->pAssigns ); + free( p->pSeens ); + free( p->pVarTypes ); + free( p->pReasons ); + free( p->pWatches ); + free( p->pResLits ); + free( p ); +} + + + + +/**Function************************************************************* + + Synopsis [Prints the clause.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Int_ManPrintClause( Int_Man_t * p, Sto_Cls_t * pClause ) +{ + int i; + printf( "Clause ID = %d. Proof = %d. {", pClause->Id, Int_ManProofRead(p, pClause) ); + for ( i = 0; i < (int)pClause->nLits; i++ ) + printf( " %d", pClause->pLits[i] ); + printf( " }\n" ); +} + +/**Function************************************************************* + + Synopsis [Prints the resolvent.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Int_ManPrintResolvent( lit * pResLits, int nResLits ) +{ + int i; + printf( "Resolvent: {" ); + for ( i = 0; i < nResLits; i++ ) + printf( " %d", pResLits[i] ); + printf( " }\n" ); +} + +/**Function************************************************************* + + Synopsis [Records the proof.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Extra_PrintBinary__( FILE * pFile, unsigned Sign[], int nBits ) +{ + int Remainder, nWords; + int w, i; + + Remainder = (nBits%(sizeof(unsigned)*8)); + nWords = (nBits/(sizeof(unsigned)*8)) + (Remainder>0); + + for ( w = nWords-1; w >= 0; w-- ) + for ( i = ((w == nWords-1 && Remainder)? Remainder-1: 31); i >= 0; i-- ) + fprintf( pFile, "%c", '0' + (int)((Sign[w] & (1<<i)) > 0) ); +} + +/**Function************************************************************* + + Synopsis [Prints the interpolant for one clause.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Int_ManPrintInterOne( Int_Man_t * p, Sto_Cls_t * pClause ) +{ + printf( "Clause %2d : ", pClause->Id ); + Extra_PrintBinary__( stdout, Int_ManTruthRead(p, pClause), (1 << p->nVarsAB) ); + printf( "\n" ); +} + + + +/**Function************************************************************* + + Synopsis [Adds one clause to the watcher list.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline void Int_ManWatchClause( Int_Man_t * p, Sto_Cls_t * pClause, lit Lit ) +{ + assert( lit_check(Lit, p->pCnf->nVars) ); + if ( pClause->pLits[0] == Lit ) + pClause->pNext0 = p->pWatches[lit_neg(Lit)]; + else + { + assert( pClause->pLits[1] == Lit ); + pClause->pNext1 = p->pWatches[lit_neg(Lit)]; + } + p->pWatches[lit_neg(Lit)] = pClause; +} + + +/**Function************************************************************* + + Synopsis [Records implication.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline int Int_ManEnqueue( Int_Man_t * p, lit Lit, Sto_Cls_t * pReason ) +{ + int Var = lit_var(Lit); + if ( p->pAssigns[Var] != LIT_UNDEF ) + return p->pAssigns[Var] == Lit; + p->pAssigns[Var] = Lit; + p->pReasons[Var] = pReason; + p->pTrail[p->nTrailSize++] = Lit; +//printf( "assigning var %d value %d\n", Var, !lit_sign(Lit) ); + return 1; +} + +/**Function************************************************************* + + Synopsis [Records implication.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline void Int_ManCancelUntil( Int_Man_t * p, int Level ) +{ + lit Lit; + int i, Var; + for ( i = p->nTrailSize - 1; i >= Level; i-- ) + { + Lit = p->pTrail[i]; + Var = lit_var( Lit ); + p->pReasons[Var] = NULL; + p->pAssigns[Var] = LIT_UNDEF; +//printf( "cancelling var %d\n", Var ); + } + p->nTrailSize = Level; +} + +/**Function************************************************************* + + Synopsis [Propagate one assignment.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline Sto_Cls_t * Int_ManPropagateOne( Int_Man_t * p, lit Lit ) +{ + Sto_Cls_t ** ppPrev, * pCur, * pTemp; + lit LitF = lit_neg(Lit); + int i; + // iterate through the literals + ppPrev = p->pWatches + Lit; + for ( pCur = p->pWatches[Lit]; pCur; pCur = *ppPrev ) + { + // make sure the false literal is in the second literal of the clause + if ( pCur->pLits[0] == LitF ) + { + pCur->pLits[0] = pCur->pLits[1]; + pCur->pLits[1] = LitF; + pTemp = pCur->pNext0; + pCur->pNext0 = pCur->pNext1; + pCur->pNext1 = pTemp; + } + assert( pCur->pLits[1] == LitF ); + + // if the first literal is true, the clause is satisfied + if ( pCur->pLits[0] == p->pAssigns[lit_var(pCur->pLits[0])] ) + { + ppPrev = &pCur->pNext1; + continue; + } + + // look for a new literal to watch + for ( i = 2; i < (int)pCur->nLits; i++ ) + { + // skip the case when the literal is false + if ( lit_neg(pCur->pLits[i]) == p->pAssigns[lit_var(pCur->pLits[i])] ) + continue; + // the literal is either true or unassigned - watch it + pCur->pLits[1] = pCur->pLits[i]; + pCur->pLits[i] = LitF; + // remove this clause from the watch list of Lit + *ppPrev = pCur->pNext1; + // add this clause to the watch list of pCur->pLits[i] (now it is pCur->pLits[1]) + Int_ManWatchClause( p, pCur, pCur->pLits[1] ); + break; + } + if ( i < (int)pCur->nLits ) // found new watch + continue; + + // clause is unit - enqueue new implication + if ( Int_ManEnqueue(p, pCur->pLits[0], pCur) ) + { + ppPrev = &pCur->pNext1; + continue; + } + + // conflict detected - return the conflict clause + return pCur; + } + return NULL; +} + +/**Function************************************************************* + + Synopsis [Propagate the current assignments.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Sto_Cls_t * Int_ManPropagate( Int_Man_t * p, int Start ) +{ + Sto_Cls_t * pClause; + int i; + int clk = clock(); + for ( i = Start; i < p->nTrailSize; i++ ) + { + pClause = Int_ManPropagateOne( p, p->pTrail[i] ); + if ( pClause ) + { +p->timeBcp += clock() - clk; + return pClause; + } + } +p->timeBcp += clock() - clk; + return NULL; +} + + +/**Function************************************************************* + + Synopsis [Writes one root clause into a file.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Int_ManProofWriteOne( Int_Man_t * p, Sto_Cls_t * pClause ) +{ + Int_ManProofWrite( p, pClause, ++p->Counter ); + + if ( p->fProofWrite ) + { + int v; + fprintf( p->pFile, "%d", Int_ManProofRead(p, pClause) ); + for ( v = 0; v < (int)pClause->nLits; v++ ) + fprintf( p->pFile, " %d", lit_print(pClause->pLits[v]) ); + fprintf( p->pFile, " 0 0\n" ); + } +} + +/**Function************************************************************* + + Synopsis [Traces the proof for one clause.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Int_ManProofTraceOne( Int_Man_t * p, Sto_Cls_t * pConflict, Sto_Cls_t * pFinal ) +{ + Sto_Cls_t * pReason; + int i, v, Var, PrevId; + int fPrint = 0; + int clk = clock(); + + // collect resolvent literals + if ( p->fProofVerif ) + { + assert( (int)pConflict->nLits <= p->nResLitsAlloc ); + memcpy( p->pResLits, pConflict->pLits, sizeof(lit) * pConflict->nLits ); + p->nResLits = pConflict->nLits; + } + + // mark all the variables in the conflict as seen + for ( v = 0; v < (int)pConflict->nLits; v++ ) + p->pSeens[lit_var(pConflict->pLits[v])] = 1; + + // start the anticedents +// pFinal->pAntis = Vec_PtrAlloc( 32 ); +// Vec_PtrPush( pFinal->pAntis, pConflict ); + + if ( p->pCnf->nClausesA ) + Int_ManTruthCopy( Int_ManTruthRead(p, pFinal), Int_ManTruthRead(p, pConflict), p->nWords ); + + // follow the trail backwards + PrevId = Int_ManProofRead(p, pConflict); + for ( i = p->nTrailSize - 1; i >= 0; i-- ) + { + // skip literals that are not involved + Var = lit_var(p->pTrail[i]); + if ( !p->pSeens[Var] ) + continue; + p->pSeens[Var] = 0; + + // skip literals of the resulting clause + pReason = p->pReasons[Var]; + if ( pReason == NULL ) + continue; + assert( p->pTrail[i] == pReason->pLits[0] ); + + // add the variables to seen + for ( v = 1; v < (int)pReason->nLits; v++ ) + p->pSeens[lit_var(pReason->pLits[v])] = 1; + + + // record the reason clause + assert( Int_ManProofRead(p, pReason) > 0 ); + p->Counter++; + if ( p->fProofWrite ) + fprintf( p->pFile, "%d * %d %d 0\n", p->Counter, PrevId, Int_ManProofRead(p, pReason) ); + PrevId = p->Counter; + + if ( p->pCnf->nClausesA ) + { + if ( p->pVarTypes[Var] == 1 ) // var of A + Int_ManTruthOr( Int_ManTruthRead(p, pFinal), Int_ManTruthRead(p, pReason), p->nWords ); + else + Int_ManTruthAnd( Int_ManTruthRead(p, pFinal), Int_ManTruthRead(p, pReason), p->nWords ); + } + + // resolve the temporary resolvent with the reason clause + if ( p->fProofVerif ) + { + int v1, v2; + if ( fPrint ) + Int_ManPrintResolvent( p->pResLits, p->nResLits ); + // check that the var is present in the resolvent + for ( v1 = 0; v1 < p->nResLits; v1++ ) + if ( lit_var(p->pResLits[v1]) == Var ) + break; + if ( v1 == p->nResLits ) + printf( "Recording clause %d: Cannot find variable %d in the temporary resolvent.\n", pFinal->Id, Var ); + if ( p->pResLits[v1] != lit_neg(pReason->pLits[0]) ) + printf( "Recording clause %d: The resolved variable %d is in the wrong polarity.\n", pFinal->Id, Var ); + // remove this variable from the resolvent + assert( lit_var(p->pResLits[v1]) == Var ); + p->nResLits--; + for ( ; v1 < p->nResLits; v1++ ) + p->pResLits[v1] = p->pResLits[v1+1]; + // add variables of the reason clause + for ( v2 = 1; v2 < (int)pReason->nLits; v2++ ) + { + for ( v1 = 0; v1 < p->nResLits; v1++ ) + if ( lit_var(p->pResLits[v1]) == lit_var(pReason->pLits[v2]) ) + break; + // if it is a new variable, add it to the resolvent + if ( v1 == p->nResLits ) + { + if ( p->nResLits == p->nResLitsAlloc ) + printf( "Recording clause %d: Ran out of space for intermediate resolvent.\n, pFinal->Id" ); + p->pResLits[ p->nResLits++ ] = pReason->pLits[v2]; + continue; + } + // if the variable is the same, the literal should be the same too + if ( p->pResLits[v1] == pReason->pLits[v2] ) + continue; + // the literal is different + printf( "Recording clause %d: Trying to resolve the clause with more than one opposite literal.\n", pFinal->Id ); + } + } + +// Vec_PtrPush( pFinal->pAntis, pReason ); + } + + // unmark all seen variables +// for ( i = p->nTrailSize - 1; i >= 0; i-- ) +// p->pSeens[lit_var(p->pTrail[i])] = 0; + // check that the literals are unmarked +// for ( i = p->nTrailSize - 1; i >= 0; i-- ) +// assert( p->pSeens[lit_var(p->pTrail[i])] == 0 ); + + // use the resulting clause to check the correctness of resolution + if ( p->fProofVerif ) + { + int v1, v2; + if ( fPrint ) + Int_ManPrintResolvent( p->pResLits, p->nResLits ); + for ( v1 = 0; v1 < p->nResLits; v1++ ) + { + for ( v2 = 0; v2 < (int)pFinal->nLits; v2++ ) + if ( pFinal->pLits[v2] == p->pResLits[v1] ) + break; + if ( v2 < (int)pFinal->nLits ) + continue; + break; + } + if ( v1 < p->nResLits ) + { + printf( "Recording clause %d: The final resolvent is wrong.\n", pFinal->Id ); + Int_ManPrintClause( p, pConflict ); + Int_ManPrintResolvent( p->pResLits, p->nResLits ); + Int_ManPrintClause( p, pFinal ); + } + } +p->timeTrace += clock() - clk; + + // return the proof pointer + if ( p->pCnf->nClausesA ) + { +// Int_ManPrintInterOne( p, pFinal ); + } + Int_ManProofWrite( p, pFinal, p->Counter ); + return p->Counter; +} + +/**Function************************************************************* + + Synopsis [Records the proof for one clause.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Int_ManProofRecordOne( Int_Man_t * p, Sto_Cls_t * pClause ) +{ + Sto_Cls_t * pConflict; + int i; + + // empty clause never ends up there + assert( pClause->nLits > 0 ); + if ( pClause->nLits == 0 ) + printf( "Error: Empty clause is attempted.\n" ); + + // add assumptions to the trail + assert( !pClause->fRoot ); + assert( p->nTrailSize == p->nRootSize ); + for ( i = 0; i < (int)pClause->nLits; i++ ) + if ( !Int_ManEnqueue( p, lit_neg(pClause->pLits[i]), NULL ) ) + { + assert( 0 ); // impossible + return 0; + } + + // propagate the assumptions + pConflict = Int_ManPropagate( p, p->nRootSize ); + if ( pConflict == NULL ) + { + assert( 0 ); // cannot prove + return 0; + } + + // construct the proof + Int_ManProofTraceOne( p, pConflict, pClause ); + + // undo to the root level + Int_ManCancelUntil( p, p->nRootSize ); + + // add large clauses to the watched lists + if ( pClause->nLits > 1 ) + { + Int_ManWatchClause( p, pClause, pClause->pLits[0] ); + Int_ManWatchClause( p, pClause, pClause->pLits[1] ); + return 1; + } + assert( pClause->nLits == 1 ); + + // if the clause proved is unit, add it and propagate + if ( !Int_ManEnqueue( p, pClause->pLits[0], pClause ) ) + { + assert( 0 ); // impossible + return 0; + } + + // propagate the assumption + pConflict = Int_ManPropagate( p, p->nRootSize ); + if ( pConflict ) + { + // construct the proof + Int_ManProofTraceOne( p, pConflict, p->pCnf->pEmpty ); + printf( "Found last conflict after adding unit clause number %d!\n", pClause->Id ); + return 0; + } + + // update the root level + p->nRootSize = p->nTrailSize; + return 1; +} + +/**Function************************************************************* + + Synopsis [Propagate the root clauses.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Int_ManProcessRoots( Int_Man_t * p ) +{ + Sto_Cls_t * pClause; + int Counter; + + // make sure the root clauses are preceeding the learnt clauses + Counter = 0; + Sto_ManForEachClause( p->pCnf, pClause ) + { + assert( (int)pClause->fA == (Counter < (int)p->pCnf->nClausesA) ); + assert( (int)pClause->fRoot == (Counter < (int)p->pCnf->nRoots) ); + Counter++; + } + assert( p->pCnf->nClauses == Counter ); + + // make sure the last clause if empty + assert( p->pCnf->pTail->nLits == 0 ); + + // go through the root unit clauses + p->nTrailSize = 0; + Sto_ManForEachClauseRoot( p->pCnf, pClause ) + { + // create watcher lists for the root clauses + if ( pClause->nLits > 1 ) + { + Int_ManWatchClause( p, pClause, pClause->pLits[0] ); + Int_ManWatchClause( p, pClause, pClause->pLits[1] ); + } + // empty clause and large clauses + if ( pClause->nLits != 1 ) + continue; + // unit clause + assert( lit_check(pClause->pLits[0], p->pCnf->nVars) ); + if ( !Int_ManEnqueue( p, pClause->pLits[0], pClause ) ) + { + // detected root level conflict + printf( "Int_ManProcessRoots(): Detected a root-level conflict\n" ); + assert( 0 ); + return 0; + } + } + + // propagate the root unit clauses + pClause = Int_ManPropagate( p, 0 ); + if ( pClause ) + { + // detected root level conflict + printf( "Int_ManProcessRoots(): Detected a root-level conflict\n" ); + assert( 0 ); + return 0; + } + + // set the root level + p->nRootSize = p->nTrailSize; + return 1; +} + +/**Function************************************************************* + + Synopsis [Records the proof.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Int_ManPrepareInter( Int_Man_t * p ) +{ + // elementary truth tables + unsigned uTruths[8][8] = { + { 0xAAAAAAAA,0xAAAAAAAA,0xAAAAAAAA,0xAAAAAAAA,0xAAAAAAAA,0xAAAAAAAA,0xAAAAAAAA,0xAAAAAAAA }, + { 0xCCCCCCCC,0xCCCCCCCC,0xCCCCCCCC,0xCCCCCCCC,0xCCCCCCCC,0xCCCCCCCC,0xCCCCCCCC,0xCCCCCCCC }, + { 0xF0F0F0F0,0xF0F0F0F0,0xF0F0F0F0,0xF0F0F0F0,0xF0F0F0F0,0xF0F0F0F0,0xF0F0F0F0,0xF0F0F0F0 }, + { 0xFF00FF00,0xFF00FF00,0xFF00FF00,0xFF00FF00,0xFF00FF00,0xFF00FF00,0xFF00FF00,0xFF00FF00 }, + { 0xFFFF0000,0xFFFF0000,0xFFFF0000,0xFFFF0000,0xFFFF0000,0xFFFF0000,0xFFFF0000,0xFFFF0000 }, + { 0x00000000,0xFFFFFFFF,0x00000000,0xFFFFFFFF,0x00000000,0xFFFFFFFF,0x00000000,0xFFFFFFFF }, + { 0x00000000,0x00000000,0xFFFFFFFF,0xFFFFFFFF,0x00000000,0x00000000,0xFFFFFFFF,0xFFFFFFFF }, + { 0x00000000,0x00000000,0x00000000,0x00000000,0xFFFFFFFF,0xFFFFFFFF,0xFFFFFFFF,0xFFFFFFFF } + }; + Sto_Cls_t * pClause; + int Var, v; + assert( p->nVarsAB <= 8 ); + + // set interpolants for root clauses + Sto_ManForEachClauseRoot( p->pCnf, pClause ) + { + if ( !pClause->fA ) // clause of B + { + Int_ManTruthFill( Int_ManTruthRead(p, pClause), p->nWords ); +// Int_ManPrintInterOne( p, pClause ); + continue; + } + // clause of A + Int_ManTruthClear( Int_ManTruthRead(p, pClause), p->nWords ); + for ( v = 0; v < (int)pClause->nLits; v++ ) + { + Var = lit_var(pClause->pLits[v]); + if ( p->pVarTypes[Var] < 0 ) // global var + { + if ( lit_sign(pClause->pLits[v]) ) // negative var + Int_ManTruthOrNot( Int_ManTruthRead(p, pClause), uTruths[ -p->pVarTypes[Var]-1 ], p->nWords ); + else + Int_ManTruthOr( Int_ManTruthRead(p, pClause), uTruths[ -p->pVarTypes[Var]-1 ], p->nWords ); + } + } +// Int_ManPrintInterOne( p, pClause ); + } +} + +/**Function************************************************************* + + Synopsis [Computes interpolant for the given CNF.] + + Description [Returns the number of common variable found and interpolant. + Returns 0, if something did not work.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Int_ManInterpolate( Int_Man_t * p, Sto_Man_t * pCnf, int fVerbose, unsigned ** ppResult ) +{ + Sto_Cls_t * pClause; + int RetValue = 1; + int clkTotal = clock(); + + // check that the CNF makes sense + assert( pCnf->nVars > 0 && pCnf->nClauses > 0 ); + + // adjust the manager + Int_ManResize( p ); + + // propagate root level assignments + Int_ManProcessRoots( p ); + + // prepare the interpolant computation + Int_ManPrepareInter( p ); + + // construct proof for each clause + // start the proof + if ( p->fProofWrite ) + { + p->pFile = fopen( "proof.cnf_", "w" ); + p->Counter = 0; + } + + // write the root clauses + Sto_ManForEachClauseRoot( p->pCnf, pClause ) + Int_ManProofWriteOne( p, pClause ); + + // consider each learned clause + Sto_ManForEachClause( p->pCnf, pClause ) + { + if ( pClause->fRoot ) + continue; + if ( !Int_ManProofRecordOne( p, pClause ) ) + { + RetValue = 0; + break; + } + } + + // stop the proof + if ( p->fProofWrite ) + { + fclose( p->pFile ); + p->pFile = NULL; + } + + printf( "Vars = %d. Roots = %d. Learned = %d. Resol steps = %d. Ave = %.2f. Mem = %.2f Mb\n", + p->pCnf->nVars, p->pCnf->nRoots, p->pCnf->nClauses-p->pCnf->nRoots, p->Counter, + 1.0*(p->Counter-p->pCnf->nRoots)/(p->pCnf->nClauses-p->pCnf->nRoots), + 1.0*Sto_ManMemoryReport(p->pCnf)/(1<<20) ); + +p->timeTotal += clock() - clkTotal; + Int_ManFree( p ); + return 1; +} + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + diff --git a/src/sat/bsat/satSolver.c b/src/sat/bsat/satSolver.c index 1dd40155..6aafc187 100644 --- a/src/sat/bsat/satSolver.c +++ b/src/sat/bsat/satSolver.c @@ -477,6 +477,16 @@ static void sat_solver_record(sat_solver* s, veci* cls) clause* c = (veci_size(cls) > 1) ? clause_new(s,begin,end,1) : (clause*)0; enqueue(s,*begin,c); + /////////////////////////////////// + // add clause to internal storage + if ( s->pStore ) + { + extern int Sto_ManAddClause( void * p, lit * pBeg, lit * pEnd ); + int RetValue = Sto_ManAddClause( s->pStore, begin, end ); + assert( RetValue ); + } + /////////////////////////////////// + assert(veci_size(cls) > 0); if (c != 0) { @@ -1022,6 +1032,7 @@ void sat_solver_delete(sat_solver* s) free(s->tags ); } + sat_solver_store_free(s); free(s); } @@ -1046,6 +1057,7 @@ bool sat_solver_addclause(sat_solver* s, lit* begin, lit* end) *j = l; } sat_solver_setnvars(s,maxvar+1); +// sat_solver_setnvars(s, lit_var(*(end-1))+1 ); //printlits(begin,end); printf("\n"); values = s->assigns; @@ -1065,7 +1077,18 @@ bool sat_solver_addclause(sat_solver* s, lit* begin, lit* end) if (j == begin) // empty clause return false; - else if (j - begin == 1) // unit clause + + /////////////////////////////////// + // add clause to internal storage + if ( s->pStore ) + { + extern int Sto_ManAddClause( void * p, lit * pBeg, lit * pEnd ); + int RetValue = Sto_ManAddClause( s->pStore, begin, j ); + assert( RetValue ); + } + /////////////////////////////////// + + if (j - begin == 1) // unit clause return enqueue(s,*begin,(clause*)0); // create new clause @@ -1198,6 +1221,15 @@ int sat_solver_solve(sat_solver* s, lit* begin, lit* end, sint64 nConfLimit, sin printf("==============================================================================\n"); sat_solver_canceluntil(s,0); + + //////////////////////////////////////////////// + if ( status == l_Undef && s->pStore ) + { + extern int Sto_ManAddClause( void * p, lit * pBeg, lit * pEnd ); + int RetValue = Sto_ManAddClause( s->pStore, NULL, NULL ); + assert( RetValue ); + } + //////////////////////////////////////////////// return status; } @@ -1220,6 +1252,51 @@ int sat_solver_nconflicts(sat_solver* s) } //================================================================================================= +// Clause storage functions: + +void sat_solver_store_alloc( sat_solver * s ) +{ + extern void * Sto_ManAlloc(); + assert( s->pStore == NULL ); + s->pStore = Sto_ManAlloc(); +} + +void sat_solver_store_write( sat_solver * s, char * pFileName ) +{ + extern void Sto_ManDumpClauses( void * p, char * pFileName ); + Sto_ManDumpClauses( s->pStore, pFileName ); +} + +void sat_solver_store_free( sat_solver * s ) +{ + extern void Sto_ManFree( void * p ); + if ( s->pStore ) Sto_ManFree( s->pStore ); + s->pStore = NULL; +} + +void sat_solver_store_mark_roots( sat_solver * s ) +{ + extern void Sto_ManMarkRoots( void * p ); + if ( s->pStore ) Sto_ManMarkRoots( s->pStore ); +} + +void sat_solver_store_mark_clauses_a( sat_solver * s ) +{ + extern void Sto_ManMarkClausesA( void * p ); + if ( s->pStore ) Sto_ManMarkClausesA( s->pStore ); +} + +void * sat_solver_store_release( sat_solver * s ) +{ + void * pTemp; + if ( s->pStore == NULL ) + return NULL; + pTemp = s->pStore; + s->pStore = NULL; + return pTemp; +} + +//================================================================================================= // Sorting functions (sigh): static inline void selectionsort(void** array, int size, int(*comp)(const void *, const void *)) diff --git a/src/sat/bsat/satSolver.h b/src/sat/bsat/satSolver.h index 6c05a14a..8f71370f 100644 --- a/src/sat/bsat/satSolver.h +++ b/src/sat/bsat/satSolver.h @@ -33,7 +33,13 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA // Simple types: // does not work for c++ -typedef int bool; +//typedef int bool; +#ifndef __cplusplus +#ifndef bool +#define bool int +#endif +#endif + static const bool true = 1; static const bool false = 0; @@ -58,6 +64,8 @@ static inline lit toLitCond(int v, int c) { return v + v + (c != 0); } static inline lit lit_neg (lit l) { return l ^ 1; } static inline int lit_var (lit l) { return l >> 1; } static inline int lit_sign (lit l) { return l & 1; } +static inline int lit_print(lit l) { return lit_sign(l)? -lit_var(l)-1 : lit_var(l)+1; } +static inline lit lit_read (int s) { return s > 0 ? toLit(s-1) : lit_neg(toLit(-s-1)); } //================================================================================================= @@ -88,6 +96,21 @@ typedef struct stats_t stats; extern void Sat_SolverWriteDimacs( sat_solver * p, char * pFileName, lit* assumptionsBegin, lit* assumptionsEnd, int incrementVars ); extern void Sat_SolverPrintStats( FILE * pFile, sat_solver * p ); +extern int * Sat_SolverGetModel( sat_solver * p, int * pVars, int nVars ); +extern void Sat_SolverDoubleClauses( sat_solver * p, int iVar ); + +// trace recording +extern void Sat_SolverTraceStart( sat_solver * pSat, char * pName ); +extern void Sat_SolverTraceStop( sat_solver * pSat ); +extern void Sat_SolverTraceWrite( sat_solver * pSat, int * pBeg, int * pEnd, int fRoot ); + +// clause storage +extern void sat_solver_store_alloc( sat_solver * s ); +extern void sat_solver_store_write( sat_solver * s, char * pFileName ); +extern void sat_solver_store_free( sat_solver * s ); +extern void sat_solver_store_mark_roots( sat_solver * s ); +extern void sat_solver_store_mark_clauses_a( sat_solver * s ); +extern void * sat_solver_store_release( sat_solver * s ); //================================================================================================= // Solver representation: @@ -146,6 +169,14 @@ struct sat_solver_t int nRestarts; // the number of local restarts Sat_MmStep_t * pMem; + + // clause store + void * pStore; + + // trace recording + FILE * pFile; + int nClauses; + int nRoots; }; #endif diff --git a/src/sat/bsat/satStore.c b/src/sat/bsat/satStore.c new file mode 100644 index 00000000..33cba6a7 --- /dev/null +++ b/src/sat/bsat/satStore.c @@ -0,0 +1,437 @@ +/**CFile**************************************************************** + + FileName [satStore.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [SAT solver.] + + Synopsis [Records the trace of SAT solving in the CNF form.] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - June 20, 2005.] + + Revision [$Id: satStore.c,v 1.4 2005/09/16 22:55:03 casem Exp $] + +***********************************************************************/ + +#include <stdio.h> +#include <stdlib.h> +#include <string.h> +#include <assert.h> +#include <time.h> +#include "satStore.h" + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [Fetches memory.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +char * Sto_ManMemoryFetch( Sto_Man_t * p, int nBytes ) +{ + char * pMem; + if ( p->pChunkLast == NULL || nBytes > p->nChunkSize - p->nChunkUsed ) + { + pMem = (char *)malloc( p->nChunkSize ); + *(char **)pMem = p->pChunkLast; + p->pChunkLast = pMem; + p->nChunkUsed = sizeof(char *); + } + pMem = p->pChunkLast + p->nChunkUsed; + p->nChunkUsed += nBytes; + return pMem; +} + +/**Function************************************************************* + + Synopsis [Frees memory manager.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Sto_ManMemoryStop( Sto_Man_t * p ) +{ + char * pMem, * pNext; + if ( p->pChunkLast == NULL ) + return; + for ( pMem = p->pChunkLast; pNext = *(char **)pMem; pMem = pNext ) + free( pMem ); + free( pMem ); +} + +/**Function************************************************************* + + Synopsis [Reports memory usage in bytes.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Sto_ManMemoryReport( Sto_Man_t * p ) +{ + int Total; + char * pMem, * pNext; + if ( p->pChunkLast == NULL ) + return 0; + Total = p->nChunkUsed; + for ( pMem = p->pChunkLast; pNext = *(char **)pMem; pMem = pNext ) + Total += p->nChunkSize; + return Total; +} + + +/**Function************************************************************* + + Synopsis [Allocate proof manager.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Sto_Man_t * Sto_ManAlloc() +{ + Sto_Man_t * p; + // allocate the manager + p = (Sto_Man_t *)malloc( sizeof(Sto_Man_t) ); + memset( p, 0, sizeof(Sto_Man_t) ); + // memory management + p->nChunkSize = (1<<16); // use 64K chunks + return p; +} + +/**Function************************************************************* + + Synopsis [Deallocate proof manager.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Sto_ManFree( Sto_Man_t * p ) +{ + Sto_ManMemoryStop( p ); + free( p ); +} + +/**Function************************************************************* + + Synopsis [Adds one clause to the manager.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Sto_ManAddClause( Sto_Man_t * p, lit * pBeg, lit * pEnd ) +{ + Sto_Cls_t * pClause; + lit Lit, * i, * j; + int nSize; + + // process the literals + if ( pBeg < pEnd ) + { + // insertion sort + for ( i = pBeg + 1; i < pEnd; i++ ) + { + Lit = *i; + for ( j = i; j > pBeg && *(j-1) > Lit; j-- ) + *j = *(j-1); + *j = Lit; + } + // make sure there is no duplicated variables + for ( i = pBeg + 1; i < pEnd; i++ ) + if ( lit_var(*(i-1)) == lit_var(*i) ) + { + printf( "The clause contains two literals of the same variable: %d and %d.\n", *(i-1), *i ); + return 0; + } + // check the largest var size + p->nVars = STO_MAX( p->nVars, lit_var(*(pEnd-1)) + 1 ); + } + + // get memory for the clause + nSize = sizeof(Sto_Cls_t) + sizeof(lit) * (pEnd - pBeg); + pClause = (Sto_Cls_t *)Sto_ManMemoryFetch( p, nSize ); + memset( pClause, 0, sizeof(Sto_Cls_t) ); + + // assign the clause + pClause->Id = p->nClauses++; + pClause->nLits = pEnd - pBeg; + memcpy( pClause->pLits, pBeg, sizeof(lit) * (pEnd - pBeg) ); + + // add the clause to the list + if ( p->pHead == NULL ) + p->pHead = pClause; + if ( p->pTail == NULL ) + p->pTail = pClause; + else + { + p->pTail->pNext = pClause; + p->pTail = pClause; + } + + // add the empty clause + if ( pClause->nLits == 0 ) + { + if ( p->pEmpty ) + { + printf( "More than one empty clause!\n" ); + return 0; + } + p->pEmpty = pClause; + } + return 1; +} + +/**Function************************************************************* + + Synopsis [Mark all clauses added so far as root clauses.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Sto_ManMarkRoots( Sto_Man_t * p ) +{ + Sto_Cls_t * pClause; + p->nRoots = 0; + Sto_ManForEachClause( p, pClause ) + { + pClause->fRoot = 1; + p->nRoots++; + } +} + +/**Function************************************************************* + + Synopsis [Mark all clauses added so far as clause of A.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Sto_ManMarkClausesA( Sto_Man_t * p ) +{ + Sto_Cls_t * pClause; + p->nClausesA = 0; + Sto_ManForEachClause( p, pClause ) + { + pClause->fA = 1; + p->nClausesA++; + } +} + + +/**Function************************************************************* + + Synopsis [Writes the stored clauses into a file.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Sto_ManDumpClauses( Sto_Man_t * p, char * pFileName ) +{ + FILE * pFile; + Sto_Cls_t * pClause; + int i; + // start the file + pFile = fopen( pFileName, "w" ); + if ( pFile == NULL ) + { + printf( "Error: Cannot open output file (%s).\n", pFileName ); + return; + } + // write the data + fprintf( pFile, "p %d %d %d %d\n", p->nVars, p->nClauses, p->nRoots, p->nClausesA ); + Sto_ManForEachClause( p, pClause ) + { + for ( i = 0; i < (int)pClause->nLits; i++ ) + fprintf( pFile, " %d", lit_print(pClause->pLits[i]) ); + fprintf( pFile, "\n" ); + } + fprintf( pFile, "\n" ); + fclose( pFile ); +} + +/**Function************************************************************* + + Synopsis [Reads one literal from file.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Sto_ManLoadNumber( FILE * pFile, int * pNumber ) +{ + int Char, Number = 0, Sign = 0; + // skip space-like chars + do { + Char = fgetc( pFile ); + if ( Char == EOF ) + return 0; + } while ( Char == ' ' || Char == '\t' || Char == '\r' || Char == '\n' ); + // read the literal + while ( 1 ) + { + // get the next character + Char = fgetc( pFile ); + if ( Char == ' ' || Char == '\t' || Char == '\r' || Char == '\n' ) + break; + // check that the char is a digit + if ( (Char < '0' || Char > '9') && Char != '-' ) + { + printf( "Error: Wrong char (%c) in the input file.\n", Char ); + return 0; + } + // check if this is a minus + if ( Char == '-' ) + Sign = 1; + else + Number = 10 * Number + Char; + } + // return the number + *pNumber = Sign? -Number : Number; + return 1; +} + +/**Function************************************************************* + + Synopsis [Reads CNF from file.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Sto_Man_t * Sto_ManLoadClauses( char * pFileName ) +{ + FILE * pFile; + Sto_Man_t * p; + Sto_Cls_t * pClause; + char pBuffer[1024]; + int nLits, nLitsAlloc, Counter, Number; + lit * pLits; + + // start the file + pFile = fopen( pFileName, "r" ); + if ( pFile == NULL ) + { + printf( "Error: Cannot open input file (%s).\n", pFileName ); + return NULL; + } + + // create the manager + p = Sto_ManAlloc(); + + // alloc the array of literals + nLitsAlloc = 1024; + pLits = (lit *)malloc( sizeof(lit) * nLitsAlloc ); + + // read file header + p->nVars = p->nClauses = p->nRoots = p->nClausesA = 0; + while ( fgets( pBuffer, 1024, pFile ) ) + { + if ( pBuffer[0] == 'c' ) + continue; + if ( pBuffer[0] == 'p' ) + { + sscanf( pBuffer + 1, "%d %d %d %d", p->nVars, p->nClauses, p->nRoots, p->nClausesA ); + break; + } + printf( "Warning: Skipping line: \"%s\"\n", pBuffer ); + } + + // read the clauses + nLits = 0; + while ( Sto_ManLoadNumber(pFile, &Number) ) + { + if ( Number == 0 ) + { + int RetValue; + RetValue = Sto_ManAddClause( p, pLits, pLits + nLits ); + assert( RetValue ); + nLits = 0; + continue; + } + if ( nLits == nLitsAlloc ) + { + nLitsAlloc *= 2; + pLits = (lit *)realloc( pLits, sizeof(lit) * nLitsAlloc ); + } + pLits[ nLits++ ] = lit_read(Number); + } + if ( nLits > 0 ) + printf( "Error: The last clause was not saved.\n" ); + + // count clauses + Counter = 0; + Sto_ManForEachClause( p, pClause ) + Counter++; + + // check the number of clauses + if ( p->nClauses != Counter ) + { + printf( "Error: The actual number of clauses (%d) is different than declared (%d).\n", Counter, p->nClauses ); + Sto_ManFree( p ); + return NULL; + } + + free( pLits ); + fclose( pFile ); + return p; +} + + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + diff --git a/src/sat/bsat/satStore.h b/src/sat/bsat/satStore.h new file mode 100644 index 00000000..3db52ada --- /dev/null +++ b/src/sat/bsat/satStore.h @@ -0,0 +1,135 @@ +/**CFile**************************************************************** + + FileName [pr.h] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [Proof recording.] + + Synopsis [External declarations.] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - June 20, 2005.] + + Revision [$Id: pr.h,v 1.00 2005/06/20 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#ifndef __PR_H__ +#define __PR_H__ + +/* + The trace of SAT solving contains the original clause of the problem + along with the learned clauses derived during SAT solving. + The first line of the resulting file contains 3 numbers instead of 2: + c <num_vars> <num_all_clauses> <num_root_clauses> +*/ + +#ifdef __cplusplus +extern "C" { +#endif + +#ifdef _WIN32 +#define inline __inline // compatible with MS VS 6.0 +#endif + +#ifndef PRT +#define PRT(a,t) printf("%s = ", (a)); printf("%6.2f sec\n", (float)(t)/(float)(CLOCKS_PER_SEC)) +#endif + +#define STO_MAX(a,b) ((a) > (b) ? (a) : (b)) + +//////////////////////////////////////////////////////////////////////// +/// INCLUDES /// +//////////////////////////////////////////////////////////////////////// + +//////////////////////////////////////////////////////////////////////// +/// PARAMETERS /// +//////////////////////////////////////////////////////////////////////// + +//////////////////////////////////////////////////////////////////////// +/// BASIC TYPES /// +//////////////////////////////////////////////////////////////////////// + +typedef unsigned lit; + +typedef struct Sto_Cls_t_ Sto_Cls_t; +struct Sto_Cls_t_ +{ + Sto_Cls_t * pNext; // the next clause + Sto_Cls_t * pNext0; // the next 0-watch + Sto_Cls_t * pNext1; // the next 0-watch + int Id; // the clause ID + unsigned fA : 1; // belongs to A + unsigned fRoot : 1; // original clause + unsigned fVisit : 1; // visited clause + unsigned nLits : 24; // the number of literals + lit pLits[0]; // literals of this clause +}; + +typedef struct Sto_Man_t_ Sto_Man_t; +struct Sto_Man_t_ +{ + // general data + int nVars; // the number of variables + int nRoots; // the number of root clauses + int nClauses; // the number of all clauses + int nClausesA; // the number of clauses of A + Sto_Cls_t * pHead; // the head clause + Sto_Cls_t * pTail; // the tail clause + Sto_Cls_t * pEmpty; // the empty clause + // memory management + int nChunkSize; // the number of bytes in a chunk + int nChunkUsed; // the number of bytes used in the last chunk + char * pChunkLast; // the last memory chunk +}; + +// variable/literal conversions (taken from MiniSat) +static inline lit toLit (int v) { return v + v; } +static inline lit toLitCond(int v, int c) { return v + v + (c != 0); } +static inline lit lit_neg (lit l) { return l ^ 1; } +static inline int lit_var (lit l) { return l >> 1; } +static inline int lit_sign (lit l) { return l & 1; } +static inline int lit_print(lit l) { return lit_sign(l)? -lit_var(l)-1 : lit_var(l)+1; } +static inline lit lit_read (int s) { return s > 0 ? toLit(s-1) : lit_neg(toLit(-s-1)); } +static inline int lit_check(lit l, int n) { return l >= 0 && lit_var(l) < n; } + +// iterators through the clauses +#define Sto_ManForEachClause( p, pCls ) for( pCls = p->pHead; pCls; pCls = pCls->pNext ) +#define Sto_ManForEachClauseRoot( p, pCls ) for( pCls = p->pHead; pCls && pCls->fRoot; pCls = pCls->pNext ) + +//////////////////////////////////////////////////////////////////////// +/// MACRO DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +/*=== satStore.c ==========================================================*/ +extern Sto_Man_t * Sto_ManAlloc(); +extern void Sto_ManFree( Sto_Man_t * p ); +extern int Sto_ManAddClause( Sto_Man_t * p, lit * pBeg, lit * pEnd ); +extern int Sto_ManMemoryReport( Sto_Man_t * p ); +extern void Sto_ManMarkRoots( Sto_Man_t * p ); +extern void Sto_ManMarkClausesA( Sto_Man_t * p ); + +/*=== satInter.c ==========================================================*/ +typedef struct Int_Man_t_ Int_Man_t; +extern Int_Man_t * Int_ManAlloc( int nVarsAlloc ); +extern void Int_ManFree( Int_Man_t * p ); +extern int Int_ManInterpolate( Int_Man_t * p, Sto_Man_t * pCnf, int fVerbose, unsigned ** ppResult ); + +#ifdef __cplusplus +} +#endif + +#endif + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + diff --git a/src/sat/asat/satTrace.c b/src/sat/bsat/satTrace.c index 3318933a..111e8dfb 100644 --- a/src/sat/asat/satTrace.c +++ b/src/sat/bsat/satTrace.c @@ -4,7 +4,7 @@ SystemName [ABC: Logic synthesis and verification system.] - PackageName [C-language MiniSat solver.] + PackageName [SAT sat_solver.] Synopsis [Records the trace of SAT solving in the CNF form.] @@ -20,7 +20,7 @@ #include <stdio.h> #include <assert.h> -#include "solver.h" +#include "satSolver.h" /* The trace of SAT solving contains the original clause of the problem @@ -33,9 +33,6 @@ /// DECLARATIONS /// //////////////////////////////////////////////////////////////////////// -static inline int lit_var (lit l) { return l >> 1; } -static inline int lit_sign (lit l) { return l & 1; } -static inline int lit_print(lit l) { return lit_sign(l)? -lit_var(l)-1 : lit_var(l)+1; } //////////////////////////////////////////////////////////////////////// /// FUNCTION DEFINITIONS /// @@ -52,7 +49,7 @@ static inline int lit_print(lit l) { return lit_sign(l)? -lit_var(l)-1 : SeeAlso [] ***********************************************************************/ -void Sat_SolverTraceStart( solver * pSat, char * pName ) +void Sat_SolverTraceStart( sat_solver * pSat, char * pName ) { assert( pSat->pFile == NULL ); pSat->pFile = fopen( pName, "w" ); @@ -72,12 +69,12 @@ void Sat_SolverTraceStart( solver * pSat, char * pName ) SeeAlso [] ***********************************************************************/ -void Sat_SolverTraceStop( solver * pSat ) +void Sat_SolverTraceStop( sat_solver * pSat ) { if ( pSat->pFile == NULL ) return; rewind( pSat->pFile ); - fprintf( pSat->pFile, "p %d %d %d", solver_nvars(pSat), pSat->nClauses, pSat->nRoots ); + fprintf( pSat->pFile, "p %d %d %d", sat_solver_nvars(pSat), pSat->nClauses, pSat->nRoots ); fclose( pSat->pFile ); pSat->pFile = NULL; } @@ -94,7 +91,7 @@ void Sat_SolverTraceStop( solver * pSat ) SeeAlso [] ***********************************************************************/ -void Sat_SolverTraceWrite( solver * pSat, int * pBeg, int * pEnd, int fRoot ) +void Sat_SolverTraceWrite( sat_solver * pSat, int * pBeg, int * pEnd, int fRoot ) { if ( pSat->pFile == NULL ) return; diff --git a/src/sat/bsat/satUtil.c b/src/sat/bsat/satUtil.c index f2b78fe6..76cb2dc2 100644 --- a/src/sat/bsat/satUtil.c +++ b/src/sat/bsat/satUtil.c @@ -153,6 +153,77 @@ void Sat_SolverPrintStats( FILE * pFile, sat_solver * p ) printf( "inspects : %d\n", (int)p->stats.inspects ); } +/**Function************************************************************* + + Synopsis [Returns a counter-example.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int * Sat_SolverGetModel( sat_solver * p, int * pVars, int nVars ) +{ + int * pModel; + int i; + pModel = ALLOC( int, nVars ); + for ( i = 0; i < nVars; i++ ) + { + assert( pVars[i] >= 0 && pVars[i] < p->size ); + pModel[i] = (int)(p->model.ptr[pVars[i]] == l_True); + } + return pModel; +} + +/**Function************************************************************* + + Synopsis [Duplicates all clauses, complements unit clause of the given var.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Sat_SolverDoubleClauses( sat_solver * p, int iVar ) +{ + clause ** pClauses; + lit Lit, * pLits; + int RetValue, nClauses, nVarsOld, nLitsOld, nLits, c, v; + // get the number of variables + nVarsOld = p->size; + nLitsOld = 2 * p->size; + // extend the solver to depend on two sets of variables + sat_solver_setnvars( p, 2 * p->size ); + // duplicate implications + for ( v = 0; v < nVarsOld; v++ ) + if ( p->assigns[v] != l_Undef ) + { + Lit = nLitsOld + toLitCond( v, p->assigns[v]==l_False ); + if ( v == iVar ) + Lit = lit_neg(Lit); + RetValue = sat_solver_addclause( p, &Lit, &Lit + 1 ); + assert( RetValue ); + } + // duplicate clauses + nClauses = vecp_size(&p->clauses); + pClauses = (clause**)vecp_begin(&p->clauses); + for ( c = 0; c < nClauses; c++ ) + { + nLits = clause_size(pClauses[c]); + pLits = clause_begin(pClauses[c]); + for ( v = 0; v < nLits; v++ ) + pLits[v] += nLitsOld; + RetValue = sat_solver_addclause( p, pLits, pLits + nLits ); + assert( RetValue ); + for ( v = 0; v < nLits; v++ ) + pLits[v] -= nLitsOld; + } +} + //////////////////////////////////////////////////////////////////////// /// END OF FILE /// diff --git a/src/sat/csat/csat_apis.c b/src/sat/csat/csat_apis.c index e45b1b81..c7340824 100644 --- a/src/sat/csat/csat_apis.c +++ b/src/sat/csat/csat_apis.c @@ -612,7 +612,7 @@ enum CSAT_StatusT ABC_Solve( ABC_Manager mng ) // try to prove the miter using a number of techniques if ( mng->mode ) - RetValue = Abc_NtkMiterSat( mng->pTarget, (sint64)pParams->nMiteringLimitLast, (sint64)0, 0, 0, NULL, NULL ); + RetValue = Abc_NtkMiterSat( mng->pTarget, (sint64)pParams->nMiteringLimitLast, (sint64)0, 0, NULL, NULL ); else // RetValue = Abc_NtkMiterProve( &mng->pTarget, pParams ); // old CEC engine RetValue = Abc_NtkIvyProve( &mng->pTarget, pParams ); // new CEC engine diff --git a/src/sat/fraig/fraig.h b/src/sat/fraig/fraig.h index 7f15c58f..7e595390 100644 --- a/src/sat/fraig/fraig.h +++ b/src/sat/fraig/fraig.h @@ -27,7 +27,11 @@ extern "C" { /// INCLUDES /// //////////////////////////////////////////////////////////////////////// -#include "solver.h" +#ifdef _WIN32 +typedef signed __int64 sint64; // compatible with MS VS 6.0 +#else +typedef long long sint64; +#endif //////////////////////////////////////////////////////////////////////// /// PARAMETERS /// diff --git a/src/sat/proof/pr.c b/src/sat/proof/pr.c index 4e8a3522..2d1ab2d1 100644 --- a/src/sat/proof/pr.c +++ b/src/sat/proof/pr.c @@ -23,7 +23,7 @@ #include <string.h> #include <assert.h> #include <time.h> -#include "vec.h" +//#include "vec.h" #include "pr.h" //////////////////////////////////////////////////////////////////////// @@ -150,7 +150,7 @@ Pr_Man_t * Pr_ManAlloc( int nVarsAlloc ) // set the starting number of variables p->nVars = 0; // memory management - p->nChunkSize = (1<<18); // use 256K chunks + p->nChunkSize = (1<<16); // use 64K chunks // verification p->nResLitsAlloc = (1<<16); p->pResLits = malloc( sizeof(lit) * p->nResLitsAlloc ); @@ -329,13 +329,6 @@ int Pr_ManAddClause( Pr_Man_t * p, lit * pBeg, lit * pEnd, int fRoot, int fClaus printf( "More than one empty clause!\n" ); p->pEmpty = pClause; } - - // create watcher lists for the root clauses - if ( fRoot && pClause->nLits > 1 ) - { - Pr_ManWatchClause( p, pClause, pClause->pLits[0] ); - Pr_ManWatchClause( p, pClause, pClause->pLits[1] ); - } return 1; } @@ -388,6 +381,29 @@ void Pr_ManMemoryStop( Pr_Man_t * p ) /**Function************************************************************* + Synopsis [Reports memory usage in bytes.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Pr_ManMemoryReport( Pr_Man_t * p ) +{ + int Total; + char * pMem, * pNext; + if ( p->pChunkLast == NULL ) + return 0; + Total = p->nChunkUsed; + for ( pMem = p->pChunkLast; pNext = *(char **)pMem; pMem = pNext ) + Total += p->nChunkSize; + return Total; +} + +/**Function************************************************************* + Synopsis [Records the proof.] Description [] @@ -688,6 +704,7 @@ int Pr_ManProofTraceOne( Pr_Man_t * p, Pr_Cls_t * pConflict, Pr_Cls_t * pFinal ) Var = lit_var(p->pTrail[i]); if ( !p->pSeens[Var] ) continue; + p->pSeens[Var] = 0; // skip literals of the resulting clause pReason = p->pReasons[Var]; @@ -695,6 +712,11 @@ int Pr_ManProofTraceOne( Pr_Man_t * p, Pr_Cls_t * pConflict, Pr_Cls_t * pFinal ) continue; assert( p->pTrail[i] == pReason->pLits[0] ); + // add the variables to seen + for ( v = 1; v < (int)pReason->nLits; v++ ) + p->pSeens[lit_var(pReason->pLits[v])] = 1; + + // record the reason clause assert( pReason->pProof > 0 ); p->Counter++; @@ -751,16 +773,15 @@ int Pr_ManProofTraceOne( Pr_Man_t * p, Pr_Cls_t * pConflict, Pr_Cls_t * pFinal ) } } - // add the variables to seen - for ( v = 1; v < (int)pReason->nLits; v++ ) - p->pSeens[lit_var(pReason->pLits[v])] = 1; - // Vec_PtrPush( pFinal->pAntis, pReason ); } // unmark all seen variables - for ( i = p->nTrailSize - 1; i >= 0; i-- ) - p->pSeens[lit_var(p->pTrail[i])] = 0; +// for ( i = p->nTrailSize - 1; i >= 0; i-- ) +// p->pSeens[lit_var(p->pTrail[i])] = 0; + // check that the literals are unmarked +// for ( i = p->nTrailSize - 1; i >= 0; i-- ) +// assert( p->pSeens[lit_var(p->pTrail[i])] == 0 ); // use the resulting clause to check the correctness of resolution if ( p->fProofVerif ) @@ -904,6 +925,12 @@ int Pr_ManProcessRoots( Pr_Man_t * p ) p->nTrailSize = 0; Pr_ManForEachClauseRoot( p, pClause ) { + // create watcher lists for the root clauses + if ( pClause->nLits > 1 ) + { + Pr_ManWatchClause( p, pClause, pClause->pLits[0] ); + Pr_ManWatchClause( p, pClause, pClause->pLits[1] ); + } // empty clause and large clauses if ( pClause->nLits != 1 ) continue; @@ -1218,9 +1245,10 @@ p->timeRead = clock() - clk; 1.0*(p->Counter-p->nRoots)/(p->nClauses-p->nRoots), nUsed, 1.0*nUsed/(p->nClauses-p->nRoots) ); */ - printf( "Vars = %d. Roots = %d. Learned = %d. Resolution steps = %d. Ave = %.2f.\n", + printf( "Vars = %d. Roots = %d. Learned = %d. Resol steps = %d. Ave = %.2f. Mem = %.2f Mb\n", p->nVars, p->nRoots, p->nClauses-p->nRoots, p->Counter, - 1.0*(p->Counter-p->nRoots)/(p->nClauses-p->nRoots) ); + 1.0*(p->Counter-p->nRoots)/(p->nClauses-p->nRoots), + 1.0*Pr_ManMemoryReport(p)/(1<<20) ); p->timeTotal = clock() - clkTotal; Pr_ManFree( p ); |