diff options
-rw-r--r-- | Makefile | 2 | ||||
-rw-r--r-- | src/base/abci/abc.c | 339 | ||||
-rw-r--r-- | src/sat/xsat/license | 39 | ||||
-rw-r--r-- | src/sat/xsat/module.make | 3 | ||||
-rw-r--r-- | src/sat/xsat/xsat.h | 59 | ||||
-rw-r--r-- | src/sat/xsat/xsatBQueue.h | 189 | ||||
-rw-r--r-- | src/sat/xsat/xsatClause.h | 109 | ||||
-rw-r--r-- | src/sat/xsat/xsatCnfReader.c | 236 | ||||
-rw-r--r-- | src/sat/xsat/xsatHeap.h | 330 | ||||
-rw-r--r-- | src/sat/xsat/xsatMemory.h | 225 | ||||
-rw-r--r-- | src/sat/xsat/xsatSolver.c | 995 | ||||
-rw-r--r-- | src/sat/xsat/xsatSolver.h | 247 | ||||
-rw-r--r-- | src/sat/xsat/xsatSolverAPI.c | 345 | ||||
-rw-r--r-- | src/sat/xsat/xsatUtils.h | 106 | ||||
-rw-r--r-- | src/sat/xsat/xsatWatchList.h | 268 |
15 files changed, 3392 insertions, 100 deletions
@@ -23,7 +23,7 @@ MODULES := \ src/opt/cut src/opt/fxu src/opt/fxch src/opt/rwr src/opt/mfs src/opt/sim \ src/opt/ret src/opt/fret src/opt/res src/opt/lpk src/opt/nwk src/opt/rwt \ src/opt/cgt src/opt/csw src/opt/dar src/opt/dau src/opt/dsc src/opt/sfm src/opt/sbd \ - src/sat/bsat src/sat/csat src/sat/msat src/sat/psat src/sat/cnf src/sat/bmc \ + src/sat/bsat src/sat/xsat src/sat/csat src/sat/msat src/sat/psat src/sat/cnf src/sat/bmc \ src/bool/bdc src/bool/deco src/bool/dec src/bool/kit src/bool/lucky \ src/bool/rsb src/bool/rpo \ src/proof/pdr src/proof/abs src/proof/live src/proof/ssc src/proof/int \ diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index 7da88d3c..dabeb982 100644 --- a/src/base/abci/abc.c +++ b/src/base/abci/abc.c @@ -1,15 +1,15 @@ /**CFile**************************************************************** - - FileName [abc.c] + + FileName [abc.c] SystemName [ABC: Logic synthesis and verification system.] PackageName [Network and node package.] - + Synopsis [Command file.] Author [Alan Mishchenko] - + Affiliation [UC Berkeley] Date [Ver. 1.0. Started - June 20, 2005.] @@ -42,6 +42,7 @@ #include "bool/kit/kit.h" #include "map/amap/amap.h" #include "opt/ret/retInt.h" +#include "sat/xsat/xsat.h" #include "sat/cnf/cnf.h" #include "proof/cec/cec.h" #include "proof/acec/acec.h" @@ -306,6 +307,7 @@ static int Abc_CommandDCec ( Abc_Frame_t * pAbc, int argc, cha static int Abc_CommandDSec ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandSat ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandDSat ( Abc_Frame_t * pAbc, int argc, char ** argv ); +static int Abc_CommandXSat ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandPSat ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandProve ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandIProve ( Abc_Frame_t * pAbc, int argc, char ** argv ); @@ -520,7 +522,7 @@ extern Abc_Ntk_t * Abc_NtkFromAigPhase( Aig_Man_t * pMan ); Synopsis [] Description [] - + SideEffects [] SeeAlso [] @@ -545,7 +547,7 @@ void Abc_FrameReplaceCex( Abc_Frame_t * pAbc, Abc_Cex_t ** ppCex ) Synopsis [] Description [] - + SideEffects [] SeeAlso [] @@ -623,7 +625,7 @@ Vec_Int_t * Abc_FrameDeriveStatusArray( Vec_Ptr_t * vCexes ) Vec_PtrForEachEntry( Abc_Cex_t *, vCexes, pCex, i ) if ( pCex != NULL ) Vec_IntWriteEntry( vStatuses, i, 0 ); // set this output as SAT - return vStatuses; + return vStatuses; } /**Function************************************************************* @@ -951,6 +953,7 @@ void Abc_Init( Abc_Frame_t * pAbc ) Cmd_CommandAdd( pAbc, "Verification", "match", Abc_CommandMatch, 0 ); Cmd_CommandAdd( pAbc, "Verification", "sat", Abc_CommandSat, 0 ); Cmd_CommandAdd( pAbc, "Verification", "dsat", Abc_CommandDSat, 0 ); + Cmd_CommandAdd( pAbc, "Verification", "xsat", Abc_CommandXSat, 0 ); Cmd_CommandAdd( pAbc, "Verification", "psat", Abc_CommandPSat, 0 ); Cmd_CommandAdd( pAbc, "Verification", "prove", Abc_CommandProve, 1 ); Cmd_CommandAdd( pAbc, "Verification", "iprove", Abc_CommandIProve, 1 ); @@ -966,8 +969,8 @@ void Abc_Init( Abc_Frame_t * pAbc ) Cmd_CommandAdd( pAbc, "Verification", "constr", Abc_CommandConstr, 0 ); Cmd_CommandAdd( pAbc, "Verification", "unfold", Abc_CommandUnfold, 1 ); Cmd_CommandAdd( pAbc, "Verification", "fold", Abc_CommandFold, 1 ); - Cmd_CommandAdd( pAbc, "Verification", "unfold2", Abc_CommandUnfold2, 1 ); // jlong - Cmd_CommandAdd( pAbc, "Verification", "fold2", Abc_CommandFold2, 1 ); // jlong + Cmd_CommandAdd( pAbc, "Verification", "unfold2", Abc_CommandUnfold2, 1 ); // jlong + Cmd_CommandAdd( pAbc, "Verification", "fold2", Abc_CommandFold2, 1 ); // jlong Cmd_CommandAdd( pAbc, "Verification", "bm", Abc_CommandBm, 1 ); Cmd_CommandAdd( pAbc, "Verification", "bm2", Abc_CommandBm2, 1 ); Cmd_CommandAdd( pAbc, "Verification", "saucy3", Abc_CommandSaucy, 1 ); @@ -2717,8 +2720,8 @@ int Abc_CommandPrintStatus( Abc_Frame_t * pAbc, int argc, char ** argv ) { if ( fShort ) { - printf( "Status array contains %d SAT, %d UNSAT, and %d UNDEC entries (out of %d).", - Vec_IntCountEntry(pAbc->vStatuses, 0), Vec_IntCountEntry(pAbc->vStatuses, 1), + printf( "Status array contains %d SAT, %d UNSAT, and %d UNDEC entries (out of %d).", + Vec_IntCountEntry(pAbc->vStatuses, 0), Vec_IntCountEntry(pAbc->vStatuses, 1), Vec_IntCountEntry(pAbc->vStatuses, -1), Vec_IntSize(pAbc->vStatuses) ); } else @@ -5296,7 +5299,7 @@ int Abc_CommandMfs2( Abc_Frame_t * pAbc, int argc, char ** argv ) } if ( Vec_IntSize(pAbc->vIndFlops) != Abc_NtkLatchNum(pNtk) ) { - Abc_Print( -1, "The saved flop count (%d) does not match that of the current network (%d).\n", + Abc_Print( -1, "The saved flop count (%d) does not match that of the current network (%d).\n", Vec_IntSize(pAbc->vIndFlops), Abc_NtkLatchNum(pNtk) ); return 0; } @@ -6380,7 +6383,7 @@ int Abc_CommandTestRPO(Abc_Frame_t * pAbc, int argc, char ** argv) { goto usage; } } - if (argc != globalUtilOptind + 1) + if (argc != globalUtilOptind + 1) { Abc_Print(1, "Input file is not given.\n"); goto usage; @@ -12007,7 +12010,7 @@ int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv ) } */ // if ( pNtk ) -// Abc_NtkMakeLegit( pNtk ); +// Abc_NtkMakeLegit( pNtk ); { // extern void Ifd_ManDsdTest(); // Ifd_ManDsdTest(); @@ -14270,7 +14273,7 @@ usage: Synopsis [] Description [] - + SideEffects [] SeeAlso [] @@ -14311,7 +14314,7 @@ usage: Synopsis [] Description [] - + SideEffects [] SeeAlso [] @@ -14390,7 +14393,7 @@ usage: Synopsis [] Description [] - + SideEffects [] SeeAlso [] @@ -15765,7 +15768,7 @@ int Abc_CommandMap( Abc_Frame_t * pAbc, int argc, char ** argv ) } nGatesMin = atoi(argv[globalUtilOptind]); globalUtilOptind++; - if ( nGatesMin < 0 ) + if ( nGatesMin < 0 ) goto usage; break; case 'a': @@ -16468,7 +16471,7 @@ usage: SeeAlso [] ***********************************************************************/ -#if 0 +#if 0 int Abc_CommandFpga( Abc_Frame_t * pAbc, int argc, char ** argv ) { char Buffer[100]; @@ -16839,7 +16842,7 @@ int Abc_CommandIf( Abc_Frame_t * pAbc, int argc, char ** argv ) } pPars->nRelaxRatio = atoi(argv[globalUtilOptind]); globalUtilOptind++; - if ( pPars->nRelaxRatio < 0 ) + if ( pPars->nRelaxRatio < 0 ) goto usage; break; case 'N': @@ -17213,7 +17216,7 @@ int Abc_CommandIf( Abc_Frame_t * pAbc, int argc, char ** argv ) return 0; } } - + // complain if truth tables are requested but the cut size is too large if ( pPars->fTruth && pPars->nLutSize > IF_MAX_FUNC_LUTSIZE ) { @@ -18120,7 +18123,7 @@ int Abc_CommandInit( Abc_Frame_t * pAbc, int argc, char ** argv ) Abc_LatchSetInit0( pObj ); else if ( pInitStr[i] == '1' ) Abc_LatchSetInit1( pObj ); - else + else Abc_LatchSetInitDc( pObj ); return 0; } @@ -18302,7 +18305,7 @@ int Abc_CommandUndc( Abc_Frame_t * pAbc, int argc, char ** argv ) if ( fUseCex ) { - char * pInit; + char * pInit; Abc_Cex_t * pTemp; int k, nFlopsX = 0; if ( pAbc->pCex == NULL ) @@ -18317,7 +18320,7 @@ int Abc_CommandUndc( Abc_Frame_t * pAbc, int argc, char ** argv ) // compare this value if ( Abc_NtkPiNum(pNtk) + nFlopsX != pAbc->pCex->nPis ) { - Abc_Print( -1, "The number of PIs (%d) plus X-valued flops (%d) in the original network does not match the number of PIs in the current CEX (%d).\n", + Abc_Print( -1, "The number of PIs (%d) plus X-valued flops (%d) in the original network does not match the number of PIs in the current CEX (%d).\n", Abc_NtkPiNum(pNtk), Abc_NtkLatchNum(pNtk), pAbc->pCex->nPis ); return 1; } @@ -20701,7 +20704,7 @@ int Abc_CommandSim3( Abc_Frame_t * pAbc, int argc, char ** argv ) extern int Abc_NtkDarSeqSim3( Abc_Ntk_t * pNtk, Ssw_RarPars_t * pPars ); Ssw_RarPars_t Pars, * pPars = &Pars; Abc_Ntk_t * pNtkRes, * pNtk = Abc_FrameReadNtk(pAbc); - Vec_Ptr_t * vSeqModelVec; + Vec_Ptr_t * vSeqModelVec; int c; Ssw_RarSetDefaultParams( pPars ); Extra_UtilGetoptReset(); @@ -23168,6 +23171,144 @@ usage: SeeAlso [] ***********************************************************************/ +int Abc_CommandXSat( Abc_Frame_t * pAbc, int argc, char ** argv ) +{ + abctime clk; + int c; + int fVerbose = 0; + int nConfLimit = 0; + int nInsLimit = 0; + int nLearnedStart = 0; + int nLearnedDelta = 0; + int nLearnedPerce = 0; + Extra_UtilGetoptReset(); + while ( ( c = Extra_UtilGetopt( argc, argv, "CILDEhv" ) ) != EOF ) + { + switch ( c ) + { + case 'C': + if ( globalUtilOptind >= argc ) + { + Abc_Print( -1, "Command line switch \"-C\" should be followed by an integer.\n" ); + goto usage; + } + nConfLimit = atoi(argv[globalUtilOptind]); + globalUtilOptind++; + if ( nConfLimit < 0 ) + goto usage; + break; + case 'I': + if ( globalUtilOptind >= argc ) + { + Abc_Print( -1, "Command line switch \"-I\" should be followed by an integer.\n" ); + goto usage; + } + nInsLimit = atoi(argv[globalUtilOptind]); + globalUtilOptind++; + if ( nInsLimit < 0 ) + goto usage; + break; + case 'L': + if ( globalUtilOptind >= argc ) + { + Abc_Print( -1, "Command line switch \"-L\" should be followed by an integer.\n" ); + goto usage; + } + nLearnedStart = atoi(argv[globalUtilOptind]); + globalUtilOptind++; + if ( nLearnedStart < 0 ) + goto usage; + break; + case 'D': + if ( globalUtilOptind >= argc ) + { + Abc_Print( -1, "Command line switch \"-D\" should be followed by an integer.\n" ); + goto usage; + } + nLearnedDelta = atoi(argv[globalUtilOptind]); + globalUtilOptind++; + if ( nLearnedDelta < 0 ) + goto usage; + break; + case 'E': + if ( globalUtilOptind >= argc ) + { + Abc_Print( -1, "Command line switch \"-E\" should be followed by an integer.\n" ); + goto usage; + } + nLearnedPerce = atoi(argv[globalUtilOptind]); + globalUtilOptind++; + if ( nLearnedPerce < 0 ) + goto usage; + break; + case 'h': + goto usage; + case 'v': + fVerbose ^= 1; + break; + + default: + goto usage; + } + } + + if ( argc == globalUtilOptind + 1 ) + { + char * pFileName = argv[globalUtilOptind]; + xSAT_Solver_t * p; + int status; + + FILE * pFile = fopen( pFileName, "rb" ); + if ( pFile == NULL ) + { + printf( "Cannot open file \"%s\" for writing.\n", pFileName ); + return 0; + } + xSAT_SolverParseDimacs( pFile, &p ); + + clk = Abc_Clock(); + status = xSAT_SolverSolve( p ); + fclose( pFile ); + + xSAT_SolverPrintStats( p ); + if ( status == 0 ) + Abc_Print( 1, "UNDECIDED " ); + else if ( status == 1 ) + Abc_Print( 1, "SATISFIABLE " ); + else + Abc_Print( 1, "UNSATISFIABLE " ); + + Abc_PrintTime( 1, "Time", Abc_Clock() - clk ); + + xSAT_SolverDestroy( p ); + return 0; + } + +usage: + Abc_Print( -2, "usage: xsat [-CILDE num] [-hv]<file>.cnf\n" ); + Abc_Print( -2, "\t solves the combinational miter using SAT solver MiniSat-1.14\n" ); + Abc_Print( -2, "\t derives CNF from the current network and leaves it unchanged\n" ); + Abc_Print( -2, "\t-C num : limit on the number of conflicts [default = %d]\n", nConfLimit ); + Abc_Print( -2, "\t-I num : limit on the number of inspections [default = %d]\n", nInsLimit ); + Abc_Print( -2, "\t-L num : starting value for learned clause removal [default = %d]\n", nLearnedStart ); + Abc_Print( -2, "\t-D num : delta value for learned clause removal [default = %d]\n", nLearnedDelta ); + Abc_Print( -2, "\t-E num : ratio percentage for learned clause removal [default = %d]\n", nLearnedPerce ); + Abc_Print( -2, "\t-v : prints verbose information [default = %s]\n", fVerbose? "yes": "no" ); + Abc_Print( -2, "\t-h : print the command usage\n"); + return 1; +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ int Abc_CommandPSat( Abc_Frame_t * pAbc, int argc, char ** argv ) { Abc_Ntk_t * pNtk = Abc_FrameReadNtk(pAbc); @@ -24155,7 +24296,7 @@ int Abc_CommandBmc3( Abc_Frame_t * pAbc, int argc, char ** argv ) } } vStatuses = Abc_FrameDeriveStatusArray( vSeqModelVec ); - Abc_FrameReplacePoStatuses( pAbc, &vStatuses ); + Abc_FrameReplacePoStatuses( pAbc, &vStatuses ); if ( vSeqModelVec ) Abc_FrameReplaceCexVec( pAbc, &vSeqModelVec ); else @@ -25483,47 +25624,47 @@ usage: Synopsis [] Description [] - + SideEffects [] SeeAlso [] ***********************************************************************/ int Abc_CommandBm2( Abc_Frame_t * pAbc, int argc, char ** argv ) -{ +{ FILE * pOut, * pErr; Abc_Ntk_t *pNtk, *pNtk1, *pNtk2; - int fDelete1, fDelete2; + int fDelete1, fDelete2; Abc_Obj_t * pObj; char ** pArgvNew; - int c, nArgcNew, i; + int c, nArgcNew, i; extern void saucyGateWay( Abc_Ntk_t * pNtk, Abc_Obj_t * pNodePo, FILE * gFile, int fBooleanMatching, int fLookForSwaps, int fFixOutputs, int fFixInputs, int fQuiet, int fPrintTree); pNtk = Abc_FrameReadNtk(pAbc); pOut = Abc_FrameReadOut(pAbc); - pErr = Abc_FrameReadErr(pAbc); - + pErr = Abc_FrameReadErr(pAbc); + Extra_UtilGetoptReset(); while ( ( c = Extra_UtilGetopt( argc, argv, "h" ) ) != EOF ) { switch ( c ) { case 'h': - goto usage; + goto usage; default: Abc_Print( -2, "Unknown switch.\n"); goto usage; } } - + pArgvNew = argv + globalUtilOptind; nArgcNew = argc - globalUtilOptind; if ( !Abc_NtkPrepareTwoNtks( pErr, pNtk, pArgvNew, nArgcNew , &pNtk1, &pNtk2, &fDelete1, &fDelete2 ) ) return 1; - - if( (unsigned)Abc_NtkPiNum(pNtk1) != (unsigned)Abc_NtkPiNum(pNtk2) || + + if( (unsigned)Abc_NtkPiNum(pNtk1) != (unsigned)Abc_NtkPiNum(pNtk2) || (unsigned)Abc_NtkPoNum(pNtk1) != (unsigned)Abc_NtkPoNum(pNtk2) ) { Abc_Print( -2, "Mismatch in the number of inputs or outputs\n"); @@ -25532,7 +25673,7 @@ int Abc_CommandBm2( Abc_Frame_t * pAbc, int argc, char ** argv ) if ( fDelete2 ) Abc_NtkDelete( pNtk2 ); return 1; } - + Abc_NtkPermute(pNtk2, 1, 1, 0, NULL ); Abc_NtkShortNames(pNtk2); @@ -25562,7 +25703,7 @@ int Abc_CommandBm2( Abc_Frame_t * pAbc, int argc, char ** argv ) saucyGateWay( pNtk1, NULL, NULL, 1, 0, 0, 0, 0, 0); if ( fDelete1 ) Abc_NtkDelete( pNtk1 ); - if ( fDelete2 ) Abc_NtkDelete( pNtk2 ); + if ( fDelete2 ) Abc_NtkDelete( pNtk2 ); return 0; usage: @@ -25570,8 +25711,8 @@ usage: Abc_Print( -2, "\t performs Boolean matching (PP-equivalence)\n" ); Abc_Print( -2, "\t for equivalent circuits, permutation that maps one circuit\n" ); Abc_Print( -2, "\t to another is printed to standard output (PIs and POs of the\n" ); - Abc_Print( -2, "\t first network have prefix \"N1:\", while PIs and POs of the\n" ); - Abc_Print( -2, "\t second network have prefix \"N2:\")\n" ); + Abc_Print( -2, "\t first network have prefix \"N1:\", while PIs and POs of the\n" ); + Abc_Print( -2, "\t second network have prefix \"N2:\")\n" ); Abc_Print( -2, "\t-h : print the command usage\n"); Abc_Print( -2, "\tfile1 : the file with the first network\n"); Abc_Print( -2, "\tfile2 : the file with the second network\n"); @@ -25593,14 +25734,14 @@ usage: Synopsis [] Description [] - + SideEffects [] SeeAlso [] ***********************************************************************/ int Abc_CommandSaucy( Abc_Frame_t * pAbc, int argc, char ** argv ) -{ +{ Abc_Ntk_t *pNtk; char * outputName = NULL; FILE * gFile = NULL; @@ -25629,20 +25770,20 @@ int Abc_CommandSaucy( Abc_Frame_t * pAbc, int argc, char ** argv ) outputName = argv[globalUtilOptind]; if ( !strcmp(argv[globalUtilOptind], "all") ) fOutputsOneAtTime ^= 1; - globalUtilOptind++; + globalUtilOptind++; break; case 'F': if ( globalUtilOptind >= argc ) { Abc_Print( -1, "Command line switch \"-F\" should be followed by a file name.\n" ); goto usage; - } + } if ( (gFile = fopen( argv[globalUtilOptind], "w" )) == NULL ) { - Abc_Print( -1, "Cannot create output file \"%s\". ", argv[globalUtilOptind] ); + Abc_Print( -1, "Cannot create output file \"%s\". ", argv[globalUtilOptind] ); return 1; } - globalUtilOptind++; + globalUtilOptind++; break; case 'i': fFixOutputs ^= 1; @@ -25665,9 +25806,9 @@ int Abc_CommandSaucy( Abc_Frame_t * pAbc, int argc, char ** argv ) Abc_Print( -2, "Unknown switch.\n"); goto usage; } - } - - pNtk = Abc_FrameReadNtk(pAbc); + } + + pNtk = Abc_FrameReadNtk(pAbc); if ( pNtk == NULL ) { @@ -25690,21 +25831,21 @@ int Abc_CommandSaucy( Abc_Frame_t * pAbc, int argc, char ** argv ) Abc_NtkForEachPo( pNtk, pNodePo, i ) { printf("Ouput %s\n\n", Abc_ObjName(pNodePo)); saucyGateWay( pNtk, pNodePo, gFile, 0, fLookForSwaps, fFixOutputs, fFixInputs, fQuiet, fPrintTree ); - printf("----------------------------------------\n"); + printf("----------------------------------------\n"); } fclose(hadi); } else if (outputName != NULL) { int i; - Abc_Obj_t * pNodePo; + Abc_Obj_t * pNodePo; Abc_NtkForEachPo( pNtk, pNodePo, i ) { if (!strcmp(Abc_ObjName(pNodePo), outputName)) { saucyGateWay( pNtk, pNodePo, gFile, 0, fLookForSwaps, fFixOutputs, fFixInputs, fQuiet, fPrintTree ); Abc_NtkDelete( pNtk ); return 0; - } + } } Abc_Print( -1, "Output not found\n" ); - return 1; + return 1; } else saucyGateWay( pNtk, NULL, gFile, 0, fLookForSwaps, fFixOutputs, fFixInputs, fQuiet, fPrintTree ); @@ -25715,9 +25856,9 @@ int Abc_CommandSaucy( Abc_Frame_t * pAbc, int argc, char ** argv ) usage: Abc_Print( -2, "usage: saucy3 [-O <name>] [-F <file>] [-iosqvh]\n\n" ); Abc_Print( -2, "\t computes functional symmetries of the netowrk\n" ); - Abc_Print( -2, "\t prints symmetry generators to the standard output\n" ); + Abc_Print( -2, "\t prints symmetry generators to the standard output\n" ); Abc_Print( -2, "\t-O <name> : (optional) compute symmetries only for output given by name\n"); - Abc_Print( -2, "\t only inputs in the output cone are permuted\n"); + Abc_Print( -2, "\t only inputs in the output cone are permuted\n"); Abc_Print( -2, "\t (special case) name=all, compute symmetries for each\n" ); Abc_Print( -2, "\t output, but only one output at a time\n" ); Abc_Print( -2, "\t [default = compute symmetries by permuting all I/Os]\n" ); @@ -25726,8 +25867,8 @@ usage: Abc_Print( -2, "\t-o : permute just the outputs (fix the inputs) [default = no]\n"); Abc_Print( -2, "\t-s : only look for swaps of inputs [default = no]\n"); Abc_Print( -2, "\t-q : quiet (do not print symmetry generators) [default = no]\n"); - Abc_Print( -2, "\t-v : verbose (print the search tree) [default = no]\n"); - Abc_Print( -2, "\t-h : print the command usage\n"); + Abc_Print( -2, "\t-v : verbose (print the search tree) [default = no]\n"); + Abc_Print( -2, "\t-h : print the command usage\n"); Abc_Print( -2, "\t \n" ); Abc_Print( -2, "\t This command was contributed by Hadi Katebi from U Michigan.\n" ); @@ -27055,7 +27196,7 @@ int Abc_CommandAbc9Read( Abc_Frame_t * pAbc, int argc, char ** argv ) pAig = Gia_ManReadMiniLut( FileName ); // else if ( Extra_FileIsType( FileName, ".v", NULL, NULL ) ) // Abc3_ReadShowHie( FileName, fSkipStrash ); - else + else pAig = Gia_AigerRead( FileName, fGiaSimple, fSkipStrash, 0 ); if ( pAig ) Abc_FrameUpdateGia( pAbc, pAig ); @@ -27466,8 +27607,8 @@ int Abc_CommandAbc9Get( Abc_Frame_t * pAbc, int argc, char ** argv ) Vec_FltFreeP( &pGia->vOutReqs ); pGia->DefInArrs = Abc_NtkReadDefaultArrivalWorst(pNtk); pGia->DefOutReqs = Abc_NtkReadDefaultRequiredWorst(pNtk); - pGia->vInArrs = Vec_FltAllocArray( Abc_NtkGetCiArrivalFloats(pNtk), Abc_NtkCiNum(pNtk) ); - pGia->vOutReqs = Vec_FltAllocArray( Abc_NtkGetCoRequiredFloats(pNtk), Abc_NtkCoNum(pNtk) ); + pGia->vInArrs = Vec_FltAllocArray( Abc_NtkGetCiArrivalFloats(pNtk), Abc_NtkCiNum(pNtk) ); + pGia->vOutReqs = Vec_FltAllocArray( Abc_NtkGetCoRequiredFloats(pNtk), Abc_NtkCoNum(pNtk) ); } Abc_FrameUpdateGia( pAbc, pGia ); return 0; @@ -27626,7 +27767,7 @@ usage: Synopsis [Compares to versions of the design and finds the best.] Description [] - + SideEffects [] SeeAlso [] @@ -27637,11 +27778,11 @@ static inline int Gia_ManCompareWithBest( Gia_Man_t * pBest, Gia_Man_t * p, int int nCurLuts, nCurEdges, nCurLevels; Gia_ManLutParams( p, &nCurLuts, &nCurEdges, &nCurLevels ); if ( pBest == NULL || - Gia_ManPiNum(pBest) != Gia_ManPiNum(p) || - Gia_ManPoNum(pBest) != Gia_ManPoNum(p) || + Gia_ManPiNum(pBest) != Gia_ManPiNum(p) || + Gia_ManPoNum(pBest) != Gia_ManPoNum(p) || Gia_ManRegNum(pBest) != Gia_ManRegNum(p) || strcmp(Gia_ManName(pBest), Gia_ManName(p)) || - (!fArea && (*pnBestLevels > nCurLevels || (*pnBestLevels == nCurLevels && 2*(*pnBestLuts) + *pnBestEdges > 2*nCurLuts + nCurEdges))) || + (!fArea && (*pnBestLevels > nCurLevels || (*pnBestLevels == nCurLevels && 2*(*pnBestLuts) + *pnBestEdges > 2*nCurLuts + nCurEdges))) || ( fArea && (*pnBestLuts > nCurLuts || (*pnBestLuts == nCurLuts && *pnBestLevels > nCurLevels))) ) { @@ -27659,7 +27800,7 @@ static inline int Gia_ManCompareWithBest( Gia_Man_t * pBest, Gia_Man_t * p, int Synopsis [] Description [] - + SideEffects [] SeeAlso [] @@ -27697,7 +27838,7 @@ int Abc_CommandAbc9Save( Abc_Frame_t * pAbc, int argc, char ** argv ) // save the design as best Gia_ManStopP( &pAbc->pGiaBest ); pAbc->pGiaBest = Gia_ManDupWithAttributes( pAbc->pGia ); - return 0; + return 0; usage: Abc_Print( -2, "usage: &save [-ah]\n" ); @@ -27712,7 +27853,7 @@ usage: Synopsis [] Description [] - + SideEffects [] SeeAlso [] @@ -30868,7 +31009,7 @@ int Abc_CommandAbc9Syn2( Abc_Frame_t * pAbc, int argc, char ** argv ) } nRelaxRatio = atoi(argv[globalUtilOptind]); globalUtilOptind++; - if ( nRelaxRatio < 0 ) + if ( nRelaxRatio < 0 ) goto usage; break; case 'a': @@ -30908,7 +31049,7 @@ int Abc_CommandAbc9Syn2( Abc_Frame_t * pAbc, int argc, char ** argv ) printf( "DSD manager has incompatible number of variables. Delay minimization is not performed.\n" ); fDelayMin = 0; } - } + } pTemp = Gia_ManAigSyn2( pAbc->pGia, fOldAlgo, fCoarsen, fCutMin, nRelaxRatio, fDelayMin, fVerbose, fVeryVerbose ); Abc_FrameUpdateGia( pAbc, pTemp ); return 0; @@ -31005,7 +31146,7 @@ int Abc_CommandAbc9Synch2( Abc_Frame_t * pAbc, int argc, char ** argv ) } nRelaxRatio = atoi(argv[globalUtilOptind]); globalUtilOptind++; - if ( nRelaxRatio < 0 ) + if ( nRelaxRatio < 0 ) goto usage; break; case 'f': @@ -32857,7 +32998,7 @@ int Abc_CommandAbc9Cec( Abc_Frame_t * pAbc, int argc, char ** argv ) pAbc->Status = Cec_ManVerify( pTemp, pPars ); ABC_SWAP( Abc_Cex_t *, pAbc->pGia->pCexComb, pTemp->pCexComb ); Gia_ManStop( pTemp ); - } + } Abc_FrameReplaceCex( pAbc, &pAbc->pGia->pCexComb ); return 0; } @@ -33749,7 +33890,7 @@ int Abc_CommandAbc9If( Abc_Frame_t * pAbc, int argc, char ** argv ) } pPars->nRelaxRatio = atoi(argv[globalUtilOptind]); globalUtilOptind++; - if ( pPars->nRelaxRatio < 0 ) + if ( pPars->nRelaxRatio < 0 ) goto usage; break; case 'T': @@ -34867,7 +35008,7 @@ int Abc_CommandAbc9Lf( Abc_Frame_t * pAbc, int argc, char ** argv ) } pPars->nRelaxRatio = atoi(argv[globalUtilOptind]); globalUtilOptind++; - if ( pPars->nRelaxRatio < 0 ) + if ( pPars->nRelaxRatio < 0 ) goto usage; break; case 'L': @@ -34878,7 +35019,7 @@ int Abc_CommandAbc9Lf( Abc_Frame_t * pAbc, int argc, char ** argv ) } pPars->nCoarseLimit = atoi(argv[globalUtilOptind]); globalUtilOptind++; - if ( pPars->nCoarseLimit < 0 ) + if ( pPars->nCoarseLimit < 0 ) goto usage; break; case 'E': @@ -34889,7 +35030,7 @@ int Abc_CommandAbc9Lf( Abc_Frame_t * pAbc, int argc, char ** argv ) } pPars->nAreaTuner = atoi(argv[globalUtilOptind]); globalUtilOptind++; - if ( pPars->nAreaTuner < 0 ) + if ( pPars->nAreaTuner < 0 ) goto usage; break; case 'D': @@ -35099,7 +35240,7 @@ int Abc_CommandAbc9Mf( Abc_Frame_t * pAbc, int argc, char ** argv ) } pPars->nRelaxRatio = atoi(argv[globalUtilOptind]); globalUtilOptind++; - if ( pPars->nRelaxRatio < 0 ) + if ( pPars->nRelaxRatio < 0 ) goto usage; break; case 'L': @@ -35110,7 +35251,7 @@ int Abc_CommandAbc9Mf( Abc_Frame_t * pAbc, int argc, char ** argv ) } pPars->nCoarseLimit = atoi(argv[globalUtilOptind]); globalUtilOptind++; - if ( pPars->nCoarseLimit < 0 ) + if ( pPars->nCoarseLimit < 0 ) goto usage; break; case 'E': @@ -35121,7 +35262,7 @@ int Abc_CommandAbc9Mf( Abc_Frame_t * pAbc, int argc, char ** argv ) } pPars->nAreaTuner = atoi(argv[globalUtilOptind]); globalUtilOptind++; - if ( pPars->nAreaTuner < 0 ) + if ( pPars->nAreaTuner < 0 ) goto usage; break; case 'D': @@ -35303,7 +35444,7 @@ int Abc_CommandAbc9Nf( Abc_Frame_t * pAbc, int argc, char ** argv ) } pPars->nRelaxRatio = atoi(argv[globalUtilOptind]); globalUtilOptind++; - if ( pPars->nRelaxRatio < 0 ) + if ( pPars->nRelaxRatio < 0 ) goto usage; break; case 'L': @@ -35314,7 +35455,7 @@ int Abc_CommandAbc9Nf( Abc_Frame_t * pAbc, int argc, char ** argv ) } pPars->nCoarseLimit = atoi(argv[globalUtilOptind]); globalUtilOptind++; - if ( pPars->nCoarseLimit < 0 ) + if ( pPars->nCoarseLimit < 0 ) goto usage; break; case 'E': @@ -35325,7 +35466,7 @@ int Abc_CommandAbc9Nf( Abc_Frame_t * pAbc, int argc, char ** argv ) } pPars->nAreaTuner = atoi(argv[globalUtilOptind]); globalUtilOptind++; - if ( pPars->nAreaTuner < 0 ) + if ( pPars->nAreaTuner < 0 ) goto usage; break; case 'D': @@ -35518,7 +35659,7 @@ int Abc_CommandAbc9Of( Abc_Frame_t * pAbc, int argc, char ** argv ) } pPars->nRelaxRatio = atoi(argv[globalUtilOptind]); globalUtilOptind++; - if ( pPars->nRelaxRatio < 0 ) + if ( pPars->nRelaxRatio < 0 ) goto usage; break; case 'L': @@ -35529,7 +35670,7 @@ int Abc_CommandAbc9Of( Abc_Frame_t * pAbc, int argc, char ** argv ) } pPars->nCoarseLimit = atoi(argv[globalUtilOptind]); globalUtilOptind++; - if ( pPars->nCoarseLimit < 0 ) + if ( pPars->nCoarseLimit < 0 ) goto usage; break; case 'E': @@ -35540,7 +35681,7 @@ int Abc_CommandAbc9Of( Abc_Frame_t * pAbc, int argc, char ** argv ) } pPars->nAreaTuner = atoi(argv[globalUtilOptind]); globalUtilOptind++; - if ( pPars->nAreaTuner < 0 ) + if ( pPars->nAreaTuner < 0 ) goto usage; break; case 'D': @@ -35886,7 +36027,7 @@ int Abc_CommandAbc9Edge( Abc_Frame_t * pAbc, int argc, char ** argv ) { //Edg_ManAssignEdgeNew( pAbc->pGia, nEdges, fVerbose ); Seg_ManComputeDelay( pAbc->pGia, DelayMax, nFanouts, nEdges==2, fVerbose ); - return 0; + return 0; } if ( pAbc->pGia->pManTime && fReverse ) { @@ -35895,7 +36036,7 @@ int Abc_CommandAbc9Edge( Abc_Frame_t * pAbc, int argc, char ** argv ) } if ( fReverse ) DelayMax = Gia_ManComputeEdgeDelay2( pAbc->pGia ); - else + else DelayMax = Gia_ManComputeEdgeDelay( pAbc->pGia, nEdges == 2 ); //printf( "The number of edges = %d. Delay = %d.\n", Gia_ManEvalEdgeCount(pAbc->pGia), DelayMax ); return 0; @@ -38307,7 +38448,7 @@ int Abc_CommandAbc9MultiProve( Abc_Frame_t * pAbc, int argc, char ** argv ) } pAbc->Status = Gia_ManMultiProve( pAbc->pGia, pPars ); vStatuses = Abc_FrameDeriveStatusArray( pAbc->pGia->vSeqModelVec ); - Abc_FrameReplacePoStatuses( pAbc, &vStatuses ); + Abc_FrameReplacePoStatuses( pAbc, &vStatuses ); Abc_FrameReplaceCexVec( pAbc, &pAbc->pGia->vSeqModelVec ); return 0; @@ -38454,7 +38595,7 @@ int Abc_CommandAbc9Bmc( Abc_Frame_t * pAbc, int argc, char ** argv ) Bmc_AndPar_t Pars, * pPars = &Pars; memset( pPars, 0, sizeof(Bmc_AndPar_t) ); pPars->nStart = 0; // starting timeframe - pPars->nFramesMax = 0; // maximum number of timeframes + pPars->nFramesMax = 0; // maximum number of timeframes pPars->nFramesAdd = 50; // the number of additional frames pPars->nConfLimit = 0; // maximum number of conflicts at a node pPars->nTimeOut = 0; // timeout in seconds @@ -38463,9 +38604,9 @@ int Abc_CommandAbc9Bmc( Abc_Frame_t * pAbc, int argc, char ** argv ) pPars->fDumpFrames = 0; // dump unrolled timeframes pPars->fUseSynth = 0; // use synthesis pPars->fUseOldCnf = 0; // use old CNF construction - pPars->fVerbose = 0; // verbose - pPars->fVeryVerbose = 0; // very verbose - pPars->fNotVerbose = 0; // skip line-by-line print-out + pPars->fVerbose = 0; // verbose + pPars->fVeryVerbose = 0; // very verbose + pPars->fNotVerbose = 0; // skip line-by-line print-out pPars->iFrame = 0; // explored up to this frame pPars->nFailOuts = 0; // the number of failed outputs pPars->nDropOuts = 0; // the number of dropped outputs @@ -39166,7 +39307,7 @@ usage: Abc_Print( -2, "\t ((a&b)^p) complement at the output\n"); Abc_Print( -2, "\t (((a^p)&(b^q))^r) complement at the inputs and at the output\n"); Abc_Print( -2, "\t (a?(b?~s:r):(b?q:p)) functionally observable fault at the output\n"); - Abc_Print( -2, "\t (p?(a|b):(a&b)) replace AND by OR\n"); + Abc_Print( -2, "\t (p?(a|b):(a&b)) replace AND by OR\n"); return 1; } @@ -40039,7 +40180,7 @@ int Abc_CommandAbc9Demiter( Abc_Frame_t * pAbc, int argc, char ** argv ) { char pName0[1000] = "miter_part0.aig"; char pName1[1000] = "miter_part1.aig"; - Gia_Man_t * pPart1, * pPart2; + Gia_Man_t * pPart1, * pPart2; if ( Gia_ManPoNum(pAbc->pGia) % 2 != 0 ) { Abc_Print( -1, "Abc_CommandAbc9Demiter(): Does not look like a dual-output miter.\n" ); @@ -40481,7 +40622,7 @@ int Abc_CommandAbc9Acec( Abc_Frame_t * pAbc, int argc, char ** argv ) Gia_ManDemiterDual( pDual, &pGia0, &pGia1 ); Gia_ManStop( pDual ); pAbc->Status = Gia_PolynCec( pGia0, pGia1, pPars ); - } + } Abc_FrameReplaceCex( pAbc, &pGia0->pCexComb ); Gia_ManStop( pGia0 ); Gia_ManStop( pGia1 ); @@ -40687,7 +40828,7 @@ usage: Synopsis [] Description [] - + SideEffects [] SeeAlso [] @@ -40701,7 +40842,7 @@ int Abc_CommandAbc9Mfs( Abc_Frame_t * pAbc, int argc, char ** argv ) Sfm_ParSetDefault( pPars ); pPars->nTfoLevMax = 5; pPars->nDepthMax = 100; - pPars->nWinSizeMax = 2000; + pPars->nWinSizeMax = 2000; Extra_UtilGetoptReset(); while ( ( c = Extra_UtilGetopt( argc, argv, "WFDMLCNdaebvwh" ) ) != EOF ) { @@ -40852,7 +40993,7 @@ usage: Synopsis [] Description [] - + SideEffects [] SeeAlso [] @@ -41324,7 +41465,7 @@ usage: Synopsis [] Description [] - + SideEffects [] SeeAlso [] @@ -41385,7 +41526,7 @@ usage: Synopsis [] Description [] - + SideEffects [] SeeAlso [] diff --git a/src/sat/xsat/license b/src/sat/xsat/license new file mode 100644 index 00000000..a6389ab1 --- /dev/null +++ b/src/sat/xsat/license @@ -0,0 +1,39 @@ +xSAT - Copyright (c) 2016, Bruno Schmitt - UC Berkeley / UFRGS (boschmitt@inf.ufrgs.br) + +xSAT is based on Glucose v3(see Glucose copyrights below) and ABC C version of +MiniSat (bsat) developed by Niklas Sorensson and modified by Alan Mishchenko. +Permissions and copyrights of xSAT are exactly the same as Glucose v3/Minisat. +(see below). + +--------------- + +Glucose -- Copyright (c) 2013, Gilles Audemard, Laurent Simon + CRIL - Univ. Artois, France + LRI - Univ. Paris Sud, France + +Glucose sources are based on MiniSat (see below MiniSat copyrights). Permissions +and copyrights of Glucose are exactly the same as Minisat on which it is based +on. (see below). + +--------------- + +Copyright (c) 2003-2006, Niklas Een, Niklas Sorensson +Copyright (c) 2007-2010, Niklas Sorensson + +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. +*******************************************************************************/ diff --git a/src/sat/xsat/module.make b/src/sat/xsat/module.make new file mode 100644 index 00000000..1d7352e2 --- /dev/null +++ b/src/sat/xsat/module.make @@ -0,0 +1,3 @@ +SRC += src/sat/xsat/xsatSolver.c \ + src/sat/xsat/xsatSolverAPI.c \ + src/sat/xsat/xsatCnfReader.c diff --git a/src/sat/xsat/xsat.h b/src/sat/xsat/xsat.h new file mode 100644 index 00000000..b2962d91 --- /dev/null +++ b/src/sat/xsat/xsat.h @@ -0,0 +1,59 @@ +/**CFile**************************************************************** + + FileName [xsat.h] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [xSAT - A SAT solver written in C. + Read the license file for more info.] + + Synopsis [External definitions of the solver.] + + Author [Bruno Schmitt <boschmitt@inf.ufrgs.br>] + + Affiliation [UC Berkeley / UFRGS] + + Date [Ver. 1.0. Started - November 10, 2016.] + + Revision [] + +***********************************************************************/ +#ifndef ABC__sat__xSAT__xSAT_h +#define ABC__sat__xSAT__xSAT_h + +//////////////////////////////////////////////////////////////////////// +/// INCLUDES /// +//////////////////////////////////////////////////////////////////////// +#include "misc/util/abc_global.h" +#include "misc/vec/vecInt.h" + +ABC_NAMESPACE_HEADER_START + +//////////////////////////////////////////////////////////////////////// +/// STRUCTURE DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// +struct xSAT_Solver_t_; +typedef struct xSAT_Solver_t_ xSAT_Solver_t; + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// +/*=== xsatCnfReader.c ================================================*/ +extern int xSAT_SolverParseDimacs( FILE *, xSAT_Solver_t ** ); + +/*=== xsatSolverAPI.c ================================================*/ +extern xSAT_Solver_t * xSAT_SolverCreate(); +extern void xSAT_SolverDestroy( xSAT_Solver_t * ); + +extern int xSAT_SolverAddClause( xSAT_Solver_t *, Vec_Int_t * ); +extern int xSAT_SolverSimplify( xSAT_Solver_t * ); +extern int xSAT_SolverSolve( xSAT_Solver_t * ); + +extern void xSAT_SolverPrintStats( xSAT_Solver_t * ); + +ABC_NAMESPACE_HEADER_END + +#endif +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// diff --git a/src/sat/xsat/xsatBQueue.h b/src/sat/xsat/xsatBQueue.h new file mode 100644 index 00000000..37951684 --- /dev/null +++ b/src/sat/xsat/xsatBQueue.h @@ -0,0 +1,189 @@ +/**CFile**************************************************************** + + FileName [xsatBQueue.h] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [xSAT - A SAT solver written in C. + Read the license file for more info.] + + Synopsis [Bounded queue implementation.] + + Author [Bruno Schmitt <boschmitt@inf.ufrgs.br>] + + Affiliation [UC Berkeley / UFRGS] + + Date [Ver. 1.0. Started - November 10, 2016.] + + Revision [] + +***********************************************************************/ +#ifndef ABC__sat__xSAT__xsatBQueue_h +#define ABC__sat__xSAT__xsatBQueue_h + +//////////////////////////////////////////////////////////////////////// +/// INCLUDES /// +//////////////////////////////////////////////////////////////////////// +#include "misc/util/abc_global.h" + +ABC_NAMESPACE_HEADER_START + +//////////////////////////////////////////////////////////////////////// +/// STRUCTURE DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// +typedef struct xSAT_BQueue_t_ xSAT_BQueue_t; +struct xSAT_BQueue_t_ +{ + int nSize; + int nCap; + int iFirst; + int iEmpty; + uint64_t nSum; + uint32_t * pData; +}; + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline xSAT_BQueue_t * xSAT_BQueueNew( int nCap ) +{ + xSAT_BQueue_t * p = ABC_CALLOC( xSAT_BQueue_t, 1 ); + p->nCap = nCap; + p->pData = ABC_CALLOC( uint32_t, nCap ); + return p; +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline void xSAT_BQueueFree( xSAT_BQueue_t * p ) +{ + ABC_FREE( p->pData ); + ABC_FREE( p ); +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline void xSAT_BQueuePush( xSAT_BQueue_t * p, uint32_t Value ) +{ + if ( p->nSize == p->nCap ) + { + assert(p->iFirst == p->iEmpty); + p->nSum -= p->pData[p->iFirst]; + p->iFirst = ( p->iFirst + 1 ) % p->nCap; + } + else + p->nSize++; + + p->nSum += Value; + p->pData[p->iEmpty] = Value; + if ( ( ++p->iEmpty ) == p->nCap ) + { + p->iEmpty = 0; + p->iFirst = 0; + } +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline int xSAT_BQueuePop( xSAT_BQueue_t * p ) +{ + assert( p->nSize >= 1 ); + int RetValue = p->pData[p->iFirst]; + p->nSum -= RetValue; + p->iFirst = ( p->iFirst + 1 ) % p->nCap; + p->nSize--; + return RetValue; +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline uint32_t xSAT_BQueueAvg( xSAT_BQueue_t * p ) +{ + return ( uint32_t )( p->nSum / ( ( uint64_t ) p->nSize ) ); +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline int xSAT_BQueueIsValid( xSAT_BQueue_t * p ) +{ + return ( p->nCap == p->nSize ); +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline void xSAT_BQueueClean( xSAT_BQueue_t * p ) +{ + p->iFirst = 0; + p->iEmpty = 0; + p->nSize = 0; + p->nSum = 0; +} + +ABC_NAMESPACE_HEADER_END + +#endif diff --git a/src/sat/xsat/xsatClause.h b/src/sat/xsat/xsatClause.h new file mode 100644 index 00000000..39f0a0c8 --- /dev/null +++ b/src/sat/xsat/xsatClause.h @@ -0,0 +1,109 @@ +/**CFile**************************************************************** + + FileName [xsatClause.h] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [xSAT - A SAT solver written in C. + Read the license file for more info.] + + Synopsis [Clause data type definition.] + + Author [Bruno Schmitt <boschmitt@inf.ufrgs.br>] + + Affiliation [UC Berkeley / UFRGS] + + Date [Ver. 1.0. Started - November 10, 2016.] + + Revision [] + +***********************************************************************/ +#ifndef ABC__sat__xSAT__xsatClause_h +#define ABC__sat__xSAT__xsatClause_h + +//////////////////////////////////////////////////////////////////////// +/// INCLUDES /// +//////////////////////////////////////////////////////////////////////// +#include "misc/util/abc_global.h" + +ABC_NAMESPACE_HEADER_START + +//////////////////////////////////////////////////////////////////////// +/// STRUCTURE DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// +typedef struct xSAT_Clause_t_ xSAT_Clause_t; +struct xSAT_Clause_t_ +{ + unsigned fLearnt : 1; + unsigned fMark : 1; + unsigned fReallocd : 1; + unsigned fCanBeDel : 1; + unsigned nLBD : 28; + unsigned nSize; + union { + int Lit; + unsigned Act; + } pData[0]; +}; + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static int xSAT_ClauseCompare( const void * p1, const void * p2 ) +{ + xSAT_Clause_t * pC1 = ( xSAT_Clause_t * ) p1; + xSAT_Clause_t * pC2 = ( xSAT_Clause_t * ) p2; + + if ( pC1->nSize > 2 && pC2->nSize == 2 ) + return 1; + if ( pC1->nSize == 2 && pC2->nSize > 2 ) + return 0; + if ( pC1->nSize == 2 && pC2->nSize == 2 ) + return 0; + + if ( pC1->nLBD > pC2->nLBD ) + return 1; + if ( pC1->nLBD < pC2->nLBD ) + return 0; + + return pC1->pData[pC1->nSize].Act < pC2->pData[pC2->nSize].Act; +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static void xSAT_ClausePrint( xSAT_Clause_t * pCla ) +{ + int i; + + printf("{ "); + for ( i = 0; i < pCla->nSize; i++ ) + printf("%d ", pCla->pData[i].Lit ); + printf("}\n"); +} + +ABC_NAMESPACE_HEADER_END + +#endif +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// diff --git a/src/sat/xsat/xsatCnfReader.c b/src/sat/xsat/xsatCnfReader.c new file mode 100644 index 00000000..d23e8a0a --- /dev/null +++ b/src/sat/xsat/xsatCnfReader.c @@ -0,0 +1,236 @@ +/**CFile**************************************************************** + + FileName [xsatCnfReader.h] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [xSAT - A SAT solver written in C. + Read the license file for more info.] + + Synopsis [CNF DIMACS file format parser.] + + Author [Bruno Schmitt <boschmitt@inf.ufrgs.br>] + + Affiliation [UC Berkeley / UFRGS] + + Date [Ver. 1.0. Started - November 10, 2016.] + + Revision [] + +***********************************************************************/ + +//////////////////////////////////////////////////////////////////////// +/// INCLUDES /// +//////////////////////////////////////////////////////////////////////// +#include <ctype.h> + +#include "misc/util/abc_global.h" +#include "misc/vec/vecInt.h" + +#include "xsatSolver.h" + +ABC_NAMESPACE_IMPL_START + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [Read the file into the internal buffer.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +char * xSAT_FileRead( FILE * pFile ) +{ + int nFileSize; + char * pBuffer; + int RetValue; + // get the file size, in bytes + fseek( pFile, 0, SEEK_END ); + nFileSize = ftell( pFile ); + // move the file current reading position to the beginning + rewind( pFile ); + // load the contents of the file into memory + pBuffer = ABC_ALLOC( char, nFileSize + 3 ); + RetValue = fread( pBuffer, nFileSize, 1, pFile ); + // terminate the string with '\0' + pBuffer[ nFileSize + 0] = '\n'; + pBuffer[ nFileSize + 1] = '\0'; + return pBuffer; +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static void skipLine( char ** pIn ) +{ + while ( 1 ) + { + if (**pIn == 0) + return; + if (**pIn == '\n') + { + (*pIn)++; + return; + } + (*pIn)++; + } +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static int xSAT_ReadInt( char ** pIn ) +{ + int val = 0; + int neg = 0; + + for(; isspace(**pIn); (*pIn)++); + if ( **pIn == '-' ) + neg = 1, + (*pIn)++; + else if ( **pIn == '+' ) + (*pIn)++; + if ( !isdigit(**pIn) ) + fprintf(stderr, "PARSE ERROR! Unexpected char: %c\n", **pIn), + exit(1); + while ( isdigit(**pIn) ) + val = val*10 + (**pIn - '0'), + (*pIn)++; + return neg ? -val : val; +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static void xSAT_ReadClause( char ** pIn, xSAT_Solver_t * p, Vec_Int_t * vLits ) +{ + int token, var, sign; + + Vec_IntClear( vLits ); + while ( 1 ) + { + token = xSAT_ReadInt( pIn ); + if ( token == 0 ) + break; + var = abs(token) - 1; + sign = (token > 0); + Vec_IntPush( vLits, xSAT_Var2Lit( var, !sign ) ); + } +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static int xSAT_ParseDimacs( char * pText, xSAT_Solver_t ** pS ) +{ + xSAT_Solver_t * p = NULL; + Vec_Int_t * vLits = NULL; + char * pIn = pText; + int nVars, nClas; + while ( 1 ) + { + for(; isspace(*pIn); pIn++); + if ( *pIn == 0 ) + break; + else if ( *pIn == 'c' ) + skipLine( &pIn ); + else if ( *pIn == 'p' ) + { + pIn++; + for(; isspace(*pIn); pIn++); + for(; !isspace(*pIn); pIn++); + + nVars = xSAT_ReadInt( &pIn ); + nClas = xSAT_ReadInt( &pIn ); + skipLine( &pIn ); + + /* start the solver */ + p = xSAT_SolverCreate(); + /* allocate the vector */ + vLits = Vec_IntAlloc( nVars ); + } + else + { + if ( p == NULL ) + { + printf( "There is no parameter line.\n" ); + exit(1); + } + xSAT_ReadClause( &pIn, p, vLits ); + if ( !xSAT_SolverAddClause( p, vLits ) ) + { + Vec_IntPrint(vLits); + return 0; + } + } + } + Vec_IntFree( vLits ); + *pS = p; + return xSAT_SolverSimplify( p ); +} + +/**Function************************************************************* + + Synopsis [Starts the solver and reads the DIMAC file.] + + Description [Returns FALSE upon immediate conflict.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int xSAT_SolverParseDimacs( FILE * pFile, xSAT_Solver_t ** p ) +{ + char * pText; + int Value; + pText = xSAT_FileRead( pFile ); + Value = xSAT_ParseDimacs( pText, p ); + ABC_FREE( pText ); + return Value; +} + +ABC_NAMESPACE_IMPL_END + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// diff --git a/src/sat/xsat/xsatHeap.h b/src/sat/xsat/xsatHeap.h new file mode 100644 index 00000000..2e873e59 --- /dev/null +++ b/src/sat/xsat/xsatHeap.h @@ -0,0 +1,330 @@ +/**CFile**************************************************************** + + FileName [xsatHeap.h] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [xSAT - A SAT solver written in C. + Read the license file for more info.] + + Synopsis [Heap implementation.] + + Author [Bruno Schmitt <boschmitt@inf.ufrgs.br>] + + Affiliation [UC Berkeley / UFRGS] + + Date [Ver. 1.0. Started - November 10, 2016.] + + Revision [] + +***********************************************************************/ +#ifndef ABC__sat__xSAT__xsatHeap_h +#define ABC__sat__xSAT__xsatHeap_h + +#include "misc/util/abc_global.h" +#include "misc/vec/vecInt.h" + +ABC_NAMESPACE_HEADER_START + +//////////////////////////////////////////////////////////////////////// +/// STRUCTURE DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// +typedef struct xSAT_Heap_t_ xSAT_Heap_t; +struct xSAT_Heap_t_ +{ + Vec_Int_t * vActivity; + Vec_Int_t * vIndices; + Vec_Int_t * vHeap; +}; + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +inline int xSAT_HeapSize( xSAT_Heap_t * h ) +{ + return Vec_IntSize( h->vHeap ); +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +inline int xSAT_HeapInHeap( xSAT_Heap_t * h, int Var ) +{ + return ( Var < Vec_IntSize( h->vIndices ) ) && ( Vec_IntEntry( h->vIndices, Var ) >= 0 ); +} + +static inline int Left ( int i ) { return 2 * i + 1; } +static inline int Right ( int i ) { return ( i + 1 ) * 2; } +static inline int Parent( int i ) { return ( i - 1 ) >> 1; } +static inline int Compare( xSAT_Heap_t * p, int x, int y ) +{ + return ( unsigned )Vec_IntEntry( p->vActivity, x ) > ( unsigned )Vec_IntEntry( p->vActivity, y ); +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline void xSAT_HeapPercolateUp( xSAT_Heap_t * h, int i ) +{ + int x = Vec_IntEntry( h->vHeap, i ); + int p = Parent( i ); + + while ( i != 0 && Compare( h, x, Vec_IntEntry( h->vHeap, p ) ) ) + { + Vec_IntWriteEntry( h->vHeap, i, Vec_IntEntry( h->vHeap, p ) ); + Vec_IntWriteEntry( h->vIndices, Vec_IntEntry( h->vHeap, p ), i ); + i = p; + p = Parent(p); + } + Vec_IntWriteEntry( h->vHeap, i, x ); + Vec_IntWriteEntry( h->vIndices, x, i ); +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline void xSAT_HeapPercolateDown( xSAT_Heap_t * h, int i ) +{ + int x = Vec_IntEntry( h->vHeap, i ); + + while ( Left( i ) < Vec_IntSize( h->vHeap ) ) + { + int child = Right( i ) < Vec_IntSize( h->vHeap ) && + Compare( h, Vec_IntEntry( h->vHeap, Right( i ) ), Vec_IntEntry( h->vHeap, Left( i ) ) ) ? + Right( i ) : Left( i ); + + if ( !Compare( h, Vec_IntEntry( h->vHeap, child ), x ) ) + break; + + Vec_IntWriteEntry( h->vHeap, i, Vec_IntEntry( h->vHeap, child ) ); + Vec_IntWriteEntry( h->vIndices, Vec_IntEntry( h->vHeap, i ), i ); + i = child; + } + Vec_IntWriteEntry( h->vHeap, i, x ); + Vec_IntWriteEntry( h->vIndices, x, i ); +} + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline xSAT_Heap_t * xSAT_HeapAlloc( Vec_Int_t * vActivity ) +{ + xSAT_Heap_t * p = ABC_ALLOC( xSAT_Heap_t, 1 ); + p->vActivity = vActivity; + p->vIndices = Vec_IntAlloc( 0 ); + p->vHeap = Vec_IntAlloc( 0 ); + + return p; +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline void xSAT_HeapFree( xSAT_Heap_t * p ) +{ + Vec_IntFree( p->vIndices ); + Vec_IntFree( p->vHeap ); + ABC_FREE( p ); +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline void xSAT_HeapIncrease( xSAT_Heap_t * h, int e ) +{ + assert( xSAT_HeapInHeap( h, e ) ); + xSAT_HeapPercolateDown( h, Vec_IntEntry( h->vIndices, e ) ); +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline void xSAT_HeapDecrease( xSAT_Heap_t * p, int e ) +{ + assert( xSAT_HeapInHeap( p, e ) ); + xSAT_HeapPercolateUp( p , Vec_IntEntry( p->vIndices, e ) ); +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline void xSAT_HeapInsert( xSAT_Heap_t * p, int n ) +{ + Vec_IntFillExtra( p->vIndices, n + 1, -1); + assert( !xSAT_HeapInHeap( p, n ) ); + + Vec_IntWriteEntry( p->vIndices, n, Vec_IntSize( p->vHeap ) ); + Vec_IntPush( p->vHeap, n ); + xSAT_HeapPercolateUp( p, Vec_IntEntry( p->vIndices, n ) ); +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline void xSAT_HeapUpdate( xSAT_Heap_t * p, int i ) +{ + if ( !xSAT_HeapInHeap( p, i ) ) + xSAT_HeapInsert( p, i ); + else + { + xSAT_HeapPercolateUp( p, Vec_IntEntry( p->vIndices, i ) ); + xSAT_HeapPercolateDown( p, Vec_IntEntry( p->vIndices, i ) ); + } +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline void xSAT_HeapBuild( xSAT_Heap_t * p, Vec_Int_t * Vars ) +{ + int i, Var; + + Vec_IntForEachEntry( p->vHeap, Var, i ) + Vec_IntWriteEntry( p->vIndices, Var, -1 ); + Vec_IntClear( p->vHeap ); + + Vec_IntForEachEntry( Vars, Var, i ) + { + Vec_IntWriteEntry( p->vIndices, Var, i ); + Vec_IntPush( p->vHeap, Var ); + } + + for ( ( i = Vec_IntSize( p->vHeap ) / 2 - 1 ); i >= 0; i-- ) + xSAT_HeapPercolateDown( p, i ); +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline void xSAT_HeapClear( xSAT_Heap_t * p ) +{ + Vec_IntFill( p->vIndices, Vec_IntSize( p->vIndices ), -1 ); + Vec_IntClear( p->vHeap ); +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline int xSAT_HeapRemoveMin( xSAT_Heap_t * p ) +{ + int x = Vec_IntEntry( p->vHeap, 0 ); + Vec_IntWriteEntry( p->vHeap, 0, Vec_IntEntryLast( p->vHeap ) ); + Vec_IntWriteEntry( p->vIndices, Vec_IntEntry( p->vHeap, 0), 0 ); + Vec_IntWriteEntry( p->vIndices, x, -1 ); + Vec_IntPop( p->vHeap ); + if ( Vec_IntSize( p->vHeap ) > 1 ) + xSAT_HeapPercolateDown( p, 0 ); + return x; +} + +ABC_NAMESPACE_HEADER_END + +#endif diff --git a/src/sat/xsat/xsatMemory.h b/src/sat/xsat/xsatMemory.h new file mode 100644 index 00000000..3a961b97 --- /dev/null +++ b/src/sat/xsat/xsatMemory.h @@ -0,0 +1,225 @@ +/**CFile**************************************************************** + + FileName [xsatMemory.h] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [xSAT - A SAT solver written in C. + Read the license file for more info.] + + Synopsis [Memory management implementation.] + + Author [Bruno Schmitt <boschmitt@inf.ufrgs.br>] + + Affiliation [UC Berkeley / UFRGS] + + Date [Ver. 1.0. Started - November 10, 2016.] + + Revision [] + +***********************************************************************/ +#ifndef ABC__sat__xSAT__xsatMemory_h +#define ABC__sat__xSAT__xsatMemory_h + +//////////////////////////////////////////////////////////////////////// +/// INCLUDES /// +//////////////////////////////////////////////////////////////////////// +#include "misc/util/abc_global.h" + +#include "xsatClause.h" + +ABC_NAMESPACE_HEADER_START + +//////////////////////////////////////////////////////////////////////// +/// STRUCTURE DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// +typedef struct xSAT_Mem_t_ xSAT_Mem_t; +struct xSAT_Mem_t_ +{ + uint32_t nSize; + uint32_t nCap; + uint32_t nWasted; + uint32_t * pData; +}; + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline xSAT_Clause_t * xSAT_MemClauseHand( xSAT_Mem_t * p, int h ) +{ + return h != UINT32_MAX ? ( xSAT_Clause_t * )( p->pData + h ) : NULL; +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline void xSAT_MemGrow( xSAT_Mem_t * p, uint32_t nCap ) +{ + if ( p->nCap >= nCap ) + return; + + uint32_t nPrevCap = p->nCap; + while (p->nCap < nCap) + { + uint32_t delta = ((p->nCap >> 1) + (p->nCap >> 3) + 2) & ~1; + p->nCap += delta; + assert(p->nCap >= nPrevCap); + } + + assert(p->nCap > 0); + p->pData = ABC_REALLOC(uint32_t, p->pData, p->nCap); +} + +/**Function************************************************************* + + Synopsis [Allocating vector.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline xSAT_Mem_t * xSAT_MemAlloc( int nCap ) +{ + xSAT_Mem_t * p; + p = ABC_CALLOC( xSAT_Mem_t, 1 ); + if (nCap <= 0) + nCap = 1024*1024; + + xSAT_MemGrow(p, nCap); + return p; +} + +/**Function************************************************************* + + Synopsis [Resetting vector.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline void xSAT_MemRestart( xSAT_Mem_t * p ) +{ + p->nSize = 0; + p->nWasted = 0; +} + +/**Function************************************************************* + + Synopsis [Freeing vector.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline void xSAT_MemFree( xSAT_Mem_t * p ) +{ + ABC_FREE( p->pData ); + ABC_FREE( p ); +} + +/**Function************************************************************* + + Synopsis [Creates new clause.] + + Description [The resulting clause is fully initialized.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline uint32_t xSAT_MemAppend( xSAT_Mem_t * p, int nSize ) +{ + assert(nSize > 0); + xSAT_MemGrow(p, p->nSize + nSize); + + uint32_t nPrevSize = p->nSize; + p->nSize += nSize; + assert(p->nSize > nPrevSize); + + return nPrevSize; +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline uint32_t xSAT_MemCRef( xSAT_Mem_t * p, uint32_t * pC ) +{ + return ( uint32_t )( pC - &(p->pData[0]) ); +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline uint32_t xSAT_MemCap( xSAT_Mem_t * p ) +{ + return p->nCap; +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline uint32_t xSAT_MemWastedCap( xSAT_Mem_t * p ) +{ + return p->nWasted; +} + +ABC_NAMESPACE_HEADER_END + +#endif + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// diff --git a/src/sat/xsat/xsatSolver.c b/src/sat/xsat/xsatSolver.c new file mode 100644 index 00000000..d6968a2d --- /dev/null +++ b/src/sat/xsat/xsatSolver.c @@ -0,0 +1,995 @@ +/**CFile**************************************************************** + + FileName [xsatSolver.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [xSAT - A SAT solver written in C. + Read the license file for more info.] + + Synopsis [Solver internal functions implementation.] + + Author [Bruno Schmitt <boschmitt@inf.ufrgs.br>] + + Affiliation [UC Berkeley / UFRGS] + + Date [Ver. 1.0. Started - November 10, 2016.] + + Revision [] + +***********************************************************************/ +//////////////////////////////////////////////////////////////////////// +/// INCLUDES /// +//////////////////////////////////////////////////////////////////////// +#include <stdio.h> +#include <assert.h> +#include <string.h> +#include <math.h> + +#include "xsatHeap.h" +#include "xsatSolver.h" +#include "xsatUtils.h" + +ABC_NAMESPACE_IMPL_START + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline int xSAT_SolverDecide( xSAT_Solver_t* s ) +{ + int NextVar = VarUndef; + + while ( NextVar == VarUndef || Vec_StrEntry( s->vAssigns, NextVar ) != VarX ) + { + if ( xSAT_HeapSize( s->hOrder ) == 0 ) + { + NextVar = VarUndef; + break; + } + else + NextVar = xSAT_HeapRemoveMin( s->hOrder ); + } + return NextVar; +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void xSAT_SolverRebuildOrderHeap( xSAT_Solver_t* s ) +{ + Vec_Int_t * vTemp = Vec_IntAlloc( Vec_StrSize( s->vAssigns ) ); + int Var; + + for ( Var = 0; Var < Vec_StrSize( s->vAssigns ); Var++ ) + if ( Vec_StrEntry( s->vAssigns, Var ) == VarX ) + Vec_IntPush( vTemp, Var ); + + xSAT_HeapBuild( s->hOrder, vTemp ); + Vec_IntFree( vTemp ); +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline void xSAT_SolverVarActRescale( xSAT_Solver_t * s ) +{ + unsigned * pActivity = (unsigned *) Vec_IntArray( s->vActivity ); + + for ( int i = 0; i < Vec_IntSize( s->vActivity ); i++ ) + pActivity[i] >>= 19; + + s->nVarActInc >>= 19; + s->nVarActInc = Abc_MaxInt( s->nVarActInc, (1 << 5) ); +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline void xSAT_SolverVarActBump( xSAT_Solver_t* s, int Var ) +{ + unsigned * pActivity = (unsigned *) Vec_IntArray( s->vActivity ); + + pActivity[Var] += s->nVarActInc; + if ( pActivity[Var] & 0x80000000 ) + xSAT_SolverVarActRescale( s ); + + if ( xSAT_HeapInHeap( s->hOrder, Var ) ) + xSAT_HeapDecrease( s->hOrder, Var ); +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline void xSAT_SolverVarActDecay( xSAT_Solver_t * s ) +{ + s->nVarActInc += ( s->nVarActInc >> 4 ); +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline void xSAT_SolverClaActRescale( xSAT_Solver_t * s ) +{ + xSAT_Clause_t * pC; + int i, CRef; + + Vec_IntForEachEntry( s->vLearnts, CRef, i ) + { + pC = xSAT_SolverReadClause( s, (uint32_t) CRef ); + pC->pData[pC->nSize].Act >>= 14; + } + s->nClaActInc >>= 14; + s->nClaActInc = Abc_MaxInt( s->nClaActInc, ( 1 << 10 ) ); +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline void xSAT_SolverClaActBump( xSAT_Solver_t* s, xSAT_Clause_t * pCla ) +{ + pCla->pData[pCla->nSize].Act += s->nClaActInc; + if ( pCla->pData[pCla->nSize].Act & 0x80000000 ) + xSAT_SolverClaActRescale( s ); +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline void xSAT_SolverClaActDecay( xSAT_Solver_t * s ) +{ + s->nClaActInc += ( s->nClaActInc >> 10 ); +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline int xSAT_SolverClaCalcLBD( xSAT_Solver_t * s, xSAT_Clause_t * pCla ) +{ + int nLBD = 0; + + s->nStamp++; + for ( int i = 0; i < pCla->nSize; i++ ) + { + int Level = Vec_IntEntry( s->vLevels, xSAT_Lit2Var( pCla->pData[i].Lit ) ); + if ( (unsigned) Vec_IntEntry( s->vStamp, Level ) != s->nStamp ) + { + Vec_IntWriteEntry( s->vStamp, Level, (int) s->nStamp ); + nLBD++; + } + } + return nLBD; +} + +static inline int xSAT_SolverClaCalcLBD2( xSAT_Solver_t * s, Vec_Int_t * vLits ) +{ + int nLBD = 0; + + s->nStamp++; + for ( int i = 0; i < Vec_IntSize( vLits ); i++ ) + { + int Level = Vec_IntEntry( s->vLevels, xSAT_Lit2Var( Vec_IntEntry( vLits, i ) ) ); + if ( (unsigned) Vec_IntEntry( s->vStamp, Level ) != s->nStamp ) + { + Vec_IntWriteEntry( s->vStamp, Level, (int) s->nStamp ); + nLBD++; + } + } + return nLBD; +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +uint32_t xSAT_SolverClaNew( xSAT_Solver_t * s, Vec_Int_t * vLits , int fLearnt ) +{ + assert( Vec_IntSize( vLits ) > 1); + assert( fLearnt == 0 || fLearnt == 1 ); + + uint32_t CRef; + xSAT_Clause_t * pCla; + xSAT_Watcher_t w1; + xSAT_Watcher_t w2; + + uint32_t nWords = 3 + fLearnt + Vec_IntSize( vLits ); + CRef = xSAT_MemAppend( s->pMemory, nWords ); + pCla = xSAT_SolverReadClause( s, CRef ); + pCla->fLearnt = fLearnt; + pCla->fMark = 0; + pCla->fReallocd = 0; + pCla->fCanBeDel = fLearnt; + pCla->nSize = Vec_IntSize( vLits ); + memcpy( &( pCla->pData[0].Lit ), Vec_IntArray( vLits ), sizeof( int ) * Vec_IntSize( vLits ) ); + + if ( fLearnt ) + { + Vec_IntPush( s->vLearnts, CRef ); + pCla->nLBD = xSAT_SolverClaCalcLBD2( s, vLits ); + pCla->pData[pCla->nSize].Act = 0; + s->Stats.nLearntLits += Vec_IntSize( vLits ); + xSAT_SolverClaActBump(s, pCla); + } + else + { + Vec_IntPush( s->vClauses, CRef ); + s->Stats.nClauseLits += Vec_IntSize( vLits ); + } + + w1.CRef = CRef; + w2.CRef = CRef; + w1.Blocker = pCla->pData[1].Lit; + w2.Blocker = pCla->pData[0].Lit; + + if ( Vec_IntSize( vLits ) == 2 ) + { + xSAT_WatchListPush( xSAT_VecWatchListEntry( s->vBinWatches, xSAT_NegLit( pCla->pData[0].Lit ) ), w1 ); + xSAT_WatchListPush( xSAT_VecWatchListEntry( s->vBinWatches, xSAT_NegLit( pCla->pData[1].Lit ) ), w2 ); + } + else + { + xSAT_WatchListPush( xSAT_VecWatchListEntry( s->vWatches, xSAT_NegLit( pCla->pData[0].Lit ) ), w1 ); + xSAT_WatchListPush( xSAT_VecWatchListEntry( s->vWatches, xSAT_NegLit( pCla->pData[1].Lit ) ), w2 ); + } + return CRef; +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int xSAT_SolverEnqueue( xSAT_Solver_t* s, int Lit, uint32_t Reason ) +{ + int Var = xSAT_Lit2Var( Lit ); + + Vec_StrWriteEntry( s->vAssigns, Var, xSAT_LitSign( Lit ) ); + Vec_IntWriteEntry( s->vLevels, Var, xSAT_SolverDecisionLevel( s ) ); + Vec_IntWriteEntry( s->vReasons, Var, (int) Reason ); + Vec_IntPush( s->vTrail, Lit ); + + return true; +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline void xSAT_SolverNewDecision( xSAT_Solver_t* s, int Lit ) +{ + assert( Vec_StrEntry( s->vAssigns, xSAT_Lit2Var( Lit ) ) == VarX ); + s->Stats.nDecisions++; + Vec_IntPush( s->vTrailLim, Vec_IntSize( s->vTrail ) ); + xSAT_SolverEnqueue( s, Lit, CRefUndef ); +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void xSAT_SolverCancelUntil( xSAT_Solver_t * s, int Level ) +{ + if ( xSAT_SolverDecisionLevel( s ) <= Level ) + return; + + for ( int c = Vec_IntSize( s->vTrail ) - 1; c >= Vec_IntEntry( s->vTrailLim, Level ); c-- ) + { + int Var = xSAT_Lit2Var( Vec_IntEntry( s->vTrail, c ) ); + + Vec_StrWriteEntry( s->vAssigns, Var, VarX ); + Vec_IntWriteEntry( s->vReasons, Var, ( int ) CRefUndef ); + Vec_StrWriteEntry( s->vPolarity, Var, xSAT_LitSign( Vec_IntEntry( s->vTrail, c ) ) ); + + if ( !xSAT_HeapInHeap( s->hOrder, Var ) ) + xSAT_HeapInsert( s->hOrder, Var ); + } + + s->iQhead = Vec_IntEntry( s->vTrailLim, Level ); + Vec_IntShrink( s->vTrail, Vec_IntEntry( s->vTrailLim, Level ) ); + Vec_IntShrink( s->vTrailLim, Level ); +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static int xSAT_SolverIsLitRemovable( xSAT_Solver_t* s, int Lit, int MinLevel ) +{ + int top = Vec_IntSize( s->vTagged ); + + assert( (uint32_t) Vec_IntEntry( s->vReasons, xSAT_Lit2Var( Lit ) ) != CRefUndef ); + Vec_IntClear( s->vStack ); + Vec_IntPush( s->vStack, xSAT_Lit2Var( Lit ) ); + + while ( Vec_IntSize( s->vStack ) ) + { + int v = Vec_IntPop( s->vStack ); + assert( (uint32_t) Vec_IntEntry( s->vReasons, v ) != CRefUndef); + xSAT_Clause_t* c = xSAT_SolverReadClause(s, ( uint32_t ) Vec_IntEntry( s->vReasons, v ) ); + int* Lits = &( c->pData[0].Lit ); + int i; + + if( c->nSize == 2 && Vec_StrEntry( s->vAssigns, xSAT_Lit2Var( Lits[0] ) ) == xSAT_LitSign( xSAT_NegLit( Lits[0] ) ) ) + { + assert( Vec_StrEntry( s->vAssigns, xSAT_Lit2Var( Lits[1] ) ) == xSAT_LitSign( ( Lits[1] ) ) ); + ABC_SWAP( int, Lits[0], Lits[1] ); + } + + for (i = 1; i < c->nSize; i++) + { + int v = xSAT_Lit2Var( Lits[i] ); + if ( !Vec_StrEntry( s->vSeen, v ) && Vec_IntEntry( s->vLevels, v ) ) + { + if ( (uint32_t) Vec_IntEntry( s->vReasons, v ) != CRefUndef && ((1 << (Vec_IntEntry( s->vLevels, v ) & 31)) & MinLevel)) + { + Vec_IntPush( s->vStack, v ); + Vec_IntPush( s->vTagged, Lits[i] ); + Vec_StrWriteEntry( s->vSeen, v, 1 ); + } + else + { + int Lit; + Vec_IntForEachEntryStart( s->vTagged, Lit, i, top ) + Vec_StrWriteEntry( s->vSeen, xSAT_Lit2Var(Lit), 0 ); + Vec_IntShrink( s->vTagged, top ); + return 0; + } + } + } + } + return 1; +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static void xSAT_SolverClaMinimisation( xSAT_Solver_t * s, Vec_Int_t * vLits ) +{ + int * pLits = Vec_IntArray( vLits ); + int MinLevel = 0; + int i, j; + + for ( i = 1; i < Vec_IntSize( vLits ); i++ ) + { + int Level = Vec_IntEntry( s->vLevels, xSAT_Lit2Var( pLits[i] ) ); + MinLevel |= 1 << ( Level & 31 ); + } + + /* Remove reduntant literals */ + Vec_IntAppend( s->vTagged, vLits ); + for ( i = j = 1; i < Vec_IntSize( vLits ); i++ ) + if ( (uint32_t) Vec_IntEntry( s->vReasons, xSAT_Lit2Var( pLits[i] ) ) == CRefUndef || !xSAT_SolverIsLitRemovable( s, pLits[i], MinLevel ) ) + pLits[j++] = pLits[i]; + Vec_IntShrink( vLits, j ); + + /* Binary Resolution */ + if( Vec_IntSize( vLits ) <= 30 && xSAT_SolverClaCalcLBD2( s, vLits ) <= 6 ) + { + int Lit; + int FlaseLit = xSAT_NegLit( pLits[0] ); + + s->nStamp++; + Vec_IntForEachEntry( vLits, Lit, i ) + Vec_IntWriteEntry( s->vStamp, xSAT_Lit2Var( Lit ), s->nStamp ); + + xSAT_WatchList_t * ws = xSAT_VecWatchListEntry( s->vBinWatches, FlaseLit ); + xSAT_Watcher_t * begin = xSAT_WatchListArray( ws ); + xSAT_Watcher_t * end = begin + xSAT_WatchListSize( ws ); + xSAT_Watcher_t * pWatcher; + + int nb = 0; + for ( pWatcher = begin; pWatcher < end; pWatcher++ ) + { + int ImpLit = pWatcher->Blocker; + + if ( Vec_IntEntry( s->vStamp, xSAT_Lit2Var( ImpLit ) ) == s->nStamp && Vec_StrEntry( s->vAssigns, xSAT_Lit2Var( ImpLit ) ) == xSAT_LitSign( ImpLit ) ) + { + nb++; + Vec_IntWriteEntry( s->vStamp, xSAT_Lit2Var( ImpLit ), s->nStamp - 1 ); + } + } + + int l = Vec_IntSize( vLits ) - 1; + if ( nb > 0 ) + { + for ( i = 1; i < Vec_IntSize( vLits ) - nb; i++ ) + if ( Vec_IntEntry( s->vStamp, xSAT_Lit2Var( pLits[i] ) ) != s->nStamp ) + { + int TempLit = pLits[l]; + pLits[l] = pLits[i]; + pLits[i] = TempLit; + i--; l--; + } + + Vec_IntShrink( vLits, Vec_IntSize( vLits ) - nb ); + } + } +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static void xSAT_SolverAnalyze( xSAT_Solver_t* s, uint32_t ConfCRef, Vec_Int_t * vLearnt, int * OutBtLevel, unsigned * nLBD ) +{ + int* trail = Vec_IntArray( s->vTrail ); + int Count = 0; + int p = LitUndef; + int Idx = Vec_IntSize( s->vTrail ) - 1; + int* Lits; + int i, j; + + Vec_IntPush( vLearnt, LitUndef ); + do + { + assert( ConfCRef != CRefUndef ); + xSAT_Clause_t * c = xSAT_SolverReadClause(s, ConfCRef); + Lits = &( c->pData[0].Lit ); + + if( p != LitUndef && c->nSize == 2 && Vec_StrEntry( s->vAssigns, xSAT_Lit2Var(Lits[0])) == xSAT_LitSign( xSAT_NegLit( Lits[0] ) ) ) + { + assert( Vec_StrEntry( s->vAssigns, xSAT_Lit2Var( Lits[1] ) ) == xSAT_LitSign( ( Lits[1] ) ) ); + ABC_SWAP( int, Lits[0], Lits[1] ); + } + + if ( c->fLearnt ) + xSAT_SolverClaActBump( s, c ); + + if ( c->fLearnt && c->nLBD > 2 ) + { + unsigned int nblevels = xSAT_SolverClaCalcLBD(s, c); + if ( nblevels + 1 < c->nLBD ) + { + if (c->nLBD <= s->Config.nLBDFrozenClause) + c->fCanBeDel = 0; + c->nLBD = nblevels; + } + } + + for ( j = ( p == LitUndef ? 0 : 1 ); j < c->nSize; j++ ) + { + int Var = xSAT_Lit2Var( Lits[j] ); + + if ( Vec_StrEntry( s->vSeen, Var ) == 0 && Vec_IntEntry( s->vLevels, Var ) > 0 ) + { + Vec_StrWriteEntry( s->vSeen, Var, 1 ); + xSAT_SolverVarActBump( s, Var ); + if ( Vec_IntEntry( s->vLevels, Var ) >= xSAT_SolverDecisionLevel( s ) ) + { + Count++; + if ( Vec_IntEntry( s->vReasons, Var ) != CRefUndef && xSAT_SolverReadClause( s, Vec_IntEntry( s->vReasons, Var ) )->fLearnt ) + Vec_IntPush( s->vLastDLevel, Var ); + } + else + Vec_IntPush( vLearnt, Lits[j] ); + } + } + + while ( !Vec_StrEntry( s->vSeen, xSAT_Lit2Var( trail[Idx--] ) ) ); + + // Next clause to look at + p = trail[Idx+1]; + ConfCRef = (uint32_t) Vec_IntEntry( s->vReasons, xSAT_Lit2Var( p ) ); + Vec_StrWriteEntry( s->vSeen, xSAT_Lit2Var( p ), 0 ); + Count--; + + } while ( Count > 0 ); + + Vec_IntArray( vLearnt )[0] = xSAT_NegLit( p ); + + xSAT_SolverClaMinimisation( s, vLearnt ); + + // Find the backtrack level + Lits = Vec_IntArray( vLearnt ); + if ( Vec_IntSize( vLearnt ) == 1 ) + *OutBtLevel = 0; + else + { + int iMax = 1; + int Max = Vec_IntEntry( s->vLevels, xSAT_Lit2Var( Lits[1] ) ); + int Tmp; + + for (i = 2; i < Vec_IntSize( vLearnt ); i++) + if ( Vec_IntEntry( s->vLevels, xSAT_Lit2Var( Lits[i]) ) > Max) + { + Max = Vec_IntEntry( s->vLevels, xSAT_Lit2Var( Lits[i]) ); + iMax = i; + } + + Tmp = Lits[1]; + Lits[1] = Lits[iMax]; + Lits[iMax] = Tmp; + *OutBtLevel = Vec_IntEntry( s->vLevels, xSAT_Lit2Var( Lits[1] ) ); + } + + *nLBD = xSAT_SolverClaCalcLBD2( s, vLearnt ); + if ( Vec_IntSize( s->vLastDLevel ) > 0 ) + { + int Var; + Vec_IntForEachEntry( s->vLastDLevel, Var, i ) + { + if ( xSAT_SolverReadClause( s, Vec_IntEntry( s->vReasons, Var ) )->nLBD < *nLBD ) + xSAT_SolverVarActBump( s, Var ); + } + + Vec_IntClear( s->vLastDLevel ); + } + + int Lit; + Vec_IntForEachEntry( s->vTagged, Lit, i ) + Vec_StrWriteEntry( s->vSeen, xSAT_Lit2Var( Lit ), 0 ); + Vec_IntClear( s->vTagged ); +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +uint32_t xSAT_SolverPropagate( xSAT_Solver_t* s ) +{ + uint32_t hConfl = CRefUndef; + int * Lits; + int NegLit; + int nProp = 0; + + while ( s->iQhead < Vec_IntSize( s->vTrail ) ) + { + int p = Vec_IntEntry( s->vTrail, s->iQhead++ ); + + xSAT_WatchList_t* ws = xSAT_VecWatchListEntry( s->vBinWatches, p ); + xSAT_Watcher_t* begin = xSAT_WatchListArray( ws ); + xSAT_Watcher_t* end = begin + xSAT_WatchListSize( ws ); + xSAT_Watcher_t *i, *j; + + nProp++; + for (i = begin; i < end; i++) + { + if ( Vec_StrEntry( s->vAssigns, xSAT_Lit2Var(i->Blocker)) == xSAT_LitSign(xSAT_NegLit(i->Blocker))) + { + return i->CRef; + } + else if ( Vec_StrEntry( s->vAssigns, xSAT_Lit2Var(i->Blocker)) == VarX) + xSAT_SolverEnqueue(s, i->Blocker, i->CRef); + } + + + ws = xSAT_VecWatchListEntry( s->vWatches, p); + begin = xSAT_WatchListArray( ws ); + end = begin + xSAT_WatchListSize( ws ); + + for ( i = j = begin; i < end; ) + { + if ( Vec_StrEntry( s->vAssigns, xSAT_Lit2Var( i->Blocker ) ) == xSAT_LitSign( i->Blocker ) ) + { + *j++ = *i++; + continue; + } + + xSAT_Clause_t* c = xSAT_SolverReadClause( s, i->CRef ); + Lits = &( c->pData[0].Lit ); + + // Make sure the false literal is data[1]: + NegLit = xSAT_NegLit( p ); + if ( Lits[0] == NegLit ) + { + Lits[0] = Lits[1]; + Lits[1] = NegLit; + } + assert( Lits[1] == NegLit ); + + xSAT_Watcher_t w = { .CRef = i->CRef, + .Blocker = Lits[0] }; + // If 0th watch is true, then clause is already satisfied. + if ( Lits[0] != i->Blocker && Vec_StrEntry( s->vAssigns, xSAT_Lit2Var( Lits[0] ) ) == xSAT_LitSign( Lits[0] ) ) + *j++ = w; + else + { + // Look for new watch: + int* stop = Lits + c->nSize; + int* k; + for ( k = Lits + 2; k < stop; k++ ) + { + if (Vec_StrEntry( s->vAssigns, xSAT_Lit2Var( *k ) ) != !xSAT_LitSign( *k ) ) + { + Lits[1] = *k; + *k = NegLit; + xSAT_WatchListPush( xSAT_VecWatchListEntry( s->vWatches, xSAT_NegLit( Lits[1] ) ), w ); + goto next; + } + } + + *j++ = w; + + // Clause is unit under assignment: + if (Vec_StrEntry( s->vAssigns, xSAT_Lit2Var( Lits[0] ) ) == xSAT_LitSign( xSAT_NegLit( Lits[0] ) ) ) + { + hConfl = i->CRef; + i++; + s->iQhead = Vec_IntSize( s->vTrail ); + // Copy the remaining watches: + while (i < end) + *j++ = *i++; + } + else + xSAT_SolverEnqueue( s, Lits[0], i->CRef ); + } + next: + i++; + } + + s->Stats.nInspects += j - xSAT_WatchListArray( ws ); + xSAT_WatchListShrink( ws, j - xSAT_WatchListArray( ws ) ); + } + + s->Stats.nPropagations += nProp; + s->nPropSimplify -= nProp; + + return hConfl; +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void xSAT_SolverReduceDB( xSAT_Solver_t * s ) +{ + static abctime TimeTotal = 0; + abctime clk = Abc_Clock(); + int nLearnedOld = Vec_IntSize( s->vLearnts ); + int i, limit; + uint32_t CRef; + xSAT_Clause_t * c; + xSAT_Clause_t ** learnts_cls; + + learnts_cls = ABC_ALLOC( xSAT_Clause_t *, nLearnedOld ); + Vec_IntForEachEntry( s->vLearnts, CRef, i ) + learnts_cls[i] = xSAT_SolverReadClause(s, CRef); + + limit = nLearnedOld / 2; + + xSAT_UtilSort((void *) learnts_cls, nLearnedOld, + (int (*)( const void *, const void * )) xSAT_ClauseCompare); + + if ( learnts_cls[nLearnedOld / 2]->nLBD <= 3 ) + s->nRC2 += s->Config.nSpecialIncReduce; + if ( learnts_cls[nLearnedOld - 1]->nLBD <= 5 ) + s->nRC2 += s->Config.nSpecialIncReduce; + + Vec_IntClear( s->vLearnts ); + for ( i = 0; i < nLearnedOld; i++ ) + { + c = learnts_cls[i]; + uint32_t CRef = xSAT_MemCRef( s->pMemory, (uint32_t * ) c ); + assert(c->fMark == 0); + if ( c->fCanBeDel && c->nLBD > 2 && c->nSize > 2 && (uint32_t) Vec_IntEntry( s->vReasons, xSAT_Lit2Var( c->pData[0].Lit ) ) != CRef && ( i < limit ) ) + { + c->fMark = 1; + s->Stats.nLearntLits -= c->nSize; + xSAT_WatchListRemove( xSAT_VecWatchListEntry( s->vWatches, xSAT_NegLit( c->pData[0].Lit ) ), CRef ); + xSAT_WatchListRemove( xSAT_VecWatchListEntry( s->vWatches, xSAT_NegLit( c->pData[1].Lit ) ), CRef ); + } + else + { + if (!c->fCanBeDel) + limit++; + c->fCanBeDel = 1; + Vec_IntPush( s->vLearnts, CRef ); + } + } + ABC_FREE( learnts_cls ); + + TimeTotal += Abc_Clock() - clk; + if ( s->Config.fVerbose ) + { + Abc_Print(1, "reduceDB: Keeping %7d out of %7d clauses (%5.2f %%) ", + Vec_IntSize( s->vLearnts ), nLearnedOld, 100.0 * Vec_IntSize( s->vLearnts ) / nLearnedOld ); + Abc_PrintTime( 1, "Time", TimeTotal ); + } + xSAT_SolverGarbageCollect(s); +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +char xSAT_SolverSearch( xSAT_Solver_t * s ) +{ + ABC_INT64_T conflictC = 0; + + s->Stats.nStarts++; + for (;;) + { + uint32_t hConfl = xSAT_SolverPropagate( s ); + + if ( hConfl != CRefUndef ) + { + /* Conflict */ + int BacktrackLevel; + unsigned nLBD; + uint32_t CRef; + + s->Stats.nConflicts++; + conflictC++; + + if ( xSAT_SolverDecisionLevel( s ) == 0 ) + return LBoolFalse; + + xSAT_BQueuePush( s->bqTrail, Vec_IntSize( s->vTrail ) ); + if ( s->Stats.nConflicts > s->Config.nFirstBlockRestart && xSAT_BQueueIsValid( s->bqLBD ) && ( Vec_IntSize( s->vTrail ) > ( s->Config.R * xSAT_BQueueAvg( s->bqTrail ) ) ) ) + xSAT_BQueueClean(s->bqLBD); + + Vec_IntClear( s->vLearntClause ); + xSAT_SolverAnalyze( s, hConfl, s->vLearntClause, &BacktrackLevel, &nLBD ); + + s->nSumLBD += nLBD; + xSAT_BQueuePush( s->bqLBD, nLBD ); + xSAT_SolverCancelUntil( s, BacktrackLevel ); + + CRef = Vec_IntSize( s->vLearntClause ) == 1 ? CRefUndef : xSAT_SolverClaNew( s, s->vLearntClause , 1 ); + xSAT_SolverEnqueue( s, Vec_IntEntry( s->vLearntClause , 0 ), CRef ); + + xSAT_SolverVarActDecay( s ); + xSAT_SolverClaActDecay( s ); + } + else + { + /* No conflict */ + int NextVar; + if ( xSAT_BQueueIsValid( s->bqLBD ) && ( ( xSAT_BQueueAvg( s->bqLBD ) * s->Config.K ) > ( s->nSumLBD / s->Stats.nConflicts ) ) ) + { + xSAT_BQueueClean( s->bqLBD ); + xSAT_SolverCancelUntil( s, 0 ); + return LBoolUndef; + } + + // Simplify the set of problem clauses: + if ( xSAT_SolverDecisionLevel( s ) == 0 ) + xSAT_SolverSimplify( s ); + + // Reduce the set of learnt clauses: + if ( s->Stats.nConflicts >= s->nConfBeforeReduce ) + { + s->nRC1 = ( s->Stats.nConflicts / s->nRC2 ) + 1; + xSAT_SolverReduceDB(s); + s->nRC2 += s->Config.nIncReduce; + s->nConfBeforeReduce = s->nRC1 * s->nRC2; + } + + // New variable decision: + NextVar = xSAT_SolverDecide( s ); + + if ( NextVar == VarUndef ) + return LBoolTrue; + + xSAT_SolverNewDecision( s, xSAT_Var2Lit( NextVar, ( int ) Vec_StrEntry( s->vPolarity, NextVar ) ) ); + } + } + + return LBoolUndef; // cannot happen +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void xSAT_SolverClaRealloc( xSAT_Mem_t * pDest, xSAT_Mem_t * pSrc, uint32_t * pCRef ) +{ + xSAT_Clause_t * pOldCla = xSAT_MemClauseHand( pSrc, *pCRef ); + if ( pOldCla->fReallocd ) + { + *pCRef = (uint32_t) pOldCla->nSize; + return; + } + + uint32_t nNewCRef = xSAT_MemAppend( pDest, 3 + pOldCla->fLearnt + pOldCla->nSize ); + xSAT_Clause_t * pNewCla = xSAT_MemClauseHand( pDest, nNewCRef ); + + memcpy( pNewCla, pOldCla, ( 3 + pOldCla->fLearnt + pOldCla->nSize ) * 4 ); + + pOldCla->fReallocd = 1; + pOldCla->nSize = (unsigned) nNewCRef; + *pCRef = nNewCRef; +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void xSAT_SolverGarbageCollect( xSAT_Solver_t * s ) +{ + int i; + uint32_t * pArray; + xSAT_Mem_t * pNewMemMngr = xSAT_MemAlloc( xSAT_MemCap( s->pMemory ) - xSAT_MemWastedCap( s->pMemory ) ); + + for ( i = 0; i < 2 * Vec_StrSize( s->vAssigns ); i++ ) + { + xSAT_WatchList_t* ws = xSAT_VecWatchListEntry( s->vWatches, i); + xSAT_Watcher_t* begin = xSAT_WatchListArray(ws); + xSAT_Watcher_t* end = begin + xSAT_WatchListSize(ws); + xSAT_Watcher_t *w; + + for ( w = begin; w != end; w++ ) + xSAT_SolverClaRealloc( pNewMemMngr, s->pMemory, &(w->CRef) ); + + ws = xSAT_VecWatchListEntry( s->vBinWatches, i); + begin = xSAT_WatchListArray(ws); + end = begin + xSAT_WatchListSize(ws); + for ( w = begin; w != end; w++ ) + xSAT_SolverClaRealloc( pNewMemMngr, s->pMemory, &(w->CRef) ); + } + + for ( i = 0; i < Vec_IntSize( s->vTrail ); i++ ) + if ( (uint32_t) Vec_IntEntry( s->vReasons, xSAT_Lit2Var( Vec_IntEntry( s->vTrail, i ) ) ) != CRefUndef ) + xSAT_SolverClaRealloc( pNewMemMngr, s->pMemory, &( Vec_IntArray( s->vReasons )[xSAT_Lit2Var( Vec_IntEntry( s->vTrail, i ) )] ) ); + + pArray = ( uint32_t * ) Vec_IntArray( s->vLearnts ); + for ( i = 0; i < Vec_IntSize( s->vLearnts ); i++ ) + xSAT_SolverClaRealloc( pNewMemMngr, s->pMemory, &(pArray[i]) ); + + pArray = (uint32_t *) Vec_IntArray( s->vClauses ); + for ( i = 0; i < Vec_IntSize( s->vClauses ); i++ ) + xSAT_SolverClaRealloc( pNewMemMngr, s->pMemory, &(pArray[i]) ); + + xSAT_MemFree( s->pMemory ); + s->pMemory = pNewMemMngr; +} + +ABC_NAMESPACE_IMPL_END diff --git a/src/sat/xsat/xsatSolver.h b/src/sat/xsat/xsatSolver.h new file mode 100644 index 00000000..a6d646c6 --- /dev/null +++ b/src/sat/xsat/xsatSolver.h @@ -0,0 +1,247 @@ +/**CFile**************************************************************** + + FileName [xsatSolver.h] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [xSAT - A SAT solver written in C. + Read the license file for more info.] + + Synopsis [Internal definitions of the solver.] + + Author [Bruno Schmitt <boschmitt@inf.ufrgs.br>] + + Affiliation [UC Berkeley / UFRGS] + + Date [Ver. 1.0. Started - November 10, 2016.] + + Revision [] + +***********************************************************************/ +#ifndef ABC__sat__xSAT__xsatSolver_h +#define ABC__sat__xSAT__xsatSolver_h + +//////////////////////////////////////////////////////////////////////// +/// INCLUDES /// +//////////////////////////////////////////////////////////////////////// +#include <stdio.h> +#include <stdlib.h> +#include <string.h> +#include <assert.h> + +#include "misc/util/abc_global.h" +#include "misc/vec/vecStr.h" + +#include "xsat.h" +#include "xsatBQueue.h" +#include "xsatClause.h" +#include "xsatHeap.h" +#include "xsatMemory.h" +#include "xsatWatchList.h" + +ABC_NAMESPACE_HEADER_START + +#ifndef __cplusplus +#ifndef false +# define false 0 +#endif +#ifndef true +# define true 1 +#endif +#endif + +enum +{ + Var0 = 1, + Var1 = 0, + VarX = 3 +}; + +enum +{ + LBoolUndef = 0, + LBoolTrue = 1, + LBoolFalse = -1 +}; + +enum +{ + VarUndef = -1, + LitUndef = -2 +}; + +#define CRefUndef UINT32_MAX + +//////////////////////////////////////////////////////////////////////// +/// STRUCTURE DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// +typedef struct xSAT_SolverOptions_t_ xSAT_SolverOptions_t; +struct xSAT_SolverOptions_t_ +{ + char fVerbose; + + // Limits + ABC_INT64_T nConfLimit; // external limit on the number of conflicts + ABC_INT64_T nInsLimit; // external limit on the number of implications + abctime nRuntimeLimit; // external limit on runtime + + // Constants used for restart heuristic + double K; // Forces a restart + double R; // Block a restart + int nFirstBlockRestart; // Lower bound number of conflicts for start blocking restarts + int nSizeLBDQueue; // Size of the moving avarege queue for LBD (force restart) + int nSizeTrailQueue; // Size of the moving avarege queue for Trail size (block restart) + + // Constants used for clause database reduction heuristic + int nConfFirstReduce; // Number of conflicts before first reduction + int nIncReduce; // Increment to reduce + int nSpecialIncReduce; // Special increment to reduce + unsigned nLBDFrozenClause; +}; + +typedef struct xSAT_Stats_t_ xSAT_Stats_t; +struct xSAT_Stats_t_ +{ + unsigned nStarts; + unsigned nReduceDB; + + ABC_INT64_T nDecisions; + ABC_INT64_T nPropagations; + ABC_INT64_T nInspects; + ABC_INT64_T nConflicts; + + ABC_INT64_T nClauseLits; + ABC_INT64_T nLearntLits; +}; + +struct xSAT_Solver_t_ +{ + /* Clauses Database */ + xSAT_Mem_t * pMemory; + Vec_Int_t * vLearnts; + Vec_Int_t * vClauses; + xSAT_VecWatchList_t * vWatches; + xSAT_VecWatchList_t * vBinWatches; + + /* Activity heuristic */ + int nVarActInc; /* Amount to bump next variable with. */ + int nClaActInc; /* Amount to bump next clause with. */ + + /* Variable Information */ + Vec_Int_t * vActivity; /* A heuristic measurement of the activity of a variable. */ + xSAT_Heap_t * hOrder; + Vec_Int_t * vLevels; /* Decision level of the current assignment */ + Vec_Int_t * vReasons; /* Reason (clause) of the current assignment */ + Vec_Str_t * vAssigns; /* Current assignment. */ + Vec_Str_t * vPolarity; + Vec_Str_t * vTags; + + /* Assignments */ + Vec_Int_t * vTrail; + Vec_Int_t * vTrailLim; // Separator indices for different decision levels in 'trail'. + int iQhead; // Head of propagation queue (as index into the trail). + + int nAssignSimplify; /* Number of top-level assignments since last + * execution of 'simplify()'. */ + int64_t nPropSimplify; /* Remaining number of propagations that must be + * made before next execution of 'simplify()'. */ + + /* Temporary data used by Search method */ + xSAT_BQueue_t * bqTrail; + xSAT_BQueue_t * bqLBD; + float nSumLBD; + int nConfBeforeReduce; + long nRC1; + int nRC2; + + /* Temporary data used by Analyze */ + Vec_Int_t * vLearntClause; + Vec_Str_t * vSeen; + Vec_Int_t * vTagged; + Vec_Int_t * vStack; + Vec_Int_t * vLastDLevel; + + /* Misc temporary */ + unsigned nStamp; + Vec_Int_t * vStamp; /* Multipurpose stamp used to calculate LBD and + * clauses minimization with binary resolution */ + + xSAT_SolverOptions_t Config; + xSAT_Stats_t Stats; +}; + +static inline int xSAT_Var2Lit( int Var, int c ) +{ + return Var + Var + ( c != 0 ); +} + +static inline int xSAT_NegLit( int Lit ) +{ + return Lit ^ 1; +} + +static inline int xSAT_Lit2Var( int Lit ) +{ + return Lit >> 1; +} + +static inline int xSAT_LitSign( int Lit ) +{ + return Lit & 1; +} + +static inline int xSAT_SolverDecisionLevel( xSAT_Solver_t * s ) +{ + return Vec_IntSize( s->vTrailLim ); +} + +static inline xSAT_Clause_t * xSAT_SolverReadClause( xSAT_Solver_t * s, uint32_t h ) +{ + return xSAT_MemClauseHand( s->pMemory, h ); +} + +static inline int xSAT_SolverIsClauseSatisfied( xSAT_Solver_t * s, xSAT_Clause_t * pCla ) +{ + int * lits = &( pCla->pData[0].Lit ); + + for ( int i = 0; i < pCla->nSize; i++ ) + if ( Vec_StrEntry( s->vAssigns, xSAT_Lit2Var( lits[i] ) ) == xSAT_LitSign( ( lits[i] ) ) ) + return true; + + return false; +} + +static inline void xSAT_SolverPrintClauses( xSAT_Solver_t * s ) +{ + int i; + unsigned CRef; + + Vec_IntForEachEntry( s->vClauses, CRef, i ) + xSAT_ClausePrint( xSAT_SolverReadClause( s, CRef ) ); +} + +static inline void xSAT_SolverPrintState( xSAT_Solver_t * s ) +{ + printf( "starts : %10d\n", s->Stats.nStarts ); + printf( "conflicts : %10ld\n", s->Stats.nConflicts ); + printf( "decisions : %10ld\n", s->Stats.nDecisions ); + printf( "propagations : %10ld\n", s->Stats.nPropagations ); +} + + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// +extern uint32_t xSAT_SolverClaNew( xSAT_Solver_t* s, Vec_Int_t * vLits, int fLearnt ); +extern char xSAT_SolverSearch( xSAT_Solver_t * s ); + +extern void xSAT_SolverGarbageCollect( xSAT_Solver_t * s ); + +extern int xSAT_SolverEnqueue( xSAT_Solver_t* s, int Lit, uint32_t From ); +extern void xSAT_SolverCancelUntil( xSAT_Solver_t* s, int Level); +extern uint32_t xSAT_SolverPropagate( xSAT_Solver_t* s ); +extern void xSAT_SolverRebuildOrderHeap( xSAT_Solver_t* s ); + +ABC_NAMESPACE_HEADER_END + +#endif diff --git a/src/sat/xsat/xsatSolverAPI.c b/src/sat/xsat/xsatSolverAPI.c new file mode 100644 index 00000000..7ee817ee --- /dev/null +++ b/src/sat/xsat/xsatSolverAPI.c @@ -0,0 +1,345 @@ +/**CFile**************************************************************** + + FileName [xsatSolverAPI.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [xSAT - A SAT solver written in C. + Read the license file for more info.] + + Synopsis [Solver external API functions implementation.] + + Author [Bruno Schmitt <boschmitt@inf.ufrgs.br>] + + Affiliation [UC Berkeley / UFRGS] + + Date [Ver. 1.0. Started - November 10, 2016.] + + Revision [] + +***********************************************************************/ +//////////////////////////////////////////////////////////////////////// +/// INCLUDES /// +//////////////////////////////////////////////////////////////////////// +#include <stdio.h> +#include <assert.h> +#include <string.h> +#include <math.h> + +#include "xsatSolver.h" + +ABC_NAMESPACE_IMPL_START + +xSAT_SolverOptions_t DefaultConfig = +{ + .fVerbose = 1, + + .nConfLimit = 0, + .nInsLimit = 0, + .nRuntimeLimit = 0, + + .K = 0.8, + .R = 1.4, + .nFirstBlockRestart = 10000, + .nSizeLBDQueue = 50, + .nSizeTrailQueue = 5000, + + .nConfFirstReduce = 2000, + .nIncReduce = 300, + .nSpecialIncReduce = 1000, + + .nLBDFrozenClause = 30 +}; + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +xSAT_Solver_t* xSAT_SolverCreate() +{ + xSAT_Solver_t * s = (xSAT_Solver_t *) ABC_CALLOC( char, sizeof( xSAT_Solver_t ) ); + s->Config = DefaultConfig; + + s->pMemory = xSAT_MemAlloc(0); + s->vClauses = Vec_IntAlloc(0); + s->vLearnts = Vec_IntAlloc(0); + s->vWatches = xSAT_VecWatchListAlloc( 0 ); + s->vBinWatches = xSAT_VecWatchListAlloc( 0 ); + + s->vTrailLim = Vec_IntAlloc(0); + s->vTrail = Vec_IntAlloc( 0 ); + + s->vActivity = Vec_IntAlloc( 0 ); + s->hOrder = xSAT_HeapAlloc( s->vActivity ); + + s->vPolarity = Vec_StrAlloc( 0 ); + s->vTags = Vec_StrAlloc( 0 ); + s->vAssigns = Vec_StrAlloc( 0 ); + s->vLevels = Vec_IntAlloc( 0 ); + s->vReasons = Vec_IntAlloc( 0 ); + s->vStamp = Vec_IntAlloc( 0 ); + + s->vTagged = Vec_IntAlloc(0); + s->vStack = Vec_IntAlloc(0); + + s->vSeen = Vec_StrAlloc( 0 ); + s->vLearntClause = Vec_IntAlloc(0); + s->vLastDLevel = Vec_IntAlloc(0); + + + s->bqTrail = xSAT_BQueueNew( s->Config.nSizeTrailQueue ); + s->bqLBD = xSAT_BQueueNew( s->Config.nSizeLBDQueue ); + + s->nVarActInc = (1 << 5); + s->nClaActInc = (1 << 11); + + s->nConfBeforeReduce = s->Config.nConfFirstReduce; + s->nRC1 = 1; + s->nRC2 = s->Config.nConfFirstReduce; + return s; +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void xSAT_SolverDestroy( xSAT_Solver_t * s ) +{ + xSAT_MemFree( s->pMemory ); + Vec_IntFree( s->vClauses ); + Vec_IntFree( s->vLearnts ); + xSAT_VecWatchListFree( s->vWatches ); + xSAT_VecWatchListFree( s->vBinWatches ); + + // delete vectors + xSAT_HeapFree(s->hOrder); + Vec_IntFree( s->vTrailLim ); + Vec_IntFree( s->vTrail ); + Vec_IntFree( s->vTagged ); + Vec_IntFree( s->vStack ); + + Vec_StrFree( s->vSeen ); + Vec_IntFree( s->vLearntClause ); + Vec_IntFree( s->vLastDLevel ); + + Vec_IntFree( s->vActivity ); + Vec_StrFree( s->vPolarity ); + Vec_StrFree( s->vTags ); + Vec_StrFree( s->vAssigns ); + Vec_IntFree( s->vLevels ); + Vec_IntFree( s->vReasons ); + + xSAT_BQueueFree(s->bqLBD); + xSAT_BQueueFree(s->bqTrail); + + ABC_FREE(s); +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int xSAT_SolverSimplify( xSAT_Solver_t * s ) +{ + int i, j; + uint32_t CRef; + assert( xSAT_SolverDecisionLevel(s) == 0 ); + + if ( xSAT_SolverPropagate(s) != CRefUndef ) + return false; + + if ( s->nAssignSimplify == Vec_IntSize( s->vTrail ) || s->nPropSimplify > 0 ) + return true; + + j = 0; + Vec_IntForEachEntry( s->vClauses, CRef, i ) + { + xSAT_Clause_t * pCla = xSAT_SolverReadClause( s, CRef ); + if ( xSAT_SolverIsClauseSatisfied( s, pCla ) ) + { + pCla->fMark = 1; + s->Stats.nClauseLits -= pCla->nSize; + + if ( pCla->nSize == 2 ) + { + xSAT_WatchListRemove( xSAT_VecWatchListEntry( s->vBinWatches, xSAT_NegLit(pCla->pData[0].Lit) ), CRef ); + xSAT_WatchListRemove( xSAT_VecWatchListEntry( s->vBinWatches, xSAT_NegLit(pCla->pData[1].Lit) ), CRef ); + } + else + { + xSAT_WatchListRemove( xSAT_VecWatchListEntry( s->vWatches, xSAT_NegLit(pCla->pData[0].Lit) ), CRef ); + xSAT_WatchListRemove( xSAT_VecWatchListEntry( s->vWatches, xSAT_NegLit(pCla->pData[1].Lit) ), CRef ); + } + } + else + Vec_IntWriteEntry( s->vClauses, j++, CRef ); + } + Vec_IntShrink( s->vClauses, j ); + xSAT_SolverRebuildOrderHeap( s ); + + s->nAssignSimplify = Vec_IntSize( s->vTrail ); + s->nPropSimplify = s->Stats.nClauseLits + s->Stats.nLearntLits; + + return true; +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void xSAT_SolverAddVariable( xSAT_Solver_t* s, int Sign ) +{ + int Var = Vec_IntSize( s->vActivity ); + + xSAT_VecWatchListPush( s->vWatches ); + xSAT_VecWatchListPush( s->vWatches ); + xSAT_VecWatchListPush( s->vBinWatches ); + xSAT_VecWatchListPush( s->vBinWatches ); + + Vec_IntPush( s->vActivity, 0 ); + Vec_IntPush( s->vLevels, 0 ); + Vec_StrPush( s->vAssigns, VarX ); + Vec_StrPush( s->vPolarity, 1 ); + Vec_StrPush( s->vTags, 0 ); + Vec_IntPush( s->vReasons, ( int ) CRefUndef ); + Vec_IntPush( s->vStamp, 0 ); + Vec_StrPush( s->vSeen, 0 ); + + xSAT_HeapInsert( s->hOrder, Var ); +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int xSAT_SolverAddClause( xSAT_Solver_t * s, Vec_Int_t * vLits ) +{ + int i, j; + int Lit, PrevLit; + int MaxVar; + + Vec_IntSort( vLits, 0 ); + MaxVar = xSAT_Lit2Var( Vec_IntEntryLast( vLits ) ); + while ( MaxVar >= Vec_IntSize( s->vActivity ) ) + xSAT_SolverAddVariable( s, 1 ); + + j = 0; + PrevLit = LitUndef; + Vec_IntForEachEntry( vLits, Lit, i ) + { + if ( Lit == xSAT_NegLit( PrevLit ) || Vec_StrEntry( s->vAssigns, xSAT_Lit2Var( Lit ) ) == xSAT_LitSign( Lit ) ) + return true; + else if ( Lit != PrevLit && Vec_StrEntry( s->vAssigns, xSAT_Lit2Var( Lit ) ) == VarX ) + { + PrevLit = Lit; + Vec_IntWriteEntry( vLits, j++, Lit ); + } + } + Vec_IntShrink( vLits, j ); + + if ( Vec_IntSize( vLits ) == 0 ) + return false; + if ( Vec_IntSize( vLits ) == 1 ) + { + xSAT_SolverEnqueue( s, Vec_IntEntry( vLits, 0 ), CRefUndef ); + return ( xSAT_SolverPropagate( s ) == CRefUndef ); + } + + xSAT_SolverClaNew( s, vLits, 0 ); + return true; +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int xSAT_SolverSolve( xSAT_Solver_t* s ) +{ + char status = LBoolUndef; + + assert(s); + if ( s->Config.fVerbose ) + { + printf( "==========================================[ BLACK MAGIC ]================================================\n" ); + printf( "| | | |\n" ); + printf( "| - Restarts: | - Reduce Clause DB: | - Minimize Asserting: |\n" ); + printf( "| * LBD Queue : %6d | * First : %6d | * size < %3d |\n", s->Config.nSizeLBDQueue, s->Config.nConfFirstReduce, 0 ); + printf( "| * Trail Queue : %6d | * Inc : %6d | * lbd < %3d |\n", s->Config.nSizeTrailQueue, s->Config.nIncReduce, 0 ); + printf( "| * K : %6.2f | * Special : %6d | |\n", s->Config.K, s->Config.nSpecialIncReduce ); + printf( "| * R : %6.2f | * Protected : (lbd)< %2d | |\n", s->Config.R, s->Config.nLBDFrozenClause ); + printf( "| | | |\n" ); + printf( "=========================================================================================================\n" ); + } + + while ( status == LBoolUndef ) + status = xSAT_SolverSearch( s ); + + if ( s->Config.fVerbose ) + printf( "=========================================================================================================\n" ); + + xSAT_SolverCancelUntil( s, 0 ); + return status; +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void xSAT_SolverPrintStats( xSAT_Solver_t * s ) +{ + printf( "starts : %10d\n", s->Stats.nStarts ); + printf( "conflicts : %10ld\n", s->Stats.nConflicts ); + printf( "decisions : %10ld\n", s->Stats.nDecisions ); + printf( "propagations : %10ld\n", s->Stats.nPropagations ); +} + +ABC_NAMESPACE_IMPL_END diff --git a/src/sat/xsat/xsatUtils.h b/src/sat/xsat/xsatUtils.h new file mode 100644 index 00000000..7f774d85 --- /dev/null +++ b/src/sat/xsat/xsatUtils.h @@ -0,0 +1,106 @@ +/**CFile**************************************************************** + + FileName [xsatUtils.h] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [xSAT - A SAT solver written in C. + Read the license file for more info.] + + Synopsis [Utility functions used in xSAT] + + Author [Bruno Schmitt <boschmitt@inf.ufrgs.br>] + + Affiliation [UC Berkeley / UFRGS] + + Date [Ver. 1.0. Started - November 10, 2016.] + + Revision [] + +***********************************************************************/ +#ifndef ABC__sat__xSAT__xsatUtils_h +#define ABC__sat__xSAT__xsatUtils_h + +//////////////////////////////////////////////////////////////////////// +/// INCLUDES /// +//////////////////////////////////////////////////////////////////////// +#include "misc/util/abc_global.h" + +ABC_NAMESPACE_HEADER_START + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline void xSAT_UtilSelectSort( void** pArray, int nSize, int(* CompFnct )( const void *, const void * ) ) +{ + int i, j, iBest; + void* pTmp; + + for ( i = 0; i < ( nSize - 1 ); i++ ) + { + iBest = i; + for ( j = i + 1; j < nSize; j++ ) + { + if ( CompFnct( pArray[j], pArray[iBest] ) ) + iBest = j; + } + pTmp = pArray[i]; + pArray[i] = pArray[iBest]; + pArray[iBest] = pTmp; + } +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static void xSAT_UtilSort( void** pArray, int nSize, int(* CompFnct )( const void *, const void *) ) +{ + if ( nSize <= 15 ) + xSAT_UtilSelectSort( pArray, nSize, CompFnct ); + else + { + void* pPivot = pArray[nSize / 2]; + void* pTmp; + int i = -1; + int j = nSize; + + for(;;) + { + do i++; while( CompFnct( pArray[i], pPivot ) ); + do j--; while( CompFnct( pPivot, pArray[j] ) ); + + if ( i >= j ) + break; + + pTmp = pArray[i]; + pArray[i] = pArray[j]; + pArray[j] = pTmp; + } + + xSAT_UtilSort( pArray, i, CompFnct ); + xSAT_UtilSort( pArray + i, ( nSize - i ), CompFnct ); + } +} + +ABC_NAMESPACE_HEADER_END + +#endif +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// diff --git a/src/sat/xsat/xsatWatchList.h b/src/sat/xsat/xsatWatchList.h new file mode 100644 index 00000000..454cfe44 --- /dev/null +++ b/src/sat/xsat/xsatWatchList.h @@ -0,0 +1,268 @@ +/**CFile**************************************************************** + + FileName [xsatWatchList.h] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [xSAT - A SAT solver written in C. + Read the license file for more info.] + + Synopsis [Watch list and its related structures implementation] + + Author [Bruno Schmitt <boschmitt@inf.ufrgs.br>] + + Affiliation [UC Berkeley / UFRGS] + + Date [Ver. 1.0. Started - November 10, 2016.] + + Revision [] + +***********************************************************************/ +#ifndef ABC__sat__xSAT__xsatWatchList_h +#define ABC__sat__xSAT__xsatWatchList_h + +//////////////////////////////////////////////////////////////////////// +/// INCLUDES /// +//////////////////////////////////////////////////////////////////////// +#include "misc/util/abc_global.h" + +ABC_NAMESPACE_HEADER_START + +//////////////////////////////////////////////////////////////////////// +/// STRUCTURE DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// +typedef struct xSAT_Watcher_t_ xSAT_Watcher_t; +struct xSAT_Watcher_t_ +{ + uint32_t CRef; + int Blocker; +}; + +typedef struct xSAT_WatchList_t_ xSAT_WatchList_t; +struct xSAT_WatchList_t_ +{ + int nCap; + int nSize; + xSAT_Watcher_t * pArray; +}; + +typedef struct xSAT_VecWatchList_t_ xSAT_VecWatchList_t; +struct xSAT_VecWatchList_t_ +{ + int nCap; + int nSize; + xSAT_WatchList_t * pArray; +}; + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline void xSAT_WatchListFree( xSAT_WatchList_t * v ) +{ + if ( v->pArray ) + ABC_FREE( v->pArray ); +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline int xSAT_WatchListSize( xSAT_WatchList_t * v ) +{ + return v->nSize; +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline void xSAT_WatchListShrink( xSAT_WatchList_t * v, int k ) +{ + assert(k <= v->nSize); + v->nSize = k; +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline void xSAT_WatchListPush( xSAT_WatchList_t * v, xSAT_Watcher_t e ) +{ + assert( v ); + if (v->nSize == v->nCap) + { + int newsize = (v->nCap < 4) ? 4 : (v->nCap / 2) * 3; + + v->pArray = ABC_REALLOC( xSAT_Watcher_t, v->pArray, newsize ); + if ( v->pArray == NULL ) + { + printf( "Failed to realloc memory from %.1f MB to %.1f MB.\n", + 1.0 * v->nCap / (1<<20), 1.0 * newsize / (1<<20) ); + fflush( stdout ); + } + v->nCap = newsize; + } + + v->pArray[v->nSize++] = e; +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline xSAT_Watcher_t* xSAT_WatchListArray( xSAT_WatchList_t * v ) +{ + return v->pArray; +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline void xSAT_WatchListRemove( xSAT_WatchList_t * v, uint32_t CRef ) +{ + xSAT_Watcher_t* ws = xSAT_WatchListArray(v); + int j = 0; + + for (; ws[j].CRef != CRef; j++); + assert(j < xSAT_WatchListSize(v)); + memmove(v->pArray + j, v->pArray + j + 1, (v->nSize - j - 1) * sizeof(xSAT_Watcher_t)); + v->nSize -= 1; +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline xSAT_VecWatchList_t * xSAT_VecWatchListAlloc( int nCap ) +{ + xSAT_VecWatchList_t * v = ABC_ALLOC( xSAT_VecWatchList_t, 1 ); + + v->nCap = 4; + v->nSize = 0; + v->pArray = (xSAT_WatchList_t *) ABC_CALLOC(xSAT_WatchList_t, sizeof( xSAT_WatchList_t ) * v->nCap); + return v; +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline void xSAT_VecWatchListFree( xSAT_VecWatchList_t* v ) +{ + for( int i = 0; i < v->nSize; i++ ) + xSAT_WatchListFree( v->pArray + i ); + + ABC_FREE( v->pArray ); + ABC_FREE( v ); +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline void xSAT_VecWatchListPush( xSAT_VecWatchList_t* v ) +{ + if ( v->nSize == v->nCap ) + { + int newsize = (v->nCap < 4) ? v->nCap * 2 : (v->nCap / 2) * 3; + + v->pArray = ABC_REALLOC( xSAT_WatchList_t, v->pArray, newsize ); + memset( v->pArray + v->nCap, 0, sizeof(xSAT_WatchList_t) * (newsize - v->nCap) ); + if ( v->pArray == NULL ) + { + printf( "Failed to realloc memory from %.1f MB to %.1f MB.\n", + 1.0 * v->nCap / (1<<20), 1.0 * newsize / (1<<20) ); + fflush( stdout ); + } + v->nCap = newsize; + } + + v->nSize++; +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline xSAT_WatchList_t * xSAT_VecWatchListEntry( xSAT_VecWatchList_t* v, int iEntry ) +{ + assert( iEntry < v->nCap ); + assert( iEntry < v->nSize ); + return v->pArray + iEntry; +} + +ABC_NAMESPACE_HEADER_END + +#endif |