diff options
Diffstat (limited to 'libsolidity/formal/SMTLib2Interface.cpp')
| -rw-r--r-- | libsolidity/formal/SMTLib2Interface.cpp | 14 |
1 files changed, 13 insertions, 1 deletions
diff --git a/libsolidity/formal/SMTLib2Interface.cpp b/libsolidity/formal/SMTLib2Interface.cpp index 4b118abc..e7a9ef8c 100644 --- a/libsolidity/formal/SMTLib2Interface.cpp +++ b/libsolidity/formal/SMTLib2Interface.cpp @@ -95,10 +95,11 @@ void SMTLib2Interface::addAssertion(Expression const& _expr) pair<CheckResult, vector<string>> SMTLib2Interface::check(vector<Expression> const& _expressionsToEvaluate) { - string response = m_communicator.communicate( + string response = querySolver( boost::algorithm::join(m_accumulatedOutput, "\n") + checkSatAndGetValuesCommand(_expressionsToEvaluate) ); + CheckResult result; // TODO proper parsing if (boost::starts_with(response, "sat\n")) @@ -173,3 +174,14 @@ vector<string> SMTLib2Interface::parseValues(string::const_iterator _start, stri return values; } + +string SMTLib2Interface::querySolver(string const& _input) +{ + if (!m_queryCallback) + BOOST_THROW_EXCEPTION(SolverError() << errinfo_comment("No SMT solver available.")); + + ReadCallback::Result queryResult = m_queryCallback(_input); + if (!queryResult.success) + BOOST_THROW_EXCEPTION(SolverError() << errinfo_comment(queryResult.responseOrErrorMessage)); + return queryResult.responseOrErrorMessage; +} |