tarski.h

Go to the documentation of this file.

#ifndef _TRK
#define _TRK

#include "assert.h"
#include "util.h"
#include "stdarg.h"
#include "bdd.h"

typedef enum {
  Undef_c,

  List_c, // LISP style cons list
  Pair_c, // used to encode a pair of nodes -- differs from a list
          // in that we use a single node rather than two nodes

  // inputs
  ScalarPI_c, // scalar primary input node has id in left field, right is nil
  BooleanPI_c, // Boolean primary input node has id in left field, right is nil

  // regs
  ScalarReg_c, // scalar register, left child is name, right is list of 
               // length two; first entry is the init, second is the ns function
  BooleanReg_c, // Boolean register, same org as for scalar

  // internal vars
  InternalScalarVar_c, // internal scalar variable, leftchild is its name, right is nil
  InternalBooleanVar_c, // internal boolean variable, leftchild is its name, right is nil

  Assign_c, // left node is variable name, right node is expression it's being assigned to

  // Boolean ops
  And_c, // left node is one of two ops, right is the other
  Or_c, // left node is one of two ops, right is the other
  Not_c, // left node is argument, right node is nil
  Iff_c, // children are arguments, applies to booleans only
  TRUE_c, // Boolean const TRUE, no children
  FALSE_c, // Boolean const FALSE, no children

  // scalar ops
  Mux_c, // left node is control, right is pair of two inputs, first is for IF case
  Equal_c, // children are arguments, applies to scalars
  UnaryFunc_c, // single argument function, name is in left node, arg in right
  Func_c, // multi argument function, name is left node, args are in list form on right
  Relation_c, // uninterpreted relation, name is left node, args are in list form on right
  ScalarConst_c, // scalar constant, its name is in left child, right child is nil

} Operator_t;

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

class cube;

class Fnode {
  public:
    Operator_t type;
    Fnode* lchild;
    Fnode* rchild;
    Fnode *operator&( Fnode * );
    Fnode *operator|( Fnode * );
    Fnode *operator%( Fnode * );
    Fnode *operator^( Fnode * );
    Fnode *operator==(Fnode * );
    Fnode *operator<<(Fnode * );
    Fnode *operator!( );
    Fnode *operator,( Fnode *);
};


class F {
  public:
    Fnode *raw;
    Operator_t type() {return raw->type;}
    Fnode *lchild() {return (Fnode *) raw->lchild;}
    Fnode *rchild() {return (Fnode *) raw->rchild;}
    int node_print();
    F operator&( F B ) {F R; R.raw = (*(raw) & B.raw); return R;}
    F operator|( F B ) {F R; R.raw = (*(raw) | B.raw); return R;}
    F operator%( F B ) {F R; R.raw = (*(raw) % B.raw); return R;}
    F operator^( F B ) {F R; R.raw = (*(raw) ^ B.raw); return R;}
    F operator==(F B ) {F R; R.raw = (*(raw) == B.raw); return R;}
    F operator<<(F B ) {F R; R.raw = (*(raw) << B.raw); return R;}
    F operator,( F B ) {F R; R.raw = (*(raw) , B.raw); return R;}
    F operator>>( F B ) {F R; R.raw = *!(*raw) | B.raw; return R;}
    F operator!( ) {F R; R.raw = ( !(*(raw) ) );  return R;}
    int    operator()(cube);
};


// forward declaration, needed for vector matrix product
class Fmatrix;

class Fvector {
  public:
    int N;
    char *name;
    F *array;
    F operator[]( int ); 
    Fvector* operator!( ); 
    Fvector* operator|( Fvector * ); 
    Fvector* operator&( Fvector * ); 
    Fvector* operator*( Fmatrix * ); 
    F operator++( );  // takes or of all entries
    F operator--( );  // takes and of all entries; mnemonic: makes smaller
}; 


class Fv {
  public:
    Fvector *raw;
    int N() {return raw->N;}
    char *name() {return raw->name;}
    F *array() {return raw->array;}
    F operator[]( int index )  {return (*raw)[index];}
    Fv operator!( ) {Fv R; R.raw= !(*raw); return R;}
    Fv operator|( Fv B) {Fv R; R.raw= (*raw | B.raw); return R;}
    Fv operator&( Fv B) {Fv R; R.raw= (*raw & B.raw); return R;}
    F operator++( ) {F R; R = (++(*raw)); return R;}
    Fv operator>>( Fv B ) {Fv R; R.raw = ( *!(*raw) | B.raw); return R;}
    F operator--( ) {F R; R = (--(*raw)); return R;}
};

class Fmatrix {
  public:
    char *name;
    int N;
    int M;
    Fvector **rows;
    Fmatrix *operator~( );
    Fmatrix *operator!( ); // point wise negation
    Fmatrix *operator*( Fmatrix * );
    Fmatrix *operator|( Fmatrix * );
    Fvector *operator[]( int );
    F operator++(); // or all entries
    F operator--(); // and all entries
}; 


class Fm {
  public:
    Fmatrix *raw;
    char *name() { return raw->name; }
    int N() {return raw->N; }
    int M() {return raw->M; }
    Fvector **rows() {return raw->rows;}
    Fm operator~( ) {Fm R; R.raw = ~(*raw); return R; }
    Fm operator!( )  {Fm R; R.raw = !(*raw); return R;}
    Fm operator*( Fm B ) {Fm R; R.raw = (*raw) * (B.raw); return R;}
    Fm operator|( Fm B ) {Fm R; R.raw = *raw | (B.raw); return R;}
    Fv operator[]( int index ) {Fv R; R.raw = (*raw)[index]; return R; }
    Fm operator>>( Fm B ) {Fm R; R.raw = ( *!(*(raw)) | B.raw ); return R;}
    F operator++() {return ++(*raw); }
    F operator--() {return --(*raw); }
}; 


struct NetStruct {
  public: 
  array_t * formulas;
  int numNodes;
  array_t *allNodes;
  array_t *PIs;
  array_t *constants;
  st_table *UIFs;
  st_table *nameToNodeHash;
  st_table *nodeToId;
  st_table *nodeToFanoutArray;
  st_table *memToSizeHash;
};

typedef struct NetStruct Net_t;


class cube {
  public:
    st_table *nodeToValue;  
    cube( );
    ~cube( );
    int operator[]( F );
    void insert( F, int );
};

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

#define USE  __attribute__((unused)) 


extern F Fnil;
#define nil ( ( Fnode * ) 0 )   

/*---------------------------------------------------------------------------*/
/* Extern function prototypes                                                */
/*---------------------------------------------------------------------------*/

#ifdef __cplusplus
extern "C" {
#endif

extern Fnode *new_node( Operator_t type, Fnode *lchild, Fnode *rchild );
extern Fnode *new_node_raw( Operator_t type, Fnode *lchild, Fnode *rchild );
extern char *string_register( char *aString );
extern Fnode *node_register( Fnode *aNode );
extern int node_cmp( Fnode *aNode, Fnode *bNode );
extern int node_hash( Fnode *aNode, int modulus );
extern Fnode *node_dup( Net_t *net, Fnode *formula, char *suf, st_table *processedTable );
extern int node_test_is_boolean( Fnode*A );
extern int node_test_is_scalar( Fnode *A );
extern F TRUE();
extern F FALSE();
extern F si( char *name );
extern F bi( char *name );
extern F sr( char *name );
extern F br( char *name );
extern F sc( char *name );
extern F bc( char *name );
extern F uif2( char *name, F arg1, F arg2 );
extern F uir3( char *name, F arg1, F arg2, F arg3 );
extern F uif3( char *name, F arg1, F arg2, F arg3 );
extern F uif( char *name, F arg );
extern F assign( char *name, F arg );
extern F mux( F c, F D1, F D0 );
extern int Node_HasLeftChildNode( Fnode*node );
extern int Node_HasRightChildNode( Fnode*node );
extern Fnode * node_GetUnique(Fnode *node);
extern Fnode *cons( Fnode *a, Fnode *b );
extern Fnode *car( Fnode *a );
extern Fnode *cdr( Fnode *a );
extern F list( F startNode, ... );
extern int listlength( F aList );
extern F ri( char *name, F restrictedList );
extern F restrict( F aNode, F restrictedList );
extern Fnode *nn( Operator_t a, Fnode *b, Fnode *c);
extern Fnode *rn( Fnode *aNode );
extern char*rs( char*aString );
extern Fnode*Mux_ThenInput( Fnode*aNode );
extern Fnode*Mux_ElseInput( Fnode*aNode );
extern Fnode *Reg_InitFunc( Fnode *node );
extern Fnode *Reg_NsFunc( Fnode *node );
extern Fnode *Func_FirstArg( Fnode *node );
extern Fnode *Func_SecondArg( Fnode *node );
extern Fnode *Func_ThirdArg( Fnode *node );
extern Fnode* Func_NextArg (Fnode *node, Fnode *node);
extern st_table *nodeGetSupport( F aNode );
extern void nodeGetSupportRecur( F aNode, st_table *result, st_table *processedTable );
extern void reg( F aReg, F nextState, F initState );
extern Fnode *Net_NameToNode( Net_t *net, char *name );
extern Net_t *Net_CreateFromFormula( Fnode *aFormula );
extern Net_t *Net_CreateFromFormulaArray( array_t *aFormulas );
extern int Net_FreeNet( Net_t *net );
extern int Net_PopulateFields( Net_t *net, Fnode *aFormula, Fnode *parentFormula, st_table *processedNodes );
extern int Net_DoBryantReduction( Net_t *net );
extern int Net_PrintFormula( Net_t *net, Fnode *formula, char *filename);
extern int Node_PrintVHDL( Net_t *net, Fnode *formula, FILE *fptr, st_table *nodeToNameHash, st_table *processedNodes, st_table *uifInstantiateHash, st_table *uifToNumInputs, int vector_width);
extern int Net_NodeGetId( Net_t *net, Fnode *formula );
extern int Net_ConstrainInput( Net_t *net, char *input, Fnode *const_formula );
extern int Net_UnConstrainInput( Net_t *net, char *input, Fnode *const_formula );
extern array_t *node_array_tfe( array_t *input_array, int N );
extern Fnode *node_tfe( Fnode *formula, int N );
extern int ReplaceWritewithRead( Net_t *net, char *writeUifName, char *readUifName);
extern int AddReadatEnd(Net_t *net, Fnode *readAddress, char *readUifName, int formula_index);
extern int Net_TopologicalSort(Fnode *aFormula, st_table *sortedTable, st_table *processedNodes);
extern int Net_ConstantPropagation(st_table *sortedTable, st_table *equivalentNodeHash, int max_depth);
extern Fnode* Net_SimplifyUsingConstantPropagation(Fnode *aFormula);
extern Fv ivec( char *name, int N, int boolean );
extern Fvector *ivecraw( char *name, int N, int boolean );
extern Fv sivec( char *name, int N );
extern Fv bivec( char *name, int N );
extern Fmatrix *imatrixraw( char *name, int N, int M, int boolean );
extern Fm imatrix( char *name, int N, int M, int boolean );
extern Fm simatrix( char *name, int N, int M );
extern Fm bimatrix( char *name, int N, int M );
extern Fmatrix *bcm( int N, int M, int value );
extern Fmatrix *raw_matrix( int N, int M );
extern Fvector *raw_vector( int M );
extern F matrix_lone_cols( Fm A );
extern F matrix_lone_rows( Fm A );
extern F vector_lone( Fv x );
extern  Fv operator*( Fv x, Fm M);
extern F mexists( Fm A );
extern F mforall( Fm A );
extern F vexists( Fv A );
extern F vforall( Fv A );
extern F build_dlx();
extern array_t *build_dlx_impl();
extern array_t *build_dlx_impl2();
extern F build_dlx_spec();
extern array_t *build_dlx_spec2();
extern array_t *build_dlx_spec3();
extern F build_fs();
extern F build_dlxuclidmain();
extern F build_dlxuclidmain_nosimplify();
extern F build_dlxuclid_seq();
extern bdd_t *nodeComputeBdd( F aNode );
extern int test_bdd();
extern int bdd_print_dot( bdd_t *aBdd );
extern int bdd_print_recur( bdd_t *aBdd, st_table *processedTable );
extern int bdd_cmp( char *aBdd, char *bBdd );
extern int bdd_hash( char *aBdd, int modulus );
extern st_table *Net_ReadNodeVals( char * );
extern int Net_CheckBurchFeasibility(Fnode *aFormula, Fnode *ctrl_child);
extern void Net_CollectMuxes(Fnode *aFormula, st_table *mux_hash);
extern F build_dlx_uclid_wholemodel();
extern array_t * build_double_instr();
extern F build_microarch_wrapper();
extern array_t * build_single_instr();
extern F build_dlx_uclid_compare();
extern array_t * build_dlx_uclid_spec();
extern array_t *build_dlx_uclid_impl();
extern F build_dlx_uclid_superscalar();
extern F build_dlx_uclid_superscalar_seq();
extern F build_fold_unfold_check();
extern void NodeAssignRegister( F reg,
                                F init_state, 
                                F next_state);
extern Net_t* Net_ReplaceWritewithRead( Net_t *net, 
                                        char *writeUifName, 
                                        char *readUifName,
                                        int output_index);
extern Fnode* Net_AccessOutput (Net_t *net,
                                int output_index);

extern int Net_PrintVHDL (Net_t * net, int scalarWidth, char *fileName, char *entityName="example");
extern int Net_SetMemSize (Net_t *net, char *memName, int memSize);
extern int Net_AnalyzeScalarBitWidth (Net_t *net);
#ifdef __cplusplus
} /* extern "C" */
#endif


#endif /* _TRK */

---