31 #include "../DdSpec.hpp" 36 class BddLookahead:
public DdSpecBase<BddLookahead<S>,S::ARITY> {
40 std::vector<char> work0;
41 std::vector<char> work1;
43 int lookahead(
void* p,
int level) {
45 spec.get_copy(work0.data(), p);
46 int level0 = spec.get_child(work0.data(), level, 0);
48 for (
int b = 1; b < Spec::ARITY; ++b) {
49 spec.get_copy(work1.data(), p);
50 int level1 = spec.get_child(work1.data(), level, b);
51 if (!(level0 == level1
53 || spec.equal_to(work0.data(), work1.data(),
55 spec.destruct(work0.data());
56 spec.destruct(work1.data());
59 spec.destruct(work1.data());
63 spec.get_copy(p, work0.data());
64 spec.destruct(work0.data());
72 BddLookahead(S
const& s)
73 : spec(s), work0(spec.datasize()), work1(spec.datasize()) {
76 int datasize()
const {
77 return spec.datasize();
80 int get_root(
void* p) {
81 return lookahead(p, spec.get_root(p));
84 int get_child(
void* p,
int level,
int b) {
85 return lookahead(p, spec.get_child(p, level, b));
88 void get_copy(
void* to,
void const* from) {
89 spec.get_copy(to, from);
92 int merge_states(
void* p1,
void* p2) {
93 return spec.merge_states(p1, p2);
96 void destruct(
void* p) {
100 void destructLevel(
int level) {
101 spec.destructLevel(level);
104 size_t hash_code(
void const* p,
int level)
const {
105 return spec.hash_code(p, level);
108 bool equal_to(
void const* p,
void const* q,
int level)
const {
109 return spec.equal_to(p, q, level);
112 void print_state(std::ostream& os,
void const* p,
int level)
const {
113 spec.print_state(os, p, level);
116 void print_level(std::ostream& os,
int level)
const {
117 spec.print_level(os, level);
122 class ZddLookahead:
public DdSpecBase<ZddLookahead<S>,S::ARITY> {
126 std::vector<char> work;
128 int lookahead(
void* p,
int level) {
129 void*
const q = work.data();
131 for (
int b = 1; b < Spec::ARITY; ++b) {
133 if (spec.get_child(q, level, b) != 0) {
139 level = spec.get_child(p, level, 0);
146 ZddLookahead(S
const& s)
147 : spec(s), work(spec.datasize()) {
150 int datasize()
const {
151 return spec.datasize();
154 int get_root(
void* p) {
155 return lookahead(p, spec.get_root(p));
158 int get_child(
void* p,
int level,
int b) {
159 return lookahead(p, spec.get_child(p, level, b));
162 void get_copy(
void* to,
void const* from) {
163 spec.get_copy(to, from);
166 int merge_states(
void* p1,
void* p2) {
167 return spec.merge_states(p1, p2);
170 void destruct(
void* p) {
174 void destructLevel(
int level) {
175 spec.destructLevel(level);
178 size_t hash_code(
void const* p,
int level)
const {
179 return spec.hash_code(p, level);
182 bool equal_to(
void const* p,
void const* q,
int level)
const {
183 return spec.equal_to(p, q, level);
186 void print_state(std::ostream& os,
void const* p,
int level)
const {
187 spec.print_state(os, p, level);
190 void print_level(std::ostream& os,
int level)
const {
191 spec.print_level(os, level);