[SMTChecker] Simplify symbolic variables

2 files changed, 19 insertions, 29 deletions

diff --git a/libsolidity/formal/SymbolicVariables.cpp b/libsolidity/formal/SymbolicVariables.cpp
index efaeb97a..f7d2a119 100644
--- a/libsolidity/formal/SymbolicVariables.cpp
+++ b/libsolidity/formal/SymbolicVariables.cpp
@@ -37,16 +37,32 @@ SymbolicVariable::SymbolicVariable(
 {
 }
 
+smt::Expression SymbolicVariable::currentValue() const
+{
+	return valueAtIndex(m_ssa->index());
+}
+
 string SymbolicVariable::currentName() const
 {
 	return uniqueSymbol(m_ssa->index());
 }
 
+smt::Expression SymbolicVariable::valueAtIndex(int _index) const
+{
+	return m_interface.newVariable(uniqueSymbol(_index), smtSort(*m_type));
+}
+
 string SymbolicVariable::uniqueSymbol(unsigned _index) const
 {
 	return m_uniqueName + "_" + to_string(_index);
 }
 
+smt::Expression SymbolicVariable::increaseIndex()
+{
+	++(*m_ssa);
+	return currentValue();
+}
+
 SymbolicBoolVariable::SymbolicBoolVariable(
 	TypePointer _type,
 	string const& _uniqueName,
@@ -57,11 +73,6 @@ SymbolicBoolVariable::SymbolicBoolVariable(
 	solAssert(m_type->category() == Type::Category::Bool, "");
 }
 
-smt::Expression SymbolicBoolVariable::valueAtIndex(int _index) const
-{
-	return m_interface.newVariable(uniqueSymbol(_index), make_shared<smt::Sort>(smt::Kind::Bool));
-}
-
 SymbolicIntVariable::SymbolicIntVariable(
 	TypePointer _type,
 	string const& _uniqueName,
@@ -72,11 +83,6 @@ SymbolicIntVariable::SymbolicIntVariable(
 	solAssert(isNumber(m_type->category()), "");
 }
 
-smt::Expression SymbolicIntVariable::valueAtIndex(int _index) const
-{
-	return m_interface.newVariable(uniqueSymbol(_index), make_shared<smt::Sort>(smt::Kind::Int));
-}
-
 SymbolicAddressVariable::SymbolicAddressVariable(
 	string const& _uniqueName,
 	smt::SolverInterface& _interface
diff --git a/libsolidity/formal/SymbolicVariables.h b/libsolidity/formal/SymbolicVariables.h
index fcf32760..ef40944c 100644
--- a/libsolidity/formal/SymbolicVariables.h
+++ b/libsolidity/formal/SymbolicVariables.h
@@ -46,20 +46,10 @@ public:
 
 	virtual ~SymbolicVariable() = default;
 
-	smt::Expression currentValue() const
-	{
-		return valueAtIndex(m_ssa->index());
-	}
-
+	smt::Expression currentValue() const;
 	std::string currentName() const;
-
-	virtual smt::Expression valueAtIndex(int _index) const = 0;
-
-	smt::Expression increaseIndex()
-	{
-		++(*m_ssa);
-		return currentValue();
-	}
+	virtual smt::Expression valueAtIndex(int _index) const;
+	smt::Expression increaseIndex();
 
 	unsigned index() const { return m_ssa->index(); }
 	unsigned& index() { return m_ssa->index(); }
@@ -86,9 +76,6 @@ public:
 		std::string const& _uniqueName,
 		smt::SolverInterface& _interface
 	);
-
-protected:
-	smt::Expression valueAtIndex(int _index) const;
 };
 
 /**
@@ -102,9 +89,6 @@ public:
 		std::string const& _uniqueName,
 		smt::SolverInterface& _interface
 	);
-
-protected:
-	smt::Expression valueAtIndex(int _index) const;
 };
 
 /**