1 /** 2 * Copyright (c) 2021-2022 Huawei Device Co., Ltd. 3 * Licensed under the Apache License, Version 2.0 (the "License"); 4 * you may not use this file except in compliance with the License. 5 * You may obtain a copy of the License at 6 * 7 * http://www.apache.org/licenses/LICENSE-2.0 8 * 9 * Unless required by applicable law or agreed to in writing, software 10 * distributed under the License is distributed on an "AS IS" BASIS, 11 * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. 12 * See the License for the specific language governing permissions and 13 * limitations under the License. 14 */ 15 16 #ifndef PANDA_VERIFICATION_VALUE_VAR_BINDING_H 17 #define PANDA_VERIFICATION_VALUE_VAR_BINDING_H 18 19 #include "verifier/type_system.h" 20 #include "verifier/value/variable.h" 21 #include "verifier/relation.h" 22 23 #include <variant> 24 #include <optional> 25 #include <unordered_map> 26 27 namespace panda::verifier { 28 template <typename BoundVarValue> 29 class VarBindings { 30 public: 31 using EqualityRel = panda::type_system::Realtion<Variables::Var>; 32 Equate(Variables::Var lhs,Variable::Var rhs)33 void Equate(Variables::Var lhs, Variable::Var rhs) 34 { 35 Equality_.SymmRelate(lhs, rhs); 36 } 37 void Bind(Variables::Var var, BoundVarValue val); 38 bool IsEquated(Variables::Var v); 39 bool IsBound(Variables::Var v); 40 std::optional<BoundVarValue> operator[](Variable::Var v); 41 auto AllInEqualClass(Variables::Var var); 42 43 private: 44 std::unordered_map<Variables::Var, BoundVarValue> Bindings_; 45 EqualityRel Equality_; 46 }; 47 } // namespace panda::verifier 48 49 #endif // PANDA_VERIFICATION_VALUE_VAR_BINDING_H 50