cerc-io/solidity
10
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

Remove repeated declarations in Z3 and CVC4 as well

Browse Source
This commit is contained in:
Leonardo Alt 2018-08-01 11:12:56 +02:00
parent f249f9c86f
commit 41ac3d6cfb
2 changed files with 15 additions and 7 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

5
libsolidity/formal/CVC4Interface.cpp
View File

@ -52,17 +52,22 @@ void CVC4Interface::pop()
void CVC4Interface::declareFunction(string _name, Sort _domain, Sort _codomain) void CVC4Interface::declareFunction(string _name, Sort _domain, Sort _codomain)
{ {
if (!m_functions.count(_name))
{
CVC4::Type fType = m_context.mkFunctionType(cvc4Sort(_domain), cvc4Sort(_codomain)); CVC4::Type fType = m_context.mkFunctionType(cvc4Sort(_domain), cvc4Sort(_codomain));
m_functions.insert({_name, m_context.mkVar(_name.c_str(), fType)}); m_functions.insert({_name, m_context.mkVar(_name.c_str(), fType)});
}
} }
void CVC4Interface::declareInteger(string _name) void CVC4Interface::declareInteger(string _name)
{ {
if (!m_constants.count(_name))
m_constants.insert({_name, m_context.mkVar(_name.c_str(), m_context.integerType())}); m_constants.insert({_name, m_context.mkVar(_name.c_str(), m_context.integerType())});
} }
void CVC4Interface::declareBool(string _name) void CVC4Interface::declareBool(string _name)
{ {
if (!m_constants.count(_name))
m_constants.insert({_name, m_context.mkVar(_name.c_str(), m_context.booleanType())}); m_constants.insert({_name, m_context.mkVar(_name.c_str(), m_context.booleanType())});
} }

3
libsolidity/formal/Z3Interface.cpp
View File

@ -53,16 +53,19 @@ void Z3Interface::pop()
void Z3Interface::declareFunction(string _name, Sort _domain, Sort _codomain) void Z3Interface::declareFunction(string _name, Sort _domain, Sort _codomain)
{ {
if (!m_functions.count(_name))
m_functions.insert({_name, m_context.function(_name.c_str(), z3Sort(_domain), z3Sort(_codomain))}); m_functions.insert({_name, m_context.function(_name.c_str(), z3Sort(_domain), z3Sort(_codomain))});
} }
void Z3Interface::declareInteger(string _name) void Z3Interface::declareInteger(string _name)
{ {
if (!m_constants.count(_name))
m_constants.insert({_name, m_context.int_const(_name.c_str())}); m_constants.insert({_name, m_context.int_const(_name.c_str())});
} }
void Z3Interface::declareBool(string _name) void Z3Interface::declareBool(string _name)
{ {
if (!m_constants.count(_name))
m_constants.insert({_name, m_context.bool_const(_name.c_str())}); m_constants.insert({_name, m_context.bool_const(_name.c_str())});
} }