aboutsummaryrefslogtreecommitdiffstats
path: root/libsolidity/formal/SMTLib2Interface.h
diff options
context:
space:
mode:
Diffstat (limited to 'libsolidity/formal/SMTLib2Interface.h')
-rw-r--r--libsolidity/formal/SMTLib2Interface.h10
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;
};
}