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