1 /* 2 This file is part of solidity. 3 4 solidity is free software: you can redistribute it and/or modify 5 it under the terms of the GNU General Public License as published by 6 the Free Software Foundation, either version 3 of the License, or 7 (at your option) any later version. 8 9 solidity is distributed in the hope that it will be useful, 10 but WITHOUT ANY WARRANTY; without even the implied warranty of 11 MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the 12 GNU General Public License for more details. 13 14 You should have received a copy of the GNU General Public License 15 along with solidity. If not, see <http://www.gnu.org/licenses/>. 16 */ 17 // SPDX-License-Identifier: GPL-3.0 18 19 #pragma once 20 21 /** 22 * Formats SMT expressions into Solidity-like strings. 23 */ 24 25 #include <libsolidity/formal/Predicate.h> 26 27 #include <map> 28 #include <string> 29 30 namespace solidity::frontend::smt 31 { 32 33 /// @returns another smtutil::Expressions where every term in _from 34 /// may be replaced if it is in the substitution map _subst. 35 smtutil::Expression substitute(smtutil::Expression _from, std::map<std::string, std::string> const& _subst); 36 37 /// @returns a Solidity-like expression string built from _expr. 38 /// This is done at best-effort and is not guaranteed to always create a perfect Solidity expression string. 39 std::string toSolidityStr(smtutil::Expression const& _expr); 40 41 } 42