diff options
Diffstat (limited to 'libsolidity/formal/SolverInterface.h')
| -rw-r--r-- | libsolidity/formal/SolverInterface.h | 15 |
1 files changed, 10 insertions, 5 deletions
diff --git a/libsolidity/formal/SolverInterface.h b/libsolidity/formal/SolverInterface.h index 88487310..38d3236e 100644 --- a/libsolidity/formal/SolverInterface.h +++ b/libsolidity/formal/SolverInterface.h @@ -46,7 +46,8 @@ enum class Sort { Int, Bool, - IntIntFun // Function of one Int returning a single Int + IntIntFun, // Function of one Int returning a single Int + IntBoolFun // Function of one Int returning a single Bool }; /// C++ representation of an SMTLIB2 expression. @@ -132,10 +133,12 @@ public: Expression operator()(Expression _a) const { solAssert( - sort == Sort::IntIntFun && arguments.empty(), + (sort == Sort::IntIntFun || sort == Sort::IntBoolFun) && arguments.empty(), "Attempted function application to non-function." ); - return Expression(name, _a, Sort::Int); + if (sort == Sort::IntIntFun) + return Expression(name, _a, Sort::Int); + return Expression(name, _a, Sort::Bool); } std::string const name; @@ -167,9 +170,11 @@ public: virtual Expression newFunction(std::string _name, Sort _domain, Sort _codomain) { - solAssert(_domain == Sort::Int && _codomain == Sort::Int, "Function sort not supported."); + solAssert(_domain == Sort::Int && (_codomain == Sort::Int || _codomain == Sort::Bool), "Function sort not supported."); // Subclasses should do something here - return Expression(std::move(_name), {}, Sort::IntIntFun); + if (_codomain == Sort::Int) + return Expression(std::move(_name), {}, Sort::IntIntFun); + return Expression(std::move(_name), {}, Sort::IntBoolFun); } virtual Expression newInteger(std::string _name) { |