1 // -*- coding: utf-8 -*- 2 // Copyright (C) 2009, 2013-2015, 2020 Laboratoire de Recherche et 3 // Développement de l'Epita (LRDE). 4 // Copyright (C) 2003, 2004 Laboratoire d'Informatique de Paris 5 // 6 (LIP6), département Systèmes Répartis Coopératifs (SRC), 6 // Université Pierre et Marie Curie. 7 // 8 // This file is part of Spot, a model checking library. 9 // 10 // Spot is free software; you can redistribute it and/or modify it 11 // under the terms of the GNU General Public License as published by 12 // the Free Software Foundation; either version 3 of the License, or 13 // (at your option) any later version. 14 // 15 // Spot is distributed in the hope that it will be useful, but WITHOUT 16 // ANY WARRANTY; without even the implied warranty of MERCHANTABILITY 17 // or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public 18 // License for more details. 19 // 20 // You should have received a copy of the GNU General Public License 21 // along with this program. If not, see <http://www.gnu.org/licenses/>. 22 23 #include "config.h" 24 #include <spot/misc/minato.hh> 25 #include <cassert> 26 27 namespace spot 28 { 29 minato_isop(bdd input)30 minato_isop::minato_isop(bdd input) 31 : minato_isop(input, bdd_support(input)) 32 { 33 } 34 minato_isop(bdd input,bdd vars)35 minato_isop::minato_isop(bdd input, bdd vars) 36 : ret_(bddfalse) 37 { 38 // If INPUT has the form a&b&c&(binary function) we want to 39 // compute the ISOP of the only binary and prepend a&b&c latter. 40 // 41 // Calling bdd_satprefix (it returns a&b&c and modify input to 42 // point to function) this way is an optimization to the 43 // original algorithm, because in many cases we are trying to 44 // build ISOPs out of formulae that are already cubes. 45 cube_.push(bdd_satprefix(input)); 46 todo_.emplace(input, input, vars); 47 } 48 minato_isop(bdd input_min,bdd input_max,bool)49 minato_isop::minato_isop(bdd input_min, bdd input_max, bool) 50 : ret_(bddfalse) 51 { 52 if (input_min == input_max) 53 { 54 cube_.push(bdd_satprefix(input_min)); 55 input_max = input_min; 56 } 57 else 58 { 59 cube_.push(bddtrue); 60 } 61 bdd common = input_min & input_max; 62 todo_.emplace(input_min, input_max, bdd_support(common)); 63 } 64 65 bdd next()66 minato_isop::next() 67 { 68 while (!todo_.empty()) 69 { 70 local_vars& l = todo_.top(); 71 switch (l.step) 72 { 73 case local_vars::FirstStep: 74 next_var: 75 { 76 if (l.f_min == bddfalse) 77 { 78 ret_ = bddfalse; 79 todo_.pop(); 80 continue; 81 } 82 if (l.vars == bddtrue || l.f_max == bddtrue) 83 { 84 ret_ = l.f_max; 85 todo_.pop(); 86 return cube_.top() & ret_; 87 } 88 assert(l.vars != bddfalse); 89 90 // Pick the first variable in VARS that is used by F_MIN 91 // or F_MAX. We know that VARS, F_MIN or F_MAX are not 92 // constants (bddtrue or bddfalse) because one of the 93 // two above `if' would have matched; so it's ok to call 94 // bdd_var(). 95 int v = bdd_var(l.vars); 96 l.vars = bdd_high(l.vars); 97 int v_min = bdd_var(l.f_min); 98 int v_max = bdd_var(l.f_max); 99 if (v < v_min && v < v_max) 100 // Do not use a while() for this goto, because we want 101 // `continue' to be relative to the outermost while(). 102 goto next_var; 103 104 l.step = local_vars::SecondStep; 105 106 bdd v0 = bdd_nithvar(v); 107 l.v1 = bdd_ithvar(v); 108 109 // All the following should be equivalent to 110 // f0_min = bdd_restrict(f_min, v0); 111 // f0_max = bdd_restrict(f_max, v0); 112 // f1_min = bdd_restrict(f_min, v1); 113 // f1_max = bdd_restrict(f_max, v1); 114 // but we try to avoid bdd_restrict when possible. 115 if (v == v_min) 116 { 117 l.f0_min = bdd_low(l.f_min); 118 l.f1_min = bdd_high(l.f_min); 119 } 120 else if (v_min < v) 121 { 122 l.f0_min = bdd_restrict(l.f_min, v0); 123 l.f1_min = bdd_restrict(l.f_min, l.v1); 124 } 125 else 126 { 127 l.f1_min = l.f0_min = l.f_min; 128 } 129 if (v == v_max) 130 { 131 l.f0_max = bdd_low(l.f_max); 132 l.f1_max = bdd_high(l.f_max); 133 } 134 else if (v_max < v) 135 { 136 l.f0_max = bdd_restrict(l.f_max, v0); 137 l.f1_max = bdd_restrict(l.f_max, l.v1); 138 } 139 else 140 { 141 l.f1_max = l.f0_max = l.f_max; 142 } 143 144 cube_.push(cube_.top() & v0); 145 todo_.emplace(l.f0_min - l.f1_max, l.f0_max, l.vars); 146 } 147 continue; 148 149 case local_vars::SecondStep: 150 l.step = local_vars::ThirdStep; 151 l.g0 = ret_; 152 cube_.pop(); 153 cube_.push(cube_.top() & l.v1); 154 todo_.emplace(l.f1_min - l.f0_max, l.f1_max, l.vars); 155 continue; 156 157 case local_vars::ThirdStep: 158 l.step = local_vars::FourthStep; 159 l.g1 = ret_; 160 cube_.pop(); 161 { 162 bdd fs_max = l.f0_max & l.f1_max; 163 bdd fs_min = fs_max & ((l.f0_min - l.g0) | (l.f1_min - l.g1)); 164 todo_.emplace(fs_min, fs_max, l.vars); 165 } 166 continue; 167 168 case local_vars::FourthStep: 169 ret_ |= bdd_ite(l.v1, l.g1, l.g0); 170 todo_.pop(); 171 continue; 172 } 173 SPOT_UNREACHABLE(); 174 } 175 return bddfalse; 176 } 177 178 } 179