/******************************************************************************\ * * * SimpleCUDD library (www.cs.kuleuven.be/~theo/tools/simplecudd.html) * * SimpleCUDD was developed at Katholieke Universiteit Leuven(www.kuleuven.be) * * * * Copyright Katholieke Universiteit Leuven 2008 * * * * Author: Theofrastos Mantadelis * * File: simplecudd.h * * * ******************************************************************************** * * * Artistic License 2.0 * * * * Copyright (c) 2000-2006, The Perl Foundation. * * * * Everyone is permitted to copy and distribute verbatim copies of this license * * document, but changing it is not allowed. * * * * Preamble * * * * This license establishes the terms under which a given free software Package * * may be copied, modified, distributed, and/or redistributed. The intent is * * that the Copyright Holder maintains some artistic control over the * * development of that Package while still keeping the Package available as * * open source and free software. * * * * You are always permitted to make arrangements wholly outside of this license * * directly with the Copyright Holder of a given Package. If the terms of this * * license do not permit the full use that you propose to make of the Package, * * you should contact the Copyright Holder and seek a different licensing * * arrangement. * * Definitions * * * * "Copyright Holder" means the individual(s) or organization(s) named in the * * copyright notice for the entire Package. * * * * "Contributor" means any party that has contributed code or other material to * * the Package, in accordance with the Copyright Holder's procedures. * * * * "You" and "your" means any person who would like to copy, distribute, or * * modify the Package. * * * * "Package" means the collection of files distributed by the Copyright Holder, * * and derivatives of that collection and/or of those files. A given Package * * may consist of either the Standard Version, or a Modified Version. * * * * "Distribute" means providing a copy of the Package or making it accessible * * to anyone else, or in the case of a company or organization, to others * * outside of your company or organization. * * * * "Distributor Fee" means any fee that you charge for Distributing this * * Package or providing support for this Package to another party. It does not * * mean licensing fees. * * * * "Standard Version" refers to the Package if it has not been modified, or has * * been modified only in ways explicitly requested by the Copyright Holder. * * * * "Modified Version" means the Package, if it has been changed, and such * * changes were not explicitly requested by the Copyright Holder. * * * * "Original License" means this Artistic License as Distributed with the * * Standard Version of the Package, in its current version or as it may be * * modified by The Perl Foundation in the future. * * * * "Source" form means the source code, documentation source, and configuration * * files for the Package. * * * * "Compiled" form means the compiled bytecode, object code, binary, or any * * other form resulting from mechanical transformation or translation of the * * Source form. * * Permission for Use and Modification Without Distribution * * * * (1) You are permitted to use the Standard Version and create and use * * Modified Versions for any purpose without restriction, provided that you do * * not Distribute the Modified Version. * * Permissions for Redistribution of the Standard Version * * * * (2) You may Distribute verbatim copies of the Source form of the Standard * * Version of this Package in any medium without restriction, either gratis or * * for a Distributor Fee, provided that you duplicate all of the original * * copyright notices and associated disclaimers. At your discretion, such * * verbatim copies may or may not include a Compiled form of the Package. * * * * (3) You may apply any bug fixes, portability changes, and other * * modifications made available from the Copyright Holder. The resulting * * Package will still be considered the Standard Version, and as such will be * * subject to the Original License. * * Distribution of Modified Versions of the Package as Source * * * * (4) You may Distribute your Modified Version as Source (either gratis or for * * a Distributor Fee, and with or without a Compiled form of the Modified * * Version) provided that you clearly document how it differs from the Standard * * Version, including, but not limited to, documenting any non-standard * * features, executables, or modules, and provided that you do at least ONE of * * the following: * * * * (a) make the Modified Version available to the Copyright Holder of the * * Standard Version, under the Original License, so that the Copyright Holder * * may include your modifications in the Standard Version. * * (b) ensure that installation of your Modified Version does not prevent the * * user installing or running the Standard Version. In addition, the Modified * * Version must bear a name that is different from the name of the Standard * * Version. * * (c) allow anyone who receives a copy of the Modified Version to make the * * Source form of the Modified Version available to others under * * (i) the Original License or * * (ii) a license that permits the licensee to freely copy, modify and * * redistribute the Modified Version using the same licensing terms that apply * * to the copy that the licensee received, and requires that the Source form of * * the Modified Version, and of any works derived from it, be made freely * * available in that license fees are prohibited but Distributor Fees are * * allowed. * * Distribution of Compiled Forms of the Standard Version or Modified Versions * * without the Source * * * * (5) You may Distribute Compiled forms of the Standard Version without the * * Source, provided that you include complete instructions on how to get the * * Source of the Standard Version. Such instructions must be valid at the time * * of your distribution. If these instructions, at any time while you are * * carrying out such distribution, become invalid, you must provide new * * instructions on demand or cease further distribution. If you provide valid * * instructions or cease distribution within thirty days after you become aware * * that the instructions are invalid, then you do not forfeit any of your * * rights under this license. * * * * (6) You may Distribute a Modified Version in Compiled form without the * * Source, provided that you comply with Section 4 with respect to the Source * * of the Modified Version. * * Aggregating or Linking the Package * * * * (7) You may aggregate the Package (either the Standard Version or Modified * * Version) with other packages and Distribute the resulting aggregation * * provided that you do not charge a licensing fee for the Package. Distributor * * Fees are permitted, and licensing fees for other components in the * * aggregation are permitted. The terms of this license apply to the use and * * Distribution of the Standard or Modified Versions as included in the * * aggregation. * * * * (8) You are permitted to link Modified and Standard Versions with other * * works, to embed the Package in a larger work of your own, or to build * * stand-alone binary or bytecode versions of applications that include the * * Package, and Distribute the result without restriction, provided the result * * does not expose a direct interface to the Package. * * Items That are Not Considered Part of a Modified Version * * * * (9) Works (including, but not limited to, modules and scripts) that merely * * extend or make use of the Package, do not, by themselves, cause the Package * * to be a Modified Version. In addition, such works are not considered parts * * of the Package itself, and are not subject to the terms of this license. * * General Provisions * * * * (10) Any use, modification, and distribution of the Standard or Modified * * Versions is governed by this Artistic License. By using, modifying or * * distributing the Package, you accept this license. Do not use, modify, or * * distribute the Package, if you do not accept this license. * * * * (11) If your Modified Version has been derived from a Modified Version made * * by someone other than you, you are nevertheless required to ensure that your * * Modified Version complies with the requirements of this license. * * * * (12) This license does not grant you the right to use any trademark, service * * mark, tradename, or logo of the Copyright Holder. * * * * (13) This license includes the non-exclusive, worldwide, free-of-charge * * patent license to make, have made, use, offer to sell, sell, import and * * otherwise transfer the Package with respect to any patent claims licensable * * by the Copyright Holder that are necessarily infringed by the Package. If * * you institute patent litigation (including a cross-claim or counterclaim) * * against any party alleging that the Package constitutes direct or * * contributory patent infringement, then this Artistic License to you shall * * terminate on the date that such litigation is filed. * * * * (14) Disclaimer of Warranty: THE PACKAGE IS PROVIDED BY THE COPYRIGHT HOLDER * * AND CONTRIBUTORS "AS IS' AND WITHOUT ANY EXPRESS OR IMPLIED WARRANTIES. THE * * IMPLIED WARRANTIES OF MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE, OR * * NON-INFRINGEMENT ARE DISCLAIMED TO THE EXTENT PERMITTED BY YOUR LOCAL LAW. * * UNLESS REQUIRED BY LAW, NO COPYRIGHT HOLDER OR CONTRIBUTOR WILL BE LIABLE * * FOR ANY DIRECT, INDIRECT, INCIDENTAL, OR CONSEQUENTIAL DAMAGES ARISING IN * * ANY WAY OUT OF THE USE OF THE PACKAGE, EVEN IF ADVISED OF THE POSSIBILITY OF * * SUCH DAMAGE. * * * * The End * * * \******************************************************************************/ #include #include #include #include #include #include "pqueue.h" #include "../../../config.h" #if HAVE_UTIL_H #include #endif #if HAVE_CUDD_UTIL_H #include #endif #if HAVE_CUDD_H #include "cudd.h" #endif #if HAVE_CUDD_CUDD_H #include "cudd/cudd.h" #endif #if HAVE_CUDDINT_H #include "cuddInt.h" #endif #if HAVE_CUDD_CUDDINT_H #include "cudd/cuddInt.h" #endif #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 GetOrder(manager, node) Cudd_ReadPerm(manager, GetIndex(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; /** Custom struct to store a DdNode with assigned values */ /** semantics of values depends on algorithm used */ typedef struct _hisnode { DdNode *key; double dvalue; double dvalue2;// =0; //needed for expected counts 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** FileGenerateBDDForest(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); char** GetVariableOrder(char *filename, int varcnt); int LoadVariableData(namedvars varmap, char *filename); /* Named variables */ int ImposeOrder(DdManager *manager, const namedvars varmap, char **map); int get_var_pos_in_map(char **map, const char *var, int varcnt); 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);