SMTChecker: Remove unused functionality

Author: blishko

libsolidity/CMakeLists.txt

@@ -137,8 +137,6 @@ set(sources
 	formal/SymbolicTypes.h
 	formal/SymbolicVariables.cpp
 	formal/SymbolicVariables.h
-	formal/VariableUsage.cpp
-	formal/VariableUsage.h
 	formal/Z3CHCSmtLib2Interface.cpp
 	formal/Z3CHCSmtLib2Interface.h
 	formal/Z3SMTLib2Interface.cpp

libsolidity/formal/BMC.cpp

@@ -80,7 +80,6 @@ void BMC::analyze(SourceUnit const& _source, std::map<ASTNode const*, std::set<V
 	m_context.setSolver(m_interface.get());
 	m_context.reset();
 	m_context.setAssertionAccumulation(true);
-	m_variableUsage.setFunctionInlining(shouldInlineFunctionCall);
 	auto const& sources = sourceDependencies(_source);
 	createFreeConstants(sources);
 	createStateVariables(sources);

libsolidity/formal/SMTEncoder.cpp

@@ -756,7 +756,6 @@ void SMTEncoder::initContract(ContractDefinition const& _contract)
 	m_context.pushSolver();
 	createStateVariables(_contract);
 	clearIndices(m_currentContract, nullptr);
-	m_variableUsage.setCurrentContract(_contract);
 	m_checked = true;
 }
 
@@ -2813,14 +2812,6 @@ Expression const* SMTEncoder::cleanExpression(Expression const& _expr)
 	return expr;
 }
 
-std::set<VariableDeclaration const*> SMTEncoder::touchedVariables(ASTNode const& _node)
-{
-	std::vector<CallableDeclaration const*> callStack;
-	for (auto const& call: m_callStack)
-		callStack.push_back(call.first);
-	return m_variableUsage.touchedVariables(_node, callStack);
-}
-
 Declaration const* SMTEncoder::expressionToDeclaration(Expression const& _expr) const
 {
 	if (auto const* identifier = dynamic_cast<Identifier const*>(&_expr))

libsolidity/formal/SMTEncoder.h

@@ -27,7 +27,6 @@
 #include <libsolidity/formal/EncodingContext.h>
 #include <libsolidity/formal/ModelCheckerSettings.h>
 #include <libsolidity/formal/SymbolicVariables.h>
-#include <libsolidity/formal/VariableUsage.h>
 
 #include <libsolidity/ast/AST.h>
 #include <libsolidity/ast/ASTVisitor.h>
@@ -454,7 +453,6 @@ class SMTEncoder: public ASTConstVisitor
 		smtutil::Expression constraints;
 	};
 
-	smt::VariableUsage m_variableUsage;
 	bool m_arrayAssignmentHappened = false;
 
 	/// Stores the instances of an Uninterpreted Function applied to arguments.