[SMTChecker] Add FunctionSort and refactors the solver interface to create variables

1 files changed, 31 insertions, 29 deletions

diff --git a/libsolidity/formal/SMTLib2Interface.cpp b/libsolidity/formal/SMTLib2Interface.cpp
index 7a6b558b..bb85860f 100644
--- a/libsolidity/formal/SMTLib2Interface.cpp
+++ b/libsolidity/formal/SMTLib2Interface.cpp
@@ -47,8 +47,7 @@ void SMTLib2Interface::reset()
 {
 	m_accumulatedOutput.clear();
 	m_accumulatedOutput.emplace_back();
-	m_constants.clear();
-	m_functions.clear();
+	m_variables.clear();
 	write("(set-option :produce-models true)");
 	write("(set-logic QF_UFLIA)");
 }
@@ -64,45 +63,39 @@ void SMTLib2Interface::pop()
 	m_accumulatedOutput.pop_back();
 }
 
-void SMTLib2Interface::declareFunction(string _name, vector<SortPointer> const& _domain, Sort const& _codomain)
+void SMTLib2Interface::declareVariable(string const& _name, Sort const& _sort)
 {
+	if (_sort.kind == Kind::Function)
+		declareFunction(_name, _sort);
+	else if (!m_variables.count(_name))
+	{
+		m_variables.insert(_name);
+		write("(declare-fun |" + _name + "| () " + toSmtLibSort(_sort) + ')');
+	}
+}
+
+void SMTLib2Interface::declareFunction(string const& _name, Sort const& _sort)
+{
+	solAssert(_sort.kind == smt::Kind::Function, "");
 	// TODO Use domain and codomain as key as well
-	string domain("");
-	for (auto const& sort: _domain)
-		domain += toSmtLibSort(*sort) + ' ';
-	if (!m_functions.count(_name))
+	if (!m_variables.count(_name))
 	{
-		m_functions.insert(_name);
+		FunctionSort fSort = dynamic_cast<FunctionSort const&>(_sort);
+		string domain = toSmtLibSort(fSort.domain);
+		string codomain = toSmtLibSort(*fSort.codomain);
+		m_variables.insert(_name);
 		write(
 			"(declare-fun |" +
 			_name +
-			"| (" +
+			"| " +
 			domain +
-			") " +
-			(_codomain.kind == Kind::Int ? "Int" : "Bool") +
+			" " +
+			codomain +
 			")"
 		);
 	}
 }
 
-void SMTLib2Interface::declareInteger(string _name)
-{
-	if (!m_constants.count(_name))
-	{
-		m_constants.insert(_name);
-		write("(declare-const |" + _name + "| Int)");
-	}
-}
-
-void SMTLib2Interface::declareBool(string _name)
-{
-	if (!m_constants.count(_name))
-	{
-		m_constants.insert(_name);
-		write("(declare-const |" + _name + "| Bool)");
-	}
-}
-
 void SMTLib2Interface::addAssertion(Expression const& _expr)
 {
 	write("(assert " + toSExpr(_expr) + ")");
@@ -156,6 +149,15 @@ string SMTLib2Interface::toSmtLibSort(Sort const& _sort)
 	}
 }
 
+string SMTLib2Interface::toSmtLibSort(vector<SortPointer> const& _sorts)
+{
+	string ssort("(");
+	for (auto const& sort: _sorts)
+		ssort += toSmtLibSort(*sort) + " ";
+	ssort += ")";
+	return ssort;
+}
+
 void SMTLib2Interface::write(string _data)
 {
 	solAssert(!m_accumulatedOutput.empty(), "");