Skip to content

A
abc
Commit b1a913fb by Alan Mishchenko
Options

Version abc70123

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