source: vis_dev/vis-2.3/src/baig/baigInt.h @ 38

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

vis2.3
File size: 4.7 KB
Line 
1/**CHeaderFile*****************************************************************
2
3  FileName    [baigInt.h]
4
5  PackageName [baig]
6
7  Synopsis    []
8
9  Description [Internal data structures of the bAig package.]
10
11  SeeAlso     []
12
13  Author      [Mohammad Awedh]
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: baigInt.h,v 1.21 2005/07/15 21:09:26 jinh Exp $]
21
22******************************************************************************/
23
24#ifndef _bAIGINT
25#define _bAIGINT
26
27#include "util.h"
28#include "array.h"
29#include "baig.h"
30
31/*---------------------------------------------------------------------------*/
32/* Constant declarations                                                     */
33/*---------------------------------------------------------------------------*/
34
35/* Each node occupies 8 location.  The following describes these locations */
36
37/*---------------------------------------------------------------------------*/
38/* Type declarations                                                         */
39/*---------------------------------------------------------------------------*/
40
41/*---------------------------------------------------------------------------*/
42/* Structure declarations                                                    */
43/*---------------------------------------------------------------------------*/
44
45
46
47/*---------------------------------------------------------------------------*/
48/* Variable declarations                                                     */
49/*---------------------------------------------------------------------------*/
50
51
52/*---------------------------------------------------------------------------*/
53/* Macro declarations                                                        */
54/*---------------------------------------------------------------------------*/
55
56
57
58
59/**AutomaticStart*************************************************************/
60
61/*---------------------------------------------------------------------------*/
62/* Function prototypes                                                       */
63/*---------------------------------------------------------------------------*/
64
65EXTERN void bAigSetPassFlag(bAig_Manager_t *manager, bAigEdge_t node);
66EXTERN void bAigResetPassFlag(bAig_Manager_t *manager, bAigEdge_t node);
67EXTERN int bAigGetPassFlag(bAig_Manager_t *manager, bAigEdge_t node);
68EXTERN bAigEdge_t bAigCreateAndNode(bAig_Manager_t *manager, bAigEdge_t node1, bAigEdge_t node2);
69EXTERN bAigTransition_t * bAigCreateTransitionRelation( Ntk_Network_t *network, mAig_Manager_t *manager);
70EXTERN int bAigCheckInvariantWithAG( bAigTransition_t *t, bAigEdge_t objective);
71EXTERN void bAigCleanUpDataFromPreviousExecution(bAigTransition_t *t);
72EXTERN bAigEdge_t bAigBuildObjectiveFromFrontierSet(bAigTransition_t *t);
73EXTERN satManager_t * bAigCirCUsInterfaceForAX(bAigTransition_t *t);
74EXTERN void bAigMarkConeOfInfluenceForAX(bAigTransition_t *t, satManager_t *cm);
75EXTERN void bAig_ComputeAX(bAigTransition_t *t);
76EXTERN void bAig_PostProcessForAX(bAigTransition_t *t, satManager_t *cm);
77EXTERN void bAigCreateSatManagerForLifting(bAigTransition_t *t);
78EXTERN void bAigSolveAllSatWithLifting(bAigTransition_t *t);
79EXTERN void bAigBlockingClauseAnalysisBasedOnLifting(bAigTransition_t *t, satManager_t *allsat);
80EXTERN void bAigCollectAntecdentOfObjective( bAigTransition_t *t, satManager_t *cm, bAigEdge_t obj, satArray_t *clauseArray);
81EXTERN void bAigMinimizationBasedOnLifting( bAigTransition_t *t, bAigEdge_t obj, satArray_t *orderArray);
82EXTERN int bAigCheckExistenceOfUIP( satManager_t *cm, satArray_t *clauseArray,int mLevel,  bAigEdge_t *fdaLit, int *bLevel);
83EXTERN void bAigSolverForLifting(satManager_t *cm, int tLevel);
84EXTERN void bAigCollectAntecdentOfObjectiveAux(satManager_t *cm, bAigEdge_t v);
85EXTERN int bAigInclusionTestOnInitialStates(bAigTransition_t *t);
86EXTERN void bAigPrintTransitionInfo(bAigTransition_t *t);
87EXTERN void bAigMinimizationBasedOnLiftingAllAtOnce( bAigTransition_t *t, bAigEdge_t obj, satArray_t *orderArray); 
88EXTERN satArray_t * bAigCreateCNFInstanceForInclusionTestOnInitialStates(bAigTransition_t *t);
89EXTERN void bAig_CreateCNFFromAIG( bAig_Manager_t *manager, satArray_t *rootArray, satArray_t *cnfArray);
90EXTERN void bAigCreateSatManagerForLiftingUnconstrained(bAigTransition_t *t);
91EXTERN bAigEdge_t bAigBuildComplementedObjectiveWithCNF( bAigTransition_t *t, satManager_t *cm, satArray_t *narr, satArray_t *carr);
92EXTERN void bAigPreProcessingForLiftingInstance(bAigTransition_t *t, satManager_t *cm);
93
94
95
96/**AutomaticEnd***************************************************************/
97
98#endif /* _bAIGINT */
Note: See TracBrowser for help on using the repository browser.