[SMTChecker] Refactor setZeroValue and setUnknownValue

1 files changed, 3 insertions, 18 deletions

diff --git a/libsolidity/formal/SymbolicVariables.h b/libsolidity/formal/SymbolicVariables.h
index 13b944a5..fcf32760 100644
--- a/libsolidity/formal/SymbolicVariables.h
+++ b/libsolidity/formal/SymbolicVariables.h
@@ -64,20 +64,15 @@ public:
 	unsigned index() const { return m_ssa->index(); }
 	unsigned& index() { return m_ssa->index(); }
 
-	/// Sets the var to the default value of its type.
-	/// Inherited types must implement.
-	virtual void setZeroValue() = 0;
-	/// The unknown value is the full range of valid values.
-	/// It is sub-type dependent, but not mandatory.
-	virtual void setUnknownValue() {}
+	TypePointer const& type() const { return m_type; }
 
 protected:
 	std::string uniqueSymbol(unsigned _index) const;
 
-	TypePointer m_type = nullptr;
+	TypePointer m_type;
 	std::string m_uniqueName;
 	smt::SolverInterface& m_interface;
-	std::shared_ptr<SSAVariable> m_ssa = nullptr;
+	std::shared_ptr<SSAVariable> m_ssa;
 };
 
 /**
@@ -92,11 +87,6 @@ public:
 		smt::SolverInterface& _interface
 	);
 
-	/// Sets the var to false.
-	void setZeroValue();
-	/// Does nothing since the SMT solver already knows the valid values for Bool.
-	void setUnknownValue();
-
 protected:
 	smt::Expression valueAtIndex(int _index) const;
 };
@@ -113,11 +103,6 @@ public:
 		smt::SolverInterface& _interface
 	);
 
-	/// Sets the var to 0.
-	void setZeroValue();
-	/// Sets the variable to the full valid value range.
-	void setUnknownValue();
-
 protected:
 	smt::Expression valueAtIndex(int _index) const;
 };