first commit

AUTHORS.md

+# Authors
+
+This project has been mainly developed by:
+
+- Yasmine CHOUIKHA (Université Sorbonne Paris Nord)

Causality/main.cpp

+#include <time.h>
+#include <iostream>
+#include <string>
+
+
+#include <iomanip>
+#include<fstream>
+#include <map>
+#include <cmath>
+#include <algorithm>
+
+using namespace std;
+#include "Net.h"
+#include "Net.cpp"
+#include "bdd.h"
+#include "fdd.h"
+
+#include "RdPBDD.h"
+
+double getTime(){
+	return (double)clock() / (double)CLOCKS_PER_SEC;
+}
+  
+int main(int argc, char** argv) {
+
+if (argc <=2 or std::string(argv[1]).find("help")!=-1)
+cout <<"/**************************************************************/\n/********************         help         ********************/ \n -To generate the reachability graph: use the option -r <filename.net>. \n -To generate test paths covering the given observable transitions t1,t2...tn: use the option -o <filename.net> <fileobs.txt >. \n -To generate test paths using structural analysis: use the option -a <filename.net>\n -To generate the conplete SOG corresponding to obs trans: use the option -c <filename.net>/**************************************************************/"<<endl;
+
+
+else{
+  	string option= std::string (argv[1]);
+  	cout << "nom fichier source " << endl;
+	cout<<"Fichier net : "<<argv[2]<<endl;
+	net R(argv[2]);	
+	cout << "parser...done" << endl;
+	set <vector<int>> abstrait;
+    int pp=string(argv[2]).find(".n");
+    int ps=string(argv[2]).rfind("/");
+    string nom=string(argv[2]).substr(ps+1,pp-ps-1);
+    double d,tps;  
+    int b = 32;
+    map<int,int> obs;
+    set<int> unobs;
+    set<vector<int>> chemins;
+   
+    d = getTime();
+
+
+
+
+// option -a for structural analysis 
+if(!option.compare("-a")or !option.compare("-o")or !option.compare("-c")){
+ 
+ if (!option.compare("-a")or !option.compare("-c")){
+    unobs=R.calcul1();
+    for (long unsigned int i = 0; i < R.transitions.size(); i++ )
+    {
+         if ((unobs.find(i))== unobs.end())
+         {
+             obs.insert({i,1}); 
+         }  
+    }
+  } 
+    
+ if (!option.compare("-o")){      //lire les trnansitions observable a partie d'un fichier 
+ ifstream flux(argv[3]); 
+     string ligne;
+	if (flux){
+	while(getline(flux, ligne))
+		{
+		int tr =stoi(ligne.substr(1)); // le ligne sous forme de t1 prendre le1
+		 obs.insert({tr,1}); 
+		}
+ 
+	}
+	for (long unsigned int i = 0; i < R.transitions.size(); i++ )
+    {
+         if ((obs.find(i))== obs.end())
+         {
+             unobs.insert(i); 
+         }  
+    }
+ }
+
+
+  
+    RdPBDD DR(R,obs,unobs, b);
+    cout<<"RdpBDD construit"<<endl;
+    MDGraph g;
+
+
+if(!option.compare("-c") ) { 
+	DR.complete_sog(g,obs);
+      	g.generate_Dotfile_of_reachability_graph("complete_sog_"+nom);
+      	 cout << " Result in ./result/complete_sog_"+nom+".dot" << endl;
+}
+
+ ofstream monFlux("./result/result_no_opt_"+nom+".txt");
+
+ int n=0;
+if(!option.compare("-a")or !option.compare("-o"))
+{ chemins= DR.chem_obs(g,obs);
+ monFlux<<"le nombre de chemins observés: "<<chemins.size()<<endl;
+ for (auto i: chemins)
+ {
+  n++;
+  monFlux<<"le "<<n<<" ch: " <<i.size()<< " tr."<<endl; //result in file result/result_no_opt.txt"
+
+  vector<int> chem_abs;
+  chem_abs= DR.chem_abs(i,g);
+  
+  abstrait.insert(chem_abs);
+}
+
+  
+  
+ tps = getTime() - d;
+
+  
+ cout << " Temps de construction du graphe d'observation " << tps << endl;
+ g.printCompleteInformation();
+ cout<< "transition "<<R.transitions.size()<<endl;
+ cout<< "places "<<R.places.size()<<endl;
+ cout<< "trans obs "<<obs.size()<<endl;
+ cout<< "--- abstract path ----"<<endl;
+ set<int> visit;
+ float somme =0 ;
+ float ecart=0; 
+
+
+ for (auto i: abstrait)
+  {
+ 
+  for (auto tr:i)
+   {
+    visit.insert(tr);
+   }
+
+     somme=somme+i.size();
+     
+ }
+  
+ 
+    
+float moy= somme/(abstrait.size());
+cout<< "nb de chemins: "<<abstrait.size()<<endl;
+cout<< "nb moyen de transitions par chemin: "<<moy<<endl;
+
+    
+for (auto i: abstrait)
+ {
+
+ecart = ecart+ (((i.size()-moy)*(i.size()-moy))); 
+
+     
+  }
+
+    ecart =pow((ecart/abstrait.size()),0.5);
+    cout<< "ecart type: "<<ecart<<endl;
+
+      cout<< "nb of covered transitions: "<< visit.size()<<endl;  
+       cout << " Result in  " << "./result/result_no_opt_"+nom+".txt" << endl;
+	return 0;
+
+} 
+
+
+
+ }
+
+else if (!option.compare("-r")){
+    for (long unsigned int i = 0; i < R.transitions.size(); i++ )
+    {
+
+             obs.insert({i,1});  
+    }	
+  
+    RdPBDD DR(R,obs,unobs, b);
+    MDGraph g;
+    DR.complete_sog(g,obs);
+    g.generate_Dotfile_of_reachability_graph("reach_"+nom);
+   return 0;
+    }
+
+ 
+ }
+ }

Causality/src/bddio.c

+/*========================================================================
+               Copyright (C) 1996-2002 by Jorn Lind-Nielsen
+                            All rights reserved
+
+    Permission is hereby granted, without written agreement and without
+    license or royalty fees, to use, reproduce, prepare derivative
+    works, distribute, and display this software and its documentation
+    for any purpose, provided that (1) the above copyright notice and
+    the following two paragraphs appear in all copies of the source code
+    and (2) redistributions, including without limitation binaries,
+    reproduce these notices in the supporting documentation. Substantial
+    modifications to this software may be copyrighted by their authors
+    and need not follow the licensing terms described here, provided
+    that the new terms are clearly indicated in all files where they apply.
+
+    IN NO EVENT SHALL JORN LIND-NIELSEN, OR DISTRIBUTORS OF THIS
+    SOFTWARE BE LIABLE TO ANY PARTY FOR DIRECT, INDIRECT, SPECIAL,
+    INCIDENTAL, OR CONSEQUENTIAL DAMAGES ARISING OUT OF THE USE OF THIS
+    SOFTWARE AND ITS DOCUMENTATION, EVEN IF THE AUTHORS OR ANY OF THE
+    ABOVE PARTIES HAVE BEEN ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
+
+    JORN LIND-NIELSEN SPECIFICALLY DISCLAIM ANY WARRANTIES, INCLUDING,
+    BUT NOT LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND
+    FITNESS FOR A PARTICULAR PURPOSE. THE SOFTWARE PROVIDED HEREUNDER IS
+    ON AN "AS IS" BASIS, AND THE AUTHORS AND DISTRIBUTORS HAVE NO
+    OBLIGATION TO PROVIDE MAINTENANCE, SUPPORT, UPDATES, ENHANCEMENTS, OR
+    MODIFICATIONS.
+========================================================================*/
+
+/*************************************************************************
+  $Header: /home/jln/phd/bdd/src/RCS/bddio.c,v 1.5 2000/05/31 19:11:43 jln Exp jln $
+  FILE:  bddio.c
+  DESCR: File I/O routines for BDD package
+  AUTH:  Jorn Lind
+  DATE:  (C) june 1997
+*************************************************************************/
+#include <string.h>
+#include <stdlib.h>
+#include <fcntl.h>
+#include <assert.h>
+#include <sys/stat.h>
+#include "kernel.h"
+
+static void bdd_printset_rec(FILE *, int, int *);
+static void bdd_fprintdot_rec(FILE*, BDD);
+static int  bdd_save_rec(FILE*, int);
+static int  bdd_loaddata(FILE *);
+static int  loadhash_get(int);
+static void loadhash_add(int, int);
+
+static bddfilehandler filehandler;
+
+typedef struct s_LoadHash
+{
+   int key;
+   int data;
+   int first;
+   int next;
+} LoadHash;
+
+static LoadHash *lh_table;
+static int       lh_freepos;
+static int       lh_nodenum;
+static int      *loadvar2level;
+
+/*=== PRINTING ========================================================*/
+
+
+/*
+NAME    {* bdd\_file\_hook *}
+SECTION {* kernel *}
+SHORT   {* Specifies a printing callback handler *}
+PROTO   {* bddfilehandler bdd_file_hook(bddfilehandler handler) *}
+DESCR   {* A printing callback handler for use with BDDs is used to
+           convert the BDD variable number into something readable by the
+	   end user. Typically the handler will print a string name
+	   instead of the number. A handler could look like this:
+	   \begin{verbatim}
+void printhandler(FILE *o, int var)
+{
+   extern char **names;
+   fprintf(o, "%s", names[var]);
+}
+\end{verbatim}
+
+           \noindent
+           The handler can then be passed to BuDDy like this:
+	   {\tt bdd\_file\_hook(printhandler)}.
+
+	   No default handler is supplied. The argument {\tt handler} may be
+	   NULL if no handler is needed. *}
+RETURN  {* The old handler *}
+ALSO    {* bdd\_printset, bdd\_strm\_hook, fdd\_file\_hook *}
+*/
+bddfilehandler bdd_file_hook(bddfilehandler handler)
+{
+   bddfilehandler old = filehandler;
+   filehandler = handler;
+   return old;
+}
+
+
+/*
+NAME    {* bdd\_printall *}
+EXTRA   {* bdd\_fprintall *}
+SECTION {* fileio *}
+SHORT   {* prints all used entries in the node table *}
+PROTO   {* void bdd_printall(void)
+void bdd_fprintall(FILE* ofile) *}
+DESCR   {* Prints to either stdout or the file {\tt ofile} all the used
+           entries in the main node table. The format is:
+	   \begin{Ill}
+  	     {\tt [Nodenum] Var/level Low High}
+	   \end{Ill}
+	   Where {\tt Nodenum} is the position in the node table and level
+	   is the position in the current variable order. *}
+ALSO    {* bdd\_printtable, bdd\_printset, bdd\_printdot *}
+*/
+void bdd_printall(void)
+{
+   bdd_fprintall(stdout);
+}
+
+
+void bdd_fprintall(FILE *ofile)
+{
+   int n;
+   
+   for (n=0 ; n<bddnodesize ; n++)
+   {
+      if (LOW(n) != -1)
+      {
+	 fprintf(ofile, "[%5d - %2d] ", n, bddnodes[n].refcou);
+	 if (filehandler)
+	    filehandler(ofile, bddlevel2var[LEVEL(n)]);
+	 else
+	    fprintf(ofile, "%3d", bddlevel2var[LEVEL(n)]);
+
+	 fprintf(ofile, ": %3d", LOW(n));
+	 fprintf(ofile, " %3d", HIGH(n));
+	 fprintf(ofile, "\n");
+      }
+   }
+}
+
+
+/*
+NAME    {* bdd\_printtable *}
+EXTRA   {* bdd\_fprinttable *}
+SECTION {* fileio *}
+SHORT   {* prints the node table entries used by a BDD *}
+PROTO   {* void bdd_printtable(BDD r)
+void bdd_fprinttable(FILE* ofile, BDD r) *}
+DESCR   {* Prints to either stdout or the file {\tt ofile} all the entries
+           in the main node table used by {\tt r}. The format is:
+	   \begin{Ill}
+  	     {\tt [Nodenum] Var/level :  Low High}
+	   \end{Ill}
+	   Where {\tt Nodenum} is the position in the node table and level
+	   is the position in the current variable order. *}
+ALSO    {* bdd\_printall, bdd\_printset, bdd\_printdot *}
+*/
+void bdd_printtable(BDD r)
+{
+   bdd_fprinttable(stdout, r);
+}
+
+
+void bdd_fprinttable(FILE *ofile, BDD r)
+{
+   BddNode *node;
+   int n;
+   
+   fprintf(ofile, "ROOT: %d\n", r);
+   if (r < 2)
+      return;
+
+   bdd_mark(r);
+   
+   for (n=0 ; n<bddnodesize ; n++)
+   {
+      if (LEVEL(n) & MARKON)
+      {
+	 node = &bddnodes[n];
+	 
+	 LEVELp(node) &= MARKOFF;
+
+	 fprintf(ofile, "[%5d] ", n);
+	 if (filehandler)
+	    filehandler(ofile, bddlevel2var[LEVELp(node)]);
+	 else
+	    fprintf(ofile, "%3d", bddlevel2var[LEVELp(node)]);
+
+	 fprintf(ofile, ": %3d", LOWp(node));
+	 fprintf(ofile, " %3d", HIGHp(node));
+	 fprintf(ofile, "\n");
+      }
+   }
+}
+
+
+/*
+NAME    {* bdd\_printset *}
+EXTRA   {* bdd\_fprintset *}
+SECTION {* fileio *}
+SHORT   {* prints the set of truth assignments specified by a BDD *}
+PROTO   {* bdd_printset(BDD r)
+bdd_fprintset(FILE* ofile, BDD r) *}
+DESCR   {* Prints all the truth assignments for {\tt r} that would yield
+           it true. The format is:
+	   \begin{Ill}
+	     {\tt < $x_{1,1}:c_{1,1},\ldots,x_{1,n_1}:c_{1,n_1}$ >\\
+	          < $x_{2,1}:c_{2,1},\ldots,x_{2,n_2}:c_{2,n_2}$ >\\
+		  $\ldots$ \\
+	          < $x_{N,1}:c_{N,1},\ldots,x_{N,n_3}:c_{N,n_3}$ > }
+	   \end{Ill} 
+	   Where the $x$'s are variable numbers (and the position in the
+	   current order) and the $c$'s are the
+	   possible assignments to these. Each set of brackets designates
+	   one possible assignment to the set of variables that make up the
+	   BDD. All variables not shown are don't cares. It is possible to
+	   specify a callback handler for printing of the variables using
+	   {\tt bdd\_file\_hook} or {\tt bdd\_strm\_hook}. *}
+ALSO    {* bdd\_printall, bdd\_printtable, bdd\_printdot, bdd\_file\_hook, bdd\_strm\_hook *}
+*/
+void bdd_printset(BDD r)
+{
+   bdd_fprintset(stdout, r);
+}
+
+
+void bdd_fprintset(FILE *ofile, BDD r)
+{
+   int *set;
+   
+   if (r < 2)
+   {
+      fprintf(ofile, "%s", r == 0 ? "F" : "T");
+      return;
+   }
+
+   if ((set=(int *)malloc(sizeof(int)*bddvarnum)) == NULL)
+   {
+      bdd_error(BDD_MEMORY);
+      return;
+   }
+   
+   memset(set, 0, sizeof(int) * bddvarnum);
+   bdd_printset_rec(ofile, r, set);
+   free(set);
+}
+
+
+static void bdd_printset_rec(FILE *ofile, int r, int *set)
+{
+   int n;
+   int first;
+   
+   if (r == 0)
+      return;
+   else
+   if (r == 1)
+   {
+      fprintf(ofile, "<");
+      first = 1;
+      
+      for (n=0 ; n<bddvarnum ; n++)
+      {
+	 if (set[n] > 0)
+	 {
+	    if (!first)
+	       fprintf(ofile, ", ");
+	    first = 0;
+	    if (filehandler)
+	       filehandler(ofile, bddlevel2var[n]);
+	    else
+	       fprintf(ofile, "%d", bddlevel2var[n]);
+	    fprintf(ofile, ":%d", (set[n]==2 ? 1 : 0));
+	 }
+      }
+
+      fprintf(ofile, ">");
+   }
+   else
+   {
+      set[LEVEL(r)] = 1;
+      bdd_printset_rec(ofile, LOW(r), set);
+      
+      set[LEVEL(r)] = 2;
+      bdd_printset_rec(ofile, HIGH(r), set);
+      
+      set[LEVEL(r)] = 0;
+   }
+}
+
+
+/*
+NAME    {* bdd\_printdot *}
+EXTRA   {* bdd\_fprintdot *}
+SECTION {* fileio *}
+SHORT   {* prints a description of a BDD in DOT format *}
+PROTO   {* void bdd_printdot(BDD r)
+int bdd_fnprintdot(char* fname, BDD r)
+void bdd_fprintdot(FILE* ofile, BDD r) *}
+DESCR   {* Prints a BDD in a format suitable for use with the graph
+           drawing program DOT to either stdout, a designated file
+	   {\tt ofile} or the file named by {\tt fname}. In the last case
+	   the file will be opened for writing, any previous contents
+	   destroyed and then closed again. *}
+ALSO    {* bdd\_printall, bdd\_printtable, bdd\_printset *}
+*/
+void bdd_printdot(BDD r)
+{
+   bdd_fprintdot(stdout, r);
+}
+
+
+int bdd_fnprintdot(char *fname, BDD r)
+{
+   FILE *ofile = fopen(fname, "w");
+   if (ofile == NULL)
+      return bdd_error(BDD_FILE);
+   bdd_fprintdot(ofile, r);
+   fclose(ofile);
+   return 0;
+}
+
+
+void bdd_fprintdot(FILE* ofile, BDD r)
+{
+   fprintf(ofile, "digraph G {\n");
+   fprintf(ofile, "0 [shape=box, label=\"0\", style=filled, shape=box, height=0.3, width=0.3];\n");
+   fprintf(ofile, "1 [shape=box, label=\"1\", style=filled, shape=box, height=0.3, width=0.3];\n");
+
+   bdd_fprintdot_rec(ofile, r);
+
+   fprintf(ofile, "}\n");
+
+   bdd_unmark(r);
+}
+
+
+static void bdd_fprintdot_rec(FILE* ofile, BDD r)
+{
+   if (ISCONST(r) || MARKED(r))
+      return;
+
+   fprintf(ofile, "%d [label=\"", r);
+   if (filehandler)
+      filehandler(ofile, bddlevel2var[LEVEL(r)]);
+   else
+      fprintf(ofile, "%d", bddlevel2var[LEVEL(r)]);
+   fprintf(ofile, "\"];\n");
+
+   fprintf(ofile, "%d -> %d [style=dotted];\n", r, LOW(r));
+   fprintf(ofile, "%d -> %d [style=filled];\n", r, HIGH(r));
+
+   SETMARK(r);
+   
+   bdd_fprintdot_rec(ofile, LOW(r));
+   bdd_fprintdot_rec(ofile, HIGH(r));
+}
+
+
+/*=== SAVE =============================================================*/
+
+/*
+NAME    {* bdd\_save *}
+EXTRA   {* bdd\_fnsave *}
+SECTION {* fileio *}
+SHORT   {* saves a BDD to a file *}
+PROTO   {* int bdd_fnsave(char *fname, BDD r)
+int bdd_save(FILE *ofile, BDD r) *}
+DESCR   {* Saves the nodes used by {\tt r} to either a file {\tt ofile}
+           which must be opened for writing or to the file named {\tt fname}.
+	   In the last case the file will be truncated and opened for
+	   writing. *}
+ALSO    {* bdd\_load *}
+RETURN  {* Zero on succes, otherwise an error code from {\tt bdd.h}. *}
+*/
+int bdd_fnsave(char *fname, BDD r)
+{
+   FILE *ofile;
+   int ok;
+
+   if ((ofile=fopen(fname,"w")) == NULL)
+      return bdd_error(BDD_FILE);
+
+   ok = bdd_save(ofile, r);
+   fclose(ofile);
+   return ok;
+}
+
+
+int bdd_save(FILE *ofile, BDD r)
+{
+   int err, n=0;
+
+   if (r < 2)
+   {
+      fprintf(ofile, "0 0 %d\n", r);
+      return 0;
+   }
+   
+   bdd_markcount(r, &n);
+   bdd_unmark(r);
+   fprintf(ofile, "%d %d\n", n, bddvarnum);
+
+   for (n=0 ; n<bddvarnum ; n++)
+      fprintf(ofile, "%d ", bddvar2level[n]);
+   fprintf(ofile, "\n");
+   
+   err = bdd_save_rec(ofile, r);
+   bdd_unmark(r);
+
+   return err;
+}
+
+
+static int bdd_save_rec(FILE *ofile, int root)
+{
+   BddNode *node = &bddnodes[root];
+   int err;
+   
+   if (root < 2)
+      return 0;
+
+   if (LEVELp(node) & MARKON)
+      return 0;
+   LEVELp(node) |= MARKON;
+   
+   if ((err=bdd_save_rec(ofile, LOWp(node))) < 0)
+      return err;
+   if ((err=bdd_save_rec(ofile, HIGHp(node))) < 0)
+      return err;
+
+   fprintf(ofile, "%d %d %d %d\n",
+	   root, bddlevel2var[LEVELp(node) & MARKHIDE],
+	   LOWp(node), HIGHp(node));
+
+   return 0;
+}
+
+
+/*=== LOAD =============================================================*/
+
+/*
+NAME    {* bdd\_load *}
+EXTRA   {* bdd\_fnload *}
+SECTION {* fileio *}
+SHORT   {* loads a BDD from a file *}
+PROTO   {* int bdd_fnload(char *fname, BDD *r)
+int bdd_load(FILE *ifile, BDD *r) *}
+DESCR   {* Loads a BDD from a file into the BDD pointed to by {\tt r}.
+           The file can either be the file {\tt ifile} which must be opened
+	   for reading or the file named {\tt fname} which will be opened
+	   automatically for reading.
+
+	   The input file format consists of integers arranged in the following
+	   manner. First the number of nodes $N$ used by the BDD and then the
+	   number of variables $V$ allocated and the variable ordering
+	   in use at the time the BDD was saved.
+	   If $N$ and $V$ are both zero then the BDD is either the constant
+	   true or false BDD, indicated by a $1$ or a $0$ as the next integer.
+
+	   In any other case the next $N$ sets of $4$ integers will describe
+	   the nodes used by the BDD. Each set consists of first the node
+	   number, then the variable number and then the low and high nodes.
+
+	   The nodes {\it must} be saved in a order such that any low or
+	   high node must be defined before it is mentioned. *}
+ALSO    {* bdd\_save *}
+RETURN  {* Zero on succes, otherwise an error code from {\tt bdd.h}. *}
+*/
+int bdd_fnload(char *fname, BDD *root)
+{
+   FILE *ifile;
+   int ok;
+
+   if ((ifile=fopen(fname,"r")) == NULL)
+      return bdd_error(BDD_FILE);
+
+   ok = bdd_load(ifile, root);
+   fclose(ifile);
+   return ok;
+}
+
+
+int bdd_load(FILE *ifile, BDD *root)
+{
+   int n, vnum, tmproot;
+
+   if (fscanf(ifile, "%d %d", &lh_nodenum, &vnum) != 2)
+      return bdd_error(BDD_FORMAT);
+
+      /* Check for constant true / false */
+   if (lh_nodenum==0  &&  vnum==0)
+   {
+      fscanf(ifile, "%d", root);
+      return 0;
+   }
+
+   if ((loadvar2level=(int*)malloc(sizeof(int)*vnum)) == NULL)
+      return bdd_error(BDD_MEMORY);
+   for (n=0 ; n<vnum ; n++)
+      fscanf(ifile, "%d", &loadvar2level[n]);
+   
+   if (vnum > bddvarnum)
+      bdd_setvarnum(vnum);
+
+   if ((lh_table=(LoadHash*)malloc(lh_nodenum*sizeof(LoadHash))) == NULL)
+      return bdd_error(BDD_MEMORY);
+   
+   for (n=0 ; n<lh_nodenum ; n++)
+   {
+      lh_table[n].first = -1;
+      lh_table[n].next = n+1;
+   }
+   lh_table[lh_nodenum-1].next = -1;
+   lh_freepos = 0;
+
+   tmproot = bdd_loaddata(ifile);
+
+   for (n=0 ; n<lh_nodenum ; n++)
+      bdd_delref(lh_table[n].data);
+   
+   free(lh_table);
+   free(loadvar2level);
+   
+   *root = 0;
+   if (tmproot < 0)
+      return tmproot;
+   else
+      *root = tmproot;
+   
+   return 0;
+}
+
+
+static int bdd_loaddata(FILE *ifile)
+{
+   int key,var,low,high,root=0,n;
+   
+   for (n=0 ; n<lh_nodenum ; n++)
+   {
+      if (fscanf(ifile,"%d %d %d %d", &key, &var, &low, &high) != 4)
+	 return bdd_error(BDD_FORMAT);
+
+      if (low >= 2)
+	 low = loadhash_get(low);
+      if (high >= 2)
+	 high = loadhash_get(high);
+
+      if (low<0 || high<0 || var<0)
+	 return bdd_error(BDD_FORMAT);
+
+      root = bdd_addref( bdd_ite(bdd_ithvar(var), high, low) );
+
+      loadhash_add(key, root);
+   }
+
+   return root;
+}
+
+
+static void loadhash_add(int key, int data)
+{
+   int hash = key % lh_nodenum;
+   int pos = lh_freepos;
+
+   lh_freepos = lh_table[pos].next;
+   lh_table[pos].next = lh_table[hash].first;
+   lh_table[hash].first = pos;
+
+   lh_table[pos].key = key;
+   lh_table[pos].data = data;
+}
+
+
+static int loadhash_get(int key)
+{
+   int hash = lh_table[key % lh_nodenum].first;
+
+   while (hash != -1  &&  lh_table[hash].key != key)
+      hash = lh_table[hash].next;
+
+   if (hash == -1)
+      return -1;
+   return lh_table[hash].data;
+}
+
+
+/* EOF */

Causality/src/bddtest.cxx

+/*========================================================================
+               Copyright (C) 1996-2002 by Jorn Lind-Nielsen
+                            All rights reserved
+
+    Permission is hereby granted, without written agreement and without
+    license or royalty fees, to use, reproduce, prepare derivative
+    works, distribute, and display this software and its documentation
+    for any purpose, provided that (1) the above copyright notice and
+    the following two paragraphs appear in all copies of the source code
+    and (2) redistributions, including without limitation binaries,
+    reproduce these notices in the supporting documentation. Substantial
+    modifications to this software may be copyrighted by their authors
+    and need not follow the licensing terms described here, provided
+    that the new terms are clearly indicated in all files where they apply.
+
+    IN NO EVENT SHALL JORN LIND-NIELSEN, OR DISTRIBUTORS OF THIS
+    SOFTWARE BE LIABLE TO ANY PARTY FOR DIRECT, INDIRECT, SPECIAL,
+    INCIDENTAL, OR CONSEQUENTIAL DAMAGES ARISING OUT OF THE USE OF THIS
+    SOFTWARE AND ITS DOCUMENTATION, EVEN IF THE AUTHORS OR ANY OF THE
+    ABOVE PARTIES HAVE BEEN ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
+
+    JORN LIND-NIELSEN SPECIFICALLY DISCLAIM ANY WARRANTIES, INCLUDING,
+    BUT NOT LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND
+    FITNESS FOR A PARTICULAR PURPOSE. THE SOFTWARE PROVIDED HEREUNDER IS
+    ON AN "AS IS" BASIS, AND THE AUTHORS AND DISTRIBUTORS HAVE NO
+    OBLIGATION TO PROVIDE MAINTENANCE, SUPPORT, UPDATES, ENHANCEMENTS, OR
+    MODIFICATIONS.
+========================================================================*/
+
+#include <string>
+#include "bdd.h"
+#include "bvec.h"
+
+using namespace std;
+
+
+#define ERROR(msg) fail(msg, __FILE__, __LINE__)
+
+static void fail(const string msg, const char* file, int lineNum)
+{
+  cout << "Error in " << file << "(" << lineNum << "): " << msg << endl;
+  exit(1);
+}
+
+
+static void testSupport(void)
+{
+  bdd even = bdd_ithvar(0) | bdd_ithvar(2) | bdd_ithvar(4);
+  bdd odd  = bdd_ithvar(1) | bdd_ithvar(3) | bdd_ithvar(5);
+
+  cout << "Testing support\n";
+  
+  bdd s1 = bdd_support(even);
+  bdd s2 = bdd_support(odd);
+
+  if (s1 != (bdd_ithvar(0) & bdd_ithvar(2) & bdd_ithvar(4)))
+    ERROR("Support of 'even' failed\n");
+  if (s2 != (bdd_ithvar(1) & bdd_ithvar(3) & bdd_ithvar(5)))
+    ERROR("Support of 'odd' failed\n");
+
+  /* Try many time in order check that the internal support ID
+   * is set correctly */
+  for (int n=0 ; n<500 ; ++n)
+  {
+    s1 = bdd_support(even);
+    s2 = bdd_support(odd);
+
+    if (s1 != (bdd_ithvar(0) & bdd_ithvar(2) & bdd_ithvar(4)))
+      ERROR("Support of 'even' failed");
+    if (s2 != (bdd_ithvar(1) & bdd_ithvar(3) & bdd_ithvar(5)))
+      ERROR("Support of 'odd' failed");
+  }
+}
+
+
+void testBvecIte()
+{
+  cout << "Testing ITE for vector\n";
+  
+  bdd  a = bdd_ithvar(0);
+  bvec b = bvec_var(3, 1, 2);
+  bvec c = bvec_var(3, 2, 2);
+
+  bvec res = bvec_ite(a,b,c);
+
+  bdd r0 = bdd_ite( bdd_ithvar(0), bdd_ithvar(1), bdd_ithvar(2) );
+  bdd r1 = bdd_ite( bdd_ithvar(0), bdd_ithvar(3), bdd_ithvar(4) );
+  bdd r2 = bdd_ite( bdd_ithvar(0), bdd_ithvar(5), bdd_ithvar(6) );
+
+  if (res[0] != r0)
+    ERROR("Bit 0 failed.");
+  if (res[1] != r1)
+    ERROR("Bit 1 failed.");
+  if (res[2] != r2)
+    ERROR("Bit 2 failed.");
+}
+
+
+int main(int ac, char** av)
+{
+  bdd_init(1000,1000);
+
+  bdd_setvarnum(10);
+
+  testSupport();
+  testBvecIte();
+
+  bdd_done();
+  return 0;
+}

Causality/src/bddtree.h

+/*========================================================================
+               Copyright (C) 1996-2002 by Jorn Lind-Nielsen
+                            All rights reserved
+
+    Permission is hereby granted, without written agreement and without
+    license or royalty fees, to use, reproduce, prepare derivative
+    works, distribute, and display this software and its documentation
+    for any purpose, provided that (1) the above copyright notice and
+    the following two paragraphs appear in all copies of the source code
+    and (2) redistributions, including without limitation binaries,
+    reproduce these notices in the supporting documentation. Substantial
+    modifications to this software may be copyrighted by their authors
+    and need not follow the licensing terms described here, provided
+    that the new terms are clearly indicated in all files where they apply.
+
+    IN NO EVENT SHALL JORN LIND-NIELSEN, OR DISTRIBUTORS OF THIS
+    SOFTWARE BE LIABLE TO ANY PARTY FOR DIRECT, INDIRECT, SPECIAL,
+    INCIDENTAL, OR CONSEQUENTIAL DAMAGES ARISING OUT OF THE USE OF THIS
+    SOFTWARE AND ITS DOCUMENTATION, EVEN IF THE AUTHORS OR ANY OF THE
+    ABOVE PARTIES HAVE BEEN ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
+
+    JORN LIND-NIELSEN SPECIFICALLY DISCLAIM ANY WARRANTIES, INCLUDING,
+    BUT NOT LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND
+    FITNESS FOR A PARTICULAR PURPOSE. THE SOFTWARE PROVIDED HEREUNDER IS
+    ON AN "AS IS" BASIS, AND THE AUTHORS AND DISTRIBUTORS HAVE NO
+    OBLIGATION TO PROVIDE MAINTENANCE, SUPPORT, UPDATES, ENHANCEMENTS, OR
+    MODIFICATIONS.
+========================================================================*/
+
+/*************************************************************************
+  $Header: /home/jln/phd/bdd/src/RCS/bddtree.h,v 1.1 2000/05/17 20:00:05 jln Exp jln $
+  FILE:  tree.h
+  DESCR: Trees for BDD variables
+  AUTH:  Jorn Lind
+  DATE:  (C) march 1998
+*************************************************************************/
+
+#ifndef _TREE_H
+#define _TREE_H
+
+typedef struct s_BddTree
+{
+   int first, last;  /* First and last variable in this block */
+   int pos;          /* Sifting position */
+   int *seq;         /* Sequence of first...last in the current order */
+   char fixed;       /* Are the sub-blocks fixed or may they be reordered */
+   int id;           /* A sequential id number given by addblock */
+   struct s_BddTree *next, *prev;
+   struct s_BddTree *nextlevel;
+} BddTree;
+
+BddTree *bddtree_new(int);
+void     bddtree_del(BddTree *);
+BddTree *bddtree_addrange(BddTree *, int, int, int, int);
+void     bddtree_print(FILE *, BddTree *, int);
+
+#endif /* _TREE_H */
+
+
+/* EOF */

Causality/src/bvec.h

+/*========================================================================
+               Copyright (C) 1996-2002 by Jorn Lind-Nielsen
+                            All rights reserved
+
+    Permission is hereby granted, without written agreement and without
+    license or royalty fees, to use, reproduce, prepare derivative
+    works, distribute, and display this software and its documentation
+    for any purpose, provided that (1) the above copyright notice and
+    the following two paragraphs appear in all copies of the source code
+    and (2) redistributions, including without limitation binaries,
+    reproduce these notices in the supporting documentation. Substantial
+    modifications to this software may be copyrighted by their authors
+    and need not follow the licensing terms described here, provided
+    that the new terms are clearly indicated in all files where they apply.
+
+    IN NO EVENT SHALL JORN LIND-NIELSEN, OR DISTRIBUTORS OF THIS
+    SOFTWARE BE LIABLE TO ANY PARTY FOR DIRECT, INDIRECT, SPECIAL,
+    INCIDENTAL, OR CONSEQUENTIAL DAMAGES ARISING OUT OF THE USE OF THIS
+    SOFTWARE AND ITS DOCUMENTATION, EVEN IF THE AUTHORS OR ANY OF THE
+    ABOVE PARTIES HAVE BEEN ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
+
+    JORN LIND-NIELSEN SPECIFICALLY DISCLAIM ANY WARRANTIES, INCLUDING,
+    BUT NOT LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND
+    FITNESS FOR A PARTICULAR PURPOSE. THE SOFTWARE PROVIDED HEREUNDER IS
+    ON AN "AS IS" BASIS, AND THE AUTHORS AND DISTRIBUTORS HAVE NO
+    OBLIGATION TO PROVIDE MAINTENANCE, SUPPORT, UPDATES, ENHANCEMENTS, OR
+    MODIFICATIONS.
+========================================================================*/
+
+/*************************************************************************
+  $Header: /home/jln/phd/bdd/src/RCS/bvec.h,v 1.3 2000/05/17 20:00:05 jln Exp jln $
+  FILE:  bvec.h
+  DESCR: Boolean (BDD) vector handling
+  AUTH:  Jorn Lind
+  DATE:  (C) may 1999
+*************************************************************************/
+
+#ifndef _BVEC_H
+#define _BVEC_H
+
+#include "fdd.h"
+
+   /* Boolean (BDD) vector */
+/*
+NAME    {* bvec *}
+SECTION {* bvec *}
+SHORT   {* A boolean vector *}
+PROTO   {* typedef struct s_bvec
+{
+   int bitnum;
+   BDD *bitvec;
+} BVEC;
+
+typedef BVEC bvec; *}
+DESCR   {* This data structure is used to store boolean vectors. The field
+           {\tt bitnum} is the number of elements in the vector and the
+	   field {\tt bitvec} contains the actual BDDs in the vector.
+	   The C++ version of {\tt bvec} is documented at the beginning of
+	   this document *}
+*/
+typedef struct s_bvec
+{
+   int bitnum;
+   BDD *bitvec;
+} BVEC;
+
+#ifndef CPLUSPLUS
+typedef BVEC bvec;
+#endif
+
+
+#ifdef CPLUSPLUS
+extern "C" {
+#endif
+   
+   /* Prototypes for bvec.c */
+extern BVEC bvec_copy(BVEC v);
+extern BVEC bvec_true(int bitnum);
+extern BVEC bvec_false(int bitnum);
+extern BVEC bvec_con(int bitnum, int val);
+extern BVEC bvec_var(int bitnum, int offset, int step);
+extern BVEC bvec_varfdd(int var);
+extern BVEC bvec_varvec(int bitnum, int *var);
+extern BVEC bvec_coerce(int bitnum, BVEC v);
+extern int  bvec_isconst(BVEC e);   
+extern int  bvec_val(BVEC e);   
+extern void bvec_free(BVEC v);
+extern BVEC bvec_addref(BVEC v);
+extern BVEC bvec_delref(BVEC v);
+extern BVEC bvec_map1(BVEC a, BDD (*fun)(BDD));
+extern BVEC bvec_map2(BVEC a, BVEC b, BDD (*fun)(BDD,BDD));
+extern BVEC bvec_map3(BVEC a, BVEC b, BVEC c, BDD (*fun)(BDD,BDD,BDD));
+extern BVEC bvec_add(BVEC left, BVEC right);
+extern BVEC bvec_sub(BVEC left, BVEC right);
+extern BVEC bvec_mulfixed(BVEC e, int c);
+extern BVEC bvec_mul(BVEC left, BVEC right);
+extern int  bvec_divfixed(BVEC e, int c, BVEC *res, BVEC *rem);
+extern int  bvec_div(BVEC left, BVEC right, BVEC *res, BVEC *rem);
+extern BVEC bvec_ite(BDD a, BVEC b, BVEC c);
+extern BVEC bvec_shlfixed(BVEC e, int pos, BDD c);
+extern BVEC bvec_shl(BVEC l, BVEC r, BDD c);
+extern BVEC bvec_shrfixed(BVEC e, int pos, BDD c);
+extern BVEC bvec_shr(BVEC l, BVEC r, BDD c);
+extern BDD  bvec_lth(BVEC left, BVEC right);
+extern BDD  bvec_lte(BVEC left, BVEC right);
+extern BDD  bvec_gth(BVEC left, BVEC right);
+extern BDD  bvec_gte(BVEC left, BVEC right);
+extern BDD  bvec_equ(BVEC left, BVEC right);
+extern BDD  bvec_neq(BVEC left, BVEC right);
+
+#ifdef CPLUSPLUS
+}
+#endif
+
+
+/*************************************************************************
+   If this file is included from a C++ compiler then the following
+   classes, wrappers and hacks are supplied.
+*************************************************************************/
+#ifdef CPLUSPLUS
+
+/*=== User BVEC class ==================================================*/
+
+class bvec
+{
+ public:
+
+   bvec(void)                { roots.bitvec=NULL; roots.bitnum=0; }
+   bvec(int bitnum)          { roots=bvec_false(bitnum); }
+   bvec(int bitnum, int val) { roots=bvec_con(bitnum,val); }
+   bvec(const bvec &v)       { roots=bvec_copy(v.roots); }
+   ~bvec(void)               { bvec_free(roots); }
+
+   void set(int i, const bdd &b);
+   bdd operator[](int i)  const { return roots.bitvec[i]; }
+   int bitnum(void) const       { return roots.bitnum; }
+   int empty(void) const        { return roots.bitnum==0; }
+   bvec operator=(const bvec &src);
+   
+private:
+   BVEC roots;
+
+   bvec(const BVEC &v) { roots=v; } /* NOTE: Must be a shallow copy! */
+
+   friend bvec bvec_truepp(int bitnum);
+   friend bvec bvec_falsepp(int bitnum);
+   friend bvec bvec_conpp(int bitnum, int val);
+   friend bvec bvec_varpp(int bitnum, int offset, int step);
+   friend bvec bvec_varfddpp(int var);
+   friend bvec bvec_varvecpp(int bitnum, int *var);
+   friend bvec bvec_coerce(int bitnum, const bvec &v);
+   friend int  bvec_isconst(const bvec &e);   
+   friend int  bvec_val(const bvec &e);   
+   friend bvec bvec_copy(const bvec &v);
+   friend bvec bvec_map1(const bvec &a,
+			 bdd (*fun)(const bdd &));
+   friend bvec bvec_map2(const bvec &a, const bvec &b,
+			 bdd (*fun)(const bdd &, const bdd &));
+   friend bvec bvec_map3(const bvec &a, const bvec &b, const bvec &c,
+			 bdd (*fun)(const bdd &, const bdd &, const bdd &));
+   friend bvec bvec_add(const bvec &left, const bvec &right);
+   friend bvec bvec_sub(const bvec &left, const bvec &right);
+   friend bvec bvec_mulfixed(const bvec &e, int c);
+   friend bvec bvec_mul(const bvec &left, const bvec &right);
+   friend int  bvec_divfixed(const bvec &e, int c, bvec &res, bvec &rem);
+   friend int  bvec_div(const bvec &l, const bvec &r, bvec &res, bvec &rem);
+   friend bvec bvec_ite(const bdd& a, const bvec& b, const bvec& c);
+   friend bvec bvec_shlfixed(const bvec &e, int pos, const bdd &c);
+   friend bvec bvec_shl(const bvec &left, const bvec &right, const bdd &c);
+   friend bvec bvec_shrfixed(const bvec &e, int pos, const bdd &c);
+   friend bvec bvec_shr(const bvec &left, const bvec &right, const bdd &c);
+   friend bdd  bvec_lth(const bvec &left, const bvec &right);
+   friend bdd  bvec_lte(const bvec &left, const bvec &right);
+   friend bdd  bvec_gth(const bvec &left, const bvec &right);
+   friend bdd  bvec_gte(const bvec &left, const bvec &right);
+   friend bdd  bvec_equ(const bvec &left, const bvec &right);
+   friend bdd  bvec_neq(const bvec &left, const bvec &right);
+
+public:
+   bvec operator&(const bvec &a) const { return bvec_map2(*this, a, bdd_and); }
+   bvec operator^(const bvec &a) const { return bvec_map2(*this, a, bdd_xor); }
+   bvec operator|(const bvec &a) const { return bvec_map2(*this, a, bdd_or); }
+   bvec operator!(void) const          { return bvec_map1(*this, bdd_not); }
+   bvec operator<<(int a)   const   { return bvec_shlfixed(*this,a,bddfalse); }
+   bvec operator<<(const bvec &a) const  { return bvec_shl(*this,a,bddfalse); }
+   bvec operator>>(int a)   const   { return bvec_shrfixed(*this,a,bddfalse); }
+   bvec operator>>(const bvec &a) const  { return bvec_shr(*this,a,bddfalse); }
+   bvec operator+(const bvec &a) const { return bvec_add(*this, a); }
+   bvec operator-(const bvec &a) const { return bvec_sub(*this, a); }
+   bvec operator*(int a) const         { return bvec_mulfixed(*this, a); }
+   bvec operator*(const bvec a) const  { return bvec_mul(*this, a); }
+   bdd operator<(const bvec &a) const  { return bvec_lth(*this, a); }
+   bdd operator<=(const bvec &a) const { return bvec_lte(*this, a); }
+   bdd operator>(const bvec &a) const  { return bvec_gth(*this, a); }
+   bdd operator>=(const bvec &a) const { return bvec_gte(*this, a); }
+   bdd operator==(const bvec &a) const { return bvec_equ(*this, a); }
+   bdd operator!=(const bvec &a) const { return bvec_neq(*this, a); }
+};
+
+std::ostream &operator<<(std::ostream &, const bvec &);
+
+inline bvec bvec_truepp(int bitnum)
+{ return bvec_true(bitnum); }
+
+inline bvec bvec_falsepp(int bitnum)
+{ return bvec_false(bitnum); }
+
+inline bvec bvec_conpp(int bitnum, int val)
+{ return bvec_con(bitnum, val); }
+
+inline bvec bvec_varpp(int bitnum, int offset, int step)
+{ return bvec_var(bitnum, offset, step); }
+
+inline bvec bvec_varfddpp(int var)
+{ return bvec_varfdd(var); }
+
+inline bvec bvec_varvecpp(int bitnum, int *var)
+{ return bvec_varvec(bitnum, var); }
+
+inline bvec bvec_coerce(int bitnum, const bvec &v)
+{ return bvec_coerce(bitnum, v.roots); }
+
+inline int  bvec_isconst(const bvec &e)
+{ return bvec_isconst(e.roots); }
+
+inline int  bvec_val(const bvec &e)
+{ return bvec_val(e.roots); }
+
+inline bvec bvec_copy(const bvec &v)
+{ return bvec_copy(v.roots); }
+
+inline bvec bvec_add(const bvec &left, const bvec &right)
+{ return bvec_add(left.roots, right.roots); }
+
+inline bvec bvec_sub(const bvec &left, const bvec &right)
+{ return bvec_sub(left.roots, right.roots); }
+
+inline bvec bvec_mulfixed(const bvec &e, int c)
+{ return bvec_mulfixed(e.roots, c); }
+
+inline bvec bvec_mul(const bvec &left, const bvec &right)
+{ return bvec_mul(left.roots, right.roots); }
+
+inline int bvec_divfixed(const bvec &e, int c, bvec &res, bvec &rem)
+{ return bvec_divfixed(e.roots, c, &res.roots, &rem.roots); }
+
+inline int bvec_div(const bvec &l, const bvec &r, bvec &res, bvec &rem)
+{ return bvec_div(l.roots, r.roots, &res.roots, &rem.roots); }
+
+inline bvec bvec_ite(const bdd& a, const bvec& b, const bvec& c)
+{ return bvec_ite(a.root, b.roots, c.roots); }
+
+inline bvec bvec_shlfixed(const bvec &e, int pos, const bdd &c)
+{ return bvec_shlfixed(e.roots, pos, c.root); }
+
+inline bvec bvec_shl(const bvec &left, const bvec &right, const bdd &c)
+{ return bvec_shl(left.roots, right.roots, c.root); }
+
+inline bvec bvec_shrfixed(const bvec &e, int pos, const bdd &c)
+{ return bvec_shrfixed(e.roots, pos, c.root); }
+
+inline bvec bvec_shr(const bvec &left, const bvec &right, const bdd &c)
+{ return bvec_shr(left.roots, right.roots, c.root); }
+
+inline bdd  bvec_lth(const bvec &left, const bvec &right)
+{ return bvec_lth(left.roots, right.roots); }
+
+inline bdd  bvec_lte(const bvec &left, const bvec &right)
+{ return bvec_lte(left.roots, right.roots); }
+
+inline bdd  bvec_gth(const bvec &left, const bvec &right)
+{ return bvec_gth(left.roots, right.roots); }
+
+inline bdd  bvec_gte(const bvec &left, const bvec &right)
+{ return bvec_gte(left.roots, right.roots); }
+
+inline bdd  bvec_equ(const bvec &left, const bvec &right)
+{ return bvec_equ(left.roots, right.roots); }
+
+inline bdd  bvec_neq(const bvec &left, const bvec &right)
+{ return bvec_neq(left.roots, right.roots); }
+
+
+   /* Hack to allow for overloading */
+#define bvec_var(a,b,c)  bvec_varpp(a,b,c)
+#define bvec_varfdd(a)   bvec_varfddpp(a)
+#define bvec_varvec(a,b) bvec_varvecpp(a,b)
+#define bvec_true(a)     bvec_truepp(a)
+#define bvec_false(a)    bvec_falsepp(a)
+#define bvec_con(a,b)    bvec_conpp((a),(b))
+
+   
+#endif /* CPLUSPLUS */
+
+#endif /* _BVEC_H */
+
+/* EOF */

Causality/src/cache.h

+/*========================================================================
+               Copyright (C) 1996-2002 by Jorn Lind-Nielsen
+                            All rights reserved
+
+    Permission is hereby granted, without written agreement and without
+    license or royalty fees, to use, reproduce, prepare derivative
+    works, distribute, and display this software and its documentation
+    for any purpose, provided that (1) the above copyright notice and
+    the following two paragraphs appear in all copies of the source code
+    and (2) redistributions, including without limitation binaries,
+    reproduce these notices in the supporting documentation. Substantial
+    modifications to this software may be copyrighted by their authors
+    and need not follow the licensing terms described here, provided
+    that the new terms are clearly indicated in all files where they apply.
+
+    IN NO EVENT SHALL JORN LIND-NIELSEN, OR DISTRIBUTORS OF THIS
+    SOFTWARE BE LIABLE TO ANY PARTY FOR DIRECT, INDIRECT, SPECIAL,
+    INCIDENTAL, OR CONSEQUENTIAL DAMAGES ARISING OUT OF THE USE OF THIS
+    SOFTWARE AND ITS DOCUMENTATION, EVEN IF THE AUTHORS OR ANY OF THE
+    ABOVE PARTIES HAVE BEEN ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
+
+    JORN LIND-NIELSEN SPECIFICALLY DISCLAIM ANY WARRANTIES, INCLUDING,
+    BUT NOT LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND
+    FITNESS FOR A PARTICULAR PURPOSE. THE SOFTWARE PROVIDED HEREUNDER IS
+    ON AN "AS IS" BASIS, AND THE AUTHORS AND DISTRIBUTORS HAVE NO
+    OBLIGATION TO PROVIDE MAINTENANCE, SUPPORT, UPDATES, ENHANCEMENTS, OR
+    MODIFICATIONS.
+========================================================================*/
+
+/*************************************************************************
+  $Header: /home/jln/phd/bdd/src/RCS/cache.h,v 1.8 2000/05/17 20:00:05 jln Exp jln $
+  FILE:  cache.h
+  DESCR: Cache class for caching apply/exist etc. results
+  AUTH:  Jorn Lind
+  DATE:  (C) june 1997
+*************************************************************************/
+
+#ifndef _CACHE_H
+#define _CACHE_H
+
+typedef struct
+{
+   union
+   {
+      double dres;
+      int res;
+   } r;
+   int a,b,c;
+} BddCacheData;
+
+
+typedef struct
+{
+   BddCacheData *table;
+   int tablesize;
+} BddCache;
+
+
+extern int  BddCache_init(BddCache *, int);
+extern void BddCache_done(BddCache *);
+extern int  BddCache_resize(BddCache *, int);
+extern void BddCache_reset(BddCache *);
+
+#define BddCache_lookup(cache, hash) (&(cache)->table[hash % (cache)->tablesize])
+
+
+#endif /* _CACHE_H */
+
+
+/* EOF */