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

Last change on this file since 50 was 14, checked in by cecile, 13 years ago

vis2.3

File size: 42.5 KB
Line 
1/**CHeaderFile*****************************************************************
2
3  FileName    [sat.h]
4
5  PackageName [sat]
6
7  Synopsis    []
8
9  Description [Internal data structures of the sat package.]
10
11  SeeAlso     []
12
13  Author      [HoonSang Jin ]
14
15  Copyright [ This file was created at the University of Colorado at
16  Boulder.  The University of Colorado at Boulder makes no warranty
17  about the suitability of this software for any purpose.  It is
18  presented on an AS IS basis.]
19
20  Revision    [$Id: sat.h,v 1.30 2009/04/12 00:14:11 fabio Exp $]
21
22******************************************************************************/
23
24#ifndef _SAT
25#define _SAT
26
27#include "util.h"
28#include "array.h"
29#include "st.h"
30#include "heap.h"
31#include "cudd.h"
32#include "stdio.h"
33/*Bing*/
34#include "puresat.h"
35//#include "satInt.h"
36
37
38/*---------------------------------------------------------------------------*/
39/* Constant declarations                                                     */
40/*---------------------------------------------------------------------------*/
41
42#define  bbAigValue     0   /* Index of value. */ 
43#define  bbAigFlags     1   /* Index of flag for this node.*/
44#define  bbAigLeft      2   /* Index of the left child */ 
45#define  bbAigRight     3   /* Index of the right child */ 
46#define  bbAigNFanout   4   /* Index of number of fanout.*/
47#define  bbAigFanout    5   /* Index of fanout pointer for this node.*/
48#define  bbAigCanonical 6   /* Index of canonical node for this node.*/
49#define  bbAigNext      7   /* Index of dummy for this node.*/
50/*Bing:*/
51#define  bAigClass     8
52
53
54/**
55 * Mask bit for each flags
56 **/
57/**
58 *                      1 1 1 1 1 1 1 1 1 1 2 2 2 2 2 2 2 2 2 2 3 3
59 *  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
60 *  |_| | | | | | | | | | | | | | | | | | | | | |
61 *   |  | | | | | | | | | | | | | | | | | | | | |
62 *   |  | | | | | | | | | | | | | | | | | | | | InCoreMask
63 *   |  | | | | | | | | | | | | | | | | | | | IsFrontierClause
64 *   |  | | | | | | | | | | | | | | | | | | IsBlockingClause
65 *   |  | | | | | | | | | | | | | | | | | Visited2
66 *   |  | | | | | | | | | | | | | | | | CanonicalBit
67 *   |  | | | | | | | | | | | | | | | IsSystem
68 *   |  | | | | | | | | | | | | | | IsConflict
69 *   |  | | | | | | | | | | | | | InUse
70 *   |  | | | | | | | | | | | | InQueue
71 *   |  | | | | | | | | | | | LeafNode
72 *   |  | | | | | | | | | | BDDSatisfied
73 *   |  | | | | | | | | | StaticLearn
74 *   |  | | | | | | | | NonObj
75 *   |  | | | | | | | Obj
76 *   |  | | | | | | New
77 *   |  | | | | | Visited
78 *   |  | | | | Coi
79 *   |  | | | IsCone
80 *   |  | | StateBit
81 *   |  | IsBDD   
82 *   |  IsCNF     
83 *   HValue
84 **/
85
86/*#define PreserveMask           0x0032681e*/
87/*Bing*/
88#define PreserveMask           0xff3a681e
89
90#define HValueMask             0x00000003
91#define ResetHValueMask        0xfffffffc
92
93/**
94 * If this mask bit is marked then the node is CNF node.
95 **/
96#define IsCNFMask              0x00000004
97#define ResetIsCNFMask         0xfffffffb
98
99/**
100 * If this mask bit is marked then the node is BDD node.
101 **/
102#define IsBDDMask              0x00000008
103#define ResetIsBDDMask         0xfffffff7
104
105
106/**
107 * If this mask bit is marked then the node is state variable.
108 **/
109#define StateBitMask           0x00000010
110#define ResetStateBitMask      0xffffffef
111
112/**
113 * If this mask bit is marked then the node is transitive fanin of
114 * certain variable.
115 **/
116#define IsConeMask             0x00000020
117#define ResetIsConeMask        0xffffffdf
118
119/**
120 * If this mask bit is marked then the node is under cone of influence of root
121 * node. To be implied by BCP this flag bit has to be set.
122 **/
123#define CoiMask                0x00000040
124#define ResetCoiMask           0xffffffbf
125
126/**
127 * If this mask bit is marked then the node is visited.
128 **/
129#define VisitedMask            0x00000080
130#define ResetVisitedMask       0xffffff7f
131
132/**
133 * If this mask bit is marked then the node is visited.
134 * It can be used like a VisitedMask.
135 **/
136#define NewMask                0x00000100
137#define ResetNewMask           0xfffffeff
138
139/**
140 * If this mask bit is marked then the node is object dependent.
141 * It is used to identify object dependent conflict clause while
142 * applying incremental SAT.
143 **/
144#define ObjMask                0x00000200
145#define ResetObjMask           0xfffffdff
146
147/**
148 * If this mask bit is marked then the node is object independent.
149 * It is used to identify object independent conflict clause while
150 * applying incremental SAT.
151 **/
152#define NonobjMask             0x00000400
153#define ResetNonobjMask        0xfffffbff
154
155
156/**
157 * If this mask bit is marked then the value of node is fixed by static
158 * learning.
159 **/
160#define StaticLearnMask        0x00000400
161#define ResetStaticLearnMask   0xfffffbff
162
163/**
164 * If this mask bit is marked then the BDD node is satisfied by partial
165 * or full assignment on support variables.
166 * This flag bit is used for BDD node only, which means that IsBDDMask
167 * has to be set.
168 **/
169#define BDDSatisfiedMask       0x00000800
170#define ResetBDDSatisfiedMask  0xfffff7ff
171
172/**
173 * If this mask bit is marked then the node is support variable of
174 * BDD node.
175 **/
176#define LeafNodeMask           0x00001000
177#define ResetLeafNodeMask      0xffffefff
178
179/**
180 * If this mask bit is marked then the node is in implication queue.
181 * To avoid to put same node multiple times, it is set when the node is
182 * in the queue.
183 **/
184#define InQueueMask            0x00002000
185#define ResetInQueueMask       0xffffdfff
186
187/**
188 * If this mask bit is marked then the clause is in use.
189 * This flag bit can be set for CNF node only.
190 **/
191#define InUseMask              0x00004000
192#define ResetInUseMask         0xffffbfff
193
194/**
195 * If this mask bit is marked then the clause is conflict clause.
196 * This flag bit can be set for CNF node only.
197 **/
198#define IsConflictMask         0x00008000
199#define ResetIsConflictMask    0xffff7fff
200
201/**
202 * If this mask bit is marked then the node is part of original model.
203 * For example, BMC instance can be classified into system part and
204 * property part.
205 **/
206#define IsSystemMask           0x00010000
207#define ResetIsSystemMask      0xfffeffff
208
209/**
210 * If AIG nodes are identified as equivalent node, then they are merged
211 * into one of them. This mask bit is used identified the representative
212 * of those equivalent nodes.
213 **/
214#define CanonicalBitMask       0x00020000
215/**
216#define ResetCanonicalBitMask  0xfffdffff
217**/
218#define ResetCanonicalBitMask  ~0x00020000L
219
220/**
221 * If this mask bit is marked then the node is visited.
222 * It can be used like a VisitedMask.
223 **/
224#define Visited2Mask           0x00040000
225#define ResetVisited2Mask      0xfffbffff
226
227/**
228 * If this mask bit is marked then the clause is blocking clause
229 **/
230#define IsBlockingMask         0x00100000
231#define ResetIsBlockingMask    0xffefffff
232
233#define IsFrontierMask         0x00200000
234#define ResetIsFrontierMask    0xffdfffff
235
236#define InCoreMask             0x00400000
237#define ResetInCoreMask        0xffbfffff
238
239#define ResetNewVisitedObjMask 0xfffffc7f
240#define ResetNewVisitedObjInQueueMask 0xffffdc7f
241#define ResetNewVisitedMask    0xfffffe7f
242
243
244/*Bing: for interpolation*/
245#define VisibleVarMask         0x01000000
246#define ResetVisibleVarMask    0xfeffffff
247#define DummyMask              0x02000000
248#define ResetDummyMask         0xfdffffff
249#define Visited3Mask           0x04000000
250#define ResetVisited3Mask      0xfbffffff
251#define IsGlobalVarMask        0x08000000
252#define ResetGlobalVarMask     0xf7ffffff
253#define Visited4Mask           0x10000000
254#define ResetVisited4Mask      0xefffffff
255#define AssignedMask           0x20000000
256#define ResetAssignedMask      0xdfffffff
257/*pseudo global var*/
258
259#define PGVMask                0x40000000
260#define ResetPGVMask           0xbfffffff
261/*visible pseudo global var*/
262#define VPGVMask               0x00080000
263#define ResetVPGVMask          0xfff7ffff
264#define ResetVisited1234NewMask 0xebfbfe7f
265
266
267#define SAT_UNSAT 1
268#define SAT_SAT 2
269#define SAT_BACKTRACK 3
270#define SAT_BDD_UNSAT 4
271#define SAT_BDD_SAT 5
272#define SAT_BDD_BACKTRACK 6
273
274/*#define SATnodeID(node) ((node) >> 3)*/
275/*Bing:*/
276#define SATnodeID(node) (SATnormalNode(node)/satNodeSize)
277
278#define SATvalue(node) (cm->nodesArray[((node) &(~0x1L)) +satValue])
279
280
281/* For AIG */
282#define  satValue       bbAigValue     /* Index of value. */ 
283#define  satFlags       bbAigFlags     /* Index of flag for this node.*/
284#define  satLeft        bbAigLeft      /* Index of the left child */ 
285#define  satRight       bbAigRight     /* Index of the right child */ 
286#define  satNFanout     bbAigNFanout 
287#define  satFanout      bbAigFanout   
288#define  satCanonical   bbAigCanonical     /* Index of the right child */ 
289#define  satNext        bbAigNext     /* Index of the right child */ 
290
291/*Bing: for interpolation*/
292#define  satClass       bAigClass /* equals the timeframes it is in*/
293
294#define satNumLits  bbAigLeft
295#define satFirstLit bbAigRight
296#define satNumConflict    bbAigNext
297#define satConflictUsage  bbAigFanout
298
299/*#define satNodeSize 8*/
300/*Bing*/
301#define satNodeSize 12
302
303
304#define LATEST_CONFLICT_DECISION 0x1
305#define DVH_DECISION 0x2
306
307#define SATInvertBit 0x1
308/*Bing*/
309#define SATclass(node) (cm->nodesArray[SATnormalNode(node)+satClass])
310/*
311#define SATnext(node) (cm->nodesArray[node+satNext])
312
313
314#define SATcanonical(node) (cm->nodesArray[node+satCanonical])
315
316#define SATleftChild(node) (cm->nodesArray[node+satLeft])
317
318#define SATrightChild(node) (cm->nodesArray[node+satRight])
319
320#define SATfanout(node) ((long *)(cm->nodesArray[node+satFanout]))
321
322#define SATnFanout(node) (cm->nodesArray[node+satNFanout])
323*/
324/*Bing*/
325#define SATnext(node) (cm->nodesArray[SATnormalNode(node)+satNext])
326
327#define SATflags(node) (cm->nodesArray[SATnormalNode(node)+satFlags])
328
329#define SATcanonical(node) (cm->nodesArray[SATnormalNode(node)+satCanonical])
330
331#define SATleftChild(node) (cm->nodesArray[SATnormalNode(node)+satLeft])
332
333#define SATrightChild(node) (cm->nodesArray[SATnormalNode(node)+satRight])
334
335#define SATfanout(node) ((long *)(cm->nodesArray[SATnormalNode(node)+satFanout]))
336
337#define SATnFanout(node) (cm->nodesArray[SATnormalNode(node)+satNFanout])
338
339#define SATgetVariable(node) (&(cm->variableArray[SATnodeID(node)]))
340
341
342#define SATflags(node) (cm->nodesArray[SATnormalNode(node)+satFlags])
343
344
345#define SATgetNode(lit)  (lit >> 2)
346
347#define SATgetDir(lit) ((lit&0x03) - 2)
348
349#define SATisWL(lit) (lit&0x03)
350
351#define SATunsetWL(plit) ((*plit) = (*plit) & (0x0fffffffc))
352
353#define SATsetWL(plit, dir) ((*plit) = (*plit) + dir + 2)
354
355#define SATsetInUse(node)  (SATflags(node) |= InUseMask)
356
357#define SATreadInUse(node)  (SATflags(node) & InUseMask)
358
359#define SATresetInUse(node)  (SATflags(node) &= ResetInUseMask)
360
361#define SATgetValueChar(value) (value==0 ? '0' : (value==1 ? '1' : 'x'))
362
363
364#define SATnumConflict(node) (cm->nodesArray[node+satNumConflict])
365
366#define SATconflictUsage(node) (cm->nodesArray[node+satConflictUsage])
367
368
369#define SATlevel(node)(\
370cm->variableArray[SATnodeID(node)].level\
371)
372
373#define SATante(node)(\
374cm->variableArray[SATnodeID(node)].antecedent\
375)
376
377#define SATante2(node)(\
378cm->variableArray[SATnodeID(node)].antecedent2\
379)
380
381#define SATgetValue(left, right, v)     \
382  ( ((SATvalue(SATnormalNode(left)) ^ SATisInverted(left)) << 4) | \
383    ((SATvalue(SATnormalNode(right)) ^ SATisInverted(right)) << 2) | \
384    (SATvalue(v)))
385
386#define SATmakeImplied(v, d)                              \
387    ( sat_ArrayInsert(d->implied, v),     \
388      SATlevel(v) = d->level)
389
390
391#define SATgetDecision(level) (&(cm->decisionHead[level]))
392
393/*#define SATflags(node) (cm->nodesArray[node+satFlags])*/
394
395#define SATnormalNode(node) ((node) & (~0x1L))
396
397#define SATnot(node) ((node) ^ SATInvertBit)
398
399#define SATisInverted(node) ((node) & (SATInvertBit))
400
401#define SATnumLits(node) (cm->nodesArray[node+satNumLits])
402
403#define SATfirstLit(node) (cm->nodesArray[node+satFirstLit])
404
405
406
407
408/*---------------------------------------------------------------------------*/
409/* Type declarations                                                         */
410/*---------------------------------------------------------------------------*/
411
412typedef struct satManagerStruct         satManager_t;
413typedef struct satInterfaceStruct       satInterface_t;
414typedef struct satStatisticsStruct      satStatistics_t;
415typedef struct satOptionStruct          satOption_t;
416typedef struct satQueueStruct           satQueue_t;
417typedef struct satArrayStruct           satArray_t;
418typedef struct satLiteralDBStruct       satLiteralDB_t;
419typedef struct satLevelStruct           satLevel_t;
420typedef struct satVariableStruct        satVariable_t;
421typedef struct satTrieStruct            satTrie_t;
422
423typedef struct satLinearHeadStruct      satLinearHead_t;
424typedef struct satLinearVarStruct       satLinearVar_t;
425typedef struct satLinearElemStruct      satLinearElem_t;
426typedef struct satLinearClusterStruct   satLinearCluster_t;
427
428
429/*---------------------------------------------------------------------------*/
430/* Structure declarations                                                    */
431/*---------------------------------------------------------------------------*/
432
433/**Struct**********************************************************************
434
435  Synopsis    [A struct for manager for CirCUs.]
436
437******************************************************************************/
438struct satManagerStruct {
439    struct satOptionStruct *option; 
440    struct satTimeFrameStruct *timeframe;
441    struct satTimeFrameStruct *timeframeWOI;
442    struct satLiteralDBStruct *literals;
443
444    struct satStatisticsStruct *total; /* to gather statistics on set of SAT runs.*/
445    struct satStatisticsStruct *each;  /* to save statistics of one SAT run. */
446
447    struct satQueueStruct *queue;  /* implication queue. */
448    struct satQueueStruct *BDDQueue; /* implication queue for BDD */
449    struct satQueueStruct *unusedAigQueue; /* queue for unused AIG for CNF. */
450
451    long *nodesArray;
452    long *HashTable;
453    long nodesArraySize;
454    long maxNodesArraySize; /* These 4 fields are used as in bAigManager_t.
455                             * We copy it to isolate code of CirCUs from
456                             * baig package. When one build a interface
457                             * for CirCUs you have to copy back these
458                             * fields to bAig_Manager_t structure after
459                             * SAT solving. */
460
461    long beginConflict;   /* to save the beginning of conflict learned clauses. */
462    long initNodesArraySize; /* to save the initial AIG structure size.*/
463
464    struct satVariableStruct *variableArray; /* the array of satVariable_t. */
465
466    /* These 7 arrays are the array of AIG nodes.
467    * If the AIG node is inverted then it will be asserted to be '0'.
468    * Otherwise it is asserted to be '1'. */
469    struct satArrayStruct *auxObj;    /* the array of auxiliary objectives  */
470    struct satArrayStruct *obj;       /* the array of objective literal */
471    struct satArrayStruct *objCNF;    /* the array of objective clause */
472    struct satArrayStruct *assertion; /* the array of assertion */
473                                 /* it is now used to save static learned node. */
474    struct satArrayStruct *unitLits;  /* the array of unit literals for CNF */
475    struct satArrayStruct *pureLits;  /* the array of pure literals for CNF */
476    struct satArrayStruct *nonobjUnitLitArray; 
477                 /* to save unit objective independent conflict clauses
478                 * it is for incremental SAT. */
479    struct satArrayStruct *objUnitLitArray;
480                 /* to save unit objective dependent conflict clauses
481                 * it is for incremental SAT. */
482   
483   
484    struct satLevelStruct *decisionHead; /* the array of satLevel_t. */
485    int decisionHeadSize;                /* the size of *decisionHead.*/
486    int currentDecision;                 
487                 /* to represent the current decision level */
488
489    struct satArrayStruct *assignByBDD;
490    struct satArrayStruct *orderedVariableArray;
491                 /* the array of AIG nodes that are the variables.
492                 * It is for score based decision heuristic. */
493    int currentVarPos;
494                 /* to represent the index of orderedVariableArray that
495                 * is not assigned yet. */
496
497    struct satArrayStruct *savedConflictClauses;
498                 /* to save the conflict clauses that can be forwarded
499                 * when we apply incremental SAT */
500    struct satArrayStruct *trieArray;
501                 /* to save the trie to apply distillation method
502                 * when we apply incremental SAT */
503    struct satArrayStruct *auxArray;
504                 /* Can be used to save arbitrary array */
505
506    long *currentTopConflict;   
507                 /* to save current top clause
508                 * based on the definition of BerkMin */
509    int currentTopConflictCount;
510
511    int lowestBacktrackLevel;
512                 /* to save lowest backtrack level */
513    char *comment;
514
515    int initNumVariables; /* the number of initial variables. */
516    int initNumClauses;   /* the number of initial clauses. */
517    int initNumLiterals;  /* the number of initial literals. */
518    int implicatedSoFar; /* the number of implied node so far, which sum of all implied nodes. */
519
520    FILE *stdErr;
521    FILE *stdOut;
522
523    int status; /* the status of SAT solving result
524                * SAT_BACKTRACK, SAT_SAT, SAT_UNSAT. */
525   
526    struct satArrayStruct *dormantConflictArray;
527    struct satArrayStruct *shrinkArray;
528    int shrinkEnable;
529    int shrinkSize;
530    int forceLatestConflictDecision;
531    DdManager *mgr;
532
533    struct satArrayStruct *frontier;
534    struct satArrayStruct *reached;
535    long frontierNodesBegin;
536    long frontierNodesEnd;
537    struct satArrayStruct *clauseIndexInCore;
538
539 
540    /* BING : for conflcit core generation */
541    st_table * dependenceTable;
542    st_table *anteTable;
543    struct satArrayStruct * dependenceArray;
544    int numOfClsInCore;
545    FILE *fp, *fp2;
546
547  /*Bing:*/
548  IP_Manager_t * ipm;
549  st_table * RTreeTable;/* ConClsIdx->RT ptr */
550
551  satArray_t * assertArray, *assertArray2, *CoiAssertArray, *EqArray;
552  int class_;
553  long InitState, IPState, property;
554  satArray_t * tmpArray;
555  st_table * table;
556  int test;
557  RTManager_t * rm;
558  /*for AROSAT*/
559  st_table * layerTable;
560  int OriLevel, LatchLevel;
561  int *numArray,*assignedArray;
562  int currentLevel;
563  int Length;
564  int line;
565 
566};
567
568/**Struct**********************************************************************
569
570  Synopsis    [A struct to interface CirCUs and application.
571               One can freely add a field based on his need.]
572
573******************************************************************************/
574struct satInterfaceStruct {
575    struct satStatisticsStruct *total;
576    struct satArrayStruct *nonobjUnitLitArray;
577    struct satArrayStruct *objUnitLitArray;
578    struct satArrayStruct *savedConflictClauses;
579    struct satArrayStruct *trieArray;
580    int status;
581};
582
583/**Struct**********************************************************************
584
585  Synopsis    [A struct to gather CirCUs statistics ]
586
587******************************************************************************/
588struct satStatisticsStruct {
589    int nBacktracks;                /* the number of backtracks */
590    int nNonchonologicalBacktracks; /* the sum of backtrack levels */
591    int nDecisions;                 /* the number of decisions */
592    int nDVHDecisions;              /* the number of decisions by DVH */
593    int nVSIDSDecisions;            /* the number of decisions by VSIDS */
594    int nShrinkDecisions;           
595    int nLatestConflictDecisions;   /* the number of decisions by current top clause */
596    int maxDecisionLevel;           /* the maximum decision level */
597    int nLowScoreDecisions;         /* the number of decision without sufficient information. */
598
599    int nCNFImplications;           /* the number of implication done by CNF */
600    int nAigImplications;           /* the number of implication done by AIG */
601    int nBDDImplications;           /* the number of implication done by BDD */
602    int nHyperImplications;
603
604    int nUnitConflictCl;            /* the number of unit conflict clauses */
605    int nOldConflictCl; 
606    int nConflictCl;                /* the number of conflict clauses   */
607    int nConflictLit;               /* the sum of literals in conflict clauses  */
608    int nObjConflictCl;             /* the number of object dependent conflict clauses   */
609    int nObjConflictLit;            /* the sum of literals in object dependent conflict clauses  */
610    int nNonobjConflictCl;          /* the number of object independent conflict clauses  */ 
611    int nNonobjConflictLit;          /* the sum of literals in object dependent conflict clauses  */
612    int nInitObjConflictCl;         /* the number of conflict clauses  forwarded from previous run */
613    int nInitObjConflictLit;        /* the sum of literals in conflict clauses forwarded from previous run */
614    int nInitNonobjConflictCl;
615    int nInitNonobjConflictLit;
616    int nDistillObjConflictCl;
617    int nDistillObjConflictLit;
618    int nDistillNonobjConflictCl;
619    int nDistillNonobjConflictLit;
620    int nDeletedCl;                 /* the number of conflict clauses deleted */
621    int nDeletedLit;                /* the sum of literals in conflict clauses deleted */
622    int nBlockingCl;                 /* the number of blocking clauses deleted */
623    int nBlockingLit;                /* the sum of literals in blocking clauses deleted */
624    int nDeletedButUncompacted;
625    double satTime;
626};
627
628/**Struct**********************************************************************
629
630  Synopsis    [A struct to set option for CirCUs statistics ]
631
632******************************************************************************/
633struct satOptionStruct {
634    int verbose;
635    int decisionHeuristic;      /* to select decision heuristic */
636    int decisionAgeInterval;    /* to set aging interval */
637    int decisionAgeRestart;     /* to turn on/off restart after aging */
638
639    int clauseDeletionHeuristic; /* to select clause deletion heuristic */
640    int clauseDeletionInterval;  /* to set clause deletion interval */
641    int nextClauseDeletion;
642
643    int incTraceObjective;       /* to turn on/off incremental SAT by trace objective */
644    int incDistill;              /* to turn on/off incremental SAT by distillation */
645    int incAll;
646    int incNumObjLitsLimit;      /* to limit the number literals in objective dependent cluases that can be forwarded by incremental SAT */
647    int incNumNonobjLitsLimit;   /* to limit the number literals in objective independent cluases that can be forwarded by incremental SAT */
648    int incPreserveNonobjective; /* to keep the objective independent clause while apply clause deletion */
649
650    int aig2BDDOn;               /* convert AIG into BDD when it is advantageous */
651    int BDDRecondition;          /* extract clause from BDDs by prime implication generation */
652    int BDDMonolithic;           /* build monolithic BDD for clauses */
653    int BDDDPLL;                 /* combine BDD and DPLL procedure */
654    int BDDImplication;          /* apply BDD based implication */
655
656    int includeLevelZeroLiteral; /* do add literals implied in level zero When append conflict learned clause  */
657    int minimizeConflictClause;  /* apply conflict clause minimization procedure */
658    int shrinkConflictClause;    /* apply conflict shrinking method done by JeruSAT */
659    int unrelevance;             /* set the unrelevance of conflict clause when applying clause deletion  */
660    int minLitsLimit;            /* If the number of literals in clause less than this value then keep it when applying clause deletion  */
661    int maxLitsLimit;            /* If the number of literals in clause more than this value then delete it when applying clause deletion */
662
663    int latestUsage;
664    int obsoleteUsage;
665    int latestUnrelevance;
666    int obsoleteUnrelevance;
667    int latestRate;
668
669    int restartInterval;
670
671    int memoryLimit;
672    int timeoutLimit;
673
674    int minConflictForDecision;         /* to avoid too small clause when deciding current top clause */
675    int maxConflictForDecision;         /* to avoid too large clause when deciding current top clause */
676    int skipSatisfiedClauseForDecision; /* to skip satified clause when deciding current top clause */
677
678    int maxLimitOfClausesForMonolithicBDD;
679    int maxLimitOfVariablesForMonolithicBDD;
680    int maxLimitOfCutSizeForMonolithicBDD;
681
682    int maxLimitOfClausesForBDDDPLL;
683    int maxLimitOfVariablesForBDDDPLL;
684    int maxLimitOfCutSizeForBDDDPLL;
685
686    int maxLimitOfVariablesForBDD;
687
688    int interfaceCNF;            /* to write CNF instead of running CirCUs */
689    int cnfPrefix;
690    int runOtherSolver;          /* run other CNF solver after writing CNF */
691    char *otherSolverName;       /* specify the SAT solver name */
692
693    int newConflictAnalysis;
694    int checkNonobjForwarding;
695
696    char *outFilename;
697    struct satArrayStruct *forcedAssignArr;
698
699 
700    char * unsatCoreFileName;
701 
702    int allSatMode;
703    int useStrongConflictAnalysis; /* triggering strong conflict analysis */
704 
705    /* Bing: UNSAT core generation */
706    int coreGeneration;
707  /*Bing*/
708  int IP;
709  int SSS;
710
711  int arosat;
712  int AbRf;
713  int RT;
714  int ForceFinish;
715};
716
717
718/**Struct**********************************************************************
719
720  Synopsis    [A struct for queue]
721
722******************************************************************************/
723struct satQueueStruct {
724    long max;         /* max size of queue */
725    long size;        /* the number of current entries */
726    long front;       /* front index of entries */
727    long rear;        /* rear index of entries */
728    long *array;      /* the location to save entries */
729};
730
731/**Struct**********************************************************************
732
733  Synopsis    [A struct for array]
734
735******************************************************************************/
736struct satArrayStruct {
737    long *space;     /* the location to save entries */
738    long num;        /* the number of entries */
739    long size;       /* the size of space */
740};
741
742/**Struct**********************************************************************
743
744  Synopsis    [A struct to save lterals]
745
746******************************************************************************/
747struct satLiteralDBStruct {
748  long *begin;       /* the begin pointer of literal database */
749  long *last;        /* the pointer of last literal */
750  long *end;         /* the end pointer of literal database */
751  long *initialSize; /* the pointer of last literals that is given as input */
752};
753
754/**Struct**********************************************************************
755
756  Synopsis    [A struct for decision level]
757
758******************************************************************************/
759struct satLevelStruct {
760  int level;          /* decision level  */
761  long decisionNode;   /* decision node of this level  */
762  long conflict;       /* the conflict that happens from implication  */
763  struct satArrayStruct *implied;  /* the array of implied nodes  */
764  struct satArrayStruct *satisfied; /* the array of satisfied BDD nodes  */
765  int currentVarPos;                /* the index of decision node in orderedVariableArray  */
766  int nConflict;
767};
768
769/**Struct**********************************************************************
770
771  Synopsis    [A struct for variable]
772
773******************************************************************************/
774struct satVariableStruct {
775  int level;            /* the decision level that make implication on this variable */
776  int scores[2];        /* score for both phase   */           
777  int litsCount[2];     /* the location to save literal count */
778  int lastLitsCount[2]; /* last literal count */
779  int conflictLits[2];  /* literal count of literals in conflict clause */
780  long antecedent;      /* antecedent */
781  long antecedent2;     /* antecedent */
782  int pos;              /* position in orderedVariableArray */
783  int depth;            /* depth of variable in implication graph */
784  struct satArrayStruct *wl[2]; /* watched literal list */
785 
786  /*Bing: for AROSAT*/
787  int RecVal;  /*1 for one, -1 for zero, 0 for not recorded*/
788};
789
790/**Struct**********************************************************************
791
792  Synopsis    [A struct for trie]
793
794******************************************************************************/
795struct satTrieStruct {
796  long id;                           /* node id */
797  struct satArrayStruct *child[2];  /* childrun */
798  int depth;                        /* depth from root */
799};
800
801struct satLinearElemStruct {
802  double pos;
803  int order;
804  int num;
805  struct satArrayStruct *support;
806  long node; 
807  DdNode *bdd;
808  int flag;
809  int to;
810  struct satLinearElemStruct *next;
811};
812
813struct satLinearVarStruct {
814  double pos;
815  int order;
816  int from;
817  int to;
818  struct satArrayStruct *clauses;
819  long node;
820  DdNode *bdd;
821  int bQuantified;
822  struct satLinearVarStruct *next;
823};
824
825struct satLinearHeadStruct {
826  DdManager *mgr;
827  struct satLinearElemStruct *elemHead;
828  struct satLinearVarStruct *varHead;
829  int nVars;
830  int nCls;
831  int bddLimit;
832  int bddAndLimit;
833  long *id2edge;
834  int *edge2id;
835  int *edge2vid;
836  Heap_t *heap;
837  struct satArrayStruct *elemArray;
838  struct satArrayStruct *varArray;
839  struct satArrayStruct *clausesArray;
840  struct satArrayStruct *variablesArray;
841  struct satArrayStruct *latestClusterArray;
842  struct satArrayStruct *deadArray;
843  int reordering;
844};
845
846struct satLinearClusterStruct {
847  struct satLinearElemStruct *elem1;
848  struct satLinearElemStruct *elem2;
849  int flag;
850  int cost;
851  int overlap;
852  struct satArrayStruct *deadArray;
853};
854
855
856
857/*---------------------------------------------------------------------------*/
858/* Variable declarations                                                     */
859/*---------------------------------------------------------------------------*/
860
861
862/*---------------------------------------------------------------------------*/
863/* Macro declarations                                                        */
864/*---------------------------------------------------------------------------*/
865
866
867/*---------------------------------------------------------------------------*/
868/* Function prototypes                                                       */
869/*---------------------------------------------------------------------------*/
870EXTERN satManager_t * sat_InitManager(satInterface_t *interface);
871EXTERN satArray_t * sat_ArrayAlloc(long number);
872EXTERN satStatistics_t * sat_InitStatistics(void);
873EXTERN satOption_t * sat_InitOption(void);
874EXTERN satArray_t * sat_ReadForcedAssignment( char *filename);
875EXTERN int sat_GetNumberOfInitialClauses(satManager_t *cm);
876EXTERN int sat_GetNumberOfInitialVariables(satManager_t *cm);
877EXTERN satLevel_t * sat_AllocLevel( satManager_t *cm);
878EXTERN int sat_ConflictAnalysis( satManager_t *cm, satLevel_t *d); 
879EXTERN int sat_StrongConflictAnalysis( satManager_t *cm, satLevel_t *d); 
880EXTERN void sat_CombineStatistics(satManager_t *cm);
881EXTERN long sat_GetClauseFromLit( satManager_t *cm, long *lit);
882EXTERN long sat_DecisionBasedOnBDD( satManager_t *cm, satLevel_t *d);
883EXTERN long sat_DecisionBasedOnLatestConflict( satManager_t *cm, satLevel_t *d);
884EXTERN long sat_DecisionBasedOnScore( satManager_t *cm, satLevel_t *d);
885EXTERN void sat_CheckDecisonVariableArray( satManager_t *cm);
886EXTERN void sat_FreeManager(satManager_t *cm);
887EXTERN void sat_ArrayInsert(satArray_t *array, long datum);
888EXTERN void sat_SetIncrementalOption(satOption_t *option, int incFlag);
889EXTERN void sat_RestoreFanout(satManager_t *cm);
890EXTERN int sat_GetFanoutSize( satManager_t *cm, long v);
891EXTERN void sat_CleanLevel(satLevel_t *d);
892EXTERN void sat_CleanDatabase(satManager_t *cm);
893EXTERN void sat_SetConeOfInfluence(satManager_t *cm);
894EXTERN void sat_BuildTrieForDistill(satManager_t *cm) ;
895EXTERN void sat_AllocLiteralsDB(satManager_t *cm) ;
896EXTERN void sat_ArrayFree(satArray_t *array);
897EXTERN void sat_PrintScore(satManager_t *cm);
898EXTERN void sat_PutAssignmentValueMain( satManager_t *cm, satLevel_t *d, satArray_t *arr);
899EXTERN void sat_Main(satManager_t *cm);
900EXTERN void sat_FindUIP( satManager_t *cm, satArray_t *clauseArray, satLevel_t *d, int *objectFlag, int *bLevel, long *fdaLit);
901EXTERN void sat_FindUIPWithRT( satManager_t *cm, satArray_t *clauseArray, satLevel_t *d, int *objectFlag, int *bLevel, long *fdaLit);
902EXTERN void sat_MarkNodeInConflictClauseObjConservative( satManager_t *cm, satLevel_t *d, int *nMarked, int *oFlag, int *bLevel, satArray_t *clauseArray);
903EXTERN void sat_PrintImplicationGraph( satManager_t *cm, satLevel_t *d);
904EXTERN void sat_PrintNodeAlone(satManager_t *cm, long v);
905EXTERN void sat_PrintNode( satManager_t *cm, long v);
906EXTERN void sat_Backtrack( satManager_t *cm, int level);
907EXTERN void sat_PrintDotForConflict( satManager_t *cm, satLevel_t *d, long conflict, int includePreviousLevel);
908EXTERN long sat_AddUnitConflictClause( satManager_t *cm, satArray_t *clauseArray, int objectFlag);
909EXTERN void sat_Enqueue(satQueue_t *Q, long v);
910EXTERN long sat_AddConflictClause( satManager_t *cm, satArray_t *clauseArray, int objectFlag);
911EXTERN long sat_AddConflictClauseWithoutScoring( satManager_t *cm, satArray_t *clauseArray, int objectFlag);
912EXTERN void sat_UpdateDVH( satManager_t *cm, satLevel_t *d, satArray_t *clauseArray, int bLevel, long unitLit);
913EXTERN void sat_FindUIPForCoreGen( satManager_t *cm, satArray_t *clauseArray, satLevel_t *d, int *objectFlag, int *bLevel, long *fdaLit);
914EXTERN void sat_FindUIPForCoreGenWithRT( satManager_t *cm, satArray_t *clauseArray, satLevel_t *d, int *objectFlag, int *bLevel, long *fdaLit);
915EXTERN void sat_MarkNodeInConflict( satManager_t *cm, satLevel_t *d, int *nMarked, int *objectFlag, int *bLevel, satArray_t *clauseArray);
916EXTERN void sat_MarkNodeInImpliedNode( satManager_t *cm, satLevel_t *d, long v, int *nMarked, int *objectFlag, int *bLevel, satArray_t *clauseArray);
917EXTERN void sat_MinimizeConflictClause( satManager_t *cm, satArray_t *clauseArray);
918EXTERN void sat_ResetFlagForClauseArray( satManager_t *cm, satArray_t *clauseArray); 
919EXTERN void sat_ImplyCNF( satManager_t *cm, satLevel_t *d, long v, satArray_t *wl); 
920EXTERN int sat_ImplyNode( satManager_t *cm, satLevel_t *d, long v);
921EXTERN void sat_ImplicationMain( satManager_t *cm, satLevel_t *d);
922EXTERN void sat_CleanImplicationQueue( satManager_t *cm);
923EXTERN void sat_ImplyArray( satManager_t *cm, satLevel_t *d, satArray_t *arr);
924EXTERN void sat_ImplyBDD( satManager_t *cm, satLevel_t *d, long v);
925EXTERN void sat_BuildLevelZeroHyperImplicationGraph( satManager_t *cm);
926EXTERN void sat_PreProcessing(satManager_t *cm);
927EXTERN void sat_MarkObjectiveFlagToArray( satManager_t *cm, satArray_t *objArr);
928EXTERN void sat_PostProcessing(satManager_t *cm);
929EXTERN void sat_Solve(satManager_t *cm);
930EXTERN void sat_PeriodicFunctions(satManager_t *cm);
931EXTERN void sat_CNFMain(satOption_t *option, char *filename);
932EXTERN int sat_PrintSatisfyingAssignment(satManager_t *cm);
933EXTERN void sat_Verify(satManager_t *cm);
934EXTERN long sat_Dequeue( satQueue_t * Q );
935EXTERN long sat_CreateNode( satManager_t *cm, long left, long right);
936EXTERN int sat_EnlargeLiteralDB(satManager_t *cm);
937EXTERN void sat_AddWL( satManager_t *cm, long c, int index, int dir);
938EXTERN long sat_AddConflictClause( satManager_t *cm, satArray_t *clauseArray, int objectFlag);
939EXTERN long sat_AddUnitConflictClause( satManager_t *cm, satArray_t *clauseArray, int objectFlag);
940EXTERN void sat_FreeQueue( satQueue_t *Q );
941EXTERN void sat_ClauseDeletion(satManager_t *cm);
942EXTERN void sat_FreeLiteralsDB(satLiteralDB_t *literals);
943EXTERN void sat_CompactFanout(satManager_t *cm);
944EXTERN void sat_MarkTransitiveFaninForArray( satManager_t *cm, satArray_t *arr, unsigned int mask);
945EXTERN void sat_MarkTransitiveFaninForNode( satManager_t *cm, long v, unsigned int mask);
946EXTERN void sat_UnmarkTransitiveFaninForArray( satManager_t *cm, satArray_t *arr, unsigned int mask, unsigned int resetMask);
947EXTERN void sat_FreeInterface(satInterface_t *interface);
948EXTERN void sat_FreeOption(satOption_t * option);
949EXTERN void sat_FreeStatistics(satStatistics_t * stats);
950EXTERN int sat_ConflictAnalysisForCoreGen( satManager_t *cm, satLevel_t *d);
951EXTERN void sat_MarkNodeInConflictClauseNoObj( satManager_t *cm, satLevel_t *d, int *nMarked, int *oFlag, int *bLevel, satArray_t *clauseArray);
952EXTERN void sat_MarkNodeInImpliedNodeNoObj( satManager_t *cm, satLevel_t *d, long v, int *nMarked, int *oFlag, int *bLevel, satArray_t *clauseArray);
953EXTERN void sat_MarkNodeSub( satManager_t *cm, long v, int *nMarked, int *bLevel, satLevel_t *d, satArray_t *clauseArray); 
954EXTERN void sat_MarkNodeInImpliedNodeObjConservative( satManager_t *cm, satLevel_t *d, long v, int *nMarked, int *oFlag, int *bLevel, satArray_t *clauseArray);
955EXTERN void sat_Undo(  satManager_t *cm, satLevel_t *d); 
956EXTERN void sat_InitScore(satManager_t *cm);
957EXTERN void sat_SaveNonobjClauses(satManager_t *cm);
958EXTERN void sat_SaveAllClauses(satManager_t *cm);
959EXTERN void sat_RestoreForwardedClauses(satManager_t *cm, int objectFlag);
960EXTERN void sat_ApplyForcedAssignmentMain( satManager_t *cm, satLevel_t *d);
961EXTERN int sat_ApplyForcedAssigment( satManager_t *cm, satArray_t *arr, satLevel_t *d);
962EXTERN long sat_AddUnitClause( satManager_t *cm, satArray_t *clauseArray);
963EXTERN long sat_AddClauseIncremental( satManager_t *cm, satArray_t *clauseArray, int objectFlag, int fromDistill);
964EXTERN long sat_AddClause( satManager_t *cm, satArray_t *clauseArray);
965EXTERN long sat_AddBlockingClause( satManager_t *cm, satArray_t *clauseArray);
966EXTERN void sat_CompactClauses(satManager_t *cm);
967EXTERN void sat_UnmarkTransitiveFaninForNode( satManager_t *cm, long v, unsigned int mask, unsigned int resetMask) ;
968EXTERN void sat_IncrementalUsingDistill(satManager_t *cm);
969EXTERN void sat_UpdateScore( satManager_t *cm);
970EXTERN int sat_ReadCNF(satManager_t *cm, char *filename);
971EXTERN void sat_ReportStatistics( satManager_t *cm, satStatistics_t *stats); 
972EXTERN void sat_DeleteClause( satManager_t *cm, long v);
973EXTERN int sat_MemUsage(satManager_t *cm);
974EXTERN long sat_GetCanonical(satManager_t *cm, long v);
975EXTERN void sat_PrintClauseLitsForCore(satManager_t * cm, long concl, FILE *fp);
976EXTERN void sat_PrintClauseLits(satManager_t * cm, long concl);
977EXTERN void sat_GenerateCoreRecur(satManager_t * cm, long concl, FILE *fp, int * count);
978EXTERN void sat_GetDependence(satManager_t * cm, long concl, satArray_t* dep);
979EXTERN void sat_GenerateCore(satManager_t * cm);
980EXTERN void sat_PrintUnitLiteralClauses( satManager_t *cm, satArray_t *arr, FILE *fout);
981EXTERN void sat_CountUnitLiteralClauses( satManager_t *cm, satArray_t *arr, int *nCl);
982EXTERN void sat_WriteCNFWithPointer(satManager_t *cm, FILE *fout);
983EXTERN void sat_WriteCNF(satManager_t *cm, char *filename);
984EXTERN void sat_PrintUnitLiteralClauses( satManager_t *cm, satArray_t *arr, FILE *fout);
985EXTERN void sat_CountUnitLiteralClauses( satManager_t *cm, satArray_t *arr, int *nCl);
986EXTERN void sat_WriteCNFWithPartialAssignment(satManager_t *cm, char *filename);
987EXTERN void sat_TrieBasedImplication( satManager_t *cm, satArray_t *trieArray, int depth);
988EXTERN void sat_FreeTrie(satManager_t *cm, satArray_t *arr);
989EXTERN satLevel_t * sat_DecisionBasedOnTrie( satManager_t *cm, long v, int value);
990EXTERN void sat_TrieBasedImplication( satManager_t *cm, satArray_t *trieArray, int depth);
991EXTERN void sat_ConflictAnalysisOnTrie( satManager_t *cm, satLevel_t *d);
992EXTERN void sat_BuildTrie( satManager_t *cm, satArray_t *trieArray, long *plit, int depth);
993EXTERN void sat_FreeTrie(satManager_t *cm, satArray_t *arr);
994EXTERN void sat_PrintFlag(satManager_t *cm, long v);
995EXTERN void sat_PrintLiteral(satManager_t *cm, long lit);
996EXTERN void sat_CheckFlagsOnConflict(satManager_t *cm);
997EXTERN void sat_PrintDotForConflict( satManager_t *cm, satLevel_t *d, long conflict, int includePreviousLevel);
998EXTERN void sat_PrintDotForImplicationGraph( satManager_t *cm, satLevel_t *d, satArray_t *root, int includePreviousLevel);
999EXTERN void sat_PrintDotForWholeGraph( satManager_t *cm, satLevel_t *d, int includePreviousLevel) ;
1000EXTERN void sat_PrintDotForImplicationGraph( satManager_t *cm, satLevel_t *d, satArray_t *root, int includePreviousLevel);
1001EXTERN void sat_CheckNonobjConflictClause( satManager_t *cm, long v);
1002EXTERN void sat_CheckNonobjUnitClause( satManager_t *cm);
1003EXTERN void sat_CheckInitialCondition( satManager_t *cm);
1004EXTERN void sat_PrintClauseArray( satManager_t *cm, satArray_t *clauseArray);
1005EXTERN void sat_CheckConflictClause( satManager_t *cm, satArray_t *clauseArray) ;
1006EXTERN void sat_ImplyUnitPureLitsWithAnte(satManager_t * cm, satLevel_t *d);
1007EXTERN long sat_DecisionBasedOnShrink( satManager_t *cm);
1008EXTERN void sat_CheckOrderedVariableArray(satManager_t *cm);
1009EXTERN void sat_GetConflictAsConflictClause( satManager_t *cm, satArray_t *clauseArray);
1010EXTERN void sat_CheckForwardedClauses(satManager_t *cm);
1011EXTERN void sat_TryToBuildMonolithicBDD(satManager_t *cm);
1012EXTERN void sat_FindUIPAndNonUIP( satManager_t *cm, satArray_t *clauseArray, satLevel_t *d, int *objectFlag, int *bLevel, long *fdaLit);
1013EXTERN long sat_AddConflictClauseNoScoreUpdate( satManager_t *cm, satArray_t *clauseArray, int objectFlag);
1014EXTERN void sat_ClauseDeletionLatestActivity(satManager_t *cm);
1015EXTERN int sat_ConflictAnalysisUsingAuxImplication( satManager_t *cm, satArray_t *clauseArray); 
1016EXTERN int sat_AddConflictClauseAndBacktrack( satManager_t *cm, satArray_t *clauseArray, satLevel_t *d, long fdaLit, int bLevel, int objectFlag, int strongFlag);
1017EXTERN void sat_RestoreBlockingClauses(satManager_t *cm);
1018EXTERN void sat_RestoreFrontierClauses(satManager_t *cm);
1019EXTERN void sat_CollectBlockingClause(satManager_t *cm);
1020EXTERN void sat_PreProcessingForMixed(satManager_t *cm);
1021EXTERN satLevel_t * sat_MakeDecision(satManager_t *cm);
1022EXTERN satLevel_t * sat_AllocLevel( satManager_t *cm);
1023EXTERN int sat_AddConflictClauseWithNoScoreAndBacktrack( satManager_t *cm, satArray_t *clauseArray, satLevel_t *d, long fdaLit, int bLevel, int objectFlag, int strongFlag);
1024EXTERN void sat_InitScoreForMixed(satManager_t *cm);
1025EXTERN satArray_t *sat_ArrayDuplicate(satArray_t *old);
1026EXTERN int sat_ConflictAnalysisWithBlockingClause( satManager_t *cm, satLevel_t *d);
1027EXTERN int sat_ConflictAnalysisForLifting( satManager_t *cm, satLevel_t *d);
1028EXTERN int sat_AddConflictClauseAndBacktrackForLifting( satManager_t *cm, satArray_t *clauseArray, satLevel_t *d, long fdaLit, int bLevel, int objectFlag, int strongFlag);
1029EXTERN void sat_PreProcessingForMixedNoCompact(satManager_t *cm);
1030EXTERN int sat_CNFMainWithArray( satOption_t *option, satArray_t *cnfArray, int unsatCoreFlag, satArray_t *coreArray, st_table *mappedTable);
1031EXTERN int sat_WriteCNFFromArray(satArray_t *cnfArray, char *filename);
1032EXTERN int sat_ReadCNFFromArray( satManager_t *cm, satArray_t *cnfArray, st_table *mappedTable);
1033EXTERN void sat_RestoreClauses(satManager_t *cm, satArray_t *cnfArray);
1034EXTERN satQueue_t * sat_CreateQueue( long MaxElements );
1035
1036
1037
1038/*Bing: for AROSAT*/
1039EXTERN void sat_ASUpdateScore(satManager_t *cm);
1040EXTERN void sat_ASmergeLevel(satManager_t *cm);
1041EXTERN int sat_CE_CNF(satManager_t *cm,satLevel_t *d,
1042               int v,satArray_t *wl);
1043EXTERN int sat_CE(satManager_t *cm,satLevel_t *d,
1044           long v,int dfs,int value);
1045EXTERN int sat_ASDec(satManager_t *cm,satLevel_t *d,long v);
1046EXTERN int sat_ASImp(satManager_t *cm,satLevel_t *d,long v,int value);
1047
1048/**AutomaticEnd**************************************************************/
1049
1050#endif /* _SAT */
1051
1052
Note: See TracBrowser for help on using the repository browser.