diff options
Diffstat (limited to 'src/sat/msat/msatInt.h')
| -rw-r--r-- | src/sat/msat/msatInt.h | 304 |
1 files changed, 304 insertions, 0 deletions
diff --git a/src/sat/msat/msatInt.h b/src/sat/msat/msatInt.h new file mode 100644 index 00000000..037616f6 --- /dev/null +++ b/src/sat/msat/msatInt.h @@ -0,0 +1,304 @@ +/**CFile**************************************************************** + + FileName [msatInt.c] + + PackageName [A C version of SAT solver MINISAT, originally developed + in C++ by Niklas Een and Niklas Sorensson, Chalmers University of + Technology, Sweden: http://www.cs.chalmers.se/~een/Satzoo.] + + Synopsis [Internal definitions of the solver.] + + Author [Alan Mishchenko <alanmi@eecs.berkeley.edu>] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - January 1, 2004.] + + Revision [$Id: msatInt.c,v 1.0 2004/01/01 1:00:00 alanmi Exp $] + +***********************************************************************/ + +#ifndef __MSAT_INT_H__ +#define __MSAT_INT_H__ + +//////////////////////////////////////////////////////////////////////// +/// INCLUDES /// +//////////////////////////////////////////////////////////////////////// + +//#include "leaks.h" +#include <stdio.h> +#include <stdlib.h> +#include <string.h> +#include <assert.h> +#include <time.h> +#include <math.h> +#include "msat.h" + +//////////////////////////////////////////////////////////////////////// +/// PARAMETERS /// +//////////////////////////////////////////////////////////////////////// + +//////////////////////////////////////////////////////////////////////// +/// STRUCTURE DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +#ifdef _MSC_VER +typedef __int64 int64; +#else +typedef long long int64; +#endif + +// outputs the runtime in seconds +#define PRT(a,t) \ + printf( "%s = ", (a) ); printf( "%6.2f sec\n", (float)(t)/(float)(CLOCKS_PER_SEC) ) + +// memory management macros +#define ALLOC(type, num) \ + ((type *) malloc(sizeof(type) * (num))) +#define REALLOC(type, obj, num) \ + (obj) ? ((type *) realloc((char *) obj, sizeof(type) * (num))) : \ + ((type *) malloc(sizeof(type) * (num))) +#define FREE(obj) \ + ((obj) ? (free((char *) (obj)), (obj) = 0) : 0) + +// By default, custom memory management is used +// which guarantees constant time allocation/deallocation +// for SAT clauses and other frequently modified objects. +// For debugging, it is possible use system memory management +// directly. In which case, uncomment the macro below. +//#define USE_SYSTEM_MEMORY_MANAGEMENT + +// internal data structures +typedef struct Msat_Clause_t_ Msat_Clause_t; +typedef struct Msat_Queue_t_ Msat_Queue_t; +typedef struct Msat_Order_t_ Msat_Order_t; +// memory managers (duplicated from Extra for stand-aloneness) +typedef struct Msat_MmFixed_t_ Msat_MmFixed_t; +typedef struct Msat_MmFlex_t_ Msat_MmFlex_t; +typedef struct Msat_MmStep_t_ Msat_MmStep_t; +// variables and literals +typedef int Msat_Lit_t; +typedef int Msat_Var_t; +// the type of return value +#define MSAT_VAR_UNASSIGNED (-1) +#define MSAT_LIT_UNASSIGNED (-2) +#define MSAT_ORDER_UNKNOWN (-3) + +// printing the search tree +#define L_IND "%-*d" +#define L_ind Msat_SolverReadDecisionLevel(p)*3+3,Msat_SolverReadDecisionLevel(p) +#define L_LIT "%s%d" +#define L_lit(Lit) MSAT_LITSIGN(Lit)?"-":"", MSAT_LIT2VAR(Lit)+1 + +typedef struct Msat_SolverStats_t_ Msat_SolverStats_t; +struct Msat_SolverStats_t_ +{ + int64 nStarts; // the number of restarts + int64 nDecisions; // the number of decisions + int64 nPropagations; // the number of implications + int64 nInspects; // the number of times clauses are vising while watching them + int64 nConflicts; // the number of conflicts + int64 nSuccesses; // the number of sat assignments found +}; + +typedef struct Msat_SearchParams_t_ Msat_SearchParams_t; +struct Msat_SearchParams_t_ +{ + double dVarDecay; + double dClaDecay; +}; + +// sat solver data structure visible through all the internal files +struct Msat_Solver_t_ +{ + int nClauses; // the total number of clauses + int nClausesStart; // the number of clauses before adding + Msat_ClauseVec_t * vClauses; // problem clauses + Msat_ClauseVec_t * vLearned; // learned clauses + double dClaInc; // Amount to bump next clause with. + double dClaDecay; // INVERSE decay factor for clause activity: stores 1/decay. + + double * pdActivity; // A heuristic measurement of the activity of a variable. + double dVarInc; // Amount to bump next variable with. + double dVarDecay; // INVERSE decay factor for variable activity: stores 1/decay. Use negative value for static variable order. + Msat_Order_t * pOrder; // Keeps track of the decision variable order. + + Msat_ClauseVec_t ** pvWatched; // 'pvWatched[lit]' is a list of constraints watching 'lit' (will go there if literal becomes true). + Msat_Queue_t * pQueue; // Propagation queue. + + int nVars; // the current number of variables + int nVarsAlloc; // the maximum allowed number of variables + int * pAssigns; // The current assignments (literals or MSAT_VAR_UNKOWN) + int * pModel; // The satisfying assignment + Msat_IntVec_t * vTrail; // List of assignments made. + Msat_IntVec_t * vTrailLim; // Separator indices for different decision levels in 'trail'. + Msat_Clause_t ** pReasons; // 'reason[var]' is the clause that implied the variables current value, or 'NULL' if none. + int * pLevel; // 'level[var]' is the decision level at which assignment was made. + int nLevelRoot; // Level of first proper decision. + + double dRandSeed; // For the internal random number generator (makes solver deterministic over different platforms). + + bool fVerbose; // the verbosity flag + double dProgress; // Set by 'search()'. + + // the variable cone and variable connectivity + Msat_IntVec_t * vConeVars; + Msat_IntVec_t * vVarsUsed; + Msat_ClauseVec_t * vAdjacents; + + // internal data used during conflict analysis + int * pSeen; // time when a lit was seen for the last time + int nSeenId; // the id of current seeing + Msat_IntVec_t * vReason; // the temporary array of literals + Msat_IntVec_t * vTemp; // the temporary array of literals + + // the memory manager + Msat_MmStep_t * pMem; + + // statistics + Msat_SolverStats_t Stats; + int nTwoLits; + int nTwoLitsL; + int nClausesInit; + int nClausesAlloc; + int nClausesAllocL; + int nBackTracks; +}; + +struct Msat_ClauseVec_t_ +{ + Msat_Clause_t ** pArray; + int nSize; + int nCap; +}; + +struct Msat_IntVec_t_ +{ + int * pArray; + int nSize; + int nCap; +}; + +//////////////////////////////////////////////////////////////////////// +/// GLOBAL VARIABLES /// +//////////////////////////////////////////////////////////////////////// + +//////////////////////////////////////////////////////////////////////// +/// MACRO DEFITIONS /// +//////////////////////////////////////////////////////////////////////// + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +/*=== satActivity.c ===========================================================*/ +extern void Msat_SolverVarDecayActivity( Msat_Solver_t * p ); +extern void Msat_SolverVarRescaleActivity( Msat_Solver_t * p ); +extern void Msat_SolverClaDecayActivity( Msat_Solver_t * p ); +extern void Msat_SolverClaRescaleActivity( Msat_Solver_t * p ); +/*=== satSolverApi.c ===========================================================*/ +extern Msat_Clause_t * Msat_SolverReadClause( Msat_Solver_t * p, int Num ); +/*=== satSolver.c ===========================================================*/ +extern int Msat_SolverReadDecisionLevel( Msat_Solver_t * p ); +extern int * Msat_SolverReadDecisionLevelArray( Msat_Solver_t * p ); +extern Msat_Clause_t ** Msat_SolverReadReasonArray( Msat_Solver_t * p ); +extern Msat_Type_t Msat_SolverReadVarValue( Msat_Solver_t * p, Msat_Var_t Var ); +extern Msat_ClauseVec_t * Msat_SolverReadLearned( Msat_Solver_t * p ); +extern Msat_ClauseVec_t ** Msat_SolverReadWatchedArray( Msat_Solver_t * p ); +extern int * Msat_SolverReadSeenArray( Msat_Solver_t * p ); +extern int Msat_SolverIncrementSeenId( Msat_Solver_t * p ); +extern Msat_MmStep_t * Msat_SolverReadMem( Msat_Solver_t * p ); +extern void Msat_SolverClausesIncrement( Msat_Solver_t * p ); +extern void Msat_SolverClausesDecrement( Msat_Solver_t * p ); +extern void Msat_SolverClausesIncrementL( Msat_Solver_t * p ); +extern void Msat_SolverClausesDecrementL( Msat_Solver_t * p ); +extern void Msat_SolverVarBumpActivity( Msat_Solver_t * p, Msat_Lit_t Lit ); +extern void Msat_SolverClaBumpActivity( Msat_Solver_t * p, Msat_Clause_t * pC ); +extern bool Msat_SolverEnqueue( Msat_Solver_t * p, Msat_Lit_t Lit, Msat_Clause_t * pC ); +extern double Msat_SolverProgressEstimate( Msat_Solver_t * p ); +/*=== satSolverSearch.c ===========================================================*/ +extern bool Msat_SolverAssume( Msat_Solver_t * p, Msat_Lit_t Lit ); +extern Msat_Clause_t * Msat_SolverPropagate( Msat_Solver_t * p ); +extern void Msat_SolverCancelUntil( Msat_Solver_t * p, int Level ); +extern Msat_Type_t Msat_SolverSearch( Msat_Solver_t * p, int nConfLimit, int nLearnedLimit, int nBackTrackLimit, Msat_SearchParams_t * pPars ); +/*=== satQueue.c ===========================================================*/ +extern Msat_Queue_t * Msat_QueueAlloc( int nVars ); +extern void Msat_QueueFree( Msat_Queue_t * p ); +extern int Msat_QueueReadSize( Msat_Queue_t * p ); +extern void Msat_QueueInsert( Msat_Queue_t * p, int Lit ); +extern int Msat_QueueExtract( Msat_Queue_t * p ); +extern void Msat_QueueClear( Msat_Queue_t * p ); +/*=== satOrder.c ===========================================================*/ +extern Msat_Order_t * Msat_OrderAlloc( Msat_Solver_t * pSat ); +extern void Msat_OrderSetBounds( Msat_Order_t * p, int nVarsMax ); +extern void Msat_OrderClean( Msat_Order_t * p, Msat_IntVec_t * vCone ); +extern int Msat_OrderCheck( Msat_Order_t * p ); +extern void Msat_OrderFree( Msat_Order_t * p ); +extern int Msat_OrderVarSelect( Msat_Order_t * p ); +extern void Msat_OrderVarAssigned( Msat_Order_t * p, int Var ); +extern void Msat_OrderVarUnassigned( Msat_Order_t * p, int Var ); +extern void Msat_OrderUpdate( Msat_Order_t * p, int Var ); +/*=== satClause.c ===========================================================*/ +extern bool Msat_ClauseCreate( Msat_Solver_t * p, Msat_IntVec_t * vLits, bool fLearnt, Msat_Clause_t ** pClause_out ); +extern Msat_Clause_t * Msat_ClauseCreateFake( Msat_Solver_t * p, Msat_IntVec_t * vLits ); +extern Msat_Clause_t * Msat_ClauseCreateFakeLit( Msat_Solver_t * p, Msat_Lit_t Lit ); +extern bool Msat_ClauseReadLearned( Msat_Clause_t * pC ); +extern int Msat_ClauseReadSize( Msat_Clause_t * pC ); +extern int * Msat_ClauseReadLits( Msat_Clause_t * pC ); +extern bool Msat_ClauseReadMark( Msat_Clause_t * pC ); +extern void Msat_ClauseSetMark( Msat_Clause_t * pC, bool fMark ); +extern int Msat_ClauseReadNum( Msat_Clause_t * pC ); +extern void Msat_ClauseSetNum( Msat_Clause_t * pC, int Num ); +extern bool Msat_ClauseReadTypeA( Msat_Clause_t * pC ); +extern void Msat_ClauseSetTypeA( Msat_Clause_t * pC, bool fTypeA ); +extern bool Msat_ClauseIsLocked( Msat_Solver_t * p, Msat_Clause_t * pC ); +extern float Msat_ClauseReadActivity( Msat_Clause_t * pC ); +extern void Msat_ClauseWriteActivity( Msat_Clause_t * pC, float Num ); +extern void Msat_ClauseFree( Msat_Solver_t * p, Msat_Clause_t * pC, bool fRemoveWatched ); +extern bool Msat_ClausePropagate( Msat_Clause_t * pC, Msat_Lit_t Lit, int * pAssigns, Msat_Lit_t * pLit_out ); +extern bool Msat_ClauseSimplify( Msat_Clause_t * pC, int * pAssigns ); +extern void Msat_ClauseCalcReason( Msat_Solver_t * p, Msat_Clause_t * pC, Msat_Lit_t Lit, Msat_IntVec_t * vLits_out ); +extern void Msat_ClauseRemoveWatch( Msat_ClauseVec_t * vClauses, Msat_Clause_t * pC ); +extern void Msat_ClausePrint( Msat_Clause_t * pC ); +extern void Msat_ClausePrintSymbols( Msat_Clause_t * pC ); +extern void Msat_ClauseWriteDimacs( FILE * pFile, Msat_Clause_t * pC, bool fIncrement ); +extern unsigned Msat_ClauseComputeTruth( Msat_Solver_t * p, Msat_Clause_t * pC ); +/*=== satSort.c ===========================================================*/ +extern void Msat_SolverSortDB( Msat_Solver_t * p ); +/*=== satClauseVec.c ===========================================================*/ +extern Msat_ClauseVec_t * Msat_ClauseVecAlloc( int nCap ); +extern void Msat_ClauseVecFree( Msat_ClauseVec_t * p ); +extern Msat_Clause_t ** Msat_ClauseVecReadArray( Msat_ClauseVec_t * p ); +extern int Msat_ClauseVecReadSize( Msat_ClauseVec_t * p ); +extern void Msat_ClauseVecGrow( Msat_ClauseVec_t * p, int nCapMin ); +extern void Msat_ClauseVecShrink( Msat_ClauseVec_t * p, int nSizeNew ); +extern void Msat_ClauseVecClear( Msat_ClauseVec_t * p ); +extern void Msat_ClauseVecPush( Msat_ClauseVec_t * p, Msat_Clause_t * Entry ); +extern Msat_Clause_t * Msat_ClauseVecPop( Msat_ClauseVec_t * p ); +extern void Msat_ClauseVecWriteEntry( Msat_ClauseVec_t * p, int i, Msat_Clause_t * Entry ); +extern Msat_Clause_t * Msat_ClauseVecReadEntry( Msat_ClauseVec_t * p, int i ); + +/*=== satMem.c ===========================================================*/ +// fixed-size-block memory manager +extern Msat_MmFixed_t * Msat_MmFixedStart( int nEntrySize ); +extern void Msat_MmFixedStop( Msat_MmFixed_t * p, int fVerbose ); +extern char * Msat_MmFixedEntryFetch( Msat_MmFixed_t * p ); +extern void Msat_MmFixedEntryRecycle( Msat_MmFixed_t * p, char * pEntry ); +extern void Msat_MmFixedRestart( Msat_MmFixed_t * p ); +extern int Msat_MmFixedReadMemUsage( Msat_MmFixed_t * p ); +// flexible-size-block memory manager +extern Msat_MmFlex_t * Msat_MmFlexStart(); +extern void Msat_MmFlexStop( Msat_MmFlex_t * p, int fVerbose ); +extern char * Msat_MmFlexEntryFetch( Msat_MmFlex_t * p, int nBytes ); +extern int Msat_MmFlexReadMemUsage( Msat_MmFlex_t * p ); +// hierarchical memory manager +extern Msat_MmStep_t * Msat_MmStepStart( int nSteps ); +extern void Msat_MmStepStop( Msat_MmStep_t * p, int fVerbose ); +extern char * Msat_MmStepEntryFetch( Msat_MmStep_t * p, int nBytes ); +extern void Msat_MmStepEntryRecycle( Msat_MmStep_t * p, char * pEntry, int nBytes ); +extern int Msat_MmStepReadMemUsage( Msat_MmStep_t * p ); + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// +#endif |