diff options
| author | chriseth <chris@ethereum.org> | 2018-12-06 00:28:45 +0800 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2018-12-06 00:28:45 +0800 |
| commit | 63d67c715326209ba1dc2c3800db90830d2c4e13 (patch) | |
| tree | 0f15bc31619549cc4908278b580ad38d63a1ce2d /libsolidity/formal/SymbolicVariables.cpp | |
| parent | 57eb68a8df84e8d746214f0faac74a16dab65881 (diff) | |
| parent | b9f424e37337a6d719e3d50106034050743979b8 (diff) | |
| download | dexon-solidity-63d67c715326209ba1dc2c3800db90830d2c4e13.tar dexon-solidity-63d67c715326209ba1dc2c3800db90830d2c4e13.tar.gz dexon-solidity-63d67c715326209ba1dc2c3800db90830d2c4e13.tar.bz2 dexon-solidity-63d67c715326209ba1dc2c3800db90830d2c4e13.tar.lz dexon-solidity-63d67c715326209ba1dc2c3800db90830d2c4e13.tar.xz dexon-solidity-63d67c715326209ba1dc2c3800db90830d2c4e13.tar.zst dexon-solidity-63d67c715326209ba1dc2c3800db90830d2c4e13.zip | |
Merge pull request #5591 from ethereum/smt_simplify_sort
[SMTChecker] Simplify symbolic variables
Diffstat (limited to 'libsolidity/formal/SymbolicVariables.cpp')
| -rw-r--r-- | libsolidity/formal/SymbolicVariables.cpp | 26 |
1 files changed, 16 insertions, 10 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 |