diff options
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; }; |