source: vis_dev/dev/utilities.h @ 83

Last change on this file since 83 was 20, checked in by cecile, 13 years ago

main modified

File size: 2.7 KB
Line 
1#ifndef UTILITIES_H_
2#define UTILITIES_H_
3#include "ntk.h"
4#include "ord.h"
5#include "part.h"
6#include "maig.h"
7#include "ntmaig.h"
8#include "fsm.h"
9#include "ctlp.h"
10#include "ctlsp.h"
11#include "mcInt.h"
12#include "grabInt.h"
13#include "bmc.h"
14#include "bmcInt.h"
15#include "satInt.h"
16#include <stdio.h>
17#include <stdlib.h>
18/********************************************/
19/******* Vis magic formulae *****************/
20FILE *vis_stderr;
21FILE *vis_stdout;
22FILE *vis_historyFile;
23FILE *vis_stdpipe;
24array_t *vm_commandHistoryArray;
25char *vm_programName;
26/********************************************/
27
28
29int
30nodenameCompare(
31  const void * node1,
32  const void * node2)
33{
34Ntk_Node_t *v1, *v2;
35char *name1, *name2;
36
37  v1 = *(Ntk_Node_t **)(node1);
38  v2 = *(Ntk_Node_t **)(node2);
39  name1 = Ntk_NodeReadName(v1);
40  name2 = Ntk_NodeReadName(v2);
41 
42  return (strcmp(name1, name2));
43} 
44// Read blifmv file
45Hrc_Manager_t * rlmv(FILE * file);
46//flatten_hier
47// @ return the network
48Ntk_Network_t * flatten_hier(Hrc_Manager_t * hmgr);
49// Build_partition_maigs 
50// @ return table node_ntk to aigTable
51st_table * build_partition_maigs(Ntk_Network_t * ntk);
52void printNodeToMvFaigTable(st_table* nodeToMvfAigTable);
53// print name of table containing Ntk_Node_t
54void printLatch(st_table* CoiTable);
55// generate all node of a network
56// @return a table with all node of a given network
57st_table * generateAllLatches(Ntk_Network_t * ntk);
58// Create unroll circuit k steps 
59// Build SAT instance
60//   Create clauses database
61//       BmcOption_t *options =  BmcOptionAlloc();
62//   BmcCnfClauses_t   *cnfClauses = NIL(BmcCnfClauses_t);
63//       cnfClauses = BmcCnfClausesAlloc();
64void build_unroll_circuit(Ntk_Network_t * ntk, int bound,BmcOption_t * options,BmcCnfClauses_t* cnfClauses);
65void printSATAssig( array_t* result);
66void printCNFIndex(BmcCnfClauses_t* cnfClauses);
67void printCNFClauses(BmcCnfClauses_t* cnfClauses);
68void printClauseLits(satManager_t *cm,long concl,FILE * file);
69int getClsIndex(long concl,int numVarInCnf);
70void printSatArrayCore(satManager_t *cm,satArray_t *clauseIndexInCore);
71void printSatArrayCoreToCnf(satManager_t *cm,satArray_t *clauseIndexInCore, char *filename);
72// Check Sat
73// @return array_t empty if unsat
74// else print cex with :
75//      BmcPrintCounterExample(ntk1,nodeToMvfAigTable,cnfClauses,result,steps,CoiTable,options, NIL(array_t));
76
77array_t * checkSATCircus( satManager_t *cm,BmcOption_t * options, boolean unsatcore,    satArray_t *clauseIndexInCore);
78int findIndex(BmcCnfClauses_t* cnfClauses , char * nodeName);
79// Add val to state register
80mdd_t * buildBdd4StateVal(array_t* stateName, int max, array_t * val, mdd_manager * mddManager);
81void addObjState(array_t* stateName, int max, array_t * val, int steps,BmcCnfClauses_t *cnfClauses);
82
83#endif
Note: See TracBrowser for help on using the repository browser.