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