cerc-io/solidity
11
0
Fork 0
mirror of https://github.com/ethereum/solidity synced 2023-10-03 13:03:40 +00:00
Code Issues Actions Packages Projects Releases Wiki Activity

Merge pull request #5591 from ethereum/smt_simplify_sort

Browse Source 
[SMTChecker] Simplify symbolic variables
This commit is contained in:
chriseth
2018-12-05 17:28:45 +01:00
committed by GitHub
parent 57eb68a8df b9f424e373
commit 63d67c7153
2 changed files with 19 additions and 29 deletions
Download Patch File Download Diff File Expand all files Collapse all files
libsolidity/formal/SymbolicVariables.cpp
+16 -10
View File
@@ -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
libsolidity/formal/SymbolicVariables.h
+3 -19
View File
@@ -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;
};
/**