Merge pull request #5571 from ethereum/develop

Version 0.5.1

1 files changed, 15 insertions, 8 deletions

diff --git a/libsolidity/formal/SMTLib2Interface.h b/libsolidity/formal/SMTLib2Interface.h
index eb876a7f..55fc4096 100644
--- a/libsolidity/formal/SMTLib2Interface.h
+++ b/libsolidity/formal/SMTLib2Interface.h
@@ -19,9 +19,11 @@
 
 #include <libsolidity/formal/SolverInterface.h>
 
-#include <libsolidity/interface/Exceptions.h>
+#include <liblangutil/Exceptions.h>
 #include <libsolidity/interface/ReadFile.h>
 
+#include <libdevcore/FixedHash.h>
+
 #include <libdevcore/Common.h>
 
 #include <boost/noncopyable.hpp>
@@ -42,22 +44,26 @@ namespace smt
 class SMTLib2Interface: public SolverInterface, public boost::noncopyable
 {
 public:
-	explicit SMTLib2Interface(ReadCallback::Callback const& _queryCallback);
+	explicit SMTLib2Interface(std::map<h256, std::string> const& _queryResponses);
 
 	void reset() override;
 
 	void push() override;
 	void pop() override;
 
-	void declareFunction(std::string _name, Sort _domain, Sort _codomain) override;
-	void declareInteger(std::string _name) override;
-	void declareBool(std::string _name) override;
+	void declareVariable(std::string const&, Sort const&) override;
 
 	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&);
+
 	std::string toSExpr(Expression const& _expr);
+	std::string toSmtLibSort(Sort const& _sort);
+	std::string toSmtLibSort(std::vector<SortPointer> const& _sort);
 
 	void write(std::string _data);
 
@@ -67,10 +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::vector<std::string> m_accumulatedOutput;
-	std::set<std::string> m_constants;
-	std::set<std::string> m_functions;
+	std::set<std::string> m_variables;
+
+	std::map<h256, std::string> const& m_queryResponses;
+	std::vector<std::string> m_unhandledQueries;
 };
 
 }