abc70930: src/sat/msat/msatInt.h Source File

00001 
00021 #ifndef __MSAT_INT_H__
00022 #define __MSAT_INT_H__
00023 
00027 
00028 //#include "leaks.h"       
00029 #include <stdio.h>
00030 #include <stdlib.h>
00031 #include <string.h>
00032 #include <assert.h>
00033 #include <time.h>
00034 #include <math.h>
00035 #include "msat.h"
00036 
00040 
00044 
00045 #ifdef _MSC_VER
00046 typedef __int64     int64;
00047 #else
00048 typedef long long   int64;
00049 #endif
00050 
00051 // outputs the runtime in seconds
00052 #define PRT(a,t) \
00053     printf( "%s = ", (a) ); printf( "%6.2f sec\n", (float)(t)/(float)(CLOCKS_PER_SEC) )
00054 
00055 // memory management macros
00056 #define ALLOC(type, num)        \
00057     ((type *) malloc(sizeof(type) * (num)))
00058 #define REALLOC(type, obj, num) \
00059     ((obj) ? ((type *) realloc((char *)(obj), sizeof(type) * (num))) : \
00060             ((type *) malloc(sizeof(type) * (num))))
00061 #define FREE(obj)               \
00062     ((obj) ? (free((char *)(obj)), (obj) = 0) : 0)
00063 
00064 // By default, custom memory management is used
00065 // which guarantees constant time allocation/deallocation 
00066 // for SAT clauses and other frequently modified objects.
00067 // For debugging, it is possible use system memory management
00068 // directly. In which case, uncomment the macro below.
00069 //#define USE_SYSTEM_MEMORY_MANAGEMENT 
00070 
00071 // internal data structures
00072 typedef struct Msat_Clause_t_      Msat_Clause_t;
00073 typedef struct Msat_Queue_t_       Msat_Queue_t;
00074 typedef struct Msat_Order_t_       Msat_Order_t;
00075 // memory managers (duplicated from Extra for stand-aloneness)
00076 typedef struct Msat_MmFixed_t_     Msat_MmFixed_t;    
00077 typedef struct Msat_MmFlex_t_      Msat_MmFlex_t;     
00078 typedef struct Msat_MmStep_t_      Msat_MmStep_t;     
00079 // variables and literals
00080 typedef int                       Msat_Lit_t;  
00081 typedef int                       Msat_Var_t;  
00082 // the type of return value
00083 #define MSAT_VAR_UNASSIGNED (-1)
00084 #define MSAT_LIT_UNASSIGNED (-2)
00085 #define MSAT_ORDER_UNKNOWN  (-3)
00086 
00087 // printing the search tree
00088 #define L_IND      "%-*d"
00089 #define L_ind      Msat_SolverReadDecisionLevel(p)*3+3,Msat_SolverReadDecisionLevel(p)
00090 #define L_LIT      "%s%d"
00091 #define L_lit(Lit) MSAT_LITSIGN(Lit)?"-":"", MSAT_LIT2VAR(Lit)+1
00092 
00093 typedef struct Msat_SolverStats_t_ Msat_SolverStats_t;
00094 struct Msat_SolverStats_t_
00095 {
00096     int64   nStarts;        // the number of restarts
00097     int64   nDecisions;     // the number of decisions
00098     int64   nPropagations;  // the number of implications
00099     int64   nInspects;      // the number of times clauses are vising while watching them
00100     int64   nConflicts;     // the number of conflicts
00101     int64   nSuccesses;     // the number of sat assignments found
00102 };
00103 
00104 typedef struct Msat_SearchParams_t_ Msat_SearchParams_t;
00105 struct Msat_SearchParams_t_
00106 {
00107     double  dVarDecay;
00108     double  dClaDecay;
00109 };
00110 
00111 // sat solver data structure visible through all the internal files
00112 struct Msat_Solver_t_
00113 {
00114     int                 nClauses;    // the total number of clauses
00115     int                 nClausesStart; // the number of clauses before adding
00116     Msat_ClauseVec_t *  vClauses;    // problem clauses
00117     Msat_ClauseVec_t *  vLearned;    // learned clauses
00118     double              dClaInc;     // Amount to bump next clause with.
00119     double              dClaDecay;   // INVERSE decay factor for clause activity: stores 1/decay.
00120 
00121     double *            pdActivity;  // A heuristic measurement of the activity of a variable.
00122     float *             pFactors;    // the multiplicative factors of variable activity
00123     double              dVarInc;     // Amount to bump next variable with.
00124     double              dVarDecay;   // INVERSE decay factor for variable activity: stores 1/decay. Use negative value for static variable order.
00125     Msat_Order_t *      pOrder;      // Keeps track of the decision variable order.
00126 
00127     Msat_ClauseVec_t ** pvWatched;   // 'pvWatched[lit]' is a list of constraints watching 'lit' (will go there if literal becomes true).
00128     Msat_Queue_t *      pQueue;      // Propagation queue.
00129 
00130     int                 nVars;       // the current number of variables
00131     int                 nVarsAlloc;  // the maximum allowed number of variables
00132     int *               pAssigns;    // The current assignments (literals or MSAT_VAR_UNKOWN)
00133     int *               pModel;      // The satisfying assignment
00134     Msat_IntVec_t *     vTrail;      // List of assignments made. 
00135     Msat_IntVec_t *     vTrailLim;   // Separator indices for different decision levels in 'trail'.
00136     Msat_Clause_t **    pReasons;    // 'reason[var]' is the clause that implied the variables current value, or 'NULL' if none.
00137     int *               pLevel;      // 'level[var]' is the decision level at which assignment was made. 
00138     int                 nLevelRoot;  // Level of first proper decision.
00139 
00140     double              dRandSeed;   // For the internal random number generator (makes solver deterministic over different platforms). 
00141 
00142     bool                fVerbose;    // the verbosity flag
00143     double              dProgress;   // Set by 'search()'.
00144 
00145     // the variable cone and variable connectivity
00146     Msat_IntVec_t *     vConeVars;
00147     Msat_IntVec_t *     vVarsUsed;
00148     Msat_ClauseVec_t *  vAdjacents;
00149 
00150     // internal data used during conflict analysis
00151     int *               pSeen;       // time when a lit was seen for the last time
00152     int                 nSeenId;     // the id of current seeing
00153     Msat_IntVec_t *     vReason;     // the temporary array of literals
00154     Msat_IntVec_t *     vTemp;       // the temporary array of literals
00155     int *               pFreq;       // the number of times each var participated in conflicts
00156 
00157     // the memory manager
00158     Msat_MmStep_t *     pMem;
00159 
00160     // statistics
00161     Msat_SolverStats_t  Stats;
00162     int                 nTwoLits;
00163     int                 nTwoLitsL;
00164     int                 nClausesInit;
00165     int                 nClausesAlloc;
00166     int                 nClausesAllocL;
00167     int                 nBackTracks;
00168 };
00169 
00170 struct Msat_ClauseVec_t_
00171 {
00172     Msat_Clause_t **    pArray;
00173     int                 nSize;
00174     int                 nCap;
00175 };
00176 
00177 struct Msat_IntVec_t_
00178 {
00179     int *               pArray;
00180     int                 nSize;
00181     int                 nCap;
00182 };
00183 
00187 
00191 
00195 
00196 /*=== satActivity.c ===========================================================*/
00197 extern void                Msat_SolverVarDecayActivity( Msat_Solver_t * p );
00198 extern void                Msat_SolverVarRescaleActivity( Msat_Solver_t * p );
00199 extern void                Msat_SolverClaDecayActivity( Msat_Solver_t * p );
00200 extern void                Msat_SolverClaRescaleActivity( Msat_Solver_t * p );
00201 /*=== satSolverApi.c ===========================================================*/
00202 extern Msat_Clause_t *     Msat_SolverReadClause( Msat_Solver_t * p, int Num );
00203 /*=== satSolver.c ===========================================================*/
00204 extern int                 Msat_SolverReadDecisionLevel( Msat_Solver_t * p );
00205 extern int *               Msat_SolverReadDecisionLevelArray( Msat_Solver_t * p );
00206 extern Msat_Clause_t **    Msat_SolverReadReasonArray( Msat_Solver_t * p );
00207 extern Msat_Type_t         Msat_SolverReadVarValue( Msat_Solver_t * p, Msat_Var_t Var );
00208 extern Msat_ClauseVec_t *  Msat_SolverReadLearned( Msat_Solver_t * p );
00209 extern Msat_ClauseVec_t ** Msat_SolverReadWatchedArray( Msat_Solver_t * p );
00210 extern int *               Msat_SolverReadSeenArray( Msat_Solver_t * p );
00211 extern int                 Msat_SolverIncrementSeenId( Msat_Solver_t * p );
00212 extern Msat_MmStep_t *     Msat_SolverReadMem( Msat_Solver_t * p );
00213 extern void                Msat_SolverClausesIncrement( Msat_Solver_t * p );
00214 extern void                Msat_SolverClausesDecrement( Msat_Solver_t * p );
00215 extern void                Msat_SolverClausesIncrementL( Msat_Solver_t * p );
00216 extern void                Msat_SolverClausesDecrementL( Msat_Solver_t * p );
00217 extern void                Msat_SolverVarBumpActivity( Msat_Solver_t * p, Msat_Lit_t Lit );
00218 extern void                Msat_SolverClaBumpActivity( Msat_Solver_t * p, Msat_Clause_t * pC );
00219 extern bool                Msat_SolverEnqueue( Msat_Solver_t * p, Msat_Lit_t Lit, Msat_Clause_t * pC );
00220 extern double              Msat_SolverProgressEstimate( Msat_Solver_t * p );
00221 /*=== satSolverSearch.c ===========================================================*/
00222 extern bool                Msat_SolverAssume( Msat_Solver_t * p, Msat_Lit_t Lit );
00223 extern Msat_Clause_t *     Msat_SolverPropagate( Msat_Solver_t * p );
00224 extern void                Msat_SolverCancelUntil( Msat_Solver_t * p, int Level );
00225 extern Msat_Type_t         Msat_SolverSearch( Msat_Solver_t * p, int nConfLimit, int nLearnedLimit, int nBackTrackLimit, Msat_SearchParams_t * pPars );
00226 /*=== satQueue.c ===========================================================*/
00227 extern Msat_Queue_t *      Msat_QueueAlloc( int nVars );
00228 extern void                Msat_QueueFree( Msat_Queue_t * p );
00229 extern int                 Msat_QueueReadSize( Msat_Queue_t * p );
00230 extern void                Msat_QueueInsert( Msat_Queue_t * p, int Lit );
00231 extern int                 Msat_QueueExtract( Msat_Queue_t * p );
00232 extern void                Msat_QueueClear( Msat_Queue_t * p );
00233 /*=== satOrder.c ===========================================================*/
00234 extern Msat_Order_t *      Msat_OrderAlloc( Msat_Solver_t * pSat );
00235 extern void                Msat_OrderSetBounds( Msat_Order_t * p, int nVarsMax );
00236 extern void                Msat_OrderClean( Msat_Order_t * p, Msat_IntVec_t * vCone );
00237 extern int                 Msat_OrderCheck( Msat_Order_t * p );
00238 extern void                Msat_OrderFree( Msat_Order_t * p );
00239 extern int                 Msat_OrderVarSelect( Msat_Order_t * p );
00240 extern void                Msat_OrderVarAssigned( Msat_Order_t * p, int Var );
00241 extern void                Msat_OrderVarUnassigned( Msat_Order_t * p, int Var );
00242 extern void                Msat_OrderUpdate( Msat_Order_t * p, int Var );
00243 /*=== satClause.c ===========================================================*/
00244 extern bool                Msat_ClauseCreate( Msat_Solver_t * p, Msat_IntVec_t * vLits, bool fLearnt, Msat_Clause_t ** pClause_out );
00245 extern Msat_Clause_t *     Msat_ClauseCreateFake( Msat_Solver_t * p, Msat_IntVec_t * vLits );
00246 extern Msat_Clause_t *     Msat_ClauseCreateFakeLit( Msat_Solver_t * p, Msat_Lit_t Lit );
00247 extern bool                Msat_ClauseReadLearned( Msat_Clause_t * pC );
00248 extern int                 Msat_ClauseReadSize( Msat_Clause_t * pC );
00249 extern int *               Msat_ClauseReadLits( Msat_Clause_t * pC );
00250 extern bool                Msat_ClauseReadMark( Msat_Clause_t * pC );
00251 extern void                Msat_ClauseSetMark( Msat_Clause_t * pC, bool fMark );
00252 extern int                 Msat_ClauseReadNum( Msat_Clause_t * pC );
00253 extern void                Msat_ClauseSetNum( Msat_Clause_t * pC, int Num );
00254 extern bool                Msat_ClauseReadTypeA( Msat_Clause_t * pC );
00255 extern void                Msat_ClauseSetTypeA( Msat_Clause_t * pC, bool fTypeA );
00256 extern bool                Msat_ClauseIsLocked( Msat_Solver_t * p, Msat_Clause_t * pC );
00257 extern float               Msat_ClauseReadActivity( Msat_Clause_t * pC );
00258 extern void                Msat_ClauseWriteActivity( Msat_Clause_t * pC, float Num );
00259 extern void                Msat_ClauseFree( Msat_Solver_t * p, Msat_Clause_t * pC, bool fRemoveWatched );
00260 extern bool                Msat_ClausePropagate( Msat_Clause_t * pC, Msat_Lit_t Lit, int * pAssigns, Msat_Lit_t * pLit_out );
00261 extern bool                Msat_ClauseSimplify( Msat_Clause_t * pC, int * pAssigns );
00262 extern void                Msat_ClauseCalcReason( Msat_Solver_t * p, Msat_Clause_t * pC, Msat_Lit_t Lit, Msat_IntVec_t * vLits_out );
00263 extern void                Msat_ClauseRemoveWatch( Msat_ClauseVec_t * vClauses, Msat_Clause_t * pC );
00264 extern void                Msat_ClausePrint( Msat_Clause_t * pC );
00265 extern void                Msat_ClausePrintSymbols( Msat_Clause_t * pC );
00266 extern void                Msat_ClauseWriteDimacs( FILE * pFile, Msat_Clause_t * pC, bool fIncrement );
00267 extern unsigned            Msat_ClauseComputeTruth( Msat_Solver_t * p, Msat_Clause_t * pC );
00268 /*=== satSort.c ===========================================================*/
00269 extern void                Msat_SolverSortDB( Msat_Solver_t * p );
00270 /*=== satClauseVec.c ===========================================================*/
00271 extern Msat_ClauseVec_t *  Msat_ClauseVecAlloc( int nCap );
00272 extern void                Msat_ClauseVecFree( Msat_ClauseVec_t * p );
00273 extern Msat_Clause_t **    Msat_ClauseVecReadArray( Msat_ClauseVec_t * p );
00274 extern int                 Msat_ClauseVecReadSize( Msat_ClauseVec_t * p );
00275 extern void                Msat_ClauseVecGrow( Msat_ClauseVec_t * p, int nCapMin );
00276 extern void                Msat_ClauseVecShrink( Msat_ClauseVec_t * p, int nSizeNew );
00277 extern void                Msat_ClauseVecClear( Msat_ClauseVec_t * p );
00278 extern void                Msat_ClauseVecPush( Msat_ClauseVec_t * p, Msat_Clause_t * Entry );
00279 extern Msat_Clause_t *     Msat_ClauseVecPop( Msat_ClauseVec_t * p );
00280 extern void                Msat_ClauseVecWriteEntry( Msat_ClauseVec_t * p, int i, Msat_Clause_t * Entry );
00281 extern Msat_Clause_t *     Msat_ClauseVecReadEntry( Msat_ClauseVec_t * p, int i );
00282 
00283 /*=== satMem.c ===========================================================*/
00284 // fixed-size-block memory manager
00285 extern Msat_MmFixed_t *    Msat_MmFixedStart( int nEntrySize );
00286 extern void                Msat_MmFixedStop( Msat_MmFixed_t * p, int fVerbose );
00287 extern char *              Msat_MmFixedEntryFetch( Msat_MmFixed_t * p );
00288 extern void                Msat_MmFixedEntryRecycle( Msat_MmFixed_t * p, char * pEntry );
00289 extern void                Msat_MmFixedRestart( Msat_MmFixed_t * p );
00290 extern int                 Msat_MmFixedReadMemUsage( Msat_MmFixed_t * p );
00291 // flexible-size-block memory manager
00292 extern Msat_MmFlex_t *     Msat_MmFlexStart();
00293 extern void                Msat_MmFlexStop( Msat_MmFlex_t * p, int fVerbose );
00294 extern char *              Msat_MmFlexEntryFetch( Msat_MmFlex_t * p, int nBytes );
00295 extern int                 Msat_MmFlexReadMemUsage( Msat_MmFlex_t * p );
00296 // hierarchical memory manager
00297 extern Msat_MmStep_t *     Msat_MmStepStart( int nSteps );
00298 extern void                Msat_MmStepStop( Msat_MmStep_t * p, int fVerbose );
00299 extern char *              Msat_MmStepEntryFetch( Msat_MmStep_t * p, int nBytes );
00300 extern void                Msat_MmStepEntryRecycle( Msat_MmStep_t * p, char * pEntry, int nBytes );
00301 extern int                 Msat_MmStepReadMemUsage( Msat_MmStep_t * p );
00302 
00306 #endif