luke
/
abc
mirror of https://github.com/YosysHQ/abc.git
1
0
Fork 0
Code Issues Packages Projects Releases Wiki Activity

xSAT is an experimental SAT Solver based on Glucose v3(see Glucose copyrights below) and ABC C version of 

MiniSat (bsat) developed by Niklas Sorensson and modified by Alan Mishchenko. It’s development has reached
sufficient maturity to be committed in ABC, but still in a beta state.

TODO:
* Read compressed CNF files.
* Study the use of floating point for variables and clauses activity.
* Better documentation.
* Improve verbose messages.
* Expose parameters for tuning.
This commit is contained in:
Bruno Schmitt 2016-12-12 16:20:38 -02:00
parent cd92b1fea3
commit 5351ab4b13
15 changed files with 3392 additions and 100 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

2
Makefile
View File

@ -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 \

339
src/base/abci/abc.c
View File

@ -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();
@ -23157,6 +23160,144 @@ usage:
return 1;
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
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 []
@ -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 []

39
src/sat/xsat/license Normal file
View File

@ -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.
*******************************************************************************/

3
src/sat/xsat/module.make Normal file
View File

@ -0,0 +1,3 @@
SRC += src/sat/xsat/xsatSolver.c \
src/sat/xsat/xsatSolverAPI.c \
src/sat/xsat/xsatCnfReader.c

59
src/sat/xsat/xsat.h Normal file
View File

@ -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 ///
////////////////////////////////////////////////////////////////////////

189
src/sat/xsat/xsatBQueue.h Normal file
View File

@ -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

109
src/sat/xsat/xsatClause.h Normal file
View File

@ -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 ///
////////////////////////////////////////////////////////////////////////

236
src/sat/xsat/xsatCnfReader.c Normal file
View File

@ -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 ///
////////////////////////////////////////////////////////////////////////

330
src/sat/xsat/xsatHeap.h Normal file
View File

@ -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

225
src/sat/xsat/xsatMemory.h Normal file
View File

@ -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 ///
////////////////////////////////////////////////////////////////////////

995
src/sat/xsat/xsatSolver.c Normal file
View File

@ -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

247
src/sat/xsat/xsatSolver.h Normal file
View File

@ -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

345
src/sat/xsat/xsatSolverAPI.c Normal file
View File

@ -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

106
src/sat/xsat/xsatUtils.h Normal file
View File

@ -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 ///
////////////////////////////////////////////////////////////////////////

268
src/sat/xsat/xsatWatchList.h Normal file
View File

@ -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