source: vis_dev/vis-2.3/src/puresat/puresatInt.h @ 40

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

vis2.3
File size: 24.3 KB
Line 
1/**CHeaderFile*****************************************************************
2
3  FileName    [puresatInt.h]
4
5  PackageName [puresat]
6
7  Synopsis    [Internal declarations.]
8
9  Author      [Bing Li]
10
11  Copyright   [Copyright (c) 2004 The Regents of the Univ. of Colorado.
12  All rights reserved.
13
14  Permission is hereby granted, without written agreement and without license
15  or royalty fees, to use, copy, modify, and distribute this software and its
16  documentation for any purpose, provided that the above copyright notice and
17  the following two paragraphs appear in all copies of this software.
18  ]
19
20  Revision    [$Id: puresatInt.h,v 1.22 2009/04/11 18:26:31 fabio Exp $]
21
22******************************************************************************/
23
24#ifndef _PURESATINT
25#define _PURESATINT
26
27
28/*---------------------------------------------------------------------------*/
29/* Nested includes                                                           */
30/*---------------------------------------------------------------------------*/
31
32#include "bmcInt.h"
33#include "mdd.h"
34#include "satInt.h"
35#include "sat.h"
36#include "puresat.h"
37#include "baig.h"
38
39/*---------------------------------------------------------------------------*/
40/* Constant declarations                                                     */
41/*---------------------------------------------------------------------------*/
42
43#define NO_OP 0
44#define MAX_LENGTH 80
45
46
47#define RESTORE_AIG 0
48#define PR 0
49#define TESTIP 1
50/*#define TIMEFRAME_VERIFY_*/
51#define COI 0 /*must be zero*/
52#define UNSATCORE 0
53#define IP_PROCESS 1 /*MUST be one*/
54/*#define TWOLEVEL_MIN 1*/
55#define DBG 1
56#define LARGEDFS 10000
57#define LAI 0 /*latch interface abstraction*/
58#define COREREFMIN 0
59#define THROUGHPICK 1
60#define DIFABSCON 0 /*must be zero,diff abs and contst model*/
61#define INCRECON  1/*Incremental Concretization*/
62#define AROSAT 1
63#define NOREFMIN 0
64#define ADD_HIGHRC_LATCH 0
65#define INC 0
66#define SWITCH 0
67#define SWITCH_DA 0 /*switch to DirAdd*/
68
69
70/*---------------------------------------------------------------------------*/
71/* Structure declarations                                                    */
72/*---------------------------------------------------------------------------*/
73
74struct PureSatManager {
75  int Length;
76  int sameAbsCon;
77  satArray_t * savedConCls;
78  int returnVal;
79  satArray_t * AuxObj;
80  int switch_da;
81  boolean Arosat; /*enable Arosat*/
82  boolean CoreRefMin;/*enable unsat proof-based refinement minimization*/
83  boolean RefPredict; /*enable refinement prediction*/
84  boolean Switch; /* enable dynamic switching*/
85  st_table *latchToTableBaigNodes;
86  st_table *ClsidxToLatchTable;
87  st_table  *CoiTable;
88  st_table  *oldCoiTable;
89  st_table  *AbsTable;
90  st_table  *vertexTable;
91  st_table  *SufAbsTable;
92  st_table  *supportTable;
93  st_table  *IdenLatchTable;  /*store indentical latch*/
94
95  st_table  *node2dfsTable;
96
97  /*for dir cone in abs order*/
98  st_table *nicTable;/*num in cone*/
99  st_table *niaTable; /*num in abs*/
100  boolean incre;
101  boolean sss;
102  int verbosity;
103  char * ltlFileName;
104  int timeOutPeriod;
105  int oldPos;
106  int dbgLevel;
107  FILE *dbgOut;
108  boolean printInputs;
109  array_t * result;
110  double tIP; /*general IP time*/
111  double tIPUnsat; /*real and bogus Cex detection time*/
112  double tIPGen;  /*IP generation time*/
113  double tIPImply;/*IP verification time*/
114  double tIPCon;  /*IP convergence test time*/
115  double tRefMin; /*Refine minimization time*/
116  double tRef;    /*Refine time*/
117  double tCoreGen;/*Core generation time in refine*/
118  double tRefExtract;/*time for extracting ref candidates*/
119  double tCon;    /*Incremental concretization time*/
120  double tGFree;
121  double tPro; /*time for processing*/
122  double tExp; /*time for expandsion*/
123  array_t *latchArray;
124};
125
126struct PureSatIncreSATManager {
127  int beginPosition;
128  int Length;
129  int oldLength;
130  int propertyPos;
131  BmcCnfClauses_t *cnfClauses;
132  satArray_t *savedConCls;
133  satManager_t *cm;
134};
135
136
137/*---------------------------------------------------------------------------*/
138/* Type declarations                                                         */
139/*---------------------------------------------------------------------------*/
140
141typedef enum {
142  dfsWhite_c,   /* unvisited node */
143  dfsGrey_c,    /* node on "stack" */
144  dfsBlack_c    /* node completely visited */
145} DfsColor;
146
147typedef struct PureSatManager PureSat_Manager_t;
148typedef struct PureSatIncreSATManager PureSat_IncreSATManager_t;
149
150
151/*---------------------------------------------------------------------------*/
152/* Variable declarations                                                     */
153/*---------------------------------------------------------------------------*/
154
155/*---------------------------------------------------------------------------*/
156/* Macro declarations                                                        */
157/*---------------------------------------------------------------------------*/
158
159
160/**AutomaticStart*************************************************************/
161
162/*---------------------------------------------------------------------------*/
163/* Function prototypes                                                       */
164/*---------------------------------------------------------------------------*/
165
166EXTERN void PureSatInsertNewClauseForSimplePath(array_t *vertexArray, Ntk_Network_t *network, int step1, int step2, BmcCnfClauses_t *cnfClauses, st_table *nodeToMvfAigTable);
167EXTERN void PureSatInsertNewClauseForInit(array_t *vertexArray, Ntk_Network_t *network, int step1, int step2, BmcCnfClauses_t *cnfClauses, st_table *nodeToMvfAigTable);
168EXTERN void PureSatSetInitStatesForSimplePath(array_t * vertexArray, Ntk_Network_t *network, BmcCnfClauses_t *cnfClauses, st_table * nodeToMvfAigTable);
169EXTERN boolean PureSatExistASimplePath(Ntk_Network_t *network, PureSat_IncreSATManager_t * pism, array_t * vertexArray, bAigEdge_t property, PureSat_Manager_t * pm);
170EXTERN boolean PureSatExistCE(Ntk_Network_t * network, PureSat_IncreSATManager_t * pism, BmcOption_t *options, array_t *vertexArray, bAigEdge_t property, PureSat_Manager_t * pm, int extractCexInfo);
171EXTERN boolean PureSatIncreExistCE(Ntk_Network_t * network, PureSat_IncreSATManager_t *pism, array_t *vertexArray, bAigEdge_t property, PureSat_Manager_t * pm);
172EXTERN boolean PureSatIncreExistCEForRefineOnAbs(Ntk_Network_t *network, PureSat_IncreSATManager_t *pism, array_t *vertexArray, bAigEdge_t property, boolean firstTime, PureSat_Manager_t * pm);
173EXTERN void PureSatGenerateClausesFromStateTostateWithTable(bAig_Manager_t *manager, bAigEdge_t *fromAigArray, bAigEdge_t *toAigArray, int mvfSize, int fromState, int toState, BmcCnfClauses_t *cnfClauses, int outIndex, st_table *ClsidxToLatchTable, char *nodeName);
174EXTERN void PureSatGenerateClausesForPath_EnhanceInit(Ntk_Network_t *network, int from, int to, PureSat_IncreSATManager_t * pism, PureSat_Manager_t * pm, st_table *nodeToMvfAigTable, st_table *CoiTable);
175EXTERN boolean PureSatCheckInv_SSS(Ntk_Network_t * network, Ctlsp_Formula_t *ltlFormula, PureSat_Manager_t *pm);
176
177EXTERN boolean PureSatCheckInv_FlatIP(Ntk_Network_t * network,
178                                      Ctlsp_Formula_t *ltlFormula,
179                                      PureSat_Manager_t *pm);
180EXTERN void PureSatCmdParse(int argc, char **argv, PureSat_Manager_t *pm);
181EXTERN array_t * PureSatRefineOnAbs(Ntk_Network_t *network, PureSat_Manager_t *pm, bAigEdge_t property, int latchThreshHold);
182EXTERN PureSat_Manager_t * PureSatManagerAlloc(void);
183EXTERN void PureSatManagerFree(PureSat_Manager_t * pm);
184EXTERN PureSat_IncreSATManager_t * PureSatIncreSATManagerAlloc(PureSat_Manager_t * pm);
185EXTERN void PureSatIncreSATManagerFree(PureSat_Manager_t *pm, PureSat_IncreSATManager_t * pism);
186EXTERN void PureSatBmcGetCoiForNtkNode(Ntk_Node_t *node, st_table *CoiTable, st_table *visited);
187EXTERN void PureSatBmcGetCoiForLtlFormulaRecursive(Ntk_Network_t *network, Ctlsp_Formula_t *formula, st_table *ltlCoiTable, st_table *visited);
188EXTERN DfsColor PureSatNodeReadColor(Ntk_Node_t * node);
189EXTERN void PureSatNodeSetColor(Ntk_Node_t * node, DfsColor color);
190EXTERN void PureSatNodeRecursivelyComputeTransitiveFaninNodes_AllNodes(Ntk_Node_t *node, int * NumofSupports, boolean stopAtLatches);
191EXTERN int PureSatNodeComputeCombinationalSupport_AllNodes(Ntk_Network_t *network, array_t * nodeArray, boolean stopAtLatches);
192EXTERN void PureSatGenerateSupportTable(Ntk_Network_t *network, PureSat_Manager_t *pm);
193EXTERN void PureSatBmcGetCoiForLtlFormula(Ntk_Network_t *network, Ctlsp_Formula_t *formula, st_table *ltlCoiTable);
194EXTERN void PureSatGetFormulaNodes(Ntk_Network_t *network, Ctlsp_Formula_t *F, array_t *formulaNodes);
195EXTERN void PureSatGetFaninLatches(Ntk_Node_t *node, st_table *visited, st_table *vertexTable);
196EXTERN st_table * PureSatCreateInitialAbstraction(Ntk_Network_t *network, Ctlsp_Formula_t *invFormula, int * Num, PureSat_Manager_t *pm);
197EXTERN void PureSatRecursivelyComputeTableForLatch(Ntk_Network_t * network, st_table *Table, Ntk_Node_t * node);
198EXTERN void PureSatComputeTableForLatch(Ntk_Network_t * network, st_table * Table, Ntk_Node_t * Latch);
199EXTERN void PureSatGetCoiForVisibleArray_Ring(Ntk_Network_t *network, array_t *visibleArray, int position, st_table *ltlCoiTable);
200EXTERN int NumInConeCompare(int *ptrX, int *ptrY);
201EXTERN int NumInConeCompare_Ring(int *ptrX, int *ptrY);
202EXTERN void PureSatRecursivelyComputeCorrelationforLatch(Ntk_Network_t *network, st_table *AbsTable, st_table * visited, Ntk_Node_t *node, int *count);
203EXTERN int PureSatComputeCorrelationforLatch(Ntk_Network_t * network, st_table * AbsTable, Ntk_Node_t *Latch);
204EXTERN array_t * PureSatGenerateRingFromAbs(Ntk_Network_t *network, PureSat_Manager_t *pm, array_t *invisibleArray, int * NumInSecondLevel);
205EXTERN void PureSatCleanSat(satManager_t * cm);
206EXTERN void PureSatReadClauses(PureSat_IncreSATManager_t * pism, PureSat_Manager_t * pm);
207EXTERN array_t * PureSatGetImmediateSupportLatches(Ntk_Network_t *network, int beginPosition, array_t *latchNameArray);
208EXTERN void PureSatWriteClausesToFile(PureSat_IncreSATManager_t * pism, mAig_Manager_t *maigManager, char *coreFile);
209EXTERN void PureSatWriteAllClausesToFile(PureSat_IncreSATManager_t * pism, char *coreFile);
210EXTERN array_t * PureSatGetLatchFromTable(Ntk_Network_t *network, PureSat_Manager_t * pm, char *coreFile);
211EXTERN array_t * PureSatRemove_char(array_t * array1, int i);
212
213EXTERN boolean PureSat_CheckAceByIP(Ntk_Network_t *network,
214                             PureSat_Manager_t * pm,
215                             PureSat_IncreSATManager_t *pism,
216                             array_t *vertexArray,
217                             int * k,
218                             Ctlsp_Formula_t *ltlFormula,
219                             bAigEdge_t * returnProp,
220                                    array_t *previousResultArray);
221EXTERN boolean PureSatCheckInv_IP(Ntk_Network_t * network, Ctlsp_Formula_t *ltlFormula, PureSat_Manager_t *pm);
222EXTERN boolean PureSatIPOnCon(Ntk_Network_t * network, Ctlsp_Formula_t *ltlFormula,PureSat_Manager_t *pm);
223EXTERN array_t * PureSat_GetSufAbsFromCore(Ntk_Network_t *network,satManager_t * cm,PureSat_Manager_t *pm,bAigEdge_t property,st_table * SufAbsNameTable);
224EXTERN void PureSat_GetSufAbsFromCoreRecur(mAig_Manager_t *manager,satManager_t * cm,RTnode_t RTnode, st_table *ctTable, st_table *refineTable);
225EXTERN void PureSat_GetSufAbsFromCoreRecur_2side(mAig_Manager_t *manager,satManager_t * cm,RTnode_t RTnode,st_table *ctTable,st_table *refineTable,st_table *SufNameTable);
226EXTERN array_t *PureSat_RefineOnAbs(Ntk_Network_t *network,PureSat_Manager_t *pm,bAigEdge_t property,array_t *previousResultArray,int latchThreshHold,int * sccArray,array_t * sufArray);
227EXTERN RTnode_t RTCreateNode(RTManager_t * rm);
228EXTERN IP_Manager_t * IPManagerAlloc();
229EXTERN void IPManagerFree(IP_Manager_t *ipm);
230EXTERN int PureSat_IdentifyConflict(
231  satManager_t *cm,
232  long left,
233  bAigEdge_t right,
234  bAigEdge_t node);
235EXTERN void PureSatBmcGetCoiForNtkNode_New(
236  Ntk_Node_t  *node,
237  st_table    *CoiTable,
238  st_table    *visited);
239EXTERN void PureSatBmcGetCoiForLtlFormulaRecursive_New(
240  Ntk_Network_t   *network,
241  Ctlsp_Formula_t *formula,
242  st_table        *ltlCoiTable,
243  st_table        *visited);
244EXTERN void PureSatBmcGetCoiForLtlFormula_New(
245  Ntk_Network_t   *network,
246  Ctlsp_Formula_t *formula,
247  st_table        *ltlCoiTable);
248EXTERN void PureSat_MarkTransitiveFaninForNode(
249        satManager_t *cm,
250        bAigEdge_t v,
251        unsigned int mask);
252EXTERN void PureSat_MarkTransitiveFaninForArray(
253        satManager_t *cm,
254        satArray_t *arr,
255        unsigned int mask);
256EXTERN void PureSat_MarkTransitiveFaninForNode2(
257        mAig_Manager_t *manager,
258        bAigEdge_t v,
259        unsigned int mask);
260EXTERN void PureSat_MarkTransitiveFaninForArray2(
261        mAig_Manager_t *manager,
262        satArray_t *arr,
263        unsigned int mask);
264EXTERN void PureSat_MarkTransitiveFaninForNode3(
265        mAig_Manager_t *manager,
266        bAigEdge_t v,
267        unsigned int mask);
268EXTERN void PureSat_MarkTransitiveFaninForArray3(
269        mAig_Manager_t *manager,
270        satArray_t *arr,
271        unsigned int mask);
272EXTERN void PureSat_MarkTransitiveFaninForNode4(
273        mAig_Manager_t *manager,
274        bAigEdge_t v,
275        unsigned int mask,
276        int bound);
277EXTERN void PureSat_MarkTransitiveFaninForArray4(
278        mAig_Manager_t *manager,
279        satArray_t *arr,
280        unsigned int mask,
281        int bound);
282EXTERN void PureSat_CleanMask(mAig_Manager_t *manager,
283                              unsigned int mask);
284EXTERN void PureSat_ResetCoi(satManager_t *cm);
285EXTERN void PureSat_SetCOI(satManager_t *cm);
286EXTERN void PureSatSetLatchCOI(Ntk_Network_t * network,
287                               PureSat_Manager_t *pm,
288                               satManager_t * cm,
289                               st_table * AbsTable,
290                               int from,
291                               int to);
292EXTERN void PureSatSetLatchCOI2(Ntk_Network_t * network,
293                                PureSat_Manager_t *pm,
294                                satManager_t * cm,
295                                bAigEdge_t obj,
296                                int bound);
297EXTERN void PureSatSetCOI(Ntk_Network_t * network,
298                          PureSat_Manager_t *pm,
299                          satManager_t * cm,
300                          st_table * AbsTable,
301                          int from,
302                          int to,
303                          int bound);
304EXTERN void PureSatAbstractLatch(bAig_Manager_t *manager,
305                          bAigEdge_t v,
306                          st_table * tmpTable);
307EXTERN void PureSatKillPseudoGVNode(bAig_Manager_t *manager,
308                                    bAigEdge_t v,
309                                    st_table * tmpTable);
310EXTERN void PureSatKillPseudoGV(Ntk_Network_t * network,
311                                PureSat_Manager_t *pm,
312                                st_table * AbsTable,
313                                int from,
314                                int to);
315EXTERN int PureSat_CountNodesInCoi(satManager_t* cm);
316EXTERN void PureSat_ResetManager(mAig_Manager_t *manager,
317                                 satManager_t *cm, int clean);
318EXTERN void PureSat_RestoreAigForDummyNode(mAig_Manager_t *manager,
319                                           int oldPosition);
320EXTERN void PureSatProcessFanout(satManager_t * cm);
321EXTERN long PureSatRecoverFanoutNode(satManager_t * cm,
322                                     bAigEdge_t v);
323EXTERN void PureSatRecoverISVNode(satManager_t *cm,
324                             bAigEdge_t v);
325EXTERN void PureSatRecoverFanout(satManager_t * cm,
326                                 PureSat_Manager_t *pm);
327EXTERN void PureSatPreprocess(Ntk_Network_t * network,
328                              satManager_t *cm,
329                              PureSat_Manager_t *pm,
330                              st_table *vertexTable,
331                              int Length);
332EXTERN void PureSatPostprocess(bAig_Manager_t *manager,
333                               satManager_t *cm,
334                               PureSat_Manager_t *pm);
335/*EXTERN int PureSat_TestImply_AbRf(Ntk_Network_t *network,
336                                  satManager_t *cm,
337                                  PureSat_Manager_t *pm,
338                                  st_table *vertexTable,
339                                  bAigEdge_t state1,
340                                  bAigEdge_t state2);*/
341EXTERN int PureSat_TestConvergeForIP(mAig_Manager_t *manager,
342                                     PureSat_Manager_t *pm,
343                                     satManager_t *cm,
344                                     bAigEdge_t state1,
345                                     bAigEdge_t state2);
346EXTERN int PureSat_TestConvergeForIP_AbRf(Ntk_Network_t *network,
347                                   satManager_t *cm,
348                                   PureSat_Manager_t *pm,
349                                   array_t  * CoiArray,
350                                   bAigEdge_t state1,
351                                          bAigEdge_t state2);
352EXTERN satManager_t * PureSat_SatManagerAlloc(bAig_Manager_t *manager,
353                                              PureSat_Manager_t *pm,
354                                              bAigEdge_t     object,
355                                              array_t        *auxObjectArray);
356EXTERN satManager_t * PureSat_SatManagerAlloc_WOCOI(mAig_Manager_t *manager,
357                                                    PureSat_Manager_t *pm,
358                                                    bAigEdge_t     object,
359                                                    array_t    *auxObjectArray);
360EXTERN void PureSat_SatFreeManager(satManager_t*cm);
361EXTERN void PureSat_PrintAigStatus(mAig_Manager_t *manager);
362EXTERN void PureSat_unconnectOutput(
363   bAig_Manager_t *manager,
364   bAigEdge_t from,
365   bAigEdge_t to);
366EXTERN void PureSat_MarkGlobalVar(bAig_Manager_t *manager,
367                                  int length);
368EXTERN void PureSat_UnMarkGlobalVar(bAig_Manager_t *manager,
369                                    int length);
370EXTERN void PureSat_MarkGlobalVar_AbRf(bAig_Manager_t *manager,
371                                       int length);
372EXTERN void PuresatMarkVisibleVarWithVPGV(Ntk_Network_t *network,
373                                  array_t * visibleArray,
374                                  PureSat_Manager_t *pm,
375                                  int from,
376                                          int to);
377EXTERN void PuresatMarkVisibleVar(Ntk_Network_t *network,
378                           array_t * visibleArray,
379                           PureSat_Manager_t *pm,
380                           int from,
381                                  int to);
382EXTERN bAigEdge_t PureSat_MapIPRecur(mAig_Manager_t *manager,
383                         bAigEdge_t  node,
384                                     st_table * tmpTable);
385EXTERN bAigEdge_t PureSat_MapIP(mAig_Manager_t *manager,
386                         bAigEdge_t node,
387                         int from,
388                                int to);
389EXTERN void PureSatProcessDummy(bAig_Manager_t *manager,
390                         satManager_t *cm,
391                         RTnode_t  RTnode);
392EXTERN bAigEdge_t
393PureSat_FindNodeByName(
394  bAig_Manager_t *manager,
395  nameType_t     *name,
396  int bound);
397EXTERN bAigEdge_t
398PureSatCreatebAigOfPropFormula(
399    Ntk_Network_t *network,
400    bAig_Manager_t *manager,
401    int bound,
402    Ctlsp_Formula_t *ltl,
403    int withInitialState);
404EXTERN void PureSatMarkObj(bAig_Manager_t * manager,
405                    long from,
406                    long to);
407EXTERN boolean PureSat_ConcretTest(Ntk_Network_t *network,
408                            PureSat_Manager_t *pm,
409                            array_t *sufArray,
410                            bAigEdge_t property,
411                            array_t *previousResultArray,
412                            int Con,
413                            int satStat,
414                                   int inc);
415EXTERN boolean PureSat_ConcretTest_Core(Ntk_Network_t *network,
416                                 PureSat_Manager_t *pm,
417                                 array_t *sufArray,
418                                 bAigEdge_t property,
419                                 array_t *previousResultArray,
420                                        st_table * junkTable);
421EXTERN void PureSatGenerateRingForNode(Ntk_Network_t *network,
422                                PureSat_Manager_t *pm,
423                                Ntk_Node_t * node1,
424                                array_t * ringArray,
425                                //st_table * node2dfsTable,
426                                       int *dfs);
427EXTERN array_t * PureSatGenerateRing(Ntk_Network_t *network,
428                              PureSat_Manager_t *pm,
429                              array_t * coreArray,
430                              //  st_table *node2dfsTable,
431                                     int * dfs);
432EXTERN void PureSatGenerateDfs(Ntk_Network_t *network,
433                        PureSat_Manager_t *pm,
434                               array_t * vertexArray);
435/*EXTERN array_t * PureSatGenerateRCArray(Ntk_Network_t *network,
436                                 PureSat_Manager_t *pm,
437                                 array_t *invisibleArray,
438                                // st_table * node2dfsTable,
439                                 int *sccArray,
440                                 int *NumInSecondLevel);*/
441EXTERN void PureSatComputeNumGatesInAbsForNode(Ntk_Network_t * network,
442                                        PureSat_Manager_t * pm,
443                                        Ntk_Node_t * node,
444                                        st_table * visited,
445                                        int  * ct,
446                                               int  * ct1);
447EXTERN void PureSatComputeNumGatesInAbs(Ntk_Network_t *network,
448                                PureSat_Manager_t *pm,
449                                        array_t * invisibleArray);
450EXTERN void PureSatComputeNumGatesInConeForNode(Ntk_Network_t * network,
451                                       PureSat_Manager_t * pm,
452                                       Ntk_Node_t * node,
453                                       st_table * visited,
454                                                int  * ct);
455EXTERN void PureSatComputeNumGatesInCone(Ntk_Network_t *network,
456                                PureSat_Manager_t *pm,
457                                         array_t * latchArray);
458EXTERN array_t * PureSatGenerateRCArray_2(Ntk_Network_t *network,
459                                   PureSat_Manager_t *pm,
460                                   array_t *invisibleArray,
461                                          int *NumInSecondLevel);
462/*EXTERN array_t * PureSatComputeOrder(Ntk_Network_t *network,
463                              PureSat_Manager_t *pm,
464                              array_t * vertexArray,
465                              array_t * invisibleArray,
466                              int * sccArray,
467                              int * NumInSecondLevel);*/
468EXTERN array_t * PureSatComputeOrder_2(Ntk_Network_t *network,
469                              PureSat_Manager_t *pm,
470                              array_t * vertexArray,
471                              array_t * invisibleArray,
472                              int * sccArray,
473                                       int * NumInSecondLevel);
474EXTERN void PureSatAddIdenLatchToAbs(Ntk_Network_t *network,
475                              PureSat_Manager_t *pm,
476                                     array_t *nameArray);
477EXTERN void PureSatCreateInitAbsByAIG(bAig_Manager_t *manager,
478                          PureSat_Manager_t *pm,
479                          bAigEdge_t node,
480                                 st_table * tmpTable);
481EXTERN void PureSat_GetLatchForNode(bAig_Manager_t *manager,
482                        PureSat_Manager_t *pm,
483                        bAigEdge_t node,
484                        array_t * nameArray,
485                        st_table *tmpTable,
486                                    int cut);
487EXTERN st_table * PureSatGetAigCoi(Ntk_Network_t *network,
488                            PureSat_Manager_t *pm,
489                                   bAigEdge_t property);
490EXTERN void PureSatPreProcLatch(Ntk_Network_t *network,
491                                PureSat_Manager_t *pm);
492EXTERN void PureSatGetIndenticalLatch(Ntk_Network_t *network,
493                                      PureSat_Manager_t *pm);
494EXTERN void PureSat_connectOutput(
495   bAig_Manager_t *manager,
496   bAigEdge_t from,
497   bAigEdge_t to,
498   int inputIndex);
499EXTERN bAigEdge_t
500PureSat_HashTableLookup(
501  bAig_Manager_t *manager,
502  bAigEdge_t  node1,
503  bAigEdge_t  node2);
504EXTERN int
505PureSat_HashTableAdd(
506  bAig_Manager_t   *manager,
507  bAigEdge_t  nodeIndexParent,
508  bAigEdge_t  nodeIndex1,
509  bAigEdge_t  nodeIndex2);
510EXTERN bAigEdge_t
511PureSat_CreateAndNode(
512   bAig_Manager_t  *manager,
513   bAigEdge_t node1,
514   bAigEdge_t node2);
515EXTERN bAigEdge_t
516PureSat_And2(
517   bAig_Manager_t *manager,
518   bAigEdge_t nodeIndex1,
519   bAigEdge_t nodeIndex2);
520EXTERN bAigEdge_t
521PureSat_And3(
522           bAig_Manager_t *manager,
523           bAigEdge_t l,
524           bAigEdge_t r);
525EXTERN bAigEdge_t
526PureSat_And4(
527           bAig_Manager_t *manager,
528           bAigEdge_t l,
529           bAigEdge_t r);
530EXTERN int PureSat_Test2LevelMini(bAig_Manager_t *manager,
531                           bAigEdge_t l,
532                           bAigEdge_t r);
533EXTERN bAigEdge_t
534PureSat_And(
535   bAig_Manager_t *manager,
536   bAigEdge_t nodeIndex1,
537   bAigEdge_t nodeIndex2);
538EXTERN bAigEdge_t
539PureSat_Or(
540   bAig_Manager_t *manager,
541   bAigEdge_t nodeIndex1,
542   bAigEdge_t nodeIndex2);
543EXTERN bAigEdge_t
544PureSat_Xor(
545   bAig_Manager_t *manager,
546   bAigEdge_t nodeIndex1,
547   bAigEdge_t nodeIndex2);
548EXTERN bAigEdge_t
549PureSat_Eq(
550   bAig_Manager_t *manager,
551   bAigEdge_t nodeIndex1,
552   bAigEdge_t nodeIndex2);
553EXTERN bAigEdge_t
554PureSat_Then(
555   bAig_Manager_t *manager,
556   bAigEdge_t nodeIndex1,
557   bAigEdge_t nodeIndex2);
558EXTERN bAigEdge_t
559PureSat_CreateVarNode(
560   bAig_Manager_t  *manager,
561   nameType_t      *name);
562EXTERN int AS_ImplyStop( satManager_t *cm, satLevel_t *d, long v, long left, long right);
563EXTERN int AS_ImplySplit( satManager_t *cm, satLevel_t *d, long v, long left, long right);
564EXTERN int AS_ImplyConflict( satManager_t *cm, satLevel_t *d, long v, long left, long right);
565EXTERN int AS_ImplyLeftForward( satManager_t *cm, satLevel_t *d, long v, long left, long right);
566EXTERN int AS_ImplyRightForward( satManager_t *cm, satLevel_t *d, long v, long left, long right);
567EXTERN int AS_ImplyForwardOne( satManager_t *cm, satLevel_t *d, long v, long left, long right);
568EXTERN int AS_ImplyPropRight( satManager_t *cm, satLevel_t *d, long v, long left, long right);
569EXTERN int AS_ImplyPropRightOne( satManager_t *cm, satLevel_t *d, long v, long left, long right);
570EXTERN int AS_ImplyPropLeft( satManager_t *cm, satLevel_t *d, long v, long left, long right);
571EXTERN int AS_ImplyPropLeftOne( satManager_t *cm, satLevel_t *d, long v, long left, long right);
572EXTERN int AS_ImplyPropLeftRight( satManager_t *cm, satLevel_t *d, long v, long left, long right);
573EXTERN void
574AS_Undo(
575        satManager_t *cm,
576        satLevel_t *d);
577EXTERN void
578AS_ImplyCNF(
579        satManager_t *cm,
580        satLevel_t *d,
581        long v,
582        satArray_t *wl);
583EXTERN int
584AS_ImplyNode(
585        satManager_t *cm,
586        satLevel_t *d,
587        long v);
588
589EXTERN void AS_ImplicationMain(
590        satManager_t *cm,
591        satLevel_t *d);
592EXTERN void
593AS_ImplyArray(
594        satManager_t *cm,
595        satLevel_t *d,
596        satArray_t *arr);
597EXTERN void
598AS_PreProcessing(satManager_t *cm);
599EXTERN void
600AS_Backtrack(
601        satManager_t *cm,
602        int level);
603EXTERN void
604AS_UpdateScore(
605  satManager_t *cm);
606EXTERN void
607AS_PeriodicFunctions(satManager_t *cm);
608EXTERN satLevel_t *
609AS_MakeDecision(satManager_t *cm);
610EXTERN void
611AS_FindUIP(
612        satManager_t *cm,
613        satArray_t *clauseArray,
614        satLevel_t *d,
615        int *objectFlag,
616        int *bLevel,
617        long *fdaLit);
618EXTERN int
619AS_ConflictAnalysis(
620        satManager_t *cm,
621        satLevel_t *d);
622EXTERN void
623AS_Solve(satManager_t *cm);
624EXTERN void AS_Main(satManager_t *cm);
625EXTERN void PureSatCreateOneLayer(Ntk_Network_t *network,
626                                  PureSat_Manager_t *pm,
627                                  satManager_t *cm,
628                                  array_t * latchArray,
629                                  int layer);
630EXTERN void PureSatCreateLayer(Ntk_Network_t *network,
631                               PureSat_Manager_t *pm,
632                               satManager_t *cm,
633                               array_t *absModel,
634                               array_t *sufArray);
635EXTERN void bAig_PureSat_ExpandTimeFrame(
636        Ntk_Network_t *network,
637        mAig_Manager_t *manager,
638        PureSat_Manager_t *pm,
639        int bound,
640        int withInitialState);
641EXTERN bAigTimeFrame_t * bAig_PureSat_InitTimeFrame(
642        Ntk_Network_t *network,
643        mAig_Manager_t *manager,
644        PureSat_Manager_t *pm,
645        int withInitialState);
646EXTERN void PureSatCheckCoi(bAig_Manager_t *manager);
647EXTERN void PureSat_CheckFanoutFanin(bAig_Manager_t *manager);
648
649/**AutomaticEnd***************************************************************/
650
651#endif /*_PURESATINT*/
Note: See TracBrowser for help on using the repository browser.