Browse Source
Fixed wrong includes of cuddObj.hh in expression classes. Added missing files of cudd.
main
Fixed wrong includes of cuddObj.hh in expression classes. Added missing files of cudd.
main
dehnert
13 years ago
8 changed files with 7068 additions and 9 deletions
-
5699resources/3rdparty/cudd-2.5.0/obj/cuddObj.cc
-
762resources/3rdparty/cudd-2.5.0/obj/cuddObj.hh
-
607resources/3rdparty/cudd-2.5.0/obj/testobj.cc
-
1src/ir/expressions/BaseExpression.h
-
2src/ir/expressions/BinaryBooleanFunctionExpression.h
-
2src/ir/expressions/BinaryNumericalFunctionExpression.h
-
2src/ir/expressions/BinaryRelationExpression.h
-
2src/ir/expressions/BooleanConstantExpression.h
5699
resources/3rdparty/cudd-2.5.0/obj/cuddObj.cc
File diff suppressed because it is too large
View File
File diff suppressed because it is too large
View File
@ -0,0 +1,762 @@ |
|||||
|
/**CHeaderFile***************************************************************
|
||||
|
|
||||
|
FileName [cuddObj.hh] |
||||
|
|
||||
|
PackageName [cudd] |
||||
|
|
||||
|
Synopsis [Class definitions for C++ object-oriented encapsulation of |
||||
|
CUDD.] |
||||
|
|
||||
|
Description [Class definitions for C++ object-oriented encapsulation of |
||||
|
CUDD.] |
||||
|
|
||||
|
SeeAlso [] |
||||
|
|
||||
|
Author [Fabio Somenzi] |
||||
|
|
||||
|
Copyright [Copyright (c) 1995-2012, Regents of the University of Colorado |
||||
|
|
||||
|
All rights reserved. |
||||
|
|
||||
|
Redistribution and use in source and binary forms, with or without |
||||
|
modification, are permitted provided that the following conditions |
||||
|
are met: |
||||
|
|
||||
|
Redistributions of source code must retain the above copyright |
||||
|
notice, this list of conditions and the following disclaimer. |
||||
|
|
||||
|
Redistributions in binary form must reproduce the above copyright |
||||
|
notice, this list of conditions and the following disclaimer in the |
||||
|
documentation and/or other materials provided with the distribution. |
||||
|
|
||||
|
Neither the name of the University of Colorado nor the names of its |
||||
|
contributors may be used to endorse or promote products derived from |
||||
|
this software without specific prior written permission. |
||||
|
|
||||
|
THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS |
||||
|
"AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT |
||||
|
LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS |
||||
|
FOR A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE |
||||
|
COPYRIGHT OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, |
||||
|
INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, |
||||
|
BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; |
||||
|
LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER |
||||
|
CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT |
||||
|
LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN |
||||
|
ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE |
||||
|
POSSIBILITY OF SUCH DAMAGE.] |
||||
|
|
||||
|
Revision [$Id: cuddObj.hh,v 1.13 2012/02/05 01:06:40 fabio Exp fabio $] |
||||
|
|
||||
|
******************************************************************************/ |
||||
|
|
||||
|
#ifndef _CPPCUDD
|
||||
|
#define _CPPCUDD
|
||||
|
|
||||
|
#if defined (__GNUC__)
|
||||
|
#if (__GNUC__ >2 || __GNUC_MINOR__ >=7) && !defined(UNUSED)
|
||||
|
#define UNUSED __attribute__ ((unused))
|
||||
|
#else
|
||||
|
#define UNUSED
|
||||
|
#endif
|
||||
|
#else
|
||||
|
#define UNUSED
|
||||
|
#endif
|
||||
|
|
||||
|
/*---------------------------------------------------------------------------*/ |
||||
|
/* Nested includes */ |
||||
|
/*---------------------------------------------------------------------------*/ |
||||
|
|
||||
|
#include <cstdio>
|
||||
|
#include <string>
|
||||
|
#include <vector>
|
||||
|
#include "cudd.h"
|
||||
|
|
||||
|
/*---------------------------------------------------------------------------*/ |
||||
|
/* Type definitions */ |
||||
|
/*---------------------------------------------------------------------------*/ |
||||
|
class BDD; |
||||
|
class ADD; |
||||
|
class ZDD; |
||||
|
class Cudd; |
||||
|
|
||||
|
typedef void (*PFC)(std::string); // handler function type
|
||||
|
|
||||
|
/*---------------------------------------------------------------------------*/ |
||||
|
/* Class definitions */ |
||||
|
/*---------------------------------------------------------------------------*/ |
||||
|
|
||||
|
/**Class***********************************************************************
|
||||
|
|
||||
|
Synopsis [Class for reference counting of CUDD managers.] |
||||
|
|
||||
|
Description [] |
||||
|
|
||||
|
SeeAlso [Cudd DD ABDD ADD BDD ZDD] |
||||
|
|
||||
|
******************************************************************************/ |
||||
|
class Capsule { |
||||
|
friend class DD; |
||||
|
friend class ABDD; |
||||
|
friend class BDD; |
||||
|
friend class ADD; |
||||
|
friend class ZDD; |
||||
|
friend class Cudd; |
||||
|
private: |
||||
|
DdManager *manager; |
||||
|
PFC errorHandler; |
||||
|
PFC timeoutHandler; |
||||
|
bool verbose; |
||||
|
int ref; |
||||
|
}; |
||||
|
|
||||
|
|
||||
|
/**Class***********************************************************************
|
||||
|
|
||||
|
Synopsis [Base class for all decision diagrams in CUDD.] |
||||
|
|
||||
|
Description [] |
||||
|
|
||||
|
SeeAlso [Cudd ABDD ADD BDD ZDD] |
||||
|
|
||||
|
******************************************************************************/ |
||||
|
class DD { |
||||
|
friend class ABDD; |
||||
|
friend class BDD; |
||||
|
friend class ADD; |
||||
|
friend class ZDD; |
||||
|
private: |
||||
|
Capsule *p; |
||||
|
DdNode *node; |
||||
|
inline DdManager * checkSameManager(const DD &other) const; |
||||
|
inline void checkReturnValue(const DdNode *result) const; |
||||
|
inline void checkReturnValue(const int result, const int expected = 1) |
||||
|
const; |
||||
|
public: |
||||
|
DD(); |
||||
|
DD(Capsule *cap, DdNode *ddNode); |
||||
|
DD(Cudd const & manager, DdNode *ddNode); |
||||
|
DD(const DD &from); |
||||
|
virtual ~DD(); |
||||
|
operator bool() const { return node; } |
||||
|
DdManager *manager() const; |
||||
|
DdNode * getNode() const; |
||||
|
DdNode * getRegularNode() const; |
||||
|
int nodeCount() const; |
||||
|
unsigned int NodeReadIndex() const; |
||||
|
|
||||
|
}; // DD
|
||||
|
|
||||
|
|
||||
|
/**Class***********************************************************************
|
||||
|
|
||||
|
Synopsis [Class for ADDs and BDDs.] |
||||
|
|
||||
|
Description [] |
||||
|
|
||||
|
SeeAlso [Cudd ADD BDD] |
||||
|
|
||||
|
******************************************************************************/ |
||||
|
class ABDD : public DD { |
||||
|
friend class BDD; |
||||
|
friend class ADD; |
||||
|
friend class Cudd; |
||||
|
public: |
||||
|
ABDD(); |
||||
|
ABDD(Capsule *cap, DdNode *bddNode); |
||||
|
ABDD(Cudd const & manager, DdNode *ddNode); |
||||
|
ABDD(const ABDD &from); |
||||
|
virtual ~ABDD(); |
||||
|
bool operator==(const ABDD &other) const; |
||||
|
bool operator!=(const ABDD &other) const; |
||||
|
void print(int nvars, int verbosity = 1) const; |
||||
|
DdApaNumber ApaCountMinterm(int nvars, int * digits) const; |
||||
|
void ApaPrintMinterm(int nvars, FILE * fp = stdout) const; |
||||
|
void EpdPrintMinterm(int nvars, FILE * fp = stdout) const; |
||||
|
bool IsOne() const; |
||||
|
bool IsCube() const; |
||||
|
BDD FindEssential() const; |
||||
|
void PrintTwoLiteralClauses(char ** names, FILE * fp = stdout) const; |
||||
|
BDD ShortestPath(int * weight, int * support, int * length) const; |
||||
|
BDD LargestCube(int * length = 0) const; |
||||
|
int ShortestLength(int * weight) const; |
||||
|
bool EquivDC(const ABDD& G, const ABDD& D) const; |
||||
|
double * CofMinterm() const; |
||||
|
void PrintMinterm() const; |
||||
|
double CountMinterm(int nvars) const; |
||||
|
double CountPath() const; |
||||
|
BDD Support() const; |
||||
|
int SupportSize() const; |
||||
|
std::vector<unsigned int> SupportIndices() const; |
||||
|
void ClassifySupport(const ABDD& g, BDD* common, BDD* onlyF, BDD* onlyG) |
||||
|
const; |
||||
|
int CountLeaves() const; |
||||
|
DdGen * FirstCube(int ** cube, CUDD_VALUE_TYPE * value) const; |
||||
|
double Density(int nvars) const; |
||||
|
|
||||
|
}; // ABDD
|
||||
|
|
||||
|
|
||||
|
/**Class***********************************************************************
|
||||
|
|
||||
|
Synopsis [Class for BDDs.] |
||||
|
|
||||
|
Description [] |
||||
|
|
||||
|
SeeAlso [Cudd] |
||||
|
|
||||
|
******************************************************************************/ |
||||
|
class BDD : public ABDD { |
||||
|
friend class Cudd; |
||||
|
public: |
||||
|
BDD(); |
||||
|
BDD(Capsule *cap, DdNode *bddNode); |
||||
|
BDD(Cudd const & manager, DdNode *ddNode); |
||||
|
BDD(const BDD &from); |
||||
|
BDD operator=(const BDD& right); |
||||
|
bool operator<=(const BDD& other) const; |
||||
|
bool operator>=(const BDD& other) const; |
||||
|
bool operator<(const BDD& other) const; |
||||
|
bool operator>(const BDD& other) const; |
||||
|
BDD operator!() const; |
||||
|
BDD operator~() const; |
||||
|
BDD operator*(const BDD& other) const; |
||||
|
BDD operator*=(const BDD& other); |
||||
|
BDD operator&(const BDD& other) const; |
||||
|
BDD operator&=(const BDD& other); |
||||
|
BDD operator+(const BDD& other) const; |
||||
|
BDD operator+=(const BDD& other); |
||||
|
BDD operator|(const BDD& other) const; |
||||
|
BDD operator|=(const BDD& other); |
||||
|
BDD operator^(const BDD& other) const; |
||||
|
BDD operator^=(const BDD& other); |
||||
|
BDD operator-(const BDD& other) const; |
||||
|
BDD operator-=(const BDD& other); |
||||
|
bool IsZero() const; |
||||
|
BDD AndAbstract(const BDD& g, const BDD& cube, unsigned int limit = 0) |
||||
|
const; |
||||
|
BDD UnderApprox( |
||||
|
int numVars, |
||||
|
int threshold = 0, |
||||
|
bool safe = false, |
||||
|
double quality = 1.0) const; |
||||
|
BDD OverApprox( |
||||
|
int numVars, |
||||
|
int threshold = 0, |
||||
|
bool safe = false, |
||||
|
double quality = 1.0) const; |
||||
|
BDD RemapUnderApprox(int numVars, int threshold = 0, double quality = 1.0) |
||||
|
const; |
||||
|
BDD RemapOverApprox(int numVars, int threshold = 0, double quality = 1.0) |
||||
|
const; |
||||
|
BDD BiasedUnderApprox(const BDD& bias, int numVars, int threshold = 0, |
||||
|
double quality1 = 1.0, double quality0 = 1.0) const; |
||||
|
BDD BiasedOverApprox(const BDD& bias, int numVars, int threshold = 0, |
||||
|
double quality1 = 1.0, double quality0 = 1.0) const; |
||||
|
BDD ExistAbstract(const BDD& cube, unsigned int limit = 0) const; |
||||
|
BDD XorExistAbstract(const BDD& g, const BDD& cube) const; |
||||
|
BDD UnivAbstract(const BDD& cube) const; |
||||
|
BDD BooleanDiff(int x) const; |
||||
|
bool VarIsDependent(const BDD& var) const; |
||||
|
double Correlation(const BDD& g) const; |
||||
|
double CorrelationWeights(const BDD& g, double * prob) const; |
||||
|
BDD Ite(const BDD& g, const BDD& h, unsigned int limit = 0) const; |
||||
|
BDD IteConstant(const BDD& g, const BDD& h) const; |
||||
|
BDD Intersect(const BDD& g) const; |
||||
|
BDD And(const BDD& g, unsigned int limit = 0) const; |
||||
|
BDD Or(const BDD& g, unsigned int limit = 0) const; |
||||
|
BDD Nand(const BDD& g) const; |
||||
|
BDD Nor(const BDD& g) const; |
||||
|
BDD Xor(const BDD& g) const; |
||||
|
BDD Xnor(const BDD& g, unsigned int limit = 0) const; |
||||
|
bool Leq(const BDD& g) const; |
||||
|
ADD Add() const; |
||||
|
BDD Transfer(Cudd& destination) const; |
||||
|
BDD ClippingAnd(const BDD& g, int maxDepth, int direction) const; |
||||
|
BDD ClippingAndAbstract(const BDD& g, const BDD& cube, int maxDepth, |
||||
|
int direction) const; |
||||
|
BDD Cofactor(const BDD& g) const; |
||||
|
BDD Compose(const BDD& g, int v) const; |
||||
|
BDD Permute(int * permut) const; |
||||
|
BDD SwapVariables(std::vector<BDD> x, std::vector<BDD> y) const; |
||||
|
BDD AdjPermuteX(std::vector<BDD> x) const; |
||||
|
BDD VectorCompose(std::vector<BDD> vector) const; |
||||
|
void ApproxConjDecomp(BDD* g, BDD* h) const; |
||||
|
void ApproxDisjDecomp(BDD* g, BDD* h) const; |
||||
|
void IterConjDecomp(BDD* g, BDD* h) const; |
||||
|
void IterDisjDecomp(BDD* g, BDD* h) const; |
||||
|
void GenConjDecomp(BDD* g, BDD* h) const; |
||||
|
void GenDisjDecomp(BDD* g, BDD* h) const; |
||||
|
void VarConjDecomp(BDD* g, BDD* h) const; |
||||
|
void VarDisjDecomp(BDD* g, BDD* h) const; |
||||
|
bool IsVarEssential(int id, int phase) const; |
||||
|
BDD Constrain(const BDD& c) const; |
||||
|
BDD Restrict(const BDD& c) const; |
||||
|
BDD NPAnd(const BDD& g) const; |
||||
|
std::vector<BDD> ConstrainDecomp() const; |
||||
|
std::vector<BDD> CharToVect() const; |
||||
|
BDD LICompaction(const BDD& c) const; |
||||
|
BDD Squeeze(const BDD& u) const; |
||||
|
BDD Minimize(const BDD& c) const; |
||||
|
BDD SubsetCompress(int nvars, int threshold) const; |
||||
|
BDD SupersetCompress(int nvars, int threshold) const; |
||||
|
BDD LiteralSetIntersection(const BDD& g) const; |
||||
|
BDD PrioritySelect(std::vector<BDD> x, std::vector<BDD> y, |
||||
|
std::vector<BDD> z, const BDD& Pi, DD_PRFP Pifunc) const; |
||||
|
BDD CProjection(const BDD& Y) const; |
||||
|
int MinHammingDist(int *minterm, int upperBound) const; |
||||
|
BDD Eval(int * inputs) const; |
||||
|
BDD Decreasing(int i) const; |
||||
|
BDD Increasing(int i) const; |
||||
|
bool LeqUnless(const BDD& G, const BDD& D) const; |
||||
|
BDD MakePrime(const BDD& F) const; |
||||
|
BDD MaximallyExpand(const BDD& ub, const BDD& f); |
||||
|
BDD LargestPrimeUnate(const BDD& phases); |
||||
|
BDD SolveEqn(const BDD& Y, BDD* G, int ** yIndex, int n) const; |
||||
|
BDD VerifySol(BDD* G, int * yIndex, int n) const; |
||||
|
BDD SplitSet(std::vector<BDD> xVars, double m) const; |
||||
|
BDD SubsetHeavyBranch(int numVars, int threshold) const; |
||||
|
BDD SupersetHeavyBranch(int numVars, int threshold) const; |
||||
|
BDD SubsetShortPaths(int numVars, int threshold, bool hardlimit = false) const; |
||||
|
BDD SupersetShortPaths(int numVars, int threshold, bool hardlimit = false) const; |
||||
|
void PrintCover() const; |
||||
|
void PrintCover(const BDD& u) const; |
||||
|
int EstimateCofactor(int i, int phase) const; |
||||
|
int EstimateCofactorSimple(int i) const; |
||||
|
void PickOneCube(char * string) const; |
||||
|
BDD PickOneMinterm(std::vector<BDD> vars) const; |
||||
|
DdGen * FirstNode(BDD* fnode) const; |
||||
|
BDD zddIsop(const BDD& U, ZDD* zdd_I) const; |
||||
|
BDD Isop(const BDD& U) const; |
||||
|
ZDD PortToZdd() const; |
||||
|
|
||||
|
}; // BDD
|
||||
|
|
||||
|
|
||||
|
/**Class***********************************************************************
|
||||
|
|
||||
|
Synopsis [Class for ADDs.] |
||||
|
|
||||
|
Description [] |
||||
|
|
||||
|
SeeAlso [Cudd] |
||||
|
|
||||
|
******************************************************************************/ |
||||
|
class ADD : public ABDD { |
||||
|
friend class Cudd; |
||||
|
public: |
||||
|
ADD(); |
||||
|
ADD(Capsule *cap, DdNode *bddNode); |
||||
|
ADD(Cudd const & manager, DdNode *ddNode); |
||||
|
ADD(const ADD &from); |
||||
|
ADD operator=(const ADD& right); |
||||
|
// Relational operators
|
||||
|
bool operator<=(const ADD& other) const; |
||||
|
bool operator>=(const ADD& other) const; |
||||
|
bool operator<(const ADD& other) const; |
||||
|
bool operator>(const ADD& other) const; |
||||
|
// Arithmetic operators
|
||||
|
ADD operator-() const; |
||||
|
ADD operator*(const ADD& other) const; |
||||
|
ADD operator*=(const ADD& other); |
||||
|
ADD operator+(const ADD& other) const; |
||||
|
ADD operator+=(const ADD& other); |
||||
|
ADD operator-(const ADD& other) const; |
||||
|
ADD operator-=(const ADD& other); |
||||
|
// Logical operators
|
||||
|
ADD operator~() const; |
||||
|
ADD operator&(const ADD& other) const; |
||||
|
ADD operator&=(const ADD& other); |
||||
|
ADD operator|(const ADD& other) const; |
||||
|
ADD operator|=(const ADD& other); |
||||
|
bool IsZero() const; |
||||
|
ADD ExistAbstract(const ADD& cube) const; |
||||
|
ADD UnivAbstract(const ADD& cube) const; |
||||
|
ADD OrAbstract(const ADD& cube) const; |
||||
|
ADD Plus(const ADD& g) const; |
||||
|
ADD Times(const ADD& g) const; |
||||
|
ADD Threshold(const ADD& g) const; |
||||
|
ADD SetNZ(const ADD& g) const; |
||||
|
ADD Divide(const ADD& g) const; |
||||
|
ADD Minus(const ADD& g) const; |
||||
|
ADD Minimum(const ADD& g) const; |
||||
|
ADD Maximum(const ADD& g) const; |
||||
|
ADD OneZeroMaximum(const ADD& g) const; |
||||
|
ADD Diff(const ADD& g) const; |
||||
|
ADD Agreement(const ADD& g) const; |
||||
|
ADD Or(const ADD& g) const; |
||||
|
ADD Nand(const ADD& g) const; |
||||
|
ADD Nor(const ADD& g) const; |
||||
|
ADD Xor(const ADD& g) const; |
||||
|
ADD Xnor(const ADD& g) const; |
||||
|
ADD Log() const; |
||||
|
ADD FindMax() const; |
||||
|
ADD FindMin() const; |
||||
|
ADD IthBit(int bit) const; |
||||
|
ADD ScalarInverse(const ADD& epsilon) const; |
||||
|
ADD Ite(const ADD& g, const ADD& h) const; |
||||
|
ADD IteConstant(const ADD& g, const ADD& h) const; |
||||
|
ADD EvalConst(const ADD& g) const; |
||||
|
bool Leq(const ADD& g) const; |
||||
|
ADD Cmpl() const; |
||||
|
ADD Negate() const; |
||||
|
ADD RoundOff(int N) const; |
||||
|
BDD BddThreshold(CUDD_VALUE_TYPE value) const; |
||||
|
BDD BddStrictThreshold(CUDD_VALUE_TYPE value) const; |
||||
|
BDD BddInterval(CUDD_VALUE_TYPE lower, CUDD_VALUE_TYPE upper) const; |
||||
|
BDD BddIthBit(int bit) const; |
||||
|
BDD BddPattern() const; |
||||
|
ADD Cofactor(const ADD& g) const; |
||||
|
ADD Compose(const ADD& g, int v) const; |
||||
|
ADD Permute(int * permut) const; |
||||
|
ADD SwapVariables(std::vector<ADD> x, std::vector<ADD> y) const; |
||||
|
ADD VectorCompose(std::vector<ADD> vector) const; |
||||
|
ADD NonSimCompose(std::vector<ADD> vector) const; |
||||
|
ADD Constrain(const ADD& c) const; |
||||
|
ADD Restrict(const ADD& c) const; |
||||
|
ADD MatrixMultiply(const ADD& B, std::vector<ADD> z) const; |
||||
|
ADD TimesPlus(const ADD& B, std::vector<ADD> z) const; |
||||
|
ADD Triangle(const ADD& g, std::vector<ADD> z) const; |
||||
|
ADD Eval(int * inputs) const; |
||||
|
bool EqualSupNorm(const ADD& g, CUDD_VALUE_TYPE tolerance, int pr) const; |
||||
|
|
||||
|
}; // ADD
|
||||
|
|
||||
|
|
||||
|
/**Class***********************************************************************
|
||||
|
|
||||
|
Synopsis [Class for ZDDs.] |
||||
|
|
||||
|
Description [] |
||||
|
|
||||
|
SeeAlso [Cudd] |
||||
|
|
||||
|
******************************************************************************/ |
||||
|
class ZDD : public DD { |
||||
|
friend class Cudd; |
||||
|
public: |
||||
|
ZDD(Capsule *cap, DdNode *bddNode); |
||||
|
ZDD(); |
||||
|
ZDD(const ZDD &from); |
||||
|
~ZDD(); |
||||
|
ZDD operator=(const ZDD& right); |
||||
|
bool operator==(const ZDD& other) const; |
||||
|
bool operator!=(const ZDD& other) const; |
||||
|
bool operator<=(const ZDD& other) const; |
||||
|
bool operator>=(const ZDD& other) const; |
||||
|
bool operator<(const ZDD& other) const; |
||||
|
bool operator>(const ZDD& other) const; |
||||
|
void print(int nvars, int verbosity = 1) const; |
||||
|
ZDD operator*(const ZDD& other) const; |
||||
|
ZDD operator*=(const ZDD& other); |
||||
|
ZDD operator&(const ZDD& other) const; |
||||
|
ZDD operator&=(const ZDD& other); |
||||
|
ZDD operator+(const ZDD& other) const; |
||||
|
ZDD operator+=(const ZDD& other); |
||||
|
ZDD operator|(const ZDD& other) const; |
||||
|
ZDD operator|=(const ZDD& other); |
||||
|
ZDD operator-(const ZDD& other) const; |
||||
|
ZDD operator-=(const ZDD& other); |
||||
|
int Count() const; |
||||
|
double CountDouble() const; |
||||
|
ZDD Product(const ZDD& g) const; |
||||
|
ZDD UnateProduct(const ZDD& g) const; |
||||
|
ZDD WeakDiv(const ZDD& g) const; |
||||
|
ZDD Divide(const ZDD& g) const; |
||||
|
ZDD WeakDivF(const ZDD& g) const; |
||||
|
ZDD DivideF(const ZDD& g) const; |
||||
|
double CountMinterm(int path) const; |
||||
|
BDD PortToBdd() const; |
||||
|
ZDD Ite(const ZDD& g, const ZDD& h) const; |
||||
|
ZDD Union(const ZDD& Q) const; |
||||
|
ZDD Intersect(const ZDD& Q) const; |
||||
|
ZDD Diff(const ZDD& Q) const; |
||||
|
ZDD DiffConst(const ZDD& Q) const; |
||||
|
ZDD Subset1(int var) const; |
||||
|
ZDD Subset0(int var) const; |
||||
|
ZDD Change(int var) const; |
||||
|
void PrintMinterm() const; |
||||
|
void PrintCover() const; |
||||
|
BDD Support() const; |
||||
|
|
||||
|
}; // ZDD
|
||||
|
|
||||
|
|
||||
|
/**Class***********************************************************************
|
||||
|
|
||||
|
Synopsis [Class for CUDD managers.] |
||||
|
|
||||
|
Description [] |
||||
|
|
||||
|
SeeAlso [DD] |
||||
|
|
||||
|
******************************************************************************/ |
||||
|
class Cudd { |
||||
|
friend class DD; |
||||
|
friend class ABDD; |
||||
|
friend class BDD; |
||||
|
friend class ADD; |
||||
|
friend class ZDD; |
||||
|
private: |
||||
|
Capsule *p; |
||||
|
public: |
||||
|
Cudd( |
||||
|
unsigned int numVars = 0, |
||||
|
unsigned int numVarsZ = 0, |
||||
|
unsigned int numSlots = CUDD_UNIQUE_SLOTS, |
||||
|
unsigned int cacheSize = CUDD_CACHE_SLOTS, |
||||
|
unsigned long maxMemory = 0); |
||||
|
Cudd(const Cudd& x); |
||||
|
~Cudd(); |
||||
|
PFC setHandler(PFC newHandler) const; |
||||
|
PFC getHandler() const; |
||||
|
PFC setTimeoutHandler(PFC newHandler) const; |
||||
|
PFC getTimeoutHandler() const; |
||||
|
DdManager *getManager() const {return p->manager;} |
||||
|
inline void makeVerbose() const {p->verbose = 1;} |
||||
|
inline void makeTerse() {p->verbose = 0;} |
||||
|
inline bool isVerbose() const {return p->verbose;} |
||||
|
inline void checkReturnValue(const DdNode *result) const; |
||||
|
inline void checkReturnValue(const int result) const; |
||||
|
Cudd& operator=(const Cudd& right); |
||||
|
void info() const; |
||||
|
BDD bddVar() const; |
||||
|
BDD bddVar(int index) const; |
||||
|
BDD bddOne() const; |
||||
|
BDD bddZero() const; |
||||
|
ADD addVar() const; |
||||
|
ADD addVar(int index) const; |
||||
|
ADD addOne() const; |
||||
|
ADD addZero() const; |
||||
|
ADD constant(CUDD_VALUE_TYPE c) const; |
||||
|
ADD plusInfinity() const; |
||||
|
ADD minusInfinity() const; |
||||
|
ZDD zddVar(int index) const; |
||||
|
ZDD zddOne(int i) const; |
||||
|
ZDD zddZero() const; |
||||
|
ADD addNewVarAtLevel(int level) const; |
||||
|
BDD bddNewVarAtLevel(int level) const; |
||||
|
void zddVarsFromBddVars(int multiplicity) const; |
||||
|
unsigned long ReadStartTime() const; |
||||
|
unsigned long ReadElapsedTime() const; |
||||
|
void SetStartTime(unsigned long st) const; |
||||
|
void ResetStartTime() const; |
||||
|
unsigned long ReadTimeLimit() const; |
||||
|
void SetTimeLimit(unsigned long tl) const; |
||||
|
void UpdateTimeLimit() const; |
||||
|
void IncreaseTimeLimit(unsigned long increase) const; |
||||
|
void UnsetTimeLimit() const; |
||||
|
bool TimeLimited() const; |
||||
|
void AutodynEnable(Cudd_ReorderingType method) const; |
||||
|
void AutodynDisable() const; |
||||
|
bool ReorderingStatus(Cudd_ReorderingType * method) const; |
||||
|
void AutodynEnableZdd(Cudd_ReorderingType method) const; |
||||
|
void AutodynDisableZdd() const; |
||||
|
bool ReorderingStatusZdd(Cudd_ReorderingType * method) const; |
||||
|
bool zddRealignmentEnabled() const; |
||||
|
void zddRealignEnable() const; |
||||
|
void zddRealignDisable() const; |
||||
|
bool bddRealignmentEnabled() const; |
||||
|
void bddRealignEnable() const; |
||||
|
void bddRealignDisable() const; |
||||
|
ADD background() const; |
||||
|
void SetBackground(ADD bg) const; |
||||
|
unsigned int ReadCacheSlots() const; |
||||
|
double ReadCacheUsedSlots() const; |
||||
|
double ReadCacheLookUps() const; |
||||
|
double ReadCacheHits() const; |
||||
|
unsigned int ReadMinHit() const; |
||||
|
void SetMinHit(unsigned int hr) const; |
||||
|
unsigned int ReadLooseUpTo() const; |
||||
|
void SetLooseUpTo(unsigned int lut) const; |
||||
|
unsigned int ReadMaxCache() const; |
||||
|
unsigned int ReadMaxCacheHard() const; |
||||
|
void SetMaxCacheHard(unsigned int mc) const; |
||||
|
int ReadSize() const; |
||||
|
int ReadZddSize() const; |
||||
|
unsigned int ReadSlots() const; |
||||
|
unsigned int ReadKeys() const; |
||||
|
unsigned int ReadDead() const; |
||||
|
unsigned int ReadMinDead() const; |
||||
|
unsigned int ReadReorderings() const; |
||||
|
unsigned int ReadMaxReorderings() const; |
||||
|
void SetMaxReorderings(unsigned int mr) const; |
||||
|
long ReadReorderingTime() const; |
||||
|
int ReadGarbageCollections() const; |
||||
|
long ReadGarbageCollectionTime() const; |
||||
|
int ReadSiftMaxVar() const; |
||||
|
void SetSiftMaxVar(int smv) const; |
||||
|
int ReadSiftMaxSwap() const; |
||||
|
void SetSiftMaxSwap(int sms) const; |
||||
|
double ReadMaxGrowth() const; |
||||
|
void SetMaxGrowth(double mg) const; |
||||
|
MtrNode * ReadTree() const; |
||||
|
void SetTree(MtrNode * tree) const; |
||||
|
void FreeTree() const; |
||||
|
MtrNode * ReadZddTree() const; |
||||
|
void SetZddTree(MtrNode * tree) const; |
||||
|
void FreeZddTree() const; |
||||
|
int ReadPerm(int i) const; |
||||
|
int ReadPermZdd(int i) const; |
||||
|
int ReadInvPerm(int i) const; |
||||
|
int ReadInvPermZdd(int i) const; |
||||
|
BDD ReadVars(int i) const; |
||||
|
CUDD_VALUE_TYPE ReadEpsilon() const; |
||||
|
void SetEpsilon(CUDD_VALUE_TYPE ep) const; |
||||
|
Cudd_AggregationType ReadGroupcheck() const; |
||||
|
void SetGroupcheck(Cudd_AggregationType gc) const; |
||||
|
bool GarbageCollectionEnabled() const; |
||||
|
void EnableGarbageCollection() const; |
||||
|
void DisableGarbageCollection() const; |
||||
|
bool DeadAreCounted() const; |
||||
|
void TurnOnCountDead() const; |
||||
|
void TurnOffCountDead() const; |
||||
|
int ReadRecomb() const; |
||||
|
void SetRecomb(int recomb) const; |
||||
|
int ReadSymmviolation() const; |
||||
|
void SetSymmviolation(int symmviolation) const; |
||||
|
int ReadArcviolation() const; |
||||
|
void SetArcviolation(int arcviolation) const; |
||||
|
int ReadPopulationSize() const; |
||||
|
void SetPopulationSize(int populationSize) const; |
||||
|
int ReadNumberXovers() const; |
||||
|
void SetNumberXovers(int numberXovers) const; |
||||
|
unsigned int ReadOrderRandomization() const; |
||||
|
void SetOrderRandomization(unsigned int factor) const; |
||||
|
unsigned long ReadMemoryInUse() const; |
||||
|
long ReadPeakNodeCount() const; |
||||
|
long ReadNodeCount() const; |
||||
|
long zddReadNodeCount() const; |
||||
|
void AddHook(DD_HFP f, Cudd_HookType where) const; |
||||
|
void RemoveHook(DD_HFP f, Cudd_HookType where) const; |
||||
|
bool IsInHook(DD_HFP f, Cudd_HookType where) const; |
||||
|
void EnableReorderingReporting() const; |
||||
|
void DisableReorderingReporting() const; |
||||
|
bool ReorderingReporting() const; |
||||
|
int ReadErrorCode() const; |
||||
|
void ClearErrorCode() const; |
||||
|
FILE *ReadStdout() const; |
||||
|
void SetStdout(FILE *) const; |
||||
|
FILE *ReadStderr() const; |
||||
|
void SetStderr(FILE *) const; |
||||
|
unsigned int ReadNextReordering() const; |
||||
|
void SetNextReordering(unsigned int) const; |
||||
|
double ReadSwapSteps() const; |
||||
|
unsigned int ReadMaxLive() const; |
||||
|
void SetMaxLive(unsigned int) const; |
||||
|
unsigned long ReadMaxMemory() const; |
||||
|
void SetMaxMemory(unsigned long) const; |
||||
|
int bddBindVar(int) const; |
||||
|
int bddUnbindVar(int) const; |
||||
|
bool bddVarIsBound(int) const; |
||||
|
ADD Walsh(std::vector<ADD> x, std::vector<ADD> y); |
||||
|
ADD addResidue(int n, int m, int options, int top); |
||||
|
int ApaNumberOfDigits(int binaryDigits) const; |
||||
|
DdApaNumber NewApaNumber(int digits) const; |
||||
|
void ApaCopy(int digits, DdApaNumber source, DdApaNumber dest) const; |
||||
|
DdApaDigit ApaAdd(int digits, DdApaNumber a, DdApaNumber b, DdApaNumber |
||||
|
sum) const; |
||||
|
DdApaDigit ApaSubtract(int digits, DdApaNumber a, DdApaNumber b, |
||||
|
DdApaNumber diff) const; |
||||
|
DdApaDigit ApaShortDivision(int digits, DdApaNumber dividend, DdApaDigit |
||||
|
divisor, DdApaNumber quotient) const; |
||||
|
void ApaShiftRight(int digits, DdApaDigit in, DdApaNumber a, DdApaNumber |
||||
|
b) const; |
||||
|
void ApaSetToLiteral(int digits, DdApaNumber number, DdApaDigit literal) |
||||
|
const; |
||||
|
void ApaPowerOfTwo(int digits, DdApaNumber number, int power) const; |
||||
|
void ApaPrintHex(FILE * fp, int digits, DdApaNumber number) const; |
||||
|
void ApaPrintDecimal(FILE * fp, int digits, DdApaNumber number) const; |
||||
|
void DebugCheck(); |
||||
|
void CheckKeys(); |
||||
|
MtrNode * MakeTreeNode(unsigned int low, unsigned int size, unsigned int type) const; |
||||
|
// void Harwell(FILE * fp, ADD* E, ADD** x, ADD** y, ADD** xn, ADD** yn_, int * nx, int * ny, int * m, int * n, int bx, int sx, int by, int sy, int pr);
|
||||
|
void PrintLinear(); |
||||
|
int ReadLinear(int x, int y); |
||||
|
BDD Xgty(std::vector<BDD> z, std::vector<BDD> x, std::vector<BDD> y); |
||||
|
BDD Xeqy(std::vector<BDD> x, std::vector<BDD> y); |
||||
|
ADD Xeqy(std::vector<ADD> x, std::vector<ADD> y); |
||||
|
BDD Dxygtdxz(std::vector<BDD> x, std::vector<BDD> y, std::vector<BDD> z); |
||||
|
BDD Dxygtdyz(std::vector<BDD> x, std::vector<BDD> y, std::vector<BDD> z); |
||||
|
BDD Inequality(int c, std::vector<BDD> x, std::vector<BDD> y); |
||||
|
BDD Disequality(int c, std::vector<BDD> x, std::vector<BDD> y); |
||||
|
BDD Interval(std::vector<BDD> x, unsigned int lowerB, unsigned int upperB); |
||||
|
ADD Hamming(std::vector<ADD> xVars, std::vector<ADD> yVars); |
||||
|
// void Read(FILE * fp, ADD* E, ADD** x, ADD** y, ADD** xn, ADD** yn_, int * nx, int * ny, int * m, int * n, int bx, int sx, int by, int sy);
|
||||
|
// void Read(FILE * fp, BDD* E, BDD** x, BDD** y, int * nx, int * ny, int * m, int * n, int bx, int sx, int by, int sy);
|
||||
|
void ReduceHeap(Cudd_ReorderingType heuristic, int minsize); |
||||
|
void ShuffleHeap(int * permutation); |
||||
|
void SymmProfile(int lower, int upper) const; |
||||
|
unsigned int Prime(unsigned int pr) const; |
||||
|
void Reserve(int amount) const; |
||||
|
int SharingSize(DD* nodes, int n) const; |
||||
|
int SharingSize(const std::vector<BDD>& v) const; |
||||
|
BDD bddComputeCube(BDD * vars, int * phase, int n) const; |
||||
|
ADD addComputeCube(ADD * vars, int * phase, int n); |
||||
|
int NextNode(DdGen * gen, BDD * nnode); |
||||
|
BDD IndicesToCube(int * array, int n); |
||||
|
void PrintVersion(FILE * fp) const; |
||||
|
double AverageDistance() const; |
||||
|
long Random() const; |
||||
|
void Srandom(long seed) const; |
||||
|
MtrNode * MakeZddTreeNode(unsigned int low, unsigned int size, unsigned int type); |
||||
|
void zddPrintSubtable() const; |
||||
|
void zddReduceHeap(Cudd_ReorderingType heuristic, int minsize); |
||||
|
void zddShuffleHeap(int * permutation); |
||||
|
void zddSymmProfile(int lower, int upper) const; |
||||
|
void DumpDot( |
||||
|
const std::vector<BDD>& nodes, |
||||
|
char ** inames = 0, |
||||
|
char ** onames = 0, |
||||
|
FILE * fp = stdout) const; |
||||
|
void DumpDaVinci( |
||||
|
const std::vector<BDD>& nodes, |
||||
|
char ** inames = 0, |
||||
|
char ** onames = 0, |
||||
|
FILE * fp = stdout) const; |
||||
|
void DumpBlif( |
||||
|
const std::vector<BDD>& nodes, |
||||
|
char ** inames = 0, |
||||
|
char ** onames = 0, |
||||
|
char * mname = 0, |
||||
|
FILE * fp = stdout, |
||||
|
int mv = 0) const; |
||||
|
void DumpDDcal( |
||||
|
const std::vector<BDD>& nodes, |
||||
|
char ** inames = 0, |
||||
|
char ** onames = 0, |
||||
|
FILE * fp = stdout) const; |
||||
|
void DumpFactoredForm( |
||||
|
const std::vector<BDD>& nodes, |
||||
|
char ** inames = 0, |
||||
|
char ** onames = 0, |
||||
|
FILE * fp = stdout) const; |
||||
|
BDD VectorSupport(const std::vector<BDD>& roots) const; |
||||
|
std::vector<unsigned int> |
||||
|
SupportIndices(const std::vector<ABDD>& roots) const; |
||||
|
int nodeCount(const std::vector<BDD>& roots) const; |
||||
|
int VectorSupportSize(const std::vector<BDD>& roots) const; |
||||
|
void DumpDot( |
||||
|
const std::vector<ADD>& nodes, |
||||
|
char ** inames = 0, |
||||
|
char ** onames = 0, |
||||
|
FILE * fp = stdout) const; |
||||
|
void DumpDaVinci( |
||||
|
const std::vector<ADD>& nodes, |
||||
|
char ** inames = 0, |
||||
|
char ** onames = 0, |
||||
|
FILE * fp = stdout) const; |
||||
|
BDD VectorSupport(const std::vector<ADD>& roots) const; |
||||
|
int VectorSupportSize(const std::vector<ADD>& roots) const; |
||||
|
void DumpDot( |
||||
|
const std::vector<ZDD>& nodes, |
||||
|
char ** inames = 0, |
||||
|
char ** onames = 0, |
||||
|
FILE * fp = stdout) const; |
||||
|
|
||||
|
}; // Cudd
|
||||
|
|
||||
|
|
||||
|
extern void defaultError(std::string message); |
||||
|
|
||||
|
#endif
|
||||
@ -0,0 +1,607 @@ |
|||||
|
/**CFile***********************************************************************
|
||||
|
|
||||
|
FileName [testobj.cc] |
||||
|
|
||||
|
PackageName [cuddObj] |
||||
|
|
||||
|
Synopsis [Test program for the C++ object-oriented encapsulation of CUDD.] |
||||
|
|
||||
|
Description [] |
||||
|
|
||||
|
SeeAlso [] |
||||
|
|
||||
|
Author [Fabio Somenzi] |
||||
|
|
||||
|
Copyright [Copyright (c) 1995-2012, Regents of the University of Colorado |
||||
|
|
||||
|
All rights reserved. |
||||
|
|
||||
|
Redistribution and use in source and binary forms, with or without |
||||
|
modification, are permitted provided that the following conditions |
||||
|
are met: |
||||
|
|
||||
|
Redistributions of source code must retain the above copyright |
||||
|
notice, this list of conditions and the following disclaimer. |
||||
|
|
||||
|
Redistributions in binary form must reproduce the above copyright |
||||
|
notice, this list of conditions and the following disclaimer in the |
||||
|
documentation and/or other materials provided with the distribution. |
||||
|
|
||||
|
Neither the name of the University of Colorado nor the names of its |
||||
|
contributors may be used to endorse or promote products derived from |
||||
|
this software without specific prior written permission. |
||||
|
|
||||
|
THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS |
||||
|
"AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT |
||||
|
LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS |
||||
|
FOR A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE |
||||
|
COPYRIGHT OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, |
||||
|
INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, |
||||
|
BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; |
||||
|
LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER |
||||
|
CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT |
||||
|
LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN |
||||
|
ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE |
||||
|
POSSIBILITY OF SUCH DAMAGE.] |
||||
|
|
||||
|
******************************************************************************/ |
||||
|
|
||||
|
#include "cuddObj.hh"
|
||||
|
#include <math.h>
|
||||
|
#include <iostream>
|
||||
|
#include <cassert>
|
||||
|
|
||||
|
using namespace std; |
||||
|
|
||||
|
/*---------------------------------------------------------------------------*/ |
||||
|
/* Variable declarations */ |
||||
|
/*---------------------------------------------------------------------------*/ |
||||
|
|
||||
|
#ifndef lint
|
||||
|
static char rcsid[] UNUSED = "$Id: testobj.cc,v 1.7 2012/02/05 01:06:40 fabio Exp fabio $"; |
||||
|
#endif
|
||||
|
|
||||
|
/*---------------------------------------------------------------------------*/ |
||||
|
/* Static function prototypes */ |
||||
|
/*---------------------------------------------------------------------------*/ |
||||
|
|
||||
|
static void testBdd(Cudd& mgr, int verbosity); |
||||
|
static void testAdd(Cudd& mgr, int verbosity); |
||||
|
static void testAdd2(Cudd& mgr, int verbosity); |
||||
|
static void testZdd(Cudd& mgr, int verbosity); |
||||
|
static void testBdd2(Cudd& mgr, int verbosity); |
||||
|
static void testBdd3(Cudd& mgr, int verbosity); |
||||
|
static void testZdd2(Cudd& mgr, int verbosity); |
||||
|
static void testBdd4(Cudd& mgr, int verbosity); |
||||
|
static void testBdd5(Cudd& mgr, int verbosity); |
||||
|
|
||||
|
|
||||
|
/*---------------------------------------------------------------------------*/ |
||||
|
/* Definition of exported functions */ |
||||
|
/*---------------------------------------------------------------------------*/ |
||||
|
|
||||
|
/**Function********************************************************************
|
||||
|
|
||||
|
Synopsis [Main program for testobj.] |
||||
|
|
||||
|
Description [] |
||||
|
|
||||
|
SideEffects [None] |
||||
|
|
||||
|
SeeAlso [] |
||||
|
|
||||
|
******************************************************************************/ |
||||
|
int |
||||
|
main(int argc, char **argv) |
||||
|
{ |
||||
|
int verbosity = 0; |
||||
|
|
||||
|
if (argc == 2) { |
||||
|
int retval = sscanf(argv[1], "%d", &verbosity); |
||||
|
if (retval != 1) |
||||
|
return 1; |
||||
|
} else if (argc != 1) { |
||||
|
return 1; |
||||
|
} |
||||
|
|
||||
|
Cudd mgr(0,2); |
||||
|
// mgr.makeVerbose(); // trace constructors and destructors
|
||||
|
testBdd(mgr,verbosity); |
||||
|
testAdd(mgr,verbosity); |
||||
|
testAdd2(mgr,verbosity); |
||||
|
testZdd(mgr,verbosity); |
||||
|
testBdd2(mgr,verbosity); |
||||
|
testBdd3(mgr,verbosity); |
||||
|
testZdd2(mgr,verbosity); |
||||
|
testBdd4(mgr,verbosity); |
||||
|
testBdd5(mgr,verbosity); |
||||
|
if (verbosity) mgr.info(); |
||||
|
return 0; |
||||
|
|
||||
|
} // main
|
||||
|
|
||||
|
|
||||
|
/**Function********************************************************************
|
||||
|
|
||||
|
Synopsis [Test basic operators on BDDs.] |
||||
|
|
||||
|
Description [Test basic operators on BDDs. The function returns void |
||||
|
because it relies on the error handling done by the interface. The |
||||
|
default error handler causes program termination.] |
||||
|
|
||||
|
SideEffects [Creates BDD variables in the manager.] |
||||
|
|
||||
|
SeeAlso [testBdd2 testBdd3 testBdd4 testBdd5] |
||||
|
|
||||
|
******************************************************************************/ |
||||
|
static void |
||||
|
testBdd( |
||||
|
Cudd& mgr, |
||||
|
int verbosity) |
||||
|
{ |
||||
|
if (verbosity) cout << "Entering testBdd\n"; |
||||
|
// Create two new variables in the manager. If testBdd is called before
|
||||
|
// any variable is created in mgr, then x gets index 0 and y gets index 1.
|
||||
|
BDD x = mgr.bddVar(); |
||||
|
BDD y = mgr.bddVar(); |
||||
|
|
||||
|
BDD f = x * y; |
||||
|
if (verbosity) cout << "f"; f.print(2,verbosity); |
||||
|
|
||||
|
BDD g = y + !x; |
||||
|
if (verbosity) cout << "g"; g.print(2,verbosity); |
||||
|
|
||||
|
if (verbosity) |
||||
|
cout << "f and g are" << (f == !g ? "" : " not") << " complementary\n"; |
||||
|
if (verbosity) |
||||
|
cout << "f is" << (f <= g ? "" : " not") << " less than or equal to g\n"; |
||||
|
|
||||
|
g = f | ~g; |
||||
|
if (verbosity) cout << "g"; g.print(2,verbosity); |
||||
|
|
||||
|
BDD h = f = y; |
||||
|
if (verbosity) cout << "h"; h.print(2,verbosity); |
||||
|
|
||||
|
if (verbosity) cout << "x + h has " << (x+h).nodeCount() << " nodes\n"; |
||||
|
|
||||
|
h += x; |
||||
|
if (verbosity) cout << "h"; h.print(2,verbosity); |
||||
|
|
||||
|
} // testBdd
|
||||
|
|
||||
|
|
||||
|
/**Function********************************************************************
|
||||
|
|
||||
|
Synopsis [Test basic operators on ADDs.] |
||||
|
|
||||
|
Description [Test basic operators on ADDs. The function returns void |
||||
|
because it relies on the error handling done by the interface. The |
||||
|
default error handler causes program termination.] |
||||
|
|
||||
|
SideEffects [May create ADD variables in the manager.] |
||||
|
|
||||
|
SeeAlso [testAdd2] |
||||
|
|
||||
|
******************************************************************************/ |
||||
|
static void |
||||
|
testAdd( |
||||
|
Cudd& mgr, |
||||
|
int verbosity) |
||||
|
{ |
||||
|
if (verbosity) cout << "Entering testAdd\n"; |
||||
|
// Create two ADD variables. If we called method addVar without an
|
||||
|
// argument, we would get two new indices. If testAdd is indeed called
|
||||
|
// after testBdd, then those indices would be 2 and 3. By specifying the
|
||||
|
// arguments, on the other hand, we avoid creating new unnecessary BDD
|
||||
|
// variables.
|
||||
|
ADD p = mgr.addVar(0); |
||||
|
ADD q = mgr.addVar(1); |
||||
|
|
||||
|
// Test arithmetic operators.
|
||||
|
ADD r = p + q; |
||||
|
if (verbosity) cout << "r"; r.print(2,verbosity); |
||||
|
|
||||
|
// CUDD_VALUE_TYPE is double.
|
||||
|
ADD s = mgr.constant(3.0); |
||||
|
s *= p * q; |
||||
|
if (verbosity) cout << "s"; s.print(2,verbosity); |
||||
|
|
||||
|
s += mgr.plusInfinity(); |
||||
|
if (verbosity) cout << "s"; s.print(2,verbosity); |
||||
|
|
||||
|
// Test relational operators.
|
||||
|
if (verbosity) |
||||
|
cout << "p is" << (p <= r ? "" : " not") << " less than or equal to r\n"; |
||||
|
|
||||
|
// Test logical operators.
|
||||
|
r = p | q; |
||||
|
if (verbosity) cout << "r"; r.print(2,verbosity); |
||||
|
|
||||
|
} // testAdd
|
||||
|
|
||||
|
|
||||
|
/**Function********************************************************************
|
||||
|
|
||||
|
Synopsis [Test some more operators on ADDs.] |
||||
|
|
||||
|
Description [Test some more operators on ADDs. The function returns void |
||||
|
because it relies on the error handling done by the interface. The |
||||
|
default error handler causes program termination.] |
||||
|
|
||||
|
SideEffects [May create ADD variables in the manager.] |
||||
|
|
||||
|
SeeAlso [testAdd] |
||||
|
|
||||
|
******************************************************************************/ |
||||
|
static void |
||||
|
testAdd2( |
||||
|
Cudd& mgr, |
||||
|
int verbosity) |
||||
|
{ |
||||
|
if (verbosity) cout << "Entering testAdd2\n"; |
||||
|
// Create two ADD variables. If we called method addVar without an
|
||||
|
// argument, we would get two new indices.
|
||||
|
int i; |
||||
|
vector<ADD> x(2); |
||||
|
for (i = 0; i < 2; i++) { |
||||
|
x[i] = mgr.addVar(i); |
||||
|
} |
||||
|
|
||||
|
// Build a probability density function: [0.1, 0.2, 0.3, 0.4].
|
||||
|
ADD f0 = x[1].Ite(mgr.constant(0.2), mgr.constant(0.1)); |
||||
|
ADD f1 = x[1].Ite(mgr.constant(0.4), mgr.constant(0.3)); |
||||
|
ADD f = x[0].Ite(f1, f0); |
||||
|
if (verbosity) cout << "f"; f.print(2,verbosity); |
||||
|
|
||||
|
// Compute the entropy.
|
||||
|
ADD l = f.Log(); |
||||
|
if (verbosity) cout << "l"; l.print(2,verbosity); |
||||
|
ADD r = f * l; |
||||
|
if (verbosity) cout << "r"; r.print(2,verbosity); |
||||
|
|
||||
|
ADD e = r.MatrixMultiply(mgr.constant(-1.0/log(2.0)),x); |
||||
|
if (verbosity) cout << "e"; e.print(2,verbosity); |
||||
|
|
||||
|
} // testAdd2
|
||||
|
|
||||
|
|
||||
|
/**Function********************************************************************
|
||||
|
|
||||
|
Synopsis [Test basic operators on ZDDs.] |
||||
|
|
||||
|
Description [Test basic operators on ZDDs. The function returns void |
||||
|
because it relies on the error handling done by the interface. The |
||||
|
default error handler causes program termination.] |
||||
|
|
||||
|
SideEffects [May create ZDD variables in the manager.] |
||||
|
|
||||
|
SeeAlso [testZdd2] |
||||
|
|
||||
|
******************************************************************************/ |
||||
|
static void |
||||
|
testZdd( |
||||
|
Cudd& mgr, |
||||
|
int verbosity) |
||||
|
{ |
||||
|
if (verbosity) cout << "Entering testZdd\n"; |
||||
|
ZDD v = mgr.zddVar(0); |
||||
|
ZDD w = mgr.zddVar(1); |
||||
|
|
||||
|
ZDD s = v + w; |
||||
|
if (verbosity) cout << "s"; s.print(2,verbosity); |
||||
|
|
||||
|
if (verbosity) cout << "v is" << (v < s ? "" : " not") << " less than s\n"; |
||||
|
|
||||
|
s -= v; |
||||
|
if (verbosity) cout << "s"; s.print(2,verbosity); |
||||
|
|
||||
|
} // testZdd
|
||||
|
|
||||
|
|
||||
|
/**Function********************************************************************
|
||||
|
|
||||
|
Synopsis [Test vector operators on BDDs.] |
||||
|
|
||||
|
Description [Test vector operators on BDDs. The function returns void |
||||
|
because it relies on the error handling done by the interface. The |
||||
|
default error handler causes program termination.] |
||||
|
|
||||
|
SideEffects [May create BDD variables in the manager.] |
||||
|
|
||||
|
SeeAlso [testBdd testBdd3 testBdd4 testBdd5] |
||||
|
|
||||
|
******************************************************************************/ |
||||
|
static void |
||||
|
testBdd2( |
||||
|
Cudd& mgr, |
||||
|
int verbosity) |
||||
|
{ |
||||
|
if (verbosity) cout << "Entering testBdd2\n"; |
||||
|
vector<BDD> x(4); |
||||
|
for (int i = 0; i < 4; i++) { |
||||
|
x[i] = mgr.bddVar(i); |
||||
|
} |
||||
|
|
||||
|
// Create the BDD for the Achilles' Heel function.
|
||||
|
BDD p1 = x[0] * x[2]; |
||||
|
BDD p2 = x[1] * x[3]; |
||||
|
BDD f = p1 + p2; |
||||
|
const char* inames[] = {"x0", "x1", "x2", "x3"}; |
||||
|
if (verbosity) { |
||||
|
cout << "f"; f.print(4,verbosity); |
||||
|
cout << "Irredundant cover of f:" << endl; f.PrintCover(); |
||||
|
cout << "Number of minterms (arbitrary precision): "; f.ApaPrintMinterm(4); |
||||
|
cout << "Number of minterms (extended precision): "; f.EpdPrintMinterm(4); |
||||
|
cout << "Two-literal clauses of f:" << endl; |
||||
|
f.PrintTwoLiteralClauses((char **)inames); cout << endl; |
||||
|
} |
||||
|
|
||||
|
vector<BDD> vect = f.CharToVect(); |
||||
|
if (verbosity) { |
||||
|
for (size_t i = 0; i < vect.size(); i++) { |
||||
|
cout << "vect[" << i << "]" << endl; vect[i].PrintCover(); |
||||
|
} |
||||
|
} |
||||
|
|
||||
|
// v0,...,v3 suffice if testBdd2 is called before testBdd3.
|
||||
|
if (verbosity) { |
||||
|
const char* onames[] = {"v0", "v1", "v2", "v3", "v4", "v5"}; |
||||
|
mgr.DumpDot(vect, (char **)inames,(char **)onames); |
||||
|
} |
||||
|
|
||||
|
} // testBdd2
|
||||
|
|
||||
|
|
||||
|
/**Function********************************************************************
|
||||
|
|
||||
|
Synopsis [Test additional operators on BDDs.] |
||||
|
|
||||
|
Description [Test additional operators on BDDs. The function returns |
||||
|
void because it relies on the error handling done by the |
||||
|
interface. The default error handler causes program termination.] |
||||
|
|
||||
|
SideEffects [May create BDD variables in the manager.] |
||||
|
|
||||
|
SeeAlso [testBdd testBdd2 testBdd4 testBdd5] |
||||
|
|
||||
|
******************************************************************************/ |
||||
|
static void |
||||
|
testBdd3( |
||||
|
Cudd& mgr, |
||||
|
int verbosity) |
||||
|
{ |
||||
|
if (verbosity) cout << "Entering testBdd3\n"; |
||||
|
vector<BDD> x(6); |
||||
|
for (int i = 0; i < 6; i++) { |
||||
|
x[i] = mgr.bddVar(i); |
||||
|
} |
||||
|
|
||||
|
BDD G = x[4] + !x[5]; |
||||
|
BDD H = x[4] * x[5]; |
||||
|
BDD E = x[3].Ite(G,!x[5]); |
||||
|
BDD F = x[3] + !H; |
||||
|
BDD D = x[2].Ite(F,!H); |
||||
|
BDD C = x[2].Ite(E,!F); |
||||
|
BDD B = x[1].Ite(C,!F); |
||||
|
BDD A = x[0].Ite(B,!D); |
||||
|
BDD f = !A; |
||||
|
if (verbosity) cout << "f"; f.print(6,verbosity); |
||||
|
|
||||
|
BDD f1 = f.RemapUnderApprox(6); |
||||
|
if (verbosity) cout << "f1"; f1.print(6,verbosity); |
||||
|
if (verbosity) |
||||
|
cout << "f1 is" << (f1 <= f ? "" : " not") << " less than or equal to f\n"; |
||||
|
|
||||
|
BDD g; |
||||
|
BDD h; |
||||
|
f.GenConjDecomp(&g,&h); |
||||
|
if (verbosity) { |
||||
|
cout << "g"; g.print(6,verbosity); |
||||
|
cout << "h"; h.print(6,verbosity); |
||||
|
cout << "g * h " << (g * h == f ? "==" : "!=") << " f\n"; |
||||
|
} |
||||
|
|
||||
|
} // testBdd3
|
||||
|
|
||||
|
|
||||
|
/**Function********************************************************************
|
||||
|
|
||||
|
Synopsis [Test cover manipulation with BDDs and ZDDs.] |
||||
|
|
||||
|
Description [Test cover manipulation with BDDs and ZDDs. The |
||||
|
function returns void because it relies on the error handling done by |
||||
|
the interface. The default error handler causes program |
||||
|
termination. This function builds the BDDs for a transformed adder: |
||||
|
one in which the inputs are transformations of the original |
||||
|
inputs. It then creates ZDDs for the covers from the BDDs.] |
||||
|
|
||||
|
SideEffects [May create BDD and ZDD variables in the manager.] |
||||
|
|
||||
|
SeeAlso [testZdd] |
||||
|
|
||||
|
******************************************************************************/ |
||||
|
static void |
||||
|
testZdd2( |
||||
|
Cudd& mgr, |
||||
|
int verbosity) |
||||
|
{ |
||||
|
if (verbosity) cout << "Entering testZdd2\n"; |
||||
|
int N = 3; // number of bits
|
||||
|
// Create variables.
|
||||
|
vector<BDD> a(N); |
||||
|
vector<BDD> b(N); |
||||
|
vector<BDD> c(N+1); |
||||
|
for (int i = 0; i < N; i++) { |
||||
|
a[N-1-i] = mgr.bddVar(2*i); |
||||
|
b[N-1-i] = mgr.bddVar(2*i+1); |
||||
|
} |
||||
|
c[0] = mgr.bddVar(2*N); |
||||
|
// Build functions.
|
||||
|
vector<BDD> s(N); |
||||
|
for (int i = 0; i < N; i++) { |
||||
|
s[i] = a[i].Xnor(c[i]); |
||||
|
c[i+1] = a[i].Ite(b[i],c[i]); |
||||
|
} |
||||
|
|
||||
|
// Create array of outputs and print it.
|
||||
|
vector<BDD> p(N+1); |
||||
|
for (int i = 0; i < N; i++) { |
||||
|
p[i] = s[i]; |
||||
|
} |
||||
|
p[N] = c[N]; |
||||
|
if (verbosity) { |
||||
|
for (size_t i = 0; i < p.size(); i++) { |
||||
|
cout << "p[" << i << "]"; p[i].print(2*N+1,verbosity); |
||||
|
} |
||||
|
} |
||||
|
const char* onames[] = {"s0", "s1", "s2", "c3"}; |
||||
|
if (verbosity) { |
||||
|
const char* inames[] = {"a2", "b2", "a1", "b1", "a0", "b0", "c0"}; |
||||
|
mgr.DumpDot(p, (char **)inames,(char **)onames); |
||||
|
} |
||||
|
|
||||
|
// Create ZDD variables and build ZDD covers from BDDs.
|
||||
|
mgr.zddVarsFromBddVars(2); |
||||
|
vector<ZDD> z(N+1); |
||||
|
for (int i = 0; i < N+1; i++) { |
||||
|
ZDD temp; |
||||
|
BDD dummy = p[i].zddIsop(p[i],&temp); |
||||
|
z[i] = temp; |
||||
|
} |
||||
|
|
||||
|
// Print out covers.
|
||||
|
if (verbosity) { |
||||
|
for (size_t i = 0; i < z.size(); i++) { |
||||
|
cout << "z[" << i << "]"; z[i].print(4*N+2,verbosity); |
||||
|
} |
||||
|
for (size_t i = 0; i < z.size(); i++) { |
||||
|
cout << "z[" << i << "]\n"; z[i].PrintCover(); |
||||
|
} |
||||
|
const char* znames[] = {"a2+", "a2-", "b2+", "b2-", "a1+", "a1-", "b1+", |
||||
|
"b1-", "a0+", "a0-", "b0+", "b0-", "c0+", "c0-"}; |
||||
|
mgr.DumpDot(z, (char **)znames,(char **)onames); |
||||
|
} |
||||
|
|
||||
|
} // testZdd2
|
||||
|
|
||||
|
|
||||
|
/**Function********************************************************************
|
||||
|
|
||||
|
Synopsis [Test transfer between BDD managers.] |
||||
|
|
||||
|
Description [Test transfer between BDD managers. The |
||||
|
function returns void because it relies on the error handling done by |
||||
|
the interface. The default error handler causes program |
||||
|
termination.] |
||||
|
|
||||
|
SideEffects [May create BDD variables in the manager.] |
||||
|
|
||||
|
SeeAlso [testBdd testBdd2 testBdd3 testBdd5] |
||||
|
|
||||
|
******************************************************************************/ |
||||
|
static void |
||||
|
testBdd4( |
||||
|
Cudd& mgr, |
||||
|
int verbosity) |
||||
|
{ |
||||
|
if (verbosity) cout << "Entering testBdd4\n"; |
||||
|
BDD x = mgr.bddVar(0); |
||||
|
BDD y = mgr.bddVar(1); |
||||
|
BDD z = mgr.bddVar(2); |
||||
|
|
||||
|
BDD f = !x * !y * !z + x * y; |
||||
|
if (verbosity) cout << "f"; f.print(3,verbosity); |
||||
|
|
||||
|
Cudd otherMgr(0,0); |
||||
|
BDD g = f.Transfer(otherMgr); |
||||
|
if (verbosity) cout << "g"; g.print(3,verbosity); |
||||
|
|
||||
|
BDD h = g.Transfer(mgr); |
||||
|
if (verbosity) |
||||
|
cout << "f and h are" << (f == h ? "" : " not") << " identical\n"; |
||||
|
|
||||
|
} // testBdd4
|
||||
|
|
||||
|
|
||||
|
|
||||
|
/**Function********************************************************************
|
||||
|
|
||||
|
Synopsis [Test maximal expansion of cubes.] |
||||
|
|
||||
|
Description [Test maximal expansion of cubes. The function returns |
||||
|
void because it relies on the error handling done by the interface. |
||||
|
The default error handler causes program termination.] |
||||
|
|
||||
|
SideEffects [May create BDD variables in the manager.] |
||||
|
|
||||
|
SeeAlso [testBdd testBdd2 testBdd3 testBdd4] |
||||
|
|
||||
|
******************************************************************************/ |
||||
|
static void |
||||
|
testBdd5( |
||||
|
Cudd& mgr, |
||||
|
int verbosity) |
||||
|
{ |
||||
|
if (verbosity) cout << "Entering testBdd5\n"; |
||||
|
vector<BDD> x; |
||||
|
x.reserve(4); |
||||
|
for (int i = 0; i < 4; i++) { |
||||
|
x.push_back(mgr.bddVar(i)); |
||||
|
} |
||||
|
const char* inames[] = {"a", "b", "c", "d"}; |
||||
|
BDD f = (x[1] & x[3]) | (x[0] & !x[2] & x[3]) | (!x[0] & x[1] & !x[2]); |
||||
|
BDD lb = x[1] & !x[2] & x[3]; |
||||
|
BDD ub = x[3]; |
||||
|
BDD primes = lb.MaximallyExpand(ub,f); |
||||
|
assert(primes == (x[1] & x[3])); |
||||
|
BDD lprime = primes.LargestPrimeUnate(lb); |
||||
|
assert(lprime == primes); |
||||
|
if (verbosity) { |
||||
|
const char * onames[] = {"lb", "ub", "f", "primes", "lprime"}; |
||||
|
vector<BDD> z; |
||||
|
z.reserve(5); |
||||
|
z.push_back(lb); |
||||
|
z.push_back(ub); |
||||
|
z.push_back(f); |
||||
|
z.push_back(primes); |
||||
|
z.push_back(lprime); |
||||
|
mgr.DumpDot(z, (char **)inames, (char **)onames); |
||||
|
cout << "primes(1)"; primes.print(4,verbosity); |
||||
|
} |
||||
|
|
||||
|
lb = !x[0] & x[2] & x[3]; |
||||
|
primes = lb.MaximallyExpand(ub,f); |
||||
|
assert(primes == mgr.bddZero()); |
||||
|
if (verbosity) { |
||||
|
cout << "primes(2)"; primes.print(4,verbosity); |
||||
|
} |
||||
|
|
||||
|
lb = x[0] & !x[2] & x[3]; |
||||
|
primes = lb.MaximallyExpand(ub,f); |
||||
|
assert(primes == lb); |
||||
|
lprime = primes.LargestPrimeUnate(lb); |
||||
|
assert(lprime == primes); |
||||
|
if (verbosity) { |
||||
|
cout << "primes(3)"; primes.print(4,verbosity); |
||||
|
} |
||||
|
|
||||
|
lb = !x[0] & x[1] & !x[2] & x[3]; |
||||
|
ub = mgr.bddOne(); |
||||
|
primes = lb.MaximallyExpand(ub,f); |
||||
|
assert(primes == ((x[1] & x[3]) | (!x[0] & x[1] & !x[2]))); |
||||
|
lprime = primes.LargestPrimeUnate(lb); |
||||
|
assert(lprime == (x[1] & x[3])); |
||||
|
if (verbosity) { |
||||
|
cout << "primes(4)"; primes.print(4,1); primes.PrintCover(); |
||||
|
} |
||||
|
|
||||
|
ub = !x[0] & x[3]; |
||||
|
primes = lb.MaximallyExpand(ub,f); |
||||
|
assert(primes == (!x[0] & x[1] & x[3])); |
||||
|
lprime = primes.LargestPrimeUnate(lb); |
||||
|
assert(lprime == primes); |
||||
|
if (verbosity) { |
||||
|
cout << "primes(5)"; primes.print(4,verbosity); |
||||
|
} |
||||
|
|
||||
|
} // testBdd5
|
||||
Write
Preview
Loading…
Cancel
Save
Reference in new issue