Functions for the solution of satisfiability related problems. More...
#include "util.h"
#include "cuddInt.h"
Data Structures | |
struct | cuddPathPair |
Type of item stored in memoization table. More... | |
Defines | |
#define | DD_BIGGY 100000000 |
#define | WEIGHT(weight, col) ((weight) == NULL ? 1 : weight[col]) |
Functions | |
DdNode * | Cudd_Eval (DdManager *dd, DdNode *f, int *inputs) |
Returns the value of a DD for a given variable assignment. | |
DdNode * | Cudd_ShortestPath (DdManager *manager, DdNode *f, int *weight, int *support, int *length) |
Finds a shortest path in a DD. | |
DdNode * | Cudd_LargestCube (DdManager *manager, DdNode *f, int *length) |
Finds a largest cube in a DD. | |
int | Cudd_ShortestLength (DdManager *manager, DdNode *f, int *weight) |
Find the length of the shortest path(s) in a DD. | |
DdNode * | Cudd_Decreasing (DdManager *dd, DdNode *f, int i) |
Checks whether a BDD is negative unate in a variable. | |
DdNode * | Cudd_Increasing (DdManager *dd, DdNode *f, int i) |
Checks whether a BDD is positive unate in a variable. | |
int | Cudd_EquivDC (DdManager *dd, DdNode *F, DdNode *G, DdNode *D) |
Tells whether F and G are identical wherever D is 0. | |
int | Cudd_bddLeqUnless (DdManager *dd, DdNode *f, DdNode *g, DdNode *D) |
Tells whether f is less than of equal to G unless D is 1. | |
int | Cudd_EqualSupNorm (DdManager *dd, DdNode *f, DdNode *g, CUDD_VALUE_TYPE tolerance, int pr) |
Compares two ADDs for equality within tolerance. | |
DdNode * | Cudd_bddMakePrime (DdManager *dd, DdNode *cube, DdNode *f) |
Expands cube to a prime implicant of f. | |
DdNode * | Cudd_bddMaximallyExpand (DdManager *dd, DdNode *lb, DdNode *ub, DdNode *f) |
Expands lb to prime implicants of (f and ub). | |
DdNode * | Cudd_bddLargestPrimeUnate (DdManager *dd, DdNode *f, DdNode *phaseBdd) |
Find a largest prime implicant of a unate function. | |
DdNode * | cuddBddMakePrime (DdManager *dd, DdNode *cube, DdNode *f) |
Performs the recursive step of Cudd_bddMakePrime. | |
static enum st_retval | freePathPair (void *key, void *value, void *arg) |
Frees the entries of the visited symbol table. | |
static cuddPathPair | getShortest (DdManager *dd, DdNode *root, int *cost, int *support, st_table *visited) |
Finds the length of the shortest path(s) in a DD. | |
static DdNode * | getPath (DdManager *manager, st_table *visited, DdNode *f, int *weight, int cost) |
Build a BDD for a shortest path of f. | |
static cuddPathPair | getLargest (DdManager *dd, DdNode *root, st_table *visited) |
Finds the size of the largest cube(s) in a DD. | |
static DdNode * | getCube (DdManager *manager, st_table *visited, DdNode *f, int cost) |
Build a BDD for a largest cube of f. | |
static DdNode * | ddBddMaximallyExpand (DdManager *dd, DdNode *lb, DdNode *ub, DdNode *f) |
Performs the recursive step of Cudd_bddMaximallyExpand. | |
static int | ddBddShortestPathUnate (DdManager *dd, DdNode *f, int *phases, st_table *table) |
Performs shortest path computation on a unate function. | |
static DdNode * | ddGetLargestCubeUnate (DdManager *dd, DdNode *f, int *phases, st_table *table) |
Extracts largest prime of a unate function. |
Functions for the solution of satisfiability related problems.
Copyright (c) 1995-2015, 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.
Find a largest prime implicant of a unate function.
The behavior is undefined if f is not unate. The third argument is used to determine whether f is unate positive (increasing) or negative (decreasing) in each of the variables in its support.
dd | manager | |
f | unate function | |
phaseBdd | cube of the phases |
Tells whether f is less than of equal to G unless D is 1.
f, g, and D are BDDs. No new nodes are created.
Expands cube to a prime implicant of f.
dd | manager | |
cube | cube to be expanded | |
f | function of which the cube is to be made a prime |
Expands lb to prime implicants of (f and ub).
Expands lb to all prime implicants of (f and ub) that contain lb. Assumes that lb is contained in ub.
dd | manager | |
lb | cube to be expanded | |
ub | upper bound cube | |
f | function against which to expand |
Checks whether a BDD is negative unate in a variable.
Determines whether the function represented by BDD f is negative unate (monotonic decreasing) in variable i. This function does not generate any new nodes.
int Cudd_EqualSupNorm | ( | DdManager * | dd, | |
DdNode * | f, | |||
DdNode * | g, | |||
CUDD_VALUE_TYPE | tolerance, | |||
int | pr | |||
) |
Compares two ADDs for equality within tolerance.
Two ADDs are reported to be equal if the maximum difference between them (the sup norm of their difference) is less than or equal to the tolerance parameter. If parameter pr
is positive the first failure is reported to the standard output.
dd | manager | |
f | first ADD | |
g | second ADD | |
tolerance | maximum allowed difference | |
pr | verbosity level |
Tells whether F and G are identical wherever D is 0.
F and G are either two ADDs or two BDDs. D is either a 0-1 ADD or a BDD. No new nodes are created.
Returns the value of a DD for a given variable assignment.
The variable assignment is passed in an array of int's, that should specify a zero or a one for each variable in the support of the function.
Checks whether a BDD is positive unate in a variable.
Determines whether the function represented by BDD f is positive unate (monotonic increasing) in variable i. It is based on Cudd_Decreasing and the fact that f is monotonic increasing in i if and only if its complement is monotonic decreasing in i.
Finds a largest cube in a DD.
f is the DD we want to get the largest cube for. The problem is translated into the one of finding a shortest path in f, when both THEN and ELSE arcs are assumed to have unit length. This yields a largest cube in the disjoint cover corresponding to the DD. Therefore, it is not necessarily the largest implicant of f.
Find the length of the shortest path(s) in a DD.
f is the DD we want to get the shortest path for; weight\[i\] is the weight of the THEN edge coming from the node whose index is i. All ELSE edges have 0 weight.
DdNode* Cudd_ShortestPath | ( | DdManager * | manager, | |
DdNode * | f, | |||
int * | weight, | |||
int * | support, | |||
int * | length | |||
) |
Finds a shortest path in a DD.
f is the DD we want to get the shortest path for; weight\[i\] is the weight of the THEN arc coming from the node whose index is i. If weight is NULL, then unit weights are assumed for all THEN arcs. All ELSE arcs have 0 weight. If non-NULL, both weight and support should point to arrays with at least as many entries as there are variables in the manager.
Performs the recursive step of Cudd_bddMakePrime.
dd | manager | |
cube | cube to be expanded | |
f | function of which the cube is to be made a prime |
static DdNode* ddBddMaximallyExpand | ( | DdManager * | dd, | |
DdNode * | lb, | |||
DdNode * | ub, | |||
DdNode * | f | |||
) | [static] |
Performs the recursive step of Cudd_bddMaximallyExpand.
On entry to this function, ub and lb should be different from the zero BDD. The function then maintains this invariant.
There are three major terminal cases in theory: ub -> f : return ub lb == f : return lb not(lb -> f): return zero Only the second case can be checked exactly in constant time. For the others, we check for sufficient conditions.
dd | manager | |
lb | cube to be expanded | |
ub | upper bound cube | |
f | function against which to expand |
static int ddBddShortestPathUnate | ( | DdManager * | dd, | |
DdNode * | f, | |||
int * | phases, | |||
st_table * | table | |||
) | [static] |
Performs shortest path computation on a unate function.
This function is based on the observation that in the BDD of a unate function no node except the constant is reachable from the root via paths of different parity.
static DdNode* ddGetLargestCubeUnate | ( | DdManager * | dd, | |
DdNode * | f, | |||
int * | phases, | |||
st_table * | table | |||
) | [static] |
Extracts largest prime of a unate function.
static enum st_retval freePathPair | ( | void * | key, | |
void * | value, | |||
void * | arg | |||
) | [static] |
Frees the entries of the visited symbol table.
Build a BDD for a largest cube of f.
Given the minimum length from the root, and the minimum lengths for each node (in visited), apply triangulation at each node. Of the two children of each node on a shortest path, at least one is on a shortest path. In case of ties the procedure chooses the THEN children.
static cuddPathPair getLargest | ( | DdManager * | dd, | |
DdNode * | root, | |||
st_table * | visited | |||
) | [static] |
Finds the size of the largest cube(s) in a DD.
This problem is translated into finding the shortest paths from a node when both THEN and ELSE arcs have unit lengths. Uses a local symbol table to store the lengths for each node. Only the lengths for the regular nodes are entered in the table, because those for the complement nodes are simply obtained by swapping the two lenghts.
static DdNode* getPath | ( | DdManager * | manager, | |
st_table * | visited, | |||
DdNode * | f, | |||
int * | weight, | |||
int | cost | |||
) | [static] |
Build a BDD for a shortest path of f.
Given the minimum length from the root, and the minimum lengths for each node (in visited), apply triangulation at each node. Of the two children of each node on a shortest path, at least one is on a shortest path. In case of ties the procedure chooses the THEN children.
static cuddPathPair getShortest | ( | DdManager * | dd, | |
DdNode * | root, | |||
int * | cost, | |||
int * | support, | |||
st_table * | visited | |||
) | [static] |
Finds the length of the shortest path(s) in a DD.
Uses a local symbol table to store the lengths for each node. Only the lengths for the regular nodes are entered in the table, because those for the complement nodes are simply obtained by swapping the two lenghts.