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.h | |
| 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.h')
| -rw-r--r-- | libsolidity/formal/SMTLib2Interface.h | 6 |
1 files changed, 4 insertions, 2 deletions
diff --git a/libsolidity/formal/SMTLib2Interface.h b/libsolidity/formal/SMTLib2Interface.h index 957f2ea4..b8dac366 100644 --- a/libsolidity/formal/SMTLib2Interface.h +++ b/libsolidity/formal/SMTLib2Interface.h @@ -17,7 +17,6 @@ #pragma once -#include <libsolidity/formal/SMTSolverCommunicator.h> #include <libsolidity/formal/SolverInterface.h> #include <libsolidity/interface/Exceptions.h> @@ -64,7 +63,10 @@ private: std::string checkSatAndGetValuesCommand(std::vector<Expression> const& _expressionsToEvaluate); std::vector<std::string> parseValues(std::string::const_iterator _start, std::string::const_iterator _end); - SMTSolverCommunicator m_communicator; + /// Communicates with the solver via the callback. Throws SMTSolverError on error. + std::string querySolver(std::string const& _input); + + ReadCallback::Callback m_queryCallback; std::vector<std::string> m_accumulatedOutput; }; |