/**CHeaderFile*****************************************************************

  FileName    [puresat.h]

  PackageName [puresat]

  Synopsis    [Abstraction refinement for large scale invariant checking.]

  Description [Abstraction refinement for large scale invariant checking.]

  Author      [Bing Li]

  Copyright   [Copyright (c) 2004 The Regents of the Univ. of Colorado. All 
  rights reserved.

  Permission is hereby granted, without written agreement and without license
  or royalty fees, to use, copy, modify, and distribute this software and its
  documentation for any purpose, provided that the above copyright notice and
  the following two paragraphs appear in all copies of this software.
  ]
  
******************************************************************************/

#ifndef _PURESAT
#define _PURESAT

/*---------------------------------------------------------------------------*/
/* Nested includes                                                           */
/*---------------------------------------------------------------------------*/

#include "ntk.h"
#include "st.h"

/*---------------------------------------------------------------------------*/
/* Constant declarations                                                     */
/*---------------------------------------------------------------------------*/

#define DUMMY -10000

#define  RTnodeSize   8
#define  RTfSize      0
#define  RTformula    1
#define  RToriClsIdx  2
#define  RTpivot      3
#define  RTflag       4
#define  RTIPnode     5
#define  RTleft       6
#define  RTright      7
#define  RT_NULL      0
#define  RT_BLOCK     1000
#define  FORMULA_BLOCK 2000


#define RT_VisitedMask  0x00000001
#define RT_ResetVisitedMask  0xfffffffe


/*---------------------------------------------------------------------------*/
/* Structure declarations                                                    */
/*---------------------------------------------------------------------------*/

typedef  long        RTnode_t;

struct ResolutionTreeManager{
  RTnode_t * nArray; /*record of RTnodes*/
  long       aSize;  /*current position for nArray*/
  long       maxSize;/*max pos for nArray*/
  long     * fArray; /*record of AigNodes -- AIg node pool*/
  long       cpos;   /*current position for fArray;*/
  long       maxpos; /*max position for fArray;*/
  RTnode_t   root;
};


struct InterpolationManager{
  struct ResolutionTree *root;
  st_table * CoiTable;/*for EffIP*/
};

/*---------------------------------------------------------------------------*/
/* Type declarations                                                         */
/*---------------------------------------------------------------------------*/

typedef  struct ResolutionTreeManager  RTManager_t;
/*typedef  long        RTnode_t;*/
typedef struct InterpolationManager IP_Manager_t;
/*---------------------------------------------------------------------------*/
/* Variable declarations                                                     */
/*---------------------------------------------------------------------------*/

/*---------------------------------------------------------------------------*/
/* Macro declarations                                                        */
/*---------------------------------------------------------------------------*/

#define RT_fSize(node) (rm->nArray[node+RTfSize])
/*#define RT_formula(node) ((long*)rm->nArray[node+RTformula])*/
#define RT_formula(node) (rm->nArray[node+RTformula])
#define RT_oriClsIdx(node) (rm->nArray[node+RToriClsIdx])
#define RT_pivot(node) (rm->nArray[node+RTpivot])
#define RT_flag(node) (rm->nArray[node+RTflag])
#define RT_IPnode(node) (rm->nArray[node+RTIPnode])
#define RT_left(node) (rm->nArray[node+RTleft])
#define RT_right(node) (rm->nArray[node+RTright])

/**AutomaticStart*************************************************************/

/*---------------------------------------------------------------------------*/
/* Function prototypes                                                       */
/*---------------------------------------------------------------------------*/

EXTERN void PureSat_Init(void);
EXTERN void PureSat_End(void);
EXTERN void PureSat_CheckInvariant(Ntk_Network_t *network, array_t
				   *InvariantFormulaArray, int verbosity,
				   int dbgLevel, FILE *dbgOUt, boolean printInputs,
                                   boolean incremental, boolean sss, 
				   boolean flatIP, int speed);

/**AutomaticEnd***************************************************************/

#endif /* _PURESAT */