[SMTChecker] A little refactoring on SSA vars

1 files changed, 4 insertions, 8 deletions

diff --git a/libsolidity/formal/SMTChecker.h b/libsolidity/formal/SMTChecker.h
index b57f0f96..7481e1c8 100644
--- a/libsolidity/formal/SMTChecker.h
+++ b/libsolidity/formal/SMTChecker.h
@@ -20,6 +20,8 @@
 
 #include <libsolidity/formal/SolverInterface.h>
 
+#include <libsolidity/formal/SSAVariable.h>
+
 #include <libsolidity/ast/ASTVisitor.h>
 
 #include <libsolidity/interface/ReadFile.h>
@@ -76,7 +78,7 @@ private:
 	void assignment(Declaration const& _variable, smt::Expression const& _value, SourceLocation const& _location);
 
 	/// Maps a variable to an SSA index.
-	using VariableSequenceCounters = std::map<Declaration const*, int>;
+	using VariableSequenceCounters = std::map<Declaration const*, SSAVariable>;
 
 	/// Visits the branch given by the statement, pushes and pops the current path conditions.
 	/// @param _condition if present, asserts that this condition is true within the branch.
@@ -118,7 +120,6 @@ private:
 	/// This fails if the type is not supported.
 	bool createVariable(VariableDeclaration const& _varDecl);
 
-	static std::string uniqueSymbol(Declaration const& _decl);
 	static std::string uniqueSymbol(Expression const& _expr);
 
 	/// @returns true if _delc is a variable that is known at the current point, i.e.
@@ -148,9 +149,6 @@ private:
 	void createExpr(Expression const& _e);
 	/// Creates the expression and sets its value.
 	void defineExpr(Expression const& _e, smt::Expression _value);
-	/// Returns the function declaration corresponding to the given variable.
-	/// The function takes one argument which is the "sequence number".
-	smt::Expression var(Declaration const& _decl);
 
 	/// Adds a new path condition
 	void pushPathCondition(smt::Expression const& _e);
@@ -166,10 +164,8 @@ private:
 	std::shared_ptr<smt::SolverInterface> m_interface;
 	std::shared_ptr<VariableUsage> m_variableUsage;
 	bool m_conditionalExecutionHappened = false;
-	std::map<Declaration const*, int> m_currentSequenceCounter;
-	std::map<Declaration const*, int> m_nextFreeSequenceCounter;
 	std::map<Expression const*, smt::Expression> m_expressions;
-	std::map<Declaration const*, smt::Expression> m_variables;
+	std::map<Declaration const*, SSAVariable> m_variables;
 	std::vector<smt::Expression> m_pathConditions;
 	ErrorReporter& m_errorReporter;