diff options
| author | chriseth <chris@ethereum.org> | 2017-07-14 03:06:29 +0800 |
|---|---|---|
| committer | chriseth <chris@ethereum.org> | 2017-08-23 23:37:35 +0800 |
| commit | 1e05ebe50e0530beb62c96fc1112e935a5b11473 (patch) | |
| tree | 922b4aa1cb0d862d6c744e63243dfd4ef47ff869 /libsolidity/formal/SMTLib2Interface.cpp | |
| parent | 9ac2ac14c1819be2341c6947245bf63b02795528 (diff) | |
| download | dexon-solidity-1e05ebe50e0530beb62c96fc1112e935a5b11473.tar dexon-solidity-1e05ebe50e0530beb62c96fc1112e935a5b11473.tar.gz dexon-solidity-1e05ebe50e0530beb62c96fc1112e935a5b11473.tar.bz2 dexon-solidity-1e05ebe50e0530beb62c96fc1112e935a5b11473.tar.lz dexon-solidity-1e05ebe50e0530beb62c96fc1112e935a5b11473.tar.xz dexon-solidity-1e05ebe50e0530beb62c96fc1112e935a5b11473.tar.zst dexon-solidity-1e05ebe50e0530beb62c96fc1112e935a5b11473.zip | |
Refactor Z3 read callback.
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; +} |