|
|
|
@ -25,16 +25,17 @@ |
|
|
|
|
|
|
|
namespace sylvan { |
|
|
|
|
|
|
|
class BddMap; |
|
|
|
class BddSet; |
|
|
|
class BddMap; |
|
|
|
class Mtbdd; |
|
|
|
|
|
|
|
class Mtbdd; |
|
|
|
|
|
|
|
class Bdd { |
|
|
|
class Bdd { |
|
|
|
friend class Sylvan; |
|
|
|
friend class BddSet; |
|
|
|
friend class BddMap; |
|
|
|
friend class Mtbdd; |
|
|
|
|
|
|
|
public: |
|
|
|
public: |
|
|
|
Bdd() { bdd = sylvan_false; sylvan_protect(&bdd); } |
|
|
|
Bdd(const BDD from) : bdd(from) { sylvan_protect(&bdd); } |
|
|
|
Bdd(const Bdd &from) : bdd(from.bdd) { sylvan_protect(&bdd); } |
|
|
|
@ -66,7 +67,7 @@ namespace sylvan { |
|
|
|
* if it is 1, it will appear in its positive form, and if it is 2, it will appear as "any", thus it will |
|
|
|
* be skipped. |
|
|
|
*/ |
|
|
|
static Bdd bddCube(const Bdd &variables, unsigned char *values); |
|
|
|
static Bdd bddCube(const BddSet &variables, unsigned char *values); |
|
|
|
|
|
|
|
/**
|
|
|
|
* @brief Returns the Bdd representing a cube of variables, according to the given values. |
|
|
|
@ -77,7 +78,7 @@ namespace sylvan { |
|
|
|
* if it is 1, it will appear in its positive form, and if it is 2, it will appear as "any", thus it will |
|
|
|
* be skipped. |
|
|
|
*/ |
|
|
|
static Bdd bddCube(const Bdd &variables, std::vector<uint8_t> values); |
|
|
|
static Bdd bddCube(const BddSet &variables, std::vector<uint8_t> values); |
|
|
|
|
|
|
|
int operator==(const Bdd& other) const; |
|
|
|
int operator!=(const Bdd& other) const; |
|
|
|
@ -139,17 +140,17 @@ namespace sylvan { |
|
|
|
/**
|
|
|
|
* @brief Computes \exists cube: f \and g |
|
|
|
*/ |
|
|
|
Bdd AndAbstract(const Bdd& g, const Bdd& cube) const; |
|
|
|
Bdd AndAbstract(const Bdd& g, const BddSet& cube) const; |
|
|
|
|
|
|
|
/**
|
|
|
|
* @brief Computes \exists cube: f |
|
|
|
*/ |
|
|
|
Bdd ExistAbstract(const Bdd& cube) const; |
|
|
|
Bdd ExistAbstract(const BddSet& cube) const; |
|
|
|
|
|
|
|
/**
|
|
|
|
* @brief Computes \forall cube: f |
|
|
|
*/ |
|
|
|
Bdd UnivAbstract(const Bdd& cube) const; |
|
|
|
Bdd UnivAbstract(const BddSet& cube) const; |
|
|
|
|
|
|
|
/**
|
|
|
|
* @brief Computes if f then g else h |
|
|
|
@ -202,7 +203,7 @@ namespace sylvan { |
|
|
|
* Use this function to concatenate two relations --> --> |
|
|
|
* or to take the 'previous' of a set --> S |
|
|
|
*/ |
|
|
|
Bdd RelPrev(const Bdd& relation, const Bdd& cube) const; |
|
|
|
Bdd RelPrev(const Bdd& relation, const BddSet& cube) const; |
|
|
|
|
|
|
|
/**
|
|
|
|
* @brief Computes the application of a transition relation to this set. |
|
|
|
@ -214,7 +215,7 @@ namespace sylvan { |
|
|
|
* |
|
|
|
* Use this function to take the 'next' of a set S --> |
|
|
|
*/ |
|
|
|
Bdd RelNext(const Bdd& relation, const Bdd& cube) const; |
|
|
|
Bdd RelNext(const Bdd& relation, const BddSet& cube) const; |
|
|
|
|
|
|
|
/**
|
|
|
|
* @brief Computes the transitive closure by traversing the BDD recursively. |
|
|
|
@ -244,7 +245,7 @@ namespace sylvan { |
|
|
|
/**
|
|
|
|
* @brief Substitute all variables in the array from by the corresponding variables in to. |
|
|
|
*/ |
|
|
|
Bdd Permute(const std::vector<Bdd>& from, const std::vector<Bdd>& to) const; |
|
|
|
Bdd Permute(const std::vector<uint32_t>& from, const std::vector<uint32_t>& to) const; |
|
|
|
|
|
|
|
/**
|
|
|
|
* @brief Computes the support of a Bdd. |
|
|
|
@ -273,7 +274,7 @@ namespace sylvan { |
|
|
|
/**
|
|
|
|
* @brief Computes the number of satisfying variable assignments, using variables in cube. |
|
|
|
*/ |
|
|
|
double SatCount(const Bdd &variables) const; |
|
|
|
double SatCount(const BddSet &cube) const; |
|
|
|
|
|
|
|
/**
|
|
|
|
* @brief Compute the number of satisfying variable assignments, using the given number of variables. |
|
|
|
@ -284,14 +285,14 @@ namespace sylvan { |
|
|
|
* @brief Gets one satisfying assignment according to the variables. |
|
|
|
* @param variables The set of variables to be assigned, must include the support of the Bdd. |
|
|
|
*/ |
|
|
|
void PickOneCube(const Bdd &variables, uint8_t *string) const; |
|
|
|
void PickOneCube(const BddSet &variables, uint8_t *string) const; |
|
|
|
|
|
|
|
/**
|
|
|
|
* @brief Gets one satisfying assignment according to the variables. |
|
|
|
* @param variables The set of variables to be assigned, must include the support of the Bdd. |
|
|
|
* Returns an empty vector when either this Bdd equals bddZero() or the cube is empty. |
|
|
|
*/ |
|
|
|
std::vector<bool> PickOneCube(const Bdd &variables) const; |
|
|
|
std::vector<bool> PickOneCube(const BddSet &variables) const; |
|
|
|
|
|
|
|
/**
|
|
|
|
* @brief Gets a cube that satisfies this Bdd. |
|
|
|
@ -301,12 +302,12 @@ namespace sylvan { |
|
|
|
/**
|
|
|
|
* @brief Faster version of: *this + Sylvan::bddCube(variables, values); |
|
|
|
*/ |
|
|
|
Bdd UnionCube(const Bdd &variables, uint8_t *values) const; |
|
|
|
Bdd UnionCube(const BddSet &variables, uint8_t *values) const; |
|
|
|
|
|
|
|
/**
|
|
|
|
* @brief Faster version of: *this + Sylvan::bddCube(variables, values); |
|
|
|
*/ |
|
|
|
Bdd UnionCube(const Bdd &variables, std::vector<uint8_t> values) const; |
|
|
|
Bdd UnionCube(const BddSet &variables, std::vector<uint8_t> values) const; |
|
|
|
|
|
|
|
/**
|
|
|
|
* @brief Generate a cube representing a set of variables |
|
|
|
@ -326,17 +327,166 @@ namespace sylvan { |
|
|
|
|
|
|
|
#include "sylvan_obj_bdd_storm.hpp"
|
|
|
|
|
|
|
|
private: |
|
|
|
private: |
|
|
|
BDD bdd; |
|
|
|
}; |
|
|
|
}; |
|
|
|
|
|
|
|
class BddSet |
|
|
|
{ |
|
|
|
friend class Bdd; |
|
|
|
friend class Mtbdd; |
|
|
|
Bdd set; |
|
|
|
|
|
|
|
public: |
|
|
|
/**
|
|
|
|
* @brief Create a new empty set. |
|
|
|
*/ |
|
|
|
BddSet() : set(Bdd::bddOne()) {} |
|
|
|
|
|
|
|
/**
|
|
|
|
* @brief Wrap the BDD cube <other> in a set. |
|
|
|
*/ |
|
|
|
BddSet(const Bdd &other) : set(other) {} |
|
|
|
|
|
|
|
/**
|
|
|
|
* @brief Create a copy of the set <other>. |
|
|
|
*/ |
|
|
|
BddSet(const BddSet &other) : set(other.set) {} |
|
|
|
|
|
|
|
/**
|
|
|
|
* @brief Add the variable <variable> to this set. |
|
|
|
*/ |
|
|
|
void add(uint32_t variable) { |
|
|
|
set *= Bdd::bddVar(variable); |
|
|
|
} |
|
|
|
|
|
|
|
/**
|
|
|
|
* @brief Add all variables in the set <other> to this set. |
|
|
|
*/ |
|
|
|
void add(BddSet &other) { |
|
|
|
set *= other.set; |
|
|
|
} |
|
|
|
|
|
|
|
/**
|
|
|
|
* @brief Remove the variable <variable> from this set. |
|
|
|
*/ |
|
|
|
void remove(uint32_t variable) { |
|
|
|
set = set.ExistAbstract(Bdd::bddVar(variable)); |
|
|
|
} |
|
|
|
|
|
|
|
/**
|
|
|
|
* @brief Remove all variables in the set <other> from this set. |
|
|
|
*/ |
|
|
|
void remove(BddSet &other) { |
|
|
|
set = set.ExistAbstract(other.set); |
|
|
|
} |
|
|
|
|
|
|
|
/**
|
|
|
|
* @brief Retrieve the head of the set. (The first variable.) |
|
|
|
*/ |
|
|
|
uint32_t TopVar() const { |
|
|
|
return set.TopVar(); |
|
|
|
} |
|
|
|
|
|
|
|
/**
|
|
|
|
* @brief Retrieve the tail of the set. (The set containing all but the first variables.) |
|
|
|
*/ |
|
|
|
BddSet Next() const { |
|
|
|
Bdd then = set.Then(); |
|
|
|
return BddSet(then); |
|
|
|
} |
|
|
|
|
|
|
|
/**
|
|
|
|
* @brief Return true if this set is empty, or false otherwise. |
|
|
|
*/ |
|
|
|
bool isEmpty() const { |
|
|
|
return set.isOne(); |
|
|
|
} |
|
|
|
|
|
|
|
/**
|
|
|
|
* @brief Return true if this set contains the variable <variable>, or false otherwise. |
|
|
|
*/ |
|
|
|
bool contains(uint32_t variable) const { |
|
|
|
if (isEmpty()) return false; |
|
|
|
else if (TopVar() == variable) return true; |
|
|
|
else return Next().contains(variable); |
|
|
|
} |
|
|
|
|
|
|
|
/**
|
|
|
|
* @brief Return the number of variables in this set. |
|
|
|
*/ |
|
|
|
size_t size() const { |
|
|
|
if (isEmpty()) return 0; |
|
|
|
else return 1 + Next().size(); |
|
|
|
} |
|
|
|
|
|
|
|
/**
|
|
|
|
* @brief Create a set containing the <length> variables in <arr>. |
|
|
|
* It is advised to have the variables in <arr> in ascending order. |
|
|
|
*/ |
|
|
|
static BddSet fromArray(BDDVAR *arr, size_t length) { |
|
|
|
BddSet set; |
|
|
|
for (size_t i = 0; i < length; i++) { |
|
|
|
set.add(arr[length-i-1]); |
|
|
|
} |
|
|
|
} |
|
|
|
|
|
|
|
/**
|
|
|
|
* @brief Create a set containing the variables in <variables>. |
|
|
|
* It is advised to have the variables in <arr> in ascending order. |
|
|
|
*/ |
|
|
|
static BddSet fromVector(const std::vector<Bdd> variables) { |
|
|
|
BddSet set; |
|
|
|
for (int i=variables.size()-1; i>=0; i--) { |
|
|
|
set.set *= variables[i]; |
|
|
|
} |
|
|
|
return set; |
|
|
|
} |
|
|
|
|
|
|
|
/**
|
|
|
|
* @brief Create a set containing the variables in <variables>. |
|
|
|
* It is advised to have the variables in <arr> in ascending order. |
|
|
|
*/ |
|
|
|
static BddSet fromVector(const std::vector<uint32_t> variables) { |
|
|
|
BddSet set; |
|
|
|
for (int i=variables.size()-1; i>=0; i--) { |
|
|
|
set.add(variables[i]); |
|
|
|
} |
|
|
|
return set; |
|
|
|
} |
|
|
|
|
|
|
|
/**
|
|
|
|
* @brief Write all variables in this set to <arr>. |
|
|
|
* @param arr An array of at least size this.size(). |
|
|
|
*/ |
|
|
|
void toArray(BDDVAR *arr) const { |
|
|
|
if (!isEmpty()) { |
|
|
|
*arr = TopVar(); |
|
|
|
Next().toArray(arr+1); |
|
|
|
} |
|
|
|
} |
|
|
|
|
|
|
|
/**
|
|
|
|
* @brief Return the vector of all variables in this set. |
|
|
|
*/ |
|
|
|
std::vector<uint32_t> toVector() const { |
|
|
|
std::vector<uint32_t> result; |
|
|
|
Bdd x = set; |
|
|
|
while (!x.isOne()) { |
|
|
|
result.push_back(x.TopVar()); |
|
|
|
x = x.Then(); |
|
|
|
} |
|
|
|
return result; |
|
|
|
} |
|
|
|
}; |
|
|
|
|
|
|
|
class BddMap |
|
|
|
{ |
|
|
|
class BddMap |
|
|
|
{ |
|
|
|
friend class Bdd; |
|
|
|
BDD bdd; |
|
|
|
BddMap(const BDD from) : bdd(from) { sylvan_protect(&bdd); } |
|
|
|
BddMap(const Bdd &from) : bdd(from.bdd) { sylvan_protect(&bdd); } |
|
|
|
public: |
|
|
|
public: |
|
|
|
BddMap() : bdd(sylvan_map_empty()) { sylvan_protect(&bdd); } |
|
|
|
~BddMap() { sylvan_unprotect(&bdd); } |
|
|
|
|
|
|
|
@ -366,15 +516,15 @@ namespace sylvan { |
|
|
|
* @brief Returns non-zero when this map is empty |
|
|
|
*/ |
|
|
|
int isEmpty() const; |
|
|
|
}; |
|
|
|
}; |
|
|
|
|
|
|
|
class MtbddMap; |
|
|
|
class MtbddMap; |
|
|
|
|
|
|
|
class Mtbdd { |
|
|
|
class Mtbdd { |
|
|
|
friend class Sylvan; |
|
|
|
friend class MtbddMap; |
|
|
|
|
|
|
|
public: |
|
|
|
public: |
|
|
|
Mtbdd() { mtbdd = sylvan_false; mtbdd_protect(&mtbdd); } |
|
|
|
Mtbdd(const MTBDD from) : mtbdd(from) { mtbdd_protect(&mtbdd); } |
|
|
|
Mtbdd(const Mtbdd &from) : mtbdd(from.mtbdd) { mtbdd_protect(&mtbdd); } |
|
|
|
@ -429,7 +579,7 @@ namespace sylvan { |
|
|
|
* if it is 1, it will appear in its positive form, and if it is 2, it will appear as "any", thus it will |
|
|
|
* be skipped. |
|
|
|
*/ |
|
|
|
static Mtbdd mtbddCube(const Mtbdd &variables, unsigned char *values, const Mtbdd &terminal); |
|
|
|
static Mtbdd mtbddCube(const BddSet &variables, unsigned char *values, const Mtbdd &terminal); |
|
|
|
|
|
|
|
/**
|
|
|
|
* @brief Returns the Mtbdd representing a cube of variables, according to the given values. |
|
|
|
@ -441,7 +591,7 @@ namespace sylvan { |
|
|
|
* if it is 1, it will appear in its positive form, and if it is 2, it will appear as "any", thus it will |
|
|
|
* be skipped. |
|
|
|
*/ |
|
|
|
static Mtbdd mtbddCube(const Mtbdd &variables, std::vector<uint8_t> values, const Mtbdd &terminal); |
|
|
|
static Mtbdd mtbddCube(const BddSet &variables, std::vector<uint8_t> values, const Mtbdd &terminal); |
|
|
|
|
|
|
|
int operator==(const Mtbdd& other) const; |
|
|
|
int operator!=(const Mtbdd& other) const; |
|
|
|
@ -512,7 +662,7 @@ namespace sylvan { |
|
|
|
* @brief Computers the abstraction on variables <variables> using operator <op>. |
|
|
|
* See also: AbstractPlus, AbstractTimes, AbstractMin, AbstractMax |
|
|
|
*/ |
|
|
|
Mtbdd Abstract(const Mtbdd &variables, mtbdd_abstract_op op) const; |
|
|
|
Mtbdd Abstract(const BddSet &variables, mtbdd_abstract_op op) const; |
|
|
|
|
|
|
|
/**
|
|
|
|
* @brief Computes if f then g else h |
|
|
|
@ -543,27 +693,27 @@ namespace sylvan { |
|
|
|
/**
|
|
|
|
* @brief Computes abstraction by summation (existential quantification) |
|
|
|
*/ |
|
|
|
Mtbdd AbstractPlus(const Mtbdd &variables) const; |
|
|
|
Mtbdd AbstractPlus(const BddSet &variables) const; |
|
|
|
|
|
|
|
/**
|
|
|
|
* @brief Computes abstraction by multiplication (universal quantification) |
|
|
|
*/ |
|
|
|
Mtbdd AbstractTimes(const Mtbdd &variables) const; |
|
|
|
Mtbdd AbstractTimes(const BddSet &variables) const; |
|
|
|
|
|
|
|
/**
|
|
|
|
* @brief Computes abstraction by minimum |
|
|
|
*/ |
|
|
|
Mtbdd AbstractMin(const Mtbdd &variables) const; |
|
|
|
Mtbdd AbstractMin(const BddSet &variables) const; |
|
|
|
|
|
|
|
/**
|
|
|
|
* @brief Computes abstraction by maximum |
|
|
|
*/ |
|
|
|
Mtbdd AbstractMax(const Mtbdd &variables) const; |
|
|
|
Mtbdd AbstractMax(const BddSet &variables) const; |
|
|
|
|
|
|
|
/**
|
|
|
|
* @brief Computes abstraction by summation of f \times g |
|
|
|
*/ |
|
|
|
Mtbdd AndExists(const Mtbdd &other, const Mtbdd &variables) const; |
|
|
|
Mtbdd AndExists(const Mtbdd &other, const BddSet &variables) const; |
|
|
|
|
|
|
|
/**
|
|
|
|
* @brief Convert floating-point/fraction Mtbdd to a Boolean Mtbdd, leaf >= value ? true : false |
|
|
|
@ -607,12 +757,12 @@ namespace sylvan { |
|
|
|
/**
|
|
|
|
* @brief Substitute all variables in the array from by the corresponding variables in to. |
|
|
|
*/ |
|
|
|
Mtbdd Permute(const std::vector<Mtbdd>& from, const std::vector<Mtbdd>& to) const; |
|
|
|
Mtbdd Permute(const std::vector<uint32_t>& from, const std::vector<uint32_t>& to) const; |
|
|
|
|
|
|
|
/**
|
|
|
|
* @brief Compute the number of satisfying variable assignments, using variables in cube. |
|
|
|
*/ |
|
|
|
double SatCount(const Mtbdd &variables) const; |
|
|
|
double SatCount(const BddSet &variables) const; |
|
|
|
|
|
|
|
/**
|
|
|
|
* @brief Compute the number of satisfying variable assignments, using the given number of variables. |
|
|
|
@ -626,17 +776,17 @@ namespace sylvan { |
|
|
|
|
|
|
|
#include "sylvan_obj_mtbdd_storm.hpp"
|
|
|
|
|
|
|
|
private: |
|
|
|
private: |
|
|
|
MTBDD mtbdd; |
|
|
|
}; |
|
|
|
}; |
|
|
|
|
|
|
|
class MtbddMap |
|
|
|
{ |
|
|
|
class MtbddMap |
|
|
|
{ |
|
|
|
friend class Mtbdd; |
|
|
|
MTBDD mtbdd; |
|
|
|
MtbddMap(MTBDD from) : mtbdd(from) { mtbdd_protect(&mtbdd); } |
|
|
|
MtbddMap(Mtbdd &from) : mtbdd(from.mtbdd) { mtbdd_protect(&mtbdd); } |
|
|
|
public: |
|
|
|
public: |
|
|
|
MtbddMap() : mtbdd(mtbdd_map_empty()) { mtbdd_protect(&mtbdd); } |
|
|
|
~MtbddMap() { mtbdd_unprotect(&mtbdd); } |
|
|
|
|
|
|
|
@ -666,10 +816,10 @@ namespace sylvan { |
|
|
|
* @brief Returns non-zero when this map is empty |
|
|
|
*/ |
|
|
|
int isEmpty(); |
|
|
|
}; |
|
|
|
}; |
|
|
|
|
|
|
|
class Sylvan { |
|
|
|
public: |
|
|
|
class Sylvan { |
|
|
|
public: |
|
|
|
/**
|
|
|
|
* @brief Initializes the Sylvan framework, call this only once in your program. |
|
|
|
* @param initialTableSize The initial size of the nodes table. Must be a power of two. |
|
|
|
@ -697,7 +847,7 @@ namespace sylvan { |
|
|
|
* Warning: if you have any Bdd objects which are not bddZero() or bddOne() after this, your program may crash! |
|
|
|
*/ |
|
|
|
static void quitPackage(); |
|
|
|
}; |
|
|
|
}; |
|
|
|
|
|
|
|
} |
|
|
|
|
|
|
|
|
dehnert
9 years ago