source: vis_dev/dev/utilities.h @ 18

#ifndef UTILITIES_H_
#define UTILITIES_H_
#include "ntk.h"
#include "ord.h"
#include "part.h"
#include "maig.h"
#include "ntmaig.h"
#include "fsm.h"
#include "ctlp.h"
#include "ctlsp.h"
#include "mcInt.h"
#include "grabInt.h"
#include "bmc.h"
#include "bmcInt.h"
#include "satInt.h"
#include <stdio.h>
#include <stdlib.h>


static int
nodenameCompare(
  const void * node1,
  const void * node2)
{
Ntk_Node_t *v1, *v2;
char *name1, *name2;

  v1 = *(Ntk_Node_t **)(node1);
  v2 = *(Ntk_Node_t **)(node2);
  name1 = Ntk_NodeReadName(v1);
  name2 = Ntk_NodeReadName(v2);
  
  return (strcmp(name1, name2));
} 

// Read blifmv file 
Hrc_Manager_t * rlmv(FILE * file);
//flatten_hier
// @ return the network
Ntk_Network_t * flatten_hier(Hrc_Manager_t * hmgr);
// Build_partition_maigs  
// @ return table node_ntk to aigTable
st_table * build_partition_maigs(Ntk_Network_t * ntk);
void printNodeToMvFaigTable(st_table* nodeToMvfAigTable);
// print name of table containing Ntk_Node_t
void printLatch(st_table* CoiTable);
// generate all node of a network
// @return a table with all node of a given network
st_table * generateAllLatches(Ntk_Network_t * ntk);
// Create unroll circuit k steps  
// Build SAT instance
//   Create clauses database 
//       BmcOption_t *options =  BmcOptionAlloc();
//   BmcCnfClauses_t   *cnfClauses = NIL(BmcCnfClauses_t);
//       cnfClauses = BmcCnfClausesAlloc();
void build_unroll_circuit(Ntk_Network_t * ntk, int bound,BmcOption_t * options,BmcCnfClauses_t* cnfClauses);
void printSATAssig( array_t* result);
void printCNFIndex(BmcCnfClauses_t* cnfClauses);
void printCNFClauses(BmcCnfClauses_t* cnfClauses);
void printClauseLits(satManager_t *cm,long concl,FILE * file);
int getClsIndex(long concl,int numVarInCnf);
void printSatArrayCore(satManager_t *cm,satArray_t *clauseIndexInCore);
void printSatArrayCoreToCnf(satManager_t *cm,satArray_t *clauseIndexInCore, char *filename);
// Check Sat
// @return array_t empty if unsat
// else print cex with : 
//      BmcPrintCounterExample(ntk1,nodeToMvfAigTable,cnfClauses,result,steps,CoiTable,options, NIL(array_t));

array_t * checkSATCircus( satManager_t *cm,BmcOption_t * options, boolean unsatcore,    satArray_t *clauseIndexInCore);
int findIndex(BmcCnfClauses_t* cnfClauses , char * nodeName);
// Add val to state register
mdd_t * buildBdd4StateVal(array_t* stateName, int max, array_t * val, mdd_manager * mddManager);
void addObjState(array_t* stateName, int max, array_t * val, int steps,BmcCnfClauses_t *cnfClauses);

#endif