diff options
Diffstat (limited to 'libsolidity/formal/SMTLib2Interface.h')
-rw-r--r-- | libsolidity/formal/SMTLib2Interface.h | 10 |
1 files changed, 8 insertions, 2 deletions
diff --git a/libsolidity/formal/SMTLib2Interface.h b/libsolidity/formal/SMTLib2Interface.h index 4f72d27c..c67101ae 100644 --- a/libsolidity/formal/SMTLib2Interface.h +++ b/libsolidity/formal/SMTLib2Interface.h @@ -22,6 +22,8 @@ #include <liblangutil/Exceptions.h> #include <libsolidity/interface/ReadFile.h> +#include <libdevcore/FixedHash.h> + #include <libdevcore/Common.h> #include <boost/noncopyable.hpp> @@ -42,7 +44,7 @@ namespace smt class SMTLib2Interface: public SolverInterface, public boost::noncopyable { public: - explicit SMTLib2Interface(ReadCallback::Callback const& _queryCallback); + explicit SMTLib2Interface(std::map<h256, std::string> const& _smtlib2Responses); void reset() override; @@ -54,6 +56,8 @@ public: void addAssertion(Expression const& _expr) override; std::pair<CheckResult, std::vector<std::string>> check(std::vector<Expression> const& _expressionsToEvaluate) override; + std::vector<std::string> unhandledQueries() override { return m_unhandledQueries; } + private: void declareFunction(std::string const&, Sort const&); @@ -69,9 +73,11 @@ private: /// Communicates with the solver via the callback. Throws SMTSolverError on error. std::string querySolver(std::string const& _input); - ReadCallback::Callback m_queryCallback; + std::map<h256, std::string> const& m_smtlib2Responses; std::vector<std::string> m_accumulatedOutput; std::set<std::string> m_variables; + + std::vector<std::string> m_unhandledQueries; }; } |