/**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