Introduce sorts for smt expressions.

3 files changed, 37 insertions, 48 deletions

diff --git a/libsolidity/formal/SMTLib2Interface.cpp b/libsolidity/formal/SMTLib2Interface.cpp
index c627057a..0e00665a 100644
--- a/libsolidity/formal/SMTLib2Interface.cpp
+++ b/libsolidity/formal/SMTLib2Interface.cpp
@@ -64,8 +64,6 @@ void SMTLib2Interface::pop()
 
 Expression SMTLib2Interface::newFunction(string _name, Sort _domain, Sort _codomain)
 {
-	solAssert(!m_variables.count(_name), "");
-	m_variables[_name] = SMTVariableType::Function;
 	write(
 		"(declare-fun |" +
 		_name +
@@ -80,16 +78,12 @@ Expression SMTLib2Interface::newFunction(string _name, Sort _domain, Sort _codom
 
 Expression SMTLib2Interface::newInteger(string _name)
 {
-	solAssert(!m_variables.count(_name), "");
-	m_variables[_name] = SMTVariableType::Integer;
 	write("(declare-const |" + _name + "| Int)");
 	return SolverInterface::newInteger(move(_name));
 }
 
 Expression SMTLib2Interface::newBool(string _name)
 {
-	solAssert(!m_variables.count(_name), "");
-	m_variables[_name] = SMTVariableType::Bool;
 	write("(declare-const |" + _name + "| Bool)");
 	return SolverInterface::newBool(std::move(_name));
 }
@@ -151,9 +145,8 @@ string SMTLib2Interface::checkSatAndGetValuesCommand(vector<Expression> const& _
 		for (size_t i = 0; i < _expressionsToEvaluate.size(); i++)
 		{
 			auto const& e = _expressionsToEvaluate.at(i);
-			solAssert(m_variables.count(e.name), "");
-			solAssert(m_variables[e.name] == SMTVariableType::Integer, "");
-			command += "(declare-const |EVALEXPR_" + to_string(i) + "| Int)\n";
+			solAssert(e.sort == Sort::Int || e.sort == Sort::Bool, "Invalid sort for expression to evaluate.");
+			command += "(declare-const |EVALEXPR_" + to_string(i) + "| " + (e.sort == Sort::Int ? "Int" : "Bool") + "\n";
 			command += "(assert (= |EVALEXPR_" + to_string(i) + "| " + toSExpr(e) + "))\n";
 		}
 		command += "(check-sat)\n";
diff --git a/libsolidity/formal/SMTLib2Interface.h b/libsolidity/formal/SMTLib2Interface.h
index e827449f..63188acd 100644
--- a/libsolidity/formal/SMTLib2Interface.h
+++ b/libsolidity/formal/SMTLib2Interface.h
@@ -68,14 +68,6 @@ private:
 
 	ReadCallback::Callback m_queryCallback;
 	std::vector<std::string> m_accumulatedOutput;
-
-	enum class SMTVariableType {
-		Function,
-		Integer,
-		Bool
-	};
-
-	std::map<std::string,SMTVariableType> m_variables;
 };
 
 }
diff --git a/libsolidity/formal/SolverInterface.h b/libsolidity/formal/SolverInterface.h
index a69d19d5..ac722dad 100644
--- a/libsolidity/formal/SolverInterface.h
+++ b/libsolidity/formal/SolverInterface.h
@@ -44,7 +44,7 @@ enum class CheckResult
 
 enum class Sort
 {
-	Int, Bool
+	Int, Bool, IntIntFun
 };
 
 /// C++ representation of an SMTLIB2 expression.
@@ -52,10 +52,10 @@ class Expression
 {
 	friend class SolverInterface;
 public:
-	explicit Expression(bool _v): name(_v ? "true" : "false") {}
-	Expression(size_t _number): name(std::to_string(_number)) {}
-	Expression(u256 const& _number): name(_number.str()) {}
-	Expression(bigint const& _number): name(_number.str()) {}
+	explicit Expression(bool _v): name(_v ? "true" : "false"), sort(Sort::Bool) {}
+	Expression(size_t _number): name(std::to_string(_number)), sort(Sort::Int) {}
+	Expression(u256 const& _number): name(_number.str()), sort(Sort::Int) {}
+	Expression(bigint const& _number): name(_number.str()), sort(Sort::Int) {}
 
 	Expression(Expression const&) = default;
 	Expression(Expression&&) = default;
@@ -64,26 +64,27 @@ public:
 
 	static Expression ite(Expression _condition, Expression _trueValue, Expression _falseValue)
 	{
+		solAssert(_trueValue.sort == _falseValue.sort, "");
 		return Expression("ite", std::vector<Expression>{
 			std::move(_condition), std::move(_trueValue), std::move(_falseValue)
-		});
+		}, _trueValue.sort);
 	}
 
 	friend Expression operator!(Expression _a)
 	{
-		return Expression("not", std::move(_a));
+		return Expression("not", std::move(_a), Sort::Bool);
 	}
 	friend Expression operator&&(Expression _a, Expression _b)
 	{
-		return Expression("and", std::move(_a), std::move(_b));
+		return Expression("and", std::move(_a), std::move(_b), Sort::Bool);
 	}
 	friend Expression operator||(Expression _a, Expression _b)
 	{
-		return Expression("or", std::move(_a), std::move(_b));
+		return Expression("or", std::move(_a), std::move(_b), Sort::Bool);
 	}
 	friend Expression operator==(Expression _a, Expression _b)
 	{
-		return Expression("=", std::move(_a), std::move(_b));
+		return Expression("=", std::move(_a), std::move(_b), Sort::Bool);
 	}
 	friend Expression operator!=(Expression _a, Expression _b)
 	{
@@ -91,52 +92,54 @@ public:
 	}
 	friend Expression operator<(Expression _a, Expression _b)
 	{
-		return Expression("<", std::move(_a), std::move(_b));
+		return Expression("<", std::move(_a), std::move(_b), Sort::Bool);
 	}
 	friend Expression operator<=(Expression _a, Expression _b)
 	{
-		return Expression("<=", std::move(_a), std::move(_b));
+		return Expression("<=", std::move(_a), std::move(_b), Sort::Bool);
 	}
 	friend Expression operator>(Expression _a, Expression _b)
 	{
-		return Expression(">", std::move(_a), std::move(_b));
+		return Expression(">", std::move(_a), std::move(_b), Sort::Bool);
 	}
 	friend Expression operator>=(Expression _a, Expression _b)
 	{
-		return Expression(">=", std::move(_a), std::move(_b));
+		return Expression(">=", std::move(_a), std::move(_b), Sort::Bool);
 	}
 	friend Expression operator+(Expression _a, Expression _b)
 	{
-		return Expression("+", std::move(_a), std::move(_b));
+		return Expression("+", std::move(_a), std::move(_b), Sort::Int);
 	}
 	friend Expression operator-(Expression _a, Expression _b)
 	{
-		return Expression("-", std::move(_a), std::move(_b));
+		return Expression("-", std::move(_a), std::move(_b), Sort::Int);
 	}
 	friend Expression operator*(Expression _a, Expression _b)
 	{
-		return Expression("*", std::move(_a), std::move(_b));
+		return Expression("*", std::move(_a), std::move(_b), Sort::Int);
 	}
 	Expression operator()(Expression _a) const
 	{
+		solAssert(sort == Sort::IntIntFun, "Attempted function application to non-function.");
 		solAssert(arguments.empty(), "Attempted function application to non-function.");
-		return Expression(name, _a);
+		return Expression(name, _a, Sort::Int);
 	}
 
 	std::string const name;
 	std::vector<Expression> const arguments;
+	Sort sort;
 
 private:
 	/// Manual constructor, should only be used by SolverInterface and this class itself.
-	Expression(std::string _name, std::vector<Expression> _arguments):
-		name(std::move(_name)), arguments(std::move(_arguments)) {}
-
-	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)}) {}
+	Expression(std::string _name, std::vector<Expression> _arguments, Sort _sort):
+		name(std::move(_name)), arguments(std::move(_arguments)), sort(_sort) {}
+
+	explicit Expression(std::string _name, Sort _sort):
+		Expression(std::move(_name), std::vector<Expression>{}, _sort) {}
+	Expression(std::string _name, Expression _arg, Sort _sort):
+		Expression(std::move(_name), std::vector<Expression>{std::move(_arg)}, _sort) {}
+	Expression(std::string _name, Expression _arg1, Expression _arg2, Sort _sort):
+		Expression(std::move(_name), std::vector<Expression>{std::move(_arg1), std::move(_arg2)}, _sort) {}
 };
 
 DEV_SIMPLE_EXCEPTION(SolverError);
@@ -149,20 +152,21 @@ public:
 	virtual void push() = 0;
 	virtual void pop() = 0;
 
-	virtual Expression newFunction(std::string _name, Sort /*_domain*/, Sort /*_codomain*/)
+	virtual Expression newFunction(std::string _name, Sort _domain, Sort _codomain)
 	{
+		solAssert(_domain == Sort::Int && _codomain == Sort::Int, "Function sort not supported.");
 		// Subclasses should do something here
-		return Expression(std::move(_name), {});
+		return Expression(std::move(_name), {}, Sort::IntIntFun);
 	}
 	virtual Expression newInteger(std::string _name)
 	{
 		// Subclasses should do something here
-		return Expression(std::move(_name), {});
+		return Expression(std::move(_name), {}, Sort::Int);
 	}
 	virtual Expression newBool(std::string _name)
 	{
 		// Subclasses should do something here
-		return Expression(std::move(_name), {});
+		return Expression(std::move(_name), {}, Sort::Bool);
 	}
 
 	virtual void addAssertion(Expression const& _expr) = 0;