288 lines
16 KiB
C
288 lines
16 KiB
C
|
/******************************************************************************\
|
||
|
|
* *
|
||
|
|
* SimpleCUDD library (www.cs.kuleuven.be/~theo/tools/simplecudd.html) *
|
||
|
|
* SimpleCUDD was developed at Katholieke Universiteit Leuven(www.kuleuven.be) *
|
||
|
|
* *
|
||
|
|
* Copyright T. Mantadelis and Katholieke Universiteit Leuven 2008 *
|
||
|
|
* *
|
||
|
|
* Author: Theofrastos Mantadelis *
|
||
|
|
* File: simplecudd.h *
|
||
|
|
* *
|
||
|
|
********************************************************************************
|
||
|
|
* *
|
||
|
|
* The "Artistic License" *
|
||
|
|
* *
|
||
|
|
* Preamble *
|
||
|
|
* *
|
||
|
|
* The intent of this document is to state the conditions under which a *
|
||
|
|
* Package may be copied, such that the Copyright Holder maintains some *
|
||
|
|
* semblance of artistic control over the development of the package, *
|
||
|
|
* while giving the users of the package the right to use and distribute *
|
||
|
|
* the Package in a more-or-less customary fashion, plus the right to make *
|
||
|
|
* reasonable modifications. *
|
||
|
|
* *
|
||
|
|
* Definitions: *
|
||
|
|
* *
|
||
|
|
* "Package" refers to the collection of files distributed by the *
|
||
|
|
* Copyright Holder, and derivatives of that collection of files *
|
||
|
|
* created through textual modification. *
|
||
|
|
* *
|
||
|
|
* "Standard Version" refers to such a Package if it has not been *
|
||
|
|
* modified, or has been modified in accordance with the wishes *
|
||
|
|
* of the Copyright Holder as specified below. *
|
||
|
|
* *
|
||
|
|
* "Copyright Holder" is whoever is named in the copyright or *
|
||
|
|
* copyrights for the package. *
|
||
|
|
* *
|
||
|
|
* "You" is you, if you're thinking about copying or distributing *
|
||
|
|
* this Package. *
|
||
|
|
* *
|
||
|
|
* "Reasonable copying fee" is whatever you can justify on the *
|
||
|
|
* basis of media cost, duplication charges, time of people involved, *
|
||
|
|
* and so on. (You will not be required to justify it to the *
|
||
|
|
* Copyright Holder, but only to the computing community at large *
|
||
|
|
* as a market that must bear the fee.) *
|
||
|
|
* *
|
||
|
|
* "Freely Available" means that no fee is charged for the item *
|
||
|
|
* itself, though there may be fees involved in handling the item. *
|
||
|
|
* It also means that recipients of the item may redistribute it *
|
||
|
|
* under the same conditions they received it. *
|
||
|
|
* *
|
||
|
|
* 1. You may make and give away verbatim copies of the source form of the *
|
||
|
|
* Standard Version of this Package without restriction, provided that you *
|
||
|
|
* duplicate all of the original copyright notices and associated disclaimers. *
|
||
|
|
* *
|
||
|
|
* 2. You may apply bug fixes, portability fixes and other modifications *
|
||
|
|
* derived from the Public Domain or from the Copyright Holder. A Package *
|
||
|
|
* modified in such a way shall still be considered the Standard Version. *
|
||
|
|
* *
|
||
|
|
* 3. You may otherwise modify your copy of this Package in any way, provided *
|
||
|
|
* that you insert a prominent notice in each changed file stating how and *
|
||
|
|
* when you changed that file, and provided that you do at least ONE of the *
|
||
|
|
* following: *
|
||
|
|
* *
|
||
|
|
* a) place your modifications in the Public Domain or otherwise make them *
|
||
|
|
* Freely Available, such as by posting said modifications to Usenet or *
|
||
|
|
* an equivalent medium, or placing the modifications on a major archive *
|
||
|
|
* site such as uunet.uu.net, or by allowing the Copyright Holder to include *
|
||
|
|
* your modifications in the Standard Version of the Package. *
|
||
|
|
* *
|
||
|
|
* b) use the modified Package only within your corporation or organization. *
|
||
|
|
* *
|
||
|
|
* c) rename any non-standard executables so the names do not conflict *
|
||
|
|
* with standard executables, which must also be provided, and provide *
|
||
|
|
* a separate manual page for each non-standard executable that clearly *
|
||
|
|
* documents how it differs from the Standard Version. *
|
||
|
|
* *
|
||
|
|
* d) make other distribution arrangements with the Copyright Holder. *
|
||
|
|
* *
|
||
|
|
* 4. You may distribute the programs of this Package in object code or *
|
||
|
|
* executable form, provided that you do at least ONE of the following: *
|
||
|
|
* *
|
||
|
|
* a) distribute a Standard Version of the executables and library files, *
|
||
|
|
* together with instructions (in the manual page or equivalent) on where *
|
||
|
|
* to get the Standard Version. *
|
||
|
|
* *
|
||
|
|
* b) accompany the distribution with the machine-readable source of *
|
||
|
|
* the Package with your modifications. *
|
||
|
|
* *
|
||
|
|
* c) give non-standard executables non-standard names, and clearly *
|
||
|
|
* document the differences in manual pages (or equivalent), together *
|
||
|
|
* with instructions on where to get the Standard Version. *
|
||
|
|
* *
|
||
|
|
* d) make other distribution arrangements with the Copyright Holder. *
|
||
|
|
* *
|
||
|
|
* 5. You may charge a reasonable copying fee for any distribution of this *
|
||
|
|
* Package. You may charge any fee you choose for support of this *
|
||
|
|
* Package. You may not charge a fee for this Package itself. However, *
|
||
|
|
* you may distribute this Package in aggregate with other (possibly *
|
||
|
|
* commercial) programs as part of a larger (possibly commercial) software *
|
||
|
|
* distribution provided that you do not advertise this Package as a *
|
||
|
|
* product of your own. You may embed this Package's interpreter within *
|
||
|
|
* an executable of yours (by linking); this shall be construed as a mere *
|
||
|
|
* form of aggregation, provided that the complete Standard Version of the *
|
||
|
|
* interpreter is so embedded. *
|
||
|
|
* *
|
||
|
|
* 6. The scripts and library files supplied as input to or produced as *
|
||
|
|
* output from the programs of this Package do not automatically fall *
|
||
|
|
* under the copyright of this Package, but belong to whoever generated *
|
||
|
|
* them, and may be sold commercially, and may be aggregated with this *
|
||
|
|
* Package. If such scripts or library files are aggregated with this *
|
||
|
|
* Package via the so-called "undump" or "unexec" methods of producing a *
|
||
|
|
* binary executable image, then distribution of such an image shall *
|
||
|
|
* neither be construed as a distribution of this Package nor shall it *
|
||
|
|
* fall under the restrictions of Paragraphs 3 and 4, provided that you do *
|
||
|
|
* not represent such an executable image as a Standard Version of this *
|
||
|
|
* Package. *
|
||
|
|
* *
|
||
|
|
* 7. C subroutines (or comparably compiled subroutines in other *
|
||
|
|
* languages) supplied by you and linked into this Package in order to *
|
||
|
|
* emulate subroutines and variables of the language defined by this *
|
||
|
|
* Package shall not be considered part of this Package, but are the *
|
||
|
|
* equivalent of input as in Paragraph 6, provided these subroutines do *
|
||
|
|
* not change the language in any way that would cause it to fail the *
|
||
|
|
* regression tests for the language. *
|
||
|
|
* *
|
||
|
|
* 8. Aggregation of this Package with a commercial distribution is always *
|
||
|
|
* permitted provided that the use of this Package is embedded; that is, *
|
||
|
|
* when no overt attempt is made to make this Package's interfaces visible *
|
||
|
|
* to the end user of the commercial distribution. Such use shall not be *
|
||
|
|
* construed as a distribution of this Package. *
|
||
|
|
* *
|
||
|
|
* 9. The name of the Copyright Holder may not be used to endorse or promote *
|
||
|
|
* products derived from this software without specific prior written *
|
||
|
|
* permission. *
|
||
|
|
* *
|
||
|
|
* 10. THIS PACKAGE IS PROVIDED "AS IS" AND WITHOUT ANY EXPRESS OR *
|
||
|
|
* IMPLIED WARRANTIES, INCLUDING, WITHOUT LIMITATION, THE IMPLIED *
|
||
|
|
* WARRANTIES OF MERCHANTIBILITY AND FITNESS FOR A PARTICULAR PURPOSE. *
|
||
|
|
* *
|
||
|
|
* The End *
|
||
|
|
* *
|
||
|
|
\******************************************************************************/
|
||
|
|
|
||
|
|
|
||
|
|
#include <stdio.h>
|
||
|
|
#include <stdlib.h>
|
||
|
|
#include <string.h>
|
||
|
|
#include <math.h>
|
||
|
|
#include <time.h>
|
||
|
|
#include "util.h"
|
||
|
|
#include "cudd.h"
|
||
|
|
#include "cuddInt.h"
|
||
|
|
#include "general.h"
|
||
|
|
|
||
|
|
#define IsHigh(manager, node) HIGH(manager) == node
|
||
|
|
#define IsLow(manager, node) LOW(manager) == node
|
||
|
|
#define HIGH(manager) Cudd_ReadOne(manager)
|
||
|
|
#define LOW(manager) Cudd_Not(Cudd_ReadOne(manager))
|
||
|
|
#define NOT(node) Cudd_Not(node)
|
||
|
|
#define GetIndex(node) Cudd_NodeReadIndex(node)
|
||
|
|
#define GetVar(manager, index) Cudd_bddIthVar(manager, index)
|
||
|
|
#define NewVar(manager) Cudd_bddNewVar(manager)
|
||
|
|
#define KillBDD(manager) Cudd_Quit(manager)
|
||
|
|
#define GetVarCount(manager) Cudd_ReadSize(manager)
|
||
|
|
#define DEBUGON _debug = 1
|
||
|
|
#define DEBUGOFF _debug = 0
|
||
|
|
#define RAPIDLOADON _RapidLoad = 1
|
||
|
|
#define RAPIDLOADOFF _RapidLoad = 0
|
||
|
|
#define SETMAXBUFSIZE(size) _maxbufsize = size
|
||
|
|
#define BDDFILE_ERROR -1
|
||
|
|
#define BDDFILE_OTHER 0
|
||
|
|
#define BDDFILE_SCRIPT 1
|
||
|
|
#define BDDFILE_NODEDUMP 2
|
||
|
|
|
||
|
|
extern int _RapidLoad;
|
||
|
|
extern int _debug;
|
||
|
|
extern int _maxbufsize;
|
||
|
|
|
||
|
|
typedef struct _bddfileheader {
|
||
|
|
FILE *inputfile;
|
||
|
|
int version;
|
||
|
|
int varcnt;
|
||
|
|
int varstart;
|
||
|
|
int intercnt;
|
||
|
|
int filetype;
|
||
|
|
} bddfileheader;
|
||
|
|
|
||
|
|
typedef struct _namedvars {
|
||
|
|
int varcnt;
|
||
|
|
int varstart;
|
||
|
|
char **vars;
|
||
|
|
int *loaded;
|
||
|
|
double *dvalue;
|
||
|
|
int *ivalue;
|
||
|
|
void **dynvalue;
|
||
|
|
} namedvars;
|
||
|
|
|
||
|
|
typedef struct _hisnode {
|
||
|
|
DdNode *key;
|
||
|
|
double dvalue;
|
||
|
|
int ivalue;
|
||
|
|
void *dynvalue;
|
||
|
|
} hisnode;
|
||
|
|
|
||
|
|
typedef struct _hisqueue {
|
||
|
|
int cnt;
|
||
|
|
hisnode *thenode;
|
||
|
|
} hisqueue;
|
||
|
|
|
||
|
|
typedef struct _nodeline {
|
||
|
|
char *varname;
|
||
|
|
char *truevar;
|
||
|
|
char *falsevar;
|
||
|
|
int nodenum;
|
||
|
|
int truenode;
|
||
|
|
int falsenode;
|
||
|
|
} nodeline;
|
||
|
|
|
||
|
|
/* Initialization */
|
||
|
|
|
||
|
|
DdManager* simpleBDDinit(int varcnt);
|
||
|
|
|
||
|
|
/* BDD Generation */
|
||
|
|
|
||
|
|
DdNode* D_BDDAnd(DdManager *manager, DdNode *bdd1, DdNode *bdd2);
|
||
|
|
DdNode* D_BDDNand(DdManager *manager, DdNode *bdd1, DdNode *bdd2);
|
||
|
|
DdNode* D_BDDOr(DdManager *manager, DdNode *bdd1, DdNode *bdd2);
|
||
|
|
DdNode* D_BDDNor(DdManager *manager, DdNode *bdd1, DdNode *bdd2);
|
||
|
|
DdNode* D_BDDXor(DdManager *manager, DdNode *bdd1, DdNode *bdd2);
|
||
|
|
DdNode* D_BDDXnor(DdManager *manager, DdNode *bdd1, DdNode *bdd2);
|
||
|
|
|
||
|
|
DdNode* FileGenerateBDD(DdManager *manager, namedvars varmap, bddfileheader fileheader);
|
||
|
|
DdNode* OnlineGenerateBDD(DdManager *manager, namedvars *varmap);
|
||
|
|
DdNode* LineParser(DdManager *manager, namedvars varmap, DdNode **inter, int maxinter, char *function, int iline);
|
||
|
|
DdNode* OnlineLineParser(DdManager *manager, namedvars *varmap, DdNode **inter, int maxinter, char *function, int iline);
|
||
|
|
DdNode* BDD_Operator(DdManager *manager, DdNode *bdd1, DdNode *bdd2, char Operator, int inegoper);
|
||
|
|
int getInterBDD(char *function);
|
||
|
|
char* getFileName(const char *function);
|
||
|
|
int GetParam(char *inputline, int iParam);
|
||
|
|
int LoadVariableData(namedvars varmap, char *filename);
|
||
|
|
|
||
|
|
/* Named variables */
|
||
|
|
|
||
|
|
namedvars InitNamedVars(int varcnt, int varstart);
|
||
|
|
void EnlargeNamedVars(namedvars *varmap, int newvarcnt);
|
||
|
|
int AddNamedVarAt(namedvars varmap, const char *varname, int index);
|
||
|
|
int AddNamedVar(namedvars varmap, const char *varname);
|
||
|
|
void SetNamedVarValuesAt(namedvars varmap, int index, double dvalue, int ivalue, void *dynvalue);
|
||
|
|
int SetNamedVarValues(namedvars varmap, const char *varname, double dvalue, int ivalue, void *dynvalue);
|
||
|
|
int GetNamedVarIndex(const namedvars varmap, const char *varname);
|
||
|
|
int RepairVarcnt(namedvars *varmap);
|
||
|
|
char* GetNodeVarName(DdManager *manager, namedvars varmap, DdNode *node);
|
||
|
|
char* GetNodeVarNameDisp(DdManager *manager, namedvars varmap, DdNode *node);
|
||
|
|
int all_loaded(namedvars varmap, int disp);
|
||
|
|
|
||
|
|
/* Traversal */
|
||
|
|
|
||
|
|
DdNode* HighNodeOf(DdManager *manager, DdNode *node);
|
||
|
|
DdNode* LowNodeOf(DdManager *manager, DdNode *node);
|
||
|
|
|
||
|
|
/* Traversal - History */
|
||
|
|
|
||
|
|
hisqueue* InitHistory(int varcnt);
|
||
|
|
void ReInitHistory(hisqueue *HisQueue, int varcnt);
|
||
|
|
void AddNode(hisqueue *HisQueue, int varstart, DdNode *node, double dvalue, int ivalue, void *dynvalue);
|
||
|
|
hisnode* GetNode(hisqueue *HisQueue, int varstart, DdNode *node);
|
||
|
|
int GetNodeIndex(hisqueue *HisQueue, int varstart, DdNode *node);
|
||
|
|
void onlinetraverse(DdManager *manager, namedvars varmap, hisqueue *HisQueue, DdNode *bdd);
|
||
|
|
|
||
|
|
/* Save-load */
|
||
|
|
|
||
|
|
bddfileheader ReadFileHeader(char *filename);
|
||
|
|
int CheckFileVersion(const char *version);
|
||
|
|
|
||
|
|
DdNode * LoadNodeDump(DdManager *manager, namedvars varmap, FILE *inputfile);
|
||
|
|
DdNode * LoadNodeRec(DdManager *manager, namedvars varmap, hisqueue *Nodes, FILE *inputfile, nodeline current);
|
||
|
|
DdNode * GetIfExists(DdManager *manager, namedvars varmap, hisqueue *Nodes, char *varname, int nodenum);
|
||
|
|
|
||
|
|
int SaveNodeDump(DdManager *manager, namedvars varmap, DdNode *bdd, char *filename);
|
||
|
|
void SaveExpand(DdManager *manager, namedvars varmap, hisqueue *Nodes, DdNode *Current, FILE *outputfile);
|
||
|
|
void ExpandNodes(hisqueue *Nodes, int index, int nodenum);
|
||
|
|
|
||
|
|
/* Export */
|
||
|
|
|
||
|
|
int simpleBDDtoDot(DdManager *manager, DdNode *bdd, char *filename);
|
||
|
|
int simpleNamedBDDtoDot(DdManager *manager, namedvars varmap, DdNode *bdd, char *filename);
|
||
|
|
|