TdZdd  1.1
A top-down/breadth-first decision diagram manipulation framework
ToZBDD.hpp
1 /*
2  * TdZdd: a Top-down/Breadth-first Decision Diagram Manipulation Framework
3  * by Hiroaki Iwashita <iwashita@erato.ist.hokudai.ac.jp>
4  * Copyright (c) 2014 ERATO MINATO Project
5  *
6  * Permission is hereby granted, free of charge, to any person obtaining a
7  * copy of this software and associated documentation files (the "Software"),
8  * to deal in the Software without restriction, including without limitation
9  * the rights to use, copy, modify, merge, publish, distribute, sublicense,
10  * and/or sell copies of the Software, and to permit persons to whom the
11  * Software is furnished to do so, subject to the following conditions:
12  *
13  * The above copyright notice and this permission notice shall be included in
14  * all copies or substantial portions of the Software.
15  *
16  * THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
17  * IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,
18  * FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE
19  * AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER
20  * LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING
21  * FROM, OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER
22  * DEALINGS IN THE SOFTWARE.
23  */
24 
25 #pragma once
26 
27 #ifndef B_64
28 #if __SIZEOF_POINTER__ == 8
29 #define B_64
30 #endif
31 #endif
32 #include <ZBDD.h>
33 
34 #include "../DdEval.hpp"
35 
36 namespace tdzdd {
37 
45 struct ToZBDD: public tdzdd::DdEval<ToZBDD,ZBDD> {
46  int const offset;
47 
48 public:
49  ToZBDD(int offset = 0)
50  : offset(offset) {
51  }
52 
53  bool isThreadSafe() const {
54  return false;
55  }
56 
57  void initialize(int topLevel) const {
58  while (BDD_VarUsed() < topLevel + offset) {
59  BDD_NewVar();
60  }
61  }
62 
63  void evalTerminal(ZBDD& f, int value) const {
64  f = ZBDD(value);
65  }
66 
67  void evalNode(ZBDD& f, int level, tdzdd::DdValues<ZBDD,2> const& values) const {
68  f = values.get(0);
69  if (level + offset > 0) {
70  ZBDD f1 = values.get(1);
71  f += f1.Change(BDD_VarOfLev(level + offset));
72  }
73  }
74 };
75 
76 } // namespace tdzdd
T const & get(int b) const
Returns the value of the b-th child.
Definition: DdEval.hpp:49
Collection of child node values/levels for DdEval::evalNode function interface.
Definition: DdEval.hpp:39
Base class of DD evaluators.
Definition: DdEval.hpp:102
Exporter to ZBDD.
Definition: ToZBDD.hpp:45