1 // -*- coding: utf-8 -*- 2 // Copyright (C) 2016, 2018-2019 Laboratoire de Recherche et 3 // Developpement de l'Epita (LRDE). 4 // 5 // This file is part of Spot, a model checking library. 6 // 7 // Spot is free software; you can redistribute it and/or modify it 8 // under the terms of the GNU General Public License as published by 9 // the Free Software Foundation; either version 3 of the License, or 10 // (at your option) any later version. 11 // 12 // Spot is distributed in the hope that it will be useful, but WITHOUT 13 // ANY WARRANTY; without even the implied warranty of MERCHANTABILITY 14 // or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public 15 // License for more details. 16 // 17 // You should have received a copy of the GNU General Public License 18 // along with this program. If not, see <http://www.gnu.org/licenses/>. 19 20 #pragma once 21 22 #include <iostream> 23 24 namespace spot 25 { 26 27 /// \ingroup misc_tools 28 /// @{ 29 30 /// \brief A class implementing Kleene's three-valued logic. 31 /// 32 /// https://en.wikipedia.org/wiki/Three-valued_logic#Kleene_and_Priest_logics 33 class trival 34 { 35 public: 36 // We use repr_t instead of value_t in bitfields to avoid a warning from gcc 37 // https://gcc.gnu.org/bugzilla/show_bug.cgi?id=51242 38 typedef signed char repr_t; 39 enum value_t : repr_t { no_value = -1, maybe_value = 0, yes_value = 1 }; 40 private: 41 value_t val_; 42 public: trival()43 constexpr trival() 44 : val_(maybe_value) 45 { 46 } 47 trival(bool v)48 constexpr trival(bool v) 49 : val_(v ? yes_value : no_value) 50 { 51 } 52 53 #ifndef SWIG 54 // This is needed internally by Spot to work around the bitfield 55 // issue mentioned earlier, it makes no sense to use it in Python. from_repr_t(repr_t v)56 static trival from_repr_t(repr_t v) 57 { 58 return trival(static_cast<value_t>(v)); 59 } 60 #endif 61 trival(value_t v)62 constexpr explicit trival(value_t v) 63 : val_(v) 64 { 65 } 66 maybe()67 static constexpr trival maybe() noexcept 68 { 69 return trival(); 70 } 71 72 /// Is true or false, but not maybe. is_known() const73 constexpr bool is_known() const 74 { 75 return val_ != maybe_value; 76 } 77 is_maybe() const78 constexpr bool is_maybe() const 79 { 80 return val_ == maybe_value; 81 } 82 is_true() const83 constexpr bool is_true() const 84 { 85 return val_ == yes_value; 86 } 87 is_false() const88 constexpr bool is_false() const 89 { 90 return val_ == no_value; 91 } 92 val() const93 constexpr value_t val() const 94 { 95 return val_; 96 } 97 98 #ifndef SWIG 99 // constexpr explicit only supported in SWIG >= 3.0.4 100 constexpr 101 #endif operator bool() const102 explicit operator bool() const 103 { 104 return val_ == yes_value; 105 } 106 operator !() const107 constexpr trival operator!() const 108 { 109 return trival((val_ == yes_value) ? no_value : 110 (val_ == no_value) ? yes_value : 111 maybe_value); 112 } 113 }; 114 115 // We prefer a global version of the operator so that the left 116 // argument can be promoted (think "bool == trival" being promoted 117 // to "trival == trival"). However Swig's generated Python bindings 118 // cannot deal with operators in the global namespace, so we use an 119 // in-class version (coded in impl.i) in this case. This will fail 120 // on a "bool == trival" comparison in Python, but we usually write 121 // "trival == bool" and that works. 122 #ifndef SWIG operator ==(trival a,trival b)123 constexpr bool operator==(trival a, trival b) 124 { 125 return a.val() == b.val(); 126 } 127 operator !=(trival a,trival b)128 constexpr bool operator!=(trival a, trival b) 129 { 130 return !(a == b); 131 } 132 #endif 133 operator &&(trival a,trival b)134 constexpr trival operator&&(trival a, trival b) 135 { 136 return 137 (a.val() == trival::no_value || b.val() == trival::no_value) 138 ? trival(false) 139 : (a.val() == trival::maybe_value || b.val() == trival::maybe_value) 140 ? trival::maybe() 141 : trival(true); 142 } 143 operator &&(bool a,trival b)144 constexpr trival operator&&(bool a, trival b) 145 { 146 return trival(a) && b; 147 } 148 operator &&(trival a,bool b)149 constexpr trival operator&&(trival a, bool b) 150 { 151 return a && trival(b); 152 } 153 operator ||(trival a,trival b)154 constexpr trival operator||(trival a, trival b) 155 { 156 return 157 (a.val() == trival::yes_value || b.val() == trival::yes_value) 158 ? trival(true) 159 : (a.val() == trival::maybe_value || b.val() == trival::maybe_value) 160 ? trival::maybe() 161 : trival(false); 162 } 163 operator ||(bool a,trival b)164 constexpr trival operator||(bool a, trival b) 165 { 166 return trival(a) || b; 167 } 168 operator ||(trival a,bool b)169 constexpr trival operator||(trival a, bool b) 170 { 171 return a || trival(b); 172 } 173 operator <<(std::ostream & os,trival v)174 inline std::ostream& operator<<(std::ostream& os, trival v) 175 { 176 return os << ((v.val() == trival::no_value) ? "no" 177 : (v.val() == trival::maybe_value) ? "maybe" 178 : "yes"); 179 } 180 181 /// @} 182 } 183