diff options
Diffstat (limited to 'libsolidity/formal/SMTPortfolio.cpp')
| -rw-r--r-- | libsolidity/formal/SMTPortfolio.cpp | 25 |
1 files changed, 4 insertions, 21 deletions
diff --git a/libsolidity/formal/SMTPortfolio.cpp b/libsolidity/formal/SMTPortfolio.cpp index 8b9fe9ce..2a109b89 100644 --- a/libsolidity/formal/SMTPortfolio.cpp +++ b/libsolidity/formal/SMTPortfolio.cpp @@ -23,27 +23,22 @@ #ifdef HAVE_CVC4 #include <libsolidity/formal/CVC4Interface.h> #endif -#if !defined (HAVE_Z3) && !defined (HAVE_CVC4) #include <libsolidity/formal/SMTLib2Interface.h> -#endif using namespace std; using namespace dev; using namespace dev::solidity; using namespace dev::solidity::smt; -SMTPortfolio::SMTPortfolio(ReadCallback::Callback const& _readCallback) +SMTPortfolio::SMTPortfolio(map<h256, string> const& _smtlib2Responses) { + m_solvers.emplace_back(make_shared<smt::SMTLib2Interface>(_smtlib2Responses)); #ifdef HAVE_Z3 m_solvers.emplace_back(make_shared<smt::Z3Interface>()); #endif #ifdef HAVE_CVC4 m_solvers.emplace_back(make_shared<smt::CVC4Interface>()); #endif -#if !defined (HAVE_Z3) && !defined (HAVE_CVC4) - m_solvers.emplace_back(make_shared<smt::SMTLib2Interface>(_readCallback)), -#endif - (void)_readCallback; } void SMTPortfolio::reset() @@ -64,22 +59,10 @@ void SMTPortfolio::pop() s->pop(); } -void SMTPortfolio::declareFunction(string _name, Sort _domain, Sort _codomain) -{ - for (auto s : m_solvers) - s->declareFunction(_name, _domain, _codomain); -} - -void SMTPortfolio::declareInteger(string _name) -{ - for (auto s : m_solvers) - s->declareInteger(_name); -} - -void SMTPortfolio::declareBool(string _name) +void SMTPortfolio::declareVariable(string const& _name, Sort const& _sort) { for (auto s : m_solvers) - s->declareBool(_name); + s->declareVariable(_name, _sort); } void SMTPortfolio::addAssertion(Expression const& _expr) |