mirror of https://github.com/YosysHQ/abc.git
Adding Glucose 3.0 as a separate package.
This commit is contained in:
Alan Mishchenko
parent
7857b7fd8b
commit
9e46ebe3f8
108
abclib.dsp
108
abclib.dsp
|
|
@ -2174,6 +2174,114 @@ SOURCE=.\src\sat\xsat\xsatUtils.h
|
|||
SOURCE=.\src\sat\xsat\xsatWatchList.h
|
||||
# End Source File
|
||||
# End Group
|
||||
# Begin Group "glucose"
|
||||
|
||||
# PROP Default_Filter ""
|
||||
# Begin Source File
|
||||
|
||||
SOURCE=.\src\sat\glucose\AbcGlucose.cpp
|
||||
# End Source File
|
||||
# Begin Source File
|
||||
|
||||
SOURCE=.\src\sat\glucose\AbcGlucose.h
|
||||
# End Source File
|
||||
# Begin Source File
|
||||
|
||||
SOURCE=.\src\sat\glucose\AbcGlucoseCmd.cpp
|
||||
# End Source File
|
||||
# Begin Source File
|
||||
|
||||
SOURCE=.\src\sat\glucose\Alg.h
|
||||
# End Source File
|
||||
# Begin Source File
|
||||
|
||||
SOURCE=.\src\sat\glucose\Alloc.h
|
||||
# End Source File
|
||||
# Begin Source File
|
||||
|
||||
SOURCE=.\src\sat\glucose\BoundedQueue.h
|
||||
# End Source File
|
||||
# Begin Source File
|
||||
|
||||
SOURCE=.\src\sat\glucose\Constants.h
|
||||
# End Source File
|
||||
# Begin Source File
|
||||
|
||||
SOURCE=.\src\sat\glucose\Dimacs.h
|
||||
# End Source File
|
||||
# Begin Source File
|
||||
|
||||
SOURCE=.\src\sat\glucose\Glucose.cpp
|
||||
# End Source File
|
||||
# Begin Source File
|
||||
|
||||
SOURCE=.\src\sat\glucose\Heap.h
|
||||
# End Source File
|
||||
# Begin Source File
|
||||
|
||||
SOURCE=.\src\sat\glucose\IntTypes.h
|
||||
# End Source File
|
||||
# Begin Source File
|
||||
|
||||
SOURCE=.\src\sat\glucose\Map.h
|
||||
# End Source File
|
||||
# Begin Source File
|
||||
|
||||
SOURCE=.\src\sat\glucose\Options.cpp
|
||||
# End Source File
|
||||
# Begin Source File
|
||||
|
||||
SOURCE=.\src\sat\glucose\Options.h
|
||||
# End Source File
|
||||
# Begin Source File
|
||||
|
||||
SOURCE=.\src\sat\glucose\ParseUtils.h
|
||||
# End Source File
|
||||
# Begin Source File
|
||||
|
||||
SOURCE=.\src\sat\glucose\pstdint.h
|
||||
# End Source File
|
||||
# Begin Source File
|
||||
|
||||
SOURCE=.\src\sat\glucose\Queue.h
|
||||
# End Source File
|
||||
# Begin Source File
|
||||
|
||||
SOURCE=.\src\sat\glucose\SimpSolver.cpp
|
||||
# End Source File
|
||||
# Begin Source File
|
||||
|
||||
SOURCE=.\src\sat\glucose\SimpSolver.h
|
||||
# End Source File
|
||||
# Begin Source File
|
||||
|
||||
SOURCE=.\src\sat\glucose\Solver.h
|
||||
# End Source File
|
||||
# Begin Source File
|
||||
|
||||
SOURCE=.\src\sat\glucose\SolverTypes.h
|
||||
# End Source File
|
||||
# Begin Source File
|
||||
|
||||
SOURCE=.\src\sat\glucose\Sort.h
|
||||
# End Source File
|
||||
# Begin Source File
|
||||
|
||||
SOURCE=.\src\sat\glucose\System.cpp
|
||||
# End Source File
|
||||
# Begin Source File
|
||||
|
||||
SOURCE=.\src\sat\glucose\System.h
|
||||
# End Source File
|
||||
# Begin Source File
|
||||
|
||||
SOURCE=.\src\sat\glucose\Vec.h
|
||||
# End Source File
|
||||
# Begin Source File
|
||||
|
||||
SOURCE=.\src\sat\glucose\XAlloc.h
|
||||
# End Source File
|
||||
# End Group
|
||||
# End Group
|
||||
# Begin Group "opt"
|
||||
|
||||
|
|
|
|||
|
|
@ -61,6 +61,8 @@ extern void Abc2_Init( Abc_Frame_t * pAbc );
|
|||
extern void Abc2_End ( Abc_Frame_t * pAbc );
|
||||
extern void Abc85_Init( Abc_Frame_t * pAbc );
|
||||
extern void Abc85_End( Abc_Frame_t * pAbc );
|
||||
extern void Glucose_Init( Abc_Frame_t * pAbc );
|
||||
extern void Glucose_End( Abc_Frame_t * pAbc );
|
||||
|
||||
static Abc_FrameInitializer_t* s_InitializerStart = NULL;
|
||||
static Abc_FrameInitializer_t* s_InitializerEnd = NULL;
|
||||
|
|
@ -114,6 +116,7 @@ void Abc_FrameInit( Abc_Frame_t * pAbc )
|
|||
Cba_Init( pAbc );
|
||||
Pla_Init( pAbc );
|
||||
Test_Init( pAbc );
|
||||
Glucose_Init( pAbc );
|
||||
for( p = s_InitializerStart ; p ; p = p->next )
|
||||
if(p->init)
|
||||
p->init(pAbc);
|
||||
|
|
@ -152,6 +155,7 @@ void Abc_FrameEnd( Abc_Frame_t * pAbc )
|
|||
Cba_End( pAbc );
|
||||
Pla_End( pAbc );
|
||||
Test_End( pAbc );
|
||||
Glucose_End( pAbc );
|
||||
}
|
||||
|
||||
|
||||
|
|
|
|||
|
|
@ -0,0 +1,268 @@
|
|||
/**CFile****************************************************************
|
||||
|
||||
FileName [AbcGlucose.cpp]
|
||||
|
||||
SystemName [ABC: Logic synthesis and verification system.]
|
||||
|
||||
PackageName [SAT solver Glucose 3.0.]
|
||||
|
||||
Synopsis [Interface to Glucose.]
|
||||
|
||||
Author [Alan Mishchenko]
|
||||
|
||||
Affiliation [UC Berkeley]
|
||||
|
||||
Date [Ver. 1.0. Started - September 6, 2017.]
|
||||
|
||||
Revision [$Id: AbcGlucose.cpp,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
|
||||
|
||||
***********************************************************************/
|
||||
|
||||
#include "sat/glucose/System.h"
|
||||
#include "sat/glucose/ParseUtils.h"
|
||||
#include "sat/glucose/Options.h"
|
||||
#include "sat/glucose/Dimacs.h"
|
||||
#include "sat/glucose/SimpSolver.h"
|
||||
|
||||
#include "sat/glucose/AbcGlucose.h"
|
||||
|
||||
#include "aig/gia/gia.h"
|
||||
#include "sat/cnf/cnf.h"
|
||||
|
||||
using namespace Glucose;
|
||||
|
||||
ABC_NAMESPACE_IMPL_START
|
||||
|
||||
extern "C" {
|
||||
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
/// DECLARATIONS ///
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
/// FUNCTION DEFINITIONS ///
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
|
||||
/**Function*************************************************************
|
||||
|
||||
Synopsis []
|
||||
|
||||
Description []
|
||||
|
||||
SideEffects []
|
||||
|
||||
SeeAlso []
|
||||
|
||||
***********************************************************************/
|
||||
Glucose::Solver * glucose_solver_start()
|
||||
{
|
||||
Solver * S = new Solver;
|
||||
S->setIncrementalMode();
|
||||
return S;
|
||||
}
|
||||
|
||||
void glucose_solver_stop(Glucose::Solver* S)
|
||||
{
|
||||
delete S;
|
||||
}
|
||||
|
||||
int glucose_solver_addclause(Glucose::Solver* S, int * plits, int nlits)
|
||||
{
|
||||
vec<Lit> lits;
|
||||
for ( int i = 0; i < nlits; i++,plits++)
|
||||
{
|
||||
// note: Glucose uses the same var->lit conventiaon as ABC
|
||||
while ((*plits)/2 >= S->nVars()) S->newVar();
|
||||
assert((*plits)/2 < S->nVars()); // NOTE: since we explicitely use new function bmc_add_var
|
||||
Lit p;
|
||||
p.x = *plits;
|
||||
lits.push(p);
|
||||
}
|
||||
return S->addClause(lits); // returns 0 if the problem is UNSAT
|
||||
}
|
||||
|
||||
int glucose_solver_setcallback(Glucose::Solver* S, void * pman, int(*pfunc)(void*, int, int*))
|
||||
{
|
||||
S->pCnfMan = pman;
|
||||
S->pCnfFunc = pfunc;
|
||||
S->nCallConfl = 1000;
|
||||
return 0;
|
||||
}
|
||||
|
||||
int glucose_solver_solve(Glucose::Solver* S, int * plits, int nlits)
|
||||
{
|
||||
vec<Lit> lits;
|
||||
for (int i=0;i<nlits;i++,plits++)
|
||||
{
|
||||
Lit p;
|
||||
p.x = *plits;
|
||||
lits.push(p);
|
||||
}
|
||||
Glucose::lbool res = S->solveLimited(lits);
|
||||
return (res == l_True ? 1 : res == l_False ? -1 : 0);
|
||||
}
|
||||
|
||||
int glucose_solver_addvar(Glucose::Solver* S)
|
||||
{
|
||||
S->newVar();
|
||||
return S->nVars() - 1;
|
||||
}
|
||||
|
||||
int glucose_solver_read_cex_varvalue(Glucose::Solver* S, int ivar)
|
||||
{
|
||||
return S->model[ivar] == l_True;
|
||||
}
|
||||
|
||||
void glucose_solver_setstop(Glucose::Solver* S, int * pstop)
|
||||
{
|
||||
S->pstop = pstop;
|
||||
}
|
||||
|
||||
void glucose_print_stats(Solver& s, abctime clk)
|
||||
{
|
||||
double cpu_time = (double)(unsigned)clk / CLOCKS_PER_SEC;
|
||||
double mem_used = memUsed();
|
||||
printf("c restarts : %d (%d conflicts on average)\n", (int)s.starts, s.starts > 0 ? s.conflicts/s.starts : 0);
|
||||
printf("c blocked restarts : %d (multiple: %d) \n", (int)s.nbstopsrestarts,s.nbstopsrestartssame);
|
||||
printf("c last block at restart : %d\n", (int)s.lastblockatrestart);
|
||||
printf("c nb ReduceDB : %-12d\n", (int)s.nbReduceDB);
|
||||
printf("c nb removed Clauses : %-12d\n", (int)s.nbRemovedClauses);
|
||||
printf("c nb learnts DL2 : %-12d\n", (int)s.nbDL2);
|
||||
printf("c nb learnts size 2 : %-12d\n", (int)s.nbBin);
|
||||
printf("c nb learnts size 1 : %-12d\n", (int)s.nbUn);
|
||||
printf("c conflicts : %-12d (%.0f /sec)\n", (int)s.conflicts, s.conflicts /cpu_time);
|
||||
printf("c decisions : %-12d (%4.2f %% random) (%.0f /sec)\n", (int)s.decisions, (float)s.rnd_decisions*100 / (float)s.decisions, s.decisions /cpu_time);
|
||||
printf("c propagations : %-12d (%.0f /sec)\n", (int)s.propagations, s.propagations/cpu_time);
|
||||
printf("c conflict literals : %-12d (%4.2f %% deleted)\n", (int)s.tot_literals, (s.max_literals - s.tot_literals)*100 / (double)s.max_literals);
|
||||
printf("c nb reduced Clauses : %-12d\n", (int)s.nbReducedClauses);
|
||||
if (mem_used != 0) printf("Memory used : %.2f MB\n", mem_used);
|
||||
//printf("c CPU time : %.2f sec\n", cpu_time);
|
||||
}
|
||||
|
||||
/**Function*************************************************************
|
||||
|
||||
Synopsis []
|
||||
|
||||
Description []
|
||||
|
||||
SideEffects []
|
||||
|
||||
SeeAlso []
|
||||
|
||||
***********************************************************************/
|
||||
void Glucose_SolveCnf( char * pFilename, ExtSat_Pars * pPars )
|
||||
{
|
||||
abctime clk = Abc_Clock();
|
||||
SimpSolver S;
|
||||
S.verbosity = pPars->verb;
|
||||
S.setConfBudget( pPars->nConfls > 0 ? (int64_t)pPars->nConfls : -1 );
|
||||
|
||||
gzFile in = gzopen(pFilename, "rb");
|
||||
parse_DIMACS(in, S);
|
||||
gzclose(in);
|
||||
|
||||
printf("c ============================[ Problem Statistics ]=============================\n");
|
||||
printf("c | |\n");
|
||||
printf("c | Number of variables: %12d |\n", S.nVars());
|
||||
printf("c | Number of clauses: %12d |\n", S.nClauses());
|
||||
|
||||
if ( pPars->pre ) S.eliminate(true);
|
||||
|
||||
vec<Lit> dummy;
|
||||
lbool ret = S.solveLimited(dummy);
|
||||
if ( pPars->verb ) glucose_print_stats(S, Abc_Clock() - clk);
|
||||
printf(ret == l_True ? "SATISFIABLE" : ret == l_False ? "UNSATISFIABLE" : "INDETERMINATE");
|
||||
Abc_PrintTime( 1, " Time", Abc_Clock() - clk );
|
||||
}
|
||||
|
||||
/**Function*************************************************************
|
||||
|
||||
Synopsis []
|
||||
|
||||
Description []
|
||||
|
||||
SideEffects []
|
||||
|
||||
SeeAlso []
|
||||
|
||||
***********************************************************************/
|
||||
Vec_Int_t * Glucose_SolverFromAig( Gia_Man_t * p, SimpSolver& S )
|
||||
{
|
||||
abctime clk = Abc_Clock();
|
||||
int * pLit, * pStop, i;
|
||||
Cnf_Dat_t * pCnf = (Cnf_Dat_t *)Mf_ManGenerateCnf( p, 8 /*nLutSize*/, 0 /*fCnfObjIds*/, 1/*fAddOrCla*/, 0, 0/*verbose*/ );
|
||||
for ( i = 0; i < pCnf->nClauses; i++ )
|
||||
{
|
||||
vec<Lit> lits;
|
||||
for ( pLit = pCnf->pClauses[i], pStop = pCnf->pClauses[i+1]; pLit < pStop; pLit++ )
|
||||
{
|
||||
int Lit = *pLit;
|
||||
int parsed_lit = (Lit & 1)? -(Lit >> 1)-1 : (Lit >> 1)+1;
|
||||
int var = abs(parsed_lit)-1;
|
||||
while (var >= S.nVars()) S.newVar();
|
||||
lits.push( (parsed_lit > 0) ? mkLit(var) : ~mkLit(var) );
|
||||
}
|
||||
S.addClause(lits);
|
||||
}
|
||||
Vec_Int_t * vCnfIds = Vec_IntAllocArrayCopy(pCnf->pVarNums,pCnf->nVars);
|
||||
//printf( "CNF stats: Vars = %6d. Clauses = %7d. Literals = %8d. ", pCnf->nVars, pCnf->nClauses, pCnf->nLiterals );
|
||||
//Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
|
||||
Cnf_DataFree(pCnf);
|
||||
return vCnfIds;
|
||||
}
|
||||
|
||||
int Glucose_SolveAig(Gia_Man_t * p, ExtSat_Pars * pPars)
|
||||
{
|
||||
abctime clk = Abc_Clock();
|
||||
|
||||
SimpSolver S;
|
||||
S.verbosity = pPars->verb;
|
||||
S.verbEveryConflicts = 50000;
|
||||
S.showModel = false;
|
||||
S.setConfBudget( pPars->nConfls > 0 ? (int64_t)pPars->nConfls : -1 );
|
||||
|
||||
S.parsing = 1;
|
||||
Vec_Int_t * vCnfIds = Glucose_SolverFromAig(p,S);
|
||||
S.parsing = 0;
|
||||
|
||||
if (pPars->verb)
|
||||
{
|
||||
printf("c ============================[ Problem Statistics ]=============================\n");
|
||||
printf("c | |\n");
|
||||
printf("c | Number of variables: %12d |\n", S.nVars());
|
||||
printf("c | Number of clauses: %12d |\n", S.nClauses());
|
||||
}
|
||||
|
||||
if (pPars->pre)
|
||||
S.eliminate(true);
|
||||
|
||||
vec<Lit> dummy;
|
||||
lbool ret = S.solveLimited(dummy);
|
||||
|
||||
if ( pPars->verb ) glucose_print_stats(S, Abc_Clock() - clk);
|
||||
printf(ret == l_True ? "SATISFIABLE" : ret == l_False ? "UNSATISFIABLE" : "INDETERMINATE");
|
||||
Abc_PrintTime( 1, " Time", Abc_Clock() - clk );
|
||||
|
||||
// port counterexample
|
||||
if (ret == l_True)
|
||||
{
|
||||
Gia_Obj_t * pObj; int i;
|
||||
p->pCexComb = Abc_CexAlloc(0,Gia_ManCiNum(p),1);
|
||||
Gia_ManForEachCi( p, pObj, i )
|
||||
{
|
||||
assert(Vec_IntEntry(vCnfIds,Gia_ObjId(p, pObj))!=-1);
|
||||
if (S.model[Vec_IntEntry(vCnfIds,Gia_ObjId(p, pObj))] == l_True)
|
||||
Abc_InfoSetBit( p->pCexComb->pData, i);
|
||||
}
|
||||
}
|
||||
Vec_IntFree(vCnfIds);
|
||||
return (ret == l_True ? 10 : ret == l_False ? 20 : 0);
|
||||
}
|
||||
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
/// END OF FILE ///
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
|
||||
}
|
||||
|
||||
ABC_NAMESPACE_IMPL_END
|
||||
|
|
@ -0,0 +1,76 @@
|
|||
/**CFile****************************************************************
|
||||
|
||||
FileName [AbcGlucose.h]
|
||||
|
||||
SystemName [ABC: Logic synthesis and verification system.]
|
||||
|
||||
PackageName [SAT solver Glucose 3.0.]
|
||||
|
||||
Synopsis [Interface to Glucose.]
|
||||
|
||||
Author [Alan Mishchenko]
|
||||
|
||||
Affiliation [UC Berkeley]
|
||||
|
||||
Date [Ver. 1.0. Started - September 6, 2017.]
|
||||
|
||||
Revision [$Id: AbcGlucose.h,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
|
||||
|
||||
***********************************************************************/
|
||||
|
||||
#ifndef SRC_EXTSAT_GLUCOSE_ABC_H_
|
||||
#define SRC_EXTSAT_GLUCOSE_ABC_H_
|
||||
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
/// INCLUDES ///
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
|
||||
#include "aig/gia/gia.h"
|
||||
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
/// PARAMETERS ///
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
|
||||
ABC_NAMESPACE_HEADER_START
|
||||
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
/// BASIC TYPES ///
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
|
||||
typedef struct ExtSat_Pars_ ExtSat_Pars;
|
||||
struct ExtSat_Pars_ {
|
||||
int pre; // preprocessing
|
||||
int verb; // verbosity
|
||||
int cust; // customizable
|
||||
int nConfls; // conflict limit (0 = no limit)
|
||||
};
|
||||
|
||||
static inline ExtSat_Pars ExtSat_CreatePars(int p, int v, int c, int nConfls)
|
||||
{
|
||||
ExtSat_Pars pars;
|
||||
pars.pre = p;
|
||||
pars.verb = v;
|
||||
pars.cust = c;
|
||||
pars.nConfls = nConfls;
|
||||
return pars;
|
||||
}
|
||||
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
/// MACRO DEFINITIONS ///
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
/// FUNCTION DECLARATIONS ///
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
|
||||
extern void Glucose_SolveCnf( char * pFilename, ExtSat_Pars * pPars );
|
||||
extern int Glucose_SolveAig( Gia_Man_t * p, ExtSat_Pars * pPars );
|
||||
|
||||
ABC_NAMESPACE_HEADER_END
|
||||
|
||||
#endif
|
||||
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
/// END OF FILE ///
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
|
||||
|
|
@ -0,0 +1,146 @@
|
|||
/**CFile****************************************************************
|
||||
|
||||
FileName [AbcGlucoseCmd.cpp]
|
||||
|
||||
SystemName [ABC: Logic synthesis and verification system.]
|
||||
|
||||
PackageName [SAT solver Glucose 3.0.]
|
||||
|
||||
Synopsis [Interface to Glucose.]
|
||||
|
||||
Author [Alan Mishchenko]
|
||||
|
||||
Affiliation [UC Berkeley]
|
||||
|
||||
Date [Ver. 1.0. Started - September 6, 2017.]
|
||||
|
||||
Revision [$Id: AbcGlucoseCmd.cpp,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
|
||||
|
||||
***********************************************************************/
|
||||
|
||||
#include "aig/gia/gia.h"
|
||||
#include "base/main/mainInt.h"
|
||||
|
||||
#include "sat/glucose/AbcGlucose.h"
|
||||
|
||||
ABC_NAMESPACE_IMPL_START
|
||||
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
/// DECLARATIONS ///
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
|
||||
static int Abc_CommandGlucose( Abc_Frame_t * pAbc, int argc, char ** argv );
|
||||
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
/// FUNCTION DEFINITIONS ///
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
|
||||
/**Function*************************************************************
|
||||
|
||||
Synopsis []
|
||||
|
||||
Description []
|
||||
|
||||
SideEffects []
|
||||
|
||||
SeeAlso []
|
||||
|
||||
***********************************************************************/
|
||||
extern "C" {
|
||||
|
||||
void Glucose_Init(Abc_Frame_t *pAbc)
|
||||
{
|
||||
Cmd_CommandAdd( pAbc, "ABC9", "&glucose", Abc_CommandGlucose, 0 );
|
||||
}
|
||||
|
||||
void Glucose_End( Abc_Frame_t * pAbc )
|
||||
{
|
||||
}
|
||||
|
||||
}
|
||||
|
||||
/**Function*************************************************************
|
||||
|
||||
Synopsis []
|
||||
|
||||
Description []
|
||||
|
||||
SideEffects []
|
||||
|
||||
SeeAlso []
|
||||
|
||||
***********************************************************************/
|
||||
int Abc_CommandGlucose( Abc_Frame_t * pAbc, int argc, char ** argv )
|
||||
{
|
||||
extern void Glucose_SolveCnf( char * pFilename, ExtSat_Pars * pPars );
|
||||
extern int Glucose_SolveAig( Gia_Man_t * p, ExtSat_Pars * pPars );
|
||||
|
||||
int c = 0;
|
||||
int pre = 1;
|
||||
int verb = 0;
|
||||
int nConfls = 0;
|
||||
|
||||
Extra_UtilGetoptReset();
|
||||
while ( ( c = Extra_UtilGetopt( argc, argv, "Cpvh" ) ) != EOF )
|
||||
{
|
||||
switch ( c )
|
||||
{
|
||||
case 'C':
|
||||
if ( globalUtilOptind >= argc )
|
||||
{
|
||||
Abc_Print( -1, "Command line switch \"-C\" should be followed by an integer.\n" );
|
||||
goto usage;
|
||||
}
|
||||
nConfls = atoi(argv[globalUtilOptind]);
|
||||
globalUtilOptind++;
|
||||
if ( nConfls < 0 )
|
||||
goto usage;
|
||||
break;
|
||||
case 'p':
|
||||
pre ^= 1;
|
||||
break;
|
||||
case 'v':
|
||||
verb ^= 1;
|
||||
break;
|
||||
case 'h':
|
||||
goto usage;
|
||||
default:
|
||||
goto usage;
|
||||
}
|
||||
}
|
||||
|
||||
ExtSat_Pars pPars = ExtSat_CreatePars(pre,verb,0,nConfls);
|
||||
|
||||
if ( argc == globalUtilOptind + 1 )
|
||||
{
|
||||
Glucose_SolveCnf( argv[globalUtilOptind], &pPars );
|
||||
return 0;
|
||||
}
|
||||
|
||||
if ( pAbc->pGia == NULL )
|
||||
{
|
||||
Abc_Print( -1, "Abc_CommandGlucose(): There is no AIG.\n" );
|
||||
return 1;
|
||||
}
|
||||
|
||||
if ( Glucose_SolveAig( pAbc->pGia, &pPars ) == 10 )
|
||||
Abc_FrameReplaceCex( pAbc, &pAbc->pGia->pCexComb );
|
||||
|
||||
return 0;
|
||||
|
||||
usage:
|
||||
Abc_Print( -2, "usage: &glucose [-C num] [-pvh] <file.cnf>\n" );
|
||||
Abc_Print( -2, "\t run glucose\n" );
|
||||
Abc_Print( -2, "\t-C num : conflict limit [default = %d]\n", nConfls );
|
||||
Abc_Print( -2, "\t-p : enable preprocessing [default = %d]\n",pre);
|
||||
Abc_Print( -2, "\t-v : verbosity [default = %d]\n",verb);
|
||||
Abc_Print( -2, "\t-h : print the command usage\n");
|
||||
Abc_Print( -2, "\t<file.cnf> : (optional) CNF file to solve\n");
|
||||
return 1;
|
||||
}
|
||||
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
/// END OF FILE ///
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
|
||||
ABC_NAMESPACE_IMPL_END
|
||||
|
|
@ -0,0 +1,84 @@
|
|||
/*******************************************************************************************[Alg.h]
|
||||
Copyright (c) 2003-2006, Niklas Een, Niklas Sorensson
|
||||
Copyright (c) 2007-2010, Niklas Sorensson
|
||||
|
||||
Permission is hereby granted, free of charge, to any person obtaining a copy of this software and
|
||||
associated documentation files (the "Software"), to deal in the Software without restriction,
|
||||
including without limitation the rights to use, copy, modify, merge, publish, distribute,
|
||||
sublicense, and/or sell copies of the Software, and to permit persons to whom the Software is
|
||||
furnished to do so, subject to the following conditions:
|
||||
|
||||
The above copyright notice and this permission notice shall be included in all copies or
|
||||
substantial portions of the Software.
|
||||
|
||||
THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR IMPLIED, INCLUDING BUT
|
||||
NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND
|
||||
NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM,
|
||||
DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT
|
||||
OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
|
||||
**************************************************************************************************/
|
||||
|
||||
#ifndef Glucose_Alg_h
|
||||
#define Glucose_Alg_h
|
||||
|
||||
#include "sat/glucose/Vec.h"
|
||||
|
||||
namespace Glucose {
|
||||
|
||||
//=================================================================================================
|
||||
// Useful functions on vector-like types:
|
||||
|
||||
//=================================================================================================
|
||||
// Removing and searching for elements:
|
||||
//
|
||||
|
||||
template<class V, class T>
|
||||
static inline void remove(V& ts, const T& t)
|
||||
{
|
||||
int j = 0;
|
||||
for (; j < ts.size() && ts[j] != t; j++);
|
||||
assert(j < ts.size());
|
||||
for (; j < ts.size()-1; j++) ts[j] = ts[j+1];
|
||||
ts.pop();
|
||||
}
|
||||
|
||||
|
||||
template<class V, class T>
|
||||
static inline bool find(V& ts, const T& t)
|
||||
{
|
||||
int j = 0;
|
||||
for (; j < ts.size() && ts[j] != t; j++);
|
||||
return j < ts.size();
|
||||
}
|
||||
|
||||
|
||||
//=================================================================================================
|
||||
// Copying vectors with support for nested vector types:
|
||||
//
|
||||
|
||||
// Base case:
|
||||
template<class T>
|
||||
static inline void copy(const T& from, T& to)
|
||||
{
|
||||
to = from;
|
||||
}
|
||||
|
||||
// Recursive case:
|
||||
template<class T>
|
||||
static inline void copy(const vec<T>& from, vec<T>& to, bool append = false)
|
||||
{
|
||||
if (!append)
|
||||
to.clear();
|
||||
for (int i = 0; i < from.size(); i++){
|
||||
to.push();
|
||||
copy(from[i], to.last());
|
||||
}
|
||||
}
|
||||
|
||||
template<class T>
|
||||
static inline void append(const vec<T>& from, vec<T>& to){ copy(from, to, true); }
|
||||
|
||||
//=================================================================================================
|
||||
}
|
||||
|
||||
#endif
|
||||
|
|
@ -0,0 +1,131 @@
|
|||
/*****************************************************************************************[Alloc.h]
|
||||
Copyright (c) 2008-2010, Niklas Sorensson
|
||||
|
||||
Permission is hereby granted, free of charge, to any person obtaining a copy of this software and
|
||||
associated documentation files (the "Software"), to deal in the Software without restriction,
|
||||
including without limitation the rights to use, copy, modify, merge, publish, distribute,
|
||||
sublicense, and/or sell copies of the Software, and to permit persons to whom the Software is
|
||||
furnished to do so, subject to the following conditions:
|
||||
|
||||
The above copyright notice and this permission notice shall be included in all copies or
|
||||
substantial portions of the Software.
|
||||
|
||||
THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR IMPLIED, INCLUDING BUT
|
||||
NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND
|
||||
NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM,
|
||||
DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT
|
||||
OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
|
||||
**************************************************************************************************/
|
||||
|
||||
|
||||
#ifndef Glucose_Alloc_h
|
||||
#define Glucose_Alloc_h
|
||||
|
||||
#include "sat/glucose/XAlloc.h"
|
||||
#include "sat/glucose/Vec.h"
|
||||
|
||||
namespace Glucose {
|
||||
|
||||
//=================================================================================================
|
||||
// Simple Region-based memory allocator:
|
||||
|
||||
template<class T>
|
||||
class RegionAllocator
|
||||
{
|
||||
T* memory;
|
||||
uint32_t sz;
|
||||
uint32_t cap;
|
||||
uint32_t wasted_;
|
||||
|
||||
void capacity(uint32_t min_cap);
|
||||
|
||||
public:
|
||||
// TODO: make this a class for better type-checking?
|
||||
typedef uint32_t Ref;
|
||||
enum { Ref_Undef = UINT32_MAX };
|
||||
enum { Unit_Size = sizeof(uint32_t) };
|
||||
|
||||
explicit RegionAllocator(uint32_t start_cap = 1024*1024) : memory(NULL), sz(0), cap(0), wasted_(0){ capacity(start_cap); }
|
||||
~RegionAllocator()
|
||||
{
|
||||
if (memory != NULL)
|
||||
::free(memory);
|
||||
}
|
||||
|
||||
|
||||
uint32_t size () const { return sz; }
|
||||
uint32_t wasted () const { return wasted_; }
|
||||
|
||||
Ref alloc (int size);
|
||||
void free_ (int size) { wasted_ += size; }
|
||||
|
||||
// Deref, Load Effective Address (LEA), Inverse of LEA (AEL):
|
||||
T& operator[](Ref r) { assert(r >= 0 && r < sz); return memory[r]; }
|
||||
const T& operator[](Ref r) const { assert(r >= 0 && r < sz); return memory[r]; }
|
||||
|
||||
T* lea (Ref r) { assert(r >= 0 && r < sz); return &memory[r]; }
|
||||
const T* lea (Ref r) const { assert(r >= 0 && r < sz); return &memory[r]; }
|
||||
Ref ael (const T* t) { assert((void*)t >= (void*)&memory[0] && (void*)t < (void*)&memory[sz-1]);
|
||||
return (Ref)(t - &memory[0]); }
|
||||
|
||||
void moveTo(RegionAllocator& to) {
|
||||
if (to.memory != NULL) ::free(to.memory);
|
||||
to.memory = memory;
|
||||
to.sz = sz;
|
||||
to.cap = cap;
|
||||
to.wasted_ = wasted_;
|
||||
|
||||
memory = NULL;
|
||||
sz = cap = wasted_ = 0;
|
||||
}
|
||||
|
||||
|
||||
};
|
||||
|
||||
template<class T>
|
||||
void RegionAllocator<T>::capacity(uint32_t min_cap)
|
||||
{
|
||||
if (cap >= min_cap) return;
|
||||
|
||||
uint32_t prev_cap = cap;
|
||||
while (cap < min_cap){
|
||||
// NOTE: Multiply by a factor (13/8) without causing overflow, then add 2 and make the
|
||||
// result even by clearing the least significant bit. The resulting sequence of capacities
|
||||
// is carefully chosen to hit a maximum capacity that is close to the '2^32-1' limit when
|
||||
// using 'uint32_t' as indices so that as much as possible of this space can be used.
|
||||
uint32_t delta = ((cap >> 1) + (cap >> 3) + 2) & ~1;
|
||||
cap += delta;
|
||||
|
||||
if (cap <= prev_cap)
|
||||
throw OutOfMemoryException();
|
||||
}
|
||||
//printf(" .. (%p) cap = %u\n", this, cap);
|
||||
|
||||
assert(cap > 0);
|
||||
memory = (T*)xrealloc(memory, sizeof(T)*cap);
|
||||
}
|
||||
|
||||
|
||||
template<class T>
|
||||
typename RegionAllocator<T>::Ref
|
||||
RegionAllocator<T>::alloc(int size)
|
||||
{
|
||||
//printf("ALLOC called (this = %p, size = %d)\n", this, size); fflush(stdout);
|
||||
assert(size > 0);
|
||||
capacity(sz + size);
|
||||
|
||||
uint32_t prev_sz = sz;
|
||||
sz += size;
|
||||
|
||||
// Handle overflow:
|
||||
if (sz < prev_sz)
|
||||
throw OutOfMemoryException();
|
||||
|
||||
return prev_sz;
|
||||
}
|
||||
|
||||
|
||||
//=================================================================================================
|
||||
}
|
||||
|
||||
#endif
|
||||
|
|
@ -0,0 +1,110 @@
|
|||
/***********************************************************************************[BoundedQueue.h]
|
||||
Glucose -- Copyright (c) 2009, Gilles Audemard, Laurent Simon
|
||||
CRIL - Univ. Artois, France
|
||||
LRI - Univ. Paris Sud, France
|
||||
|
||||
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.
|
||||
**************************************************************************************************/
|
||||
|
||||
|
||||
#ifndef BoundedQueue_h
|
||||
#define BoundedQueue_h
|
||||
|
||||
#include "sat/glucose/Vec.h"
|
||||
|
||||
//=================================================================================================
|
||||
|
||||
namespace Glucose {
|
||||
|
||||
template <class T>
|
||||
class bqueue {
|
||||
vec<T> elems;
|
||||
int first;
|
||||
int last;
|
||||
uint64_t sumofqueue;
|
||||
int maxsize;
|
||||
int queuesize; // Number of current elements (must be < maxsize !)
|
||||
bool expComputed;
|
||||
double exp,value;
|
||||
public:
|
||||
bqueue(void) : first(0), last(0), sumofqueue(0), maxsize(0), queuesize(0),expComputed(false) { }
|
||||
|
||||
void initSize(int size) {growTo(size);exp = 2.0/(size+1);} // Init size of bounded size queue
|
||||
|
||||
void push(T x) {
|
||||
expComputed = false;
|
||||
if (queuesize==maxsize) {
|
||||
assert(last==first); // The queue is full, next value to enter will replace oldest one
|
||||
sumofqueue -= elems[last];
|
||||
if ((++last) == maxsize) last = 0;
|
||||
} else
|
||||
queuesize++;
|
||||
sumofqueue += x;
|
||||
elems[first] = x;
|
||||
if ((++first) == maxsize) {first = 0;last = 0;}
|
||||
}
|
||||
|
||||
T peek() { assert(queuesize>0); return elems[last]; }
|
||||
void pop() {sumofqueue-=elems[last]; queuesize--; if ((++last) == maxsize) last = 0;}
|
||||
|
||||
uint64_t getsum() const {return sumofqueue;}
|
||||
unsigned int getavg() const {return (unsigned int)(sumofqueue/((uint64_t)queuesize));}
|
||||
int maxSize() const {return maxsize;}
|
||||
double getavgDouble() const {
|
||||
double tmp = 0;
|
||||
for(int i=0;i<elems.size();i++) {
|
||||
tmp+=elems[i];
|
||||
}
|
||||
return tmp/elems.size();
|
||||
}
|
||||
int isvalid() const {return (queuesize==maxsize);}
|
||||
|
||||
void growTo(int size) {
|
||||
elems.growTo(size);
|
||||
first=0; maxsize=size; queuesize = 0;last = 0;
|
||||
for(int i=0;i<size;i++) elems[i]=0;
|
||||
}
|
||||
|
||||
double getAvgExp() {
|
||||
if(expComputed) return value;
|
||||
double a=exp;
|
||||
value = elems[first];
|
||||
for(int i = first;i<maxsize;i++) {
|
||||
value+=a*((double)elems[i]);
|
||||
a=a*exp;
|
||||
}
|
||||
for(int i = 0;i<last;i++) {
|
||||
value+=a*((double)elems[i]);
|
||||
a=a*exp;
|
||||
}
|
||||
value = value*(1-exp)/(1-a);
|
||||
expComputed = true;
|
||||
return value;
|
||||
|
||||
|
||||
}
|
||||
void fastclear() {first = 0; last = 0; queuesize=0; sumofqueue=0;} // to be called after restarts... Discard the queue
|
||||
|
||||
int size(void) { return queuesize; }
|
||||
|
||||
void clear(bool dealloc = false) { elems.clear(dealloc); first = 0; maxsize=0; queuesize=0;sumofqueue=0;}
|
||||
|
||||
|
||||
};
|
||||
}
|
||||
//=================================================================================================
|
||||
|
||||
#endif
|
||||
|
|
@ -0,0 +1,33 @@
|
|||
/************************************************************************************[Constants.h]
|
||||
Glucose -- Copyright (c) 2009, Gilles Audemard, Laurent Simon
|
||||
CRIL - Univ. Artois, France
|
||||
LRI - Univ. Paris Sud, France
|
||||
|
||||
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.
|
||||
**************************************************************************************************/
|
||||
|
||||
#define DYNAMICNBLEVEL
|
||||
#define CONSTANTREMOVECLAUSE
|
||||
#define UPDATEVARACTIVITY
|
||||
|
||||
// Constants for clauses reductions
|
||||
#define RATIOREMOVECLAUSES 2
|
||||
|
||||
|
||||
|
||||
// Constants for restarts
|
||||
#define LOWER_BOUND_FOR_BLOCKING_RESTART 10000
|
||||
|
||||
|
|
@ -0,0 +1,89 @@
|
|||
/****************************************************************************************[Dimacs.h]
|
||||
Copyright (c) 2003-2006, Niklas Een, Niklas Sorensson
|
||||
Copyright (c) 2007-2010, Niklas Sorensson
|
||||
|
||||
Permission is hereby granted, free of charge, to any person obtaining a copy of this software and
|
||||
associated documentation files (the "Software"), to deal in the Software without restriction,
|
||||
including without limitation the rights to use, copy, modify, merge, publish, distribute,
|
||||
sublicense, and/or sell copies of the Software, and to permit persons to whom the Software is
|
||||
furnished to do so, subject to the following conditions:
|
||||
|
||||
The above copyright notice and this permission notice shall be included in all copies or
|
||||
substantial portions of the Software.
|
||||
|
||||
THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR IMPLIED, INCLUDING BUT
|
||||
NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND
|
||||
NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM,
|
||||
DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT
|
||||
OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
|
||||
**************************************************************************************************/
|
||||
|
||||
#ifndef Glucose_Dimacs_h
|
||||
#define Glucose_Dimacs_h
|
||||
|
||||
#include <stdio.h>
|
||||
|
||||
#include "sat/glucose/ParseUtils.h"
|
||||
#include "sat/glucose/SolverTypes.h"
|
||||
|
||||
namespace Glucose {
|
||||
|
||||
//=================================================================================================
|
||||
// DIMACS Parser:
|
||||
|
||||
template<class B, class Solver>
|
||||
static void readClause(B& in, Solver& S, vec<Lit>& lits) {
|
||||
int parsed_lit, var;
|
||||
lits.clear();
|
||||
for (;;){
|
||||
parsed_lit = parseInt(in);
|
||||
if (parsed_lit == 0) break;
|
||||
var = abs(parsed_lit)-1;
|
||||
while (var >= S.nVars()) S.newVar();
|
||||
lits.push( (parsed_lit > 0) ? mkLit(var) : ~mkLit(var) );
|
||||
}
|
||||
}
|
||||
|
||||
template<class B, class Solver>
|
||||
static void parse_DIMACS_main(B& in, Solver& S) {
|
||||
vec<Lit> lits;
|
||||
int vars = 0;
|
||||
int clauses = 0;
|
||||
int cnt = 0;
|
||||
for (;;){
|
||||
skipWhitespace(in);
|
||||
if (*in == EOF) break;
|
||||
else if (*in == 'p'){
|
||||
if (eagerMatch(in, "p cnf")){
|
||||
vars = parseInt(in);
|
||||
clauses = parseInt(in);
|
||||
// SATRACE'06 hack
|
||||
// if (clauses > 4000000)
|
||||
// S.eliminate(true);
|
||||
}else{
|
||||
printf("PARSE ERROR! Unexpected char: %c\n", *in), exit(3);
|
||||
}
|
||||
} else if (*in == 'c' || *in == 'p')
|
||||
skipLine(in);
|
||||
else{
|
||||
cnt++;
|
||||
readClause(in, S, lits);
|
||||
S.addClause_(lits); }
|
||||
}
|
||||
if (vars != S.nVars())
|
||||
fprintf(stderr, "WARNING! DIMACS header mismatch: wrong number of variables.\n");
|
||||
if (cnt != clauses)
|
||||
fprintf(stderr, "WARNING! DIMACS header mismatch: wrong number of clauses.\n");
|
||||
}
|
||||
|
||||
// Inserts problem into solver.
|
||||
//
|
||||
template<class Solver>
|
||||
static void parse_DIMACS(gzFile input_stream, Solver& S) {
|
||||
StreamBuffer in(input_stream);
|
||||
parse_DIMACS_main(in, S); }
|
||||
|
||||
//=================================================================================================
|
||||
}
|
||||
|
||||
#endif
|
||||
File diff suppressed because it is too large
Load Diff
|
|
@ -0,0 +1,150 @@
|
|||
/******************************************************************************************[Heap.h]
|
||||
Copyright (c) 2003-2006, Niklas Een, Niklas Sorensson
|
||||
Copyright (c) 2007-2010, Niklas Sorensson
|
||||
|
||||
Permission is hereby granted, free of charge, to any person obtaining a copy of this software and
|
||||
associated documentation files (the "Software"), to deal in the Software without restriction,
|
||||
including without limitation the rights to use, copy, modify, merge, publish, distribute,
|
||||
sublicense, and/or sell copies of the Software, and to permit persons to whom the Software is
|
||||
furnished to do so, subject to the following conditions:
|
||||
|
||||
The above copyright notice and this permission notice shall be included in all copies or
|
||||
substantial portions of the Software.
|
||||
|
||||
THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR IMPLIED, INCLUDING BUT
|
||||
NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND
|
||||
NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM,
|
||||
DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT
|
||||
OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
|
||||
**************************************************************************************************/
|
||||
|
||||
#ifndef Glucose_Heap_h
|
||||
#define Glucose_Heap_h
|
||||
|
||||
#include "sat/glucose/Vec.h"
|
||||
|
||||
namespace Glucose {
|
||||
|
||||
//=================================================================================================
|
||||
// A heap implementation with support for decrease/increase key.
|
||||
|
||||
|
||||
template<class Comp>
|
||||
class Heap {
|
||||
Comp lt; // The heap is a minimum-heap with respect to this comparator
|
||||
vec<int> heap; // Heap of integers
|
||||
vec<int> indices; // Each integers position (index) in the Heap
|
||||
|
||||
// Index "traversal" functions
|
||||
static inline int left (int i) { return i*2+1; }
|
||||
static inline int right (int i) { return (i+1)*2; }
|
||||
static inline int parent(int i) { return (i-1) >> 1; }
|
||||
|
||||
|
||||
void percolateUp(int i)
|
||||
{
|
||||
int x = heap[i];
|
||||
int p = parent(i);
|
||||
|
||||
while (i != 0 && lt(x, heap[p])){
|
||||
heap[i] = heap[p];
|
||||
indices[heap[p]] = i;
|
||||
i = p;
|
||||
p = parent(p);
|
||||
}
|
||||
heap [i] = x;
|
||||
indices[x] = i;
|
||||
}
|
||||
|
||||
|
||||
void percolateDown(int i)
|
||||
{
|
||||
int x = heap[i];
|
||||
while (left(i) < heap.size()){
|
||||
int child = right(i) < heap.size() && lt(heap[right(i)], heap[left(i)]) ? right(i) : left(i);
|
||||
if (!lt(heap[child], x)) break;
|
||||
heap[i] = heap[child];
|
||||
indices[heap[i]] = i;
|
||||
i = child;
|
||||
}
|
||||
heap [i] = x;
|
||||
indices[x] = i;
|
||||
}
|
||||
|
||||
|
||||
public:
|
||||
Heap(const Comp& c) : lt(c) { }
|
||||
|
||||
int size () const { return heap.size(); }
|
||||
bool empty () const { return heap.size() == 0; }
|
||||
bool inHeap (int n) const { return n < indices.size() && indices[n] >= 0; }
|
||||
int operator[](int index) const { assert(index < heap.size()); return heap[index]; }
|
||||
|
||||
|
||||
void decrease (int n) { assert(inHeap(n)); percolateUp (indices[n]); }
|
||||
void increase (int n) { assert(inHeap(n)); percolateDown(indices[n]); }
|
||||
|
||||
|
||||
// Safe variant of insert/decrease/increase:
|
||||
void update(int n)
|
||||
{
|
||||
if (!inHeap(n))
|
||||
insert(n);
|
||||
else {
|
||||
percolateUp(indices[n]);
|
||||
percolateDown(indices[n]); }
|
||||
}
|
||||
|
||||
|
||||
void insert(int n)
|
||||
{
|
||||
indices.growTo(n+1, -1);
|
||||
assert(!inHeap(n));
|
||||
|
||||
indices[n] = heap.size();
|
||||
heap.push(n);
|
||||
percolateUp(indices[n]);
|
||||
}
|
||||
|
||||
|
||||
int removeMin()
|
||||
{
|
||||
int x = heap[0];
|
||||
heap[0] = heap.last();
|
||||
indices[heap[0]] = 0;
|
||||
indices[x] = -1;
|
||||
heap.pop();
|
||||
if (heap.size() > 1) percolateDown(0);
|
||||
return x;
|
||||
}
|
||||
|
||||
|
||||
// Rebuild the heap from scratch, using the elements in 'ns':
|
||||
void build(vec<int>& ns) {
|
||||
int i;
|
||||
for (i = 0; i < heap.size(); i++)
|
||||
indices[heap[i]] = -1;
|
||||
heap.clear();
|
||||
|
||||
for (i = 0; i < ns.size(); i++){
|
||||
indices[ns[i]] = i;
|
||||
heap.push(ns[i]); }
|
||||
|
||||
for (i = heap.size() / 2 - 1; i >= 0; i--)
|
||||
percolateDown(i);
|
||||
}
|
||||
|
||||
void clear(bool dealloc = false)
|
||||
{
|
||||
int i;
|
||||
for (i = 0; i < heap.size(); i++)
|
||||
indices[heap[i]] = -1;
|
||||
heap.clear(dealloc);
|
||||
}
|
||||
};
|
||||
|
||||
|
||||
//=================================================================================================
|
||||
}
|
||||
|
||||
#endif
|
||||
|
|
@ -0,0 +1,47 @@
|
|||
/**************************************************************************************[IntTypes.h]
|
||||
Copyright (c) 2009-2010, Niklas Sorensson
|
||||
|
||||
Permission is hereby granted, free of charge, to any person obtaining a copy of this software and
|
||||
associated documentation files (the "Software"), to deal in the Software without restriction,
|
||||
including without limitation the rights to use, copy, modify, merge, publish, distribute,
|
||||
sublicense, and/or sell copies of the Software, and to permit persons to whom the Software is
|
||||
furnished to do so, subject to the following conditions:
|
||||
|
||||
The above copyright notice and this permission notice shall be included in all copies or
|
||||
substantial portions of the Software.
|
||||
|
||||
THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR IMPLIED, INCLUDING BUT
|
||||
NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND
|
||||
NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM,
|
||||
DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT
|
||||
OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
|
||||
**************************************************************************************************/
|
||||
|
||||
#ifndef Glucose_IntTypes_h
|
||||
#define Glucose_IntTypes_h
|
||||
|
||||
#ifdef __sun
|
||||
// Not sure if there are newer versions that support C99 headers. The
|
||||
// needed features are implemented in the headers below though:
|
||||
|
||||
# include <sys/int_types.h>
|
||||
# include <sys/int_fmtio.h>
|
||||
# include <sys/int_limits.h>
|
||||
|
||||
#else
|
||||
|
||||
#define __STDC_LIMIT_MACROS
|
||||
# include "pstdint.h"
|
||||
//# include <inttypes.h>
|
||||
|
||||
#endif
|
||||
|
||||
#include <limits.h>
|
||||
|
||||
#ifndef PRIu64
|
||||
#define PRIu64 "lu"
|
||||
#define PRIi64 "ld"
|
||||
#endif
|
||||
//=================================================================================================
|
||||
|
||||
#endif
|
||||
|
|
@ -0,0 +1,193 @@
|
|||
/*******************************************************************************************[Map.h]
|
||||
Copyright (c) 2006-2010, Niklas Sorensson
|
||||
|
||||
Permission is hereby granted, free of charge, to any person obtaining a copy of this software and
|
||||
associated documentation files (the "Software"), to deal in the Software without restriction,
|
||||
including without limitation the rights to use, copy, modify, merge, publish, distribute,
|
||||
sublicense, and/or sell copies of the Software, and to permit persons to whom the Software is
|
||||
furnished to do so, subject to the following conditions:
|
||||
|
||||
The above copyright notice and this permission notice shall be included in all copies or
|
||||
substantial portions of the Software.
|
||||
|
||||
THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR IMPLIED, INCLUDING BUT
|
||||
NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND
|
||||
NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM,
|
||||
DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT
|
||||
OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
|
||||
**************************************************************************************************/
|
||||
|
||||
#ifndef Glucose_Map_h
|
||||
#define Glucose_Map_h
|
||||
|
||||
#include "sat/glucose/IntTypes.h"
|
||||
#include "sat/glucose/Vec.h"
|
||||
|
||||
namespace Glucose {
|
||||
|
||||
//=================================================================================================
|
||||
// Default hash/equals functions
|
||||
//
|
||||
|
||||
template<class K> struct Hash { uint32_t operator()(const K& k) const { return hash(k); } };
|
||||
template<class K> struct Equal { bool operator()(const K& k1, const K& k2) const { return k1 == k2; } };
|
||||
|
||||
template<class K> struct DeepHash { uint32_t operator()(const K* k) const { return hash(*k); } };
|
||||
template<class K> struct DeepEqual { bool operator()(const K* k1, const K* k2) const { return *k1 == *k2; } };
|
||||
|
||||
static inline uint32_t hash(uint32_t x){ return x; }
|
||||
static inline uint32_t hash(uint64_t x){ return (uint32_t)x; }
|
||||
static inline uint32_t hash(int32_t x) { return (uint32_t)x; }
|
||||
static inline uint32_t hash(int64_t x) { return (uint32_t)x; }
|
||||
|
||||
|
||||
//=================================================================================================
|
||||
// Some primes
|
||||
//
|
||||
|
||||
static const int nprimes = 25;
|
||||
static const int primes [nprimes] = { 31, 73, 151, 313, 643, 1291, 2593, 5233, 10501, 21013, 42073, 84181, 168451, 337219, 674701, 1349473, 2699299, 5398891, 10798093, 21596719, 43193641, 86387383, 172775299, 345550609, 691101253 };
|
||||
|
||||
//=================================================================================================
|
||||
// Hash table implementation of Maps
|
||||
//
|
||||
|
||||
template<class K, class D, class H = Hash<K>, class E = Equal<K> >
|
||||
class Map {
|
||||
public:
|
||||
struct Pair { K key; D data; };
|
||||
|
||||
private:
|
||||
H hash;
|
||||
E equals;
|
||||
|
||||
vec<Pair>* table;
|
||||
int cap;
|
||||
int size;
|
||||
|
||||
// Don't allow copying (error prone):
|
||||
Map<K,D,H,E>& operator = (Map<K,D,H,E>& other) { assert(0); }
|
||||
Map (Map<K,D,H,E>& other) { assert(0); }
|
||||
|
||||
bool checkCap(int new_size) const { return new_size > cap; }
|
||||
|
||||
int32_t index (const K& k) const { return hash(k) % cap; }
|
||||
void _insert (const K& k, const D& d) {
|
||||
vec<Pair>& ps = table[index(k)];
|
||||
ps.push(); ps.last().key = k; ps.last().data = d; }
|
||||
|
||||
void rehash () {
|
||||
const vec<Pair>* old = table;
|
||||
|
||||
int old_cap = cap;
|
||||
int newsize = primes[0];
|
||||
for (int i = 1; newsize <= cap && i < nprimes; i++)
|
||||
newsize = primes[i];
|
||||
|
||||
table = new vec<Pair>[newsize];
|
||||
cap = newsize;
|
||||
|
||||
for (int i = 0; i < old_cap; i++){
|
||||
for (int j = 0; j < old[i].size(); j++){
|
||||
_insert(old[i][j].key, old[i][j].data); }}
|
||||
|
||||
delete [] old;
|
||||
|
||||
// printf(" --- rehashing, old-cap=%d, new-cap=%d\n", cap, newsize);
|
||||
}
|
||||
|
||||
|
||||
public:
|
||||
|
||||
Map () : table(NULL), cap(0), size(0) {}
|
||||
Map (const H& h, const E& e) : hash(h), equals(e), table(NULL), cap(0), size(0){}
|
||||
~Map () { delete [] table; }
|
||||
|
||||
// PRECONDITION: the key must already exist in the map.
|
||||
const D& operator [] (const K& k) const
|
||||
{
|
||||
assert(size != 0);
|
||||
const D* res = NULL;
|
||||
const vec<Pair>& ps = table[index(k)];
|
||||
for (int i = 0; i < ps.size(); i++)
|
||||
if (equals(ps[i].key, k))
|
||||
res = &ps[i].data;
|
||||
assert(res != NULL);
|
||||
return *res;
|
||||
}
|
||||
|
||||
// PRECONDITION: the key must already exist in the map.
|
||||
D& operator [] (const K& k)
|
||||
{
|
||||
assert(size != 0);
|
||||
D* res = NULL;
|
||||
vec<Pair>& ps = table[index(k)];
|
||||
for (int i = 0; i < ps.size(); i++)
|
||||
if (equals(ps[i].key, k))
|
||||
res = &ps[i].data;
|
||||
assert(res != NULL);
|
||||
return *res;
|
||||
}
|
||||
|
||||
// PRECONDITION: the key must *NOT* exist in the map.
|
||||
void insert (const K& k, const D& d) { if (checkCap(size+1)) rehash(); _insert(k, d); size++; }
|
||||
bool peek (const K& k, D& d) const {
|
||||
if (size == 0) return false;
|
||||
const vec<Pair>& ps = table[index(k)];
|
||||
for (int i = 0; i < ps.size(); i++)
|
||||
if (equals(ps[i].key, k)){
|
||||
d = ps[i].data;
|
||||
return true; }
|
||||
return false;
|
||||
}
|
||||
|
||||
bool has (const K& k) const {
|
||||
if (size == 0) return false;
|
||||
const vec<Pair>& ps = table[index(k)];
|
||||
for (int i = 0; i < ps.size(); i++)
|
||||
if (equals(ps[i].key, k))
|
||||
return true;
|
||||
return false;
|
||||
}
|
||||
|
||||
// PRECONDITION: the key must exist in the map.
|
||||
void remove(const K& k) {
|
||||
assert(table != NULL);
|
||||
vec<Pair>& ps = table[index(k)];
|
||||
int j = 0;
|
||||
for (; j < ps.size() && !equals(ps[j].key, k); j++);
|
||||
assert(j < ps.size());
|
||||
ps[j] = ps.last();
|
||||
ps.pop();
|
||||
size--;
|
||||
}
|
||||
|
||||
void clear () {
|
||||
cap = size = 0;
|
||||
delete [] table;
|
||||
table = NULL;
|
||||
}
|
||||
|
||||
int elems() const { return size; }
|
||||
int bucket_count() const { return cap; }
|
||||
|
||||
// NOTE: the hash and equality objects are not moved by this method:
|
||||
void moveTo(Map& other){
|
||||
delete [] other.table;
|
||||
|
||||
other.table = table;
|
||||
other.cap = cap;
|
||||
other.size = size;
|
||||
|
||||
table = NULL;
|
||||
size = cap = 0;
|
||||
}
|
||||
|
||||
// NOTE: given a bit more time, I could make a more C++-style iterator out of this:
|
||||
const vec<Pair>& bucket(int i) const { return table[i]; }
|
||||
};
|
||||
|
||||
//=================================================================================================
|
||||
}
|
||||
|
||||
#endif
|
||||
|
|
@ -0,0 +1,91 @@
|
|||
/**************************************************************************************[Options.cc]
|
||||
Copyright (c) 2008-2010, Niklas Sorensson
|
||||
|
||||
Permission is hereby granted, free of charge, to any person obtaining a copy of this software and
|
||||
associated documentation files (the "Software"), to deal in the Software without restriction,
|
||||
including without limitation the rights to use, copy, modify, merge, publish, distribute,
|
||||
sublicense, and/or sell copies of the Software, and to permit persons to whom the Software is
|
||||
furnished to do so, subject to the following conditions:
|
||||
|
||||
The above copyright notice and this permission notice shall be included in all copies or
|
||||
substantial portions of the Software.
|
||||
|
||||
THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR IMPLIED, INCLUDING BUT
|
||||
NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND
|
||||
NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM,
|
||||
DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT
|
||||
OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
|
||||
**************************************************************************************************/
|
||||
|
||||
#include "sat/glucose/Sort.h"
|
||||
#include "sat/glucose/Options.h"
|
||||
#include "sat/glucose/ParseUtils.h"
|
||||
|
||||
using namespace Glucose;
|
||||
|
||||
void Glucose::parseOptions(int& argc, char** argv, bool strict)
|
||||
{
|
||||
int i, j;
|
||||
for (i = j = 1; i < argc; i++){
|
||||
const char* str = argv[i];
|
||||
if (match(str, "--") && match(str, Option::getHelpPrefixString()) && match(str, "help")){
|
||||
if (*str == '\0')
|
||||
printUsageAndExit(argc, argv);
|
||||
else if (match(str, "-verb"))
|
||||
printUsageAndExit(argc, argv, true);
|
||||
} else {
|
||||
bool parsed_ok = false;
|
||||
|
||||
for (int k = 0; !parsed_ok && k < Option::getOptionList().size(); k++){
|
||||
parsed_ok = Option::getOptionList()[k]->parse(argv[i]);
|
||||
|
||||
// fprintf(stderr, "checking %d: %s against flag <%s> (%s)\n", i, argv[i], Option::getOptionList()[k]->name, parsed_ok ? "ok" : "skip");
|
||||
}
|
||||
|
||||
if (!parsed_ok)
|
||||
if (strict && match(argv[i], "-"))
|
||||
fprintf(stderr, "ERROR! Unknown flag \"%s\". Use '--%shelp' for help.\n", argv[i], Option::getHelpPrefixString()), exit(1);
|
||||
else
|
||||
argv[j++] = argv[i];
|
||||
}
|
||||
}
|
||||
|
||||
argc -= (i - j);
|
||||
}
|
||||
|
||||
|
||||
void Glucose::setUsageHelp (const char* str){ Option::getUsageString() = str; }
|
||||
void Glucose::setHelpPrefixStr (const char* str){ Option::getHelpPrefixString() = str; }
|
||||
void Glucose::printUsageAndExit (int argc, char** argv, bool verbose)
|
||||
{
|
||||
const char* usage = Option::getUsageString();
|
||||
if (usage != NULL)
|
||||
fprintf(stderr, usage, argv[0]);
|
||||
|
||||
sort(Option::getOptionList(), Option::OptionLt());
|
||||
|
||||
const char* prev_cat = NULL;
|
||||
const char* prev_type = NULL;
|
||||
|
||||
for (int i = 0; i < Option::getOptionList().size(); i++){
|
||||
const char* cat = Option::getOptionList()[i]->category;
|
||||
const char* type = Option::getOptionList()[i]->type_name;
|
||||
|
||||
if (cat != prev_cat)
|
||||
fprintf(stderr, "\n%s OPTIONS:\n\n", cat);
|
||||
else if (type != prev_type)
|
||||
fprintf(stderr, "\n");
|
||||
|
||||
Option::getOptionList()[i]->help(verbose);
|
||||
|
||||
prev_cat = Option::getOptionList()[i]->category;
|
||||
prev_type = Option::getOptionList()[i]->type_name;
|
||||
}
|
||||
|
||||
fprintf(stderr, "\nHELP OPTIONS:\n\n");
|
||||
fprintf(stderr, " --%shelp Print help message.\n", Option::getHelpPrefixString());
|
||||
fprintf(stderr, " --%shelp-verb Print verbose help message.\n", Option::getHelpPrefixString());
|
||||
fprintf(stderr, "\n");
|
||||
exit(0);
|
||||
}
|
||||
|
||||
|
|
@ -0,0 +1,388 @@
|
|||
/***************************************************************************************[Options.h]
|
||||
Copyright (c) 2008-2010, Niklas Sorensson
|
||||
|
||||
Permission is hereby granted, free of charge, to any person obtaining a copy of this software and
|
||||
associated documentation files (the "Software"), to deal in the Software without restriction,
|
||||
including without limitation the rights to use, copy, modify, merge, publish, distribute,
|
||||
sublicense, and/or sell copies of the Software, and to permit persons to whom the Software is
|
||||
furnished to do so, subject to the following conditions:
|
||||
|
||||
The above copyright notice and this permission notice shall be included in all copies or
|
||||
substantial portions of the Software.
|
||||
|
||||
THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR IMPLIED, INCLUDING BUT
|
||||
NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND
|
||||
NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM,
|
||||
DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT
|
||||
OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
|
||||
**************************************************************************************************/
|
||||
|
||||
#ifndef Glucose_Options_h
|
||||
#define Glucose_Options_h
|
||||
|
||||
#define __STDC_FORMAT_MACROS
|
||||
|
||||
#include <stdlib.h>
|
||||
#include <stdio.h>
|
||||
#include <math.h>
|
||||
#include <string.h>
|
||||
|
||||
#include "sat/glucose/IntTypes.h"
|
||||
#include "sat/glucose/Vec.h"
|
||||
#include "sat/glucose/ParseUtils.h"
|
||||
|
||||
namespace Glucose {
|
||||
|
||||
//==================================================================================================
|
||||
// Top-level option parse/help functions:
|
||||
|
||||
|
||||
extern void parseOptions (int& argc, char** argv, bool strict = false);
|
||||
extern void printUsageAndExit(int argc, char** argv, bool verbose = false);
|
||||
extern void setUsageHelp (const char* str);
|
||||
extern void setHelpPrefixStr (const char* str);
|
||||
|
||||
|
||||
//==================================================================================================
|
||||
// Options is an abstract class that gives the interface for all types options:
|
||||
|
||||
|
||||
class Option
|
||||
{
|
||||
public:
|
||||
const char* name;
|
||||
const char* description;
|
||||
const char* category;
|
||||
const char* type_name;
|
||||
|
||||
static vec<Option*>& getOptionList () { static vec<Option*> options; return options; }
|
||||
static const char*& getUsageString() { static const char* usage_str; return usage_str; }
|
||||
static const char*& getHelpPrefixString() { static const char* help_prefix_str = ""; return help_prefix_str; }
|
||||
|
||||
struct OptionLt {
|
||||
bool operator()(const Option* x, const Option* y) {
|
||||
int test1 = strcmp(x->category, y->category);
|
||||
return test1 < 0 || test1 == 0 && strcmp(x->type_name, y->type_name) < 0;
|
||||
}
|
||||
};
|
||||
|
||||
Option(const char* name_,
|
||||
const char* desc_,
|
||||
const char* cate_,
|
||||
const char* type_) :
|
||||
name (name_)
|
||||
, description(desc_)
|
||||
, category (cate_)
|
||||
, type_name (type_)
|
||||
{
|
||||
getOptionList().push(this);
|
||||
}
|
||||
|
||||
public:
|
||||
virtual ~Option() {}
|
||||
|
||||
virtual bool parse (const char* str) = 0;
|
||||
virtual void help (bool verbose = false) = 0;
|
||||
|
||||
friend void parseOptions (int& argc, char** argv, bool strict);
|
||||
friend void printUsageAndExit (int argc, char** argv, bool verbose);
|
||||
friend void setUsageHelp (const char* str);
|
||||
friend void setHelpPrefixStr (const char* str);
|
||||
};
|
||||
|
||||
|
||||
//==================================================================================================
|
||||
// Range classes with specialization for floating types:
|
||||
|
||||
|
||||
struct IntRange {
|
||||
int begin;
|
||||
int end;
|
||||
IntRange(int b, int e) : begin(b), end(e) {}
|
||||
};
|
||||
|
||||
struct Int64Range {
|
||||
int64_t begin;
|
||||
int64_t end;
|
||||
Int64Range(int64_t b, int64_t e) : begin(b), end(e) {}
|
||||
};
|
||||
|
||||
struct DoubleRange {
|
||||
double begin;
|
||||
double end;
|
||||
bool begin_inclusive;
|
||||
bool end_inclusive;
|
||||
DoubleRange(double b, bool binc, double e, bool einc) : begin(b), end(e), begin_inclusive(binc), end_inclusive(einc) {}
|
||||
};
|
||||
|
||||
|
||||
//==================================================================================================
|
||||
// Double options:
|
||||
|
||||
|
||||
class DoubleOption : public Option
|
||||
{
|
||||
protected:
|
||||
DoubleRange range;
|
||||
double value;
|
||||
|
||||
public:
|
||||
DoubleOption(const char* c, const char* n, const char* d, double def = double(), DoubleRange r = DoubleRange(-HUGE_VAL, false, HUGE_VAL, false))
|
||||
: Option(n, d, c, "<double>"), range(r), value(def) {
|
||||
// FIXME: set LC_NUMERIC to "C" to make sure that strtof/strtod parses decimal point correctly.
|
||||
}
|
||||
|
||||
operator double (void) const { return value; }
|
||||
operator double& (void) { return value; }
|
||||
DoubleOption& operator=(double x) { value = x; return *this; }
|
||||
|
||||
virtual bool parse(const char* str){
|
||||
const char* span = str;
|
||||
|
||||
if (!match(span, "-") || !match(span, name) || !match(span, "="))
|
||||
return false;
|
||||
|
||||
char* end;
|
||||
double tmp = strtod(span, &end);
|
||||
|
||||
if (end == NULL)
|
||||
return false;
|
||||
else if (tmp >= range.end && (!range.end_inclusive || tmp != range.end)){
|
||||
fprintf(stderr, "ERROR! value <%s> is too large for option \"%s\".\n", span, name);
|
||||
exit(1);
|
||||
}else if (tmp <= range.begin && (!range.begin_inclusive || tmp != range.begin)){
|
||||
fprintf(stderr, "ERROR! value <%s> is too small for option \"%s\".\n", span, name);
|
||||
exit(1); }
|
||||
|
||||
value = tmp;
|
||||
// fprintf(stderr, "READ VALUE: %g\n", value);
|
||||
|
||||
return true;
|
||||
}
|
||||
|
||||
virtual void help (bool verbose = false){
|
||||
fprintf(stderr, " -%-12s = %-8s %c%4.2g .. %4.2g%c (default: %g)\n",
|
||||
name, type_name,
|
||||
range.begin_inclusive ? '[' : '(',
|
||||
range.begin,
|
||||
range.end,
|
||||
range.end_inclusive ? ']' : ')',
|
||||
value);
|
||||
if (verbose){
|
||||
fprintf(stderr, "\n %s\n", description);
|
||||
fprintf(stderr, "\n");
|
||||
}
|
||||
}
|
||||
};
|
||||
|
||||
|
||||
//==================================================================================================
|
||||
// Int options:
|
||||
|
||||
|
||||
class IntOption : public Option
|
||||
{
|
||||
protected:
|
||||
IntRange range;
|
||||
int32_t value;
|
||||
|
||||
public:
|
||||
IntOption(const char* c, const char* n, const char* d, int32_t def = int32_t(), IntRange r = IntRange(INT32_MIN, INT32_MAX))
|
||||
: Option(n, d, c, "<int32>"), range(r), value(def) {}
|
||||
|
||||
operator int32_t (void) const { return value; }
|
||||
operator int32_t& (void) { return value; }
|
||||
IntOption& operator= (int32_t x) { value = x; return *this; }
|
||||
|
||||
virtual bool parse(const char* str){
|
||||
const char* span = str;
|
||||
|
||||
if (!match(span, "-") || !match(span, name) || !match(span, "="))
|
||||
return false;
|
||||
|
||||
char* end;
|
||||
int32_t tmp = strtol(span, &end, 10);
|
||||
|
||||
if (end == NULL)
|
||||
return false;
|
||||
else if (tmp > range.end){
|
||||
fprintf(stderr, "ERROR! value <%s> is too large for option \"%s\".\n", span, name);
|
||||
exit(1);
|
||||
}else if (tmp < range.begin){
|
||||
fprintf(stderr, "ERROR! value <%s> is too small for option \"%s\".\n", span, name);
|
||||
exit(1); }
|
||||
|
||||
value = tmp;
|
||||
|
||||
return true;
|
||||
}
|
||||
|
||||
virtual void help (bool verbose = false){
|
||||
fprintf(stderr, " -%-12s = %-8s [", name, type_name);
|
||||
if (range.begin == INT32_MIN)
|
||||
fprintf(stderr, "imin");
|
||||
else
|
||||
fprintf(stderr, "%4d", range.begin);
|
||||
|
||||
fprintf(stderr, " .. ");
|
||||
if (range.end == INT32_MAX)
|
||||
fprintf(stderr, "imax");
|
||||
else
|
||||
fprintf(stderr, "%4d", range.end);
|
||||
|
||||
fprintf(stderr, "] (default: %d)\n", value);
|
||||
if (verbose){
|
||||
fprintf(stderr, "\n %s\n", description);
|
||||
fprintf(stderr, "\n");
|
||||
}
|
||||
}
|
||||
};
|
||||
|
||||
|
||||
// Leave this out for visual C++ until Microsoft implements C99 and gets support for strtoll.
|
||||
#ifndef _MSC_VER
|
||||
|
||||
class Int64Option : public Option
|
||||
{
|
||||
protected:
|
||||
Int64Range range;
|
||||
int64_t value;
|
||||
|
||||
public:
|
||||
Int64Option(const char* c, const char* n, const char* d, int64_t def = int64_t(), Int64Range r = Int64Range(INT64_MIN, INT64_MAX))
|
||||
: Option(n, d, c, "<int64>"), range(r), value(def) {}
|
||||
|
||||
operator int64_t (void) const { return value; }
|
||||
operator int64_t& (void) { return value; }
|
||||
Int64Option& operator= (int64_t x) { value = x; return *this; }
|
||||
|
||||
virtual bool parse(const char* str){
|
||||
const char* span = str;
|
||||
|
||||
if (!match(span, "-") || !match(span, name) || !match(span, "="))
|
||||
return false;
|
||||
|
||||
char* end;
|
||||
int64_t tmp = strtoll(span, &end, 10);
|
||||
|
||||
if (end == NULL)
|
||||
return false;
|
||||
else if (tmp > range.end){
|
||||
fprintf(stderr, "ERROR! value <%s> is too large for option \"%s\".\n", span, name);
|
||||
exit(1);
|
||||
}else if (tmp < range.begin){
|
||||
fprintf(stderr, "ERROR! value <%s> is too small for option \"%s\".\n", span, name);
|
||||
exit(1); }
|
||||
|
||||
value = tmp;
|
||||
|
||||
return true;
|
||||
}
|
||||
|
||||
virtual void help (bool verbose = false){
|
||||
fprintf(stderr, " -%-12s = %-8s [", name, type_name);
|
||||
if (range.begin == INT64_MIN)
|
||||
fprintf(stderr, "imin");
|
||||
else
|
||||
fprintf(stderr, "%4d", range.begin);
|
||||
|
||||
fprintf(stderr, " .. ");
|
||||
if (range.end == INT64_MAX)
|
||||
fprintf(stderr, "imax");
|
||||
else
|
||||
fprintf(stderr, "%4d", range.end);
|
||||
|
||||
fprintf(stderr, "] (default: %d)\n", value);
|
||||
if (verbose){
|
||||
fprintf(stderr, "\n %s\n", description);
|
||||
fprintf(stderr, "\n");
|
||||
}
|
||||
}
|
||||
};
|
||||
#endif
|
||||
|
||||
//==================================================================================================
|
||||
// String option:
|
||||
|
||||
|
||||
class StringOption : public Option
|
||||
{
|
||||
const char* value;
|
||||
public:
|
||||
StringOption(const char* c, const char* n, const char* d, const char* def = NULL)
|
||||
: Option(n, d, c, "<string>"), value(def) {}
|
||||
|
||||
operator const char* (void) const { return value; }
|
||||
operator const char*& (void) { return value; }
|
||||
StringOption& operator= (const char* x) { value = x; return *this; }
|
||||
|
||||
virtual bool parse(const char* str){
|
||||
const char* span = str;
|
||||
|
||||
if (!match(span, "-") || !match(span, name) || !match(span, "="))
|
||||
return false;
|
||||
|
||||
value = span;
|
||||
return true;
|
||||
}
|
||||
|
||||
virtual void help (bool verbose = false){
|
||||
fprintf(stderr, " -%-10s = %8s\n", name, type_name);
|
||||
if (verbose){
|
||||
fprintf(stderr, "\n %s\n", description);
|
||||
fprintf(stderr, "\n");
|
||||
}
|
||||
}
|
||||
};
|
||||
|
||||
|
||||
//==================================================================================================
|
||||
// Bool option:
|
||||
|
||||
|
||||
class BoolOption : public Option
|
||||
{
|
||||
bool value;
|
||||
|
||||
public:
|
||||
BoolOption(const char* c, const char* n, const char* d, bool v)
|
||||
: Option(n, d, c, "<bool>"), value(v) {}
|
||||
|
||||
operator bool (void) const { return value; }
|
||||
operator bool& (void) { return value; }
|
||||
BoolOption& operator=(bool b) { value = b; return *this; }
|
||||
|
||||
virtual bool parse(const char* str){
|
||||
const char* span = str;
|
||||
|
||||
if (match(span, "-")){
|
||||
bool b = !match(span, "no-");
|
||||
|
||||
if (strcmp(span, name) == 0){
|
||||
value = b;
|
||||
return true; }
|
||||
}
|
||||
|
||||
return false;
|
||||
}
|
||||
|
||||
virtual void help (bool verbose = false){
|
||||
|
||||
fprintf(stderr, " -%s, -no-%s", name, name);
|
||||
|
||||
for (uint32_t i = 0; i < 32 - strlen(name)*2; i++)
|
||||
fprintf(stderr, " ");
|
||||
|
||||
fprintf(stderr, " ");
|
||||
fprintf(stderr, "(default: %s)\n", value ? "on" : "off");
|
||||
if (verbose){
|
||||
fprintf(stderr, "\n %s\n", description);
|
||||
fprintf(stderr, "\n");
|
||||
}
|
||||
}
|
||||
};
|
||||
|
||||
//=================================================================================================
|
||||
}
|
||||
|
||||
#endif
|
||||
|
|
@ -0,0 +1,151 @@
|
|||
/************************************************************************************[ParseUtils.h]
|
||||
Copyright (c) 2003-2006, Niklas Een, Niklas Sorensson
|
||||
Copyright (c) 2007-2010, Niklas Sorensson
|
||||
|
||||
Permission is hereby granted, free of charge, to any person obtaining a copy of this software and
|
||||
associated documentation files (the "Software"), to deal in the Software without restriction,
|
||||
including without limitation the rights to use, copy, modify, merge, publish, distribute,
|
||||
sublicense, and/or sell copies of the Software, and to permit persons to whom the Software is
|
||||
furnished to do so, subject to the following conditions:
|
||||
|
||||
The above copyright notice and this permission notice shall be included in all copies or
|
||||
substantial portions of the Software.
|
||||
|
||||
THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR IMPLIED, INCLUDING BUT
|
||||
NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND
|
||||
NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM,
|
||||
DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT
|
||||
OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
|
||||
**************************************************************************************************/
|
||||
|
||||
#ifndef Glucose_ParseUtils_h
|
||||
#define Glucose_ParseUtils_h
|
||||
|
||||
#include <stdlib.h>
|
||||
#include <stdio.h>
|
||||
#include <math.h>
|
||||
|
||||
#include "misc/zlib/zlib.h"
|
||||
|
||||
namespace Glucose {
|
||||
|
||||
//-------------------------------------------------------------------------------------------------
|
||||
// A simple buffered character stream class:
|
||||
|
||||
static const int buffer_size = 1048576;
|
||||
|
||||
|
||||
class StreamBuffer {
|
||||
gzFile in;
|
||||
unsigned char buf[buffer_size];
|
||||
int pos;
|
||||
int size;
|
||||
|
||||
void assureLookahead() {
|
||||
if (pos >= size) {
|
||||
pos = 0;
|
||||
size = gzread(in, buf, sizeof(buf)); } }
|
||||
|
||||
public:
|
||||
explicit StreamBuffer(gzFile i) : in(i), pos(0), size(0) { assureLookahead(); }
|
||||
|
||||
int operator * () const { return (pos >= size) ? EOF : buf[pos]; }
|
||||
void operator ++ () { pos++; assureLookahead(); }
|
||||
int position () const { return pos; }
|
||||
};
|
||||
|
||||
|
||||
//-------------------------------------------------------------------------------------------------
|
||||
// End-of-file detection functions for StreamBuffer and char*:
|
||||
|
||||
|
||||
static inline bool isEof(StreamBuffer& in) { return *in == EOF; }
|
||||
static inline bool isEof(const char* in) { return *in == '\0'; }
|
||||
|
||||
//-------------------------------------------------------------------------------------------------
|
||||
// Generic parse functions parametrized over the input-stream type.
|
||||
|
||||
|
||||
template<class B>
|
||||
static void skipWhitespace(B& in) {
|
||||
while ((*in >= 9 && *in <= 13) || *in == 32)
|
||||
++in; }
|
||||
|
||||
|
||||
template<class B>
|
||||
static void skipLine(B& in) {
|
||||
for (;;){
|
||||
if (isEof(in)) return;
|
||||
if (*in == '\n') { ++in; return; }
|
||||
++in; } }
|
||||
|
||||
template<class B>
|
||||
static double parseDouble(B& in) { // only in the form X.XXXXXe-XX
|
||||
bool neg= false;
|
||||
double accu = 0.0;
|
||||
double currentExponent = 1;
|
||||
int exponent;
|
||||
|
||||
skipWhitespace(in);
|
||||
if(*in == EOF) return 0;
|
||||
if (*in == '-') neg = true, ++in;
|
||||
else if (*in == '+') ++in;
|
||||
if (*in < '1' || *in > '9') printf("PARSE ERROR! Unexpected char: %c\n", *in), exit(3);
|
||||
accu = (double)(*in - '0');
|
||||
++in;
|
||||
if (*in != '.') printf("PARSE ERROR! Unexpected char: %c\n", *in),exit(3);
|
||||
++in; // skip dot
|
||||
currentExponent = 0.1;
|
||||
while (*in >= '0' && *in <= '9')
|
||||
accu = accu + currentExponent * ((double)(*in - '0')),
|
||||
currentExponent /= 10,
|
||||
++in;
|
||||
if (*in != 'e') printf("PARSE ERROR! Unexpected char: %c\n", *in),exit(3);
|
||||
++in; // skip dot
|
||||
exponent = parseInt(in); // read exponent
|
||||
accu *= pow(10,exponent);
|
||||
return neg ? -accu:accu;
|
||||
}
|
||||
|
||||
|
||||
template<class B>
|
||||
static int parseInt(B& in) {
|
||||
int val = 0;
|
||||
bool neg = false;
|
||||
skipWhitespace(in);
|
||||
if (*in == '-') neg = true, ++in;
|
||||
else if (*in == '+') ++in;
|
||||
if (*in < '0' || *in > '9') fprintf(stderr, "PARSE ERROR! Unexpected char: %c\n", *in), exit(3);
|
||||
while (*in >= '0' && *in <= '9')
|
||||
val = val*10 + (*in - '0'),
|
||||
++in;
|
||||
return neg ? -val : val; }
|
||||
|
||||
|
||||
// String matching: in case of a match the input iterator will be advanced the corresponding
|
||||
// number of characters.
|
||||
template<class B>
|
||||
static bool match(B& in, const char* str) {
|
||||
int i;
|
||||
for (i = 0; str[i] != '\0'; i++)
|
||||
if (in[i] != str[i])
|
||||
return false;
|
||||
|
||||
in += i;
|
||||
|
||||
return true;
|
||||
}
|
||||
|
||||
// String matching: consumes characters eagerly, but does not require random access iterator.
|
||||
template<class B>
|
||||
static bool eagerMatch(B& in, const char* str) {
|
||||
for (; *str != '\0'; ++str, ++in)
|
||||
if (*str != *in)
|
||||
return false;
|
||||
return true; }
|
||||
|
||||
|
||||
//=================================================================================================
|
||||
}
|
||||
|
||||
#endif
|
||||
|
|
@ -0,0 +1,69 @@
|
|||
/*****************************************************************************************[Queue.h]
|
||||
Copyright (c) 2003-2006, Niklas Een, Niklas Sorensson
|
||||
Copyright (c) 2007-2010, Niklas Sorensson
|
||||
|
||||
Permission is hereby granted, free of charge, to any person obtaining a copy of this software and
|
||||
associated documentation files (the "Software"), to deal in the Software without restriction,
|
||||
including without limitation the rights to use, copy, modify, merge, publish, distribute,
|
||||
sublicense, and/or sell copies of the Software, and to permit persons to whom the Software is
|
||||
furnished to do so, subject to the following conditions:
|
||||
|
||||
The above copyright notice and this permission notice shall be included in all copies or
|
||||
substantial portions of the Software.
|
||||
|
||||
THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR IMPLIED, INCLUDING BUT
|
||||
NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND
|
||||
NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM,
|
||||
DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT
|
||||
OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
|
||||
**************************************************************************************************/
|
||||
|
||||
#ifndef Glucose_Queue_h
|
||||
#define Glucose_Queue_h
|
||||
|
||||
#include "sat/glucose/Vec.h"
|
||||
|
||||
namespace Glucose {
|
||||
|
||||
//=================================================================================================
|
||||
|
||||
template<class T>
|
||||
class Queue {
|
||||
vec<T> buf;
|
||||
int first;
|
||||
int end;
|
||||
|
||||
public:
|
||||
typedef T Key;
|
||||
|
||||
Queue() : buf(1), first(0), end(0) {}
|
||||
|
||||
void clear (bool dealloc = false) { buf.clear(dealloc); buf.growTo(1); first = end = 0; }
|
||||
int size () const { return (end >= first) ? end - first : end - first + buf.size(); }
|
||||
|
||||
const T& operator [] (int index) const { assert(index >= 0); assert(index < size()); return buf[(first + index) % buf.size()]; }
|
||||
T& operator [] (int index) { assert(index >= 0); assert(index < size()); return buf[(first + index) % buf.size()]; }
|
||||
|
||||
T peek () const { assert(first != end); return buf[first]; }
|
||||
void pop () { assert(first != end); first++; if (first == buf.size()) first = 0; }
|
||||
void insert(T elem) { // INVARIANT: buf[end] is always unused
|
||||
buf[end++] = elem;
|
||||
if (end == buf.size()) end = 0;
|
||||
if (first == end){ // Resize:
|
||||
vec<T> tmp((buf.size()*3 + 1) >> 1);
|
||||
//**/printf("queue alloc: %d elems (%.1f MB)\n", tmp.size(), tmp.size() * sizeof(T) / 1000000.0);
|
||||
int j, i = 0;
|
||||
for (j = first; j < buf.size(); j++) tmp[i++] = buf[j];
|
||||
for (j = 0 ; j < end ; j++) tmp[i++] = buf[j];
|
||||
first = 0;
|
||||
end = buf.size();
|
||||
tmp.moveTo(buf);
|
||||
}
|
||||
}
|
||||
};
|
||||
|
||||
|
||||
//=================================================================================================
|
||||
}
|
||||
|
||||
#endif
|
||||
|
|
@ -0,0 +1,748 @@
|
|||
/***********************************************************************************[SimpSolver.cc]
|
||||
Copyright (c) 2006, Niklas Een, Niklas Sorensson
|
||||
Copyright (c) 2007-2010, Niklas Sorensson
|
||||
|
||||
Permission is hereby granted, free of charge, to any person obtaining a copy of this software and
|
||||
associated documentation files (the "Software"), to deal in the Software without restriction,
|
||||
including without limitation the rights to use, copy, modify, merge, publish, distribute,
|
||||
sublicense, and/or sell copies of the Software, and to permit persons to whom the Software is
|
||||
furnished to do so, subject to the following conditions:
|
||||
|
||||
The above copyright notice and this permission notice shall be included in all copies or
|
||||
substantial portions of the Software.
|
||||
|
||||
THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR IMPLIED, INCLUDING BUT
|
||||
NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND
|
||||
NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM,
|
||||
DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT
|
||||
OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
|
||||
**************************************************************************************************/
|
||||
|
||||
#include "sat/glucose/Sort.h"
|
||||
#include "sat/glucose/SimpSolver.h"
|
||||
#include "sat/glucose/System.h"
|
||||
|
||||
using namespace Glucose;
|
||||
|
||||
//=================================================================================================
|
||||
// Options:
|
||||
|
||||
|
||||
static const char* _cat = "SIMP";
|
||||
|
||||
static BoolOption opt_use_asymm (_cat, "asymm", "Shrink clauses by asymmetric branching.", false);
|
||||
static BoolOption opt_use_rcheck (_cat, "rcheck", "Check if a clause is already implied. (costly)", false);
|
||||
static BoolOption opt_use_elim (_cat, "elim", "Perform variable elimination.", true);
|
||||
static IntOption opt_grow (_cat, "grow", "Allow a variable elimination step to grow by a number of clauses.", 0);
|
||||
static IntOption opt_clause_lim (_cat, "cl-lim", "Variables are not eliminated if it produces a resolvent with a length above this limit. -1 means no limit", 20, IntRange(-1, INT32_MAX));
|
||||
static IntOption opt_subsumption_lim (_cat, "sub-lim", "Do not check if subsumption against a clause larger than this. -1 means no limit.", 1000, IntRange(-1, INT32_MAX));
|
||||
static DoubleOption opt_simp_garbage_frac(_cat, "simp-gc-frac", "The fraction of wasted memory allowed before a garbage collection is triggered during simplification.", 0.5, DoubleRange(0, false, HUGE_VAL, false));
|
||||
|
||||
|
||||
//=================================================================================================
|
||||
// Constructor/Destructor:
|
||||
|
||||
|
||||
SimpSolver::SimpSolver() :
|
||||
grow (opt_grow)
|
||||
, clause_lim (opt_clause_lim)
|
||||
, subsumption_lim (opt_subsumption_lim)
|
||||
, simp_garbage_frac (opt_simp_garbage_frac)
|
||||
, use_asymm (opt_use_asymm)
|
||||
, use_rcheck (opt_use_rcheck)
|
||||
, use_elim (opt_use_elim)
|
||||
, merges (0)
|
||||
, asymm_lits (0)
|
||||
, eliminated_vars (0)
|
||||
, elimorder (1)
|
||||
, use_simplification (true)
|
||||
, occurs (ClauseDeleted(ca))
|
||||
, elim_heap (ElimLt(n_occ))
|
||||
, bwdsub_assigns (0)
|
||||
, n_touched (0)
|
||||
{
|
||||
vec<Lit> dummy(1,lit_Undef);
|
||||
ca.extra_clause_field = true; // NOTE: must happen before allocating the dummy clause below.
|
||||
bwdsub_tmpunit = ca.alloc(dummy);
|
||||
remove_satisfied = false;
|
||||
}
|
||||
|
||||
|
||||
SimpSolver::~SimpSolver()
|
||||
{
|
||||
}
|
||||
|
||||
|
||||
Var SimpSolver::newVar(bool sign, bool dvar) {
|
||||
Var v = Solver::newVar(sign, dvar);
|
||||
|
||||
frozen .push((char)false);
|
||||
eliminated.push((char)false);
|
||||
|
||||
if (use_simplification){
|
||||
n_occ .push(0);
|
||||
n_occ .push(0);
|
||||
occurs .init(v);
|
||||
touched .push(0);
|
||||
elim_heap .insert(v);
|
||||
}
|
||||
return v; }
|
||||
|
||||
|
||||
|
||||
lbool SimpSolver::solve_(bool do_simp, bool turn_off_simp)
|
||||
{
|
||||
vec<Var> extra_frozen;
|
||||
lbool result = l_True;
|
||||
|
||||
do_simp &= use_simplification;
|
||||
|
||||
if (do_simp){
|
||||
// Assumptions must be temporarily frozen to run variable elimination:
|
||||
for (int i = 0; i < assumptions.size(); i++){
|
||||
Var v = var(assumptions[i]);
|
||||
|
||||
// If an assumption has been eliminated, remember it.
|
||||
assert(!isEliminated(v));
|
||||
|
||||
if (!frozen[v]){
|
||||
// Freeze and store.
|
||||
setFrozen(v, true);
|
||||
extra_frozen.push(v);
|
||||
} }
|
||||
|
||||
result = lbool(eliminate(turn_off_simp));
|
||||
}
|
||||
|
||||
if (result == l_True)
|
||||
result = Solver::solve_();
|
||||
else if (verbosity >= 1)
|
||||
printf("===============================================================================\n");
|
||||
|
||||
if (result == l_True)
|
||||
extendModel();
|
||||
|
||||
if (do_simp)
|
||||
// Unfreeze the assumptions that were frozen:
|
||||
for (int i = 0; i < extra_frozen.size(); i++)
|
||||
setFrozen(extra_frozen[i], false);
|
||||
|
||||
return result;
|
||||
}
|
||||
|
||||
|
||||
|
||||
bool SimpSolver::addClause_(vec<Lit>& ps)
|
||||
{
|
||||
#ifndef NDEBUG
|
||||
for (int i = 0; i < ps.size(); i++)
|
||||
assert(!isEliminated(var(ps[i])));
|
||||
#endif
|
||||
int nclauses = clauses.size();
|
||||
|
||||
if (use_rcheck && implied(ps))
|
||||
return true;
|
||||
|
||||
if (!Solver::addClause_(ps))
|
||||
return false;
|
||||
|
||||
if(!parsing && certifiedUNSAT) {
|
||||
for (int i = 0; i < ps.size(); i++)
|
||||
fprintf(certifiedOutput, "%i " , (var(ps[i]) + 1) * (-2 * sign(ps[i]) + 1) );
|
||||
fprintf(certifiedOutput, "0\n");
|
||||
}
|
||||
|
||||
if (use_simplification && clauses.size() == nclauses + 1){
|
||||
CRef cr = clauses.last();
|
||||
const Clause& c = ca[cr];
|
||||
|
||||
// NOTE: the clause is added to the queue immediately and then
|
||||
// again during 'gatherTouchedClauses()'. If nothing happens
|
||||
// in between, it will only be checked once. Otherwise, it may
|
||||
// be checked twice unnecessarily. This is an unfortunate
|
||||
// consequence of how backward subsumption is used to mimic
|
||||
// forward subsumption.
|
||||
subsumption_queue.insert(cr);
|
||||
for (int i = 0; i < c.size(); i++){
|
||||
occurs[var(c[i])].push(cr);
|
||||
n_occ[toInt(c[i])]++;
|
||||
touched[var(c[i])] = 1;
|
||||
n_touched++;
|
||||
if (elim_heap.inHeap(var(c[i])))
|
||||
elim_heap.increase(var(c[i]));
|
||||
}
|
||||
}
|
||||
|
||||
return true;
|
||||
}
|
||||
|
||||
|
||||
void SimpSolver::removeClause(CRef cr)
|
||||
{
|
||||
const Clause& c = ca[cr];
|
||||
|
||||
if (use_simplification)
|
||||
for (int i = 0; i < c.size(); i++){
|
||||
n_occ[toInt(c[i])]--;
|
||||
updateElimHeap(var(c[i]));
|
||||
occurs.smudge(var(c[i]));
|
||||
}
|
||||
|
||||
Solver::removeClause(cr);
|
||||
}
|
||||
|
||||
|
||||
bool SimpSolver::strengthenClause(CRef cr, Lit l)
|
||||
{
|
||||
Clause& c = ca[cr];
|
||||
assert(decisionLevel() == 0);
|
||||
assert(use_simplification);
|
||||
|
||||
// FIX: this is too inefficient but would be nice to have (properly implemented)
|
||||
// if (!find(subsumption_queue, &c))
|
||||
subsumption_queue.insert(cr);
|
||||
|
||||
if (certifiedUNSAT) {
|
||||
for (int i = 0; i < c.size(); i++)
|
||||
if (c[i] != l) fprintf(certifiedOutput, "%i " , (var(c[i]) + 1) * (-2 * sign(c[i]) + 1) );
|
||||
fprintf(certifiedOutput, "0\n");
|
||||
}
|
||||
|
||||
if (c.size() == 2){
|
||||
removeClause(cr);
|
||||
c.strengthen(l);
|
||||
}else{
|
||||
if (certifiedUNSAT) {
|
||||
fprintf(certifiedOutput, "d ");
|
||||
for (int i = 0; i < c.size(); i++)
|
||||
fprintf(certifiedOutput, "%i " , (var(c[i]) + 1) * (-2 * sign(c[i]) + 1) );
|
||||
fprintf(certifiedOutput, "0\n");
|
||||
}
|
||||
|
||||
detachClause(cr, true);
|
||||
c.strengthen(l);
|
||||
attachClause(cr);
|
||||
remove(occurs[var(l)], cr);
|
||||
n_occ[toInt(l)]--;
|
||||
updateElimHeap(var(l));
|
||||
}
|
||||
|
||||
return c.size() == 1 ? enqueue(c[0]) && propagate() == CRef_Undef : true;
|
||||
}
|
||||
|
||||
|
||||
// Returns FALSE if clause is always satisfied ('out_clause' should not be used).
|
||||
bool SimpSolver::merge(const Clause& _ps, const Clause& _qs, Var v, vec<Lit>& out_clause)
|
||||
{
|
||||
merges++;
|
||||
out_clause.clear();
|
||||
|
||||
bool ps_smallest = _ps.size() < _qs.size();
|
||||
const Clause& ps = ps_smallest ? _qs : _ps;
|
||||
const Clause& qs = ps_smallest ? _ps : _qs;
|
||||
|
||||
int i;
|
||||
for (i = 0; i < qs.size(); i++){
|
||||
if (var(qs[i]) != v){
|
||||
for (int j = 0; j < ps.size(); j++)
|
||||
if (var(ps[j]) == var(qs[i]))
|
||||
if (ps[j] == ~qs[i])
|
||||
return false;
|
||||
else
|
||||
goto next;
|
||||
out_clause.push(qs[i]);
|
||||
}
|
||||
next:;
|
||||
}
|
||||
|
||||
for (i = 0; i < ps.size(); i++)
|
||||
if (var(ps[i]) != v)
|
||||
out_clause.push(ps[i]);
|
||||
|
||||
return true;
|
||||
}
|
||||
|
||||
|
||||
// Returns FALSE if clause is always satisfied.
|
||||
bool SimpSolver::merge(const Clause& _ps, const Clause& _qs, Var v, int& size)
|
||||
{
|
||||
merges++;
|
||||
|
||||
bool ps_smallest = _ps.size() < _qs.size();
|
||||
const Clause& ps = ps_smallest ? _qs : _ps;
|
||||
const Clause& qs = ps_smallest ? _ps : _qs;
|
||||
const Lit* __ps = (const Lit*)ps;
|
||||
const Lit* __qs = (const Lit*)qs;
|
||||
|
||||
size = ps.size()-1;
|
||||
|
||||
for (int i = 0; i < qs.size(); i++){
|
||||
if (var(__qs[i]) != v){
|
||||
for (int j = 0; j < ps.size(); j++)
|
||||
if (var(__ps[j]) == var(__qs[i]))
|
||||
if (__ps[j] == ~__qs[i])
|
||||
return false;
|
||||
else
|
||||
goto next;
|
||||
size++;
|
||||
}
|
||||
next:;
|
||||
}
|
||||
|
||||
return true;
|
||||
}
|
||||
|
||||
|
||||
void SimpSolver::gatherTouchedClauses()
|
||||
{
|
||||
if (n_touched == 0) return;
|
||||
|
||||
int i,j;
|
||||
for (i = j = 0; i < subsumption_queue.size(); i++)
|
||||
if (ca[subsumption_queue[i]].mark() == 0)
|
||||
ca[subsumption_queue[i]].mark(2);
|
||||
|
||||
for (i = 0; i < touched.size(); i++)
|
||||
if (touched[i]){
|
||||
const vec<CRef>& cs = occurs.lookup(i);
|
||||
for (j = 0; j < cs.size(); j++)
|
||||
if (ca[cs[j]].mark() == 0){
|
||||
subsumption_queue.insert(cs[j]);
|
||||
ca[cs[j]].mark(2);
|
||||
}
|
||||
touched[i] = 0;
|
||||
}
|
||||
|
||||
for (i = 0; i < subsumption_queue.size(); i++)
|
||||
if (ca[subsumption_queue[i]].mark() == 2)
|
||||
ca[subsumption_queue[i]].mark(0);
|
||||
|
||||
n_touched = 0;
|
||||
}
|
||||
|
||||
|
||||
bool SimpSolver::implied(const vec<Lit>& c)
|
||||
{
|
||||
assert(decisionLevel() == 0);
|
||||
|
||||
trail_lim.push(trail.size());
|
||||
for (int i = 0; i < c.size(); i++)
|
||||
if (value(c[i]) == l_True){
|
||||
cancelUntil(0);
|
||||
return false;
|
||||
}else if (value(c[i]) != l_False){
|
||||
assert(value(c[i]) == l_Undef);
|
||||
uncheckedEnqueue(~c[i]);
|
||||
}
|
||||
|
||||
bool result = propagate() != CRef_Undef;
|
||||
cancelUntil(0);
|
||||
return result;
|
||||
}
|
||||
|
||||
|
||||
// Backward subsumption + backward subsumption resolution
|
||||
bool SimpSolver::backwardSubsumptionCheck(bool verbose)
|
||||
{
|
||||
int cnt = 0;
|
||||
int subsumed = 0;
|
||||
int deleted_literals = 0;
|
||||
assert(decisionLevel() == 0);
|
||||
|
||||
while (subsumption_queue.size() > 0 || bwdsub_assigns < trail.size()){
|
||||
|
||||
// Empty subsumption queue and return immediately on user-interrupt:
|
||||
if (asynch_interrupt){
|
||||
subsumption_queue.clear();
|
||||
bwdsub_assigns = trail.size();
|
||||
break; }
|
||||
|
||||
// Check top-level assignments by creating a dummy clause and placing it in the queue:
|
||||
if (subsumption_queue.size() == 0 && bwdsub_assigns < trail.size()){
|
||||
Lit l = trail[bwdsub_assigns++];
|
||||
ca[bwdsub_tmpunit][0] = l;
|
||||
ca[bwdsub_tmpunit].calcAbstraction();
|
||||
subsumption_queue.insert(bwdsub_tmpunit); }
|
||||
|
||||
CRef cr = subsumption_queue.peek(); subsumption_queue.pop();
|
||||
Clause& c = ca[cr];
|
||||
|
||||
if (c.mark()) continue;
|
||||
|
||||
if (verbose && verbosity >= 2 && cnt++ % 1000 == 0)
|
||||
printf("subsumption left: %10d (%10d subsumed, %10d deleted literals)\r", subsumption_queue.size(), subsumed, deleted_literals);
|
||||
|
||||
assert(c.size() > 1 || value(c[0]) == l_True); // Unit-clauses should have been propagated before this point.
|
||||
|
||||
// Find best variable to scan:
|
||||
Var best = var(c[0]);
|
||||
for (int i = 1; i < c.size(); i++)
|
||||
if (occurs[var(c[i])].size() < occurs[best].size())
|
||||
best = var(c[i]);
|
||||
|
||||
// Search all candidates:
|
||||
vec<CRef>& _cs = occurs.lookup(best);
|
||||
CRef* cs = (CRef*)_cs;
|
||||
|
||||
for (int j = 0; j < _cs.size(); j++)
|
||||
if (c.mark())
|
||||
break;
|
||||
else if (!ca[cs[j]].mark() && cs[j] != cr && (subsumption_lim == -1 || ca[cs[j]].size() < subsumption_lim)){
|
||||
Lit l = c.subsumes(ca[cs[j]]);
|
||||
|
||||
if (l == lit_Undef)
|
||||
subsumed++, removeClause(cs[j]);
|
||||
else if (l != lit_Error){
|
||||
deleted_literals++;
|
||||
|
||||
if (!strengthenClause(cs[j], ~l))
|
||||
return false;
|
||||
|
||||
// Did current candidate get deleted from cs? Then check candidate at index j again:
|
||||
if (var(l) == best)
|
||||
j--;
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
return true;
|
||||
}
|
||||
|
||||
|
||||
bool SimpSolver::asymm(Var v, CRef cr)
|
||||
{
|
||||
Clause& c = ca[cr];
|
||||
assert(decisionLevel() == 0);
|
||||
|
||||
if (c.mark() || satisfied(c)) return true;
|
||||
|
||||
trail_lim.push(trail.size());
|
||||
Lit l = lit_Undef;
|
||||
for (int i = 0; i < c.size(); i++)
|
||||
if (var(c[i]) != v && value(c[i]) != l_False)
|
||||
uncheckedEnqueue(~c[i]);
|
||||
else
|
||||
l = c[i];
|
||||
|
||||
if (propagate() != CRef_Undef){
|
||||
cancelUntil(0);
|
||||
asymm_lits++;
|
||||
if (!strengthenClause(cr, l))
|
||||
return false;
|
||||
}else
|
||||
cancelUntil(0);
|
||||
|
||||
return true;
|
||||
}
|
||||
|
||||
|
||||
bool SimpSolver::asymmVar(Var v)
|
||||
{
|
||||
assert(use_simplification);
|
||||
|
||||
const vec<CRef>& cls = occurs.lookup(v);
|
||||
|
||||
if (value(v) != l_Undef || cls.size() == 0)
|
||||
return true;
|
||||
|
||||
for (int i = 0; i < cls.size(); i++)
|
||||
if (!asymm(v, cls[i]))
|
||||
return false;
|
||||
|
||||
return backwardSubsumptionCheck();
|
||||
}
|
||||
|
||||
|
||||
static void mkElimClause(vec<uint32_t>& elimclauses, Lit x)
|
||||
{
|
||||
elimclauses.push(toInt(x));
|
||||
elimclauses.push(1);
|
||||
}
|
||||
|
||||
|
||||
static void mkElimClause(vec<uint32_t>& elimclauses, Var v, Clause& c)
|
||||
{
|
||||
int first = elimclauses.size();
|
||||
int v_pos = -1;
|
||||
|
||||
// Copy clause to elimclauses-vector. Remember position where the
|
||||
// variable 'v' occurs:
|
||||
for (int i = 0; i < c.size(); i++){
|
||||
elimclauses.push(toInt(c[i]));
|
||||
if (var(c[i]) == v)
|
||||
v_pos = i + first;
|
||||
}
|
||||
assert(v_pos != -1);
|
||||
|
||||
// Swap the first literal with the 'v' literal, so that the literal
|
||||
// containing 'v' will occur first in the clause:
|
||||
uint32_t tmp = elimclauses[v_pos];
|
||||
elimclauses[v_pos] = elimclauses[first];
|
||||
elimclauses[first] = tmp;
|
||||
|
||||
// Store the length of the clause last:
|
||||
elimclauses.push(c.size());
|
||||
}
|
||||
|
||||
|
||||
|
||||
bool SimpSolver::eliminateVar(Var v)
|
||||
{
|
||||
int i, j;
|
||||
assert(!frozen[v]);
|
||||
assert(!isEliminated(v));
|
||||
assert(value(v) == l_Undef);
|
||||
|
||||
// Split the occurrences into positive and negative:
|
||||
//
|
||||
const vec<CRef>& cls = occurs.lookup(v);
|
||||
vec<CRef> pos, neg;
|
||||
for (i = 0; i < cls.size(); i++)
|
||||
(find(ca[cls[i]], mkLit(v)) ? pos : neg).push(cls[i]);
|
||||
|
||||
// Check wether the increase in number of clauses stays within the allowed ('grow'). Moreover, no
|
||||
// clause must exceed the limit on the maximal clause size (if it is set):
|
||||
//
|
||||
int cnt = 0;
|
||||
int clause_size = 0;
|
||||
|
||||
for (i = 0; i < pos.size(); i++)
|
||||
for (j = 0; j < neg.size(); j++)
|
||||
if (merge(ca[pos[i]], ca[neg[j]], v, clause_size) &&
|
||||
(++cnt > cls.size() + grow || (clause_lim != -1 && clause_size > clause_lim)))
|
||||
return true;
|
||||
|
||||
// Delete and store old clauses:
|
||||
eliminated[v] = true;
|
||||
setDecisionVar(v, false);
|
||||
eliminated_vars++;
|
||||
|
||||
if (pos.size() > neg.size()){
|
||||
for (i = 0; i < neg.size(); i++)
|
||||
mkElimClause(elimclauses, v, ca[neg[i]]);
|
||||
mkElimClause(elimclauses, mkLit(v));
|
||||
}else{
|
||||
for (i = 0; i < pos.size(); i++)
|
||||
mkElimClause(elimclauses, v, ca[pos[i]]);
|
||||
mkElimClause(elimclauses, ~mkLit(v));
|
||||
}
|
||||
|
||||
|
||||
// Produce clauses in cross product:
|
||||
vec<Lit>& resolvent = add_tmp;
|
||||
for (i = 0; i < pos.size(); i++)
|
||||
for (j = 0; j < neg.size(); j++)
|
||||
if (merge(ca[pos[i]], ca[neg[j]], v, resolvent) && !addClause_(resolvent))
|
||||
return false;
|
||||
|
||||
for (i = 0; i < cls.size(); i++)
|
||||
removeClause(cls[i]);
|
||||
|
||||
// Free occurs list for this variable:
|
||||
occurs[v].clear(true);
|
||||
|
||||
// Free watchers lists for this variable, if possible:
|
||||
if (watches[ mkLit(v)].size() == 0) watches[ mkLit(v)].clear(true);
|
||||
if (watches[~mkLit(v)].size() == 0) watches[~mkLit(v)].clear(true);
|
||||
|
||||
return backwardSubsumptionCheck();
|
||||
}
|
||||
|
||||
|
||||
bool SimpSolver::substitute(Var v, Lit x)
|
||||
{
|
||||
assert(!frozen[v]);
|
||||
assert(!isEliminated(v));
|
||||
assert(value(v) == l_Undef);
|
||||
|
||||
if (!ok) return false;
|
||||
|
||||
eliminated[v] = true;
|
||||
setDecisionVar(v, false);
|
||||
const vec<CRef>& cls = occurs.lookup(v);
|
||||
|
||||
vec<Lit>& subst_clause = add_tmp;
|
||||
for (int i = 0; i < cls.size(); i++){
|
||||
Clause& c = ca[cls[i]];
|
||||
|
||||
subst_clause.clear();
|
||||
for (int j = 0; j < c.size(); j++){
|
||||
Lit p = c[j];
|
||||
subst_clause.push(var(p) == v ? x ^ sign(p) : p);
|
||||
}
|
||||
|
||||
|
||||
if (!addClause_(subst_clause))
|
||||
return ok = false;
|
||||
|
||||
removeClause(cls[i]);
|
||||
|
||||
}
|
||||
|
||||
return true;
|
||||
}
|
||||
|
||||
|
||||
void SimpSolver::extendModel()
|
||||
{
|
||||
int i, j;
|
||||
Lit x;
|
||||
|
||||
for (i = elimclauses.size()-1; i > 0; i -= j){
|
||||
for (j = elimclauses[i--]; j > 1; j--, i--)
|
||||
if (modelValue(toLit(elimclauses[i])) != l_False)
|
||||
goto next;
|
||||
|
||||
x = toLit(elimclauses[i]);
|
||||
model[var(x)] = lbool(!sign(x));
|
||||
next:;
|
||||
}
|
||||
}
|
||||
|
||||
|
||||
bool SimpSolver::eliminate(bool turn_off_elim)
|
||||
{
|
||||
if (!simplify())
|
||||
return false;
|
||||
else if (!use_simplification)
|
||||
return true;
|
||||
|
||||
// Main simplification loop:
|
||||
//
|
||||
|
||||
int toPerform = clauses.size()<=4800000;
|
||||
|
||||
if(!toPerform) {
|
||||
printf("c Too many clauses... No preprocessing\n");
|
||||
}
|
||||
|
||||
while (toPerform && (n_touched > 0 || bwdsub_assigns < trail.size() || elim_heap.size() > 0)){
|
||||
|
||||
gatherTouchedClauses();
|
||||
// printf(" ## (time = %6.2f s) BWD-SUB: queue = %d, trail = %d\n", cpuTime(), subsumption_queue.size(), trail.size() - bwdsub_assigns);
|
||||
if ((subsumption_queue.size() > 0 || bwdsub_assigns < trail.size()) &&
|
||||
!backwardSubsumptionCheck(true)){
|
||||
ok = false; goto cleanup; }
|
||||
|
||||
// Empty elim_heap and return immediately on user-interrupt:
|
||||
if (asynch_interrupt){
|
||||
assert(bwdsub_assigns == trail.size());
|
||||
assert(subsumption_queue.size() == 0);
|
||||
assert(n_touched == 0);
|
||||
elim_heap.clear();
|
||||
goto cleanup; }
|
||||
|
||||
// printf(" ## (time = %6.2f s) ELIM: vars = %d\n", cpuTime(), elim_heap.size());
|
||||
for (int cnt = 0; !elim_heap.empty(); cnt++){
|
||||
Var elim = elim_heap.removeMin();
|
||||
|
||||
if (asynch_interrupt) break;
|
||||
|
||||
if (isEliminated(elim) || value(elim) != l_Undef) continue;
|
||||
|
||||
if (verbosity >= 2 && cnt % 100 == 0)
|
||||
printf("elimination left: %10d\r", elim_heap.size());
|
||||
|
||||
if (use_asymm){
|
||||
// Temporarily freeze variable. Otherwise, it would immediately end up on the queue again:
|
||||
bool was_frozen = frozen[elim] != 0;
|
||||
frozen[elim] = true;
|
||||
if (!asymmVar(elim)){
|
||||
ok = false; goto cleanup; }
|
||||
frozen[elim] = was_frozen; }
|
||||
|
||||
// At this point, the variable may have been set by assymetric branching, so check it
|
||||
// again. Also, don't eliminate frozen variables:
|
||||
if (use_elim && value(elim) == l_Undef && !frozen[elim] && !eliminateVar(elim)){
|
||||
ok = false; goto cleanup; }
|
||||
|
||||
checkGarbage(simp_garbage_frac);
|
||||
}
|
||||
|
||||
assert(subsumption_queue.size() == 0);
|
||||
}
|
||||
cleanup:
|
||||
|
||||
// If no more simplification is needed, free all simplification-related data structures:
|
||||
if (turn_off_elim){
|
||||
touched .clear(true);
|
||||
occurs .clear(true);
|
||||
n_occ .clear(true);
|
||||
elim_heap.clear(true);
|
||||
subsumption_queue.clear(true);
|
||||
|
||||
use_simplification = false;
|
||||
remove_satisfied = true;
|
||||
ca.extra_clause_field = false;
|
||||
|
||||
// Force full cleanup (this is safe and desirable since it only happens once):
|
||||
rebuildOrderHeap();
|
||||
garbageCollect();
|
||||
}else{
|
||||
// Cheaper cleanup:
|
||||
cleanUpClauses(); // TODO: can we make 'cleanUpClauses()' not be linear in the problem size somehow?
|
||||
checkGarbage();
|
||||
}
|
||||
|
||||
if (verbosity >= 1 && elimclauses.size() > 0)
|
||||
printf("c | Eliminated clauses: %10.2f Mb |\n",
|
||||
double(elimclauses.size() * sizeof(uint32_t)) / (1024*1024));
|
||||
|
||||
return ok;
|
||||
}
|
||||
|
||||
|
||||
void SimpSolver::cleanUpClauses()
|
||||
{
|
||||
occurs.cleanAll();
|
||||
int i,j;
|
||||
for (i = j = 0; i < clauses.size(); i++)
|
||||
if (ca[clauses[i]].mark() == 0)
|
||||
clauses[j++] = clauses[i];
|
||||
clauses.shrink(i - j);
|
||||
}
|
||||
|
||||
|
||||
//=================================================================================================
|
||||
// Garbage Collection methods:
|
||||
|
||||
|
||||
void SimpSolver::relocAll(ClauseAllocator& to)
|
||||
{
|
||||
int i;
|
||||
if (!use_simplification) return;
|
||||
|
||||
// All occurs lists:
|
||||
//
|
||||
for (i = 0; i < nVars(); i++){
|
||||
vec<CRef>& cs = occurs[i];
|
||||
for (int j = 0; j < cs.size(); j++)
|
||||
ca.reloc(cs[j], to);
|
||||
}
|
||||
|
||||
// Subsumption queue:
|
||||
//
|
||||
for (i = 0; i < subsumption_queue.size(); i++)
|
||||
ca.reloc(subsumption_queue[i], to);
|
||||
|
||||
// Temporary clause:
|
||||
//
|
||||
ca.reloc(bwdsub_tmpunit, to);
|
||||
}
|
||||
|
||||
|
||||
void SimpSolver::garbageCollect()
|
||||
{
|
||||
// Initialize the next region to a size corresponding to the estimated utilization degree. This
|
||||
// is not precise but should avoid some unnecessary reallocations for the new region:
|
||||
ClauseAllocator to(ca.size() - ca.wasted());
|
||||
|
||||
cleanUpClauses();
|
||||
to.extra_clause_field = ca.extra_clause_field; // NOTE: this is important to keep (or lose) the extra fields.
|
||||
relocAll(to);
|
||||
Solver::relocAll(to);
|
||||
if (verbosity >= 2)
|
||||
printf("| Garbage collection: %12d bytes => %12d bytes |\n",
|
||||
ca.size()*ClauseAllocator::Unit_Size, to.size()*ClauseAllocator::Unit_Size);
|
||||
to.moveTo(ca);
|
||||
}
|
||||
|
|
@ -0,0 +1,198 @@
|
|||
/************************************************************************************[SimpSolver.h]
|
||||
Copyright (c) 2006, Niklas Een, Niklas Sorensson
|
||||
Copyright (c) 2007-2010, Niklas Sorensson
|
||||
|
||||
Permission is hereby granted, free of charge, to any person obtaining a copy of this software and
|
||||
associated documentation files (the "Software"), to deal in the Software without restriction,
|
||||
including without limitation the rights to use, copy, modify, merge, publish, distribute,
|
||||
sublicense, and/or sell copies of the Software, and to permit persons to whom the Software is
|
||||
furnished to do so, subject to the following conditions:
|
||||
|
||||
The above copyright notice and this permission notice shall be included in all copies or
|
||||
substantial portions of the Software.
|
||||
|
||||
THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR IMPLIED, INCLUDING BUT
|
||||
NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND
|
||||
NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM,
|
||||
DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT
|
||||
OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
|
||||
**************************************************************************************************/
|
||||
|
||||
#ifndef Glucose_SimpSolver_h
|
||||
#define Glucose_SimpSolver_h
|
||||
|
||||
#include "sat/glucose/Queue.h"
|
||||
#include "sat/glucose/Solver.h"
|
||||
|
||||
|
||||
namespace Glucose {
|
||||
|
||||
//=================================================================================================
|
||||
|
||||
|
||||
class SimpSolver : public Solver {
|
||||
public:
|
||||
// Constructor/Destructor:
|
||||
//
|
||||
SimpSolver();
|
||||
~SimpSolver();
|
||||
|
||||
// Problem specification:
|
||||
//
|
||||
Var newVar (bool polarity = true, bool dvar = true);
|
||||
bool addClause (const vec<Lit>& ps);
|
||||
bool addEmptyClause(); // Add the empty clause to the solver.
|
||||
bool addClause (Lit p); // Add a unit clause to the solver.
|
||||
bool addClause (Lit p, Lit q); // Add a binary clause to the solver.
|
||||
bool addClause (Lit p, Lit q, Lit r); // Add a ternary clause to the solver.
|
||||
bool addClause_( vec<Lit>& ps);
|
||||
bool substitute(Var v, Lit x); // Replace all occurences of v with x (may cause a contradiction).
|
||||
|
||||
// Variable mode:
|
||||
//
|
||||
void setFrozen (Var v, bool b); // If a variable is frozen it will not be eliminated.
|
||||
bool isEliminated(Var v) const;
|
||||
|
||||
// Solving:
|
||||
//
|
||||
bool solve (const vec<Lit>& assumps, bool do_simp = true, bool turn_off_simp = false);
|
||||
lbool solveLimited(const vec<Lit>& assumps, bool do_simp = true, bool turn_off_simp = false);
|
||||
bool solve ( bool do_simp = true, bool turn_off_simp = false);
|
||||
bool solve (Lit p , bool do_simp = true, bool turn_off_simp = false);
|
||||
bool solve (Lit p, Lit q, bool do_simp = true, bool turn_off_simp = false);
|
||||
bool solve (Lit p, Lit q, Lit r, bool do_simp = true, bool turn_off_simp = false);
|
||||
bool eliminate (bool turn_off_elim = false); // Perform variable elimination based simplification.
|
||||
|
||||
// Memory managment:
|
||||
//
|
||||
virtual void garbageCollect();
|
||||
|
||||
|
||||
// Generate a (possibly simplified) DIMACS file:
|
||||
//
|
||||
#if 0
|
||||
void toDimacs (const char* file, const vec<Lit>& assumps);
|
||||
void toDimacs (const char* file);
|
||||
void toDimacs (const char* file, Lit p);
|
||||
void toDimacs (const char* file, Lit p, Lit q);
|
||||
void toDimacs (const char* file, Lit p, Lit q, Lit r);
|
||||
#endif
|
||||
|
||||
// Mode of operation:
|
||||
//
|
||||
int parsing;
|
||||
int grow; // Allow a variable elimination step to grow by a number of clauses (default to zero).
|
||||
int clause_lim; // Variables are not eliminated if it produces a resolvent with a length above this limit.
|
||||
// -1 means no limit.
|
||||
int subsumption_lim; // Do not check if subsumption against a clause larger than this. -1 means no limit.
|
||||
double simp_garbage_frac; // A different limit for when to issue a GC during simplification (Also see 'garbage_frac').
|
||||
|
||||
bool use_asymm; // Shrink clauses by asymmetric branching.
|
||||
bool use_rcheck; // Check if a clause is already implied. Prett costly, and subsumes subsumptions :)
|
||||
bool use_elim; // Perform variable elimination.
|
||||
|
||||
// Statistics:
|
||||
//
|
||||
int merges;
|
||||
int asymm_lits;
|
||||
int eliminated_vars;
|
||||
|
||||
protected:
|
||||
|
||||
// Helper structures:
|
||||
//
|
||||
struct ElimLt {
|
||||
const vec<int>& n_occ;
|
||||
explicit ElimLt(const vec<int>& no) : n_occ(no) {}
|
||||
|
||||
// TODO: are 64-bit operations here noticably bad on 32-bit platforms? Could use a saturating
|
||||
// 32-bit implementation instead then, but this will have to do for now.
|
||||
uint64_t cost (Var x) const { return (uint64_t)n_occ[toInt(mkLit(x))] * (uint64_t)n_occ[toInt(~mkLit(x))]; }
|
||||
bool operator()(Var x, Var y) const { return cost(x) < cost(y); }
|
||||
|
||||
// TODO: investigate this order alternative more.
|
||||
// bool operator()(Var x, Var y) const {
|
||||
// int c_x = cost(x);
|
||||
// int c_y = cost(y);
|
||||
// return c_x < c_y || c_x == c_y && x < y; }
|
||||
};
|
||||
|
||||
struct ClauseDeleted {
|
||||
const ClauseAllocator& ca;
|
||||
explicit ClauseDeleted(const ClauseAllocator& _ca) : ca(_ca) {}
|
||||
bool operator()(const CRef& cr) const { return ca[cr].mark() == 1; } };
|
||||
|
||||
// Solver state:
|
||||
//
|
||||
int elimorder;
|
||||
bool use_simplification;
|
||||
vec<uint32_t> elimclauses;
|
||||
vec<char> touched;
|
||||
OccLists<Var, vec<CRef>, ClauseDeleted>
|
||||
occurs;
|
||||
vec<int> n_occ;
|
||||
Heap<ElimLt> elim_heap;
|
||||
Queue<CRef> subsumption_queue;
|
||||
vec<char> frozen;
|
||||
vec<char> eliminated;
|
||||
int bwdsub_assigns;
|
||||
int n_touched;
|
||||
|
||||
// Temporaries:
|
||||
//
|
||||
CRef bwdsub_tmpunit;
|
||||
|
||||
// Main internal methods:
|
||||
//
|
||||
lbool solve_ (bool do_simp = true, bool turn_off_simp = false);
|
||||
bool asymm (Var v, CRef cr);
|
||||
bool asymmVar (Var v);
|
||||
void updateElimHeap (Var v);
|
||||
void gatherTouchedClauses ();
|
||||
bool merge (const Clause& _ps, const Clause& _qs, Var v, vec<Lit>& out_clause);
|
||||
bool merge (const Clause& _ps, const Clause& _qs, Var v, int& size);
|
||||
bool backwardSubsumptionCheck (bool verbose = false);
|
||||
bool eliminateVar (Var v);
|
||||
void extendModel ();
|
||||
|
||||
void removeClause (CRef cr);
|
||||
bool strengthenClause (CRef cr, Lit l);
|
||||
void cleanUpClauses ();
|
||||
bool implied (const vec<Lit>& c);
|
||||
void relocAll (ClauseAllocator& to);
|
||||
};
|
||||
|
||||
|
||||
//=================================================================================================
|
||||
// Implementation of inline methods:
|
||||
|
||||
|
||||
inline bool SimpSolver::isEliminated (Var v) const { return eliminated[v] != 0; }
|
||||
inline void SimpSolver::updateElimHeap(Var v) {
|
||||
assert(use_simplification);
|
||||
// if (!frozen[v] && !isEliminated(v) && value(v) == l_Undef)
|
||||
if (elim_heap.inHeap(v) || (!frozen[v] && !isEliminated(v) && value(v) == l_Undef))
|
||||
elim_heap.update(v); }
|
||||
|
||||
|
||||
inline bool SimpSolver::addClause (const vec<Lit>& ps) { ps.copyTo(add_tmp); return addClause_(add_tmp); }
|
||||
inline bool SimpSolver::addEmptyClause() { add_tmp.clear(); return addClause_(add_tmp); }
|
||||
inline bool SimpSolver::addClause (Lit p) { add_tmp.clear(); add_tmp.push(p); return addClause_(add_tmp); }
|
||||
inline bool SimpSolver::addClause (Lit p, Lit q) { add_tmp.clear(); add_tmp.push(p); add_tmp.push(q); return addClause_(add_tmp); }
|
||||
inline bool SimpSolver::addClause (Lit p, Lit q, Lit r) { add_tmp.clear(); add_tmp.push(p); add_tmp.push(q); add_tmp.push(r); return addClause_(add_tmp); }
|
||||
inline void SimpSolver::setFrozen (Var v, bool b) { frozen[v] = (char)b; if (use_simplification && !b) { updateElimHeap(v); } }
|
||||
|
||||
inline bool SimpSolver::solve ( bool do_simp, bool turn_off_simp) { budgetOff(); assumptions.clear(); return solve_(do_simp, turn_off_simp) == l_True; }
|
||||
inline bool SimpSolver::solve (Lit p , bool do_simp, bool turn_off_simp) { budgetOff(); assumptions.clear(); assumptions.push(p); return solve_(do_simp, turn_off_simp) == l_True; }
|
||||
inline bool SimpSolver::solve (Lit p, Lit q, bool do_simp, bool turn_off_simp) { budgetOff(); assumptions.clear(); assumptions.push(p); assumptions.push(q); return solve_(do_simp, turn_off_simp) == l_True; }
|
||||
inline bool SimpSolver::solve (Lit p, Lit q, Lit r, bool do_simp, bool turn_off_simp) { budgetOff(); assumptions.clear(); assumptions.push(p); assumptions.push(q); assumptions.push(r); return solve_(do_simp, turn_off_simp) == l_True; }
|
||||
inline bool SimpSolver::solve (const vec<Lit>& assumps, bool do_simp, bool turn_off_simp){
|
||||
budgetOff(); assumps.copyTo(assumptions); return solve_(do_simp, turn_off_simp) == l_True; }
|
||||
|
||||
inline lbool SimpSolver::solveLimited (const vec<Lit>& assumps, bool do_simp, bool turn_off_simp){
|
||||
assumps.copyTo(assumptions); return solve_(do_simp, turn_off_simp); }
|
||||
|
||||
//=================================================================================================
|
||||
}
|
||||
|
||||
#endif
|
||||
|
|
@ -0,0 +1,485 @@
|
|||
/****************************************************************************************[Solver.h]
|
||||
Glucose -- Copyright (c) 2009, Gilles Audemard, Laurent Simon
|
||||
CRIL - Univ. Artois, France
|
||||
LRI - Univ. Paris Sud, France
|
||||
|
||||
Glucose sources are based on MiniSat (see below MiniSat copyrights). Permissions and copyrights of
|
||||
Glucose are exactly the same as Minisat on which it is based on. (see below).
|
||||
|
||||
---------------
|
||||
Copyright (c) 2003-2006, Niklas Een, Niklas Sorensson
|
||||
Copyright (c) 2007-2010, Niklas Sorensson
|
||||
|
||||
Permission is hereby granted, free of charge, to any person obtaining a copy of this software and
|
||||
associated documentation files (the "Software"), to deal in the Software without restriction,
|
||||
including without limitation the rights to use, copy, modify, merge, publish, distribute,
|
||||
sublicense, and/or sell copies of the Software, and to permit persons to whom the Software is
|
||||
furnished to do so, subject to the following conditions:
|
||||
|
||||
The above copyright notice and this permission notice shall be included in all copies or
|
||||
substantial portions of the Software.
|
||||
|
||||
THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR IMPLIED, INCLUDING BUT
|
||||
NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND
|
||||
NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM,
|
||||
DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT
|
||||
OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
|
||||
**************************************************************************************************/
|
||||
|
||||
#ifndef Glucose_Solver_h
|
||||
#define Glucose_Solver_h
|
||||
|
||||
#include "sat/glucose/Vec.h"
|
||||
#include "sat/glucose/Heap.h"
|
||||
#include "sat/glucose/Alg.h"
|
||||
#include "sat/glucose/Options.h"
|
||||
#include "sat/glucose/SolverTypes.h"
|
||||
#include "sat/glucose/BoundedQueue.h"
|
||||
#include "sat/glucose/Constants.h"
|
||||
|
||||
|
||||
namespace Glucose {
|
||||
|
||||
//=================================================================================================
|
||||
// Solver -- the main class:
|
||||
|
||||
class Solver {
|
||||
public:
|
||||
|
||||
int SolverType; // ABC identifies Glucose's type as 0
|
||||
|
||||
// Constructor/Destructor:
|
||||
//
|
||||
Solver();
|
||||
virtual ~Solver();
|
||||
|
||||
// ABC callbacks
|
||||
void * pCnfMan; // external CNF manager
|
||||
int(*pCnfFunc)(void * p, int, int*); // external callback. messages: 0: unsat; 1: sat; -1: still working
|
||||
int nCallConfl; // callback will be called every this number of conflicts
|
||||
bool terminate_search_early; // used to stop the solver early if it as instructed by an external caller
|
||||
int * pstop; // another callback
|
||||
|
||||
// Problem specification:
|
||||
//
|
||||
Var newVar (bool polarity = true, bool dvar = true); // Add a new variable with parameters specifying variable mode.
|
||||
|
||||
bool addClause (const vec<Lit>& ps); // Add a clause to the solver.
|
||||
bool addEmptyClause(); // Add the empty clause, making the solver contradictory.
|
||||
bool addClause (Lit p); // Add a unit clause to the solver.
|
||||
bool addClause (Lit p, Lit q); // Add a binary clause to the solver.
|
||||
bool addClause (Lit p, Lit q, Lit r); // Add a ternary clause to the solver.
|
||||
bool addClause_( vec<Lit>& ps); // Add a clause to the solver without making superflous internal copy. Will
|
||||
// change the passed vector 'ps'.
|
||||
|
||||
// Solving:
|
||||
//
|
||||
bool simplify (); // Removes already satisfied clauses.
|
||||
bool solve (const vec<Lit>& assumps); // Search for a model that respects a given set of assumptions.
|
||||
lbool solveLimited (const vec<Lit>& assumps); // Search for a model that respects a given set of assumptions (With resource constraints).
|
||||
bool solve (); // Search without assumptions.
|
||||
bool solve (Lit p); // Search for a model that respects a single assumption.
|
||||
bool solve (Lit p, Lit q); // Search for a model that respects two assumptions.
|
||||
bool solve (Lit p, Lit q, Lit r); // Search for a model that respects three assumptions.
|
||||
bool okay () const; // FALSE means solver is in a conflicting state
|
||||
|
||||
void toDimacs (FILE* f, const vec<Lit>& assumps); // Write CNF to file in DIMACS-format.
|
||||
void toDimacs (const char *file, const vec<Lit>& assumps);
|
||||
void toDimacs (FILE* f, Clause& c, vec<Var>& map, Var& max);
|
||||
void printLit(Lit l);
|
||||
void printClause(CRef c);
|
||||
void printInitialClause(CRef c);
|
||||
// Convenience versions of 'toDimacs()':
|
||||
void toDimacs (const char* file);
|
||||
void toDimacs (const char* file, Lit p);
|
||||
void toDimacs (const char* file, Lit p, Lit q);
|
||||
void toDimacs (const char* file, Lit p, Lit q, Lit r);
|
||||
|
||||
// Variable mode:
|
||||
//
|
||||
void setPolarity (Var v, bool b); // Declare which polarity the decision heuristic should use for a variable. Requires mode 'polarity_user'.
|
||||
void setDecisionVar (Var v, bool b); // Declare if a variable should be eligible for selection in the decision heuristic.
|
||||
|
||||
// Read state:
|
||||
//
|
||||
lbool value (Var x) const; // The current value of a variable.
|
||||
lbool value (Lit p) const; // The current value of a literal.
|
||||
lbool modelValue (Var x) const; // The value of a variable in the last model. The last call to solve must have been satisfiable.
|
||||
lbool modelValue (Lit p) const; // The value of a literal in the last model. The last call to solve must have been satisfiable.
|
||||
int nAssigns () const; // The current number of assigned literals.
|
||||
int nClauses () const; // The current number of original clauses.
|
||||
int nLearnts () const; // The current number of learnt clauses.
|
||||
int nVars () const; // The current number of variables.
|
||||
int nFreeVars () const;
|
||||
|
||||
// Incremental mode
|
||||
void setIncrementalMode();
|
||||
void initNbInitialVars(int nb);
|
||||
void printIncrementalStats();
|
||||
|
||||
// Resource contraints:
|
||||
//
|
||||
void setConfBudget(int64_t x);
|
||||
void setPropBudget(int64_t x);
|
||||
void budgetOff();
|
||||
void interrupt(); // Trigger a (potentially asynchronous) interruption of the solver.
|
||||
void clearInterrupt(); // Clear interrupt indicator flag.
|
||||
|
||||
// Memory managment:
|
||||
//
|
||||
/*virtual*/ void garbageCollect(); // virtuality causes segfault for some reason
|
||||
void checkGarbage(double gf);
|
||||
void checkGarbage();
|
||||
|
||||
|
||||
|
||||
|
||||
// Extra results: (read-only member variable)
|
||||
//
|
||||
vec<lbool> model; // If problem is satisfiable, this vector contains the model (if any).
|
||||
vec<Lit> conflict; // If problem is unsatisfiable (possibly under assumptions),
|
||||
// this vector represent the final conflict clause expressed in the assumptions.
|
||||
|
||||
// Mode of operation:
|
||||
//
|
||||
int verbosity;
|
||||
int verbEveryConflicts;
|
||||
int showModel;
|
||||
// Constants For restarts
|
||||
double K;
|
||||
double R;
|
||||
double sizeLBDQueue;
|
||||
double sizeTrailQueue;
|
||||
|
||||
// Constants for reduce DB
|
||||
int firstReduceDB;
|
||||
int incReduceDB;
|
||||
int specialIncReduceDB;
|
||||
unsigned int lbLBDFrozenClause;
|
||||
|
||||
// Constant for reducing clause
|
||||
int lbSizeMinimizingClause;
|
||||
unsigned int lbLBDMinimizingClause;
|
||||
|
||||
double var_decay;
|
||||
double clause_decay;
|
||||
double random_var_freq;
|
||||
double random_seed;
|
||||
int ccmin_mode; // Controls conflict clause minimization (0=none, 1=basic, 2=deep).
|
||||
int phase_saving; // Controls the level of phase saving (0=none, 1=limited, 2=full).
|
||||
bool rnd_pol; // Use random polarities for branching heuristics.
|
||||
bool rnd_init_act; // Initialize variable activities with a small random value.
|
||||
double garbage_frac; // The fraction of wasted memory allowed before a garbage collection is triggered.
|
||||
|
||||
// Certified UNSAT ( Thanks to Marijn Heule)
|
||||
FILE* certifiedOutput;
|
||||
bool certifiedUNSAT;
|
||||
|
||||
|
||||
// Statistics: (read-only member variable)
|
||||
//
|
||||
int64_t nbRemovedClauses,nbReducedClauses,nbDL2,nbBin,nbUn,nbReduceDB,solves, starts, decisions, rnd_decisions, propagations, conflicts,conflictsRestarts,nbstopsrestarts,nbstopsrestartssame,lastblockatrestart;
|
||||
int64_t dec_vars, clauses_literals, learnts_literals, max_literals, tot_literals;
|
||||
|
||||
protected:
|
||||
long curRestart;
|
||||
// Helper structures:
|
||||
//
|
||||
struct VarData { CRef reason; int level; };
|
||||
static inline VarData mkVarData(CRef cr, int l){ VarData d = {cr, l}; return d; }
|
||||
|
||||
struct Watcher {
|
||||
CRef cref;
|
||||
Lit blocker;
|
||||
Watcher(CRef cr, Lit p) : cref(cr), blocker(p) {}
|
||||
bool operator==(const Watcher& w) const { return cref == w.cref; }
|
||||
bool operator!=(const Watcher& w) const { return cref != w.cref; }
|
||||
};
|
||||
|
||||
struct WatcherDeleted
|
||||
{
|
||||
const ClauseAllocator& ca;
|
||||
WatcherDeleted(const ClauseAllocator& _ca) : ca(_ca) {}
|
||||
bool operator()(const Watcher& w) const { return ca[w.cref].mark() == 1; }
|
||||
};
|
||||
|
||||
struct VarOrderLt {
|
||||
const vec<double>& activity;
|
||||
bool operator () (Var x, Var y) const { return activity[x] > activity[y]; }
|
||||
VarOrderLt(const vec<double>& act) : activity(act) { }
|
||||
};
|
||||
|
||||
|
||||
// Solver state:
|
||||
//
|
||||
int lastIndexRed;
|
||||
bool ok; // If FALSE, the constraints are already unsatisfiable. No part of the solver state may be used!
|
||||
double cla_inc; // Amount to bump next clause with.
|
||||
vec<double> activity; // A heuristic measurement of the activity of a variable.
|
||||
double var_inc; // Amount to bump next variable with.
|
||||
OccLists<Lit, vec<Watcher>, WatcherDeleted>
|
||||
watches; // 'watches[lit]' is a list of constraints watching 'lit' (will go there if literal becomes true).
|
||||
OccLists<Lit, vec<Watcher>, WatcherDeleted>
|
||||
watchesBin; // 'watches[lit]' is a list of constraints watching 'lit' (will go there if literal becomes true).
|
||||
vec<CRef> clauses; // List of problem clauses.
|
||||
vec<CRef> learnts; // List of learnt clauses.
|
||||
|
||||
vec<lbool> assigns; // The current assignments.
|
||||
vec<char> polarity; // The preferred polarity of each variable.
|
||||
vec<char> decision; // Declares if a variable is eligible for selection in the decision heuristic.
|
||||
vec<Lit> trail; // Assignment stack; stores all assigments made in the order they were made.
|
||||
vec<int> nbpos;
|
||||
vec<int> trail_lim; // Separator indices for different decision levels in 'trail'.
|
||||
vec<VarData> vardata; // Stores reason and level for each variable.
|
||||
int qhead; // Head of queue (as index into the trail -- no more explicit propagation queue in MiniSat).
|
||||
int simpDB_assigns; // Number of top-level assignments since last execution of 'simplify()'.
|
||||
int64_t simpDB_props; // Remaining number of propagations that must be made before next execution of 'simplify()'.
|
||||
vec<Lit> assumptions; // Current set of assumptions provided to solve by the user.
|
||||
Heap<VarOrderLt> order_heap; // A priority queue of variables ordered with respect to the variable activity.
|
||||
double progress_estimate;// Set by 'search()'.
|
||||
bool remove_satisfied; // Indicates whether possibly inefficient linear scan for satisfied clauses should be performed in 'simplify'.
|
||||
vec<unsigned int> permDiff; // permDiff[var] contains the current conflict number... Used to count the number of LBD
|
||||
|
||||
#ifdef UPDATEVARACTIVITY
|
||||
// UPDATEVARACTIVITY trick (see competition'09 companion paper)
|
||||
vec<Lit> lastDecisionLevel;
|
||||
#endif
|
||||
|
||||
ClauseAllocator ca;
|
||||
|
||||
int nbclausesbeforereduce; // To know when it is time to reduce clause database
|
||||
|
||||
bqueue<unsigned int> trailQueue,lbdQueue; // Bounded queues for restarts.
|
||||
float sumLBD; // used to compute the global average of LBD. Restarts...
|
||||
int sumAssumptions;
|
||||
|
||||
|
||||
// Temporaries (to reduce allocation overhead). Each variable is prefixed by the method in which it is
|
||||
// used, exept 'seen' wich is used in several places.
|
||||
//
|
||||
vec<char> seen;
|
||||
vec<Lit> analyze_stack;
|
||||
vec<Lit> analyze_toclear;
|
||||
vec<Lit> add_tmp;
|
||||
unsigned int MYFLAG;
|
||||
|
||||
|
||||
double max_learnts;
|
||||
double learntsize_adjust_confl;
|
||||
int learntsize_adjust_cnt;
|
||||
|
||||
// Resource contraints:
|
||||
//
|
||||
int64_t conflict_budget; // -1 means no budget.
|
||||
int64_t propagation_budget; // -1 means no budget.
|
||||
bool asynch_interrupt;
|
||||
|
||||
|
||||
// Variables added for incremental mode
|
||||
int incremental; // Use incremental SAT Solver
|
||||
int nbVarsInitialFormula; // nb VAR in formula without assumptions (incremental SAT)
|
||||
double totalTime4Sat,totalTime4Unsat;
|
||||
int nbSatCalls,nbUnsatCalls;
|
||||
vec<int> assumptionPositions,initialPositions;
|
||||
|
||||
|
||||
// Main internal methods:
|
||||
//
|
||||
void insertVarOrder (Var x); // Insert a variable in the decision order priority queue.
|
||||
Lit pickBranchLit (); // Return the next decision variable.
|
||||
void newDecisionLevel (); // Begins a new decision level.
|
||||
void uncheckedEnqueue (Lit p, CRef from = CRef_Undef); // Enqueue a literal. Assumes value of literal is undefined.
|
||||
bool enqueue (Lit p, CRef from = CRef_Undef); // Test if fact 'p' contradicts current state, enqueue otherwise.
|
||||
CRef propagate (); // Perform unit propagation. Returns possibly conflicting clause.
|
||||
void cancelUntil (int level); // Backtrack until a certain level.
|
||||
void analyze (CRef confl, vec<Lit>& out_learnt, vec<Lit> & selectors, int& out_btlevel,unsigned int &nblevels,unsigned int &szWithoutSelectors); // (bt = backtrack)
|
||||
void analyzeFinal (Lit p, vec<Lit>& out_conflict); // COULD THIS BE IMPLEMENTED BY THE ORDINARIY "analyze" BY SOME REASONABLE GENERALIZATION?
|
||||
bool litRedundant (Lit p, uint32_t abstract_levels); // (helper method for 'analyze()')
|
||||
lbool search (int nof_conflicts); // Search for a given number of conflicts.
|
||||
lbool solve_ (); // Main solve method (assumptions given in 'assumptions').
|
||||
void reduceDB (); // Reduce the set of learnt clauses.
|
||||
void removeSatisfied (vec<CRef>& cs); // Shrink 'cs' to contain only non-satisfied clauses.
|
||||
void rebuildOrderHeap ();
|
||||
|
||||
// Maintaining Variable/Clause activity:
|
||||
//
|
||||
void varDecayActivity (); // Decay all variables with the specified factor. Implemented by increasing the 'bump' value instead.
|
||||
void varBumpActivity (Var v, double inc); // Increase a variable with the current 'bump' value.
|
||||
void varBumpActivity (Var v); // Increase a variable with the current 'bump' value.
|
||||
void claDecayActivity (); // Decay all clauses with the specified factor. Implemented by increasing the 'bump' value instead.
|
||||
void claBumpActivity (Clause& c); // Increase a clause with the current 'bump' value.
|
||||
|
||||
// Operations on clauses:
|
||||
//
|
||||
void attachClause (CRef cr); // Attach a clause to watcher lists.
|
||||
void detachClause (CRef cr, bool strict = false); // Detach a clause to watcher lists.
|
||||
void removeClause (CRef cr); // Detach and free a clause.
|
||||
bool locked (const Clause& c) const; // Returns TRUE if a clause is a reason for some implication in the current state.
|
||||
bool satisfied (const Clause& c) const; // Returns TRUE if a clause is satisfied in the current state.
|
||||
|
||||
unsigned int computeLBD(const vec<Lit> & lits,int end=-1);
|
||||
unsigned int computeLBD(const Clause &c);
|
||||
void minimisationWithBinaryResolution(vec<Lit> &out_learnt);
|
||||
|
||||
void relocAll (ClauseAllocator& to);
|
||||
|
||||
// Misc:
|
||||
//
|
||||
int decisionLevel () const; // Gives the current decisionlevel.
|
||||
uint32_t abstractLevel (Var x) const; // Used to represent an abstraction of sets of decision levels.
|
||||
CRef reason (Var x) const;
|
||||
int level (Var x) const;
|
||||
double progressEstimate () const; // DELETE THIS ?? IT'S NOT VERY USEFUL ...
|
||||
bool withinBudget () const;
|
||||
inline bool isSelector(Var v) {return (incremental && v>nbVarsInitialFormula);}
|
||||
|
||||
// Static helpers:
|
||||
//
|
||||
|
||||
// Returns a random float 0 <= x < 1. Seed must never be 0.
|
||||
static inline double drand(double& seed) {
|
||||
seed *= 1389796;
|
||||
int 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); }
|
||||
};
|
||||
|
||||
|
||||
//=================================================================================================
|
||||
// Implementation of inline methods:
|
||||
|
||||
inline CRef Solver::reason(Var x) const { return vardata[x].reason; }
|
||||
inline int Solver::level (Var x) const { return vardata[x].level; }
|
||||
|
||||
inline void Solver::insertVarOrder(Var x) {
|
||||
if (!order_heap.inHeap(x) && decision[x]) order_heap.insert(x); }
|
||||
|
||||
inline void Solver::varDecayActivity() { var_inc *= (1 / var_decay); }
|
||||
inline void Solver::varBumpActivity(Var v) { varBumpActivity(v, var_inc); }
|
||||
inline void Solver::varBumpActivity(Var v, double inc) {
|
||||
if ( (activity[v] += inc) > 1e100 ) {
|
||||
// Rescale:
|
||||
for (int i = 0; i < nVars(); i++)
|
||||
activity[i] *= 1e-100;
|
||||
var_inc *= 1e-100; }
|
||||
|
||||
// Update order_heap with respect to new activity:
|
||||
if (order_heap.inHeap(v))
|
||||
order_heap.decrease(v); }
|
||||
|
||||
inline void Solver::claDecayActivity() { cla_inc *= (1 / clause_decay); }
|
||||
inline void Solver::claBumpActivity (Clause& c) {
|
||||
if ( (c.activity() += cla_inc) > 1e20 ) {
|
||||
// Rescale:
|
||||
for (int i = 0; i < learnts.size(); i++)
|
||||
ca[learnts[i]].activity() *= (float)1e-20;
|
||||
cla_inc *= 1e-20; } }
|
||||
|
||||
inline void Solver::checkGarbage(void){ checkGarbage(garbage_frac); }
|
||||
inline void Solver::checkGarbage(double gf){
|
||||
if (ca.wasted() > ca.size() * gf)
|
||||
garbageCollect();}
|
||||
|
||||
// NOTE: enqueue does not set the ok flag! (only public methods do)
|
||||
inline bool Solver::enqueue (Lit p, CRef from) { return value(p) != l_Undef ? value(p) != l_False : (uncheckedEnqueue(p, from), true); }
|
||||
inline bool Solver::addClause (const vec<Lit>& ps) { ps.copyTo(add_tmp); return addClause_(add_tmp); }
|
||||
inline bool Solver::addEmptyClause () { add_tmp.clear(); return addClause_(add_tmp); }
|
||||
inline bool Solver::addClause (Lit p) { add_tmp.clear(); add_tmp.push(p); return addClause_(add_tmp); }
|
||||
inline bool Solver::addClause (Lit p, Lit q) { add_tmp.clear(); add_tmp.push(p); add_tmp.push(q); return addClause_(add_tmp); }
|
||||
inline bool Solver::addClause (Lit p, Lit q, Lit r) { add_tmp.clear(); add_tmp.push(p); add_tmp.push(q); add_tmp.push(r); return addClause_(add_tmp); }
|
||||
inline bool Solver::locked (const Clause& c) const {
|
||||
if(c.size()>2)
|
||||
return value(c[0]) == l_True && reason(var(c[0])) != CRef_Undef && ca.lea(reason(var(c[0]))) == &c;
|
||||
return
|
||||
(value(c[0]) == l_True && reason(var(c[0])) != CRef_Undef && ca.lea(reason(var(c[0]))) == &c)
|
||||
||
|
||||
(value(c[1]) == l_True && reason(var(c[1])) != CRef_Undef && ca.lea(reason(var(c[1]))) == &c);
|
||||
}
|
||||
inline void Solver::newDecisionLevel() { trail_lim.push(trail.size()); }
|
||||
|
||||
inline int Solver::decisionLevel () const { return trail_lim.size(); }
|
||||
inline uint32_t Solver::abstractLevel (Var x) const { return 1 << (level(x) & 31); }
|
||||
inline lbool Solver::value (Var x) const { return assigns[x]; }
|
||||
inline lbool Solver::value (Lit p) const { return assigns[var(p)] ^ sign(p); }
|
||||
inline lbool Solver::modelValue (Var x) const { return model[x]; }
|
||||
inline lbool Solver::modelValue (Lit p) const { return model[var(p)] ^ sign(p); }
|
||||
inline int Solver::nAssigns () const { return trail.size(); }
|
||||
inline int Solver::nClauses () const { return clauses.size(); }
|
||||
inline int Solver::nLearnts () const { return learnts.size(); }
|
||||
inline int Solver::nVars () const { return vardata.size(); }
|
||||
inline int Solver::nFreeVars () const { return (int)dec_vars - (trail_lim.size() == 0 ? trail.size() : trail_lim[0]); }
|
||||
inline void Solver::setPolarity (Var v, bool b) { polarity[v] = b; }
|
||||
inline void Solver::setDecisionVar(Var v, bool b)
|
||||
{
|
||||
if ( b && !decision[v]) dec_vars++;
|
||||
else if (!b && decision[v]) dec_vars--;
|
||||
|
||||
decision[v] = b;
|
||||
insertVarOrder(v);
|
||||
}
|
||||
inline void Solver::setConfBudget(int64_t x){ conflict_budget = conflicts + x; }
|
||||
inline void Solver::setPropBudget(int64_t x){ propagation_budget = propagations + x; }
|
||||
inline void Solver::interrupt(){ asynch_interrupt = true; }
|
||||
inline void Solver::clearInterrupt(){ asynch_interrupt = false; }
|
||||
inline void Solver::budgetOff(){ conflict_budget = propagation_budget = -1; }
|
||||
inline bool Solver::withinBudget() const {
|
||||
return !asynch_interrupt &&
|
||||
(conflict_budget < 0 || conflicts < (uint64_t)conflict_budget) &&
|
||||
(propagation_budget < 0 || propagations < (uint64_t)propagation_budget); }
|
||||
|
||||
// FIXME: after the introduction of asynchronous interrruptions the solve-versions that return a
|
||||
// pure bool do not give a safe interface. Either interrupts must be possible to turn off here, or
|
||||
// all calls to solve must return an 'lbool'. I'm not yet sure which I prefer.
|
||||
inline bool Solver::solve () { budgetOff(); assumptions.clear(); return solve_() == l_True; }
|
||||
inline bool Solver::solve (Lit p) { budgetOff(); assumptions.clear(); assumptions.push(p); return solve_() == l_True; }
|
||||
inline bool Solver::solve (Lit p, Lit q) { budgetOff(); assumptions.clear(); assumptions.push(p); assumptions.push(q); return solve_() == l_True; }
|
||||
inline bool Solver::solve (Lit p, Lit q, Lit r) { budgetOff(); assumptions.clear(); assumptions.push(p); assumptions.push(q); assumptions.push(r); return solve_() == l_True; }
|
||||
inline bool Solver::solve (const vec<Lit>& assumps){ budgetOff(); assumps.copyTo(assumptions); return solve_() == l_True; }
|
||||
inline lbool Solver::solveLimited (const vec<Lit>& assumps){ assumps.copyTo(assumptions); return solve_(); }
|
||||
inline bool Solver::okay () const { return ok; }
|
||||
|
||||
inline void Solver::toDimacs (const char* file){ vec<Lit> as; toDimacs(file, as); }
|
||||
inline void Solver::toDimacs (const char* file, Lit p){ vec<Lit> as; as.push(p); toDimacs(file, as); }
|
||||
inline void Solver::toDimacs (const char* file, Lit p, Lit q){ vec<Lit> as; as.push(p); as.push(q); toDimacs(file, as); }
|
||||
inline void Solver::toDimacs (const char* file, Lit p, Lit q, Lit r){ vec<Lit> as; as.push(p); as.push(q); as.push(r); toDimacs(file, as); }
|
||||
|
||||
|
||||
//=================================================================================================
|
||||
// Debug etc:
|
||||
|
||||
|
||||
inline void Solver::printLit(Lit l)
|
||||
{
|
||||
printf("%s%d:%c", sign(l) ? "-" : "", var(l)+1, value(l) == l_True ? '1' : (value(l) == l_False ? '0' : 'X'));
|
||||
}
|
||||
|
||||
|
||||
inline void Solver::printClause(CRef cr)
|
||||
{
|
||||
Clause &c = ca[cr];
|
||||
for (int i = 0; i < c.size(); i++){
|
||||
printLit(c[i]);
|
||||
printf(" ");
|
||||
}
|
||||
}
|
||||
|
||||
inline void Solver::printInitialClause(CRef cr)
|
||||
{
|
||||
Clause &c = ca[cr];
|
||||
for (int i = 0; i < c.size(); i++){
|
||||
if(!isSelector(var(c[i]))) {
|
||||
printLit(c[i]);
|
||||
printf(" ");
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
|
||||
//=================================================================================================
|
||||
}
|
||||
|
||||
#endif
|
||||
|
|
@ -0,0 +1,434 @@
|
|||
/***********************************************************************************[SolverTypes.h]
|
||||
Glucose -- Copyright (c) 2009, Gilles Audemard, Laurent Simon
|
||||
CRIL - Univ. Artois, France
|
||||
LRI - Univ. Paris Sud, France
|
||||
|
||||
Glucose sources are based on MiniSat (see below MiniSat copyrights). Permissions and copyrights of
|
||||
Glucose are exactly the same as Minisat on which it is based on. (see below).
|
||||
|
||||
---------------
|
||||
Copyright (c) 2003-2006, Niklas Een, Niklas Sorensson
|
||||
Copyright (c) 2007-2010, Niklas Sorensson
|
||||
|
||||
Permission is hereby granted, free of charge, to any person obtaining a copy of this software and
|
||||
associated documentation files (the "Software"), to deal in the Software without restriction,
|
||||
including without limitation the rights to use, copy, modify, merge, publish, distribute,
|
||||
sublicense, and/or sell copies of the Software, and to permit persons to whom the Software is
|
||||
furnished to do so, subject to the following conditions:
|
||||
|
||||
The above copyright notice and this permission notice shall be included in all copies or
|
||||
substantial portions of the Software.
|
||||
|
||||
THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR IMPLIED, INCLUDING BUT
|
||||
NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND
|
||||
NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM,
|
||||
DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT
|
||||
OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
|
||||
**************************************************************************************************/
|
||||
|
||||
|
||||
#ifndef Glucose_SolverTypes_h
|
||||
#define Glucose_SolverTypes_h
|
||||
|
||||
#include <assert.h>
|
||||
|
||||
#include "sat/glucose/IntTypes.h"
|
||||
#include "sat/glucose/Alg.h"
|
||||
#include "sat/glucose/Vec.h"
|
||||
#include "sat/glucose/Map.h"
|
||||
#include "sat/glucose/Alloc.h"
|
||||
|
||||
namespace Glucose {
|
||||
|
||||
//=================================================================================================
|
||||
// Variables, literals, lifted booleans, clauses:
|
||||
|
||||
|
||||
// NOTE! Variables are just integers. No abstraction here. They should be chosen from 0..N,
|
||||
// so that they can be used as array indices.
|
||||
|
||||
typedef int Var;
|
||||
#define var_Undef (-1)
|
||||
|
||||
|
||||
struct Lit {
|
||||
int x;
|
||||
|
||||
// Use this as a constructor:
|
||||
friend Lit mkLit(Var var, bool sign = false);
|
||||
bool operator == (Lit p) const { return x == p.x; }
|
||||
bool operator != (Lit p) const { return x != p.x; }
|
||||
bool operator < (Lit p) const { return x < p.x; } // '<' makes p, ~p adjacent in the ordering.
|
||||
};
|
||||
|
||||
|
||||
inline Lit mkLit (Var var, bool sign) { Lit p; p.x = var + var + (int)sign; return p; }
|
||||
inline Lit operator ~(Lit p) { Lit q; q.x = p.x ^ 1; return q; }
|
||||
inline Lit operator ^(Lit p, bool b) { Lit q; q.x = p.x ^ (unsigned int)b; return q; }
|
||||
inline bool sign (Lit p) { return p.x & 1; }
|
||||
inline int var (Lit p) { return p.x >> 1; }
|
||||
|
||||
// Mapping Literals to and from compact integers suitable for array indexing:
|
||||
inline int toInt (Var v) { return v; }
|
||||
inline int toInt (Lit p) { return p.x; }
|
||||
inline Lit toLit (int i) { Lit p; p.x = i; return p; }
|
||||
|
||||
//const Lit lit_Undef = mkLit(var_Undef, false); // }- Useful special constants.
|
||||
//const Lit lit_Error = mkLit(var_Undef, true ); // }
|
||||
|
||||
const Lit lit_Undef = { -2 }; // }- Useful special constants.
|
||||
const Lit lit_Error = { -1 }; // }
|
||||
|
||||
|
||||
//=================================================================================================
|
||||
// Lifted booleans:
|
||||
//
|
||||
// NOTE: this implementation is optimized for the case when comparisons between values are mostly
|
||||
// between one variable and one constant. Some care had to be taken to make sure that gcc
|
||||
// does enough constant propagation to produce sensible code, and this appears to be somewhat
|
||||
// fragile unfortunately.
|
||||
|
||||
#define l_True (Glucose::lbool((uint8_t)0)) // gcc does not do constant propagation if these are real constants.
|
||||
#define l_False (Glucose::lbool((uint8_t)1))
|
||||
#define l_Undef (Glucose::lbool((uint8_t)2))
|
||||
|
||||
class lbool {
|
||||
uint8_t value;
|
||||
|
||||
public:
|
||||
explicit lbool(uint8_t v) : value(v) { }
|
||||
|
||||
lbool() : value(0) { }
|
||||
explicit lbool(bool x) : value(!x) { }
|
||||
|
||||
bool operator == (lbool b) const { return (((b.value&2) & (value&2)) | (!(b.value&2)&(value == b.value))) != 0; }
|
||||
bool operator != (lbool b) const { return !(*this == b); }
|
||||
lbool operator ^ (bool b) const { return lbool((uint8_t)(value^(uint8_t)b)); }
|
||||
|
||||
lbool operator && (lbool b) const {
|
||||
uint8_t sel = (this->value << 1) | (b.value << 3);
|
||||
uint8_t v = (0xF7F755F4 >> sel) & 3;
|
||||
return lbool(v); }
|
||||
|
||||
lbool operator || (lbool b) const {
|
||||
uint8_t sel = (this->value << 1) | (b.value << 3);
|
||||
uint8_t v = (0xFCFCF400 >> sel) & 3;
|
||||
return lbool(v); }
|
||||
|
||||
friend int toInt (lbool l);
|
||||
friend lbool toLbool(int v);
|
||||
};
|
||||
inline int toInt (lbool l) { return l.value; }
|
||||
inline lbool toLbool(int v) { return lbool((uint8_t)v); }
|
||||
|
||||
//=================================================================================================
|
||||
// Clause -- a simple class for representing a clause:
|
||||
|
||||
class Clause;
|
||||
typedef RegionAllocator<uint32_t>::Ref CRef;
|
||||
|
||||
class Clause {
|
||||
struct {
|
||||
unsigned mark : 2;
|
||||
unsigned learnt : 1;
|
||||
unsigned has_extra : 1;
|
||||
unsigned reloced : 1;
|
||||
unsigned lbd : 26;
|
||||
unsigned canbedel : 1;
|
||||
unsigned size : 32;
|
||||
unsigned szWithoutSelectors : 32;
|
||||
|
||||
} header;
|
||||
union { Lit lit; float act; uint32_t abs; CRef rel; } data[0];
|
||||
|
||||
friend class ClauseAllocator;
|
||||
|
||||
// NOTE: This constructor cannot be used directly (doesn't allocate enough memory).
|
||||
template<class V>
|
||||
Clause(const V& ps, bool use_extra, bool learnt) {
|
||||
header.mark = 0;
|
||||
header.learnt = learnt;
|
||||
header.has_extra = use_extra;
|
||||
header.reloced = 0;
|
||||
header.size = ps.size();
|
||||
header.lbd = 0;
|
||||
header.canbedel = 1;
|
||||
for (int i = 0; i < ps.size(); i++)
|
||||
data[i].lit = ps[i];
|
||||
|
||||
if (header.has_extra){
|
||||
if (header.learnt)
|
||||
data[header.size].act = 0;
|
||||
else
|
||||
calcAbstraction(); }
|
||||
}
|
||||
|
||||
public:
|
||||
void calcAbstraction() {
|
||||
assert(header.has_extra);
|
||||
uint32_t abstraction = 0;
|
||||
for (int i = 0; i < size(); i++)
|
||||
abstraction |= 1 << (var(data[i].lit) & 31);
|
||||
data[header.size].abs = abstraction; }
|
||||
|
||||
|
||||
int size () const { return header.size; }
|
||||
void shrink (int i) { assert(i <= size()); if (header.has_extra) data[header.size-i] = data[header.size]; header.size -= i; }
|
||||
void pop () { shrink(1); }
|
||||
bool learnt () const { return header.learnt; }
|
||||
bool has_extra () const { return header.has_extra; }
|
||||
uint32_t mark () const { return header.mark; }
|
||||
void mark (uint32_t m) { header.mark = m; }
|
||||
const Lit& last () const { return data[header.size-1].lit; }
|
||||
|
||||
bool reloced () const { return header.reloced; }
|
||||
CRef relocation () const { return data[0].rel; }
|
||||
void relocate (CRef c) { header.reloced = 1; data[0].rel = c; }
|
||||
|
||||
// NOTE: somewhat unsafe to change the clause in-place! Must manually call 'calcAbstraction' afterwards for
|
||||
// subsumption operations to behave correctly.
|
||||
Lit& operator [] (int i) { return data[i].lit; }
|
||||
Lit operator [] (int i) const { return data[i].lit; }
|
||||
operator const Lit* (void) const { return (Lit*)data; }
|
||||
|
||||
float& activity () { assert(header.has_extra); return data[header.size].act; }
|
||||
uint32_t abstraction () const { assert(header.has_extra); return data[header.size].abs; }
|
||||
|
||||
Lit subsumes (const Clause& other) const;
|
||||
void strengthen (Lit p);
|
||||
void setLBD(int i) {header.lbd = i;}
|
||||
// unsigned int& lbd () { return header.lbd; }
|
||||
unsigned int lbd () const { return header.lbd; }
|
||||
void setCanBeDel(bool b) {header.canbedel = b;}
|
||||
bool canBeDel() {return header.canbedel;}
|
||||
void setSizeWithoutSelectors (unsigned int n) {header.szWithoutSelectors = n; }
|
||||
unsigned int sizeWithoutSelectors () const { return header.szWithoutSelectors; }
|
||||
|
||||
};
|
||||
|
||||
|
||||
//=================================================================================================
|
||||
// ClauseAllocator -- a simple class for allocating memory for clauses:
|
||||
|
||||
|
||||
const CRef CRef_Undef = RegionAllocator<uint32_t>::Ref_Undef;
|
||||
class ClauseAllocator : public RegionAllocator<uint32_t>
|
||||
{
|
||||
static int clauseWord32Size(int size, bool has_extra){
|
||||
return (sizeof(Clause) + (sizeof(Lit) * (size + (int)has_extra))) / sizeof(uint32_t); }
|
||||
public:
|
||||
bool extra_clause_field;
|
||||
|
||||
ClauseAllocator(uint32_t start_cap) : RegionAllocator<uint32_t>(start_cap), extra_clause_field(false){}
|
||||
ClauseAllocator() : extra_clause_field(false){}
|
||||
|
||||
void moveTo(ClauseAllocator& to){
|
||||
to.extra_clause_field = extra_clause_field;
|
||||
RegionAllocator<uint32_t>::moveTo(to); }
|
||||
|
||||
template<class Lits>
|
||||
CRef alloc(const Lits& ps, bool learnt = false)
|
||||
{
|
||||
assert(sizeof(Lit) == sizeof(uint32_t));
|
||||
assert(sizeof(float) == sizeof(uint32_t));
|
||||
bool use_extra = learnt | extra_clause_field;
|
||||
|
||||
CRef cid = RegionAllocator<uint32_t>::alloc(clauseWord32Size(ps.size(), use_extra));
|
||||
new (lea(cid)) Clause(ps, use_extra, learnt);
|
||||
|
||||
return cid;
|
||||
}
|
||||
|
||||
// Deref, Load Effective Address (LEA), Inverse of LEA (AEL):
|
||||
Clause& operator[](Ref r) { return (Clause&)RegionAllocator<uint32_t>::operator[](r); }
|
||||
const Clause& operator[](Ref r) const { return (Clause&)RegionAllocator<uint32_t>::operator[](r); }
|
||||
Clause* lea (Ref r) { return (Clause*)RegionAllocator<uint32_t>::lea(r); }
|
||||
const Clause* lea (Ref r) const { return (Clause*)RegionAllocator<uint32_t>::lea(r); }
|
||||
Ref ael (const Clause* t){ return RegionAllocator<uint32_t>::ael((uint32_t*)t); }
|
||||
|
||||
void free_(CRef cid)
|
||||
{
|
||||
Clause& c = operator[](cid);
|
||||
RegionAllocator<uint32_t>::free_(clauseWord32Size(c.size(), c.has_extra()));
|
||||
}
|
||||
|
||||
void reloc(CRef& cr, ClauseAllocator& to)
|
||||
{
|
||||
Clause& c = operator[](cr);
|
||||
|
||||
if (c.reloced()) { cr = c.relocation(); return; }
|
||||
|
||||
cr = to.alloc(c, c.learnt());
|
||||
c.relocate(cr);
|
||||
|
||||
// Copy extra data-fields:
|
||||
// (This could be cleaned-up. Generalize Clause-constructor to be applicable here instead?)
|
||||
to[cr].mark(c.mark());
|
||||
if (to[cr].learnt()) {
|
||||
to[cr].activity() = c.activity();
|
||||
to[cr].setLBD(c.lbd());
|
||||
to[cr].setSizeWithoutSelectors(c.sizeWithoutSelectors());
|
||||
to[cr].setCanBeDel(c.canBeDel());
|
||||
}
|
||||
else if (to[cr].has_extra()) to[cr].calcAbstraction();
|
||||
}
|
||||
};
|
||||
|
||||
|
||||
//=================================================================================================
|
||||
// OccLists -- a class for maintaining occurence lists with lazy deletion:
|
||||
|
||||
template<class Idx, class Vec, class Deleted>
|
||||
class OccLists
|
||||
{
|
||||
vec<Vec> occs;
|
||||
vec<char> dirty;
|
||||
vec<Idx> dirties;
|
||||
Deleted deleted;
|
||||
|
||||
public:
|
||||
OccLists(const Deleted& d) : deleted(d) {}
|
||||
|
||||
void init (const Idx& idx){ occs.growTo(toInt(idx)+1); dirty.growTo(toInt(idx)+1, 0); }
|
||||
// Vec& operator[](const Idx& idx){ return occs[toInt(idx)]; }
|
||||
Vec& operator[](const Idx& idx){ return occs[toInt(idx)]; }
|
||||
Vec& lookup (const Idx& idx){ if (dirty[toInt(idx)]) clean(idx); return occs[toInt(idx)]; }
|
||||
|
||||
void cleanAll ();
|
||||
void clean (const Idx& idx);
|
||||
void smudge (const Idx& idx){
|
||||
if (dirty[toInt(idx)] == 0){
|
||||
dirty[toInt(idx)] = 1;
|
||||
dirties.push(idx);
|
||||
}
|
||||
}
|
||||
|
||||
void clear(bool free = true){
|
||||
occs .clear(free);
|
||||
dirty .clear(free);
|
||||
dirties.clear(free);
|
||||
}
|
||||
};
|
||||
|
||||
|
||||
template<class Idx, class Vec, class Deleted>
|
||||
void OccLists<Idx,Vec,Deleted>::cleanAll()
|
||||
{
|
||||
for (int i = 0; i < dirties.size(); i++)
|
||||
// Dirties may contain duplicates so check here if a variable is already cleaned:
|
||||
if (dirty[toInt(dirties[i])])
|
||||
clean(dirties[i]);
|
||||
dirties.clear();
|
||||
}
|
||||
|
||||
|
||||
template<class Idx, class Vec, class Deleted>
|
||||
void OccLists<Idx,Vec,Deleted>::clean(const Idx& idx)
|
||||
{
|
||||
Vec& vec = occs[toInt(idx)];
|
||||
int i, j;
|
||||
for (i = j = 0; i < vec.size(); i++)
|
||||
if (!deleted(vec[i]))
|
||||
vec[j++] = vec[i];
|
||||
vec.shrink(i - j);
|
||||
dirty[toInt(idx)] = 0;
|
||||
}
|
||||
|
||||
|
||||
//=================================================================================================
|
||||
// CMap -- a class for mapping clauses to values:
|
||||
|
||||
|
||||
template<class T>
|
||||
class CMap
|
||||
{
|
||||
struct CRefHash {
|
||||
uint32_t operator()(CRef cr) const { return (uint32_t)cr; } };
|
||||
|
||||
typedef Map<CRef, T, CRefHash> HashTable;
|
||||
HashTable map;
|
||||
|
||||
public:
|
||||
// Size-operations:
|
||||
void clear () { map.clear(); }
|
||||
int size () const { return map.elems(); }
|
||||
|
||||
|
||||
// Insert/Remove/Test mapping:
|
||||
void insert (CRef cr, const T& t){ map.insert(cr, t); }
|
||||
void growTo (CRef cr, const T& t){ map.insert(cr, t); } // NOTE: for compatibility
|
||||
void remove (CRef cr) { map.remove(cr); }
|
||||
bool has (CRef cr, T& t) { return map.peek(cr, t); }
|
||||
|
||||
// Vector interface (the clause 'c' must already exist):
|
||||
const T& operator [] (CRef cr) const { return map[cr]; }
|
||||
T& operator [] (CRef cr) { return map[cr]; }
|
||||
|
||||
// Iteration (not transparent at all at the moment):
|
||||
int bucket_count() const { return map.bucket_count(); }
|
||||
const vec<typename HashTable::Pair>& bucket(int i) const { return map.bucket(i); }
|
||||
|
||||
// Move contents to other map:
|
||||
void moveTo(CMap& other){ map.moveTo(other.map); }
|
||||
|
||||
// TMP debug:
|
||||
void debug(){
|
||||
printf(" --- size = %d, bucket_count = %d\n", size(), map.bucket_count()); }
|
||||
};
|
||||
|
||||
|
||||
/*_________________________________________________________________________________________________
|
||||
|
|
||||
| subsumes : (other : const Clause&) -> Lit
|
||||
|
|
||||
| Description:
|
||||
| Checks if clause subsumes 'other', and at the same time, if it can be used to simplify 'other'
|
||||
| by subsumption resolution.
|
||||
|
|
||||
| Result:
|
||||
| lit_Error - No subsumption or simplification
|
||||
| lit_Undef - Clause subsumes 'other'
|
||||
| p - The literal p can be deleted from 'other'
|
||||
|________________________________________________________________________________________________@*/
|
||||
inline Lit Clause::subsumes(const Clause& other) const
|
||||
{
|
||||
//if (other.size() < size() || (extra.abst & ~other.extra.abst) != 0)
|
||||
//if (other.size() < size() || (!learnt() && !other.learnt() && (extra.abst & ~other.extra.abst) != 0))
|
||||
assert(!header.learnt); assert(!other.header.learnt);
|
||||
assert(header.has_extra); assert(other.header.has_extra);
|
||||
if (other.header.size < header.size || (data[header.size].abs & ~other.data[other.header.size].abs) != 0)
|
||||
return lit_Error;
|
||||
|
||||
Lit ret = lit_Undef;
|
||||
const Lit* c = (const Lit*)(*this);
|
||||
const Lit* d = (const Lit*)other;
|
||||
|
||||
for (unsigned i = 0; i < header.size; i++) {
|
||||
// search for c[i] or ~c[i]
|
||||
for (unsigned j = 0; j < other.header.size; j++)
|
||||
if (c[i] == d[j])
|
||||
goto ok;
|
||||
else if (ret == lit_Undef && c[i] == ~d[j]){
|
||||
ret = c[i];
|
||||
goto ok;
|
||||
}
|
||||
|
||||
// did not find it
|
||||
return lit_Error;
|
||||
ok:;
|
||||
}
|
||||
|
||||
return ret;
|
||||
}
|
||||
|
||||
inline void Clause::strengthen(Lit p)
|
||||
{
|
||||
remove(*this, p);
|
||||
calcAbstraction();
|
||||
}
|
||||
|
||||
//=================================================================================================
|
||||
}
|
||||
|
||||
|
||||
#endif
|
||||
|
|
@ -0,0 +1,98 @@
|
|||
/******************************************************************************************[Sort.h]
|
||||
Copyright (c) 2003-2007, Niklas Een, Niklas Sorensson
|
||||
Copyright (c) 2007-2010, Niklas Sorensson
|
||||
|
||||
Permission is hereby granted, free of charge, to any person obtaining a copy of this software and
|
||||
associated documentation files (the "Software"), to deal in the Software without restriction,
|
||||
including without limitation the rights to use, copy, modify, merge, publish, distribute,
|
||||
sublicense, and/or sell copies of the Software, and to permit persons to whom the Software is
|
||||
furnished to do so, subject to the following conditions:
|
||||
|
||||
The above copyright notice and this permission notice shall be included in all copies or
|
||||
substantial portions of the Software.
|
||||
|
||||
THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR IMPLIED, INCLUDING BUT
|
||||
NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND
|
||||
NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM,
|
||||
DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT
|
||||
OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
|
||||
**************************************************************************************************/
|
||||
|
||||
#ifndef Glucose_Sort_h
|
||||
#define Glucose_Sort_h
|
||||
|
||||
#include "sat/glucose/Vec.h"
|
||||
|
||||
//=================================================================================================
|
||||
// Some sorting algorithms for vec's
|
||||
|
||||
|
||||
namespace Glucose {
|
||||
|
||||
template<class T>
|
||||
struct LessThan_default {
|
||||
bool operator () (T x, T y) { return x < y; }
|
||||
};
|
||||
|
||||
|
||||
template <class T, class LessThan>
|
||||
void selectionSort(T* array, int size, LessThan lt)
|
||||
{
|
||||
int i, j, best_i;
|
||||
T tmp;
|
||||
|
||||
for (i = 0; i < size-1; i++){
|
||||
best_i = i;
|
||||
for (j = i+1; j < size; j++){
|
||||
if (lt(array[j], array[best_i]))
|
||||
best_i = j;
|
||||
}
|
||||
tmp = array[i]; array[i] = array[best_i]; array[best_i] = tmp;
|
||||
}
|
||||
}
|
||||
template <class T> static inline void selectionSort(T* array, int size) {
|
||||
selectionSort(array, size, LessThan_default<T>()); }
|
||||
|
||||
template <class T, class LessThan>
|
||||
void sort(T* array, int size, LessThan lt)
|
||||
{
|
||||
if (size <= 15)
|
||||
selectionSort(array, size, lt);
|
||||
|
||||
else{
|
||||
T pivot = array[size / 2];
|
||||
T tmp;
|
||||
int i = -1;
|
||||
int j = size;
|
||||
|
||||
for(;;){
|
||||
do i++; while(lt(array[i], pivot));
|
||||
do j--; while(lt(pivot, array[j]));
|
||||
|
||||
if (i >= j) break;
|
||||
|
||||
tmp = array[i]; array[i] = array[j]; array[j] = tmp;
|
||||
}
|
||||
|
||||
sort(array , i , lt);
|
||||
sort(&array[i], size-i, lt);
|
||||
}
|
||||
}
|
||||
template <class T> static inline void sort(T* array, int size) {
|
||||
sort(array, size, LessThan_default<T>()); }
|
||||
|
||||
|
||||
//=================================================================================================
|
||||
// For 'vec's:
|
||||
|
||||
|
||||
template <class T, class LessThan> void sort(vec<T>& v, LessThan lt) {
|
||||
sort((T*)v, v.size(), lt); }
|
||||
template <class T> void sort(vec<T>& v) {
|
||||
sort(v, LessThan_default<T>()); }
|
||||
|
||||
|
||||
//=================================================================================================
|
||||
}
|
||||
|
||||
#endif
|
||||
|
|
@ -0,0 +1,95 @@
|
|||
/***************************************************************************************[System.cc]
|
||||
Copyright (c) 2003-2006, Niklas Een, Niklas Sorensson
|
||||
Copyright (c) 2007-2010, Niklas Sorensson
|
||||
|
||||
Permission is hereby granted, free of charge, to any person obtaining a copy of this software and
|
||||
associated documentation files (the "Software"), to deal in the Software without restriction,
|
||||
including without limitation the rights to use, copy, modify, merge, publish, distribute,
|
||||
sublicense, and/or sell copies of the Software, and to permit persons to whom the Software is
|
||||
furnished to do so, subject to the following conditions:
|
||||
|
||||
The above copyright notice and this permission notice shall be included in all copies or
|
||||
substantial portions of the Software.
|
||||
|
||||
THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR IMPLIED, INCLUDING BUT
|
||||
NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND
|
||||
NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM,
|
||||
DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT
|
||||
OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
|
||||
**************************************************************************************************/
|
||||
|
||||
#include "sat/glucose/System.h"
|
||||
|
||||
#if defined(__linux__)
|
||||
|
||||
#include <stdio.h>
|
||||
#include <stdlib.h>
|
||||
|
||||
using namespace Glucose;
|
||||
|
||||
// TODO: split the memory reading functions into two: one for reading high-watermark of RSS, and
|
||||
// one for reading the current virtual memory size.
|
||||
|
||||
static inline int memReadStat(int field)
|
||||
{
|
||||
char name[256];
|
||||
pid_t pid = getpid();
|
||||
int value;
|
||||
|
||||
sprintf(name, "/proc/%d/statm", pid);
|
||||
FILE* in = fopen(name, "rb");
|
||||
if (in == NULL) return 0;
|
||||
|
||||
for (; field >= 0; field--)
|
||||
if (fscanf(in, "%d", &value) != 1)
|
||||
printf("ERROR! Failed to parse memory statistics from \"/proc\".\n"), exit(1);
|
||||
fclose(in);
|
||||
return value;
|
||||
}
|
||||
|
||||
|
||||
static inline int memReadPeak(void)
|
||||
{
|
||||
char name[256];
|
||||
pid_t pid = getpid();
|
||||
|
||||
sprintf(name, "/proc/%d/status", pid);
|
||||
FILE* in = fopen(name, "rb");
|
||||
if (in == NULL) return 0;
|
||||
|
||||
// Find the correct line, beginning with "VmPeak:":
|
||||
int peak_kb = 0;
|
||||
while (!feof(in) && fscanf(in, "VmPeak: %d kB", &peak_kb) != 1)
|
||||
while (!feof(in) && fgetc(in) != '\n')
|
||||
;
|
||||
fclose(in);
|
||||
|
||||
return peak_kb;
|
||||
}
|
||||
|
||||
double Glucose::memUsed() { return (double)memReadStat(0) * (double)getpagesize() / (1024*1024); }
|
||||
double Glucose::memUsedPeak() {
|
||||
double peak = memReadPeak() / 1024;
|
||||
return peak == 0 ? memUsed() : peak; }
|
||||
|
||||
#elif defined(__FreeBSD__)
|
||||
|
||||
double Glucose::memUsed(void) {
|
||||
struct rusage ru;
|
||||
getrusage(RUSAGE_SELF, &ru);
|
||||
return (double)ru.ru_maxrss / 1024; }
|
||||
double MiniSat::memUsedPeak(void) { return memUsed(); }
|
||||
|
||||
|
||||
#elif defined(__APPLE__)
|
||||
#include <malloc/malloc.h>
|
||||
|
||||
double Glucose::memUsed(void) {
|
||||
malloc_statistics_t t;
|
||||
malloc_zone_statistics(NULL, &t);
|
||||
return (double)t.max_size_in_use / (1024*1024); }
|
||||
|
||||
#else
|
||||
double Glucose::memUsed() {
|
||||
return 0; }
|
||||
#endif
|
||||
|
|
@ -0,0 +1,60 @@
|
|||
/****************************************************************************************[System.h]
|
||||
Copyright (c) 2003-2006, Niklas Een, Niklas Sorensson
|
||||
Copyright (c) 2007-2010, Niklas Sorensson
|
||||
|
||||
Permission is hereby granted, free of charge, to any person obtaining a copy of this software and
|
||||
associated documentation files (the "Software"), to deal in the Software without restriction,
|
||||
including without limitation the rights to use, copy, modify, merge, publish, distribute,
|
||||
sublicense, and/or sell copies of the Software, and to permit persons to whom the Software is
|
||||
furnished to do so, subject to the following conditions:
|
||||
|
||||
The above copyright notice and this permission notice shall be included in all copies or
|
||||
substantial portions of the Software.
|
||||
|
||||
THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR IMPLIED, INCLUDING BUT
|
||||
NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND
|
||||
NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM,
|
||||
DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT
|
||||
OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
|
||||
**************************************************************************************************/
|
||||
|
||||
#ifndef Glucose_System_h
|
||||
#define Glucose_System_h
|
||||
|
||||
#if defined(__linux__)
|
||||
#include <fpu_control.h>
|
||||
#endif
|
||||
|
||||
#include "sat/glucose/IntTypes.h"
|
||||
|
||||
//-------------------------------------------------------------------------------------------------
|
||||
|
||||
namespace Glucose {
|
||||
|
||||
static inline double cpuTime(void); // CPU-time in seconds.
|
||||
extern double memUsed(); // Memory in mega bytes (returns 0 for unsupported architectures).
|
||||
extern double memUsedPeak(); // Peak-memory in mega bytes (returns 0 for unsupported architectures).
|
||||
|
||||
}
|
||||
|
||||
//-------------------------------------------------------------------------------------------------
|
||||
// Implementation of inline functions:
|
||||
|
||||
#if defined(_MSC_VER) || defined(__MINGW32__)
|
||||
#include <time.h>
|
||||
|
||||
static inline double Glucose::cpuTime(void) { return (double)clock() / CLOCKS_PER_SEC; }
|
||||
|
||||
#else
|
||||
#include <sys/time.h>
|
||||
#include <sys/resource.h>
|
||||
#include <unistd.h>
|
||||
|
||||
static inline double Glucose::cpuTime(void) {
|
||||
struct rusage ru;
|
||||
getrusage(RUSAGE_SELF, &ru);
|
||||
return (double)ru.ru_utime.tv_sec + (double)ru.ru_utime.tv_usec / 1000000; }
|
||||
|
||||
#endif
|
||||
|
||||
#endif
|
||||
|
|
@ -0,0 +1,130 @@
|
|||
/*******************************************************************************************[Vec.h]
|
||||
Copyright (c) 2003-2007, Niklas Een, Niklas Sorensson
|
||||
Copyright (c) 2007-2010, Niklas Sorensson
|
||||
|
||||
Permission is hereby granted, free of charge, to any person obtaining a copy of this software and
|
||||
associated documentation files (the "Software"), to deal in the Software without restriction,
|
||||
including without limitation the rights to use, copy, modify, merge, publish, distribute,
|
||||
sublicense, and/or sell copies of the Software, and to permit persons to whom the Software is
|
||||
furnished to do so, subject to the following conditions:
|
||||
|
||||
The above copyright notice and this permission notice shall be included in all copies or
|
||||
substantial portions of the Software.
|
||||
|
||||
THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR IMPLIED, INCLUDING BUT
|
||||
NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND
|
||||
NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM,
|
||||
DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT
|
||||
OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
|
||||
**************************************************************************************************/
|
||||
|
||||
#ifndef Glucose_Vec_h
|
||||
#define Glucose_Vec_h
|
||||
|
||||
#include <assert.h>
|
||||
#include <new>
|
||||
|
||||
#include "sat/glucose/IntTypes.h"
|
||||
#include "sat/glucose/XAlloc.h"
|
||||
|
||||
namespace Glucose {
|
||||
|
||||
//=================================================================================================
|
||||
// Automatically resizable arrays
|
||||
//
|
||||
// NOTE! Don't use this vector on datatypes that cannot be re-located in memory (with realloc)
|
||||
|
||||
template<class T>
|
||||
class vec {
|
||||
T* data;
|
||||
int sz;
|
||||
int cap;
|
||||
|
||||
// Don't allow copying (error prone):
|
||||
vec<T>& operator = (vec<T>& other) { assert(0); return *this; }
|
||||
vec (vec<T>& other) { assert(0); }
|
||||
|
||||
// Helpers for calculating next capacity:
|
||||
static inline int imax (int x, int y) { int mask = (y-x) >> (sizeof(int)*8-1); return (x&mask) + (y&(~mask)); }
|
||||
//static inline void nextCap(int& cap){ cap += ((cap >> 1) + 2) & ~1; }
|
||||
static inline void nextCap(int& cap){ cap += ((cap >> 1) + 2) & ~1; }
|
||||
|
||||
public:
|
||||
// Constructors:
|
||||
vec() : data(NULL) , sz(0) , cap(0) { }
|
||||
explicit vec(int size) : data(NULL) , sz(0) , cap(0) { growTo(size); }
|
||||
vec(int size, const T& pad) : data(NULL) , sz(0) , cap(0) { growTo(size, pad); }
|
||||
~vec() { clear(true); }
|
||||
|
||||
// Pointer to first element:
|
||||
operator T* (void) { return data; }
|
||||
|
||||
// Size operations:
|
||||
int size (void) const { return sz; }
|
||||
void shrink (int nelems) { assert(nelems <= sz); for (int i = 0; i < nelems; i++) sz--, data[sz].~T(); }
|
||||
void shrink_ (int nelems) { assert(nelems <= sz); sz -= nelems; }
|
||||
int capacity (void) const { return cap; }
|
||||
void capacity (int min_cap);
|
||||
void growTo (int size);
|
||||
void growTo (int size, const T& pad);
|
||||
void clear (bool dealloc = false);
|
||||
|
||||
// Stack interface:
|
||||
void push (void) { if (sz == cap) capacity(sz+1); new (&data[sz]) T(); sz++; }
|
||||
void push (const T& elem) { if (sz == cap) capacity(sz+1); data[sz++] = elem; }
|
||||
void push_ (const T& elem) { assert(sz < cap); data[sz++] = elem; }
|
||||
void pop (void) { assert(sz > 0); sz--, data[sz].~T(); }
|
||||
// NOTE: it seems possible that overflow can happen in the 'sz+1' expression of 'push()', but
|
||||
// in fact it can not since it requires that 'cap' is equal to INT_MAX. This in turn can not
|
||||
// happen given the way capacities are calculated (below). Essentially, all capacities are
|
||||
// even, but INT_MAX is odd.
|
||||
|
||||
const T& last (void) const { return data[sz-1]; }
|
||||
T& last (void) { return data[sz-1]; }
|
||||
|
||||
// Vector interface:
|
||||
const T& operator [] (int index) const { return data[index]; }
|
||||
T& operator [] (int index) { return data[index]; }
|
||||
|
||||
// Duplicatation (preferred instead):
|
||||
void copyTo(vec<T>& copy) const { copy.clear(); copy.growTo(sz); for (int i = 0; i < sz; i++) copy[i] = data[i]; }
|
||||
void moveTo(vec<T>& dest) { dest.clear(true); dest.data = data; dest.sz = sz; dest.cap = cap; data = NULL; sz = 0; cap = 0; }
|
||||
};
|
||||
|
||||
|
||||
template<class T>
|
||||
void vec<T>::capacity(int min_cap) {
|
||||
if (cap >= min_cap) return;
|
||||
int add = imax((min_cap - cap + 1) & ~1, ((cap >> 1) + 2) & ~1); // NOTE: grow by approximately 3/2
|
||||
if (add > INT_MAX - cap || ((data = (T*)::realloc(data, (cap += add) * sizeof(T))) == NULL) && errno == ENOMEM)
|
||||
throw OutOfMemoryException();
|
||||
}
|
||||
|
||||
|
||||
template<class T>
|
||||
void vec<T>::growTo(int size, const T& pad) {
|
||||
if (sz >= size) return;
|
||||
capacity(size);
|
||||
for (int i = sz; i < size; i++) data[i] = pad;
|
||||
sz = size; }
|
||||
|
||||
|
||||
template<class T>
|
||||
void vec<T>::growTo(int size) {
|
||||
if (sz >= size) return;
|
||||
capacity(size);
|
||||
for (int i = sz; i < size; i++) new (&data[i]) T();
|
||||
sz = size; }
|
||||
|
||||
|
||||
template<class T>
|
||||
void vec<T>::clear(bool dealloc) {
|
||||
if (data != NULL){
|
||||
for (int i = 0; i < sz; i++) data[i].~T();
|
||||
sz = 0;
|
||||
if (dealloc) free(data), data = NULL, cap = 0; } }
|
||||
|
||||
//=================================================================================================
|
||||
}
|
||||
|
||||
#endif
|
||||
|
|
@ -0,0 +1,47 @@
|
|||
/****************************************************************************************[XAlloc.h]
|
||||
Copyright (c) 2009-2010, Niklas Sorensson
|
||||
|
||||
Permission is hereby granted, free of charge, to any person obtaining a copy of this software and
|
||||
associated documentation files (the "Software"), to deal in the Software without restriction,
|
||||
including without limitation the rights to use, copy, modify, merge, publish, distribute,
|
||||
sublicense, and/or sell copies of the Software, and to permit persons to whom the Software is
|
||||
furnished to do so, subject to the following conditions:
|
||||
|
||||
The above copyright notice and this permission notice shall be included in all copies or
|
||||
substantial portions of the Software.
|
||||
|
||||
THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR IMPLIED, INCLUDING BUT
|
||||
NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND
|
||||
NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM,
|
||||
DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT
|
||||
OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
|
||||
**************************************************************************************************/
|
||||
|
||||
|
||||
#ifndef Glucose_XAlloc_h
|
||||
#define Glucose_XAlloc_h
|
||||
|
||||
#include <errno.h>
|
||||
#include <stdlib.h>
|
||||
#include <stdio.h>
|
||||
|
||||
namespace Glucose {
|
||||
|
||||
//=================================================================================================
|
||||
// Simple layer on top of malloc/realloc to catch out-of-memory situtaions and provide some typing:
|
||||
|
||||
class OutOfMemoryException{};
|
||||
static inline void* xrealloc(void *ptr, size_t size)
|
||||
{
|
||||
void* mem = realloc(ptr, size);
|
||||
if (mem == NULL && errno == ENOMEM){
|
||||
throw OutOfMemoryException();
|
||||
}else {
|
||||
return mem;
|
||||
}
|
||||
}
|
||||
|
||||
//=================================================================================================
|
||||
}
|
||||
|
||||
#endif
|
||||
|
|
@ -0,0 +1,919 @@
|
|||
/* A portable stdint.h
|
||||
****************************************************************************
|
||||
* BSD License:
|
||||
****************************************************************************
|
||||
*
|
||||
* Copyright (c) 2005-2016 Paul Hsieh
|
||||
* All rights reserved.
|
||||
*
|
||||
* Redistribution and use in source and binary forms, with or without
|
||||
* modification, are permitted provided that the following conditions
|
||||
* are met:
|
||||
*
|
||||
* 1. Redistributions of source code must retain the above copyright
|
||||
* notice, this list of conditions and the following disclaimer.
|
||||
* 2. Redistributions in binary form must reproduce the above copyright
|
||||
* notice, this list of conditions and the following disclaimer in the
|
||||
* documentation and/or other materials provided with the distribution.
|
||||
* 3. The name of the author may not be used to endorse or promote products
|
||||
* derived from this software without specific prior written permission.
|
||||
*
|
||||
* THIS SOFTWARE IS PROVIDED BY THE AUTHOR ``AS IS'' AND ANY EXPRESS OR
|
||||
* IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED WARRANTIES
|
||||
* OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE DISCLAIMED.
|
||||
* IN NO EVENT SHALL THE AUTHOR BE LIABLE FOR ANY DIRECT, INDIRECT,
|
||||
* INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT
|
||||
* NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE,
|
||||
* DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY
|
||||
* THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT
|
||||
* (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF
|
||||
* THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
|
||||
*
|
||||
****************************************************************************
|
||||
*
|
||||
* Version 0.1.16.0
|
||||
*
|
||||
* The ANSI C standard committee, for the C99 standard, specified the
|
||||
* inclusion of a new standard include file called stdint.h. This is
|
||||
* a very useful and long desired include file which contains several
|
||||
* very precise definitions for integer scalar types that is critically
|
||||
* important for making several classes of applications portable
|
||||
* including cryptography, hashing, variable length integer libraries
|
||||
* and so on. But for most developers its likely useful just for
|
||||
* programming sanity.
|
||||
*
|
||||
* The problem is that some compiler vendors chose to ignore the C99
|
||||
* standard and some older compilers have no opportunity to be updated.
|
||||
* Because of this situation, simply including stdint.h in your code
|
||||
* makes it unportable.
|
||||
*
|
||||
* So that's what this file is all about. It's an attempt to build a
|
||||
* single universal include file that works on as many platforms as
|
||||
* possible to deliver what stdint.h is supposed to. Even compilers
|
||||
* that already come with stdint.h can use this file instead without
|
||||
* any loss of functionality. A few things that should be noted about
|
||||
* this file:
|
||||
*
|
||||
* 1) It is not guaranteed to be portable and/or present an identical
|
||||
* interface on all platforms. The extreme variability of the
|
||||
* ANSI C standard makes this an impossibility right from the
|
||||
* very get go. Its really only meant to be useful for the vast
|
||||
* majority of platforms that possess the capability of
|
||||
* implementing usefully and precisely defined, standard sized
|
||||
* integer scalars. Systems which are not intrinsically 2s
|
||||
* complement may produce invalid constants.
|
||||
*
|
||||
* 2) There is an unavoidable use of non-reserved symbols.
|
||||
*
|
||||
* 3) Other standard include files are invoked.
|
||||
*
|
||||
* 4) This file may come in conflict with future platforms that do
|
||||
* include stdint.h. The hope is that one or the other can be
|
||||
* used with no real difference.
|
||||
*
|
||||
* 5) In the current version, if your platform can't represent
|
||||
* int32_t, int16_t and int8_t, it just dumps out with a compiler
|
||||
* error.
|
||||
*
|
||||
* 6) 64 bit integers may or may not be defined. Test for their
|
||||
* presence with the test: #ifdef INT64_MAX or #ifdef UINT64_MAX.
|
||||
* Note that this is different from the C99 specification which
|
||||
* requires the existence of 64 bit support in the compiler. If
|
||||
* this is not defined for your platform, yet it is capable of
|
||||
* dealing with 64 bits then it is because this file has not yet
|
||||
* been extended to cover all of your system's capabilities.
|
||||
*
|
||||
* 7) (u)intptr_t may or may not be defined. Test for its presence
|
||||
* with the test: #ifdef PTRDIFF_MAX. If this is not defined
|
||||
* for your platform, then it is because this file has not yet
|
||||
* been extended to cover all of your system's capabilities, not
|
||||
* because its optional.
|
||||
*
|
||||
* 8) The following might not been defined even if your platform is
|
||||
* capable of defining it:
|
||||
*
|
||||
* WCHAR_MIN
|
||||
* WCHAR_MAX
|
||||
* (u)int64_t
|
||||
* PTRDIFF_MIN
|
||||
* PTRDIFF_MAX
|
||||
* (u)intptr_t
|
||||
*
|
||||
* 9) The following have not been defined:
|
||||
*
|
||||
* WINT_MIN
|
||||
* WINT_MAX
|
||||
*
|
||||
* 10) The criteria for defining (u)int_least(*)_t isn't clear,
|
||||
* except for systems which don't have a type that precisely
|
||||
* defined 8, 16, or 32 bit types (which this include file does
|
||||
* not support anyways). Default definitions have been given.
|
||||
*
|
||||
* 11) The criteria for defining (u)int_fast(*)_t isn't something I
|
||||
* would trust to any particular compiler vendor or the ANSI C
|
||||
* committee. It is well known that "compatible systems" are
|
||||
* commonly created that have very different performance
|
||||
* characteristics from the systems they are compatible with,
|
||||
* especially those whose vendors make both the compiler and the
|
||||
* system. Default definitions have been given, but its strongly
|
||||
* recommended that users never use these definitions for any
|
||||
* reason (they do *NOT* deliver any serious guarantee of
|
||||
* improved performance -- not in this file, nor any vendor's
|
||||
* stdint.h).
|
||||
*
|
||||
* 12) The following macros:
|
||||
*
|
||||
* PRINTF_INTMAX_MODIFIER
|
||||
* PRINTF_INT64_MODIFIER
|
||||
* PRINTF_INT32_MODIFIER
|
||||
* PRINTF_INT16_MODIFIER
|
||||
* PRINTF_LEAST64_MODIFIER
|
||||
* PRINTF_LEAST32_MODIFIER
|
||||
* PRINTF_LEAST16_MODIFIER
|
||||
* PRINTF_INTPTR_MODIFIER
|
||||
*
|
||||
* are strings which have been defined as the modifiers required
|
||||
* for the "d", "u" and "x" printf formats to correctly output
|
||||
* (u)intmax_t, (u)int64_t, (u)int32_t, (u)int16_t, (u)least64_t,
|
||||
* (u)least32_t, (u)least16_t and (u)intptr_t types respectively.
|
||||
* PRINTF_INTPTR_MODIFIER is not defined for some systems which
|
||||
* provide their own stdint.h. PRINTF_INT64_MODIFIER is not
|
||||
* defined if INT64_MAX is not defined. These are an extension
|
||||
* beyond what C99 specifies must be in stdint.h.
|
||||
*
|
||||
* In addition, the following macros are defined:
|
||||
*
|
||||
* PRINTF_INTMAX_HEX_WIDTH
|
||||
* PRINTF_INT64_HEX_WIDTH
|
||||
* PRINTF_INT32_HEX_WIDTH
|
||||
* PRINTF_INT16_HEX_WIDTH
|
||||
* PRINTF_INT8_HEX_WIDTH
|
||||
* PRINTF_INTMAX_DEC_WIDTH
|
||||
* PRINTF_INT64_DEC_WIDTH
|
||||
* PRINTF_INT32_DEC_WIDTH
|
||||
* PRINTF_INT16_DEC_WIDTH
|
||||
* PRINTF_UINT8_DEC_WIDTH
|
||||
* PRINTF_UINTMAX_DEC_WIDTH
|
||||
* PRINTF_UINT64_DEC_WIDTH
|
||||
* PRINTF_UINT32_DEC_WIDTH
|
||||
* PRINTF_UINT16_DEC_WIDTH
|
||||
* PRINTF_UINT8_DEC_WIDTH
|
||||
*
|
||||
* Which specifies the maximum number of characters required to
|
||||
* print the number of that type in either hexadecimal or decimal.
|
||||
* These are an extension beyond what C99 specifies must be in
|
||||
* stdint.h.
|
||||
*
|
||||
* Compilers tested (all with 0 warnings at their highest respective
|
||||
* settings): Borland Turbo C 2.0, WATCOM C/C++ 11.0 (16 bits and 32
|
||||
* bits), Microsoft Visual C++ 6.0 (32 bit), Microsoft Visual Studio
|
||||
* .net (VC7), Intel C++ 4.0, GNU gcc v3.3.3
|
||||
*
|
||||
* This file should be considered a work in progress. Suggestions for
|
||||
* improvements, especially those which increase coverage are strongly
|
||||
* encouraged.
|
||||
*
|
||||
* Acknowledgements
|
||||
*
|
||||
* The following people have made significant contributions to the
|
||||
* development and testing of this file:
|
||||
*
|
||||
* Chris Howie
|
||||
* John Steele Scott
|
||||
* Dave Thorup
|
||||
* John Dill
|
||||
* Florian Wobbe
|
||||
* Christopher Sean Morrison
|
||||
* Mikkel Fahnoe Jorgensen
|
||||
*
|
||||
*/
|
||||
|
||||
#include <stddef.h>
|
||||
#include <limits.h>
|
||||
#include <signal.h>
|
||||
|
||||
/*
|
||||
* For gcc with _STDINT_H, fill in the PRINTF_INT*_MODIFIER macros, and
|
||||
* do nothing else. On the Mac OS X version of gcc this is _STDINT_H_.
|
||||
*/
|
||||
|
||||
#if ((defined(__SUNPRO_C) && __SUNPRO_C >= 0x570) || (defined(_MSC_VER) && _MSC_VER >= 1600) || (defined(__STDC__) && __STDC__ && defined(__STDC_VERSION__) && __STDC_VERSION__ >= 199901L) || (defined (__WATCOMC__) && (defined (_STDINT_H_INCLUDED) || __WATCOMC__ >= 1250)) || (defined(__GNUC__) && (__GNUC__ > 3 || defined(_STDINT_H) || defined(_STDINT_H_) || defined (__UINT_FAST64_TYPE__)) )) && !defined (_PSTDINT_H_INCLUDED)
|
||||
#include <stdint.h>
|
||||
#define _PSTDINT_H_INCLUDED
|
||||
# if defined(__GNUC__) && (defined(__x86_64__) || defined(__ppc64__)) && !(defined(__APPLE__) && defined(__MACH__))
|
||||
# ifndef PRINTF_INT64_MODIFIER
|
||||
# define PRINTF_INT64_MODIFIER "l"
|
||||
# endif
|
||||
# ifndef PRINTF_INT32_MODIFIER
|
||||
# define PRINTF_INT32_MODIFIER ""
|
||||
# endif
|
||||
# else
|
||||
# ifndef PRINTF_INT64_MODIFIER
|
||||
# define PRINTF_INT64_MODIFIER "ll"
|
||||
# endif
|
||||
# ifndef PRINTF_INT32_MODIFIER
|
||||
# if (UINT_MAX == UINT32_MAX)
|
||||
# define PRINTF_INT32_MODIFIER ""
|
||||
# else
|
||||
# define PRINTF_INT32_MODIFIER "l"
|
||||
# endif
|
||||
# endif
|
||||
# endif
|
||||
# ifndef PRINTF_INT16_MODIFIER
|
||||
# define PRINTF_INT16_MODIFIER "h"
|
||||
# endif
|
||||
# ifndef PRINTF_INTMAX_MODIFIER
|
||||
# define PRINTF_INTMAX_MODIFIER PRINTF_INT64_MODIFIER
|
||||
# endif
|
||||
# ifndef PRINTF_INT64_HEX_WIDTH
|
||||
# define PRINTF_INT64_HEX_WIDTH "16"
|
||||
# endif
|
||||
# ifndef PRINTF_UINT64_HEX_WIDTH
|
||||
# define PRINTF_UINT64_HEX_WIDTH "16"
|
||||
# endif
|
||||
# ifndef PRINTF_INT32_HEX_WIDTH
|
||||
# define PRINTF_INT32_HEX_WIDTH "8"
|
||||
# endif
|
||||
# ifndef PRINTF_UINT32_HEX_WIDTH
|
||||
# define PRINTF_UINT32_HEX_WIDTH "8"
|
||||
# endif
|
||||
# ifndef PRINTF_INT16_HEX_WIDTH
|
||||
# define PRINTF_INT16_HEX_WIDTH "4"
|
||||
# endif
|
||||
# ifndef PRINTF_UINT16_HEX_WIDTH
|
||||
# define PRINTF_UINT16_HEX_WIDTH "4"
|
||||
# endif
|
||||
# ifndef PRINTF_INT8_HEX_WIDTH
|
||||
# define PRINTF_INT8_HEX_WIDTH "2"
|
||||
# endif
|
||||
# ifndef PRINTF_UINT8_HEX_WIDTH
|
||||
# define PRINTF_UINT8_HEX_WIDTH "2"
|
||||
# endif
|
||||
# ifndef PRINTF_INT64_DEC_WIDTH
|
||||
# define PRINTF_INT64_DEC_WIDTH "19"
|
||||
# endif
|
||||
# ifndef PRINTF_UINT64_DEC_WIDTH
|
||||
# define PRINTF_UINT64_DEC_WIDTH "20"
|
||||
# endif
|
||||
# ifndef PRINTF_INT32_DEC_WIDTH
|
||||
# define PRINTF_INT32_DEC_WIDTH "10"
|
||||
# endif
|
||||
# ifndef PRINTF_UINT32_DEC_WIDTH
|
||||
# define PRINTF_UINT32_DEC_WIDTH "10"
|
||||
# endif
|
||||
# ifndef PRINTF_INT16_DEC_WIDTH
|
||||
# define PRINTF_INT16_DEC_WIDTH "5"
|
||||
# endif
|
||||
# ifndef PRINTF_UINT16_DEC_WIDTH
|
||||
# define PRINTF_UINT16_DEC_WIDTH "5"
|
||||
# endif
|
||||
# ifndef PRINTF_INT8_DEC_WIDTH
|
||||
# define PRINTF_INT8_DEC_WIDTH "3"
|
||||
# endif
|
||||
# ifndef PRINTF_UINT8_DEC_WIDTH
|
||||
# define PRINTF_UINT8_DEC_WIDTH "3"
|
||||
# endif
|
||||
# ifndef PRINTF_INTMAX_HEX_WIDTH
|
||||
# define PRINTF_INTMAX_HEX_WIDTH PRINTF_UINT64_HEX_WIDTH
|
||||
# endif
|
||||
# ifndef PRINTF_UINTMAX_HEX_WIDTH
|
||||
# define PRINTF_UINTMAX_HEX_WIDTH PRINTF_UINT64_HEX_WIDTH
|
||||
# endif
|
||||
# ifndef PRINTF_INTMAX_DEC_WIDTH
|
||||
# define PRINTF_INTMAX_DEC_WIDTH PRINTF_UINT64_DEC_WIDTH
|
||||
# endif
|
||||
# ifndef PRINTF_UINTMAX_DEC_WIDTH
|
||||
# define PRINTF_UINTMAX_DEC_WIDTH PRINTF_UINT64_DEC_WIDTH
|
||||
# endif
|
||||
|
||||
/*
|
||||
* Something really weird is going on with Open Watcom. Just pull some of
|
||||
* these duplicated definitions from Open Watcom's stdint.h file for now.
|
||||
*/
|
||||
|
||||
# if defined (__WATCOMC__) && __WATCOMC__ >= 1250
|
||||
# if !defined (INT64_C)
|
||||
# define INT64_C(x) (x + (INT64_MAX - INT64_MAX))
|
||||
# endif
|
||||
# if !defined (UINT64_C)
|
||||
# define UINT64_C(x) (x + (UINT64_MAX - UINT64_MAX))
|
||||
# endif
|
||||
# if !defined (INT32_C)
|
||||
# define INT32_C(x) (x + (INT32_MAX - INT32_MAX))
|
||||
# endif
|
||||
# if !defined (UINT32_C)
|
||||
# define UINT32_C(x) (x + (UINT32_MAX - UINT32_MAX))
|
||||
# endif
|
||||
# if !defined (INT16_C)
|
||||
# define INT16_C(x) (x)
|
||||
# endif
|
||||
# if !defined (UINT16_C)
|
||||
# define UINT16_C(x) (x)
|
||||
# endif
|
||||
# if !defined (INT8_C)
|
||||
# define INT8_C(x) (x)
|
||||
# endif
|
||||
# if !defined (UINT8_C)
|
||||
# define UINT8_C(x) (x)
|
||||
# endif
|
||||
# if !defined (UINT64_MAX)
|
||||
# define UINT64_MAX 18446744073709551615ULL
|
||||
# endif
|
||||
# if !defined (INT64_MAX)
|
||||
# define INT64_MAX 9223372036854775807LL
|
||||
# endif
|
||||
# if !defined (UINT32_MAX)
|
||||
# define UINT32_MAX 4294967295UL
|
||||
# endif
|
||||
# if !defined (INT32_MAX)
|
||||
# define INT32_MAX 2147483647L
|
||||
# endif
|
||||
# if !defined (INTMAX_MAX)
|
||||
# define INTMAX_MAX INT64_MAX
|
||||
# endif
|
||||
# if !defined (INTMAX_MIN)
|
||||
# define INTMAX_MIN INT64_MIN
|
||||
# endif
|
||||
# endif
|
||||
#endif
|
||||
|
||||
/*
|
||||
* I have no idea what is the truly correct thing to do on older Solaris.
|
||||
* From some online discussions, this seems to be what is being
|
||||
* recommended. For people who actually are developing on older Solaris,
|
||||
* what I would like to know is, does this define all of the relevant
|
||||
* macros of a complete stdint.h? Remember, in pstdint.h 64 bit is
|
||||
* considered optional.
|
||||
*/
|
||||
|
||||
#if (defined(__SUNPRO_C) && __SUNPRO_C >= 0x420) && !defined(_PSTDINT_H_INCLUDED)
|
||||
#include <sys/inttypes.h>
|
||||
#define _PSTDINT_H_INCLUDED
|
||||
#endif
|
||||
|
||||
#ifndef _PSTDINT_H_INCLUDED
|
||||
#define _PSTDINT_H_INCLUDED
|
||||
|
||||
#ifndef SIZE_MAX
|
||||
# define SIZE_MAX ((size_t)-1)
|
||||
#endif
|
||||
|
||||
/*
|
||||
* Deduce the type assignments from limits.h under the assumption that
|
||||
* integer sizes in bits are powers of 2, and follow the ANSI
|
||||
* definitions.
|
||||
*/
|
||||
|
||||
#ifndef UINT8_MAX
|
||||
# define UINT8_MAX 0xff
|
||||
#endif
|
||||
#if !defined(uint8_t) && !defined(_UINT8_T) && !defined(vxWorks)
|
||||
# if (UCHAR_MAX == UINT8_MAX) || defined (S_SPLINT_S)
|
||||
typedef unsigned char uint8_t;
|
||||
# define UINT8_C(v) ((uint8_t) v)
|
||||
# else
|
||||
# error "Platform not supported"
|
||||
# endif
|
||||
#endif
|
||||
|
||||
#ifndef INT8_MAX
|
||||
# define INT8_MAX 0x7f
|
||||
#endif
|
||||
#ifndef INT8_MIN
|
||||
# define INT8_MIN INT8_C(0x80)
|
||||
#endif
|
||||
#if !defined(int8_t) && !defined(_INT8_T) && !defined(vxWorks)
|
||||
# if (SCHAR_MAX == INT8_MAX) || defined (S_SPLINT_S)
|
||||
typedef signed char int8_t;
|
||||
# define INT8_C(v) ((int8_t) v)
|
||||
# else
|
||||
# error "Platform not supported"
|
||||
# endif
|
||||
#endif
|
||||
|
||||
#ifndef UINT16_MAX
|
||||
# define UINT16_MAX 0xffff
|
||||
#endif
|
||||
#if !defined(uint16_t) && !defined(_UINT16_T) && !defined(vxWorks)
|
||||
#if (UINT_MAX == UINT16_MAX) || defined (S_SPLINT_S)
|
||||
typedef unsigned int uint16_t;
|
||||
# ifndef PRINTF_INT16_MODIFIER
|
||||
# define PRINTF_INT16_MODIFIER ""
|
||||
# endif
|
||||
# define UINT16_C(v) ((uint16_t) (v))
|
||||
#elif (USHRT_MAX == UINT16_MAX)
|
||||
typedef unsigned short uint16_t;
|
||||
# define UINT16_C(v) ((uint16_t) (v))
|
||||
# ifndef PRINTF_INT16_MODIFIER
|
||||
# define PRINTF_INT16_MODIFIER "h"
|
||||
# endif
|
||||
#else
|
||||
#error "Platform not supported"
|
||||
#endif
|
||||
#endif
|
||||
|
||||
#ifndef INT16_MAX
|
||||
# define INT16_MAX 0x7fff
|
||||
#endif
|
||||
#ifndef INT16_MIN
|
||||
# define INT16_MIN INT16_C(0x8000)
|
||||
#endif
|
||||
#if !defined(int16_t) && !defined(_INT16_T) && !defined(vxWorks)
|
||||
#if (INT_MAX == INT16_MAX) || defined (S_SPLINT_S)
|
||||
typedef signed int int16_t;
|
||||
# define INT16_C(v) ((int16_t) (v))
|
||||
# ifndef PRINTF_INT16_MODIFIER
|
||||
# define PRINTF_INT16_MODIFIER ""
|
||||
# endif
|
||||
#elif (SHRT_MAX == INT16_MAX)
|
||||
typedef signed short int16_t;
|
||||
# define INT16_C(v) ((int16_t) (v))
|
||||
# ifndef PRINTF_INT16_MODIFIER
|
||||
# define PRINTF_INT16_MODIFIER "h"
|
||||
# endif
|
||||
#else
|
||||
#error "Platform not supported"
|
||||
#endif
|
||||
#endif
|
||||
|
||||
#ifndef UINT32_MAX
|
||||
# define UINT32_MAX (0xffffffffUL)
|
||||
#endif
|
||||
#if !defined(uint32_t) && !defined(_UINT32_T) && !defined(vxWorks)
|
||||
#if (ULONG_MAX == UINT32_MAX) || defined (S_SPLINT_S)
|
||||
typedef unsigned long uint32_t;
|
||||
# define UINT32_C(v) v ## UL
|
||||
# ifndef PRINTF_INT32_MODIFIER
|
||||
# define PRINTF_INT32_MODIFIER "l"
|
||||
# endif
|
||||
#elif (UINT_MAX == UINT32_MAX)
|
||||
typedef unsigned int uint32_t;
|
||||
# ifndef PRINTF_INT32_MODIFIER
|
||||
# define PRINTF_INT32_MODIFIER ""
|
||||
# endif
|
||||
# define UINT32_C(v) v ## U
|
||||
#elif (USHRT_MAX == UINT32_MAX)
|
||||
typedef unsigned short uint32_t;
|
||||
# define UINT32_C(v) ((unsigned short) (v))
|
||||
# ifndef PRINTF_INT32_MODIFIER
|
||||
# define PRINTF_INT32_MODIFIER ""
|
||||
# endif
|
||||
#else
|
||||
#error "Platform not supported"
|
||||
#endif
|
||||
#endif
|
||||
|
||||
#ifndef INT32_MAX
|
||||
# define INT32_MAX (0x7fffffffL)
|
||||
#endif
|
||||
#ifndef INT32_MIN
|
||||
# define INT32_MIN INT32_C(0x80000000)
|
||||
#endif
|
||||
#if !defined(int32_t) && !defined(_INT32_T) && !defined(vxWorks)
|
||||
#if (LONG_MAX == INT32_MAX) || defined (S_SPLINT_S)
|
||||
typedef signed long int32_t;
|
||||
# define INT32_C(v) v ## L
|
||||
# ifndef PRINTF_INT32_MODIFIER
|
||||
# define PRINTF_INT32_MODIFIER "l"
|
||||
# endif
|
||||
#elif (INT_MAX == INT32_MAX)
|
||||
typedef signed int int32_t;
|
||||
# define INT32_C(v) v
|
||||
# ifndef PRINTF_INT32_MODIFIER
|
||||
# define PRINTF_INT32_MODIFIER ""
|
||||
# endif
|
||||
#elif (SHRT_MAX == INT32_MAX)
|
||||
typedef signed short int32_t;
|
||||
# define INT32_C(v) ((short) (v))
|
||||
# ifndef PRINTF_INT32_MODIFIER
|
||||
# define PRINTF_INT32_MODIFIER ""
|
||||
# endif
|
||||
#else
|
||||
#error "Platform not supported"
|
||||
#endif
|
||||
#endif
|
||||
|
||||
/*
|
||||
* The macro stdint_int64_defined is temporarily used to record
|
||||
* whether or not 64 integer support is available. It must be
|
||||
* defined for any 64 integer extensions for new platforms that are
|
||||
* added.
|
||||
*/
|
||||
|
||||
#undef stdint_int64_defined
|
||||
#if (defined(__STDC__) && defined(__STDC_VERSION__)) || defined (S_SPLINT_S)
|
||||
# if (__STDC__ && __STDC_VERSION__ >= 199901L) || defined (S_SPLINT_S)
|
||||
# define stdint_int64_defined
|
||||
typedef long long int64_t;
|
||||
typedef unsigned long long uint64_t;
|
||||
# define UINT64_C(v) v ## ULL
|
||||
# define INT64_C(v) v ## LL
|
||||
# ifndef PRINTF_INT64_MODIFIER
|
||||
# define PRINTF_INT64_MODIFIER "ll"
|
||||
# endif
|
||||
# endif
|
||||
#endif
|
||||
|
||||
#if !defined (stdint_int64_defined)
|
||||
# if defined(__GNUC__) && !defined(vxWorks)
|
||||
# define stdint_int64_defined
|
||||
__extension__ typedef long long int64_t;
|
||||
__extension__ typedef unsigned long long uint64_t;
|
||||
# define UINT64_C(v) v ## ULL
|
||||
# define INT64_C(v) v ## LL
|
||||
# ifndef PRINTF_INT64_MODIFIER
|
||||
# define PRINTF_INT64_MODIFIER "ll"
|
||||
# endif
|
||||
# elif defined(__MWERKS__) || defined (__SUNPRO_C) || defined (__SUNPRO_CC) || defined (__APPLE_CC__) || defined (_LONG_LONG) || defined (_CRAYC) || defined (S_SPLINT_S)
|
||||
# define stdint_int64_defined
|
||||
typedef long long int64_t;
|
||||
typedef unsigned long long uint64_t;
|
||||
# define UINT64_C(v) v ## ULL
|
||||
# define INT64_C(v) v ## LL
|
||||
# ifndef PRINTF_INT64_MODIFIER
|
||||
# define PRINTF_INT64_MODIFIER "ll"
|
||||
# endif
|
||||
# elif (defined(__WATCOMC__) && defined(__WATCOM_INT64__)) || (defined(_MSC_VER) && _INTEGRAL_MAX_BITS >= 64) || (defined (__BORLANDC__) && __BORLANDC__ > 0x460) || defined (__alpha) || defined (__DECC)
|
||||
# define stdint_int64_defined
|
||||
typedef __int64 int64_t;
|
||||
typedef unsigned __int64 uint64_t;
|
||||
# define UINT64_C(v) v ## UI64
|
||||
# define INT64_C(v) v ## I64
|
||||
# ifndef PRINTF_INT64_MODIFIER
|
||||
# define PRINTF_INT64_MODIFIER "I64"
|
||||
# endif
|
||||
# endif
|
||||
#endif
|
||||
|
||||
#if !defined (LONG_LONG_MAX) && defined (INT64_C)
|
||||
# define LONG_LONG_MAX INT64_C (9223372036854775807)
|
||||
#endif
|
||||
#ifndef ULONG_LONG_MAX
|
||||
# define ULONG_LONG_MAX UINT64_C (18446744073709551615)
|
||||
#endif
|
||||
|
||||
#if !defined (INT64_MAX) && defined (INT64_C)
|
||||
# define INT64_MAX INT64_C (9223372036854775807)
|
||||
#endif
|
||||
#if !defined (INT64_MIN) && defined (INT64_C)
|
||||
# define INT64_MIN INT64_C (-9223372036854775808)
|
||||
#endif
|
||||
#if !defined (UINT64_MAX) && defined (INT64_C)
|
||||
# define UINT64_MAX UINT64_C (18446744073709551615)
|
||||
#endif
|
||||
|
||||
/*
|
||||
* Width of hexadecimal for number field.
|
||||
*/
|
||||
|
||||
#ifndef PRINTF_INT64_HEX_WIDTH
|
||||
# define PRINTF_INT64_HEX_WIDTH "16"
|
||||
#endif
|
||||
#ifndef PRINTF_INT32_HEX_WIDTH
|
||||
# define PRINTF_INT32_HEX_WIDTH "8"
|
||||
#endif
|
||||
#ifndef PRINTF_INT16_HEX_WIDTH
|
||||
# define PRINTF_INT16_HEX_WIDTH "4"
|
||||
#endif
|
||||
#ifndef PRINTF_INT8_HEX_WIDTH
|
||||
# define PRINTF_INT8_HEX_WIDTH "2"
|
||||
#endif
|
||||
#ifndef PRINTF_INT64_DEC_WIDTH
|
||||
# define PRINTF_INT64_DEC_WIDTH "19"
|
||||
#endif
|
||||
#ifndef PRINTF_INT32_DEC_WIDTH
|
||||
# define PRINTF_INT32_DEC_WIDTH "10"
|
||||
#endif
|
||||
#ifndef PRINTF_INT16_DEC_WIDTH
|
||||
# define PRINTF_INT16_DEC_WIDTH "5"
|
||||
#endif
|
||||
#ifndef PRINTF_INT8_DEC_WIDTH
|
||||
# define PRINTF_INT8_DEC_WIDTH "3"
|
||||
#endif
|
||||
#ifndef PRINTF_UINT64_DEC_WIDTH
|
||||
# define PRINTF_UINT64_DEC_WIDTH "20"
|
||||
#endif
|
||||
#ifndef PRINTF_UINT32_DEC_WIDTH
|
||||
# define PRINTF_UINT32_DEC_WIDTH "10"
|
||||
#endif
|
||||
#ifndef PRINTF_UINT16_DEC_WIDTH
|
||||
# define PRINTF_UINT16_DEC_WIDTH "5"
|
||||
#endif
|
||||
#ifndef PRINTF_UINT8_DEC_WIDTH
|
||||
# define PRINTF_UINT8_DEC_WIDTH "3"
|
||||
#endif
|
||||
|
||||
/*
|
||||
* Ok, lets not worry about 128 bit integers for now. Moore's law says
|
||||
* we don't need to worry about that until about 2040 at which point
|
||||
* we'll have bigger things to worry about.
|
||||
*/
|
||||
|
||||
#ifdef stdint_int64_defined
|
||||
typedef int64_t intmax_t;
|
||||
typedef uint64_t uintmax_t;
|
||||
# define INTMAX_MAX INT64_MAX
|
||||
# define INTMAX_MIN INT64_MIN
|
||||
# define UINTMAX_MAX UINT64_MAX
|
||||
# define UINTMAX_C(v) UINT64_C(v)
|
||||
# define INTMAX_C(v) INT64_C(v)
|
||||
# ifndef PRINTF_INTMAX_MODIFIER
|
||||
# define PRINTF_INTMAX_MODIFIER PRINTF_INT64_MODIFIER
|
||||
# endif
|
||||
# ifndef PRINTF_INTMAX_HEX_WIDTH
|
||||
# define PRINTF_INTMAX_HEX_WIDTH PRINTF_INT64_HEX_WIDTH
|
||||
# endif
|
||||
# ifndef PRINTF_INTMAX_DEC_WIDTH
|
||||
# define PRINTF_INTMAX_DEC_WIDTH PRINTF_INT64_DEC_WIDTH
|
||||
# endif
|
||||
#else
|
||||
typedef int32_t intmax_t;
|
||||
typedef uint32_t uintmax_t;
|
||||
# define INTMAX_MAX INT32_MAX
|
||||
# define UINTMAX_MAX UINT32_MAX
|
||||
# define UINTMAX_C(v) UINT32_C(v)
|
||||
# define INTMAX_C(v) INT32_C(v)
|
||||
# ifndef PRINTF_INTMAX_MODIFIER
|
||||
# define PRINTF_INTMAX_MODIFIER PRINTF_INT32_MODIFIER
|
||||
# endif
|
||||
# ifndef PRINTF_INTMAX_HEX_WIDTH
|
||||
# define PRINTF_INTMAX_HEX_WIDTH PRINTF_INT32_HEX_WIDTH
|
||||
# endif
|
||||
# ifndef PRINTF_INTMAX_DEC_WIDTH
|
||||
# define PRINTF_INTMAX_DEC_WIDTH PRINTF_INT32_DEC_WIDTH
|
||||
# endif
|
||||
#endif
|
||||
|
||||
/*
|
||||
* Because this file currently only supports platforms which have
|
||||
* precise powers of 2 as bit sizes for the default integers, the
|
||||
* least definitions are all trivial. Its possible that a future
|
||||
* version of this file could have different definitions.
|
||||
*/
|
||||
|
||||
#ifndef stdint_least_defined
|
||||
typedef int8_t int_least8_t;
|
||||
typedef uint8_t uint_least8_t;
|
||||
typedef int16_t int_least16_t;
|
||||
typedef uint16_t uint_least16_t;
|
||||
typedef int32_t int_least32_t;
|
||||
typedef uint32_t uint_least32_t;
|
||||
# define PRINTF_LEAST32_MODIFIER PRINTF_INT32_MODIFIER
|
||||
# define PRINTF_LEAST16_MODIFIER PRINTF_INT16_MODIFIER
|
||||
# define UINT_LEAST8_MAX UINT8_MAX
|
||||
# define INT_LEAST8_MAX INT8_MAX
|
||||
# define UINT_LEAST16_MAX UINT16_MAX
|
||||
# define INT_LEAST16_MAX INT16_MAX
|
||||
# define UINT_LEAST32_MAX UINT32_MAX
|
||||
# define INT_LEAST32_MAX INT32_MAX
|
||||
# define INT_LEAST8_MIN INT8_MIN
|
||||
# define INT_LEAST16_MIN INT16_MIN
|
||||
# define INT_LEAST32_MIN INT32_MIN
|
||||
# ifdef stdint_int64_defined
|
||||
typedef int64_t int_least64_t;
|
||||
typedef uint64_t uint_least64_t;
|
||||
# define PRINTF_LEAST64_MODIFIER PRINTF_INT64_MODIFIER
|
||||
# define UINT_LEAST64_MAX UINT64_MAX
|
||||
# define INT_LEAST64_MAX INT64_MAX
|
||||
# define INT_LEAST64_MIN INT64_MIN
|
||||
# endif
|
||||
#endif
|
||||
#undef stdint_least_defined
|
||||
|
||||
/*
|
||||
* The ANSI C committee has defined *int*_fast*_t types as well. This,
|
||||
* of course, defies rationality -- you can't know what will be fast
|
||||
* just from the type itself. Even for a given architecture, compatible
|
||||
* implementations might have different performance characteristics.
|
||||
* Developers are warned to stay away from these types when using this
|
||||
* or any other stdint.h.
|
||||
*/
|
||||
|
||||
typedef int_least8_t int_fast8_t;
|
||||
typedef uint_least8_t uint_fast8_t;
|
||||
typedef int_least16_t int_fast16_t;
|
||||
typedef uint_least16_t uint_fast16_t;
|
||||
typedef int_least32_t int_fast32_t;
|
||||
typedef uint_least32_t uint_fast32_t;
|
||||
#define UINT_FAST8_MAX UINT_LEAST8_MAX
|
||||
#define INT_FAST8_MAX INT_LEAST8_MAX
|
||||
#define UINT_FAST16_MAX UINT_LEAST16_MAX
|
||||
#define INT_FAST16_MAX INT_LEAST16_MAX
|
||||
#define UINT_FAST32_MAX UINT_LEAST32_MAX
|
||||
#define INT_FAST32_MAX INT_LEAST32_MAX
|
||||
#define INT_FAST8_MIN INT_LEAST8_MIN
|
||||
#define INT_FAST16_MIN INT_LEAST16_MIN
|
||||
#define INT_FAST32_MIN INT_LEAST32_MIN
|
||||
#ifdef stdint_int64_defined
|
||||
typedef int_least64_t int_fast64_t;
|
||||
typedef uint_least64_t uint_fast64_t;
|
||||
# define UINT_FAST64_MAX UINT_LEAST64_MAX
|
||||
# define INT_FAST64_MAX INT_LEAST64_MAX
|
||||
# define INT_FAST64_MIN INT_LEAST64_MIN
|
||||
#endif
|
||||
|
||||
#undef stdint_int64_defined
|
||||
|
||||
/*
|
||||
* Whatever piecemeal, per compiler thing we can do about the wchar_t
|
||||
* type limits.
|
||||
*/
|
||||
|
||||
#if defined(__WATCOMC__) || defined(_MSC_VER) || defined (__GNUC__) && !defined(vxWorks)
|
||||
# include <wchar.h>
|
||||
# ifndef WCHAR_MIN
|
||||
# define WCHAR_MIN 0
|
||||
# endif
|
||||
# ifndef WCHAR_MAX
|
||||
# define WCHAR_MAX ((wchar_t)-1)
|
||||
# endif
|
||||
#endif
|
||||
|
||||
/*
|
||||
* Whatever piecemeal, per compiler/platform thing we can do about the
|
||||
* (u)intptr_t types and limits.
|
||||
*/
|
||||
|
||||
#if (defined (_MSC_VER) && defined (_UINTPTR_T_DEFINED)) || defined (_UINTPTR_T)
|
||||
# define STDINT_H_UINTPTR_T_DEFINED
|
||||
#endif
|
||||
|
||||
#ifndef STDINT_H_UINTPTR_T_DEFINED
|
||||
# if defined (__alpha__) || defined (__ia64__) || defined (__x86_64__) || defined (_WIN64) || defined (__ppc64__)
|
||||
# define stdint_intptr_bits 64
|
||||
# elif defined (__WATCOMC__) || defined (__TURBOC__)
|
||||
# if defined(__TINY__) || defined(__SMALL__) || defined(__MEDIUM__)
|
||||
# define stdint_intptr_bits 16
|
||||
# else
|
||||
# define stdint_intptr_bits 32
|
||||
# endif
|
||||
# elif defined (__i386__) || defined (_WIN32) || defined (WIN32) || defined (__ppc64__)
|
||||
# define stdint_intptr_bits 32
|
||||
# elif defined (__INTEL_COMPILER)
|
||||
/* TODO -- what did Intel do about x86-64? */
|
||||
# else
|
||||
/* #error "This platform might not be supported yet" */
|
||||
# endif
|
||||
|
||||
# ifdef stdint_intptr_bits
|
||||
# define stdint_intptr_glue3_i(a,b,c) a##b##c
|
||||
# define stdint_intptr_glue3(a,b,c) stdint_intptr_glue3_i(a,b,c)
|
||||
# ifndef PRINTF_INTPTR_MODIFIER
|
||||
# define PRINTF_INTPTR_MODIFIER stdint_intptr_glue3(PRINTF_INT,stdint_intptr_bits,_MODIFIER)
|
||||
# endif
|
||||
# ifndef PTRDIFF_MAX
|
||||
# define PTRDIFF_MAX stdint_intptr_glue3(INT,stdint_intptr_bits,_MAX)
|
||||
# endif
|
||||
# ifndef PTRDIFF_MIN
|
||||
# define PTRDIFF_MIN stdint_intptr_glue3(INT,stdint_intptr_bits,_MIN)
|
||||
# endif
|
||||
# ifndef UINTPTR_MAX
|
||||
# define UINTPTR_MAX stdint_intptr_glue3(UINT,stdint_intptr_bits,_MAX)
|
||||
# endif
|
||||
# ifndef INTPTR_MAX
|
||||
# define INTPTR_MAX stdint_intptr_glue3(INT,stdint_intptr_bits,_MAX)
|
||||
# endif
|
||||
# ifndef INTPTR_MIN
|
||||
# define INTPTR_MIN stdint_intptr_glue3(INT,stdint_intptr_bits,_MIN)
|
||||
# endif
|
||||
# ifndef INTPTR_C
|
||||
# define INTPTR_C(x) stdint_intptr_glue3(INT,stdint_intptr_bits,_C)(x)
|
||||
# endif
|
||||
# ifndef UINTPTR_C
|
||||
# define UINTPTR_C(x) stdint_intptr_glue3(UINT,stdint_intptr_bits,_C)(x)
|
||||
# endif
|
||||
typedef stdint_intptr_glue3(uint,stdint_intptr_bits,_t) uintptr_t;
|
||||
typedef stdint_intptr_glue3( int,stdint_intptr_bits,_t) intptr_t;
|
||||
# else
|
||||
/* TODO -- This following is likely wrong for some platforms, and does
|
||||
nothing for the definition of uintptr_t. */
|
||||
typedef ptrdiff_t intptr_t;
|
||||
# endif
|
||||
# define STDINT_H_UINTPTR_T_DEFINED
|
||||
#endif
|
||||
|
||||
/*
|
||||
* Assumes sig_atomic_t is signed and we have a 2s complement machine.
|
||||
*/
|
||||
|
||||
#ifndef SIG_ATOMIC_MAX
|
||||
# define SIG_ATOMIC_MAX ((((sig_atomic_t) 1) << (sizeof (sig_atomic_t)*CHAR_BIT-1)) - 1)
|
||||
#endif
|
||||
|
||||
#endif
|
||||
|
||||
#if defined (__TEST_PSTDINT_FOR_CORRECTNESS)
|
||||
|
||||
/*
|
||||
* Please compile with the maximum warning settings to make sure macros are
|
||||
* not defined more than once.
|
||||
*/
|
||||
|
||||
#include <stdlib.h>
|
||||
#include <stdio.h>
|
||||
#include <string.h>
|
||||
|
||||
#define glue3_aux(x,y,z) x ## y ## z
|
||||
#define glue3(x,y,z) glue3_aux(x,y,z)
|
||||
|
||||
#define DECLU(bits) glue3(uint,bits,_t) glue3(u,bits,) = glue3(UINT,bits,_C) (0);
|
||||
#define DECLI(bits) glue3(int,bits,_t) glue3(i,bits,) = glue3(INT,bits,_C) (0);
|
||||
|
||||
#define DECL(us,bits) glue3(DECL,us,) (bits)
|
||||
|
||||
#define TESTUMAX(bits) glue3(u,bits,) = ~glue3(u,bits,); if (glue3(UINT,bits,_MAX) != glue3(u,bits,)) printf ("Something wrong with UINT%d_MAX\n", bits)
|
||||
|
||||
#define REPORTERROR(msg) { err_n++; if (err_first <= 0) err_first = __LINE__; printf msg; }
|
||||
|
||||
#define X_SIZE_MAX ((size_t)-1)
|
||||
|
||||
int main () {
|
||||
int err_n = 0;
|
||||
int err_first = 0;
|
||||
DECL(I,8)
|
||||
DECL(U,8)
|
||||
DECL(I,16)
|
||||
DECL(U,16)
|
||||
DECL(I,32)
|
||||
DECL(U,32)
|
||||
#ifdef INT64_MAX
|
||||
DECL(I,64)
|
||||
DECL(U,64)
|
||||
#endif
|
||||
intmax_t imax = INTMAX_C(0);
|
||||
uintmax_t umax = UINTMAX_C(0);
|
||||
char str0[256], str1[256];
|
||||
|
||||
sprintf (str0, "%" PRINTF_INT32_MODIFIER "d", INT32_C(2147483647));
|
||||
if (0 != strcmp (str0, "2147483647")) REPORTERROR (("Something wrong with PRINTF_INT32_MODIFIER : %s\n", str0));
|
||||
if (atoi(PRINTF_INT32_DEC_WIDTH) != (int) strlen(str0)) REPORTERROR (("Something wrong with PRINTF_INT32_DEC_WIDTH : %s\n", PRINTF_INT32_DEC_WIDTH));
|
||||
sprintf (str0, "%" PRINTF_INT32_MODIFIER "u", UINT32_C(4294967295));
|
||||
if (0 != strcmp (str0, "4294967295")) REPORTERROR (("Something wrong with PRINTF_INT32_MODIFIER : %s\n", str0));
|
||||
if (atoi(PRINTF_UINT32_DEC_WIDTH) != (int) strlen(str0)) REPORTERROR (("Something wrong with PRINTF_UINT32_DEC_WIDTH : %s\n", PRINTF_UINT32_DEC_WIDTH));
|
||||
#ifdef INT64_MAX
|
||||
sprintf (str1, "%" PRINTF_INT64_MODIFIER "d", INT64_C(9223372036854775807));
|
||||
if (0 != strcmp (str1, "9223372036854775807")) REPORTERROR (("Something wrong with PRINTF_INT32_MODIFIER : %s\n", str1));
|
||||
if (atoi(PRINTF_INT64_DEC_WIDTH) != (int) strlen(str1)) REPORTERROR (("Something wrong with PRINTF_INT64_DEC_WIDTH : %s, %d\n", PRINTF_INT64_DEC_WIDTH, (int) strlen(str1)));
|
||||
sprintf (str1, "%" PRINTF_INT64_MODIFIER "u", UINT64_C(18446744073709550591));
|
||||
if (0 != strcmp (str1, "18446744073709550591")) REPORTERROR (("Something wrong with PRINTF_INT32_MODIFIER : %s\n", str1));
|
||||
if (atoi(PRINTF_UINT64_DEC_WIDTH) != (int) strlen(str1)) REPORTERROR (("Something wrong with PRINTF_UINT64_DEC_WIDTH : %s, %d\n", PRINTF_UINT64_DEC_WIDTH, (int) strlen(str1)));
|
||||
#endif
|
||||
|
||||
sprintf (str0, "%d %x\n", 0, ~0);
|
||||
|
||||
sprintf (str1, "%d %x\n", i8, ~0);
|
||||
if (0 != strcmp (str0, str1)) REPORTERROR (("Something wrong with i8 : %s\n", str1));
|
||||
sprintf (str1, "%u %x\n", u8, ~0);
|
||||
if (0 != strcmp (str0, str1)) REPORTERROR (("Something wrong with u8 : %s\n", str1));
|
||||
sprintf (str1, "%d %x\n", i16, ~0);
|
||||
if (0 != strcmp (str0, str1)) REPORTERROR (("Something wrong with i16 : %s\n", str1));
|
||||
sprintf (str1, "%u %x\n", u16, ~0);
|
||||
if (0 != strcmp (str0, str1)) REPORTERROR (("Something wrong with u16 : %s\n", str1));
|
||||
sprintf (str1, "%" PRINTF_INT32_MODIFIER "d %x\n", i32, ~0);
|
||||
if (0 != strcmp (str0, str1)) REPORTERROR (("Something wrong with i32 : %s\n", str1));
|
||||
sprintf (str1, "%" PRINTF_INT32_MODIFIER "u %x\n", u32, ~0);
|
||||
if (0 != strcmp (str0, str1)) REPORTERROR (("Something wrong with u32 : %s\n", str1));
|
||||
#ifdef INT64_MAX
|
||||
sprintf (str1, "%" PRINTF_INT64_MODIFIER "d %x\n", i64, ~0);
|
||||
if (0 != strcmp (str0, str1)) REPORTERROR (("Something wrong with i64 : %s\n", str1));
|
||||
#endif
|
||||
sprintf (str1, "%" PRINTF_INTMAX_MODIFIER "d %x\n", imax, ~0);
|
||||
if (0 != strcmp (str0, str1)) REPORTERROR (("Something wrong with imax : %s\n", str1));
|
||||
sprintf (str1, "%" PRINTF_INTMAX_MODIFIER "u %x\n", umax, ~0);
|
||||
if (0 != strcmp (str0, str1)) REPORTERROR (("Something wrong with umax : %s\n", str1));
|
||||
|
||||
TESTUMAX(8);
|
||||
TESTUMAX(16);
|
||||
TESTUMAX(32);
|
||||
#ifdef INT64_MAX
|
||||
TESTUMAX(64);
|
||||
#endif
|
||||
|
||||
#define STR(v) #v
|
||||
#define Q(v) printf ("sizeof " STR(v) " = %u\n", (unsigned) sizeof (v));
|
||||
if (err_n) {
|
||||
printf ("pstdint.h is not correct. Please use sizes below to correct it:\n");
|
||||
}
|
||||
|
||||
Q(int)
|
||||
Q(unsigned)
|
||||
Q(long int)
|
||||
Q(short int)
|
||||
Q(int8_t)
|
||||
Q(int16_t)
|
||||
Q(int32_t)
|
||||
#ifdef INT64_MAX
|
||||
Q(int64_t)
|
||||
#endif
|
||||
|
||||
#if UINT_MAX < X_SIZE_MAX
|
||||
printf ("UINT_MAX < X_SIZE_MAX\n");
|
||||
#else
|
||||
printf ("UINT_MAX >= X_SIZE_MAX\n");
|
||||
#endif
|
||||
printf ("%" PRINTF_INT64_MODIFIER "u vs %" PRINTF_INT64_MODIFIER "u\n", UINT_MAX, X_SIZE_MAX);
|
||||
|
||||
return EXIT_SUCCESS;
|
||||
}
|
||||
|
||||
#endif
|
||||
File diff suppressed because it is too large
Load Diff
Loading…
Reference in New Issue