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

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

vis2.3
File size: 5.4 KB
Line 
1/**CHeaderFile*****************************************************************
2
3  FileName    [satInt.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: satInt.h,v 1.19 2009/04/11 18:26:37 fabio Exp $]
21
22******************************************************************************/
23
24
25#ifndef _SATINT
26#define _SATINT
27
28/*---------------------------------------------------------------------------*/
29/* Nested includes                                                           */
30/*---------------------------------------------------------------------------*/
31#include "baig.h"
32#include "sat.h"
33
34/*---------------------------------------------------------------------------*/
35/* Constant declarations                                                     */
36/*---------------------------------------------------------------------------*/
37
38#define LATEST_ACTIVITY_DELETION 0x1
39#define MAX_UNRELEVANCE_DELETION 0x2
40#define SIMPLE_LATEST_DELETION   0x4
41
42/*Bing:*/
43#define RESET_LC 0xfffffffe
44#define RESET_DVH  0xfffffffd
45#define SCOREUNIT 100000
46
47/*---------------------------------------------------------------------------*/
48/* Type declarations                                                         */
49/*---------------------------------------------------------------------------*/
50
51
52/*---------------------------------------------------------------------------*/
53/* Structure declarations                                                    */
54/*---------------------------------------------------------------------------*/
55
56/**Struct**********************************************************************
57
58  Synopsis    [sat option]
59
60  Description []
61
62******************************************************************************/
63
64/*---------------------------------------------------------------------------*/
65/* Variable declarations                                                     */
66/*---------------------------------------------------------------------------*/
67
68
69/*---------------------------------------------------------------------------*/
70/* Macro declarations                                                        */
71/*---------------------------------------------------------------------------*/
72
73
74/*---------------------------------------------------------------------------*/
75/* Function prototypes                                                       */
76/*---------------------------------------------------------------------------*/
77
78EXTERN satLevel_t * sat_GetDecision( satManager_t *cm, int level);
79EXTERN satArray_t * sat_ArrayAlloc(long number);
80EXTERN int sat_ImplyStop( satManager_t *cm, satLevel_t *d, long v, long left, long right);
81EXTERN int sat_ImplySplit( satManager_t *cm, satLevel_t *d, long v, long left, long right);
82EXTERN int sat_ImplyConflict( satManager_t *cm, satLevel_t *d, long v, long left, long right);
83EXTERN int sat_ImplyLeftForward( satManager_t *cm, satLevel_t *d, long v, long left, long right);
84EXTERN int sat_ImplyRightForward( satManager_t *cm, satLevel_t *d, long v, long left, long right);
85EXTERN int sat_ImplyForwardOne( satManager_t *cm, satLevel_t *d, long v, long left, long right);
86EXTERN int sat_ImplyPropRight( satManager_t *cm, satLevel_t *d, long v, long left, long right);
87EXTERN int sat_ImplyPropRightOne( satManager_t *cm, satLevel_t *d, long v, long left, long right);
88EXTERN int sat_ImplyPropLeft( satManager_t *cm, satLevel_t *d, long v, long left, long right);
89EXTERN int sat_ImplyPropLeftOne( satManager_t *cm, satLevel_t *d, long v, long left, long right);
90EXTERN int sat_ImplyPropLeftRight( satManager_t *cm, satLevel_t *d, long v, long left, long right);
91EXTERN satQueue_t * sat_CreateQueue( long MaxElements );
92EXTERN satStatistics_t * sat_InitStatistics(void);
93EXTERN int  sat_BacktrackWithAdditionalTest( satManager_t *cm, int level);
94EXTERN satLinearHead_t * sat_CreateLinearHead( satManager_t *cm, int flag);
95EXTERN satLinearCluster_t * sat_CreateCluster( satLinearHead_t *head, satLinearElem_t *e1, satLinearElem_t *e2, int flagIndex, int *idArr);
96EXTERN void sat_ExtractAssignmentFromBDD( satLinearHead_t *head, DdManager *mgr, satArray_t *arr, DdNode *cube);
97EXTERN DdNode *sat_CofactorBDDArray( satLinearHead_t *head, DdManager *mgr, DdNode *l1, satArray_t *satArr);
98EXTERN char * sat_RemoveSpace(char *line);
99EXTERN char * sat_CopyWord(char *lp, char *word);
100EXTERN satLinearHead_t * sat_CreateHeadForUIP(satManager_t *cm);
101EXTERN DdNode * sat_BuildBDDForClause( satManager_t *cm, satLinearHead_t *head, long v, int includeLevel, satArray_t *arr);
102EXTERN int  sat_GetUIPFromGivenBDD(satLinearHead_t *head, DdManager *mgr, DdNode *total, satArray_t *arr);
103EXTERN void RT_Free(RTManager_t *rm);
104EXTERN void ResetRTree(RTManager_t *rm);
105EXTERN bAigEdge_t sat_GenerateFwdIP(bAig_Manager_t* manager, satManager_t *cm, RTnode_t  RTnode, int cut);
106EXTERN void sat_BuildRT(satManager_t * cm, RTnode_t root, long *lp, long *tmpIP, int size, boolean NotCNF);
107EXTERN void sat_GenerateCore_All(satManager_t * cm);
108EXTERN void sat_InitLayerScore(satManager_t * cm);
109
110/**AutomaticEnd***************************************************************/
111
112#endif /* _SATINT */
Note: See TracBrowser for help on using the repository browser.