1 files changed, 12 insertions, 115 deletions

diff --git a/libsolidity/formal/SMTLib2Interface.h b/libsolidity/formal/SMTLib2Interface.h
index d8c11df9..5755ae3f 100644
--- a/libsolidity/formal/SMTLib2Interface.h
+++ b/libsolidity/formal/SMTLib2Interface.h
@@ -18,6 +18,7 @@
 #pragma once
 
 #include <libsolidity/formal/SMTSolverCommunicator.h>
+#include <libsolidity/formal/SolverInterface.h>
 
 #include <libsolidity/interface/Exceptions.h>
 #include <libsolidity/interface/ReadFile.h>
@@ -38,129 +39,26 @@ namespace solidity
 namespace smt
 {
 
-enum class CheckResult
-{
-	SAT, UNSAT, UNKNOWN, ERROR
-};
-
-enum class Sort
-{
-	Int, Bool
-};
-
-/// C++ representation of an SMTLIB2 expression.
-class Expression
-{
-	friend class SMTLib2Interface;
-	/// Manual constructor, should only be used by SMTLib2Interface and the class itself.
-	Expression(std::string _name, std::vector<Expression> _arguments):
-		m_name(std::move(_name)), m_arguments(std::move(_arguments)) {}
-
-public:
-	Expression(size_t _number): m_name(std::to_string(_number)) {}
-	Expression(u256 const& _number): m_name(_number.str()) {}
-	Expression(bigint const& _number): m_name(_number.str()) {}
-
-	Expression(Expression const& _other) = default;
-	Expression(Expression&& _other) = default;
-	Expression& operator=(Expression const& _other) = default;
-	Expression& operator=(Expression&& _other) = default;
-
-	friend Expression operator!(Expression _a)
-	{
-		return Expression("not", std::move(_a));
-	}
-	friend Expression operator&&(Expression _a, Expression _b)
-	{
-		return Expression("and", std::move(_a), std::move(_b));
-	}
-	friend Expression operator||(Expression _a, Expression _b)
-	{
-		return Expression("or", std::move(_a), std::move(_b));
-	}
-	friend Expression operator==(Expression _a, Expression _b)
-	{
-		return Expression("=", std::move(_a), std::move(_b));
-	}
-	friend Expression operator!=(Expression _a, Expression _b)
-	{
-		return !(std::move(_a) == std::move(_b));
-	}
-	friend Expression operator<(Expression _a, Expression _b)
-	{
-		return Expression("<", std::move(_a), std::move(_b));
-	}
-	friend Expression operator<=(Expression _a, Expression _b)
-	{
-		return Expression("<=", std::move(_a), std::move(_b));
-	}
-	friend Expression operator>(Expression _a, Expression _b)
-	{
-		return Expression(">", std::move(_a), std::move(_b));
-	}
-	friend Expression operator>=(Expression _a, Expression _b)
-	{
-		return Expression(">=", std::move(_a), std::move(_b));
-	}
-	friend Expression operator+(Expression _a, Expression _b)
-	{
-		return Expression("+", std::move(_a), std::move(_b));
-	}
-	friend Expression operator-(Expression _a, Expression _b)
-	{
-		return Expression("-", std::move(_a), std::move(_b));
-	}
-	friend Expression operator*(Expression _a, Expression _b)
-	{
-		return Expression("*", std::move(_a), std::move(_b));
-	}
-	Expression operator()(Expression _a) const
-	{
-		solAssert(m_arguments.empty(), "Attempted function application to non-function.");
-		return Expression(m_name, _a);
-	}
-
-	std::string toSExpr() const
-	{
-		if (m_arguments.empty())
-			return m_name;
-		std::string sexpr = "(" + m_name;
-		for (auto const& arg: m_arguments)
-			sexpr += " " + arg.toSExpr();
-		sexpr += ")";
-		return sexpr;
-	}
-
-private:
-	explicit Expression(std::string _name):
-		Expression(std::move(_name), std::vector<Expression>{}) {}
-	Expression(std::string _name, Expression _arg):
-		Expression(std::move(_name), std::vector<Expression>{std::move(_arg)}) {}
-	Expression(std::string _name, Expression _arg1, Expression _arg2):
-		Expression(std::move(_name), std::vector<Expression>{std::move(_arg1), std::move(_arg2)}) {}
-
-	std::string const m_name;
-	std::vector<Expression> const m_arguments;
-};
-
-class SMTLib2Interface: public boost::noncopyable
+class SMTLib2Interface: public SolverInterface, public boost::noncopyable
 {
 public:
 	SMTLib2Interface(ReadFile::Callback const& _readFileCallback);
 
-	void reset();
+	void reset() override;
 
-	void push();
-	void pop();
+	void push() override;
+	void pop() override;
 
-	Expression newFunction(std::string _name, Sort _domain, Sort _codomain);
-	Expression newInteger(std::string _name);
-	Expression newBool(std::string _name);
+	Expression newFunction(std::string _name, Sort _domain, Sort _codomain) override;
+	Expression newInteger(std::string _name) override;
+	Expression newBool(std::string _name) override;
 
-	void addAssertion(Expression const& _expr);
-	std::pair<CheckResult, std::vector<std::string>> check(std::vector<Expression> const& _expressionsToEvaluate);
+	void addAssertion(Expression const& _expr) override;
+	std::pair<CheckResult, std::vector<std::string>> check(std::vector<Expression> const& _expressionsToEvaluate) override;
 
 private:
+	std::string toSExpr(Expression const& _expr);
+
 	void write(std::string _data);
 
 	std::string checkSatAndGetValuesCommand(std::vector<Expression> const& _expressionsToEvaluate);
@@ -170,7 +68,6 @@ private:
 	std::vector<std::string> m_accumulatedOutput;
 };
 
-
 }
 }
 }