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