<!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN">
<html><head><meta http-equiv="Content-Type" content="text/html;charset=UTF-8">
<title>PolyBoRi: extrafwd.h Source File</title>
<link href="tabs.css" rel="stylesheet" type="text/css">
<link href="doxygen.css" rel="stylesheet" type="text/css">
</head><body>
<!-- Generated by Doxygen 1.5.9 -->
<div class="navigation" id="top">
<div class="tabs">
<ul>
<li><a href="index.html"><span>Main Page</span></a></li>
<li><a href="pages.html"><span>Related Pages</span></a></li>
<li><a href="namespaces.html"><span>Namespaces</span></a></li>
<li><a href="annotated.html"><span>Classes</span></a></li>
<li class="current"><a href="files.html"><span>Files</span></a></li>
</ul>
</div>
<div class="tabs">
<ul>
<li><a href="files.html"><span>File List</span></a></li>
<li><a href="globals.html"><span>File Members</span></a></li>
</ul>
</div>
<h1>extrafwd.h</h1><a href="extrafwd_8h.html">Go to the documentation of this file.</a><div class="fragment"><pre class="fragment"><a name="l00001"></a>00001 <span class="comment">/* Copyright (c) 2005-2007 by The PolyBoRi Team */</span>
<a name="l00002"></a>00002
<a name="l00003"></a>00003 <span class="preprocessor">#ifndef EXTRA_FWD_HEADER</span>
<a name="l00004"></a>00004 <span class="preprocessor"></span><span class="preprocessor">#define EXTRA_FWD_HEADER</span>
<a name="l00005"></a>00005 <span class="preprocessor"></span><span class="preprocessor">#include <cudd.h></span>
<a name="l00006"></a>00006
<a name="l00007"></a>00007 <span class="keyword">extern</span> <span class="stringliteral">"C"</span>{
<a name="l00008"></a>00008 <span class="comment">/* the result of this operation is primes contained in the product of cubes */</span>
<a name="l00009"></a>00009 <span class="keyword">extern</span> DdNode * <a class="code" href="extrafwd_8h.html#f8d9c379781ea6cb476db711b5d98c0e">Extra_zddPrimeProduct</a>( DdManager *dd, DdNode * f, DdNode * g );
<a name="l00010"></a>00010
<a name="l00011"></a>00011 <span class="comment">/* an alternative implementation of the cover product */</span>
<a name="l00012"></a>00012 <span class="keyword">extern</span> DdNode * <a class="code" href="extrafwd_8h.html#1500fdd30ef03a7e1a78865a82ea1388">Extra_zddProductAlt</a>( DdManager *dd, DdNode * f, DdNode * g );
<a name="l00013"></a>00013
<a name="l00014"></a>00014 <span class="comment">/* returns the set of cubes pair-wise unate with the given cube */</span>
<a name="l00015"></a>00015 <span class="keyword">extern</span> DdNode * <a class="code" href="extrafwd_8h.html#9c486dd36b062d1ff4e2d194054cc48e">Extra_zddCompatible</a>( DdManager * dd, DdNode * zCover, DdNode * zCube );
<a name="l00016"></a>00016
<a name="l00017"></a>00017 <span class="comment">/* a wrapper for the call to Extra_zddIsop() */</span>
<a name="l00018"></a>00018 <span class="keyword">extern</span> DdNode * <a class="code" href="extrafwd_8h.html#5c633bcdfd5a636d92c273deff792217">Extra_zddIsopCover</a>( DdManager * dd, DdNode * F1, DdNode * F12 );
<a name="l00019"></a>00019 <span class="comment">/* a wrapper for the call to Extra_zddIsopCover() and Extra_zddPrintCover() */</span>
<a name="l00020"></a>00020 <span class="keyword">extern</span> <span class="keywordtype">void</span> <a class="code" href="extrafwd_8h.html#5c9a266a065d67a6b88dc87fecc77c02">Extra_zddIsopPrintCover</a>( DdManager * dd, DdNode * F1, DdNode * F12 );
<a name="l00021"></a>00021 <span class="comment">/* a simple cover computation (not ISOP) */</span>
<a name="l00022"></a>00022 <span class="keyword">extern</span> DdNode * <a class="code" href="extrafwd_8h.html#395fa276104491f1197fa840715abcba">Extra_zddSimplify</a>( DdManager * dd, DdNode * F1, DdNode * F12 );
<a name="l00023"></a>00023
<a name="l00024"></a>00024 <span class="comment">/* an alternative ISOP cover computation (faster than Extra_zddIsop()) */</span>
<a name="l00025"></a>00025 <span class="keyword">extern</span> DdNode * <a class="code" href="extrafwd_8h.html#4fdaf09bce43defc01483e16a44ece0e">Extra_zddIsopCoverAlt</a>( DdManager * dd, DdNode * F1, DdNode * F12 );
<a name="l00026"></a>00026
<a name="l00027"></a>00027 <span class="comment">/* count the number of cubes in the ISOP without building the ISOP as a ZDD */</span>
<a name="l00028"></a>00028 <span class="keyword">extern</span> <span class="keywordtype">int</span> <a class="code" href="extrafwd_8h.html#6cacec7ef13bff3b5e361a9f4329d919">Extra_zddIsopCubeNum</a>( DdManager * dd, DdNode * F1, DdNode * F12 );
<a name="l00029"></a>00029
<a name="l00030"></a>00030
<a name="l00031"></a>00031 <span class="comment">/* computes the disjoint cube cover produced by the bdd paths */</span>
<a name="l00032"></a>00032 <span class="keyword">extern</span> DdNode * <a class="code" href="extrafwd_8h.html#ecd476bf383c11c00f6b2a869a6aeff7">Extra_zddDisjointCover</a>( DdManager * dd, DdNode * F );
<a name="l00033"></a>00033 <span class="comment">/* performs resolution on the set of clauses (S) w.r.t. variables in zdd Vars */</span>
<a name="l00034"></a>00034 <span class="keyword">extern</span> DdNode * <a class="code" href="extrafwd_8h.html#d41a226092761e6c994326b8f3957b6d">Extra_zddResolve</a>( DdManager * dd, DdNode * S, DdNode * Vars );
<a name="l00035"></a>00035 <span class="comment">/* cubes from zC that are not contained by cubes from zD over area bA */</span>
<a name="l00036"></a>00036 <span class="keyword">extern</span> DdNode * <a class="code" href="extrafwd_8h.html#75147a8057b7cc6d92f71dd8e0af0949">Extra_zddNotContainedCubesOverArea</a>( DdManager * dd, DdNode * zC, DdNode * zD, DdNode * bA );
<a name="l00037"></a>00037 <span class="keyword">extern</span> DdNode * <a class="code" href="extrafwd_8h.html#abb6706d45c584fd9ecaa6f7c44d4e96">extraZddNotContainedCubesOverArea</a>( DdManager * dd, DdNode * zC, DdNode * zD, DdNode * bA );
<a name="l00038"></a>00038 <span class="comment">/* finds cofactors of the cover w.r.t. the top-most variable without creating new nodes */</span>
<a name="l00039"></a>00039 <span class="comment">/* selects one cube from a ZDD representing the cube cover */</span>
<a name="l00040"></a>00040 <span class="keyword">extern</span> DdNode * <a class="code" href="extrafwd_8h.html#b8d8c9ae83455ac549acdce69ef872c2">Extra_zddSelectOneCube</a>( DdManager * dd, DdNode * zS );
<a name="l00041"></a>00041
<a name="l00042"></a>00042 <span class="comment">/* selects one subset from a ZDD representing the set of subsets */</span>
<a name="l00043"></a>00043 <span class="keyword">extern</span> DdNode * <a class="code" href="extrafwd_8h.html#bee810dfabd5d9fcb58e62662475f685">Extra_zddSelectOneSubset</a>( DdManager * dd, DdNode * zS );
<a name="l00044"></a>00044
<a name="l00045"></a>00045 <span class="comment">/* checks unateness of the cover */</span>
<a name="l00046"></a>00046 <span class="keyword">extern</span> <span class="keywordtype">int</span> <a class="code" href="extrafwd_8h.html#3e927fd07b4a63887004037e30a0c921">Extra_zddCheckUnateness</a>( DdManager * dd, DdNode * zCover );
<a name="l00047"></a>00047 <span class="comment">/* computes the BDD of the area covered by the max number of cubes in a ZDD. */</span>
<a name="l00048"></a>00048 <span class="keyword">extern</span> DdNode * <a class="code" href="extrafwd_8h.html#f4202b181d61261800e18128eea5c18f">Extra_zddGetMostCoveredArea</a>( DdManager * dd, DdNode * zC, <span class="keywordtype">int</span> * nOverlaps );
<a name="l00049"></a>00049
<a name="l00050"></a>00050
<a name="l00051"></a>00051 <span class="comment">/*=== extraZddExor.c ==============================================================*/</span>
<a name="l00052"></a>00052
<a name="l00053"></a>00053 <span class="comment">/* computes the Exclusive-OR-type union of two cube sets */</span>
<a name="l00054"></a>00054 <span class="keyword">extern</span> DdNode * <a class="code" href="extrafwd_8h.html#b3e9d664e7fbbb038b0427a031d883ca">Extra_zddUnionExor</a>( DdManager * dd, DdNode * S, DdNode * T );
<a name="l00055"></a>00055 <span class="comment">/* given two sets of cubes, computes the set of pair-wise supercubes */</span>
<a name="l00056"></a>00056 <span class="keyword">extern</span> DdNode * <a class="code" href="extrafwd_8h.html#1c200309b6ca1abe43ac36de9ab8da2a">Extra_zddSupercubes</a>( DdManager *dd, DdNode * zA, DdNode * zB );
<a name="l00057"></a>00057
<a name="l00058"></a>00058 <span class="comment">/* selects cubes from zA that have a distance-1 cube in zB */</span>
<a name="l00059"></a>00059 <span class="keyword">extern</span> DdNode * <a class="code" href="extrafwd_8h.html#cd9f96060f6796df31669989e15d626f">Extra_zddSelectDist1Cubes</a>( DdManager *dd, DdNode * zA, DdNode * zB );
<a name="l00060"></a>00060
<a name="l00061"></a>00061 <span class="comment">/* computes the set of fast ESOP covers for the multi-output function */</span>
<a name="l00062"></a>00062 <span class="keyword">extern</span> <span class="keywordtype">int</span> <a class="code" href="extrafwd_8h.html#2e84e3da79a7f6007def48351f6663b7">Extra_zddFastEsopCoverArray</a>( DdManager * dd, DdNode ** bFs, DdNode ** zCs, <span class="keywordtype">int</span> nFs );
<a name="l00063"></a>00063 <span class="comment">/* computes a fast ESOP cover for the single-output function */</span>
<a name="l00064"></a>00064 <span class="comment">//extern DdNode * Extra_zddFastEsopCover( DdManager * dd, DdNode * bF, st_table * Visited, int * pnCubes );</span>
<a name="l00065"></a>00065
<a name="l00066"></a>00066 <span class="comment">/*=== extraZddFactor.c ================================================================*/</span>
<a name="l00067"></a>00067
<a name="l00068"></a>00068 <span class="comment">/* counting the number of literals in the factored form */</span>
<a name="l00069"></a>00069 <span class="keyword">extern</span> <span class="keywordtype">int</span> <a class="code" href="extrafwd_8h.html#43c87ee3f774141fdfbd478ad91b8ac7">Extra_bddFactoredFormLiterals</a>( DdManager * dd, DdNode * bOnSet, DdNode * bOnDcSet );
<a name="l00070"></a>00070 <span class="keyword">extern</span> DdNode * <a class="code" href="extrafwd_8h.html#b7306ecc95b68ea6b3fbe65a394e1d22">Extra_zddFactoredFormLiterals</a>( DdManager * dd, DdNode * zCover );
<a name="l00071"></a>00071 <span class="keyword">extern</span> DdNode * <a class="code" href="extrafwd_8h.html#28def03210e585b5e2a16b5bbd9b29b0">Extra_zddLFLiterals</a>( DdManager * dd, DdNode * zCover, DdNode * zCube );
<a name="l00072"></a>00072 <span class="comment">/* computing a quick divisor */</span>
<a name="l00073"></a>00073 <span class="keyword">extern</span> DdNode * <a class="code" href="extrafwd_8h.html#e5cd1b65cba07efc3955f2f261ae5c78">Extra_zddQuickDivisor</a>( DdManager * dd, DdNode * zCover );
<a name="l00074"></a>00074 <span class="keyword">extern</span> DdNode * <a class="code" href="extrafwd_8h.html#9d4f77a28b7a55efe4ea26851aa79ef6">Extra_zddLevel0Kernel</a>( DdManager * dd, DdNode * zCover );
<a name="l00075"></a>00075 <span class="comment">/* division with quotient and remainder */</span>
<a name="l00076"></a>00076 <span class="keyword">extern</span> <span class="keywordtype">void</span> <a class="code" href="extrafwd_8h.html#7eb4c52f8b785458a6e148a13e9b4db6">Extra_zddDivision</a>( DdManager * dd, DdNode * zCover, DdNode * zDiv, DdNode ** zQuo, DdNode ** zRem );
<a name="l00077"></a>00077 <span class="comment">/* the common cube */</span>
<a name="l00078"></a>00078 <span class="keyword">extern</span> DdNode * <a class="code" href="extrafwd_8h.html#6737cc65abb6a63c5d28bc3aa7fc5166">Extra_zddCommonCubeFast</a>( DdManager * dd, DdNode * zCover );
<a name="l00079"></a>00079 <span class="comment">/* the cube of literals that occur more than once */</span>
<a name="l00080"></a>00080 <span class="keyword">extern</span> DdNode * <a class="code" href="extrafwd_8h.html#75a9ed59a874556c964c3460252ffc46">Extra_zddMoreThanOnceCubeFast</a>( DdManager * dd, DdNode * zCover );
<a name="l00081"></a>00081 <span class="comment">/* making the cover cube-free */</span>
<a name="l00082"></a>00082 <span class="keyword">extern</span> DdNode * <a class="code" href="extrafwd_8h.html#8e6cfced25e324d4d06f5e8fe6efa16f">Extra_zddMakeCubeFree</a>( DdManager * dd, DdNode * zCover, <span class="keywordtype">int</span> iZVar );
<a name="l00083"></a>00083 <span class="comment">/* testing whether the cover is cube-free */</span>
<a name="l00084"></a>00084 <span class="keyword">extern</span> <span class="keywordtype">int</span> <a class="code" href="extrafwd_8h.html#582bb0b9c4c265b9a557fe8c9d01c19e">Extra_zddTestCubeFree</a>( DdManager * dd, DdNode * zCover );
<a name="l00085"></a>00085
<a name="l00086"></a>00086 <span class="comment">/* counts the number of literals in the simple cover */</span>
<a name="l00087"></a>00087 <span class="keyword">extern</span> <span class="keywordtype">int</span> <a class="code" href="extrafwd_8h.html#c34bf22b6adf7424b275bd140c3ed78f">Extra_zddCountLiteralsSimple</a>( DdManager * dd, DdNode * zCover );
<a name="l00088"></a>00088 <span class="comment">/* tests whether the cover contains more than one cube */</span>
<a name="l00089"></a>00089 <span class="keyword">extern</span> <span class="keywordtype">int</span> <a class="code" href="extrafwd_8h.html#9c34c7bb4ffc35a4eb461f1950f7fa6b">Extra_zddMoreThanOneCube</a>( DdManager * dd, DdNode * zCover );
<a name="l00090"></a>00090 <span class="comment">/* the cube from levels */</span>
<a name="l00091"></a>00091 <span class="keyword">extern</span> DdNode * <a class="code" href="extrafwd_8h.html#c4813871ec3de362bbc553ec52eb7b4f">Extra_zddCombinationFromLevels</a>( DdManager * dd, <span class="keywordtype">int</span> * pLevels, <span class="keywordtype">int</span> nVars );
<a name="l00092"></a>00092 <span class="comment">/* determines common literals */</span>
<a name="l00093"></a>00093 <span class="keyword">extern</span> <span class="keywordtype">int</span> <a class="code" href="extrafwd_8h.html#5d9ab9fc6ba963b43bd2e8f7acee6041">Extra_zddCommonLiterals</a>( DdManager * dd, DdNode * zCover, <span class="keywordtype">int</span> iZVar, <span class="keywordtype">int</span> * pLevels, <span class="keywordtype">int</span> * pLiterals );
<a name="l00094"></a>00094 <span class="comment">/* determines the set of literals that occur more than once */</span>
<a name="l00095"></a>00095 <span class="keyword">extern</span> <span class="keywordtype">int</span> <a class="code" href="extrafwd_8h.html#e8fe33218700f240f80bf24f609c9773">Extra_zddMoreThanOneLiteralSet</a>( DdManager * dd, DdNode * zCover, <span class="keywordtype">int</span> StartLevel, <span class="keywordtype">int</span> * pVars, <span class="keywordtype">int</span> * pCounters );
<a name="l00096"></a>00096 <span class="comment">/* tests whether the given literal literal occurs more than once */</span>
<a name="l00097"></a>00097 <span class="keyword">extern</span> <span class="keywordtype">int</span> <a class="code" href="extrafwd_8h.html#7f01532ad1ab7d0f5124c56b8be96316">Extra_zddMoreThanOneLiteral</a>( DdManager * dd, DdNode * zCover, <span class="keywordtype">int</span> iZVar );
<a name="l00098"></a>00098
<a name="l00099"></a>00099
<a name="l00100"></a>00100 <span class="comment">/*=== extraZddGraph.c ==============================================================*/</span>
<a name="l00101"></a>00101
<a name="l00102"></a>00102 <span class="comment">/* construct the set of cliques */</span>
<a name="l00103"></a>00103 <span class="keyword">extern</span> DdNode * <a class="code" href="extrafwd_8h.html#16cf5c0503c5847d6c09c2014dadba03">Extra_zddCliques</a>( DdManager *dd, DdNode * G, <span class="keywordtype">int</span> fMaximal );
<a name="l00104"></a>00104 <span class="comment">/* construct the set of all maximal cliques */</span>
<a name="l00105"></a>00105 <span class="keyword">extern</span> DdNode * <a class="code" href="extrafwd_8h.html#eb806906235c96cd6913f8579eae92cb">Extra_zddMaxCliques</a>( DdManager *dd, DdNode * G );
<a name="l00106"></a>00106 <span class="comment">/* incrementally contruct the set of cliques */</span>
<a name="l00107"></a>00107 <span class="keyword">extern</span> DdNode * <a class="code" href="extrafwd_8h.html#7a0d1eb9b5d548d2f62fab85413897fe">Extra_zddIncremCliques</a>( DdManager *dd, DdNode * G, DdNode * C );
<a name="l00108"></a>00108
<a name="l00109"></a>00109
<a name="l00110"></a>00110
<a name="l00111"></a>00111
<a name="l00112"></a>00112
<a name="l00113"></a>00113 <span class="keyword">extern</span> DdNode * <a class="code" href="extrafwd_8h.html#8979862b6616d87fe3a64160fb741ad5">Extra_zddIsopCoverAllVars</a>( DdManager * dd, DdNode * F1, DdNode * F12 );
<a name="l00114"></a>00114
<a name="l00115"></a>00115
<a name="l00116"></a>00116 <span class="keyword">extern</span> DdNode * <a class="code" href="extrafwd_8h.html#f8a17150fc609b653f5f52defa59d9b0">Extra_zddIsopCoverUnateVars</a>( DdManager * dd, DdNode * F1, DdNode * F12 );
<a name="l00117"></a>00117
<a name="l00118"></a>00118
<a name="l00119"></a>00119 <span class="comment">/* computes an ISOP cover with a random ordering of variables */</span>
<a name="l00120"></a>00120 <span class="keyword">extern</span> DdNode * <a class="code" href="extrafwd_8h.html#c1884cff5015b56780231239a1f256a8">Extra_zddIsopCoverRandom</a>( DdManager * dd, DdNode * F1, DdNode * F12 );
<a name="l00121"></a>00121
<a name="l00122"></a>00122 <span class="keyword">extern</span> DdNode * <a class="code" href="extrafwd_8h.html#4f3392d80793502b3bd4ffb43bb38b29">Extra_zddIsopCoverReduced</a>( DdManager * dd, DdNode * F1, DdNode * F12 );
<a name="l00123"></a>00123
<a name="l00124"></a>00124
<a name="l00125"></a>00125 <span class="comment">/*=== extraZddLitCount.c ==============================================================*/</span>
<a name="l00126"></a>00126
<a name="l00127"></a>00127 <span class="comment">/* count the number of times each variable occurs in the combinations */</span>
<a name="l00128"></a>00128 <span class="keyword">extern</span> <span class="keywordtype">int</span> * <a class="code" href="extrafwd_8h.html#1eeb9b36f3926f2ccf528c78ec52bcf5">Extra_zddLitCount</a>( DdManager * dd, DdNode * Set );
<a name="l00129"></a>00129 <span class="comment">/* count the number of literals in one ZDD combination */</span>
<a name="l00130"></a>00130 <span class="keyword">extern</span> <span class="keywordtype">int</span> <a class="code" href="extrafwd_8h.html#3f369eaad4c936db28e51ec8d254639f">Extra_zddLitCountComb</a>( DdManager * dd, DdNode * zComb );
<a name="l00131"></a>00131
<a name="l00132"></a>00132 <span class="comment">/*=== extraZddMaxMin.c ==============================================================*/</span>
<a name="l00133"></a>00133
<a name="l00134"></a>00134 <span class="comment">/* maximal/minimimal */</span>
<a name="l00135"></a>00135 <span class="keyword">extern</span> DdNode * <a class="code" href="extrafwd_8h.html#8950b1faf2d917636c2ef91f6157316b">Extra_zddMaximal</a>( DdManager *dd, DdNode * S );
<a name="l00136"></a>00136
<a name="l00137"></a>00137 <span class="keyword">extern</span> DdNode * <a class="code" href="extrafwd_8h.html#30e18eedb4e5f94ebac27795208cbb8f">Extra_zddMinimal</a>( DdManager *dd, DdNode * S );
<a name="l00138"></a>00138
<a name="l00139"></a>00139 <span class="comment">/* maximal/minimal of the union of two sets of subsets */</span>
<a name="l00140"></a>00140 <span class="keyword">extern</span> DdNode * <a class="code" href="extrafwd_8h.html#ea9fc650a01272368e44d28b6f297e31">Extra_zddMaxUnion</a>( DdManager *dd, DdNode * S, DdNode * T );
<a name="l00141"></a>00141
<a name="l00142"></a>00142 <span class="keyword">extern</span> DdNode * <a class="code" href="extrafwd_8h.html#e7d99678784f53bcb2cda56d5e25bff7">Extra_zddMinUnion</a>( DdManager *dd, DdNode * S, DdNode * T );
<a name="l00143"></a>00143
<a name="l00144"></a>00144 <span class="comment">/* dot/cross products */</span>
<a name="l00145"></a>00145 <span class="keyword">extern</span> DdNode * <a class="code" href="extrafwd_8h.html#1192f3df8e54281288caf283245de4d5">Extra_zddDotProduct</a>( DdManager *dd, DdNode * S, DdNode * T );
<a name="l00146"></a>00146
<a name="l00147"></a>00147 <span class="keyword">extern</span> DdNode * <a class="code" href="extrafwd_8h.html#ce064e13d70faba96f8513f7e5746004">Extra_zddExorProduct</a>( DdManager *dd, DdNode * S, DdNode * T );
<a name="l00148"></a>00148
<a name="l00149"></a>00149 <span class="keyword">extern</span> DdNode * <a class="code" href="extrafwd_8h.html#f2d7d570b14afda8e8bc89e20e3b952f">Extra_zddCrossProduct</a>( DdManager *dd, DdNode * S, DdNode * T );
<a name="l00150"></a>00150
<a name="l00151"></a>00151 <span class="keyword">extern</span> DdNode * <a class="code" href="extrafwd_8h.html#34e6613c394a9b5fc3b824ca75662723">Extra_zddMaxDotProduct</a>( DdManager *dd, DdNode * S, DdNode * T );
<a name="l00152"></a>00152
<a name="l00153"></a>00153
<a name="l00154"></a>00154 <span class="comment">/*=== extraZddMisc.c ==============================================================*/</span>
<a name="l00155"></a>00155
<a name="l00156"></a>00156 <span class="comment">/* create the combination composed of a single ZDD variable */</span>
<a name="l00157"></a>00157 <span class="keyword">extern</span> DdNode * <a class="code" href="extrafwd_8h.html#af4480fb7697e6ad9d142276d9dfc30b">Extra_zddVariable</a>( DdManager * dd, <span class="keywordtype">int</span> iVar );
<a name="l00158"></a>00158 <span class="comment">/* build a ZDD for a combination of variables */</span>
<a name="l00159"></a>00159 <span class="keyword">extern</span> DdNode * <a class="code" href="extrafwd_8h.html#65faa0f1312d61b68790ed4b72226f20">Extra_zddCombination</a>( DdManager *dd, <span class="keywordtype">int</span>* VarValues, <span class="keywordtype">int</span> nVars );
<a name="l00160"></a>00160
<a name="l00161"></a>00161 <span class="comment">/* the set of all possible combinations of the given set of variables */</span>
<a name="l00162"></a>00162 <span class="keyword">extern</span> DdNode * <a class="code" href="extrafwd_8h.html#a77b31754d0ee042394aaaa5aadb5088">Extra_zddUniverse</a>( DdManager * dd, DdNode * VarSet );
<a name="l00163"></a>00163
<a name="l00164"></a>00164 <span class="comment">/* build the set of all tuples of K variables out of N */</span>
<a name="l00165"></a>00165 <span class="keyword">extern</span> DdNode * <a class="code" href="extrafwd_8h.html#a7bc51789cddc5d4969f28a87e32c3bb">Extra_zddTuples</a>( DdManager * dd, <span class="keywordtype">int</span> K, DdNode * zVarsN );
<a name="l00166"></a>00166
<a name="l00167"></a>00167 <span class="comment">/* build the set of all tuples of K variables out of N from the BDD cube */</span>
<a name="l00168"></a>00168 <span class="keyword">extern</span> DdNode * <a class="code" href="extrafwd_8h.html#ae96bf627f9b515ccde340baa124127e">Extra_zddTuplesFromBdd</a>( DdManager * dd, <span class="keywordtype">int</span> K, DdNode * bVarsN );
<a name="l00169"></a>00169
<a name="l00170"></a>00170 <span class="comment">/* convert the set of singleton combinations into one combination */</span>
<a name="l00171"></a>00171 <span class="keyword">extern</span> DdNode * <a class="code" href="extrafwd_8h.html#223d8d0f4f184c4d5fc7c33c89d766bb">Extra_zddSinglesToComb</a>( DdManager * dd, DdNode * Singles );
<a name="l00172"></a>00172
<a name="l00173"></a>00173 <span class="comment">/* returns the set of combinations containing the max/min number of elements */</span>
<a name="l00174"></a>00174 <span class="keyword">extern</span> DdNode * <a class="code" href="extrafwd_8h.html#65b8f43b71080a7fd974d24314a532ce">Extra_zddMaximum</a>( DdManager * dd, DdNode * S, <span class="keywordtype">int</span> * nVars );
<a name="l00175"></a>00175
<a name="l00176"></a>00176 <span class="keyword">extern</span> DdNode * <a class="code" href="extrafwd_8h.html#8231e634fcc310f5cb70d6adbe949533">Extra_zddMinimum</a>( DdManager * dd, DdNode * S, <span class="keywordtype">int</span> * nVars );
<a name="l00177"></a>00177
<a name="l00178"></a>00178 <span class="comment">/* returns the random set of k combinations of n elements with average density d */</span>
<a name="l00179"></a>00179 <span class="keyword">extern</span> DdNode * <a class="code" href="extrafwd_8h.html#084925cf77fb970b7b977268061bd802">Extra_zddRandomSet</a>( DdManager * dd, <span class="keywordtype">int</span> n, <span class="keywordtype">int</span> k, <span class="keywordtype">double</span> d );
<a name="l00180"></a>00180 <span class="comment">/* other utilities */</span>
<a name="l00181"></a>00181 <span class="keyword">extern</span> DdNode * <a class="code" href="extrafwd_8h.html#a88cabcbdab4ae78469d352f6e17a465">Extra_zddCoveredByArea</a>( DdManager *dd, DdNode * zC, DdNode * bA );
<a name="l00182"></a>00182
<a name="l00183"></a>00183 <span class="keyword">extern</span> DdNode * <a class="code" href="extrafwd_8h.html#4088013793209204dd2150415fa15156">Extra_zddNotCoveredByCover</a>( DdManager *dd, DdNode * zC, DdNode * zD );
<a name="l00184"></a>00184
<a name="l00185"></a>00185 <span class="keyword">extern</span> DdNode * <a class="code" href="extrafwd_8h.html#83354f268466c71a4b86fa19498b984a">Extra_zddOverlappingWithArea</a>( DdManager *dd, DdNode * zC, DdNode * bA );
<a name="l00186"></a>00186
<a name="l00187"></a>00187 <span class="keyword">extern</span> DdNode * <a class="code" href="extrafwd_8h.html#91057e84bb5622f552ed3d35da61026f">Extra_zddConvertToBdd</a>( DdManager *dd, DdNode * zC );
<a name="l00188"></a>00188
<a name="l00189"></a>00189 <span class="keyword">extern</span> DdNode * <a class="code" href="extrafwd_8h.html#c4227f652cc842756666c03cd6d4870f">Extra_zddConvertToBddUnate</a>( DdManager *dd, DdNode * zC );
<a name="l00190"></a>00190
<a name="l00191"></a>00191 <span class="keyword">extern</span> DdNode * <a class="code" href="extrafwd_8h.html#875c1f5453e35b86c3f116384d99ac6d">Extra_zddConvertEsopToBdd</a>( DdManager *dd, DdNode * zC );
<a name="l00192"></a>00192
<a name="l00193"></a>00193 <span class="keyword">extern</span> DdNode * <a class="code" href="extrafwd_8h.html#2184a1e6198c498791c3210c159e34a6">Extra_zddConvertToBddAndAdd</a>( DdManager *dd, DdNode * zC, DdNode * bA );
<a name="l00194"></a>00194
<a name="l00195"></a>00195 <span class="keyword">extern</span> DdNode * <a class="code" href="extrafwd_8h.html#edae91e69efb64b4d0b65038a2d61def">Extra_zddSingleCoveredArea</a>( DdManager *dd, DdNode * zC );
<a name="l00196"></a>00196
<a name="l00197"></a>00197 <span class="keyword">extern</span> DdNode * <a class="code" href="extrafwd_8h.html#787268baab2886f4ed4c275e901b5b5b">Extra_zddConvertBddCubeIntoZddCube</a>( DdManager *dd, DdNode * bCube );
<a name="l00198"></a>00198
<a name="l00199"></a>00199 <span class="comment">/*=== extraZddPermute.c ==============================================================*/</span>
<a name="l00200"></a>00200
<a name="l00201"></a>00201 <span class="comment">/* quantifications */</span>
<a name="l00202"></a>00202 <span class="keyword">extern</span> DdNode * <a class="code" href="extrafwd_8h.html#1adf8a98e7a481e980ab36ebce6841aa">Extra_zddExistAbstract</a>( DdManager *manager, DdNode * F, DdNode * cube );
<a name="l00203"></a>00203
<a name="l00204"></a>00204 <span class="comment">/* changes the value of several variables in the ZDD */</span>
<a name="l00205"></a>00205 <span class="keyword">extern</span> DdNode * <a class="code" href="extrafwd_8h.html#9028da4fd4298e49ea4359c876e12b9c">Extra_zddChangeVars</a>( DdManager *manager, DdNode * F, DdNode * cube );
<a name="l00206"></a>00206
<a name="l00207"></a>00207 <span class="comment">/* permutes variables in ZDD */</span>
<a name="l00208"></a>00208 <span class="keyword">extern</span> DdNode * <a class="code" href="extrafwd_8h.html#727ae5a2cb3dc9e98986ac3d85694f4f">Extra_zddPermute</a> ( DdManager *dd, DdNode * N, <span class="keywordtype">int</span> *permut );
<a name="l00209"></a>00209 <span class="comment">/* computes combinations in F with vars in Cube having the negative polarity */</span>
<a name="l00210"></a>00210 <span class="keyword">extern</span> DdNode * <a class="code" href="extrafwd_8h.html#3e3db6af3a432fb67d2d5f0299184c38">Extra_zddCofactor0</a>( DdManager * dd, DdNode * f, DdNode * cube );
<a name="l00211"></a>00211
<a name="l00212"></a>00212 <span class="comment">/* computes combinations in F with vars in Cube having the positive polarity */</span>
<a name="l00213"></a>00213 <span class="keyword">extern</span> DdNode * <a class="code" href="extrafwd_8h.html#1255f7b399f9366e1f83bbf6a206b627">Extra_zddCofactor1</a>( DdManager * dd, DdNode * f, DdNode * cube, <span class="keywordtype">int</span> fIncludeVars );
<a name="l00214"></a>00214
<a name="l00215"></a>00215
<a name="l00216"></a>00216 <span class="comment">/*=== extraZddSubSup.c ==============================================================*/</span>
<a name="l00217"></a>00217
<a name="l00218"></a>00218 <span class="comment">/* subset/supset operations */</span>
<a name="l00219"></a>00219 <span class="keyword">extern</span> DdNode * <a class="code" href="extrafwd_8h.html#e71887adf63ff82b71f5752b931c2b42">Extra_zddSubSet</a> ( DdManager *dd, DdNode * X, DdNode * Y );
<a name="l00220"></a>00220
<a name="l00221"></a>00221 <span class="keyword">extern</span> DdNode * <a class="code" href="extrafwd_8h.html#4d7756c43cdee777ac3b3c97974a991a">Extra_zddSupSet</a> ( DdManager *dd, DdNode * X, DdNode * Y );
<a name="l00222"></a>00222
<a name="l00223"></a>00223 <span class="keyword">extern</span> DdNode * <a class="code" href="extrafwd_8h.html#b9712400ad8d1cba47f8a333fe869701">Extra_zddNotSubSet</a>( DdManager *dd, DdNode * X, DdNode * Y );
<a name="l00224"></a>00224
<a name="l00225"></a>00225 <span class="keyword">extern</span> DdNode * <a class="code" href="extrafwd_8h.html#597a7afef797611efc0a9edc5dd2934a">Extra_zddNotSupSet</a>( DdManager *dd, DdNode * X, DdNode * Y );
<a name="l00226"></a>00226
<a name="l00227"></a>00227 <span class="keyword">extern</span> DdNode * <a class="code" href="extrafwd_8h.html#a6e3e46579bf8f3801ec956ca35a87a8">Extra_zddMaxNotSupSet</a>( DdManager *dd, DdNode * X, DdNode * Y );
<a name="l00228"></a>00228
<a name="l00229"></a>00229 <span class="comment">/* check whether the empty combination belongs to the set of subsets */</span>
<a name="l00230"></a>00230 <span class="keyword">extern</span> <span class="keywordtype">int</span> <a class="code" href="extrafwd_8h.html#1704f4ce5f572bdbd4af8cbb4cd997b4">Extra_zddEmptyBelongs</a> ( DdManager *dd, DdNode* zS );
<a name="l00231"></a>00231 <span class="comment">/* check whether the set consists of one subset only */</span>
<a name="l00232"></a>00232 <span class="keyword">extern</span> <span class="keywordtype">int</span> <a class="code" href="extrafwd_8h.html#ae127d1b9a9142b1246a92b982af5847">Extra_zddIsOneSubset</a>( DdManager *dd, DdNode* zS );
<a name="l00233"></a>00233
<a name="l00234"></a>00234 }
<a name="l00235"></a>00235
<a name="l00236"></a>00236
<a name="l00237"></a>00237 <span class="preprocessor">#endif</span>
</pre></div></div>
<hr size="1"><address style="text-align: right;"><small>Generated on Wed Sep 9 14:30:57 2009 for PolyBoRi by
<a href="http://www.doxygen.org/index.html">
<img src="doxygen.png" alt="doxygen" align="middle" border="0"></a> 1.5.9 </small></address>
</body>
</html>
distrib
>
Mandriva
>
2010.0
>
i586
>
media
>
contrib-release
>
by-pkgid
>
a24e1a39141f9b4ca49bd1e2e23a54ba
>
files
>
644
