diff options
Diffstat (limited to 'libsolidity/formal/Z3Interface.cpp')
| -rw-r--r-- | libsolidity/formal/Z3Interface.cpp | 20 |
1 files changed, 14 insertions, 6 deletions
diff --git a/libsolidity/formal/Z3Interface.cpp b/libsolidity/formal/Z3Interface.cpp index 9a0ccf48..ac6fbd54 100644 --- a/libsolidity/formal/Z3Interface.cpp +++ b/libsolidity/formal/Z3Interface.cpp @@ -17,7 +17,7 @@ #include <libsolidity/formal/Z3Interface.h> -#include <libsolidity/interface/Exceptions.h> +#include <liblangutil/Exceptions.h> #include <libdevcore/CommonIO.h> @@ -51,7 +51,7 @@ void Z3Interface::pop() m_solver.pop(); } -void Z3Interface::declareFunction(string _name, Sort _domain, Sort _codomain) +void Z3Interface::declareFunction(string _name, vector<SortPointer> const& _domain, Sort const& _codomain) { if (!m_functions.count(_name)) m_functions.insert({_name, m_context.function(_name.c_str(), z3Sort(_domain), z3Sort(_codomain))}); @@ -168,13 +168,13 @@ z3::expr Z3Interface::toZ3Expr(Expression const& _expr) return arguments[0]; } -z3::sort Z3Interface::z3Sort(Sort _sort) +z3::sort Z3Interface::z3Sort(Sort const& _sort) { - switch (_sort) + switch (_sort.kind) { - case Sort::Bool: + case Kind::Bool: return m_context.bool_sort(); - case Sort::Int: + case Kind::Int: return m_context.int_sort(); default: break; @@ -183,3 +183,11 @@ z3::sort Z3Interface::z3Sort(Sort _sort) // Cannot be reached. return m_context.int_sort(); } + +z3::sort_vector Z3Interface::z3Sort(vector<SortPointer> const& _sorts) +{ + z3::sort_vector z3Sorts(m_context); + for (auto const& _sort: _sorts) + z3Sorts.push_back(z3Sort(*_sort)); + return z3Sorts; +} |