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

[SMTLib2] Fix repeated declarations

Browse Source
This commit is contained in:
Leonardo Alt 2018-04-17 23:46:53 +02:00 committed by Alex Beregszaszi
parent e56a88be37
commit f249f9c86f
2 changed files with 29 additions and 11 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

15
libsolidity/formal/SMTLib2Interface.cpp
View File

@ -47,6 +47,8 @@ void SMTLib2Interface::reset()
{ {
m_accumulatedOutput.clear(); m_accumulatedOutput.clear();
m_accumulatedOutput.emplace_back(); m_accumulatedOutput.emplace_back();
m_constants.clear();
m_functions.clear();
write("(set-option :produce-models true)"); write("(set-option :produce-models true)");
write("(set-logic QF_UFLIA)"); write("(set-logic QF_UFLIA)");
} }
@ -64,6 +66,10 @@ void SMTLib2Interface::pop()
void SMTLib2Interface::declareFunction(string _name, Sort _domain, Sort _codomain) void SMTLib2Interface::declareFunction(string _name, Sort _domain, Sort _codomain)
{ {
// TODO Use domain and codomain as key as well
if (!m_functions.count(_name))
{
m_functions.insert(_name);
write( write(
"(declare-fun |" + "(declare-fun |" +
_name + _name +
@ -74,16 +80,25 @@ void SMTLib2Interface::declareFunction(string _name, Sort _domain, Sort _codomai
")" ")"
); );
} }
}
void SMTLib2Interface::declareInteger(string _name) void SMTLib2Interface::declareInteger(string _name)
{ {
if (!m_constants.count(_name))
{
m_constants.insert(_name);
write("(declare-const |" + _name + "| Int)"); write("(declare-const |" + _name + "| Int)");
} }
}
void SMTLib2Interface::declareBool(string _name) void SMTLib2Interface::declareBool(string _name)
{ {
if (!m_constants.count(_name))
{
m_constants.insert(_name);
write("(declare-const |" + _name + "| Bool)"); write("(declare-const |" + _name + "| Bool)");
} }
}
void SMTLib2Interface::addAssertion(Expression const& _expr) void SMTLib2Interface::addAssertion(Expression const& _expr)
{ {

3
libsolidity/formal/SMTLib2Interface.h
View File

@ -30,6 +30,7 @@
#include <string> #include <string>
#include <vector> #include <vector>
#include <cstdio> #include <cstdio>
#include <set>
namespace dev namespace dev
{ {
@ -68,6 +69,8 @@ private:
ReadCallback::Callback m_queryCallback; ReadCallback::Callback m_queryCallback;
std::vector<std::string> m_accumulatedOutput; std::vector<std::string> m_accumulatedOutput;
std::set<std::string> m_constants;
std::set<std::string> m_functions;
}; };
} }