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

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

vis2.3
File size: 4.5 KB
Line 
1/**CHeaderFile*****************************************************************
2
3  FileName    [puresat.h]
4
5  PackageName [puresat]
6
7  Synopsis    [Abstraction refinement for large scale invariant checking.]
8
9  Description [Abstraction refinement for large scale invariant checking.]
10
11  Author      [Bing Li]
12
13  Copyright   [Copyright (c) 2004 The Regents of the Univ. of Colorado. All
14  rights reserved.
15
16  Permission is hereby granted, without written agreement and without license
17  or royalty fees, to use, copy, modify, and distribute this software and its
18  documentation for any purpose, provided that the above copyright notice and
19  the following two paragraphs appear in all copies of this software.
20  ]
21 
22******************************************************************************/
23
24#ifndef _PURESAT
25#define _PURESAT
26
27/*---------------------------------------------------------------------------*/
28/* Nested includes                                                           */
29/*---------------------------------------------------------------------------*/
30
31#include "ntk.h"
32#include "st.h"
33
34/*---------------------------------------------------------------------------*/
35/* Constant declarations                                                     */
36/*---------------------------------------------------------------------------*/
37
38#define DUMMY -10000
39
40#define  RTnodeSize   8
41#define  RTfSize      0
42#define  RTformula    1
43#define  RToriClsIdx  2
44#define  RTpivot      3
45#define  RTflag       4
46#define  RTIPnode     5
47#define  RTleft       6
48#define  RTright      7
49#define  RT_NULL      0
50#define  RT_BLOCK     1000
51#define  FORMULA_BLOCK 2000
52
53
54#define RT_VisitedMask  0x00000001
55#define RT_ResetVisitedMask  0xfffffffe
56
57
58/*---------------------------------------------------------------------------*/
59/* Structure declarations                                                    */
60/*---------------------------------------------------------------------------*/
61
62typedef  long        RTnode_t;
63
64struct ResolutionTreeManager{
65  RTnode_t * nArray; /*record of RTnodes*/
66  long       aSize;  /*current position for nArray*/
67  long       maxSize;/*max pos for nArray*/
68  long     * fArray; /*record of AigNodes -- AIg node pool*/
69  long       cpos;   /*current position for fArray;*/
70  long       maxpos; /*max position for fArray;*/
71  RTnode_t   root;
72};
73
74
75struct InterpolationManager{
76  struct ResolutionTree *root;
77  st_table * CoiTable;/*for EffIP*/
78};
79
80/*---------------------------------------------------------------------------*/
81/* Type declarations                                                         */
82/*---------------------------------------------------------------------------*/
83
84typedef  struct ResolutionTreeManager  RTManager_t;
85/*typedef  long        RTnode_t;*/
86typedef struct InterpolationManager IP_Manager_t;
87/*---------------------------------------------------------------------------*/
88/* Variable declarations                                                     */
89/*---------------------------------------------------------------------------*/
90
91/*---------------------------------------------------------------------------*/
92/* Macro declarations                                                        */
93/*---------------------------------------------------------------------------*/
94
95#define RT_fSize(node) (rm->nArray[node+RTfSize])
96/*#define RT_formula(node) ((long*)rm->nArray[node+RTformula])*/
97#define RT_formula(node) (rm->nArray[node+RTformula])
98#define RT_oriClsIdx(node) (rm->nArray[node+RToriClsIdx])
99#define RT_pivot(node) (rm->nArray[node+RTpivot])
100#define RT_flag(node) (rm->nArray[node+RTflag])
101#define RT_IPnode(node) (rm->nArray[node+RTIPnode])
102#define RT_left(node) (rm->nArray[node+RTleft])
103#define RT_right(node) (rm->nArray[node+RTright])
104
105/**AutomaticStart*************************************************************/
106
107/*---------------------------------------------------------------------------*/
108/* Function prototypes                                                       */
109/*---------------------------------------------------------------------------*/
110
111EXTERN void PureSat_Init(void);
112EXTERN void PureSat_End(void);
113EXTERN void PureSat_CheckInvariant(Ntk_Network_t *network, array_t
114                                   *InvariantFormulaArray, int verbosity,
115                                   int dbgLevel, FILE *dbgOUt, boolean printInputs,
116                                   boolean incremental, boolean sss, 
117                                   boolean flatIP, int speed);
118
119/**AutomaticEnd***************************************************************/
120
121#endif /* _PURESAT */
Note: See TracBrowser for help on using the repository browser.