/**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 ] 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 ABC__sat__msat__msatInt_h #define ABC__sat__msat__msatInt_h //////////////////////////////////////////////////////////////////////// /// INCLUDES /// //////////////////////////////////////////////////////////////////////// #include #include #include #include #include #include "misc/util/abc_global.h" #include "msat.h" ABC_NAMESPACE_HEADER_START //////////////////////////////////////////////////////////////////////// /// PARAMETERS /// //////////////////////////////////////////////////////////////////////// //////////////////////////////////////////////////////////////////////// /// STRUCTURE DEFINITIONS /// //////////////////////////////////////////////////////////////////////// // 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_ { ABC_INT64_T nStarts; // the number of restarts ABC_INT64_T nDecisions; // the number of decisions ABC_INT64_T nPropagations; // the number of implications ABC_INT64_T nInspects; // the number of times clauses are vising while watching them ABC_INT64_T nConflicts; // the number of conflicts ABC_INT64_T 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). int 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 int 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 int 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 int Msat_ClauseCreate( Msat_Solver_t * p, Msat_IntVec_t * vLits, int 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 int Msat_ClauseReadLearned( Msat_Clause_t * pC ); extern int Msat_ClauseReadSize( Msat_Clause_t * pC ); extern int * Msat_ClauseReadLits( Msat_Clause_t * pC ); extern int Msat_ClauseReadMark( Msat_Clause_t * pC ); extern void Msat_ClauseSetMark( Msat_Clause_t * pC, int fMark ); extern int Msat_ClauseReadNum( Msat_Clause_t * pC ); extern void Msat_ClauseSetNum( Msat_Clause_t * pC, int Num ); extern int Msat_ClauseReadTypeA( Msat_Clause_t * pC ); extern void Msat_ClauseSetTypeA( Msat_Clause_t * pC, int fTypeA ); extern int 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, int fRemoveWatched ); extern int Msat_ClausePropagate( Msat_Clause_t * pC, Msat_Lit_t Lit, int * pAssigns, Msat_Lit_t * pLit_out ); extern int 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, int 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 /// //////////////////////////////////////////////////////////////////////// ABC_NAMESPACE_HEADER_END #endif