diff --git a/CMakeLists.txt b/CMakeLists.txt
index 010de5b8e..d0e0aa6d0 100644
--- a/CMakeLists.txt
+++ b/CMakeLists.txt
@@ -100,6 +100,12 @@ if (NOT (${Z3_FOUND} OR ${CVC4_FOUND}))
\nPlease install Z3 or CVC4 or remove the option disabling them (USE_Z3, USE_CVC4).")
endif()
+find_package(OSMT2 QUIET)
+if (${OSMT2_FOUND})
+ add_definitions(-DHAVE_OSMT2)
+ message("OpenSMT2 SMT solver found. This enables optional SMT-based Yul optimizations with OpenSMT2.")
+endif()
+
add_subdirectory(libsolutil)
add_subdirectory(liblangutil)
add_subdirectory(libsmtutil)
diff --git a/cmake/EthCompilerSettings.cmake b/cmake/EthCompilerSettings.cmake
index 04c2a154f..dc321814b 100644
--- a/cmake/EthCompilerSettings.cmake
+++ b/cmake/EthCompilerSettings.cmake
@@ -224,6 +224,7 @@ if(UNIX AND NOT APPLE)
option(USE_Z3_DLOPEN "Dynamically load the Z3 SMT solver instead of linking against it." OFF)
endif()
option(USE_CVC4 "Allow compiling with CVC4 SMT solver integration" ON)
+option(USE_OSMT2 "Allow compiling with OpenSMT2 SMT solver integration" ON)
if (("${CMAKE_CXX_COMPILER_ID}" MATCHES "GNU") OR ("${CMAKE_CXX_COMPILER_ID}" MATCHES "Clang"))
option(USE_LD_GOLD "Use GNU gold linker" ON)
diff --git a/cmake/FindOSMT2.cmake b/cmake/FindOSMT2.cmake
new file mode 100644
index 000000000..5236e86d2
--- /dev/null
+++ b/cmake/FindOSMT2.cmake
@@ -0,0 +1,27 @@
+if (USE_OSMT2)
+ find_path(OSMT2_INCLUDE_DIR opensmt/opensmt2.h)
+ find_library(OSMT2_LIBRARY NAMES opensmt2)
+ include(FindPackageHandleStandardArgs)
+ find_package_handle_standard_args(OSMT2 DEFAULT_MSG OSMT2_LIBRARY OSMT2_INCLUDE_DIR)
+ if(OSMT2_FOUND)
+ # OSMT2 depends on GMP.
+ # We can assume that GMP is present on the system,
+ # so we quietly try to find it and link against it, if it is present.
+ find_package(GMP QUIET)
+
+ set(OSMT2_LIBRARIES ${OSMT2_LIBRARY})
+
+ if (GMP_FOUND)
+ set(OSMT2_LIBRARIES ${OSMT2_LIBRARIES} GMP::GMP)
+ endif ()
+
+ if (NOT TARGET OSMT2::OSMT2)
+ add_library(OSMT2::OSMT2 UNKNOWN IMPORTED)
+ set_property(TARGET OSMT2::OSMT2 PROPERTY IMPORTED_LOCATION ${OSMT2_LIBRARY})
+ set_property(TARGET OSMT2::OSMT2 PROPERTY INTERFACE_LINK_LIBRARIES ${OSMT2_LIBRARIES})
+ set_property(TARGET OSMT2::OSMT2 PROPERTY INTERFACE_INCLUDE_DIRECTORIES ${OSMT2_INCLUDE_DIR})
+ endif()
+ endif()
+else()
+ set(OSMT2_FOUND FALSE)
+endif()
diff --git a/libsmtutil/CMakeLists.txt b/libsmtutil/CMakeLists.txt
index af7f47b60..edef50308 100644
--- a/libsmtutil/CMakeLists.txt
+++ b/libsmtutil/CMakeLists.txt
@@ -24,19 +24,13 @@ else()
set(cvc4_SRCS)
endif()
-if (${USE_Z3_DLOPEN})
- file(GLOB Z3_HEADERS ${Z3_HEADER_PATH}/z3*.h)
- set(Z3_WRAPPER ${CMAKE_CURRENT_BINARY_DIR}/z3wrapper.cpp)
- add_custom_command(
- OUTPUT ${Z3_WRAPPER}
- COMMAND ${Python3_EXECUTABLE} genz3wrapper.py ${Z3_HEADERS} > ${Z3_WRAPPER}
- DEPENDS ${Z3_HEADERS} genz3wrapper.py
- WORKING_DIRECTORY ${CMAKE_CURRENT_SOURCE_DIR}
- )
- set(z3_SRCS ${z3_SRCS} ${Z3_WRAPPER} Z3Loader.cpp Z3Loader.h)
+if (${OSMT2_FOUND})
+ set(osmt2_SRCS OpenSMT2Interface.cpp OpenSMT2Interface.h)
+else()
+ set(osmt2_SRCS)
endif()
-add_library(smtutil ${sources} ${z3_SRCS} ${cvc4_SRCS})
+add_library(smtutil ${sources} ${z3_SRCS} ${cvc4_SRCS} ${osmt2_SRCS})
target_link_libraries(smtutil PUBLIC solutil Boost::boost)
if (${USE_Z3_DLOPEN})
@@ -49,3 +43,7 @@ endif()
if (${CVC4_FOUND})
target_link_libraries(smtutil PUBLIC CVC4::CVC4)
endif()
+
+if (${OSMT2_FOUND})
+ target_link_libraries(smtutil PUBLIC OSMT2::OSMT2)
+endif()
diff --git a/libsmtutil/OpenSMT2Interface.cpp b/libsmtutil/OpenSMT2Interface.cpp
new file mode 100644
index 000000000..80ebb05a5
--- /dev/null
+++ b/libsmtutil/OpenSMT2Interface.cpp
@@ -0,0 +1,182 @@
+/*
+ This file is part of solidity.
+
+ solidity is free software: you can redistribute it and/or modify
+ it under the terms of the GNU General Public License as published by
+ the Free Software Foundation, either version 3 of the License, or
+ (at your option) any later version.
+
+ solidity is distributed in the hope that it will be useful,
+ but WITHOUT ANY WARRANTY; without even the implied warranty of
+ MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
+ GNU General Public License for more details.
+
+ You should have received a copy of the GNU General Public License
+ along with solidity. If not, see .
+*/
+// SPDX-License-Identifier: GPL-3.0
+
+#include
+
+using namespace std;
+using namespace solidity;
+using namespace solidity::util;
+using namespace solidity::smtutil;
+
+OpenSMT2Interface::OpenSMT2Interface():
+ m_opensmt(make_unique(qf_lia, "OpenSMT")),
+ m_logic(m_opensmt->getLIALogic()),
+ m_solver(m_opensmt->getMainSolver())
+{
+}
+
+void OpenSMT2Interface::reset()
+{
+}
+
+void OpenSMT2Interface::push()
+{
+ m_solver.push();
+}
+
+void OpenSMT2Interface::pop()
+{
+ m_solver.pop();
+}
+
+void OpenSMT2Interface::declareVariable(string const& _name, SortPointer const& _sort)
+{
+ smtAssert(_sort, "");
+ m_variables[_name] = m_logic.mkVar(openSMT2Sort(*_sort), _name.c_str());
+}
+
+void OpenSMT2Interface::addAssertion(Expression const& _expr)
+{
+ m_solver.insertFormula(toOpenSMT2Expr(_expr));
+}
+
+pair> OpenSMT2Interface::check(vector const& _expressionsToEvaluate)
+{
+ CheckResult result;
+ vector values;
+
+ sstat res = m_solver.check();
+ if (res == s_True)
+ result = CheckResult::SATISFIABLE;
+ else if (res == s_False)
+ result = CheckResult::UNSATISFIABLE;
+ else if (res == s_Undef)
+ result = CheckResult::UNKNOWN;
+ else
+ result = CheckResult::ERROR;
+
+ if (result == CheckResult::SATISFIABLE && !_expressionsToEvaluate.empty())
+ {
+ for (Expression const& e: _expressionsToEvaluate)
+ values.push_back(m_solver.getValue(toOpenSMT2Expr(e)).val);
+ }
+
+ return make_pair(result, values);
+}
+
+PTRef OpenSMT2Interface::toOpenSMT2Expr(Expression const& _expr)
+{
+ // Variable
+ if (_expr.arguments.empty() && m_variables.count(_expr.name))
+ return m_variables.at(_expr.name);
+
+ vector arguments;
+ for (auto const& arg: _expr.arguments)
+ arguments.push_back(toOpenSMT2Expr(arg));
+
+ try
+ {
+ string const& n = _expr.name;
+ // Function application
+ if (!arguments.empty() && m_variables.count(_expr.name))
+ smtAssert(false, "Not implemented.");
+ // Literal
+ else if (arguments.empty())
+ {
+ if (n == "true")
+ return m_logic.getTerm_true();
+ else if (n == "false")
+ return m_logic.getTerm_false();
+ else if (auto sortSort = dynamic_pointer_cast(_expr.sort))
+ return m_logic.mkVar(openSMT2Sort(*sortSort->inner), n.c_str());
+ else
+ try
+ {
+ return m_logic.mkConst(n.c_str());
+ }
+ catch (std::exception const& _e)
+ {
+ smtAssert(false, _e.what());
+ }
+ }
+
+ smtAssert(_expr.hasCorrectArity(), "");
+ if (n == "ite")
+ return m_logic.mkIte(arguments[0], arguments[1], arguments[2]);
+ else if (n == "not")
+ return m_logic.mkNot(arguments[0]);
+ else if (n == "and")
+ return m_logic.mkAnd(arguments[0], arguments[1]);
+ else if (n == "or")
+ return m_logic.mkOr(arguments[0], arguments[1]);
+ else if (n == "implies")
+ return m_logic.mkImpl(arguments[0], arguments[1]);
+ else if (n == "=")
+ return m_logic.mkEq(arguments[0], arguments[1]);
+ else if (n == "<")
+ return m_logic.mkNumLt(arguments[0], arguments[1]);
+ else if (n == "<=")
+ return m_logic.mkNumLeq(arguments[0], arguments[1]);
+ else if (n == ">")
+ return m_logic.mkNumGt(arguments[0], arguments[1]);
+ else if (n == ">=")
+ return m_logic.mkNumGeq(arguments[0], arguments[1]);
+ else if (n == "+")
+ return m_logic.mkNumPlus(arguments[0], arguments[1]);
+ else if (n == "-")
+ return m_logic.mkNumMinus(arguments[0], arguments[1]);
+ else if (n == "*")
+ return m_logic.mkNumTimes(arguments[0], arguments[1]);
+ else if (n == "/")
+ return m_logic.mkNumDiv(arguments[0], arguments[1]);
+ else if (n == "mod")
+ smtAssert(false, "Not implemented.");
+ else
+ smtAssert(false, "Not implemented.");
+
+ smtAssert(false, "");
+ }
+ catch (std::exception const& _e)
+ {
+ smtAssert(false, _e.what());
+ }
+
+ smtAssert(false, "");
+}
+
+SRef OpenSMT2Interface::openSMT2Sort(Sort const& _sort)
+{
+ switch (_sort.kind)
+ {
+ case Kind::Bool:
+ return m_logic.getSort_bool();
+ case Kind::Int:
+ return m_logic.getSort_num();
+ default:
+ smtAssert(false, "Not implemented.");
+ }
+ smtAssert(false, "");
+}
+
+vector OpenSMT2Interface::openSMT2Sort(vector const& _sorts)
+{
+ vector opensmt2Sorts;
+ for (auto const& _sort: _sorts)
+ opensmt2Sorts.push_back(openSMT2Sort(*_sort));
+ return opensmt2Sorts;
+}
diff --git a/libsmtutil/OpenSMT2Interface.h b/libsmtutil/OpenSMT2Interface.h
new file mode 100644
index 000000000..bc443c906
--- /dev/null
+++ b/libsmtutil/OpenSMT2Interface.h
@@ -0,0 +1,55 @@
+/*
+ This file is part of solidity.
+
+ solidity is free software: you can redistribute it and/or modify
+ it under the terms of the GNU General Public License as published by
+ the Free Software Foundation, either version 3 of the License, or
+ (at your option) any later version.
+
+ solidity is distributed in the hope that it will be useful,
+ but WITHOUT ANY WARRANTY; without even the implied warranty of
+ MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
+ GNU General Public License for more details.
+
+ You should have received a copy of the GNU General Public License
+ along with solidity. If not, see .
+*/
+// SPDX-License-Identifier: GPL-3.0
+
+#pragma once
+
+#include
+#include
+
+#include
+
+namespace solidity::smtutil
+{
+
+class OpenSMT2Interface: public SolverInterface, public boost::noncopyable
+{
+public:
+ OpenSMT2Interface();
+
+ void reset() override;
+
+ void push() override;
+ void pop() override;
+
+ void declareVariable(std::string const&, SortPointer const&) override;
+
+ void addAssertion(Expression const& _expr) override;
+ std::pair> check(std::vector const& _expressionsToEvaluate) override;
+
+private:
+ PTRef toOpenSMT2Expr(Expression const& _expr);
+ SRef openSMT2Sort(Sort const& _sort);
+ std::vector openSMT2Sort(std::vector const& _sorts);
+
+ std::unique_ptr m_opensmt;
+ LIALogic& m_logic;
+ MainSolver& m_solver;
+ std::map m_variables;
+};
+
+}