aboutsummaryrefslogtreecommitdiffstats
path: root/libsolidity/formal/CVC4Interface.cpp
diff options
context:
space:
mode:
Diffstat (limited to 'libsolidity/formal/CVC4Interface.cpp')
-rw-r--r--libsolidity/formal/CVC4Interface.cpp10
1 files changed, 9 insertions, 1 deletions
diff --git a/libsolidity/formal/CVC4Interface.cpp b/libsolidity/formal/CVC4Interface.cpp
index 6cb91483..11822927 100644
--- a/libsolidity/formal/CVC4Interface.cpp
+++ b/libsolidity/formal/CVC4Interface.cpp
@@ -50,7 +50,7 @@ void CVC4Interface::pop()
m_solver.pop();
}
-void CVC4Interface::declareFunction(string _name, Sort _domain, Sort _codomain)
+void CVC4Interface::declareFunction(string _name, vector<Sort> const& _domain, Sort _codomain)
{
if (!m_functions.count(_name))
{
@@ -201,3 +201,11 @@ CVC4::Type CVC4Interface::cvc4Sort(Sort _sort)
// Cannot be reached.
return m_context.integerType();
}
+
+vector<CVC4::Type> CVC4Interface::cvc4Sort(vector<Sort> const& _sorts)
+{
+ vector<CVC4::Type> cvc4Sorts;
+ for (auto const& _sort: _sorts)
+ cvc4Sorts.push_back(cvc4Sort(_sort));
+ return cvc4Sorts;
+}