diff options
| author | Leonardo Alt <leo@ethereum.org> | 2018-12-05 16:56:52 +0800 |
|---|---|---|
| committer | Leonardo Alt <leo@ethereum.org> | 2018-12-05 16:56:52 +0800 |
| commit | b9f424e37337a6d719e3d50106034050743979b8 (patch) | |
| tree | efcf84313c3095157065cf9d248dee13e998a0ce /libsolidity/formal/SymbolicVariables.h | |
| parent | 6efe2a526691f42e83b11cf670ec3e7f51927b3e (diff) | |
| download | dexon-solidity-b9f424e37337a6d719e3d50106034050743979b8.tar dexon-solidity-b9f424e37337a6d719e3d50106034050743979b8.tar.gz dexon-solidity-b9f424e37337a6d719e3d50106034050743979b8.tar.bz2 dexon-solidity-b9f424e37337a6d719e3d50106034050743979b8.tar.lz dexon-solidity-b9f424e37337a6d719e3d50106034050743979b8.tar.xz dexon-solidity-b9f424e37337a6d719e3d50106034050743979b8.tar.zst dexon-solidity-b9f424e37337a6d719e3d50106034050743979b8.zip | |
[SMTChecker] Simplify symbolic variables
Diffstat (limited to 'libsolidity/formal/SymbolicVariables.h')
| -rw-r--r-- | libsolidity/formal/SymbolicVariables.h | 22 |
1 files changed, 3 insertions, 19 deletions
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; }; /** |