/******************************************************************************\
*                                                                              *
*    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: Example.c                                                             *
*                                                                              *
********************************************************************************
*                                                                              *
* 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 "simplecudd.h"

typedef struct _extmanager {
  DdManager *manager;
  DdNode *t, *f;
  hisqueue *his;
  namedvars varmap;
} extmanager;

void DFS(extmanager MyManager, DdNode *Current);
int compexpand(extmanager MyManager, DdNode *Current, extmanager MyManager2, DdNode *Current2);
int bufstrcat(char *targetstr, int targetmem, const char *srcstr);
void getalltruepaths(extmanager MyManager, DdNode *Current, const char *startpath, const char *prevvar);

int main(int argc, char **arg) {
  extmanager MyManager;
  DdNode *bdd, **forest;
  bddfileheader fileheader;
  int code;
  char yn;
  code = -1;
  if (argc != 2) {
    fprintf(stderr, "\nUsage: %s [filename]\nGenerates and traverses a BDD from file\n", arg[0]);
    fprintf(stderr, "\nUsage: %s -online\nGenerates and traverses a BDD online mode\n", arg[0]);
    return code;
  }
  RAPIDLOADON;
  if (strcmp("-online", arg[1]) == 0) {
    MyManager.manager = simpleBDDinit(0);
    MyManager.t = HIGH(MyManager.manager);
    MyManager.f = LOW(MyManager.manager);
    MyManager.varmap = InitNamedVars(1, 0);
    bdd = OnlineGenerateBDD(MyManager.manager, &MyManager.varmap);
  } else {
    fileheader = ReadFileHeader(arg[1]);
    switch(fileheader.filetype) {
      case BDDFILE_SCRIPT:
        MyManager.manager = simpleBDDinit(fileheader.varcnt);
        MyManager.t = HIGH(MyManager.manager);
        MyManager.f = LOW(MyManager.manager);
        MyManager.varmap = InitNamedVars(fileheader.varcnt, fileheader.varstart);
        if (fileheader.version > 1) {
          forest = FileGenerateBDDForest(MyManager.manager, MyManager.varmap, fileheader);
          bdd = forest[0];
        } else {
          forest = NULL;
          bdd = FileGenerateBDD(MyManager.manager, MyManager.varmap, fileheader);
        }
        break;
      case BDDFILE_NODEDUMP:
        MyManager.manager = simpleBDDinit(fileheader.varcnt);
        MyManager.t = HIGH(MyManager.manager);
        MyManager.f = LOW(MyManager.manager);
        MyManager.varmap = InitNamedVars(fileheader.varcnt, fileheader.varstart);
        bdd = LoadNodeDump(MyManager.manager, MyManager.varmap, fileheader.inputfile);
        break;
      default:
        fprintf(stderr, "Error: not a valid file format to load.\n");
        return code;
        break;
    }
  }
  int nextbdd = 0;
  while (bdd != NULL) {
    printf("Do you want to load parameter values from testdata.txt [y]? "); yn = getchar(); getchar();
    if (yn == 'y') {
      printf("yo\n");
      LoadVariableData(MyManager.varmap, "testdata.txt");
      printf("yo\n");
      char **a;
      a = GetVariableOrder("testdata.txt", MyManager.varmap.varcnt);
      int aa;
      for (aa = 0; aa < MyManager.varmap.varcnt; aa++)
        printf("%s\n", a[aa]);
      ImposeOrder(MyManager.manager, MyManager.varmap, a);
    }


    code = 0;
    MyManager.his = InitHistory(GetVarCount(MyManager.manager));
    if (strcmp("-online", arg[1]) != 0) {
      DFS(MyManager, bdd);
      printf("Do you need an export [y]? "); yn = getchar(); getchar();
      if (yn == 'y') simpleNamedBDDtoDot(MyManager.manager, MyManager.varmap, bdd, "SimpleCUDDExport.dot");
      printf("Do you want a save [y]? "); yn = getchar(); getchar();
      if (yn == 'y') SaveNodeDump(MyManager.manager, MyManager.varmap, bdd, "SimpleCUDDSave.sav");
      printf("Do you want to see all true paths [y]? "); yn = getchar(); getchar();
      if (yn == 'y') {
        ReInitHistory(MyManager.his, GetVarCount(MyManager.manager));
        getalltruepaths(MyManager, bdd, "", "");
      }
    } else {
      onlinetraverse(MyManager.manager, MyManager.varmap, MyManager.his, bdd);
    }
    nextbdd++;
    if (forest != NULL) bdd = forest[nextbdd]; else bdd = NULL;
  }
  if (MyManager.manager != NULL) KillBDD(MyManager.manager);
  return code;
}

void DFS(extmanager MyManager, DdNode *Current) {
  DdNode *h, *l;
  hisnode *Found;
  char *curnode;
  curnode = GetNodeVarNameDisp(MyManager.manager, MyManager.varmap, Current);
  if (GetIndex(Current) < MyManager.varmap.varcnt) {
    printf("%s(%f,%i,%s)\n", curnode, MyManager.varmap.dvalue[GetIndex(Current)], MyManager.varmap.ivalue[GetIndex(Current)], (char *) MyManager.varmap.dynvalue[GetIndex(Current)]);
  } else {
    printf("%s\n", curnode);
  }
  if ((Current != MyManager.t) && (Current != MyManager.f) &&
      ((Found = GetNode(MyManager.his, MyManager.varmap.varstart, Current)) == NULL)) {
    l = LowNodeOf(MyManager.manager, Current);
    h = HighNodeOf(MyManager.manager, Current);
    printf("l(%s)->", curnode);
    DFS(MyManager, l);
    printf("h(%s)->", curnode);
    DFS(MyManager, h);
    AddNode(MyManager.his, MyManager.varmap.varstart, Current, 0.0, 0, NULL);
  }
}

void getalltruepaths(extmanager MyManager, DdNode *Current, const char *startpath, const char *prevvar) {
  DdNode *h, *l;
  char *curnode, *curpath;
  int pathmaxsize = 1024;
  curpath = (char *) malloc(sizeof(char) * pathmaxsize);
  curpath[0] = '\0';
  pathmaxsize = bufstrcat(curpath, pathmaxsize, startpath);
  pathmaxsize = bufstrcat(curpath, pathmaxsize, prevvar);
  pathmaxsize = bufstrcat(curpath, pathmaxsize, "*");
  curnode = GetNodeVarNameDisp(MyManager.manager, MyManager.varmap, Current);
  if (Current == MyManager.t) {
    printf("%s\n", curpath);
  } else if (Current != MyManager.f) {
    h = HighNodeOf(MyManager.manager, Current);
    if (h != MyManager.f) {
      getalltruepaths(MyManager, h, curpath, curnode);
    }
    l = LowNodeOf(MyManager.manager, Current);
    if (l != MyManager.f) {
      pathmaxsize = bufstrcat(curpath, pathmaxsize, "~");
      getalltruepaths(MyManager, l, curpath, curnode);
    }
  }
  free(curpath);
}

int bufstrcat(char *targetstr, int targetmem, const char *srcstr) {
  int strinc = strlen(srcstr), strsize = strlen(targetstr);
  while ((strsize + strinc) > (targetmem - 1)) {
    targetmem *= 2;
    targetstr = (char *) realloc(targetstr, sizeof(char) * targetmem);
  }
  strcat(targetstr, srcstr);
  return targetmem;
}