diff options
Diffstat (limited to 'abc70930/src/sat/msat/msatInt.h')
-rw-r--r-- | abc70930/src/sat/msat/msatInt.h | 306 |
1 files changed, 0 insertions, 306 deletions
diff --git a/abc70930/src/sat/msat/msatInt.h b/abc70930/src/sat/msat/msatInt.h deleted file mode 100644 index 03903abe..00000000 --- a/abc70930/src/sat/msat/msatInt.h +++ /dev/null @@ -1,306 +0,0 @@ -/**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. - float * pFactors; // the multiplicative factors of variable activity - 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 - int * pFreq; // the number of times each var participated in conflicts - - // 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 DEFINITIONS /// -//////////////////////////////////////////////////////////////////////// - -//////////////////////////////////////////////////////////////////////// -/// 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 |