Inject SMTLIB2 queries and responses via standard-json-io.

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