source: vis_dev/vis-2.3/src/sat/sat.h @ 43

/**CHeaderFile*****************************************************************

  FileName    [sat.h]

  PackageName [sat]

  Synopsis    []

  Description [Internal data structures of the sat package.]

  SeeAlso     []

  Author      [HoonSang Jin ]

  Copyright [ This file was created at the University of Colorado at
  Boulder.  The University of Colorado at Boulder makes no warranty
  about the suitability of this software for any purpose.  It is
  presented on an AS IS basis.]

  Revision    [$Id: sat.h,v 1.30 2009/04/12 00:14:11 fabio Exp $]

******************************************************************************/

#ifndef _SAT
#define _SAT

#include "util.h"
#include "array.h"
#include "st.h"
#include "heap.h"
#include "cudd.h"
#include "stdio.h"
/*Bing*/
#include "puresat.h"
//#include "satInt.h"


/*---------------------------------------------------------------------------*/
/* Constant declarations                                                     */
/*---------------------------------------------------------------------------*/

#define  bbAigValue     0   /* Index of value. */  
#define  bbAigFlags     1   /* Index of flag for this node.*/
#define  bbAigLeft      2   /* Index of the left child */ 
#define  bbAigRight     3   /* Index of the right child */ 
#define  bbAigNFanout   4   /* Index of number of fanout.*/
#define  bbAigFanout    5   /* Index of fanout pointer for this node.*/
#define  bbAigCanonical 6   /* Index of canonical node for this node.*/
#define  bbAigNext      7   /* Index of dummy for this node.*/
/*Bing:*/
#define  bAigClass     8


/**
 * Mask bit for each flags
 **/
/**
 *                      1 1 1 1 1 1 1 1 1 1 2 2 2 2 2 2 2 2 2 2 3 3 
 *  0 1 2 3 4 5 6 7 8 9 0 1 2 3 4 5 6 7 8 9 0 1 2 3 4 5 6 7 8 9 0 1 
 *  |_| | | | | | | | | | | | | | | | | | | | | |
 *   |  | | | | | | | | | | | | | | | | | | | | |
 *   |  | | | | | | | | | | | | | | | | | | | | InCoreMask
 *   |  | | | | | | | | | | | | | | | | | | | IsFrontierClause
 *   |  | | | | | | | | | | | | | | | | | | IsBlockingClause
 *   |  | | | | | | | | | | | | | | | | | Visited2
 *   |  | | | | | | | | | | | | | | | | CanonicalBit
 *   |  | | | | | | | | | | | | | | | IsSystem
 *   |  | | | | | | | | | | | | | | IsConflict
 *   |  | | | | | | | | | | | | | InUse
 *   |  | | | | | | | | | | | | InQueue
 *   |  | | | | | | | | | | | LeafNode
 *   |  | | | | | | | | | | BDDSatisfied 
 *   |  | | | | | | | | | StaticLearn
 *   |  | | | | | | | | NonObj 
 *   |  | | | | | | | Obj
 *   |  | | | | | | New
 *   |  | | | | | Visited
 *   |  | | | | Coi
 *   |  | | | IsCone
 *   |  | | StateBit
 *   |  | IsBDD    
 *   |  IsCNF      
 *   HValue
 **/

/*#define PreserveMask           0x0032681e*/
/*Bing*/
#define PreserveMask           0xff3a681e

#define HValueMask             0x00000003
#define ResetHValueMask        0xfffffffc

/**
 * If this mask bit is marked then the node is CNF node.
 **/
#define IsCNFMask              0x00000004
#define ResetIsCNFMask         0xfffffffb

/**
 * If this mask bit is marked then the node is BDD node.
 **/
#define IsBDDMask              0x00000008
#define ResetIsBDDMask         0xfffffff7


/**
 * If this mask bit is marked then the node is state variable.
 **/
#define StateBitMask           0x00000010
#define ResetStateBitMask      0xffffffef

/**
 * If this mask bit is marked then the node is transitive fanin of
 * certain variable.
 **/
#define IsConeMask             0x00000020
#define ResetIsConeMask        0xffffffdf

/**
 * If this mask bit is marked then the node is under cone of influence of root
 * node. To be implied by BCP this flag bit has to be set.
 **/
#define CoiMask                0x00000040
#define ResetCoiMask           0xffffffbf

/**
 * If this mask bit is marked then the node is visited.
 **/
#define VisitedMask            0x00000080
#define ResetVisitedMask       0xffffff7f

/**
 * If this mask bit is marked then the node is visited.
 * It can be used like a VisitedMask.
 **/
#define NewMask                0x00000100
#define ResetNewMask           0xfffffeff

/**
 * If this mask bit is marked then the node is object dependent.
 * It is used to identify object dependent conflict clause while
 * applying incremental SAT.
 **/
#define ObjMask                0x00000200
#define ResetObjMask           0xfffffdff

/**
 * If this mask bit is marked then the node is object independent.
 * It is used to identify object independent conflict clause while
 * applying incremental SAT.
 **/
#define NonobjMask             0x00000400
#define ResetNonobjMask        0xfffffbff


/**
 * If this mask bit is marked then the value of node is fixed by static 
 * learning.
 **/
#define StaticLearnMask        0x00000400
#define ResetStaticLearnMask   0xfffffbff

/**
 * If this mask bit is marked then the BDD node is satisfied by partial
 * or full assignment on support variables. 
 * This flag bit is used for BDD node only, which means that IsBDDMask
 * has to be set.
 **/
#define BDDSatisfiedMask       0x00000800
#define ResetBDDSatisfiedMask  0xfffff7ff

/**
 * If this mask bit is marked then the node is support variable of 
 * BDD node.
 **/
#define LeafNodeMask           0x00001000
#define ResetLeafNodeMask      0xffffefff

/**
 * If this mask bit is marked then the node is in implication queue. 
 * To avoid to put same node multiple times, it is set when the node is
 * in the queue.
 **/
#define InQueueMask            0x00002000
#define ResetInQueueMask       0xffffdfff

/**
 * If this mask bit is marked then the clause is in use.
 * This flag bit can be set for CNF node only.
 **/
#define InUseMask              0x00004000
#define ResetInUseMask         0xffffbfff

/**
 * If this mask bit is marked then the clause is conflict clause.
 * This flag bit can be set for CNF node only.
 **/
#define IsConflictMask         0x00008000
#define ResetIsConflictMask    0xffff7fff

/**
 * If this mask bit is marked then the node is part of original model.
 * For example, BMC instance can be classified into system part and
 * property part.
 **/
#define IsSystemMask           0x00010000
#define ResetIsSystemMask      0xfffeffff

/**
 * If AIG nodes are identified as equivalent node, then they are merged
 * into one of them. This mask bit is used identified the representative
 * of those equivalent nodes.
 **/
#define CanonicalBitMask       0x00020000
/**
#define ResetCanonicalBitMask  0xfffdffff
**/
#define ResetCanonicalBitMask  ~0x00020000L

/**
 * If this mask bit is marked then the node is visited.
 * It can be used like a VisitedMask.
 **/
#define Visited2Mask           0x00040000
#define ResetVisited2Mask      0xfffbffff

/**
 * If this mask bit is marked then the clause is blocking clause
 **/
#define IsBlockingMask         0x00100000
#define ResetIsBlockingMask    0xffefffff

#define IsFrontierMask         0x00200000
#define ResetIsFrontierMask    0xffdfffff

#define InCoreMask             0x00400000
#define ResetInCoreMask        0xffbfffff

#define ResetNewVisitedObjMask 0xfffffc7f
#define ResetNewVisitedObjInQueueMask 0xffffdc7f
#define ResetNewVisitedMask    0xfffffe7f


/*Bing: for interpolation*/
#define VisibleVarMask         0x01000000
#define ResetVisibleVarMask    0xfeffffff
#define DummyMask              0x02000000
#define ResetDummyMask         0xfdffffff
#define Visited3Mask           0x04000000
#define ResetVisited3Mask      0xfbffffff
#define IsGlobalVarMask        0x08000000
#define ResetGlobalVarMask     0xf7ffffff
#define Visited4Mask           0x10000000
#define ResetVisited4Mask      0xefffffff
#define AssignedMask           0x20000000
#define ResetAssignedMask      0xdfffffff
/*pseudo global var*/

#define PGVMask                0x40000000
#define ResetPGVMask           0xbfffffff
/*visible pseudo global var*/
#define VPGVMask               0x00080000
#define ResetVPGVMask          0xfff7ffff
#define ResetVisited1234NewMask 0xebfbfe7f


#define SAT_UNSAT 1
#define SAT_SAT 2
#define SAT_BACKTRACK 3
#define SAT_BDD_UNSAT 4
#define SAT_BDD_SAT 5
#define SAT_BDD_BACKTRACK 6

/*#define SATnodeID(node) ((node) >> 3)*/
/*Bing:*/
#define SATnodeID(node) (SATnormalNode(node)/satNodeSize)

#define SATvalue(node) (cm->nodesArray[((node) &(~0x1L)) +satValue]) 


/* For AIG */
#define  satValue       bbAigValue     /* Index of value. */  
#define  satFlags       bbAigFlags     /* Index of flag for this node.*/
#define  satLeft        bbAigLeft      /* Index of the left child */ 
#define  satRight       bbAigRight     /* Index of the right child */ 
#define  satNFanout     bbAigNFanout  
#define  satFanout      bbAigFanout    
#define  satCanonical   bbAigCanonical     /* Index of the right child */ 
#define  satNext        bbAigNext     /* Index of the right child */ 

/*Bing: for interpolation*/
#define  satClass       bAigClass /* equals the timeframes it is in*/

#define satNumLits  bbAigLeft
#define satFirstLit bbAigRight
#define satNumConflict    bbAigNext
#define satConflictUsage  bbAigFanout

/*#define satNodeSize 8*/
/*Bing*/
#define satNodeSize 12


#define LATEST_CONFLICT_DECISION 0x1
#define DVH_DECISION 0x2

#define SATInvertBit 0x1
/*Bing*/
#define SATclass(node) (cm->nodesArray[SATnormalNode(node)+satClass])
/*
#define SATnext(node) (cm->nodesArray[node+satNext]) 


#define SATcanonical(node) (cm->nodesArray[node+satCanonical]) 

#define SATleftChild(node) (cm->nodesArray[node+satLeft]) 

#define SATrightChild(node) (cm->nodesArray[node+satRight]) 

#define SATfanout(node) ((long *)(cm->nodesArray[node+satFanout])) 

#define SATnFanout(node) (cm->nodesArray[node+satNFanout]) 
*/
/*Bing*/
#define SATnext(node) (cm->nodesArray[SATnormalNode(node)+satNext]) 

#define SATflags(node) (cm->nodesArray[SATnormalNode(node)+satFlags]) 

#define SATcanonical(node) (cm->nodesArray[SATnormalNode(node)+satCanonical]) 

#define SATleftChild(node) (cm->nodesArray[SATnormalNode(node)+satLeft]) 

#define SATrightChild(node) (cm->nodesArray[SATnormalNode(node)+satRight]) 

#define SATfanout(node) ((long *)(cm->nodesArray[SATnormalNode(node)+satFanout])) 

#define SATnFanout(node) (cm->nodesArray[SATnormalNode(node)+satNFanout])

#define SATgetVariable(node) (&(cm->variableArray[SATnodeID(node)]))


#define SATflags(node) (cm->nodesArray[SATnormalNode(node)+satFlags]) 


#define SATgetNode(lit)  (lit >> 2)

#define SATgetDir(lit) ((lit&0x03) - 2)

#define SATisWL(lit) (lit&0x03)

#define SATunsetWL(plit) ((*plit) = (*plit) & (0x0fffffffc))

#define SATsetWL(plit, dir) ((*plit) = (*plit) + dir + 2)

#define SATsetInUse(node)  (SATflags(node) |= InUseMask)

#define SATreadInUse(node)  (SATflags(node) & InUseMask)

#define SATresetInUse(node)  (SATflags(node) &= ResetInUseMask)

#define SATgetValueChar(value) (value==0 ? '0' : (value==1 ? '1' : 'x'))


#define SATnumConflict(node) (cm->nodesArray[node+satNumConflict]) 

#define SATconflictUsage(node) (cm->nodesArray[node+satConflictUsage])


#define SATlevel(node)(\
cm->variableArray[SATnodeID(node)].level\
)

#define SATante(node)(\
cm->variableArray[SATnodeID(node)].antecedent\
)

#define SATante2(node)(\
cm->variableArray[SATnodeID(node)].antecedent2\
)

#define SATgetValue(left, right, v)     \
  ( ((SATvalue(SATnormalNode(left)) ^ SATisInverted(left)) << 4) | \
    ((SATvalue(SATnormalNode(right)) ^ SATisInverted(right)) << 2) | \
    (SATvalue(v)))

#define SATmakeImplied(v, d)                              \
    ( sat_ArrayInsert(d->implied, v),     \
      SATlevel(v) = d->level)


#define SATgetDecision(level) (&(cm->decisionHead[level]))

/*#define SATflags(node) (cm->nodesArray[node+satFlags])*/

#define SATnormalNode(node) ((node) & (~0x1L))

#define SATnot(node) ((node) ^ SATInvertBit)

#define SATisInverted(node) ((node) & (SATInvertBit))

#define SATnumLits(node) (cm->nodesArray[node+satNumLits]) 

#define SATfirstLit(node) (cm->nodesArray[node+satFirstLit])




/*---------------------------------------------------------------------------*/
/* Type declarations                                                         */
/*---------------------------------------------------------------------------*/

typedef struct satManagerStruct         satManager_t;
typedef struct satInterfaceStruct       satInterface_t;
typedef struct satStatisticsStruct      satStatistics_t;
typedef struct satOptionStruct          satOption_t;
typedef struct satQueueStruct           satQueue_t;
typedef struct satArrayStruct           satArray_t;
typedef struct satLiteralDBStruct       satLiteralDB_t;
typedef struct satLevelStruct           satLevel_t;
typedef struct satVariableStruct        satVariable_t;
typedef struct satTrieStruct            satTrie_t;

typedef struct satLinearHeadStruct      satLinearHead_t;
typedef struct satLinearVarStruct       satLinearVar_t;
typedef struct satLinearElemStruct      satLinearElem_t;
typedef struct satLinearClusterStruct   satLinearCluster_t;


/*---------------------------------------------------------------------------*/
/* Structure declarations                                                    */
/*---------------------------------------------------------------------------*/

/**Struct**********************************************************************

  Synopsis    [A struct for manager for CirCUs.]

******************************************************************************/
struct satManagerStruct {
    struct satOptionStruct *option; 
    struct satTimeFrameStruct *timeframe;
    struct satTimeFrameStruct *timeframeWOI;
    struct satLiteralDBStruct *literals;

    struct satStatisticsStruct *total; /* to gather statistics on set of SAT runs.*/
    struct satStatisticsStruct *each;  /* to save statistics of one SAT run. */

    struct satQueueStruct *queue;  /* implication queue. */
    struct satQueueStruct *BDDQueue; /* implication queue for BDD */
    struct satQueueStruct *unusedAigQueue; /* queue for unused AIG for CNF. */

    long *nodesArray;
    long *HashTable;
    long nodesArraySize;
    long maxNodesArraySize; /* These 4 fields are used as in bAigManager_t.
                             * We copy it to isolate code of CirCUs from 
                             * baig package. When one build a interface
                             * for CirCUs you have to copy back these
                             * fields to bAig_Manager_t structure after
                             * SAT solving. */

    long beginConflict;   /* to save the beginning of conflict learned clauses. */
    long initNodesArraySize; /* to save the initial AIG structure size.*/

    struct satVariableStruct *variableArray; /* the array of satVariable_t. */

    /* These 7 arrays are the array of AIG nodes.
    * If the AIG node is inverted then it will be asserted to be '0'.
    * Otherwise it is asserted to be '1'. */
    struct satArrayStruct *auxObj;    /* the array of auxiliary objectives  */
    struct satArrayStruct *obj;       /* the array of objective literal */
    struct satArrayStruct *objCNF;    /* the array of objective clause */
    struct satArrayStruct *assertion; /* the array of assertion */
                                 /* it is now used to save static learned node. */
    struct satArrayStruct *unitLits;  /* the array of unit literals for CNF */
    struct satArrayStruct *pureLits;  /* the array of pure literals for CNF */
    struct satArrayStruct *nonobjUnitLitArray; 
                 /* to save unit objective independent conflict clauses
                 * it is for incremental SAT. */
    struct satArrayStruct *objUnitLitArray;
                 /* to save unit objective dependent conflict clauses
                 * it is for incremental SAT. */
    
    
    struct satLevelStruct *decisionHead; /* the array of satLevel_t. */
    int decisionHeadSize;                /* the size of *decisionHead.*/
    int currentDecision;                 
                 /* to represent the current decision level */

    struct satArrayStruct *assignByBDD;
    struct satArrayStruct *orderedVariableArray;
                 /* the array of AIG nodes that are the variables.
                 * It is for score based decision heuristic. */
    int currentVarPos;
                 /* to represent the index of orderedVariableArray that
                 * is not assigned yet. */

    struct satArrayStruct *savedConflictClauses;
                 /* to save the conflict clauses that can be forwarded
                 * when we apply incremental SAT */
    struct satArrayStruct *trieArray;
                 /* to save the trie to apply distillation method
                 * when we apply incremental SAT */
    struct satArrayStruct *auxArray;
                 /* Can be used to save arbitrary array */

    long *currentTopConflict;    
                 /* to save current top clause 
                 * based on the definition of BerkMin */
    int currentTopConflictCount;

    int lowestBacktrackLevel;
                 /* to save lowest backtrack level */
    char *comment;

    int initNumVariables; /* the number of initial variables. */
    int initNumClauses;   /* the number of initial clauses. */
    int initNumLiterals;  /* the number of initial literals. */
    int implicatedSoFar; /* the number of implied node so far, which sum of all implied nodes. */

    FILE *stdErr;
    FILE *stdOut;

    int status; /* the status of SAT solving result
                * SAT_BACKTRACK, SAT_SAT, SAT_UNSAT. */
    
    struct satArrayStruct *dormantConflictArray;
    struct satArrayStruct *shrinkArray;
    int shrinkEnable;
    int shrinkSize;
    int forceLatestConflictDecision;
    DdManager *mgr;

    struct satArrayStruct *frontier;
    struct satArrayStruct *reached;
    long frontierNodesBegin;
    long frontierNodesEnd;
    struct satArrayStruct *clauseIndexInCore;

  
    /* BING : for conflcit core generation */
    st_table * dependenceTable;
    st_table *anteTable;
    struct satArrayStruct * dependenceArray;
    int numOfClsInCore;
    FILE *fp, *fp2;

  /*Bing:*/
  IP_Manager_t * ipm;
  st_table * RTreeTable;/* ConClsIdx->RT ptr */

  satArray_t * assertArray, *assertArray2, *CoiAssertArray, *EqArray;
  int class_;
  long InitState, IPState, property;
  satArray_t * tmpArray;
  st_table * table;
  int test;
  RTManager_t * rm;
  /*for AROSAT*/
  st_table * layerTable;
  int OriLevel, LatchLevel;
  int *numArray,*assignedArray;
  int currentLevel;
  int Length;
  int line;
  
};

/**Struct**********************************************************************

  Synopsis    [A struct to interface CirCUs and application.
               One can freely add a field based on his need.]

******************************************************************************/
struct satInterfaceStruct {
    struct satStatisticsStruct *total;
    struct satArrayStruct *nonobjUnitLitArray;
    struct satArrayStruct *objUnitLitArray;
    struct satArrayStruct *savedConflictClauses;
    struct satArrayStruct *trieArray;
    int status;
};

/**Struct**********************************************************************

  Synopsis    [A struct to gather CirCUs statistics ]

******************************************************************************/
struct satStatisticsStruct {
    int nBacktracks;                /* the number of backtracks */
    int nNonchonologicalBacktracks; /* the sum of backtrack levels */
    int nDecisions;                 /* the number of decisions */
    int nDVHDecisions;              /* the number of decisions by DVH */
    int nVSIDSDecisions;            /* the number of decisions by VSIDS */
    int nShrinkDecisions;           
    int nLatestConflictDecisions;   /* the number of decisions by current top clause */
    int maxDecisionLevel;           /* the maximum decision level */
    int nLowScoreDecisions;         /* the number of decision without sufficient information. */

    int nCNFImplications;           /* the number of implication done by CNF */
    int nAigImplications;           /* the number of implication done by AIG */
    int nBDDImplications;           /* the number of implication done by BDD */
    int nHyperImplications;

    int nUnitConflictCl;            /* the number of unit conflict clauses */
    int nOldConflictCl;  
    int nConflictCl;                /* the number of conflict clauses   */
    int nConflictLit;               /* the sum of literals in conflict clauses  */
    int nObjConflictCl;             /* the number of object dependent conflict clauses   */
    int nObjConflictLit;            /* the sum of literals in object dependent conflict clauses  */
    int nNonobjConflictCl;          /* the number of object independent conflict clauses  */ 
    int nNonobjConflictLit;          /* the sum of literals in object dependent conflict clauses  */
    int nInitObjConflictCl;         /* the number of conflict clauses  forwarded from previous run */
    int nInitObjConflictLit;        /* the sum of literals in conflict clauses forwarded from previous run */
    int nInitNonobjConflictCl;
    int nInitNonobjConflictLit;
    int nDistillObjConflictCl;
    int nDistillObjConflictLit;
    int nDistillNonobjConflictCl;
    int nDistillNonobjConflictLit;
    int nDeletedCl;                 /* the number of conflict clauses deleted */
    int nDeletedLit;                /* the sum of literals in conflict clauses deleted */
    int nBlockingCl;                 /* the number of blocking clauses deleted */
    int nBlockingLit;                /* the sum of literals in blocking clauses deleted */
    int nDeletedButUncompacted;
    double satTime;
};

/**Struct**********************************************************************

  Synopsis    [A struct to set option for CirCUs statistics ]

******************************************************************************/
struct satOptionStruct {
    int verbose;
    int decisionHeuristic;      /* to select decision heuristic */
    int decisionAgeInterval;    /* to set aging interval */
    int decisionAgeRestart;     /* to turn on/off restart after aging */

    int clauseDeletionHeuristic; /* to select clause deletion heuristic */
    int clauseDeletionInterval;  /* to set clause deletion interval */
    int nextClauseDeletion;

    int incTraceObjective;       /* to turn on/off incremental SAT by trace objective */
    int incDistill;              /* to turn on/off incremental SAT by distillation */
    int incAll;
    int incNumObjLitsLimit;      /* to limit the number literals in objective dependent cluases that can be forwarded by incremental SAT */
    int incNumNonobjLitsLimit;   /* to limit the number literals in objective independent cluases that can be forwarded by incremental SAT */
    int incPreserveNonobjective; /* to keep the objective independent clause while apply clause deletion */

    int aig2BDDOn;               /* convert AIG into BDD when it is advantageous */
    int BDDRecondition;          /* extract clause from BDDs by prime implication generation */
    int BDDMonolithic;           /* build monolithic BDD for clauses */
    int BDDDPLL;                 /* combine BDD and DPLL procedure */
    int BDDImplication;          /* apply BDD based implication */

    int includeLevelZeroLiteral; /* do add literals implied in level zero When append conflict learned clause  */
    int minimizeConflictClause;  /* apply conflict clause minimization procedure */
    int shrinkConflictClause;    /* apply conflict shrinking method done by JeruSAT */
    int unrelevance;             /* set the unrelevance of conflict clause when applying clause deletion  */
    int minLitsLimit;            /* If the number of literals in clause less than this value then keep it when applying clause deletion  */
    int maxLitsLimit;            /* If the number of literals in clause more than this value then delete it when applying clause deletion */

    int latestUsage;
    int obsoleteUsage;
    int latestUnrelevance;
    int obsoleteUnrelevance;
    int latestRate;

    int restartInterval;

    int memoryLimit;
    int timeoutLimit;

    int minConflictForDecision;         /* to avoid too small clause when deciding current top clause */
    int maxConflictForDecision;         /* to avoid too large clause when deciding current top clause */
    int skipSatisfiedClauseForDecision; /* to skip satified clause when deciding current top clause */

    int maxLimitOfClausesForMonolithicBDD;
    int maxLimitOfVariablesForMonolithicBDD;
    int maxLimitOfCutSizeForMonolithicBDD;

    int maxLimitOfClausesForBDDDPLL;
    int maxLimitOfVariablesForBDDDPLL;
    int maxLimitOfCutSizeForBDDDPLL;

    int maxLimitOfVariablesForBDD;

    int interfaceCNF;            /* to write CNF instead of running CirCUs */
    int cnfPrefix;
    int runOtherSolver;          /* run other CNF solver after writing CNF */
    char *otherSolverName;       /* specify the SAT solver name */

    int newConflictAnalysis;
    int checkNonobjForwarding;

    char *outFilename;
    struct satArrayStruct *forcedAssignArr;

  
    char * unsatCoreFileName;
  
    int allSatMode;
    int useStrongConflictAnalysis; /* triggering strong conflict analysis */
  
    /* Bing: UNSAT core generation */
    int coreGeneration;
  /*Bing*/
  int IP;
  int SSS;

  int arosat;
  int AbRf;
  int RT;
  int ForceFinish;
};


/**Struct**********************************************************************

  Synopsis    [A struct for queue]

******************************************************************************/
struct satQueueStruct {
    long max;         /* max size of queue */
    long size;        /* the number of current entries */
    long front;       /* front index of entries */
    long rear;        /* rear index of entries */
    long *array;      /* the location to save entries */
};

/**Struct**********************************************************************

  Synopsis    [A struct for array]

******************************************************************************/
struct satArrayStruct {
    long *space;     /* the location to save entries */
    long num;        /* the number of entries */
    long size;       /* the size of space */
};

/**Struct**********************************************************************

  Synopsis    [A struct to save lterals]

******************************************************************************/
struct satLiteralDBStruct {
  long *begin;       /* the begin pointer of literal database */
  long *last;        /* the pointer of last literal */
  long *end;         /* the end pointer of literal database */
  long *initialSize; /* the pointer of last literals that is given as input */
};

/**Struct**********************************************************************

  Synopsis    [A struct for decision level]

******************************************************************************/
struct satLevelStruct {
  int level;          /* decision level  */
  long decisionNode;   /* decision node of this level  */
  long conflict;       /* the conflict that happens from implication  */
  struct satArrayStruct *implied;  /* the array of implied nodes  */
  struct satArrayStruct *satisfied; /* the array of satisfied BDD nodes  */
  int currentVarPos;                /* the index of decision node in orderedVariableArray  */
  int nConflict;
};

/**Struct**********************************************************************

  Synopsis    [A struct for variable]

******************************************************************************/
struct satVariableStruct {
  int level;            /* the decision level that make implication on this variable */
  int scores[2];        /* score for both phase   */           
  int litsCount[2];     /* the location to save literal count */
  int lastLitsCount[2]; /* last literal count */
  int conflictLits[2];  /* literal count of literals in conflict clause */
  long antecedent;      /* antecedent */
  long antecedent2;     /* antecedent */
  int pos;              /* position in orderedVariableArray */
  int depth;            /* depth of variable in implication graph */
  struct satArrayStruct *wl[2]; /* watched literal list */
  
  /*Bing: for AROSAT*/
  int RecVal;  /*1 for one, -1 for zero, 0 for not recorded*/
};

/**Struct**********************************************************************

  Synopsis    [A struct for trie]

******************************************************************************/
struct satTrieStruct {
  long id;                           /* node id */
  struct satArrayStruct *child[2];  /* childrun */
  int depth;                        /* depth from root */
};

struct satLinearElemStruct {
  double pos;
  int order;
  int num;
  struct satArrayStruct *support;
  long node; 
  DdNode *bdd;
  int flag;
  int to;
  struct satLinearElemStruct *next;
};

struct satLinearVarStruct {
  double pos;
  int order;
  int from;
  int to;
  struct satArrayStruct *clauses;
  long node;
  DdNode *bdd;
  int bQuantified;
  struct satLinearVarStruct *next;
};

struct satLinearHeadStruct {
  DdManager *mgr;
  struct satLinearElemStruct *elemHead;
  struct satLinearVarStruct *varHead;
  int nVars;
  int nCls;
  int bddLimit;
  int bddAndLimit;
  long *id2edge;
  int *edge2id;
  int *edge2vid;
  Heap_t *heap;
  struct satArrayStruct *elemArray;
  struct satArrayStruct *varArray;
  struct satArrayStruct *clausesArray;
  struct satArrayStruct *variablesArray;
  struct satArrayStruct *latestClusterArray;
  struct satArrayStruct *deadArray;
  int reordering;
};

struct satLinearClusterStruct {
  struct satLinearElemStruct *elem1;
  struct satLinearElemStruct *elem2;
  int flag;
  int cost;
  int overlap;
  struct satArrayStruct *deadArray;
};



/*---------------------------------------------------------------------------*/
/* Variable declarations                                                     */
/*---------------------------------------------------------------------------*/


/*---------------------------------------------------------------------------*/
/* Macro declarations                                                        */
/*---------------------------------------------------------------------------*/


/*---------------------------------------------------------------------------*/
/* Function prototypes                                                       */
/*---------------------------------------------------------------------------*/
EXTERN satManager_t * sat_InitManager(satInterface_t *interface);
EXTERN satArray_t * sat_ArrayAlloc(long number);
EXTERN satStatistics_t * sat_InitStatistics(void);
EXTERN satOption_t * sat_InitOption(void);
EXTERN satArray_t * sat_ReadForcedAssignment( char *filename);
EXTERN int sat_GetNumberOfInitialClauses(satManager_t *cm);
EXTERN int sat_GetNumberOfInitialVariables(satManager_t *cm);
EXTERN satLevel_t * sat_AllocLevel( satManager_t *cm);
EXTERN int sat_ConflictAnalysis( satManager_t *cm, satLevel_t *d); 
EXTERN int sat_StrongConflictAnalysis( satManager_t *cm, satLevel_t *d); 
EXTERN void sat_CombineStatistics(satManager_t *cm);
EXTERN long sat_GetClauseFromLit( satManager_t *cm, long *lit);
EXTERN long sat_DecisionBasedOnBDD( satManager_t *cm, satLevel_t *d);
EXTERN long sat_DecisionBasedOnLatestConflict( satManager_t *cm, satLevel_t *d);
EXTERN long sat_DecisionBasedOnScore( satManager_t *cm, satLevel_t *d);
EXTERN void sat_CheckDecisonVariableArray( satManager_t *cm);
EXTERN void sat_FreeManager(satManager_t *cm);
EXTERN void sat_ArrayInsert(satArray_t *array, long datum);
EXTERN void sat_SetIncrementalOption(satOption_t *option, int incFlag);
EXTERN void sat_RestoreFanout(satManager_t *cm);
EXTERN int sat_GetFanoutSize( satManager_t *cm, long v);
EXTERN void sat_CleanLevel(satLevel_t *d);
EXTERN void sat_CleanDatabase(satManager_t *cm);
EXTERN void sat_SetConeOfInfluence(satManager_t *cm);
EXTERN void sat_BuildTrieForDistill(satManager_t *cm) ;
EXTERN void sat_AllocLiteralsDB(satManager_t *cm) ;
EXTERN void sat_ArrayFree(satArray_t *array);
EXTERN void sat_PrintScore(satManager_t *cm);
EXTERN void sat_PutAssignmentValueMain( satManager_t *cm, satLevel_t *d, satArray_t *arr);
EXTERN void sat_Main(satManager_t *cm);
EXTERN void sat_FindUIP( satManager_t *cm, satArray_t *clauseArray, satLevel_t *d, int *objectFlag, int *bLevel, long *fdaLit);
EXTERN void sat_FindUIPWithRT( satManager_t *cm, satArray_t *clauseArray, satLevel_t *d, int *objectFlag, int *bLevel, long *fdaLit);
EXTERN void sat_MarkNodeInConflictClauseObjConservative( satManager_t *cm, satLevel_t *d, int *nMarked, int *oFlag, int *bLevel, satArray_t *clauseArray);
EXTERN void sat_PrintImplicationGraph( satManager_t *cm, satLevel_t *d);
EXTERN void sat_PrintNodeAlone(satManager_t *cm, long v);
EXTERN void sat_PrintNode( satManager_t *cm, long v);
EXTERN void sat_Backtrack( satManager_t *cm, int level);
EXTERN void sat_PrintDotForConflict( satManager_t *cm, satLevel_t *d, long conflict, int includePreviousLevel);
EXTERN long sat_AddUnitConflictClause( satManager_t *cm, satArray_t *clauseArray, int objectFlag);
EXTERN void sat_Enqueue(satQueue_t *Q, long v);
EXTERN long sat_AddConflictClause( satManager_t *cm, satArray_t *clauseArray, int objectFlag);
EXTERN long sat_AddConflictClauseWithoutScoring( satManager_t *cm, satArray_t *clauseArray, int objectFlag);
EXTERN void sat_UpdateDVH( satManager_t *cm, satLevel_t *d, satArray_t *clauseArray, int bLevel, long unitLit);
EXTERN void sat_FindUIPForCoreGen( satManager_t *cm, satArray_t *clauseArray, satLevel_t *d, int *objectFlag, int *bLevel, long *fdaLit);
EXTERN void sat_FindUIPForCoreGenWithRT( satManager_t *cm, satArray_t *clauseArray, satLevel_t *d, int *objectFlag, int *bLevel, long *fdaLit);
EXTERN void sat_MarkNodeInConflict( satManager_t *cm, satLevel_t *d, int *nMarked, int *objectFlag, int *bLevel, satArray_t *clauseArray);
EXTERN void sat_MarkNodeInImpliedNode( satManager_t *cm, satLevel_t *d, long v, int *nMarked, int *objectFlag, int *bLevel, satArray_t *clauseArray);
EXTERN void sat_MinimizeConflictClause( satManager_t *cm, satArray_t *clauseArray);
EXTERN void sat_ResetFlagForClauseArray( satManager_t *cm, satArray_t *clauseArray); 
EXTERN void sat_ImplyCNF( satManager_t *cm, satLevel_t *d, long v, satArray_t *wl); 
EXTERN int sat_ImplyNode( satManager_t *cm, satLevel_t *d, long v);
EXTERN void sat_ImplicationMain( satManager_t *cm, satLevel_t *d);
EXTERN void sat_CleanImplicationQueue( satManager_t *cm);
EXTERN void sat_ImplyArray( satManager_t *cm, satLevel_t *d, satArray_t *arr);
EXTERN void sat_ImplyBDD( satManager_t *cm, satLevel_t *d, long v);
EXTERN void sat_BuildLevelZeroHyperImplicationGraph( satManager_t *cm);
EXTERN void sat_PreProcessing(satManager_t *cm);
EXTERN void sat_MarkObjectiveFlagToArray( satManager_t *cm, satArray_t *objArr);
EXTERN void sat_PostProcessing(satManager_t *cm);
EXTERN void sat_Solve(satManager_t *cm);
EXTERN void sat_PeriodicFunctions(satManager_t *cm);
EXTERN void sat_CNFMain(satOption_t *option, char *filename);
EXTERN int sat_PrintSatisfyingAssignment(satManager_t *cm);
EXTERN void sat_Verify(satManager_t *cm);
EXTERN long sat_Dequeue( satQueue_t * Q );
EXTERN long sat_CreateNode( satManager_t *cm, long left, long right);
EXTERN int sat_EnlargeLiteralDB(satManager_t *cm);
EXTERN void sat_AddWL( satManager_t *cm, long c, int index, int dir);
EXTERN long sat_AddConflictClause( satManager_t *cm, satArray_t *clauseArray, int objectFlag);
EXTERN long sat_AddUnitConflictClause( satManager_t *cm, satArray_t *clauseArray, int objectFlag);
EXTERN void sat_FreeQueue( satQueue_t *Q );
EXTERN void sat_ClauseDeletion(satManager_t *cm);
EXTERN void sat_FreeLiteralsDB(satLiteralDB_t *literals);
EXTERN void sat_CompactFanout(satManager_t *cm);
EXTERN void sat_MarkTransitiveFaninForArray( satManager_t *cm, satArray_t *arr, unsigned int mask);
EXTERN void sat_MarkTransitiveFaninForNode( satManager_t *cm, long v, unsigned int mask);
EXTERN void sat_UnmarkTransitiveFaninForArray( satManager_t *cm, satArray_t *arr, unsigned int mask, unsigned int resetMask);
EXTERN void sat_FreeInterface(satInterface_t *interface);
EXTERN void sat_FreeOption(satOption_t * option);
EXTERN void sat_FreeStatistics(satStatistics_t * stats);
EXTERN int sat_ConflictAnalysisForCoreGen( satManager_t *cm, satLevel_t *d);
EXTERN void sat_MarkNodeInConflictClauseNoObj( satManager_t *cm, satLevel_t *d, int *nMarked, int *oFlag, int *bLevel, satArray_t *clauseArray);
EXTERN void sat_MarkNodeInImpliedNodeNoObj( satManager_t *cm, satLevel_t *d, long v, int *nMarked, int *oFlag, int *bLevel, satArray_t *clauseArray);
EXTERN void sat_MarkNodeSub( satManager_t *cm, long v, int *nMarked, int *bLevel, satLevel_t *d, satArray_t *clauseArray); 
EXTERN void sat_MarkNodeInImpliedNodeObjConservative( satManager_t *cm, satLevel_t *d, long v, int *nMarked, int *oFlag, int *bLevel, satArray_t *clauseArray);
EXTERN void sat_Undo(  satManager_t *cm, satLevel_t *d); 
EXTERN void sat_InitScore(satManager_t *cm);
EXTERN void sat_SaveNonobjClauses(satManager_t *cm);
EXTERN void sat_SaveAllClauses(satManager_t *cm);
EXTERN void sat_RestoreForwardedClauses(satManager_t *cm, int objectFlag);
EXTERN void sat_ApplyForcedAssignmentMain( satManager_t *cm, satLevel_t *d);
EXTERN int sat_ApplyForcedAssigment( satManager_t *cm, satArray_t *arr, satLevel_t *d);
EXTERN long sat_AddUnitClause( satManager_t *cm, satArray_t *clauseArray);
EXTERN long sat_AddClauseIncremental( satManager_t *cm, satArray_t *clauseArray, int objectFlag, int fromDistill);
EXTERN long sat_AddClause( satManager_t *cm, satArray_t *clauseArray);
EXTERN long sat_AddBlockingClause( satManager_t *cm, satArray_t *clauseArray);
EXTERN void sat_CompactClauses(satManager_t *cm);
EXTERN void sat_UnmarkTransitiveFaninForNode( satManager_t *cm, long v, unsigned int mask, unsigned int resetMask) ;
EXTERN void sat_IncrementalUsingDistill(satManager_t *cm);
EXTERN void sat_UpdateScore( satManager_t *cm);
EXTERN int sat_ReadCNF(satManager_t *cm, char *filename);
EXTERN void sat_ReportStatistics( satManager_t *cm, satStatistics_t *stats); 
EXTERN void sat_DeleteClause( satManager_t *cm, long v);
EXTERN int sat_MemUsage(satManager_t *cm);
EXTERN long sat_GetCanonical(satManager_t *cm, long v);
EXTERN void sat_PrintClauseLitsForCore(satManager_t * cm, long concl, FILE *fp);
EXTERN void sat_PrintClauseLits(satManager_t * cm, long concl);
EXTERN void sat_GenerateCoreRecur(satManager_t * cm, long concl, FILE *fp, int * count);
EXTERN void sat_GetDependence(satManager_t * cm, long concl, satArray_t* dep);
EXTERN void sat_GenerateCore(satManager_t * cm);
EXTERN void sat_PrintUnitLiteralClauses( satManager_t *cm, satArray_t *arr, FILE *fout);
EXTERN void sat_CountUnitLiteralClauses( satManager_t *cm, satArray_t *arr, int *nCl);
EXTERN void sat_WriteCNFWithPointer(satManager_t *cm, FILE *fout);
EXTERN void sat_WriteCNF(satManager_t *cm, char *filename);
EXTERN void sat_PrintUnitLiteralClauses( satManager_t *cm, satArray_t *arr, FILE *fout);
EXTERN void sat_CountUnitLiteralClauses( satManager_t *cm, satArray_t *arr, int *nCl);
EXTERN void sat_WriteCNFWithPartialAssignment(satManager_t *cm, char *filename);
EXTERN void sat_TrieBasedImplication( satManager_t *cm, satArray_t *trieArray, int depth);
EXTERN void sat_FreeTrie(satManager_t *cm, satArray_t *arr);
EXTERN satLevel_t * sat_DecisionBasedOnTrie( satManager_t *cm, long v, int value);
EXTERN void sat_TrieBasedImplication( satManager_t *cm, satArray_t *trieArray, int depth);
EXTERN void sat_ConflictAnalysisOnTrie( satManager_t *cm, satLevel_t *d);
EXTERN void sat_BuildTrie( satManager_t *cm, satArray_t *trieArray, long *plit, int depth);
EXTERN void sat_FreeTrie(satManager_t *cm, satArray_t *arr);
EXTERN void sat_PrintFlag(satManager_t *cm, long v);
EXTERN void sat_PrintLiteral(satManager_t *cm, long lit);
EXTERN void sat_CheckFlagsOnConflict(satManager_t *cm);
EXTERN void sat_PrintDotForConflict( satManager_t *cm, satLevel_t *d, long conflict, int includePreviousLevel);
EXTERN void sat_PrintDotForImplicationGraph( satManager_t *cm, satLevel_t *d, satArray_t *root, int includePreviousLevel);
EXTERN void sat_PrintDotForWholeGraph( satManager_t *cm, satLevel_t *d, int includePreviousLevel) ;
EXTERN void sat_PrintDotForImplicationGraph( satManager_t *cm, satLevel_t *d, satArray_t *root, int includePreviousLevel);
EXTERN void sat_CheckNonobjConflictClause( satManager_t *cm, long v);
EXTERN void sat_CheckNonobjUnitClause( satManager_t *cm);
EXTERN void sat_CheckInitialCondition( satManager_t *cm);
EXTERN void sat_PrintClauseArray( satManager_t *cm, satArray_t *clauseArray);
EXTERN void sat_CheckConflictClause( satManager_t *cm, satArray_t *clauseArray) ;
EXTERN void sat_ImplyUnitPureLitsWithAnte(satManager_t * cm, satLevel_t *d);
EXTERN long sat_DecisionBasedOnShrink( satManager_t *cm);
EXTERN void sat_CheckOrderedVariableArray(satManager_t *cm);
EXTERN void sat_GetConflictAsConflictClause( satManager_t *cm, satArray_t *clauseArray);
EXTERN void sat_CheckForwardedClauses(satManager_t *cm);
EXTERN void sat_TryToBuildMonolithicBDD(satManager_t *cm);
EXTERN void sat_FindUIPAndNonUIP( satManager_t *cm, satArray_t *clauseArray, satLevel_t *d, int *objectFlag, int *bLevel, long *fdaLit);
EXTERN long sat_AddConflictClauseNoScoreUpdate( satManager_t *cm, satArray_t *clauseArray, int objectFlag);
EXTERN void sat_ClauseDeletionLatestActivity(satManager_t *cm);
EXTERN int sat_ConflictAnalysisUsingAuxImplication( satManager_t *cm, satArray_t *clauseArray); 
EXTERN int sat_AddConflictClauseAndBacktrack( satManager_t *cm, satArray_t *clauseArray, satLevel_t *d, long fdaLit, int bLevel, int objectFlag, int strongFlag);
EXTERN void sat_RestoreBlockingClauses(satManager_t *cm);
EXTERN void sat_RestoreFrontierClauses(satManager_t *cm);
EXTERN void sat_CollectBlockingClause(satManager_t *cm);
EXTERN void sat_PreProcessingForMixed(satManager_t *cm);
EXTERN satLevel_t * sat_MakeDecision(satManager_t *cm);
EXTERN satLevel_t * sat_AllocLevel( satManager_t *cm);
EXTERN int sat_AddConflictClauseWithNoScoreAndBacktrack( satManager_t *cm, satArray_t *clauseArray, satLevel_t *d, long fdaLit, int bLevel, int objectFlag, int strongFlag);
EXTERN void sat_InitScoreForMixed(satManager_t *cm);
EXTERN satArray_t *sat_ArrayDuplicate(satArray_t *old);
EXTERN int sat_ConflictAnalysisWithBlockingClause( satManager_t *cm, satLevel_t *d);
EXTERN int sat_ConflictAnalysisForLifting( satManager_t *cm, satLevel_t *d);
EXTERN int sat_AddConflictClauseAndBacktrackForLifting( satManager_t *cm, satArray_t *clauseArray, satLevel_t *d, long fdaLit, int bLevel, int objectFlag, int strongFlag);
EXTERN void sat_PreProcessingForMixedNoCompact(satManager_t *cm);
EXTERN int sat_CNFMainWithArray( satOption_t *option, satArray_t *cnfArray, int unsatCoreFlag, satArray_t *coreArray, st_table *mappedTable);
EXTERN int sat_WriteCNFFromArray(satArray_t *cnfArray, char *filename);
EXTERN int sat_ReadCNFFromArray( satManager_t *cm, satArray_t *cnfArray, st_table *mappedTable);
EXTERN void sat_RestoreClauses(satManager_t *cm, satArray_t *cnfArray);
EXTERN satQueue_t * sat_CreateQueue( long MaxElements );



/*Bing: for AROSAT*/
EXTERN void sat_ASUpdateScore(satManager_t *cm);
EXTERN void sat_ASmergeLevel(satManager_t *cm);
EXTERN int sat_CE_CNF(satManager_t *cm,satLevel_t *d,
               int v,satArray_t *wl);
EXTERN int sat_CE(satManager_t *cm,satLevel_t *d,
           long v,int dfs,int value);
EXTERN int sat_ASDec(satManager_t *cm,satLevel_t *d,long v);
EXTERN int sat_ASImp(satManager_t *cm,satLevel_t *d,long v,int value);

/**AutomaticEnd**************************************************************/

#endif /* _SAT */