Skip to content

A
abc
Commit b3d3f7dd by Alan Mishchenko
Options

Duplicating Glucose package.

parent 890aa684
Showing with 8262 additions and 34 deletions
Makefile
......@@ -27,7 +27,7 @@ MODULES := \
src/opt/cut src/opt/fxu src/opt/fxch src/opt/rwr src/opt/mfs src/opt/sim \
src/opt/ret src/opt/fret src/opt/res src/opt/lpk src/opt/nwk src/opt/rwt \
src/opt/cgt src/opt/csw src/opt/dar src/opt/dau src/opt/dsc src/opt/sfm src/opt/sbd \
src/sat/bsat src/sat/xsat src/sat/satoko src/sat/csat src/sat/msat src/sat/psat src/sat/cnf src/sat/bmc src/sat/glucose \
src/sat/bsat src/sat/xsat src/sat/satoko src/sat/csat src/sat/msat src/sat/psat src/sat/cnf src/sat/bmc src/sat/glucose src/sat/glucose2 \
src/bool/bdc src/bool/deco src/bool/dec src/bool/kit src/bool/lucky \
src/bool/rsb src/bool/rpo \
src/proof/pdr src/proof/abs src/proof/live src/proof/ssc src/proof/int \
......
abclib.dsp
......@@ -2366,6 +2366,114 @@ SOURCE=.\src\sat\glucose\Vec.h
SOURCE=.\src\sat\glucose\XAlloc.h
# End Source File
# End Group
# Begin Group "glucose2"
# PROP Default_Filter ""
# Begin Source File
SOURCE=.\src\sat\glucose2\AbcGlucose2.cpp
# End Source File
# Begin Source File
SOURCE=.\src\sat\glucose2\AbcGlucose2.h
# End Source File
# Begin Source File
SOURCE=.\src\sat\glucose2\AbcGlucoseCmd2.cpp
# End Source File
# Begin Source File
SOURCE=.\src\sat\glucose2\Alg.h
# End Source File
# Begin Source File
SOURCE=.\src\sat\glucose2\Alloc.h
# End Source File
# Begin Source File
SOURCE=.\src\sat\glucose2\BoundedQueue.h
# End Source File
# Begin Source File
SOURCE=.\src\sat\glucose2\Constants.h
# End Source File
# Begin Source File
SOURCE=.\src\sat\glucose2\Dimacs.h
# End Source File
# Begin Source File
SOURCE=.\src\sat\glucose2\Glucose2.cpp
# End Source File
# Begin Source File
SOURCE=.\src\sat\glucose2\Heap.h
# End Source File
# Begin Source File
SOURCE=.\src\sat\glucose2\IntTypes.h
# End Source File
# Begin Source File
SOURCE=.\src\sat\glucose2\Map.h
# End Source File
# Begin Source File
SOURCE=.\src\sat\glucose2\Options.h
# End Source File
# Begin Source File
SOURCE=.\src\sat\glucose2\Options2.cpp
# End Source File
# Begin Source File
SOURCE=.\src\sat\glucose2\ParseUtils.h
# End Source File
# Begin Source File
SOURCE=.\src\sat\glucose2\pstdint.h
# End Source File
# Begin Source File
SOURCE=.\src\sat\glucose2\Queue.h
# End Source File
# Begin Source File
SOURCE=.\src\sat\glucose2\SimpSolver.h
# End Source File
# Begin Source File
SOURCE=.\src\sat\glucose2\SimpSolver2.cpp
# End Source File
# Begin Source File
SOURCE=.\src\sat\glucose2\Solver.h
# End Source File
# Begin Source File
SOURCE=.\src\sat\glucose2\SolverTypes.h
# End Source File
# Begin Source File
SOURCE=.\src\sat\glucose2\Sort.h
# End Source File
# Begin Source File
SOURCE=.\src\sat\glucose2\System.h
# End Source File
# Begin Source File
SOURCE=.\src\sat\glucose2\System2.cpp
# End Source File
# Begin Source File
SOURCE=.\src\sat\glucose2\Vec.h
# End Source File
# Begin Source File
SOURCE=.\src\sat\glucose2\XAlloc.h
# End Source File
# End Group
# End Group
# Begin Group "opt"
......
src/base/main/mainInit.c
......@@ -65,6 +65,8 @@ 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 );
extern void Glucose2_Init( Abc_Frame_t *pAbc );
extern void Glucose2_End( Abc_Frame_t * pAbc );
static Abc_FrameInitializer_t* s_InitializerStart = NULL;
static Abc_FrameInitializer_t* s_InitializerEnd = NULL;
......@@ -120,6 +122,7 @@ void Abc_FrameInit( Abc_Frame_t * pAbc )
Sim_Init( pAbc );
Test_Init( pAbc );
Glucose_Init( pAbc );
Glucose2_Init( pAbc );
for( p = s_InitializerStart ; p ; p = p->next )
if(p->init)
p->init(pAbc);
......
src/proof/cec/cecSatG2.c
......@@ -20,11 +20,47 @@
#include "aig/gia/gia.h"
#include "misc/util/utilTruth.h"
#include "sat/glucose/AbcGlucose.h"
#include "cec.h"
#define USE_GLUCOSE2
#ifdef USE_GLUCOSE2
#include "sat/glucose2/AbcGlucose2.h"
#define sat_solver bmcg2_sat_solver
#define sat_solver_start bmcg2_sat_solver_start
#define sat_solver_stop bmcg2_sat_solver_stop
#define sat_solver_addclause bmcg2_sat_solver_addclause
#define sat_solver_addvar bmcg2_sat_solver_addvar
#define sat_solver_read_cex_varvalue bmcg2_sat_solver_read_cex_varvalue
#define sat_solver_reset bmcg2_sat_solver_reset
#define sat_solver_set_conflict_budget bmcg2_sat_solver_set_conflict_budget
#define sat_solver_conflictnum bmcg2_sat_solver_conflictnum
#define sat_solver_solve bmcg2_sat_solver_solve
#define sat_solver_read_cex_varvalue bmcg2_sat_solver_read_cex_varvalue
#else
#include "sat/glucose/AbcGlucose.h"
#define sat_solver bmcg_sat_solver
#define sat_solver_start bmcg_sat_solver_start
#define sat_solver_stop bmcg_sat_solver_stop
#define sat_solver_addclause bmcg_sat_solver_addclause
#define sat_solver_addvar bmcg_sat_solver_addvar
#define sat_solver_read_cex_varvalue bmcg_sat_solver_read_cex_varvalue
#define sat_solver_reset bmcg_sat_solver_reset
#define sat_solver_set_conflict_budget bmcg_sat_solver_set_conflict_budget
#define sat_solver_conflictnum bmcg_sat_solver_conflictnum
#define sat_solver_solve bmcg_sat_solver_solve
#define sat_solver_read_cex_varvalue bmcg_sat_solver_read_cex_varvalue
#endif
ABC_NAMESPACE_IMPL_START
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
......@@ -37,7 +73,7 @@ struct Cec4_Man_t_
Gia_Man_t * pAig; // user's AIG
Gia_Man_t * pNew; // internal AIG
// SAT solving
bmcg_sat_solver* pSat; // SAT solver
sat_solver * pSat; // SAT solver
Vec_Ptr_t * vFrontier; // CNF construction
Vec_Ptr_t * vFanins; // CNF construction
Vec_Wrd_t * vSims; // CI simulation info
......@@ -98,7 +134,7 @@ Cec4_Man_t * Cec4_ManCreate( Gia_Man_t * pAig, Cec_ParFra_t * pPars )
p->timeStart = Abc_Clock();
p->pPars = pPars;
p->pAig = pAig;
p->pSat = bmcg_sat_solver_start();
p->pSat = sat_solver_start();
p->vFrontier = Vec_PtrAlloc( 1000 );
p->vFanins = Vec_PtrAlloc( 100 );
p->vCexMin = Vec_IntAlloc( 100 );
......@@ -135,7 +171,7 @@ void Cec4_ManDestroy( Cec4_Man_t * p )
}
Vec_WrdFreeP( &p->pAig->vSims );
Gia_ManCleanMark01( p->pAig );
bmcg_sat_solver_stop( p->pSat );
sat_solver_stop( p->pSat );
Gia_ManStopP( &p->pNew );
Vec_PtrFreeP( &p->vFrontier );
Vec_PtrFreeP( &p->vFanins );
......@@ -174,7 +210,7 @@ Gia_Man_t * Cec4_ManStartNew( Gia_Man_t * pAig )
SeeAlso []
***********************************************************************/
void Cec4_AddClausesMux( Gia_Man_t * p, Gia_Obj_t * pNode, bmcg_sat_solver * pSat )
void Cec4_AddClausesMux( Gia_Man_t * p, Gia_Obj_t * pNode, sat_solver * pSat )
{
int fPolarFlip = 0;
Gia_Obj_t * pNodeI, * pNodeT, * pNodeE;
......@@ -210,7 +246,7 @@ void Cec4_AddClausesMux( Gia_Man_t * p, Gia_Obj_t * pNode, bmcg_sat_solver * pSa
if ( Gia_Regular(pNodeT)->fPhase ) pLits[1] = Abc_LitNot( pLits[1] );
if ( pNode->fPhase ) pLits[2] = Abc_LitNot( pLits[2] );
}
RetValue = bmcg_sat_solver_addclause( pSat, pLits, 3 );
RetValue = sat_solver_addclause( pSat, pLits, 3 );
assert( RetValue );
pLits[0] = Abc_Var2Lit(VarI, 1);
pLits[1] = Abc_Var2Lit(VarT, 0^fCompT);
......@@ -221,7 +257,7 @@ void Cec4_AddClausesMux( Gia_Man_t * p, Gia_Obj_t * pNode, bmcg_sat_solver * pSa
if ( Gia_Regular(pNodeT)->fPhase ) pLits[1] = Abc_LitNot( pLits[1] );
if ( pNode->fPhase ) pLits[2] = Abc_LitNot( pLits[2] );
}
RetValue = bmcg_sat_solver_addclause( pSat, pLits, 3 );
RetValue = sat_solver_addclause( pSat, pLits, 3 );
assert( RetValue );
pLits[0] = Abc_Var2Lit(VarI, 0);
pLits[1] = Abc_Var2Lit(VarE, 1^fCompE);
......@@ -232,7 +268,7 @@ void Cec4_AddClausesMux( Gia_Man_t * p, Gia_Obj_t * pNode, bmcg_sat_solver * pSa
if ( Gia_Regular(pNodeE)->fPhase ) pLits[1] = Abc_LitNot( pLits[1] );
if ( pNode->fPhase ) pLits[2] = Abc_LitNot( pLits[2] );
}
RetValue = bmcg_sat_solver_addclause( pSat, pLits, 3 );
RetValue = sat_solver_addclause( pSat, pLits, 3 );
assert( RetValue );
pLits[0] = Abc_Var2Lit(VarI, 0);
pLits[1] = Abc_Var2Lit(VarE, 0^fCompE);
......@@ -243,7 +279,7 @@ void Cec4_AddClausesMux( Gia_Man_t * p, Gia_Obj_t * pNode, bmcg_sat_solver * pSa
if ( Gia_Regular(pNodeE)->fPhase ) pLits[1] = Abc_LitNot( pLits[1] );
if ( pNode->fPhase ) pLits[2] = Abc_LitNot( pLits[2] );
}
RetValue = bmcg_sat_solver_addclause( pSat, pLits, 3 );
RetValue = sat_solver_addclause( pSat, pLits, 3 );
assert( RetValue );
// two additional clauses
......@@ -268,7 +304,7 @@ void Cec4_AddClausesMux( Gia_Man_t * p, Gia_Obj_t * pNode, bmcg_sat_solver * pSa
if ( Gia_Regular(pNodeE)->fPhase ) pLits[1] = Abc_LitNot( pLits[1] );
if ( pNode->fPhase ) pLits[2] = Abc_LitNot( pLits[2] );
}
RetValue = bmcg_sat_solver_addclause( pSat, pLits, 3 );
RetValue = sat_solver_addclause( pSat, pLits, 3 );
assert( RetValue );
pLits[0] = Abc_Var2Lit(VarT, 1^fCompT);
pLits[1] = Abc_Var2Lit(VarE, 1^fCompE);
......@@ -279,10 +315,10 @@ void Cec4_AddClausesMux( Gia_Man_t * p, Gia_Obj_t * pNode, bmcg_sat_solver * pSa
if ( Gia_Regular(pNodeE)->fPhase ) pLits[1] = Abc_LitNot( pLits[1] );
if ( pNode->fPhase ) pLits[2] = Abc_LitNot( pLits[2] );
}
RetValue = bmcg_sat_solver_addclause( pSat, pLits, 3 );
RetValue = sat_solver_addclause( pSat, pLits, 3 );
assert( RetValue );
}
void Cec4_AddClausesSuper( Gia_Man_t * p, Gia_Obj_t * pNode, Vec_Ptr_t * vSuper, bmcg_sat_solver * pSat )
void Cec4_AddClausesSuper( Gia_Man_t * p, Gia_Obj_t * pNode, Vec_Ptr_t * vSuper, sat_solver * pSat )
{
int fPolarFlip = 0;
Gia_Obj_t * pFanin;
......@@ -303,7 +339,7 @@ void Cec4_AddClausesSuper( Gia_Man_t * p, Gia_Obj_t * pNode, Vec_Ptr_t * vSuper,
if ( Gia_Regular(pFanin)->fPhase ) pLits[0] = Abc_LitNot( pLits[0] );
if ( pNode->fPhase ) pLits[1] = Abc_LitNot( pLits[1] );
}
RetValue = bmcg_sat_solver_addclause( pSat, pLits, 2 );
RetValue = sat_solver_addclause( pSat, pLits, 2 );
assert( RetValue );
}
// add A & B => C or !A + !B + C
......@@ -320,7 +356,7 @@ void Cec4_AddClausesSuper( Gia_Man_t * p, Gia_Obj_t * pNode, Vec_Ptr_t * vSuper,
{
if ( pNode->fPhase ) pLits[nLits-1] = Abc_LitNot( pLits[nLits-1] );
}
RetValue = bmcg_sat_solver_addclause( pSat, pLits, nLits );
RetValue = sat_solver_addclause( pSat, pLits, nLits );
assert( RetValue );
ABC_FREE( pLits );
}
......@@ -357,14 +393,14 @@ void Cec4_CollectSuper( Gia_Obj_t * pObj, int fUseMuxes, Vec_Ptr_t * vSuper )
Vec_PtrClear( vSuper );
Cec4_CollectSuper_rec( pObj, vSuper, 1, fUseMuxes );
}
void Cec4_ObjAddToFrontier( Gia_Man_t * p, Gia_Obj_t * pObj, Vec_Ptr_t * vFrontier, bmcg_sat_solver * pSat )
void Cec4_ObjAddToFrontier( Gia_Man_t * p, Gia_Obj_t * pObj, Vec_Ptr_t * vFrontier, sat_solver * pSat )
{
assert( !Gia_IsComplement(pObj) );
assert( !Gia_ObjIsConst0(pObj) );
if ( Cec4_ObjSatId(p, pObj) >= 0 )
return;
assert( Cec4_ObjSatId(p, pObj) == -1 );
Cec4_ObjSetSatId( p, pObj, bmcg_sat_solver_addvar(pSat) );
Cec4_ObjSetSatId( p, pObj, sat_solver_addvar(pSat) );
if ( Gia_ObjIsAnd(pObj) )
Vec_PtrPush( vFrontier, pObj );
}
......@@ -380,7 +416,7 @@ int Cec4_ObjGetCnfVar( Cec4_Man_t * p, int iObj )
return Cec4_ObjSatId(p->pNew,pObj);
assert( iObj > 0 );
if ( Gia_ObjIsCi(pObj) )
return Cec4_ObjSetSatId( p->pNew, pObj, bmcg_sat_solver_addvar(p->pSat) );
return Cec4_ObjSetSatId( p->pNew, pObj, sat_solver_addvar(p->pSat) );
assert( Gia_ObjIsAnd(pObj) );
if ( fUseAnd2 )
{
......@@ -389,7 +425,7 @@ int Cec4_ObjGetCnfVar( Cec4_Man_t * p, int iObj )
Vec_PtrClear( p->vFanins );
Vec_PtrPush( p->vFanins, Gia_ObjChild0(pObj) );
Vec_PtrPush( p->vFanins, Gia_ObjChild1(pObj) );
Cec4_ObjSetSatId( p->pNew, pObj, bmcg_sat_solver_addvar(p->pSat) );
Cec4_ObjSetSatId( p->pNew, pObj, sat_solver_addvar(p->pSat) );
Cec4_AddClausesSuper( p->pNew, pObj, p->vFanins, p->pSat );
return Cec4_ObjSatId( p->pNew, pObj );
}
......@@ -777,7 +813,7 @@ void Cec4_ManCreateClasses( Gia_Man_t * p, Cec4_Man_t * pMan )
SeeAlso []
***********************************************************************/
int Cec4_ManVerify_rec( Gia_Man_t * p, int iObj, bmcg_sat_solver * pSat )
int Cec4_ManVerify_rec( Gia_Man_t * p, int iObj, sat_solver * pSat )
{
int Value0, Value1;
Gia_Obj_t * pObj = Gia_ManObj( p, iObj );
......@@ -786,13 +822,13 @@ int Cec4_ManVerify_rec( Gia_Man_t * p, int iObj, bmcg_sat_solver * pSat )
return pObj->fMark1;
Gia_ObjSetTravIdCurrentId(p, iObj);
if ( Gia_ObjIsCi(pObj) )
return pObj->fMark1 = bmcg_sat_solver_read_cex_varvalue(pSat, Cec4_ObjSatId(p, pObj));
return pObj->fMark1 = sat_solver_read_cex_varvalue(pSat, Cec4_ObjSatId(p, pObj));
assert( Gia_ObjIsAnd(pObj) );
Value0 = Cec4_ManVerify_rec( p, Gia_ObjFaninId0(pObj, iObj), pSat ) ^ Gia_ObjFaninC0(pObj);
Value1 = Cec4_ManVerify_rec( p, Gia_ObjFaninId1(pObj, iObj), pSat ) ^ Gia_ObjFaninC1(pObj);
return pObj->fMark1 = Value0 & Value1;
}
void Cec4_ManVerify( Gia_Man_t * p, int iObj0, int iObj1, int fPhase, bmcg_sat_solver * pSat )
void Cec4_ManVerify( Gia_Man_t * p, int iObj0, int iObj1, int fPhase, sat_solver * pSat )
{
int Value0, Value1;
Gia_ManIncrementTravId( p );
......@@ -997,10 +1033,10 @@ void Cec4_ManSatSolverRecycle( Cec4_Man_t * p )
{
Gia_Obj_t * pObj;
int i;
//printf( "Solver size = %d.\n", bmcg_sat_solver_varnum(p->pSat) );
//printf( "Solver size = %d.\n", sat_solver_varnum(p->pSat) );
p->nRecycles++;
p->nCallsSince = 0;
bmcg_sat_solver_reset( p->pSat );
sat_solver_reset( p->pSat );
// clean mapping of AigIds into SatIds
Gia_ManForEachObjVec( &p->pNew->vSuppVars, p->pNew, pObj, i )
Cec4_ObjCleanSatId( p->pNew, pObj );
......@@ -1024,7 +1060,7 @@ int Cec4_ManSolveTwo( Cec4_Man_t * p, int iObj0, int iObj1, int fPhase, int * pf
Cec4_ManSatSolverRecycle( p );
// add more logic to the solver
if ( !iObj0 && Cec4_ObjSatId(p->pNew, Gia_ManConst0(p->pNew)) == -1 )
Cec4_ObjSetSatId( p->pNew, Gia_ManConst0(p->pNew), bmcg_sat_solver_addvar(p->pSat) );
Cec4_ObjSetSatId( p->pNew, Gia_ManConst0(p->pNew), sat_solver_addvar(p->pSat) );
clk = Abc_Clock();
iVar0 = Cec4_ObjGetCnfVar( p, iObj0 );
iVar1 = Cec4_ObjGetCnfVar( p, iObj1 );
......@@ -1032,10 +1068,10 @@ int Cec4_ManSolveTwo( Cec4_Man_t * p, int iObj0, int iObj1, int fPhase, int * pf
// perform solving
Lits[0] = Abc_Var2Lit(iVar0, 1);
Lits[1] = Abc_Var2Lit(iVar1, fPhase);
bmcg_sat_solver_set_conflict_budget( p->pSat, p->pPars->nBTLimit );
nConfBeg = bmcg_sat_solver_conflictnum( p->pSat );
status = bmcg_sat_solver_solve( p->pSat, Lits, 2 );
nConfEnd = bmcg_sat_solver_conflictnum( p->pSat );
sat_solver_set_conflict_budget( p->pSat, p->pPars->nBTLimit );
nConfBeg = sat_solver_conflictnum( p->pSat );
status = sat_solver_solve( p->pSat, Lits, 2 );
nConfEnd = sat_solver_conflictnum( p->pSat );
assert( nConfEnd >= nConfBeg );
if ( fVerbose )
{
......@@ -1067,10 +1103,10 @@ int Cec4_ManSolveTwo( Cec4_Man_t * p, int iObj0, int iObj1, int fPhase, int * pf
{
Lits[0] = Abc_Var2Lit(iVar0, 0);
Lits[1] = Abc_Var2Lit(iVar1, !fPhase);
bmcg_sat_solver_set_conflict_budget( p->pSat, p->pPars->nBTLimit );
nConfBeg = bmcg_sat_solver_conflictnum( p->pSat );
status = bmcg_sat_solver_solve( p->pSat, Lits, 2 );
nConfEnd = bmcg_sat_solver_conflictnum( p->pSat );
sat_solver_set_conflict_budget( p->pSat, p->pPars->nBTLimit );
nConfBeg = sat_solver_conflictnum( p->pSat );
status = sat_solver_solve( p->pSat, Lits, 2 );
nConfEnd = sat_solver_conflictnum( p->pSat );
assert( nConfEnd >= nConfBeg );
if ( fVerbose )
{
......@@ -1112,7 +1148,7 @@ int Cec4_ManSweepNode( Cec4_Man_t * p, int iObj, int iRepr )
p->pAig->iPatsPi++;
assert( p->pAig->iPatsPi > 0 && p->pAig->iPatsPi < 64 * p->pAig->nSimWords );
Vec_IntForEachEntryDouble( &p->pNew->vCopiesTwo, IdAig, IdSat, i )
Cec4_ObjSimSetInputBit( p->pAig, IdAig, bmcg_sat_solver_read_cex_varvalue(p->pSat, IdSat) );
Cec4_ObjSimSetInputBit( p->pAig, IdAig, sat_solver_read_cex_varvalue(p->pSat, IdSat) );
if ( fEasy )
p->timeSatSat0 += Abc_Clock() - clk;
else
......
src/sat/glucose2/AbcGlucose2.cpp 0 → 100644
/**CFile****************************************************************
FileName [AbcGlucose.cpp]
SystemName [ABC: Logic synthesis and verification system.]
PackageName [SAT solver Glucose 3.0 by Gilles Audemard and Laurent Simon.]
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/glucose2/System.h"
#include "sat/glucose2/ParseUtils.h"
#include "sat/glucose2/Options.h"
#include "sat/glucose2/Dimacs.h"
#include "sat/glucose2/SimpSolver.h"
#include "sat/glucose2/AbcGlucose2.h"
#include "base/abc/abc.h"
#include "aig/gia/gia.h"
#include "sat/cnf/cnf.h"
#include "misc/extra/extra.h"
ABC_NAMESPACE_IMPL_START
using namespace Gluco2;
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
#define USE_SIMP_SOLVER 1
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
#ifdef USE_SIMP_SOLVER
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Gluco2::SimpSolver * glucose_solver_start()
{
SimpSolver * S = new SimpSolver;
S->setIncrementalMode();
return S;
}
void glucose_solver_stop(Gluco2::SimpSolver* S)
{
delete S;
}
void glucose_solver_reset(Gluco2::SimpSolver* S)
{
S->reset();
}
int glucose_solver_addclause(Gluco2::SimpSolver* 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
}
void glucose_solver_setcallback(Gluco2::SimpSolver* S, void * pman, int(*pfunc)(void*, int, int*))
{
S->pCnfMan = pman;
S->pCnfFunc = pfunc;
S->nCallConfl = 1000;
}
int glucose_solver_solve(Gluco2::SimpSolver* S, int * plits, int nlits)
{
vec<Lit> lits;
for (int i=0;i<nlits;i++,plits++)
{
Lit p;
p.x = *plits;
lits.push(p);
}
Gluco2::lbool res = S->solveLimited(lits, 0);
return (res == l_True ? 1 : res == l_False ? -1 : 0);
}
int glucose_solver_addvar(Gluco2::SimpSolver* S)
{
S->newVar();
return S->nVars() - 1;
}
int * glucose_solver_read_cex(Gluco2::SimpSolver* S )
{
return S->getCex();
}
int glucose_solver_read_cex_varvalue(Gluco2::SimpSolver* S, int ivar)
{
return S->model[ivar] == l_True;
}
void glucose_solver_setstop(Gluco2::SimpSolver* S, int * pstop)
{
S->pstop = pstop;
}
/**Function*************************************************************
Synopsis [Wrapper APIs to calling from ABC.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
bmcg2_sat_solver * bmcg2_sat_solver_start()
{
return (bmcg2_sat_solver *)glucose_solver_start();
}
void bmcg2_sat_solver_stop(bmcg2_sat_solver* s)
{
glucose_solver_stop((Gluco2::SimpSolver*)s);
}
void bmcg2_sat_solver_reset(bmcg2_sat_solver* s)
{
glucose_solver_reset((Gluco2::SimpSolver*)s);
}
int bmcg2_sat_solver_addclause(bmcg2_sat_solver* s, int * plits, int nlits)
{
return glucose_solver_addclause((Gluco2::SimpSolver*)s,plits,nlits);
}
void bmcg2_sat_solver_setcallback(bmcg2_sat_solver* s, void * pman, int(*pfunc)(void*, int, int*))
{
glucose_solver_setcallback((Gluco2::SimpSolver*)s,pman,pfunc);
}
int bmcg2_sat_solver_solve(bmcg2_sat_solver* s, int * plits, int nlits)
{
return glucose_solver_solve((Gluco2::SimpSolver*)s,plits,nlits);
}
int bmcg2_sat_solver_final(bmcg2_sat_solver* s, int ** ppArray)
{
*ppArray = (int *)(Lit *)((Gluco2::SimpSolver*)s)->conflict;
return ((Gluco2::SimpSolver*)s)->conflict.size();
}
int bmcg2_sat_solver_addvar(bmcg2_sat_solver* s)
{
return glucose_solver_addvar((Gluco2::SimpSolver*)s);
}
void bmcg2_sat_solver_set_nvars( bmcg2_sat_solver* s, int nvars )
{
int i;
for ( i = bmcg2_sat_solver_varnum(s); i < nvars; i++ )
bmcg2_sat_solver_addvar(s);
}
int bmcg2_sat_solver_eliminate( bmcg2_sat_solver* s, int turn_off_elim )
{
// return 1;
return ((Gluco2::SimpSolver*)s)->eliminate(turn_off_elim != 0);
}
int bmcg2_sat_solver_var_is_elim( bmcg2_sat_solver* s, int v )
{
// return 0;
return ((Gluco2::SimpSolver*)s)->isEliminated(v);
}
void bmcg2_sat_solver_var_set_frozen( bmcg2_sat_solver* s, int v, int freeze )
{
((Gluco2::SimpSolver*)s)->setFrozen(v, freeze != 0);
}
int bmcg2_sat_solver_elim_varnum(bmcg2_sat_solver* s)
{
// return 0;
return ((Gluco2::SimpSolver*)s)->eliminated_vars;
}
int * bmcg2_sat_solver_read_cex(bmcg2_sat_solver* s)
{
return glucose_solver_read_cex((Gluco2::SimpSolver*)s);
}
int bmcg2_sat_solver_read_cex_varvalue(bmcg2_sat_solver* s, int ivar)
{
return glucose_solver_read_cex_varvalue((Gluco2::SimpSolver*)s, ivar);
}
void bmcg2_sat_solver_set_stop(bmcg2_sat_solver* s, int * pstop)
{
glucose_solver_setstop((Gluco2::SimpSolver*)s, pstop);
}
abctime bmcg2_sat_solver_set_runtime_limit(bmcg2_sat_solver* s, abctime Limit)
{
abctime nRuntimeLimit = ((Gluco2::SimpSolver*)s)->nRuntimeLimit;
((Gluco2::SimpSolver*)s)->nRuntimeLimit = Limit;
return nRuntimeLimit;
}
void bmcg2_sat_solver_set_conflict_budget(bmcg2_sat_solver* s, int Limit)
{
if ( Limit > 0 )
((Gluco2::SimpSolver*)s)->setConfBudget( (int64_t)Limit );
else
((Gluco2::SimpSolver*)s)->budgetOff();
}
int bmcg2_sat_solver_varnum(bmcg2_sat_solver* s)
{
return ((Gluco2::SimpSolver*)s)->nVars();
}
int bmcg2_sat_solver_clausenum(bmcg2_sat_solver* s)
{
return ((Gluco2::SimpSolver*)s)->nClauses();
}
int bmcg2_sat_solver_learntnum(bmcg2_sat_solver* s)
{
return ((Gluco2::SimpSolver*)s)->nLearnts();
}
int bmcg2_sat_solver_conflictnum(bmcg2_sat_solver* s)
{
return ((Gluco2::SimpSolver*)s)->conflicts;
}
int bmcg2_sat_solver_minimize_assumptions( bmcg2_sat_solver * s, int * plits, int nlits, int pivot )
{
vec<int>*array = &((Gluco2::SimpSolver*)s)->user_vec;
int i, nlitsL, nlitsR, nresL, nresR, status;
assert( pivot >= 0 );
// assert( nlits - pivot >= 2 );
assert( nlits - pivot >= 1 );
if ( nlits - pivot == 1 )
{
// since the problem is UNSAT, we try to solve it without assuming the last literal
// if the result is UNSAT, the last literal can be dropped; otherwise, it is needed
status = bmcg2_sat_solver_solve( s, plits, pivot );
return status != GLUCOSE_UNSAT; // return 1 if the problem is not UNSAT
}
assert( nlits - pivot >= 2 );
nlitsL = (nlits - pivot) / 2;
nlitsR = (nlits - pivot) - nlitsL;
assert( nlitsL + nlitsR == nlits - pivot );
// solve with these assumptions
status = bmcg2_sat_solver_solve( s, plits, pivot + nlitsL );
if ( status == GLUCOSE_UNSAT ) // these are enough
return bmcg2_sat_solver_minimize_assumptions( s, plits, pivot + nlitsL, pivot );
// these are not enough
// solve for the right lits
// nResL = nLitsR == 1 ? 1 : sat_solver_minimize_assumptions( s, pLits + nLitsL, nLitsR, nConfLimit );
nresL = nlitsR == 1 ? 1 : bmcg2_sat_solver_minimize_assumptions( s, plits, nlits, pivot + nlitsL );
// swap literals
array->clear();
for ( i = 0; i < nlitsL; i++ )
array->push(plits[pivot + i]);
for ( i = 0; i < nresL; i++ )
plits[pivot + i] = plits[pivot + nlitsL + i];
for ( i = 0; i < nlitsL; i++ )
plits[pivot + nresL + i] = (*array)[i];
// solve with these assumptions
status = bmcg2_sat_solver_solve( s, plits, pivot + nresL );
if ( status == GLUCOSE_UNSAT ) // these are enough
return nresL;
// solve for the left lits
// nResR = nLitsL == 1 ? 1 : sat_solver_minimize_assumptions( s, pLits + nResL, nLitsL, nConfLimit );
nresR = nlitsL == 1 ? 1 : bmcg2_sat_solver_minimize_assumptions( s, plits, pivot + nresL + nlitsL, pivot + nresL );
return nresL + nresR;
}
int bmcg2_sat_solver_add_and( bmcg2_sat_solver * s, int iVar, int iVar0, int iVar1, int fCompl0, int fCompl1, int fCompl )
{
int Lits[3];
Lits[0] = Abc_Var2Lit( iVar, !fCompl );
Lits[1] = Abc_Var2Lit( iVar0, fCompl0 );
if ( !bmcg2_sat_solver_addclause( s, Lits, 2 ) )
return 0;
Lits[0] = Abc_Var2Lit( iVar, !fCompl );
Lits[1] = Abc_Var2Lit( iVar1, fCompl1 );
if ( !bmcg2_sat_solver_addclause( s, Lits, 2 ) )
return 0;
Lits[0] = Abc_Var2Lit( iVar, fCompl );
Lits[1] = Abc_Var2Lit( iVar0, !fCompl0 );
Lits[2] = Abc_Var2Lit( iVar1, !fCompl1 );
if ( !bmcg2_sat_solver_addclause( s, Lits, 3 ) )
return 0;
return 1;
}
#else
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Gluco2::Solver * glucose_solver_start()
{
Solver * S = new Solver;
S->setIncrementalMode();
return S;
}
void glucose_solver_stop(Gluco2::Solver* S)
{
delete S;
}
int glucose_solver_addclause(Gluco2::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
}
void glucose_solver_setcallback(Gluco2::Solver* S, void * pman, int(*pfunc)(void*, int, int*))
{
S->pCnfMan = pman;
S->pCnfFunc = pfunc;
S->nCallConfl = 1000;
}
int glucose_solver_solve(Gluco2::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);
}
Gluco2::lbool res = S->solveLimited(lits);
return (res == l_True ? 1 : res == l_False ? -1 : 0);
}
int glucose_solver_addvar(Gluco2::Solver* S)
{
S->newVar();
return S->nVars() - 1;
}
int * glucose_solver_read_cex(Gluco2::Solver* S )
{
return S->getCex();
}
int glucose_solver_read_cex_varvalue(Gluco2::Solver* S, int ivar)
{
return S->model[ivar] == l_True;
}
void glucose_solver_setstop(Gluco2::Solver* S, int * pstop)
{
S->pstop = pstop;
}
/**Function*************************************************************
Synopsis [Wrapper APIs to calling from ABC.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
bmcg2_sat_solver * bmcg2_sat_solver_start()
{
return (bmcg2_sat_solver *)glucose_solver_start();
}
void bmcg2_sat_solver_stop(bmcg2_sat_solver* s)
{
glucose_solver_stop((Gluco2::Solver*)s);
}
int bmcg2_sat_solver_addclause(bmcg2_sat_solver* s, int * plits, int nlits)
{
return glucose_solver_addclause((Gluco2::Solver*)s,plits,nlits);
}
void bmcg2_sat_solver_setcallback(bmcg2_sat_solver* s, void * pman, int(*pfunc)(void*, int, int*))
{
glucose_solver_setcallback((Gluco2::Solver*)s,pman,pfunc);
}
int bmcg2_sat_solver_solve(bmcg2_sat_solver* s, int * plits, int nlits)
{
return glucose_solver_solve((Gluco2::Solver*)s,plits,nlits);
}
int bmcg2_sat_solver_final(bmcg2_sat_solver* s, int ** ppArray)
{
*ppArray = (int *)(Lit *)((Gluco2::Solver*)s)->conflict;
return ((Gluco2::Solver*)s)->conflict.size();
}
int bmcg2_sat_solver_addvar(bmcg2_sat_solver* s)
{
return glucose_solver_addvar((Gluco2::Solver*)s);
}
void bmcg2_sat_solver_set_nvars( bmcg2_sat_solver* s, int nvars )
{
int i;
for ( i = bmcg2_sat_solver_varnum(s); i < nvars; i++ )
bmcg2_sat_solver_addvar(s);
}
int bmcg2_sat_solver_eliminate( bmcg2_sat_solver* s, int turn_off_elim )
{
return 1;
// return ((Gluco2::SimpSolver*)s)->eliminate(turn_off_elim != 0);
}
int bmcg2_sat_solver_var_is_elim( bmcg2_sat_solver* s, int v )
{
return 0;
// return ((Gluco2::SimpSolver*)s)->isEliminated(v);
}
void bmcg2_sat_solver_var_set_frozen( bmcg2_sat_solver* s, int v, int freeze )
{
// ((Gluco2::SimpSolver*)s)->setFrozen(v, freeze);
}
int bmcg2_sat_solver_elim_varnum(bmcg2_sat_solver* s)
{
return 0;
// return ((Gluco2::SimpSolver*)s)->eliminated_vars;
}
int * bmcg2_sat_solver_read_cex(bmcg2_sat_solver* s)
{
return glucose_solver_read_cex((Gluco2::Solver*)s);
}
int bmcg2_sat_solver_read_cex_varvalue(bmcg2_sat_solver* s, int ivar)
{
return glucose_solver_read_cex_varvalue((Gluco2::Solver*)s, ivar);
}
void bmcg2_sat_solver_set_stop(bmcg2_sat_solver* s, int * pstop)
{
glucose_solver_setstop((Gluco2::Solver*)s, pstop);
}
abctime bmcg2_sat_solver_set_runtime_limit(bmcg2_sat_solver* s, abctime Limit)
{
abctime nRuntimeLimit = ((Gluco2::Solver*)s)->nRuntimeLimit;
((Gluco2::Solver*)s)->nRuntimeLimit = Limit;
return nRuntimeLimit;
}
void bmcg2_sat_solver_set_conflict_budget(bmcg2_sat_solver* s, int Limit)
{
if ( Limit > 0 )
((Gluco2::Solver*)s)->setConfBudget( (int64_t)Limit );
else
((Gluco2::Solver*)s)->budgetOff();
}
int bmcg2_sat_solver_varnum(bmcg2_sat_solver* s)
{
return ((Gluco2::Solver*)s)->nVars();
}
int bmcg2_sat_solver_clausenum(bmcg2_sat_solver* s)
{
return ((Gluco2::Solver*)s)->nClauses();
}
int bmcg2_sat_solver_learntnum(bmcg2_sat_solver* s)
{
return ((Gluco2::Solver*)s)->nLearnts();
}
int bmcg2_sat_solver_conflictnum(bmcg2_sat_solver* s)
{
return ((Gluco2::Solver*)s)->conflicts;
}
int bmcg2_sat_solver_minimize_assumptions( bmcg2_sat_solver * s, int * plits, int nlits, int pivot )
{
vec<int>*array = &((Gluco2::Solver*)s)->user_vec;
int i, nlitsL, nlitsR, nresL, nresR, status;
assert( pivot >= 0 );
// assert( nlits - pivot >= 2 );
assert( nlits - pivot >= 1 );
if ( nlits - pivot == 1 )
{
// since the problem is UNSAT, we try to solve it without assuming the last literal
// if the result is UNSAT, the last literal can be dropped; otherwise, it is needed
status = bmcg2_sat_solver_solve( s, plits, pivot );
return status != GLUCOSE_UNSAT; // return 1 if the problem is not UNSAT
}
assert( nlits - pivot >= 2 );
nlitsL = (nlits - pivot) / 2;
nlitsR = (nlits - pivot) - nlitsL;
assert( nlitsL + nlitsR == nlits - pivot );
// solve with these assumptions
status = bmcg2_sat_solver_solve( s, plits, pivot + nlitsL );
if ( status == GLUCOSE_UNSAT ) // these are enough
return bmcg2_sat_solver_minimize_assumptions( s, plits, pivot + nlitsL, pivot );
// these are not enough
// solve for the right lits
// nResL = nLitsR == 1 ? 1 : sat_solver_minimize_assumptions( s, pLits + nLitsL, nLitsR, nConfLimit );
nresL = nlitsR == 1 ? 1 : bmcg2_sat_solver_minimize_assumptions( s, plits, nlits, pivot + nlitsL );
// swap literals
array->clear();
for ( i = 0; i < nlitsL; i++ )
array->push(plits[pivot + i]);
for ( i = 0; i < nresL; i++ )
plits[pivot + i] = plits[pivot + nlitsL + i];
for ( i = 0; i < nlitsL; i++ )
plits[pivot + nresL + i] = (*array)[i];
// solve with these assumptions
status = bmcg2_sat_solver_solve( s, plits, pivot + nresL );
if ( status == GLUCOSE_UNSAT ) // these are enough
return nresL;
// solve for the left lits
// nResR = nLitsL == 1 ? 1 : sat_solver_minimize_assumptions( s, pLits + nResL, nLitsL, nConfLimit );
nresR = nlitsL == 1 ? 1 : bmcg2_sat_solver_minimize_assumptions( s, plits, pivot + nresL + nlitsL, pivot + nresL );
return nresL + nresR;
}
#endif
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void glucose_print_stats(SimpSolver& 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 ? (int)(s.conflicts/s.starts) : 0);
printf("c blocked restarts : %d (multiple: %d) \n", (int)s.nbstopsrestarts, (int)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_ReadDimacs( char * pFileName, SimpSolver& s )
{
vec<Lit> * lits = &s.user_lits;
char * pBuffer = Extra_FileReadContents( pFileName );
char * pTemp; int fComp, Var, VarMax = 0;
lits->clear();
for ( pTemp = pBuffer; *pTemp; pTemp++ )
{
if ( *pTemp == 'c' || *pTemp == 'p' ) {
while ( *pTemp != '\n' )
pTemp++;
continue;
}
while ( *pTemp == ' ' || *pTemp == '\t' || *pTemp == '\r' || *pTemp == '\n' )
pTemp++;
fComp = 0;
if ( *pTemp == '-' )
fComp = 1, pTemp++;
if ( *pTemp == '+' )
pTemp++;
Var = atoi( pTemp );
if ( Var == 0 ) {
if ( lits->size() > 0 ) {
s.addVar( VarMax );
s.addClause(*lits);
lits->clear();
}
}
else {
Var--;
VarMax = Abc_MaxInt( VarMax, Var );
lits->push( toLit(Abc_Var2Lit(Var, fComp)) );
}
while ( *pTemp >= '0' && *pTemp <= '9' )
pTemp++;
}
ABC_FREE( pBuffer );
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Glucose2_SolveCnf( char * pFileName, Glucose2_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);
Glucose_ReadDimacs( pFileName, S );
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);
printf( "c Simplication removed %d variables and %d clauses. ", S.eliminated_vars, S.eliminated_clauses );
Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
}
vec<Lit> dummy;
lbool ret = S.solveLimited(dummy, 0);
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();
vec<Lit> * lits = &s.user_lits;
Cnf_Dat_t * pCnf = (Cnf_Dat_t *)Mf_ManGenerateCnf( p, 8 /*nLutSize*/, 0 /*fCnfObjIds*/, 1/*fAddOrCla*/, 0, 0/*verbose*/ );
for ( int i = 0; i < pCnf->nClauses; i++ )
{
lits->clear();
for ( int * pLit = pCnf->pClauses[i]; pLit < pCnf->pClauses[i+1]; pLit++ )
lits->push( toLit(*pLit) ), s.addVar( *pLit >> 1 );
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;
}
// procedure below does not work because glucose_solver_addclause() expects Solver
Vec_Int_t * Glucose_SolverFromAig2( Gia_Man_t * p, SimpSolver& S )
{
Cnf_Dat_t * pCnf = (Cnf_Dat_t *)Mf_ManGenerateCnf( p, 8 /*nLutSize*/, 0 /*fCnfObjIds*/, 1/*fAddOrCla*/, 0, 0/*verbose*/ );
for ( int i = 0; i < pCnf->nClauses; i++ )
if ( !glucose_solver_addclause( &S, pCnf->pClauses[i], pCnf->pClauses[i+1]-pCnf->pClauses[i] ) )
assert( 0 );
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;
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Vec_Str_t * Glucose2_GenerateCubes( bmcg2_sat_solver * pSat[2], Vec_Int_t * vCiSatVars, Vec_Int_t * vVar2Index, int CubeLimit )
{
int fCreatePrime = 1;
int nCubes, nSupp = Vec_IntSize(vCiSatVars);
Vec_Str_t * vSop = Vec_StrAlloc( 1000 );
Vec_Int_t * vLits = Vec_IntAlloc( nSupp );
Vec_Str_t * vCube = Vec_StrAlloc( nSupp + 4 );
Vec_StrFill( vCube, nSupp, '-' );
Vec_StrPrintF( vCube, " 1\n\0" );
for ( nCubes = 0; !CubeLimit || nCubes < CubeLimit; nCubes++ )
{
int * pFinal, nFinal, iVar, i, k = 0;
// generate onset minterm
int status = bmcg2_sat_solver_solve( pSat[1], NULL, 0 );
if ( status == GLUCOSE_UNSAT )
break;
assert( status == GLUCOSE_SAT );
Vec_IntClear( vLits );
Vec_IntForEachEntry( vCiSatVars, iVar, i )
Vec_IntPush( vLits, Abc_Var2Lit(iVar, !bmcg2_sat_solver_read_cex_varvalue(pSat[1], iVar)) );
// expand against offset
if ( fCreatePrime )
{
nFinal = bmcg2_sat_solver_minimize_assumptions( pSat[0], Vec_IntArray(vLits), Vec_IntSize(vLits), 0 );
Vec_IntShrink( vLits, nFinal );
pFinal = Vec_IntArray( vLits );
for ( i = 0; i < nFinal; i++ )
pFinal[i] = Abc_LitNot(pFinal[i]);
}
else
{
status = bmcg2_sat_solver_solve( pSat[0], Vec_IntArray(vLits), Vec_IntSize(vLits) );
assert( status == GLUCOSE_UNSAT );
nFinal = bmcg2_sat_solver_final( pSat[0], &pFinal );
}
// print cube
Vec_StrFill( vCube, nSupp, '-' );
for ( i = 0; i < nFinal; i++ )
{
int Index = Vec_IntEntry(vVar2Index, Abc_Lit2Var(pFinal[i]));
if ( Index == -1 )
continue;
pFinal[k++] = pFinal[i];
assert( Index >= 0 && Index < nSupp );
Vec_StrWriteEntry( vCube, Index, (char)('0' + Abc_LitIsCompl(pFinal[i])) );
}
nFinal = k;
Vec_StrAppend( vSop, Vec_StrArray(vCube) );
//printf( "%s\n", Vec_StrArray(vCube) );
// add blocking clause
if ( !bmcg2_sat_solver_addclause( pSat[1], pFinal, nFinal ) )
break;
}
Vec_IntFree( vLits );
Vec_StrFree( vCube );
Vec_StrPush( vSop, '\0' );
return vSop;
}
Vec_Str_t * bmcg2_sat_solver_sop( Gia_Man_t * p, int CubeLimit )
{
bmcg2_sat_solver * pSat[2] = { bmcg2_sat_solver_start(), bmcg2_sat_solver_start() };
// generate CNF for the on-set and off-set
Cnf_Dat_t * pCnf = (Cnf_Dat_t *)Mf_ManGenerateCnf( p, 8 /*nLutSize*/, 0 /*fCnfObjIds*/, 0/*fAddOrCla*/, 0, 0/*verbose*/ );
int i, n, nVars = Gia_ManCiNum(p), Lit;//, Count = 0;
int iFirstVar = pCnf->nVars - nVars;
assert( Gia_ManCoNum(p) == 1 );
for ( n = 0; n < 2; n++ )
{
bmcg2_sat_solver_set_nvars( pSat[n], pCnf->nVars );
Lit = Abc_Var2Lit( 1, !n ); // output variable is 1
for ( i = 0; i < pCnf->nClauses; i++ )
if ( !bmcg2_sat_solver_addclause( pSat[n], pCnf->pClauses[i], pCnf->pClauses[i+1]-pCnf->pClauses[i] ) )
assert( 0 );
if ( !bmcg2_sat_solver_addclause( pSat[n], &Lit, 1 ) )
{
Vec_Str_t * vSop = Vec_StrAlloc( 10 );
Vec_StrPrintF( vSop, " %d\n\0", !n );
Cnf_DataFree( pCnf );
return vSop;
}
}
Cnf_DataFree( pCnf );
// collect cube vars and map SAT vars into them
Vec_Int_t * vVars = Vec_IntAlloc( 100 );
Vec_Int_t * vVarMap = Vec_IntStartFull( iFirstVar + nVars );
for ( i = 0; i < nVars; i++ )
{
Vec_IntPush( vVars, iFirstVar+i );
Vec_IntWriteEntry( vVarMap, iFirstVar+i, i );
}
Vec_Str_t * vSop = Glucose2_GenerateCubes( pSat, vVars, vVarMap, CubeLimit );
Vec_IntFree( vVarMap );
Vec_IntFree( vVars );
bmcg2_sat_solver_stop( pSat[0] );
bmcg2_sat_solver_stop( pSat[1] );
return vSop;
}
void bmcg2_sat_solver_print_sop( Gia_Man_t * p )
{
Vec_Str_t * vSop = bmcg2_sat_solver_sop( p, 0 );
printf( "%s", Vec_StrArray(vSop) );
Vec_StrFree( vSop );
}
void bmcg2_sat_solver_print_sop_lit( Gia_Man_t * p, int Lit )
{
Vec_Int_t * vCisUsed = Vec_IntAlloc( 100 );
int i, ObjId, iNode = Abc_Lit2Var( Lit );
Gia_ManCollectCis( p, &iNode, 1, vCisUsed );
Vec_IntSort( vCisUsed, 0 );
Vec_IntForEachEntry( vCisUsed, ObjId, i )
Vec_IntWriteEntry( vCisUsed, i, Gia_ManIdToCioId(p, ObjId) );
Vec_IntPrint( vCisUsed );
Gia_Man_t * pNew = Gia_ManDupConeSupp( p, Lit, vCisUsed );
Vec_IntFree( vCisUsed );
bmcg2_sat_solver_print_sop( pNew );
Gia_ManStop( pNew );
printf( "\n" );
}
/**Function*************************************************************
Synopsis [Computing d-literals.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
#define Gia_CubeForEachVar( pCube, Value, i ) \
for ( i = 0; (pCube[i] != ' ') && (Value = pCube[i]); i++ )
#define Gia_SopForEachCube( pSop, nFanins, pCube ) \
for ( pCube = (pSop); *pCube; pCube += (nFanins) + 3 )
void bmcg2_sat_generate_dvars( Vec_Int_t * vCiVars, Vec_Str_t * vSop, Vec_Int_t * vDLits )
{
int i, Lit, Counter, nCubes = 0;
char Value, * pCube, * pSop = Vec_StrArray( vSop );
Vec_Int_t * vCounts = Vec_IntStart( 2*Vec_IntSize(vCiVars) );
Vec_IntClear( vDLits );
Gia_SopForEachCube( pSop, Vec_IntSize(vCiVars), pCube )
{
nCubes++;
Gia_CubeForEachVar( pCube, Value, i )
{
if ( Value == '1' )
Vec_IntAddToEntry( vCounts, 2*i, 1 );
else if ( Value == '0' )
Vec_IntAddToEntry( vCounts, 2*i+1, 1 );
}
}
Vec_IntForEachEntry( vCounts, Counter, Lit )
if ( Counter == nCubes )
Vec_IntPush( vDLits, Abc_Var2Lit(Vec_IntEntry(vCiVars, Abc_Lit2Var(Lit)), Abc_LitIsCompl(Lit)) );
Vec_IntSort( vDLits, 0 );
Vec_IntFree( vCounts );
}
/**Function*************************************************************
Synopsis [Performs SAT-based quantification.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int bmcg2_sat_solver_quantify2( Gia_Man_t * p, int iLit, int fHash, int(*pFuncCiToKeep)(void *, int), void * pData, Vec_Int_t * vDLits )
{
int fSynthesize = 0;
extern Gia_Man_t * Abc_SopSynthesizeOne( char * pSop, int fClp );
Gia_Man_t * pMan, * pNew, * pTemp; Vec_Str_t * vSop;
int i, CiId, ObjId, Res, nCubes = 0, nNodes, Count = 0, iNode = Abc_Lit2Var(iLit);
Vec_Int_t * vCisUsed = Vec_IntAlloc( 100 );
Gia_ManCollectCis( p, &iNode, 1, vCisUsed );
Vec_IntSort( vCisUsed, 0 );
if ( vDLits ) Vec_IntClear( vDLits );
if ( iLit < 2 )
return iLit;
// remap into CI Ids
Vec_IntForEachEntry( vCisUsed, ObjId, i )
Vec_IntWriteEntry( vCisUsed, i, Gia_ManIdToCioId(p, ObjId) );
// duplicate cone
pNew = Gia_ManDupConeSupp( p, iLit, vCisUsed );
assert( Gia_ManCiNum(pNew) == Vec_IntSize(vCisUsed) );
nNodes = Gia_ManAndNum(pNew);
// perform quantification one CI at a time
assert( pFuncCiToKeep );
Vec_IntForEachEntry( vCisUsed, CiId, i )
if ( !pFuncCiToKeep( pData, CiId ) )
{
//printf( "Quantifying %d.\n", CiId );
pNew = Gia_ManDupExist( pTemp = pNew, i );
Gia_ManStop( pTemp );
Count++;
}
if ( Gia_ManPoIsConst(pNew, 0) )
{
int RetValue = Gia_ManPoIsConst1(pNew, 0);
Vec_IntFree( vCisUsed );
Gia_ManStop( pNew );
return RetValue;
}
if ( fSynthesize )
{
vSop = bmcg2_sat_solver_sop( pNew, 0 );
Gia_ManStop( pNew );
pMan = Abc_SopSynthesizeOne( Vec_StrArray(vSop), 1 );
nCubes = Vec_StrCountEntry(vSop, '\n');
if ( vDLits )
{
// convert into object IDs
Vec_Int_t * vCisObjs = Vec_IntAlloc( Vec_IntSize(vCisUsed) );
Vec_IntForEachEntry( vCisUsed, CiId, i )
Vec_IntPush( vCisObjs, CiId + 1 );
bmcg2_sat_generate_dvars( vCisObjs, vSop, vDLits );
Vec_IntFree( vCisObjs );
}
Vec_StrFree( vSop );
if ( Gia_ManPoIsConst(pMan, 0) )
{
int RetValue = Gia_ManPoIsConst1(pMan, 0);
Vec_IntFree( vCisUsed );
Gia_ManStop( pMan );
return RetValue;
}
}
else
{
pMan = pNew;
}
Res = Gia_ManDupConeBack( p, pMan, vCisUsed );
// report the result
//printf( "Performed quantification with %5d nodes, %3d keep-vars, %3d quant-vars, resulting in %5d cubes and %5d nodes. ",
// nNodes, Vec_IntSize(vCisUsed) - Count, Count, nCubes, Gia_ManAndNum(pMan) );
//Abc_PrintTime( 1, "Time", Abc_Clock() - clkAll );
Vec_IntFree( vCisUsed );
Gia_ManStop( pMan );
return Res;
}
/**Function*************************************************************
Synopsis [Performs SAT-based quantification.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Gia_ManSatAndCollect2_rec( Gia_Man_t * p, int iObj, Vec_Int_t * vObjsUsed, Vec_Int_t * vCiVars )
{
Gia_Obj_t * pObj; int iVar;
if ( (iVar = Gia_ObjCopyArray(p, iObj)) >= 0 )
return iVar;
pObj = Gia_ManObj( p, iObj );
assert( Gia_ObjIsCand(pObj) );
if ( Gia_ObjIsAnd(pObj) )
{
Gia_ManSatAndCollect2_rec( p, Gia_ObjFaninId0(pObj, iObj), vObjsUsed, vCiVars );
Gia_ManSatAndCollect2_rec( p, Gia_ObjFaninId1(pObj, iObj), vObjsUsed, vCiVars );
}
iVar = Vec_IntSize( vObjsUsed );
Vec_IntPush( vObjsUsed, iObj );
Gia_ObjSetCopyArray( p, iObj, iVar );
if ( vCiVars && Gia_ObjIsCi(pObj) )
Vec_IntPush( vCiVars, iVar );
return iVar;
}
void Gia_ManQuantLoadCnf2( Gia_Man_t * p, Vec_Int_t * vObjsUsed, bmcg2_sat_solver * pSats[] )
{
Gia_Obj_t * pObj; int i;
bmcg2_sat_solver_reset( pSats[0] );
if ( pSats[1] )
bmcg2_sat_solver_reset( pSats[1] );
bmcg2_sat_solver_set_nvars( pSats[0], Vec_IntSize(vObjsUsed) );
if ( pSats[1] )
bmcg2_sat_solver_set_nvars( pSats[1], Vec_IntSize(vObjsUsed) );
Gia_ManForEachObjVec( vObjsUsed, p, pObj, i )
if ( Gia_ObjIsAnd(pObj) )
{
int iObj = Gia_ObjId( p, pObj );
int iVar = Gia_ObjCopyArray(p, iObj);
int iVar0 = Gia_ObjCopyArray(p, Gia_ObjFaninId0(pObj, iObj));
int iVar1 = Gia_ObjCopyArray(p, Gia_ObjFaninId1(pObj, iObj));
bmcg2_sat_solver_add_and( pSats[0], iVar, iVar0, iVar1, Gia_ObjFaninC0(pObj), Gia_ObjFaninC1(pObj), 0 );
if ( pSats[1] )
bmcg2_sat_solver_add_and( pSats[1], iVar, iVar0, iVar1, Gia_ObjFaninC0(pObj), Gia_ObjFaninC1(pObj), 0 );
}
else if ( Gia_ObjIsConst0(pObj) )
{
int Lit = Abc_Var2Lit( Gia_ObjCopyArray(p, 0), 1 );
int RetValue = bmcg2_sat_solver_addclause( pSats[0], &Lit, 1 );
assert( RetValue );
if ( pSats[1] )
bmcg2_sat_solver_addclause( pSats[1], &Lit, 1 );
assert( Lit == 1 );
}
}
int Gia_ManFactorSop2( Gia_Man_t * p, Vec_Int_t * vCiObjIds, Vec_Str_t * vSop, int fHash )
{
extern Gia_Man_t * Abc_SopSynthesizeOne( char * pSop, int fClp );
Gia_Man_t * pMan = Abc_SopSynthesizeOne( Vec_StrArray(vSop), 1 );
Gia_Obj_t * pObj; int i, Result;
assert( Gia_ManPiNum(pMan) == Vec_IntSize(vCiObjIds) );
Gia_ManConst0(pMan)->Value = 0;
Gia_ManForEachPi( pMan, pObj, i )
pObj->Value = Abc_Var2Lit( Vec_IntEntry(vCiObjIds, i), 0 );
Gia_ManForEachAnd( pMan, pObj, i )
if ( fHash )
pObj->Value = Gia_ManHashAnd( p, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
else
pObj->Value = Gia_ManAppendAnd( p, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
pObj = Gia_ManPo(pMan, 0);
Result = Gia_ObjFanin0Copy(pObj);
Gia_ManStop( pMan );
return Result;
}
int bmcg2_sat_solver_quantify( bmcg2_sat_solver * pSats[], Gia_Man_t * p, int iLit, int fHash, int(*pFuncCiToKeep)(void *, int), void * pData, Vec_Int_t * vDLits )
{
Vec_Int_t * vObjsUsed = Vec_IntAlloc( 100 ); // GIA objs
Vec_Int_t * vCiVars = Vec_IntAlloc( 100 ); // CI SAT vars
Vec_Int_t * vVarMap = NULL; Vec_Str_t * vSop = NULL;
int i, iVar, iVarLast, Lit, RetValue, Count = 0, Result = -1;
if ( vDLits ) Vec_IntClear( vDLits );
if ( iLit < 2 )
return iLit;
if ( Vec_IntSize(&p->vCopies) < Gia_ManObjNum(p) )
Vec_IntFillExtra( &p->vCopies, Gia_ManObjNum(p), -1 );
// assign variable number 0 to const0 node
iVar = Vec_IntSize(vObjsUsed);
Vec_IntPush( vObjsUsed, 0 );
Gia_ObjSetCopyArray( p, 0, iVar );
assert( iVar == 0 );
// collect other variables
iVarLast = Gia_ManSatAndCollect2_rec( p, Abc_Lit2Var(iLit), vObjsUsed, vCiVars );
Gia_ManQuantLoadCnf2( p, vObjsUsed, pSats );
// check constants
Lit = Abc_Var2Lit( iVarLast, !Abc_LitIsCompl(iLit) );
RetValue = bmcg2_sat_solver_addclause( pSats[0], &Lit, 1 ); // offset
if ( !RetValue || bmcg2_sat_solver_solve(pSats[0], NULL, 0) == GLUCOSE_UNSAT )
{
Result = 1;
goto cleanup;
}
Lit = Abc_Var2Lit( iVarLast, Abc_LitIsCompl(iLit) );
RetValue = bmcg2_sat_solver_addclause( pSats[1], &Lit, 1 ); // onset
if ( !RetValue || bmcg2_sat_solver_solve(pSats[1], NULL, 0) == GLUCOSE_UNSAT )
{
Result = 0;
goto cleanup;
}
/*
// reorder CI SAT variables to have keep-vars first
Vec_Int_t * vCiVars2 = Vec_IntAlloc( 100 ); // CI SAT vars
Vec_IntForEachEntry( vCiVars, iVar, i )
{
Gia_Obj_t * pObj = Gia_ManObj( p, Vec_IntEntry(vObjsUsed, iVar) );
assert( Gia_ObjIsCi(pObj) );
if ( pFuncCiToKeep(pData, Gia_ObjCioId(pObj)) )
Vec_IntPush( vCiVars2, iVar );
}
Vec_IntForEachEntry( vCiVars, iVar, i )
{
Gia_Obj_t * pObj = Gia_ManObj( p, Vec_IntEntry(vObjsUsed, iVar) );
assert( Gia_ObjIsCi(pObj) );
if ( !pFuncCiToKeep(pData, Gia_ObjCioId(pObj)) )
Vec_IntPush( vCiVars2, iVar );
}
ABC_SWAP( Vec_Int_t *, vCiVars2, vCiVars );
Vec_IntFree( vCiVars2 );
*/
// map CI SAT variables into their indexes used in the cubes
vVarMap = Vec_IntStartFull( Vec_IntSize(vObjsUsed) );
Vec_IntForEachEntry( vCiVars, iVar, i )
{
Gia_Obj_t * pObj = Gia_ManObj( p, Vec_IntEntry(vObjsUsed, iVar) );
assert( Gia_ObjIsCi(pObj) );
if ( pFuncCiToKeep(pData, Gia_ObjCioId(pObj)) )
Vec_IntWriteEntry( vVarMap, iVar, i ), Count++;
}
if ( Count == 0 || Count == Vec_IntSize(vCiVars) )
{
Result = Count == 0 ? 1 : iLit;
goto cleanup;
}
// generate cubes
vSop = Glucose2_GenerateCubes( pSats, vCiVars, vVarMap, 0 );
//printf( "%s", Vec_StrArray(vSop) );
// convert into object IDs
Vec_IntForEachEntry( vCiVars, iVar, i )
Vec_IntWriteEntry( vCiVars, i, Vec_IntEntry(vObjsUsed, iVar) );
// generate unate variables
if ( vDLits )
bmcg2_sat_generate_dvars( vCiVars, vSop, vDLits );
// convert into an AIG
RetValue = Gia_ManAndNum(p);
Result = Gia_ManFactorSop2( p, vCiVars, vSop, fHash );
// report the result
// printf( "Performed quantification with %5d nodes, %3d keep-vars, %3d quant-vars, resulting in %5d cubes and %5d nodes. ",
// Vec_IntSize(vObjsUsed), Count, Vec_IntSize(vCiVars) - Count, Vec_StrCountEntry(vSop, '\n'), Gia_ManAndNum(p)-RetValue );
// Abc_PrintTime( 1, "Time", Abc_Clock() - clkAll );
cleanup:
Vec_IntForEachEntry( vObjsUsed, iVar, i )
Gia_ObjSetCopyArray( p, iVar, -1 );
Vec_IntFree( vObjsUsed );
Vec_IntFree( vCiVars );
Vec_IntFreeP( &vVarMap );
Vec_StrFreeP( &vSop );
return Result;
}
int Gia_ManCiIsToKeep2( void * pData, int i )
{
return i % 5 != 0;
}
void Glucose2_QuantifyAigTest( Gia_Man_t * p )
{
bmcg2_sat_solver * pSats[3] = { bmcg2_sat_solver_start(), bmcg2_sat_solver_start(), bmcg2_sat_solver_start() };
abctime clk1 = Abc_Clock();
int iRes1 = bmcg2_sat_solver_quantify( pSats, p, Gia_ObjFaninLit0p(p, Gia_ManPo(p, 0)), 0, Gia_ManCiIsToKeep2, NULL, NULL );
abctime clk1d = Abc_Clock()-clk1;
abctime clk2 = Abc_Clock();
int iRes2 = bmcg2_sat_solver_quantify2( p, Gia_ObjFaninLit0p(p, Gia_ManPo(p, 0)), 0, Gia_ManCiIsToKeep2, NULL, NULL );
abctime clk2d = Abc_Clock()-clk2;
Abc_PrintTime( 1, "Time1", clk1d );
Abc_PrintTime( 1, "Time2", clk2d );
if ( bmcg2_sat_solver_equiv_overlap_check( pSats[2], p, iRes1, iRes2, 1 ) )
printf( "Verification passed.\n" );
else
printf( "Verification FAILED.\n" );
Gia_ManAppendCo( p, iRes1 );
Gia_ManAppendCo( p, iRes2 );
bmcg2_sat_solver_stop( pSats[0] );
bmcg2_sat_solver_stop( pSats[1] );
bmcg2_sat_solver_stop( pSats[2] );
}
int bmcg2_sat_solver_quantify_test( bmcg2_sat_solver * pSats[], Gia_Man_t * p, int iLit, int fHash, int(*pFuncCiToKeep)(void *, int), void * pData, Vec_Int_t * vDLits )
{
extern int Gia_ManQuantExist( Gia_Man_t * p, int iLit, int(*pFuncCiToKeep)(void *, int), void * pData );
int Res1 = Gia_ManQuantExist( p, iLit, pFuncCiToKeep, pData );
int Res2 = bmcg2_sat_solver_quantify2( p, iLit, 1, pFuncCiToKeep, pData, NULL );
bmcg2_sat_solver * pSat = bmcg2_sat_solver_start();
if ( bmcg2_sat_solver_equiv_overlap_check( pSat, p, Res1, Res2, 1 ) )
printf( "Verification passed.\n" );
else
{
printf( "Verification FAILED.\n" );
bmcg2_sat_solver_print_sop_lit( p, Res1 );
bmcg2_sat_solver_print_sop_lit( p, Res2 );
printf( "\n" );
}
return Res1;
}
/**Function*************************************************************
Synopsis [Checks equivalence or intersection of two nodes.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int bmcg2_sat_solver_equiv_overlap_check( bmcg2_sat_solver * pSat, Gia_Man_t * p, int iLit0, int iLit1, int fEquiv )
{
bmcg2_sat_solver * pSats[2] = { pSat, NULL };
Vec_Int_t * vObjsUsed = Vec_IntAlloc( 100 );
int i, iVar, iSatVar[2], iSatLit[2], Lits[2], status;
if ( Vec_IntSize(&p->vCopies) < Gia_ManObjNum(p) )
Vec_IntFillExtra( &p->vCopies, Gia_ManObjNum(p), -1 );
// assign const0 variable number 0
iVar = Vec_IntSize(vObjsUsed);
Vec_IntPush( vObjsUsed, 0 );
Gia_ObjSetCopyArray( p, 0, iVar );
assert( iVar == 0 );
iSatVar[0] = Gia_ManSatAndCollect2_rec( p, Abc_Lit2Var(iLit0), vObjsUsed, NULL );
iSatVar[1] = Gia_ManSatAndCollect2_rec( p, Abc_Lit2Var(iLit1), vObjsUsed, NULL );
iSatLit[0] = Abc_Var2Lit( iSatVar[0], Abc_LitIsCompl(iLit0) );
iSatLit[1] = Abc_Var2Lit( iSatVar[1], Abc_LitIsCompl(iLit1) );
Gia_ManQuantLoadCnf2( p, vObjsUsed, pSats );
Vec_IntForEachEntry( vObjsUsed, iVar, i )
Gia_ObjSetCopyArray( p, iVar, -1 );
Vec_IntFree( vObjsUsed );
if ( fEquiv )
{
Lits[0] = iSatLit[0];
Lits[1] = Abc_LitNot(iSatLit[1]);
status = bmcg2_sat_solver_solve( pSats[0], Lits, 2 );
if ( status == GLUCOSE_UNSAT )
{
Lits[0] = Abc_LitNot(iSatLit[0]);
Lits[1] = iSatLit[1];
status = bmcg2_sat_solver_solve( pSats[0], Lits, 2 );
}
return status == GLUCOSE_UNSAT;
}
else
{
Lits[0] = iSatLit[0];
Lits[1] = iSatLit[1];
status = bmcg2_sat_solver_solve( pSats[0], Lits, 2 );
return status == GLUCOSE_SAT;
}
}
void Glucose2_CheckTwoNodesTest( Gia_Man_t * p )
{
int n, Res;
bmcg2_sat_solver * pSat = bmcg2_sat_solver_start();
for ( n = 0; n < 2; n++ )
{
Res = bmcg2_sat_solver_equiv_overlap_check(
pSat, p,
Gia_ObjFaninLit0p(p, Gia_ManPo(p, 0)),
Gia_ObjFaninLit0p(p, Gia_ManPo(p, 1)),
n );
bmcg2_sat_solver_reset( pSat );
printf( "%s %s.\n", n ? "Equivalence" : "Overlap", Res ? "holds" : "fails" );
}
bmcg2_sat_solver_stop( pSat );
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Glucose2_SolveAig(Gia_Man_t * p, Glucose2_Pars * pPars)
{
abctime clk = Abc_Clock();
SimpSolver S;
S.verbosity = pPars->verb;
S.verbEveryConflicts = 50000;
S.showModel = false;
//S.verbosity = 2;
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);
printf( "c Simplication removed %d variables and %d clauses. ", S.eliminated_vars, S.eliminated_clauses );
Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
}
vec<Lit> dummy;
lbool ret = S.solveLimited(dummy, 0);
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
src/sat/glucose2/AbcGlucose2.h 0 → 100644
/**CFile****************************************************************
FileName [AbcGlucose.h]
SystemName [ABC: Logic synthesis and verification system.]
PackageName [SAT solver Glucose 3.0 by Gilles Audemard and Laurent Simon.]
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 ABC_SAT_GLUCOSE_H_
#define ABC_SAT_GLUCOSE_H_
////////////////////////////////////////////////////////////////////////
/// INCLUDES ///
////////////////////////////////////////////////////////////////////////
#include "aig/gia/gia.h"
////////////////////////////////////////////////////////////////////////
/// PARAMETERS ///
////////////////////////////////////////////////////////////////////////
#define GLUCOSE_UNSAT -1
#define GLUCOSE_SAT 1
#define GLUCOSE_UNDEC 0
ABC_NAMESPACE_HEADER_START
////////////////////////////////////////////////////////////////////////
/// BASIC TYPES ///
////////////////////////////////////////////////////////////////////////
typedef struct Glucose2_Pars_ Glucose2_Pars;
struct Glucose2_Pars_ {
int pre; // preprocessing
int verb; // verbosity
int cust; // customizable
int nConfls; // conflict limit (0 = no limit)
};
static inline Glucose2_Pars Glucose_CreatePars(int p, int v, int c, int nConfls)
{
Glucose2_Pars pars;
pars.pre = p;
pars.verb = v;
pars.cust = c;
pars.nConfls = nConfls;
return pars;
}
typedef void bmcg2_sat_solver;
////////////////////////////////////////////////////////////////////////
/// MACRO DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
////////////////////////////////////////////////////////////////////////
/// FUNCTION DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
extern bmcg2_sat_solver * bmcg2_sat_solver_start();
extern void bmcg2_sat_solver_stop( bmcg2_sat_solver* s );
extern void bmcg2_sat_solver_reset( bmcg2_sat_solver* s );
extern int bmcg2_sat_solver_addclause( bmcg2_sat_solver* s, int * plits, int nlits );
extern void bmcg2_sat_solver_setcallback( bmcg2_sat_solver* s, void * pman, int(*pfunc)(void*, int, int*) );
extern int bmcg2_sat_solver_solve( bmcg2_sat_solver* s, int * plits, int nlits );
extern int bmcg2_sat_solver_final( bmcg2_sat_solver* s, int ** ppArray );
extern int bmcg2_sat_solver_addvar( bmcg2_sat_solver* s );
extern void bmcg2_sat_solver_set_nvars( bmcg2_sat_solver* s, int nvars );
extern int bmcg2_sat_solver_eliminate( bmcg2_sat_solver* s, int turn_off_elim );
extern int bmcg2_sat_solver_var_is_elim( bmcg2_sat_solver* s, int v );
extern void bmcg2_sat_solver_var_set_frozen( bmcg2_sat_solver* s, int v, int freeze );
extern int bmcg2_sat_solver_elim_varnum(bmcg2_sat_solver* s);
extern int * bmcg2_sat_solver_read_cex( bmcg2_sat_solver* s );
extern int bmcg2_sat_solver_read_cex_varvalue( bmcg2_sat_solver* s, int );
extern void bmcg2_sat_solver_set_stop( bmcg2_sat_solver* s, int * pstop );
extern abctime bmcg2_sat_solver_set_runtime_limit( bmcg2_sat_solver* s, abctime Limit );
extern void bmcg2_sat_solver_set_conflict_budget( bmcg2_sat_solver* s, int Limit );
extern int bmcg2_sat_solver_varnum( bmcg2_sat_solver* s );
extern int bmcg2_sat_solver_clausenum( bmcg2_sat_solver* s );
extern int bmcg2_sat_solver_learntnum( bmcg2_sat_solver* s );
extern int bmcg2_sat_solver_conflictnum( bmcg2_sat_solver* s );
extern int bmcg2_sat_solver_minimize_assumptions( bmcg2_sat_solver * s, int * plits, int nlits, int pivot );
extern int bmcg2_sat_solver_add_and( bmcg2_sat_solver * s, int iVar, int iVar0, int iVar1, int fCompl0, int fCompl1, int fCompl );
extern int bmcg2_sat_solver_quantify( bmcg2_sat_solver * s[], Gia_Man_t * p, int iLit, int fHash, int(*pFuncCiToKeep)(void *, int), void * pData, Vec_Int_t * vDLits );
extern int bmcg2_sat_solver_equiv_overlap_check( bmcg2_sat_solver * s, Gia_Man_t * p, int iLit0, int iLit1, int fEquiv );
extern Vec_Str_t * bmcg2_sat_solver_sop( Gia_Man_t * p, int CubeLimit );
extern void Glucose2_SolveCnf( char * pFilename, Glucose2_Pars * pPars );
extern int Glucose2_SolveAig( Gia_Man_t * p, Glucose2_Pars * pPars );
ABC_NAMESPACE_HEADER_END
#endif
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
src/sat/glucose2/AbcGlucoseCmd2.cpp 0 → 100644
/**CFile****************************************************************
FileName [AbcGlucoseCmd.cpp]
SystemName [ABC: Logic synthesis and verification system.]
PackageName [SAT solver Glucose 3.0 by Gilles Audemard and Laurent Simon.]
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/glucose2/AbcGlucose2.h"
ABC_NAMESPACE_HEADER_START
extern void Glucose2_Init( Abc_Frame_t *pAbc );
extern void Glucose2_End( Abc_Frame_t * pAbc );
ABC_NAMESPACE_HEADER_END
ABC_NAMESPACE_IMPL_START
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
static int Abc_CommandGlucose( Abc_Frame_t * pAbc, int argc, char ** argv );
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Glucose2_Init(Abc_Frame_t *pAbc)
{
Cmd_CommandAdd( pAbc, "ABC9", "&glucose", Abc_CommandGlucose, 0 );
}
void Glucose2_End( Abc_Frame_t * pAbc )
{
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Abc_CommandGlucose( Abc_Frame_t * pAbc, int argc, char ** argv )
{
int c = 0;
int pre = 1;
int verb = 0;
int nConfls = 0;
Glucose2_Pars pPars;
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;
}
}
pPars = Glucose_CreatePars(pre,verb,0,nConfls);
if ( argc == globalUtilOptind + 1 )
{
Glucose2_SolveCnf( argv[globalUtilOptind], &pPars );
return 0;
}
if ( pAbc->pGia == NULL )
{
Abc_Print( -1, "Abc_CommandGlucose(): There is no AIG.\n" );
return 1;
}
if ( Glucose2_SolveAig( pAbc->pGia, &pPars ) == 10 )
Abc_FrameReplaceCex( pAbc, &pAbc->pGia->pCexComb );
return 0;
usage:
Abc_Print( -2, "usage: &glucose2 [-C num] [-pvh] <file.cnf>\n" );
Abc_Print( -2, "\t run Glucose 3.0 by Gilles Audemard and Laurent Simon\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
src/sat/glucose2/Alg.h 0 → 100644
/*******************************************************************************************[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/glucose2/Vec.h"
ABC_NAMESPACE_CXX_HEADER_START
namespace Gluco2 {
//=================================================================================================
// 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); }
//=================================================================================================
}
ABC_NAMESPACE_CXX_HEADER_END
#endif
src/sat/glucose2/Alloc.h 0 → 100644
/*****************************************************************************************[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/glucose2/XAlloc.h"
#include "sat/glucose2/Vec.h"
ABC_NAMESPACE_CXX_HEADER_START
namespace Gluco2 {
//=================================================================================================
// 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; }
void clear () { sz = 0; wasted_=0; }
// 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;
}
//=================================================================================================
}
ABC_NAMESPACE_CXX_HEADER_END
#endif
src/sat/glucose2/BoundedQueue.h 0 → 100644
/***********************************************************************************[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/glucose2/Vec.h"
ABC_NAMESPACE_CXX_HEADER_START
//=================================================================================================
namespace Gluco2 {
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;}
};
}
//=================================================================================================
ABC_NAMESPACE_CXX_HEADER_END
#endif
src/sat/glucose2/Constants.h 0 → 100644
/************************************************************************************[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
src/sat/glucose2/Dimacs.h 0 → 100644
/****************************************************************************************[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/glucose2/ParseUtils.h"
#include "sat/glucose2/SolverTypes.h"
ABC_NAMESPACE_CXX_HEADER_START
namespace Gluco2 {
//=================================================================================================
// 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); }
//=================================================================================================
}
ABC_NAMESPACE_CXX_HEADER_END
#endif
src/sat/glucose2/Glucose2.cpp 0 → 100644
/***************************************************************************************[Solver.cc]
Glucose -- Copyright (c) 2013, Gilles Audemard, Laurent Simon
CRIL - Univ. Artois, France
LRI - Univ. Paris Sud, France
Glucose sources are based on MiniSat (see below MiniSat copyrights). Permissions and copyrights of
Glucose are exactly the same as Minisat on which it is based on. (see below).
---------------
Copyright (c) 2003-2006, Niklas Een, Niklas Sorensson
Copyright (c) 2007-2010, Niklas Sorensson
Permission is hereby granted, free of charge, to any person obtaining a copy of this software and
associated documentation files (the "Software"), to deal in the Software without restriction,
including without limitation the rights to use, copy, modify, merge, publish, distribute,
sublicense, and/or sell copies of the Software, and to permit persons to whom the Software is
furnished to do so, subject to the following conditions:
The above copyright notice and this permission notice shall be included in all copies or
substantial portions of the Software.
THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR IMPLIED, INCLUDING BUT
NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND
NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM,
DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT
OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
**************************************************************************************************/
#include <math.h>
#include "sat/glucose2/Sort.h"
#include "sat/glucose2/Solver.h"
#include "sat/glucose2/Constants.h"
#include "sat/glucose2/System.h"
ABC_NAMESPACE_IMPL_START
using namespace Gluco2;
//=================================================================================================
// Options:
static const char* _cat = "CORE";
static const char* _cr = "CORE -- RESTART";
static const char* _cred = "CORE -- REDUCE";
static const char* _cm = "CORE -- MINIMIZE";
static const char* _certified = "CORE -- CERTIFIED UNSAT";
static BoolOption opt_incremental (_cat,"incremental", "Use incremental SAT solving", false);
static DoubleOption opt_K (_cr, "K", "The constant used to force restart", 0.8, DoubleRange(0, false, 1, false));
static DoubleOption opt_R (_cr, "R", "The constant used to block restart", 1.4, DoubleRange(1, false, 5, false));
static IntOption opt_size_lbd_queue (_cr, "szLBDQueue", "The size of moving average for LBD (restarts)", 50, IntRange(10, INT32_MAX));
static IntOption opt_size_trail_queue (_cr, "szTrailQueue", "The size of moving average for trail (block restarts)", 5000, IntRange(10, INT32_MAX));
static IntOption opt_first_reduce_db (_cred, "firstReduceDB", "The number of conflicts before the first reduce DB", 2000, IntRange(0, INT32_MAX));
static IntOption opt_inc_reduce_db (_cred, "incReduceDB", "Increment for reduce DB", 300, IntRange(0, INT32_MAX));
static IntOption opt_spec_inc_reduce_db (_cred, "specialIncReduceDB", "Special increment for reduce DB", 1000, IntRange(0, INT32_MAX));
static IntOption opt_lb_lbd_frozen_clause (_cred, "minLBDFrozenClause", "Protect clauses if their LBD decrease and is lower than (for one turn)", 30, IntRange(0, INT32_MAX));
static IntOption opt_lb_size_minimzing_clause (_cm, "minSizeMinimizingClause", "The min size required to minimize clause", 30, IntRange(3, INT32_MAX));
static IntOption opt_lb_lbd_minimzing_clause (_cm, "minLBDMinimizingClause", "The min LBD required to minimize clause", 6, IntRange(3, INT32_MAX));
static DoubleOption opt_var_decay (_cat, "var-decay", "The variable activity decay factor", 0.8, DoubleRange(0, false, 1, false));
static DoubleOption opt_clause_decay (_cat, "cla-decay", "The clause activity decay factor", 0.999, DoubleRange(0, false, 1, false));
static DoubleOption opt_random_var_freq (_cat, "rnd-freq", "The frequency with which the decision heuristic tries to choose a random variable", 0, DoubleRange(0, true, 1, true));
static DoubleOption opt_random_seed (_cat, "rnd-seed", "Used by the random variable selection", 91648253, DoubleRange(0, false, HUGE_VAL, false));
static IntOption opt_ccmin_mode (_cat, "ccmin-mode", "Controls conflict clause minimization (0=none, 1=basic, 2=deep)", 2, IntRange(0, 2));
static IntOption opt_phase_saving (_cat, "phase-saving", "Controls the level of phase saving (0=none, 1=limited, 2=full)", 2, IntRange(0, 2));
static BoolOption opt_rnd_init_act (_cat, "rnd-init", "Randomize the initial activity", false);
/*
static IntOption opt_restart_first (_cat, "rfirst", "The base restart interval", 100, IntRange(1, INT32_MAX));
static DoubleOption opt_restart_inc (_cat, "rinc", "Restart interval increase factor", 2, DoubleRange(1, false, HUGE_VAL, false));
*/
static DoubleOption opt_garbage_frac (_cat, "gc-frac", "The fraction of wasted memory allowed before a garbage collection is triggered", 0.20, DoubleRange(0, false, HUGE_VAL, false));
BoolOption opt_certified_ (_certified, "certified", "Certified UNSAT using DRUP format", false );
StringOption opt_certified_file_ (_certified, "certified-output", "Certified UNSAT output file", "NULL");
//=================================================================================================
// Constructor/Destructor:
Solver::Solver() :
// Parameters (user settable):
//
SolverType(0)
, pCnfFunc(NULL)
, nCallConfl(1000)
, terminate_search_early(false)
, pstop(NULL)
, nRuntimeLimit(0)
, verbosity (0)
, verbEveryConflicts(10000)
, showModel (0)
, K (opt_K)
, R (opt_R)
, sizeLBDQueue (opt_size_lbd_queue)
, sizeTrailQueue (opt_size_trail_queue)
, firstReduceDB (opt_first_reduce_db)
, incReduceDB (opt_inc_reduce_db)
, specialIncReduceDB (opt_spec_inc_reduce_db)
, lbLBDFrozenClause (opt_lb_lbd_frozen_clause)
, lbSizeMinimizingClause (opt_lb_size_minimzing_clause)
, lbLBDMinimizingClause (opt_lb_lbd_minimzing_clause)
, var_decay (opt_var_decay)
, clause_decay (opt_clause_decay)
, random_var_freq (opt_random_var_freq)
, random_seed (opt_random_seed)
, ccmin_mode (opt_ccmin_mode)
, phase_saving (opt_phase_saving)
, rnd_pol (false)
, rnd_init_act (opt_rnd_init_act)
, garbage_frac (opt_garbage_frac)
, certifiedOutput (NULL)
, certifiedUNSAT (opt_certified_)
// Statistics: (formerly in 'SolverStats')
//
, nbRemovedClauses(0),nbReducedClauses(0), nbDL2(0),nbBin(0),nbUn(0) , nbReduceDB(0)
, solves(0), starts(0), decisions(0), rnd_decisions(0), propagations(0),conflicts(0),conflictsRestarts(0),nbstopsrestarts(0),nbstopsrestartssame(0),lastblockatrestart(0)
, dec_vars(0), clauses_literals(0), learnts_literals(0), max_literals(0), tot_literals(0)
, curRestart(1)
, ok (true)
, cla_inc (1)
, var_inc (1)
, watches (WatcherDeleted(ca))
, watchesBin (WatcherDeleted(ca))
, qhead (0)
, simpDB_assigns (-1)
, simpDB_props (0)
, order_heap (VarOrderLt(activity))
, progress_estimate (0)
, remove_satisfied (true)
// Resource constraints:
//
, conflict_budget (-1)
, propagation_budget (-1)
, asynch_interrupt (false)
, incremental(opt_incremental)
, nbVarsInitialFormula(INT32_MAX)
{
MYFLAG=0;
// Initialize only first time. Useful for incremental solving, useless otherwise
lbdQueue.initSize(sizeLBDQueue);
trailQueue.initSize(sizeTrailQueue);
sumLBD = 0;
nbclausesbeforereduce = firstReduceDB;
totalTime4Sat=0;totalTime4Unsat=0;
nbSatCalls=0;nbUnsatCalls=0;
if(certifiedUNSAT) {
if(!strcmp(opt_certified_file_,"NULL")) {
certifiedOutput = fopen("/dev/stdout", "wb");
} else {
certifiedOutput = fopen(opt_certified_file_, "wb");
}
// fprintf(certifiedOutput,"o proof DRUP\n");
}
}
Solver::~Solver()
{
}
/****************************************************************
Set the incremental mode
****************************************************************/
// This function set the incremental mode to true.
// You can add special code for this mode here.
void Solver::setIncrementalMode() {
incremental = true;
}
// Number of variables without selectors
void Solver::initNbInitialVars(int nb) {
nbVarsInitialFormula = nb;
}
//=================================================================================================
// Minor methods:
// Creates a new SAT variable in the solver. If 'decision' is cleared, variable will not be
// used as a decision variable (NOTE! This has effects on the meaning of a SATISFIABLE result).
//
Var Solver::newVar(bool sign, bool dvar)
{
int v = nVars();
watches .init(mkLit(v, false));
watches .init(mkLit(v, true ));
watchesBin .init(mkLit(v, false));
watchesBin .init(mkLit(v, true ));
assigns .push(l_Undef);
vardata .push(mkVarData(CRef_Undef, 0));
//activity .push(0);
activity .push(rnd_init_act ? drand(random_seed) * 0.00001 : 0);
seen .push(0);
permDiff .push(0);
polarity .push(sign);
decision .push();
trail .capacity(v+1);
setDecisionVar(v, dvar);
return v;
}
bool Solver::addClause_(vec<Lit>& ps)
{
assert(decisionLevel() == 0);
if (!ok) return false;
if ( 0 ) {
for ( int i = 0; i < ps.size(); i++ )
printf( "%s%d ", (toInt(ps[i]) & 1) ? "-":"", toInt(ps[i]) >> 1 );
printf( "\n" );
}
// Check if clause is satisfied and remove false/duplicate literals:
sort(ps);
vec<Lit> oc;
oc.clear();
Lit p; int i, j, flag = 0;
if(certifiedUNSAT) {
for (i = j = 0, p = lit_Undef; i < ps.size(); i++) {
oc.push(ps[i]);
if (value(ps[i]) == l_True || ps[i] == ~p || value(ps[i]) == l_False)
flag = 1;
}
}
for (i = j = 0, p = lit_Undef; i < ps.size(); i++)
if (value(ps[i]) == l_True || ps[i] == ~p)
return true;
else if (value(ps[i]) != l_False && ps[i] != p)
ps[j++] = p = ps[i];
ps.shrink(i - j);
if ( 0 ) {
for ( int i = 0; i < ps.size(); i++ )
printf( "%s%d ", (toInt(ps[i]) & 1) ? "-":"", toInt(ps[i]) >> 1 );
printf( "\n" );
}
if (flag && (certifiedUNSAT)) {
for (i = j = 0, p = lit_Undef; i < ps.size(); i++)
fprintf(certifiedOutput, "%i ", (var(ps[i]) + 1) * (-2 * sign(ps[i]) + 1));
fprintf(certifiedOutput, "0\n");
fprintf(certifiedOutput, "d ");
for (i = j = 0, p = lit_Undef; i < oc.size(); i++)
fprintf(certifiedOutput, "%i ", (var(oc[i]) + 1) * (-2 * sign(oc[i]) + 1));
fprintf(certifiedOutput, "0\n");
}
if (ps.size() == 0)
return ok = false;
else if (ps.size() == 1){
uncheckedEnqueue(ps[0]);
return ok = (propagate() == CRef_Undef);
}else{
CRef cr = ca.alloc(ps, false);
clauses.push(cr);
attachClause(cr);
}
return true;
}
void Solver::attachClause(CRef cr) {
const Clause& c = ca[cr];
assert(c.size() > 1);
if(c.size()==2) {
watchesBin[~c[0]].push(Watcher(cr, c[1]));
watchesBin[~c[1]].push(Watcher(cr, c[0]));
} else {
watches[~c[0]].push(Watcher(cr, c[1]));
watches[~c[1]].push(Watcher(cr, c[0]));
}
if (c.learnt()) learnts_literals += c.size();
else clauses_literals += c.size(); }
void Solver::detachClause(CRef cr, bool strict) {
const Clause& c = ca[cr];
assert(c.size() > 1);
if(c.size()==2) {
if (strict){
remove(watchesBin[~c[0]], Watcher(cr, c[1]));
remove(watchesBin[~c[1]], Watcher(cr, c[0]));
}else{
// Lazy detaching: (NOTE! Must clean all watcher lists before garbage collecting this clause)
watchesBin.smudge(~c[0]);
watchesBin.smudge(~c[1]);
}
} else {
if (strict){
remove(watches[~c[0]], Watcher(cr, c[1]));
remove(watches[~c[1]], Watcher(cr, c[0]));
}else{
// Lazy detaching: (NOTE! Must clean all watcher lists before garbage collecting this clause)
watches.smudge(~c[0]);
watches.smudge(~c[1]);
}
}
if (c.learnt()) learnts_literals -= c.size();
else clauses_literals -= c.size(); }
void Solver::removeClause(CRef cr) {
Clause& c = ca[cr];
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);
// Don't leave pointers to free'd memory!
if (locked(c)) vardata[var(c[0])].reason = CRef_Undef;
c.mark(1);
ca.free_(cr);
}
bool Solver::satisfied(const Clause& c) const {
if(incremental) // Check clauses with many selectors is too time consuming
return (value(c[0]) == l_True) || (value(c[1]) == l_True);
// Default mode.
for (int i = 0; i < c.size(); i++)
if (value(c[i]) == l_True)
return true;
return false;
}
/************************************************************
* Compute LBD functions
*************************************************************/
inline unsigned int Solver::computeLBD(const vec<Lit> & lits,int end) {
int nblevels = 0;
MYFLAG++;
if(incremental) { // ----------------- INCREMENTAL MODE
if(end==-1) end = lits.size();
unsigned int nbDone = 0;
for(int i=0;i<lits.size();i++) {
if(nbDone>=end) break;
if(isSelector(var(lits[i]))) continue;
nbDone++;
int l = level(var(lits[i]));
if (permDiff[l] != MYFLAG) {
permDiff[l] = MYFLAG;
nblevels++;
}
}
} else { // -------- DEFAULT MODE. NOT A LOT OF DIFFERENCES... BUT EASIER TO READ
for(int i=0;i<lits.size();i++) {
int l = level(var(lits[i]));
if (permDiff[l] != MYFLAG) {
permDiff[l] = MYFLAG;
nblevels++;
}
}
}
return nblevels;
}
inline unsigned int Solver::computeLBD(const Clause &c) {
int nblevels = 0;
MYFLAG++;
if(incremental) { // ----------------- INCREMENTAL MODE
int nbDone = 0;
for(int i=0;i<c.size();i++) {
if(nbDone>=c.sizeWithoutSelectors()) break;
if(isSelector(var(c[i]))) continue;
nbDone++;
int l = level(var(c[i]));
if (permDiff[l] != MYFLAG) {
permDiff[l] = MYFLAG;
nblevels++;
}
}
} else { // -------- DEFAULT MODE. NOT A LOT OF DIFFERENCES... BUT EASIER TO READ
for(int i=0;i<c.size();i++) {
int l = level(var(c[i]));
if (permDiff[l] != MYFLAG) {
permDiff[l] = MYFLAG;
nblevels++;
}
}
}
return nblevels;
}
/******************************************************************
* Minimisation with binary reolution
******************************************************************/
void Solver::minimisationWithBinaryResolution(vec<Lit> &out_learnt) {
// Find the LBD measure
unsigned int lbd = computeLBD(out_learnt);
Lit p = ~out_learnt[0];
if(lbd<=lbLBDMinimizingClause){
MYFLAG++;
for(int i = 1;i<out_learnt.size();i++) {
permDiff[var(out_learnt[i])] = MYFLAG;
}
vec<Watcher>& wbin = watchesBin[p];
int nb = 0;
for(int k = 0;k<wbin.size();k++) {
Lit imp = wbin[k].blocker;
if(permDiff[var(imp)]==MYFLAG && value(imp)==l_True) {
nb++;
permDiff[var(imp)]= MYFLAG-1;
}
}
int l = out_learnt.size()-1;
if(nb>0) {
nbReducedClauses++;
for(int i = 1;i<out_learnt.size()-nb;i++) {
if(permDiff[var(out_learnt[i])]!=MYFLAG) {
Lit p = out_learnt[l];
out_learnt[l] = out_learnt[i];
out_learnt[i] = p;
l--;i--;
}
}
out_learnt.shrink(nb);
}
}
}
// Revert to the state at given level (keeping all assignment at 'level' but not beyond).
//
void Solver::cancelUntil(int level) {
if (decisionLevel() > level){
for (int c = trail.size()-1; c >= trail_lim[level]; c--){
Var x = var(trail[c]);
assigns [x] = l_Undef;
if (phase_saving > 1 || ((phase_saving == 1) && c > trail_lim.last()))
polarity[x] = sign(trail[c]);
insertVarOrder(x); }
qhead = trail_lim[level];
trail.shrink(trail.size() - trail_lim[level]);
trail_lim.shrink(trail_lim.size() - level);
}
}
//=================================================================================================
// Major methods:
Lit Solver::pickBranchLit()
{
Var next = var_Undef;
// Random decision:
if (drand(random_seed) < random_var_freq && !order_heap.empty()){
next = order_heap[irand(random_seed,order_heap.size())];
if (value(next) == l_Undef && decision[next])
rnd_decisions++; }
// Activity based decision:
while (next == var_Undef || value(next) != l_Undef || !decision[next])
if (order_heap.empty()){
next = var_Undef;
break;
}else
next = order_heap.removeMin();
return next == var_Undef ? lit_Undef : mkLit(next, rnd_pol ? drand(random_seed) < 0.5 : (polarity[next] != 0));
}
/*_________________________________________________________________________________________________
|
| analyze : (confl : Clause*) (out_learnt : vec<Lit>&) (out_btlevel : int&) -> [void]
|
| Description:
| Analyze conflict and produce a reason clause.
|
| Pre-conditions:
| * 'out_learnt' is assumed to be cleared.
| * Current decision level must be greater than root level.
|
| Post-conditions:
| * 'out_learnt[0]' is the asserting literal at level 'out_btlevel'.
| * If out_learnt.size() > 1 then 'out_learnt[1]' has the greatest decision level of the
| rest of literals. There may be others from the same level though.
|
|________________________________________________________________________________________________@*/
void Solver::analyze(CRef confl, vec<Lit>& out_learnt,vec<Lit>&selectors, int& out_btlevel,unsigned int &lbd,unsigned int &szWithoutSelectors)
{
int pathC = 0;
Lit p = lit_Undef;
// Generate conflict clause:
//
out_learnt.push(); // (leave room for the asserting literal)
int index = trail.size() - 1;
do{
assert(confl != CRef_Undef); // (otherwise should be UIP)
Clause& c = ca[confl];
// Special case for binary clauses
// The first one has to be SAT
if( p != lit_Undef && c.size()==2 && value(c[0])==l_False) {
assert(value(c[1])==l_True);
Lit tmp = c[0];
c[0] = c[1], c[1] = tmp;
}
if (c.learnt())
claBumpActivity(c);
#ifdef DYNAMICNBLEVEL
// DYNAMIC NBLEVEL trick (see competition'09 companion paper)
if(c.learnt() && c.lbd()>2) {
unsigned int nblevels = computeLBD(c);
if(nblevels+1<c.lbd() ) { // improve the LBD
if(c.lbd()<=lbLBDFrozenClause) {
c.setCanBeDel(false);
}
// seems to be interesting : keep it for the next round
c.setLBD(nblevels); // Update it
}
}
#endif
for (int j = (p == lit_Undef) ? 0 : 1; j < c.size(); j++){
Lit q = c[j];
if (!seen[var(q)] && level(var(q)) > 0){
if(!isSelector(var(q)))
varBumpActivity(var(q));
seen[var(q)] = 1;
if (level(var(q)) >= decisionLevel()) {
pathC++;
#ifdef UPDATEVARACTIVITY
// UPDATEVARACTIVITY trick (see competition'09 companion paper)
if(!isSelector(var(q)) && (reason(var(q))!= CRef_Undef) && ca[reason(var(q))].learnt())
lastDecisionLevel.push(q);
#endif
} else {
if(isSelector(var(q))) {
assert(value(q) == l_False);
selectors.push(q);
} else
out_learnt.push(q);
}
}
}
// Select next clause to look at:
while (!seen[var(trail[index--])]);
p = trail[index+1];
confl = reason(var(p));
seen[var(p)] = 0;
pathC--;
}while (pathC > 0);
out_learnt[0] = ~p;
// Simplify conflict clause:
//
int i, j;
for(i = 0;i<selectors.size();i++)
out_learnt.push(selectors[i]);
out_learnt.copyTo(analyze_toclear);
if (ccmin_mode == 2){
uint32_t abstract_level = 0;
for (i = 1; i < out_learnt.size(); i++)
abstract_level |= abstractLevel(var(out_learnt[i])); // (maintain an abstraction of levels involved in conflict)
for (i = j = 1; i < out_learnt.size(); i++)
if (reason(var(out_learnt[i])) == CRef_Undef || !litRedundant(out_learnt[i], abstract_level))
out_learnt[j++] = out_learnt[i];
}else if (ccmin_mode == 1){
for (i = j = 1; i < out_learnt.size(); i++){
Var x = var(out_learnt[i]);
if (reason(x) == CRef_Undef)
out_learnt[j++] = out_learnt[i];
else{
Clause& c = ca[reason(var(out_learnt[i]))];
// Thanks to Siert Wieringa for this bug fix!
for (int k = ((c.size()==2) ? 0:1); k < c.size(); k++)
if (!seen[var(c[k])] && level(var(c[k])) > 0){
out_learnt[j++] = out_learnt[i];
break; }
}
}
}else
i = j = out_learnt.size();
max_literals += out_learnt.size();
out_learnt.shrink(i - j);
tot_literals += out_learnt.size();
/* ***************************************
Minimisation with binary clauses of the asserting clause
First of all : we look for small clauses
Then, we reduce clauses with small LBD.
Otherwise, this can be useless
*/
if(!incremental && out_learnt.size()<=lbSizeMinimizingClause) {
minimisationWithBinaryResolution(out_learnt);
}
// Find correct backtrack level:
//
if (out_learnt.size() == 1)
out_btlevel = 0;
else{
int max_i = 1;
// Find the first literal assigned at the next-highest level:
for (int i = 2; i < out_learnt.size(); i++)
if (level(var(out_learnt[i])) > level(var(out_learnt[max_i])))
max_i = i;
// Swap-in this literal at index 1:
Lit p = out_learnt[max_i];
out_learnt[max_i] = out_learnt[1];
out_learnt[1] = p;
out_btlevel = level(var(p));
}
// Compute the size of the clause without selectors (incremental mode)
if(incremental) {
szWithoutSelectors = 0;
for(int i=0;i<out_learnt.size();i++) {
if(!isSelector(var((out_learnt[i])))) szWithoutSelectors++;
else if(i>0) break;
}
} else
szWithoutSelectors = out_learnt.size();
// Compute LBD
lbd = computeLBD(out_learnt,out_learnt.size()-selectors.size());
#ifdef UPDATEVARACTIVITY
// UPDATEVARACTIVITY trick (see competition'09 companion paper)
if(lastDecisionLevel.size()>0) {
for(int i = 0;i<lastDecisionLevel.size();i++) {
if(ca[reason(var(lastDecisionLevel[i]))].lbd()<lbd)
varBumpActivity(var(lastDecisionLevel[i]));
}
lastDecisionLevel.clear();
}
#endif
for (j = 0; j < analyze_toclear.size(); j++) seen[var(analyze_toclear[j])] = 0; // ('seen[]' is now cleared)
for(j = 0 ; j<selectors.size() ; j++) seen[var(selectors[j])] = 0;
}
// Check if 'p' can be removed. 'abstract_levels' is used to abort early if the algorithm is
// visiting literals at levels that cannot be removed later.
bool Solver::litRedundant(Lit p, uint32_t abstract_levels)
{
analyze_stack.clear(); analyze_stack.push(p);
int top = analyze_toclear.size();
while (analyze_stack.size() > 0){
assert(reason(var(analyze_stack.last())) != CRef_Undef);
Clause& c = ca[reason(var(analyze_stack.last()))]; analyze_stack.pop();
if(c.size()==2 && value(c[0])==l_False) {
assert(value(c[1])==l_True);
Lit tmp = c[0];
c[0] = c[1], c[1] = tmp;
}
for (int i = 1; i < c.size(); i++){
Lit p = c[i];
if (!seen[var(p)] && level(var(p)) > 0){
if (reason(var(p)) != CRef_Undef && (abstractLevel(var(p)) & abstract_levels) != 0){
seen[var(p)] = 1;
analyze_stack.push(p);
analyze_toclear.push(p);
}else{
for (int j = top; j < analyze_toclear.size(); j++)
seen[var(analyze_toclear[j])] = 0;
analyze_toclear.shrink(analyze_toclear.size() - top);
return false;
}
}
}
}
return true;
}
/*_________________________________________________________________________________________________
|
| analyzeFinal : (p : Lit) -> [void]
|
| Description:
| Specialized analysis procedure to express the final conflict in terms of assumptions.
| Calculates the (possibly empty) set of assumptions that led to the assignment of 'p', and
| stores the result in 'out_conflict'.
|________________________________________________________________________________________________@*/
void Solver::analyzeFinal(Lit p, vec<Lit>& out_conflict)
{
out_conflict.clear();
out_conflict.push(p);
if (decisionLevel() == 0)
return;
seen[var(p)] = 1;
for (int i = trail.size()-1; i >= trail_lim[0]; i--){
Var x = var(trail[i]);
if (seen[x]){
if (reason(x) == CRef_Undef){
assert(level(x) > 0);
out_conflict.push(~trail[i]);
}else{
Clause& c = ca[reason(x)];
// for (int j = 1; j < c.size(); j++) Minisat (glucose 2.0) loop
// Bug in case of assumptions due to special data structures for Binary.
// Many thanks to Sam Bayless (sbayless@cs.ubc.ca) for discover this bug.
for (int j = ((c.size()==2) ? 0:1); j < c.size(); j++)
if (level(var(c[j])) > 0)
seen[var(c[j])] = 1;
}
seen[x] = 0;
}
}
seen[var(p)] = 0;
}
void Solver::uncheckedEnqueue(Lit p, CRef from)
{
assert(value(p) == l_Undef);
assigns[var(p)] = lbool(!sign(p));
vardata[var(p)] = mkVarData(from, decisionLevel());
trail.push_(p);
}
/*_________________________________________________________________________________________________
|
| propagate : [void] -> [Clause*]
|
| Description:
| Propagates all enqueued facts. If a conflict arises, the conflicting clause is returned,
| otherwise CRef_Undef.
|
| Post-conditions:
| * the propagation queue is empty, even if there was a conflict.
|________________________________________________________________________________________________@*/
CRef Solver::propagate()
{
CRef confl = CRef_Undef;
int num_props = 0;
watches.cleanAll();
watchesBin.cleanAll();
while (qhead < trail.size()){
Lit p = trail[qhead++]; // 'p' is enqueued fact to propagate.
vec<Watcher>& ws = watches[p];
Watcher *i, *j, *end;
num_props++;
// First, Propagate binary clauses
vec<Watcher>& wbin = watchesBin[p];
for(int k = 0;k<wbin.size();k++) {
Lit imp = wbin[k].blocker;
if(value(imp) == l_False) {
return wbin[k].cref;
}
if(value(imp) == l_Undef) {
uncheckedEnqueue(imp,wbin[k].cref);
}
}
for (i = j = (Watcher*)ws, end = i + ws.size(); i != end;){
// Try to avoid inspecting the clause:
Lit blocker = i->blocker;
if (value(blocker) == l_True){
*j++ = *i++; continue; }
// Make sure the false literal is data[1]:
CRef cr = i->cref;
Clause& c = ca[cr];
Lit false_lit = ~p;
if (c[0] == false_lit)
c[0] = c[1], c[1] = false_lit;
assert(c[1] == false_lit);
i++;
// If 0th watch is true, then clause is already satisfied.
Lit first = c[0];
Watcher w = Watcher(cr, first);
if (first != blocker && value(first) == l_True){
*j++ = w; continue; }
// Look for new watch:
if(incremental) { // ----------------- INCREMENTAL MODE
int choosenPos = -1;
for (int k = 2; k < c.size(); k++) {
if (value(c[k]) != l_False){
if(decisionLevel()>assumptions.size()) {
choosenPos = k;
break;
} else {
choosenPos = k;
if(value(c[k])==l_True || !isSelector(var(c[k]))) {
break;
}
}
}
}
if(choosenPos!=-1) {
c[1] = c[choosenPos]; c[choosenPos] = false_lit;
watches[~c[1]].push(w);
goto NextClause; }
} else { // ----------------- DEFAULT MODE (NOT INCREMENTAL)
for (int k = 2; k < c.size(); k++) {
if (value(c[k]) != l_False){
c[1] = c[k]; c[k] = false_lit;
watches[~c[1]].push(w);
goto NextClause; }
}
}
// Did not find watch -- clause is unit under assignment:
*j++ = w;
if (value(first) == l_False){
confl = cr;
qhead = trail.size();
// Copy the remaining watches:
while (i < end)
*j++ = *i++;
}else {
uncheckedEnqueue(first, cr);
}
NextClause:;
}
ws.shrink(i - j);
}
propagations += num_props;
simpDB_props -= num_props;
return confl;
}
/*_________________________________________________________________________________________________
|
| reduceDB : () -> [void]
|
| Description:
| Remove half of the learnt clauses, minus the clauses locked by the current assignment. Locked
| clauses are clauses that are reason to some assignment. Binary clauses are never removed.
|________________________________________________________________________________________________@*/
struct reduceDB_lt {
ClauseAllocator& ca;
reduceDB_lt(ClauseAllocator& ca_) : ca(ca_) {}
bool operator () (CRef x, CRef y) {
// Main criteria... Like in MiniSat we keep all binary clauses
if(ca[x].size()> 2 && ca[y].size()==2) return 1;
if(ca[y].size()> 2 && ca[x].size()==2) return 0;
if(ca[x].size()==2 && ca[y].size()==2) return 0;
// Second one based on literal block distance
if(ca[x].lbd()> ca[y].lbd()) return 1;
if(ca[x].lbd()< ca[y].lbd()) return 0;
// Finally we can use old activity or size, we choose the last one
return ca[x].activity() < ca[y].activity();
//return x->size() < y->size();
//return ca[x].size() > 2 && (ca[y].size() == 2 || ca[x].activity() < ca[y].activity()); }
}
};
void Solver::reduceDB()
{
int i, j;
nbReduceDB++;
sort(learnts, reduceDB_lt(ca));
// We have a lot of "good" clauses, it is difficult to compare them. Keep more !
if(ca[learnts[learnts.size() / RATIOREMOVECLAUSES]].lbd()<=3) nbclausesbeforereduce +=specialIncReduceDB;
// Useless :-)
if(ca[learnts.last()].lbd()<=5) nbclausesbeforereduce +=specialIncReduceDB;
// Don't delete binary or locked clauses. From the rest, delete clauses from the first half
// Keep clauses which seem to be usefull (their lbd was reduce during this sequence)
int limit = learnts.size() / 2;
for (i = j = 0; i < learnts.size(); i++){
Clause& c = ca[learnts[i]];
if (c.lbd()>2 && c.size() > 2 && c.canBeDel() && !locked(c) && (i < limit)) {
removeClause(learnts[i]);
nbRemovedClauses++;
}
else {
if(!c.canBeDel()) limit++; //we keep c, so we can delete an other clause
c.setCanBeDel(true); // At the next step, c can be delete
learnts[j++] = learnts[i];
}
}
learnts.shrink(i - j);
checkGarbage();
}
void Solver::removeSatisfied(vec<CRef>& cs)
{
int i, j;
for (i = j = 0; i < cs.size(); i++){
Clause& c = ca[cs[i]];
if (satisfied(c))
removeClause(cs[i]);
else
cs[j++] = cs[i];
}
cs.shrink(i - j);
}
void Solver::rebuildOrderHeap()
{
vec<Var> vs;
for (Var v = 0; v < nVars(); v++)
if (decision[v] && value(v) == l_Undef)
vs.push(v);
order_heap.build(vs);
}
/*_________________________________________________________________________________________________
|
| simplify : [void] -> [bool]
|
| Description:
| Simplify the clause database according to the current top-level assigment. Currently, the only
| thing done here is the removal of satisfied clauses, but more things can be put here.
|________________________________________________________________________________________________@*/
bool Solver::simplify()
{
assert(decisionLevel() == 0);
if (!ok || propagate() != CRef_Undef)
return ok = false;
if (nAssigns() == simpDB_assigns || (simpDB_props > 0))
return true;
// Remove satisfied clauses:
removeSatisfied(learnts);
if (remove_satisfied) // Can be turned off.
removeSatisfied(clauses);
checkGarbage();
rebuildOrderHeap();
simpDB_assigns = nAssigns();
simpDB_props = clauses_literals + learnts_literals; // (shouldn't depend on stats really, but it will do for now)
return true;
}
/*_________________________________________________________________________________________________
|
| search : (nof_conflicts : int) (params : const SearchParams&) -> [lbool]
|
| Description:
| Search for a model the specified number of conflicts.
| NOTE! Use negative value for 'nof_conflicts' indicate infinity.
|
| Output:
| 'l_True' if a partial assigment that is consistent with respect to the clauseset is found. If
| all variables are decision variables, this means that the clause set is satisfiable. 'l_False'
| if the clause set is unsatisfiable. 'l_Undef' if the bound on number of conflicts is reached.
|________________________________________________________________________________________________@*/
lbool Solver::search(int nof_conflicts)
{
assert(ok);
int backtrack_level;
int conflictC = 0;
vec<Lit> learnt_clause,selectors;
unsigned int nblevels,szWoutSelectors;
bool blocked=false;
starts++;
for (;;){
CRef confl = propagate();
if (confl != CRef_Undef){
// CONFLICT
conflicts++; conflictC++;conflictsRestarts++;
if(conflicts%5000==0 && var_decay<0.95)
var_decay += 0.01;
if (verbosity >= 1 && conflicts%verbEveryConflicts==0){
printf("c | %8d %7d %5d | %7d %8d %8d | %5d %8d %6d %8d | %6.3f %% |\n",
(int)starts,(int)nbstopsrestarts, (int)(conflicts/starts),
(int)dec_vars - (trail_lim.size() == 0 ? trail.size() : trail_lim[0]), nClauses(), (int)clauses_literals,
(int)nbReduceDB, nLearnts(), (int)nbDL2,(int)nbRemovedClauses, progressEstimate()*100);
}
if (decisionLevel() == 0) {
return l_False;
}
trailQueue.push(trail.size());
// BLOCK RESTART (CP 2012 paper)
if( conflictsRestarts>LOWER_BOUND_FOR_BLOCKING_RESTART && lbdQueue.isvalid() && trail.size()>R*trailQueue.getavg()) {
lbdQueue.fastclear();
nbstopsrestarts++;
if(!blocked) {lastblockatrestart=starts;nbstopsrestartssame++;blocked=true;}
}
learnt_clause.clear();
selectors.clear();
analyze(confl, learnt_clause, selectors,backtrack_level,nblevels,szWoutSelectors);
lbdQueue.push(nblevels);
sumLBD += nblevels;
cancelUntil(backtrack_level);
if (certifiedUNSAT) {
for (int i = 0; i < learnt_clause.size(); i++)
fprintf(certifiedOutput, "%i " , (var(learnt_clause[i]) + 1) *
(-2 * sign(learnt_clause[i]) + 1) );
fprintf(certifiedOutput, "0\n");
}
if (learnt_clause.size() == 1){
uncheckedEnqueue(learnt_clause[0]);nbUn++;
}else{
CRef cr = ca.alloc(learnt_clause, true);
ca[cr].setLBD(nblevels);
ca[cr].setSizeWithoutSelectors(szWoutSelectors);
if(nblevels<=2) nbDL2++; // stats
if(ca[cr].size()==2) nbBin++; // stats
learnts.push(cr);
attachClause(cr);
claBumpActivity(ca[cr]);
uncheckedEnqueue(learnt_clause[0], cr);
}
varDecayActivity();
claDecayActivity();
}else{
// Our dynamic restart, see the SAT09 competition compagnion paper
if ( (conflictsRestarts && lbdQueue.isvalid() && lbdQueue.getavg()*K > sumLBD/conflictsRestarts) || (pstop && *pstop) ) {
lbdQueue.fastclear();
progress_estimate = progressEstimate();
int bt = 0;
if(incremental) { // DO NOT BACKTRACK UNTIL 0.. USELESS
bt = (decisionLevel()<assumptions.size()) ? decisionLevel() : assumptions.size();
}
cancelUntil(bt);
return l_Undef;
}
// Simplify the set of problem clauses:
if (decisionLevel() == 0 && !simplify()) {
return l_False;
}
// Perform clause database reduction !
if(conflicts>=curRestart* nbclausesbeforereduce)
{
assert(learnts.size()>0);
curRestart = (conflicts/ nbclausesbeforereduce)+1;
reduceDB();
nbclausesbeforereduce += incReduceDB;
}
Lit next = lit_Undef;
while (decisionLevel() < assumptions.size()){
// Perform user provided assumption:
Lit p = assumptions[decisionLevel()];
if (value(p) == l_True){
// Dummy decision level:
newDecisionLevel();
}else if (value(p) == l_False){
analyzeFinal(~p, conflict);
return l_False;
}else{
next = p;
break;
}
}
if (next == lit_Undef){
// New variable decision:
decisions++;
next = pickBranchLit();
if (next == lit_Undef){
//printf("c last restart ## conflicts : %d %d \n",conflictC,decisionLevel());
// Model found:
return l_True;
}
}
// Increase decision level and enqueue 'next'
newDecisionLevel();
uncheckedEnqueue(next);
}
}
}
double Solver::progressEstimate() const
{
double progress = 0;
double F = 1.0 / nVars();
for (int i = 0; i <= decisionLevel(); i++){
int beg = i == 0 ? 0 : trail_lim[i - 1];
int end = i == decisionLevel() ? trail.size() : trail_lim[i];
progress += pow(F, i) * (end - beg);
}
return progress / nVars();
}
void Solver::printIncrementalStats() {
printf("c---------- Glucose Stats -------------------------\n");
printf("c restarts : %ld\n", starts);
printf("c nb ReduceDB : %ld\n", nbReduceDB);
printf("c nb removed Clauses : %ld\n", nbRemovedClauses);
printf("c nb learnts DL2 : %ld\n", nbDL2);
printf("c nb learnts size 2 : %ld\n", nbBin);
printf("c nb learnts size 1 : %ld\n", nbUn);
printf("c conflicts : %ld\n", conflicts);
printf("c decisions : %ld\n", decisions);
printf("c propagations : %ld\n", propagations);
printf("c SAT Calls : %d in %g seconds\n", nbSatCalls, totalTime4Sat);
printf("c UNSAT Calls : %d in %g seconds\n", nbUnsatCalls, totalTime4Unsat);
printf("c--------------------------------------------------\n");
}
// NOTE: assumptions passed in member-variable 'assumptions'.
lbool Solver::solve_()
{
if(incremental && certifiedUNSAT) {
printf("Can not use incremental and certified unsat in the same time\n");
exit(-1);
}
model.clear();
conflict.clear();
if (!ok) return l_False;
double curTime = cpuTime();
solves++;
lbool status = l_Undef;
if(!incremental && verbosity>=1) {
printf("c ========================================[ MAGIC CONSTANTS ]==============================================\n");
printf("c | Constants are supposed to work well together :-) |\n");
printf("c | however, if you find better choices, please let us known... |\n");
printf("c |-------------------------------------------------------------------------------------------------------|\n");
printf("c | | | |\n");
printf("c | - Restarts: | - Reduce Clause DB: | - Minimize Asserting: |\n");
printf("c | * LBD Queue : %6d | * First : %6d | * size < %3d |\n",lbdQueue.maxSize(),nbclausesbeforereduce,lbSizeMinimizingClause);
printf("c | * Trail Queue : %6d | * Inc : %6d | * lbd < %3d |\n",trailQueue.maxSize(),incReduceDB,lbLBDMinimizingClause);
printf("c | * K : %6.2f | * Special : %6d | |\n",K,specialIncReduceDB);
printf("c | * R : %6.2f | * Protected : (lbd)< %2d | |\n",R,lbLBDFrozenClause);
printf("c | | | |\n");
printf("c ==================================[ Search Statistics (every %6d conflicts) ]=========================\n",verbEveryConflicts);
printf("c | |\n");
printf("c | RESTARTS | ORIGINAL | LEARNT | Progress |\n");
printf("c | NB Blocked Avg Cfc | Vars Clauses Literals | Red Learnts LBD2 Removed | |\n");
printf("c =========================================================================================================\n");
}
// Search:
int curr_restarts = 0;
while (status == l_Undef){
status = search(0); // the parameter is useless in glucose, kept to allow modifications
if (!withinBudget() || terminate_search_early || (pstop && *pstop)) break;
if (nRuntimeLimit && Abc_Clock() > nRuntimeLimit) break;
curr_restarts++;
}
if (!incremental && verbosity >= 1)
printf("c =========================================================================================================\n");
if (certifiedUNSAT){ // Want certified output
if (status == l_False)
fprintf(certifiedOutput, "0\n");
fclose(certifiedOutput);
}
if (status == l_True){
// Extend & copy model:
model.growTo(nVars());
for (int i = 0; i < nVars(); i++) model[i] = value(i);
}else if (status == l_False && conflict.size() == 0)
ok = false;
cancelUntil(0);
double finalTime = cpuTime();
if(status==l_True) {
nbSatCalls++;
totalTime4Sat +=(finalTime-curTime);
}
if(status==l_False) {
nbUnsatCalls++;
totalTime4Unsat +=(finalTime-curTime);
}
// ABC callback
if (pCnfFunc && !terminate_search_early) {// hack to avoid calling callback twise if the solver was terminated early
int * pCex = NULL;
int message = (status == l_True ? 1 : status == l_False ? 0 : -1);
if (status == l_True) {
pCex = new int[nVars()];
for (int i = 0; i < nVars(); i++)
pCex[i] = (model[i] == l_True);
}
int callback_result = pCnfFunc(pCnfMan, message, pCex);
assert(callback_result == 0);
}
else if (pCnfFunc)
terminate_search_early = false; // for next run
return status;
}
//=================================================================================================
// Writing CNF to DIMACS:
//
// FIXME: this needs to be rewritten completely.
static Var mapVar(Var x, vec<Var>& map, Var& max)
{
if (map.size() <= x || map[x] == -1){
map.growTo(x+1, -1);
map[x] = max++;
}
return map[x];
}
void Solver::toDimacs(FILE* f, Clause& c, vec<Var>& map, Var& max)
{
if (satisfied(c)) return;
for (int i = 0; i < c.size(); i++)
if (value(c[i]) != l_False)
fprintf(f, "%s%d ", sign(c[i]) ? "-" : "", mapVar(var(c[i]), map, max)+1);
fprintf(f, "0\n");
}
void Solver::toDimacs(const char *file, const vec<Lit>& assumps)
{
FILE* f = fopen(file, "wr");
if (f == NULL)
fprintf(stderr, "could not open file %s\n", file), exit(1);
toDimacs(f, assumps);
fclose(f);
}
void Solver::toDimacs(FILE* f, const vec<Lit>& assumps)
{
// Handle case when solver is in contradictory state:
if (!ok){
fprintf(f, "p cnf 1 2\n1 0\n-1 0\n");
return; }
vec<Var> map; Var max = 0;
// Cannot use removeClauses here because it is not safe
// to deallocate them at this point. Could be improved.
int i, cnt = 0;
for (i = 0; i < clauses.size(); i++)
if (!satisfied(ca[clauses[i]]))
cnt++;
for (i = 0; i < clauses.size(); i++)
if (!satisfied(ca[clauses[i]])){
Clause& c = ca[clauses[i]];
for (int j = 0; j < c.size(); j++)
if (value(c[j]) != l_False)
mapVar(var(c[j]), map, max);
}
// Assumptions are added as unit clauses:
cnt += assumptions.size();
fprintf(f, "p cnf %d %d\n", max, cnt);
for (i = 0; i < assumptions.size(); i++){
assert(value(assumptions[i]) != l_False);
fprintf(f, "%s%d 0\n", sign(assumptions[i]) ? "-" : "", mapVar(var(assumptions[i]), map, max)+1);
}
for (i = 0; i < clauses.size(); i++)
toDimacs(f, ca[clauses[i]], map, max);
if (verbosity > 0)
printf("Wrote %d clauses with %d variables.\n", cnt, max);
}
//=================================================================================================
// Garbage Collection methods:
void Solver::relocAll(ClauseAllocator& to)
{
int v, s, i, j;
// All watchers:
//
// for (int i = 0; i < watches.size(); i++)
watches.cleanAll();
watchesBin.cleanAll();
for (v = 0; v < nVars(); v++)
for (s = 0; s < 2; s++){
Lit p = mkLit(v, s != 0);
// printf(" >>> RELOCING: %s%d\n", sign(p)?"-":"", var(p)+1);
vec<Watcher>& ws = watches[p];
for (j = 0; j < ws.size(); j++)
ca.reloc(ws[j].cref, to);
vec<Watcher>& ws2 = watchesBin[p];
for (j = 0; j < ws2.size(); j++)
ca.reloc(ws2[j].cref, to);
}
// All reasons:
//
for (i = 0; i < trail.size(); i++){
Var v = var(trail[i]);
if (reason(v) != CRef_Undef && (ca[reason(v)].reloced() || locked(ca[reason(v)])))
ca.reloc(vardata[v].reason, to);
}
// All learnt:
//
for (i = 0; i < learnts.size(); i++)
ca.reloc(learnts[i], to);
// All original:
//
for (i = 0; i < clauses.size(); i++)
ca.reloc(clauses[i], to);
}
void Solver::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());
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);
}
void Solver::reset()
{
// Reset everything
ok = true;
K = (double)opt_K;
R = (double)opt_R;
firstReduceDB = opt_first_reduce_db;
var_decay = (double)opt_var_decay;
//max_var_decay = opt_max_var_decay;
solves = starts = decisions = propagations = conflicts = conflictsRestarts = 0;
curRestart = 1;
cla_inc = var_inc = 1;
watches.clear(false); // We don't free the memory, new calls should be of the same size order.
watchesBin.clear(false);
//unaryWatches.clear(false);
qhead = 0;
simpDB_assigns = -1;
simpDB_props = 0;
order_heap.clear(false);
progress_estimate = 0;
//lastLearntClause = CRef_Undef;
conflict_budget = -1;
propagation_budget = -1;
nbVarsInitialFormula = INT32_MAX;
totalTime4Sat = 0.;
totalTime4Unsat = 0.;
nbSatCalls = nbUnsatCalls = 0;
MYFLAG = 0;
lbdQueue.clear(false);
lbdQueue.initSize(sizeLBDQueue);
trailQueue.clear(false);
trailQueue.initSize(sizeTrailQueue);
sumLBD = 0;
nbclausesbeforereduce = firstReduceDB;
//stats.clear();
//stats.growTo(coreStatsSize, 0);
clauses.clear(false);
learnts.clear(false);
//permanentLearnts.clear(false);
//unaryWatchedClauses.clear(false);
model.clear(false);
conflict.clear(false);
activity.clear(false);
assigns.clear(false);
polarity.clear(false);
//forceUNSAT.clear(false);
decision.clear(false);
trail.clear(false);
nbpos.clear(false);
trail_lim.clear(false);
vardata.clear(false);
assumptions.clear(false);
permDiff.clear(false);
lastDecisionLevel.clear(false);
ca.clear();
seen.clear(false);
analyze_stack.clear(false);
analyze_toclear.clear(false);
add_tmp.clear(false);
assumptionPositions.clear(false);
initialPositions.clear(false);
}
ABC_NAMESPACE_IMPL_END
src/sat/glucose2/Heap.h 0 → 100644
/******************************************************************************************[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/glucose2/Vec.h"
ABC_NAMESPACE_CXX_HEADER_START
namespace Gluco2 {
//=================================================================================================
// 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);
}
};
//=================================================================================================
}
ABC_NAMESPACE_CXX_HEADER_END
#endif
src/sat/glucose2/IntTypes.h 0 → 100644
/**************************************************************************************[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
//=================================================================================================
#include <misc/util/abc_namespaces.h>
#endif
src/sat/glucose2/Map.h 0 → 100644
/*******************************************************************************************[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/glucose2/IntTypes.h"
#include "sat/glucose2/Vec.h"
ABC_NAMESPACE_CXX_HEADER_START
namespace Gluco2 {
//=================================================================================================
// 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]; }
};
//=================================================================================================
}
ABC_NAMESPACE_CXX_HEADER_END
#endif
src/sat/glucose2/Options.h 0 → 100644
/***************************************************************************************[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/glucose2/IntTypes.h"
#include "sat/glucose2/Vec.h"
#include "sat/glucose2/ParseUtils.h"
ABC_NAMESPACE_CXX_HEADER_START
namespace Gluco2 {
//==================================================================================================
// 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", (int)range.begin);
fprintf(stderr, " .. ");
if (range.end == INT64_MAX)
fprintf(stderr, "imax");
else
fprintf(stderr, "%4d", (int)range.end);
fprintf(stderr, "] (default: %d)\n", (int)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");
}
}
};
//=================================================================================================
}
ABC_NAMESPACE_CXX_HEADER_END
#endif
src/sat/glucose2/Options2.cpp 0 → 100644
/**************************************************************************************[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/glucose2/Sort.h"
#include "sat/glucose2/Options.h"
#include "sat/glucose2/ParseUtils.h"
ABC_NAMESPACE_IMPL_START
using namespace Gluco2;
void Gluco2::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 Gluco2::setUsageHelp (const char* str){ Option::getUsageString() = str; }
void Gluco2::setHelpPrefixStr (const char* str){ Option::getHelpPrefixString() = str; }
void Gluco2::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);
}
ABC_NAMESPACE_IMPL_END
src/sat/glucose2/ParseUtils.h 0 → 100644
/************************************************************************************[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 Glucose2_ParseUtils_h
#define Glucose2_ParseUtils_h
#include <stdlib.h>
#include <stdio.h>
#include <math.h>
#include "misc/zlib/zlib.h"
ABC_NAMESPACE_CXX_HEADER_START
namespace Gluco2 {
//-------------------------------------------------------------------------------------------------
// 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; }
//=================================================================================================
}
ABC_NAMESPACE_CXX_HEADER_END
#endif
src/sat/glucose2/Queue.h 0 → 100644
/*****************************************************************************************[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/glucose2/Vec.h"
ABC_NAMESPACE_CXX_HEADER_START
namespace Gluco2 {
//=================================================================================================
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);
}
}
};
//=================================================================================================
}
ABC_NAMESPACE_CXX_HEADER_END
#endif
src/sat/glucose2/SimpSolver.h 0 → 100644
/************************************************************************************[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/glucose2/Queue.h"
#include "sat/glucose2/Solver.h"
ABC_NAMESPACE_CXX_HEADER_START
namespace Gluco2 {
//=================================================================================================
class SimpSolver : public Solver {
public:
// Constructor/Destructor:
//
SimpSolver();
~SimpSolver();
// Problem specification:
//
Var newVar (bool polarity = true, bool dvar = true);
void addVar (Var v);
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 reset();
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;
int eliminated_clauses;
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]; }
inline bool SimpSolver::isEliminated (Var v) const { return eliminated.size() > 0 ? eliminated[v] != 0 : 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); }
inline void SimpSolver::addVar(Var v) { while (v >= nVars()) newVar(); }
//=================================================================================================
}
ABC_NAMESPACE_CXX_HEADER_END
#endif
src/sat/glucose2/SimpSolver2.cpp 0 → 100644
/***********************************************************************************[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/glucose2/Sort.h"
#include "sat/glucose2/SimpSolver.h"
#include "sat/glucose2/System.h"
ABC_NAMESPACE_IMPL_START
using namespace Gluco2;
//=================================================================================================
// 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)
, eliminated_clauses (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, j;
for (i = 0; i < qs.size(); i++){
if (var(qs[i]) != v){
for (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));
eliminated_clauses += neg.size();
}else{
for (i = 0; i < pos.size(); i++)
mkElimClause(elimclauses, v, ca[pos[i]]);
mkElimClause(elimclauses, ~mkLit(v));
eliminated_clauses += pos.size();
}
// 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)
{
//abctime clk = Abc_Clock();
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);
}
void SimpSolver::reset()
{
Solver::reset();
grow = opt_grow;
asymm_lits = eliminated_vars = bwdsub_assigns = n_touched = 0;
elimclauses.clear(false);
touched.clear(false);
occurs.clear(false);
n_occ.clear(false);
elim_heap.clear(false);
subsumption_queue.clear(false);
frozen.clear(false);
eliminated.clear(false);
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;
}
ABC_NAMESPACE_IMPL_END
src/sat/glucose2/Solver.h 0 → 100644
/****************************************************************************************[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/glucose2/Vec.h"
#include "sat/glucose2/Heap.h"
#include "sat/glucose2/Alg.h"
#include "sat/glucose2/Options.h"
#include "sat/glucose2/SolverTypes.h"
#include "sat/glucose2/BoundedQueue.h"
#include "sat/glucose2/Constants.h"
ABC_NAMESPACE_CXX_HEADER_START
namespace Gluco2 {
//=================================================================================================
// 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
uint64_t nRuntimeLimit; // runtime limit
vec<int> user_vec;
vec<Lit> user_lits;
// Problem specification:
//
Var newVar (bool polarity = true, bool dvar = true); // Add a new variable with parameters specifying variable mode.
void addVar (Var v); // Add enough variables to make sure there is variable v.
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;
int * getCex () 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 reset();
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 int * Solver::getCex () const { return NULL; }
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); }
inline void Solver::addVar(Var v) { while (v >= nVars()) newVar(); }
//=================================================================================================
// 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(" ");
}
}
}
//=================================================================================================
}
ABC_NAMESPACE_CXX_HEADER_END
#endif
src/sat/glucose2/SolverTypes.h 0 → 100644
/***********************************************************************************[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/glucose2/IntTypes.h"
#include "sat/glucose2/Alg.h"
#include "sat/glucose2/Vec.h"
#include "sat/glucose2/Map.h"
#include "sat/glucose2/Alloc.h"
ABC_NAMESPACE_CXX_HEADER_START
namespace Gluco2 {
//=================================================================================================
// 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);
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 = false) { 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 (Gluco2::lbool((uint8_t)0)) // gcc does not do constant propagation if these are real constants.
#define l_False (Gluco2::lbool((uint8_t)1))
#define l_Undef (Gluco2::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();
}
//=================================================================================================
}
ABC_NAMESPACE_CXX_HEADER_END
#endif
src/sat/glucose2/Sort.h 0 → 100644
/******************************************************************************************[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/glucose2/Vec.h"
//=================================================================================================
// Some sorting algorithms for vec's
ABC_NAMESPACE_CXX_HEADER_START
namespace Gluco2 {
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>()); }
//=================================================================================================
}
ABC_NAMESPACE_CXX_HEADER_END
#endif
src/sat/glucose2/System.h 0 → 100644
/****************************************************************************************[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/glucose2/IntTypes.h"
ABC_NAMESPACE_CXX_HEADER_START
//-------------------------------------------------------------------------------------------------
namespace Gluco2 {
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).
}
ABC_NAMESPACE_CXX_HEADER_END
//-------------------------------------------------------------------------------------------------
// Implementation of inline functions:
#if defined(_MSC_VER) || defined(__MINGW32__)
#include <time.h>
ABC_NAMESPACE_CXX_HEADER_START
static inline double Gluco2::cpuTime(void) { return (double)clock() / CLOCKS_PER_SEC; }
ABC_NAMESPACE_CXX_HEADER_END
#else
#include <sys/time.h>
#include <sys/resource.h>
#include <unistd.h>
ABC_NAMESPACE_CXX_HEADER_START
static inline double Gluco2::cpuTime(void) {
struct rusage ru;
getrusage(RUSAGE_SELF, &ru);
return (double)ru.ru_utime.tv_sec + (double)ru.ru_utime.tv_usec / 1000000; }
ABC_NAMESPACE_CXX_HEADER_END
#endif
#endif
src/sat/glucose2/System2.cpp 0 → 100644
/***************************************************************************************[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/glucose2/System.h"
#if defined(__linux__)
#include <stdio.h>
#include <stdlib.h>
ABC_NAMESPACE_IMPL_START
using namespace Gluco2;
// 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 Gluco2::memUsed() { return (double)memReadStat(0) * (double)getpagesize() / (1024*1024); }
double Gluco2::memUsedPeak() {
double peak = memReadPeak() / 1024;
return peak == 0 ? memUsed() : peak; }
ABC_NAMESPACE_IMPL_END
#elif defined(__FreeBSD__)
ABC_NAMESPACE_IMPL_START
using namespace Gluco2;
double Gluco2::memUsed(void) {
struct rusage ru;
getrusage(RUSAGE_SELF, &ru);
return (double)ru.ru_maxrss / 1024; }
double memUsedPeak(void) { return memUsed(); }
ABC_NAMESPACE_IMPL_END
#elif defined(__APPLE__)
#include <malloc/malloc.h>
ABC_NAMESPACE_IMPL_START
double Gluco2::memUsed(void) {
malloc_statistics_t t;
malloc_zone_statistics(NULL, &t);
return (double)t.max_size_in_use / (1024*1024); }
ABC_NAMESPACE_IMPL_END
#else
ABC_NAMESPACE_IMPL_START
double Gluco2::memUsed() {
return 0; }
ABC_NAMESPACE_IMPL_END
#endif
src/sat/glucose2/Vec.h 0 → 100644
/*******************************************************************************************[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/glucose2/IntTypes.h"
#include "sat/glucose2/XAlloc.h"
ABC_NAMESPACE_CXX_HEADER_START
namespace Gluco2 {
//=================================================================================================
// 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; } }
//=================================================================================================
}
ABC_NAMESPACE_CXX_HEADER_END
#endif
src/sat/glucose2/XAlloc.h 0 → 100644
/****************************************************************************************[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>
#include <misc/util/abc_namespaces.h>
ABC_NAMESPACE_CXX_HEADER_START
namespace Gluco2 {
//=================================================================================================
// 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;
}
}
//=================================================================================================
}
ABC_NAMESPACE_CXX_HEADER_END
#endif
src/sat/glucose2/license 0 → 100644
---------------
Glucose -- Copyright (c) 2013, Gilles Audemard, Laurent Simon
CRIL - Univ. Artois, France
LRI - Univ. Paris Sud, France
Glucose sources are based on MiniSat (see below MiniSat copyrights). Permissions
and copyrights of Glucose are exactly the same as Minisat on which it is based
on. (see below).
---------------
Copyright (c) 2003-2006, Niklas Een, Niklas Sorensson
Copyright (c) 2007-2010, Niklas Sorensson
Permission is hereby granted, free of charge, to any person obtaining a copy of
this software and associated documentation files (the "Software"), to deal in
the Software without restriction, including without limitation the rights to use,
copy, modify, merge, publish, distribute, sublicense, and/or sell copies of the
Software, and to permit persons to whom the Software is furnished to do so,
subject to the following conditions:
The above copyright notice and this permission notice shall be included in all
copies or substantial portions of the Software.
THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS
FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR
COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER
IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN
CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
*******************************************************************************/
\ No newline at end of file
src/sat/glucose2/module.make 0 → 100644
SRC += src/sat/glucose2/AbcGlucose2.cpp \
src/sat/glucose2/AbcGlucoseCmd2.cpp \
src/sat/glucose2/Glucose2.cpp \
src/sat/glucose2/Options2.cpp \
src/sat/glucose2/SimpSolver2.cpp \
src/sat/glucose2/System2.cpp
src/sat/glucose2/pstdint.h 0 → 100644
/* 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
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment