You can not select more than 25 topics
Topics must start with a letter or number, can include dashes ('-') and can be up to 35 characters long.
253 lines
6.3 KiB
253 lines
6.3 KiB
//==============================================================================
|
|
//
|
|
// Copyright (c) 2002-
|
|
// Authors:
|
|
// * Dave Parker <david.parker@comlab.ox.ac.uk> (University of Oxford, formerly University of Birmingham)
|
|
// Description: DD variable functions
|
|
//
|
|
//------------------------------------------------------------------------------
|
|
//
|
|
// This file is part of PRISM.
|
|
//
|
|
// PRISM is free software; you can redistribute it and/or modify
|
|
// it under the terms of the GNU General Public License as published by
|
|
// the Free Software Foundation; either version 2 of the License, or
|
|
// (at your option) any later version.
|
|
//
|
|
// PRISM is distributed in the hope that it will be useful,
|
|
// but WITHOUT ANY WARRANTY; without even the implied warranty of
|
|
// MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
|
|
// GNU General Public License for more details.
|
|
//
|
|
// You should have received a copy of the GNU General Public License
|
|
// along with PRISM; if not, write to the Free Software Foundation,
|
|
// Inc., 59 Temple Place, Suite 330, Boston, MA 02111-1307 USA
|
|
//
|
|
//==============================================================================
|
|
|
|
#include <util.h>
|
|
#include <cudd.h>
|
|
#include "dd_vars.h"
|
|
#include "dd_basics.h"
|
|
|
|
//------------------------------------------------------------------------------
|
|
|
|
// note: this PERMUTES variables (i.e. x_i -> y_i) cf. DD_SwapVariables
|
|
|
|
DdNode *DD_PermuteVariables
|
|
(
|
|
DdManager *ddman,
|
|
DdNode *dd,
|
|
DdNode **old_vars,
|
|
DdNode **new_vars,
|
|
int num_vars
|
|
)
|
|
{
|
|
int i, *permut;
|
|
DdNode *res;
|
|
|
|
permut = new int[Cudd_ReadSize(ddman)];
|
|
for (i = 0; i < Cudd_ReadSize(ddman); i++) {
|
|
permut[i] = i;
|
|
}
|
|
for (i = 0; i < num_vars; i++) {
|
|
permut[old_vars[i]->index] = new_vars[i]->index;
|
|
}
|
|
res = Cudd_addPermute(ddman, dd, permut);
|
|
Cudd_Ref(res);
|
|
Cudd_RecursiveDeref(ddman, dd);
|
|
|
|
if (permut != NULL) {
|
|
delete[] permut;
|
|
}
|
|
|
|
return res;
|
|
}
|
|
|
|
//------------------------------------------------------------------------------
|
|
|
|
// note: this SWAPS variables (i.e. x_i <-> y_i) cf. DD_PermuteVariables
|
|
|
|
DdNode *DD_SwapVariables
|
|
(
|
|
DdManager *ddman,
|
|
DdNode *dd,
|
|
DdNode **old_vars,
|
|
DdNode **new_vars,
|
|
int num_vars
|
|
)
|
|
{
|
|
DdNode *res;
|
|
|
|
res = Cudd_addSwapVariables(ddman, dd, old_vars, new_vars, num_vars);
|
|
Cudd_Ref(res);
|
|
Cudd_RecursiveDeref(ddman, dd);
|
|
|
|
return res;
|
|
}
|
|
|
|
//------------------------------------------------------------------------------
|
|
|
|
// Generates BDD for the function x > y
|
|
// where x, y are num_vars-bit numbers encoded by variables x_vars, y_vars
|
|
|
|
DdNode *DD_VariablesGreaterThan
|
|
(
|
|
DdManager *ddman,
|
|
DdNode **x_vars,
|
|
DdNode **y_vars,
|
|
int num_vars
|
|
)
|
|
{
|
|
DdNode *tmp, *res;
|
|
DdNode **x_bdd_vars, **y_bdd_vars;
|
|
int i;
|
|
|
|
// create bdd vars from add vars
|
|
x_bdd_vars = new DdNode*[num_vars];
|
|
y_bdd_vars = new DdNode*[num_vars];
|
|
for (i = 0; i < num_vars; i++) {
|
|
x_bdd_vars[i] = Cudd_bddIthVar(ddman, x_vars[i]->index);
|
|
Cudd_Ref(x_bdd_vars[i]);
|
|
y_bdd_vars[i] = Cudd_bddIthVar(ddman, y_vars[i]->index);
|
|
Cudd_Ref(y_bdd_vars[i]);
|
|
}
|
|
// call main function
|
|
tmp = Cudd_Xgty(ddman, num_vars, NULL, x_bdd_vars, y_bdd_vars);
|
|
Cudd_Ref(tmp);
|
|
// convert bdd to add
|
|
res = Cudd_BddToAdd(ddman, tmp);
|
|
Cudd_Ref(res);
|
|
Cudd_RecursiveDeref(ddman, tmp);
|
|
// free variables
|
|
for (i = 0; i < num_vars; i++) {
|
|
Cudd_RecursiveDeref(ddman, x_bdd_vars[i]);
|
|
Cudd_RecursiveDeref(ddman, y_bdd_vars[i]);
|
|
}
|
|
delete[] x_bdd_vars;
|
|
delete[] y_bdd_vars;
|
|
|
|
return res;
|
|
}
|
|
|
|
//------------------------------------------------------------------------------
|
|
|
|
// Generates BDD for the function x >= y
|
|
// where x, y are num_vars-bit numbers encoded by variables x_vars, y_vars
|
|
|
|
DdNode *DD_VariablesGreaterThanEquals
|
|
(
|
|
DdManager *ddman,
|
|
DdNode **x_vars,
|
|
DdNode **y_vars,
|
|
int num_vars
|
|
)
|
|
{
|
|
return DD_Not(ddman, DD_VariablesLessThan(ddman, x_vars, y_vars, num_vars));
|
|
}
|
|
|
|
//------------------------------------------------------------------------------
|
|
|
|
// Generates BDD for the function x < y
|
|
// where x, y are num_vars-bit numbers encoded by variables x_vars, y_vars
|
|
|
|
DdNode *DD_VariablesLessThan
|
|
(
|
|
DdManager *ddman,
|
|
DdNode **x_vars,
|
|
DdNode **y_vars,
|
|
int num_vars
|
|
)
|
|
{
|
|
DdNode *tmp, *res;
|
|
DdNode **x_bdd_vars, **y_bdd_vars;
|
|
int i;
|
|
|
|
// create bdd vars from add vars
|
|
x_bdd_vars = new DdNode*[num_vars];
|
|
y_bdd_vars = new DdNode*[num_vars];
|
|
for (i = 0; i < num_vars; i++) {
|
|
x_bdd_vars[i] = Cudd_bddIthVar(ddman, x_vars[i]->index);
|
|
Cudd_Ref(x_bdd_vars[i]);
|
|
y_bdd_vars[i] = Cudd_bddIthVar(ddman, y_vars[i]->index);
|
|
Cudd_Ref(y_bdd_vars[i]);
|
|
}
|
|
// call main function
|
|
tmp = Cudd_Xgty(ddman, num_vars, NULL, y_bdd_vars, x_bdd_vars);
|
|
Cudd_Ref(tmp);
|
|
// convert bdd to add
|
|
res = Cudd_BddToAdd(ddman, tmp);
|
|
Cudd_Ref(res);
|
|
Cudd_RecursiveDeref(ddman, tmp);
|
|
// free variables
|
|
for (i = 0; i < num_vars; i++) {
|
|
Cudd_RecursiveDeref(ddman, x_bdd_vars[i]);
|
|
Cudd_RecursiveDeref(ddman, y_bdd_vars[i]);
|
|
}
|
|
delete[] x_bdd_vars;
|
|
delete[] y_bdd_vars;
|
|
|
|
return res;
|
|
}
|
|
|
|
//------------------------------------------------------------------------------
|
|
|
|
// Generates BDD for the function x <= y
|
|
// where x, y are num_vars-bit numbers encoded by variables x_vars, y_vars
|
|
|
|
DdNode *DD_VariablesLessThanEquals
|
|
(
|
|
DdManager *ddman,
|
|
DdNode **x_vars,
|
|
DdNode **y_vars,
|
|
int num_vars
|
|
)
|
|
{
|
|
return DD_Not(ddman, DD_VariablesGreaterThan(ddman, x_vars, y_vars, num_vars));
|
|
}
|
|
|
|
//------------------------------------------------------------------------------
|
|
|
|
// Generates BDD for the function x == y
|
|
// where x, y are num_vars-bit numbers encoded by variables x_vars, y_vars
|
|
|
|
DdNode *DD_VariablesEquals
|
|
(
|
|
DdManager *ddman,
|
|
DdNode **x_vars,
|
|
DdNode **y_vars,
|
|
int num_vars
|
|
)
|
|
{
|
|
DdNode *tmp, *res;
|
|
DdNode **x_bdd_vars, **y_bdd_vars;
|
|
int i;
|
|
|
|
// create bdd vars from add vars
|
|
x_bdd_vars = new DdNode*[num_vars];
|
|
y_bdd_vars = new DdNode*[num_vars];
|
|
for (i = 0; i < num_vars; i++) {
|
|
x_bdd_vars[i] = Cudd_bddIthVar(ddman, x_vars[i]->index);
|
|
Cudd_Ref(x_bdd_vars[i]);
|
|
y_bdd_vars[i] = Cudd_bddIthVar(ddman, y_vars[i]->index);
|
|
Cudd_Ref(y_bdd_vars[i]);
|
|
}
|
|
// call main function
|
|
tmp = Cudd_Xeqy(ddman, num_vars, x_bdd_vars, y_bdd_vars);
|
|
Cudd_Ref(tmp);
|
|
// convert bdd to add
|
|
res = Cudd_BddToAdd(ddman, tmp);
|
|
Cudd_Ref(res);
|
|
Cudd_RecursiveDeref(ddman, tmp);
|
|
// free variables
|
|
for (i = 0; i < num_vars; i++) {
|
|
Cudd_RecursiveDeref(ddman, x_bdd_vars[i]);
|
|
Cudd_RecursiveDeref(ddman, y_bdd_vars[i]);
|
|
}
|
|
delete[] x_bdd_vars;
|
|
delete[] y_bdd_vars;
|
|
|
|
return res;
|
|
}
|
|
|
|
//------------------------------------------------------------------------------
|