| /**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 ABC__sat__msat__msatInt_h |
| #define ABC__sat__msat__msatInt_h |
| |
| |
| //////////////////////////////////////////////////////////////////////// |
| /// INCLUDES /// |
| //////////////////////////////////////////////////////////////////////// |
| |
| #include <stdio.h> |
| #include <stdlib.h> |
| #include <string.h> |
| #include <assert.h> |
| #include <math.h> |
| |
| #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 |
