aboutsummaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
authorLeonardo Alt <leo@ethereum.org>2018-04-18 05:46:53 +0800
committerAlex Beregszaszi <alex@rtfs.hu>2018-07-28 00:34:44 +0800
commitf249f9c86f1a9673cdc5700b326b3cfeee908851 (patch)
treea22a4239fee8e0405a2fd8b99f261e18072947bf
parente56a88be37079f27dc999e4c32446958de88be99 (diff)
downloaddexon-solidity-f249f9c86f1a9673cdc5700b326b3cfeee908851.tar.gz
dexon-solidity-f249f9c86f1a9673cdc5700b326b3cfeee908851.tar.zst
dexon-solidity-f249f9c86f1a9673cdc5700b326b3cfeee908851.zip
[SMTLib2] Fix repeated declarations
-rw-r--r--libsolidity/formal/SMTLib2Interface.cpp37
-rw-r--r--libsolidity/formal/SMTLib2Interface.h3
2 files changed, 29 insertions, 11 deletions
diff --git a/libsolidity/formal/SMTLib2Interface.cpp b/libsolidity/formal/SMTLib2Interface.cpp
index 8cac3cc6..a6c1f87c 100644
--- a/libsolidity/formal/SMTLib2Interface.cpp
+++ b/libsolidity/formal/SMTLib2Interface.cpp
@@ -47,6 +47,8 @@ void SMTLib2Interface::reset()
{
m_accumulatedOutput.clear();
m_accumulatedOutput.emplace_back();
+ m_constants.clear();
+ m_functions.clear();
write("(set-option :produce-models true)");
write("(set-logic QF_UFLIA)");
}
@@ -64,25 +66,38 @@ void SMTLib2Interface::pop()
void SMTLib2Interface::declareFunction(string _name, Sort _domain, Sort _codomain)
{
- write(
- "(declare-fun |" +
- _name +
- "| (" +
- (_domain == Sort::Int ? "Int" : "Bool") +
- ") " +
- (_codomain == Sort::Int ? "Int" : "Bool") +
- ")"
- );
+ // TODO Use domain and codomain as key as well
+ if (!m_functions.count(_name))
+ {
+ m_functions.insert(_name);
+ write(
+ "(declare-fun |" +
+ _name +
+ "| (" +
+ (_domain == Sort::Int ? "Int" : "Bool") +
+ ") " +
+ (_codomain == Sort::Int ? "Int" : "Bool") +
+ ")"
+ );
+ }
}
void SMTLib2Interface::declareInteger(string _name)
{
- write("(declare-const |" + _name + "| Int)");
+ if (!m_constants.count(_name))
+ {
+ m_constants.insert(_name);
+ write("(declare-const |" + _name + "| Int)");
+ }
}
void SMTLib2Interface::declareBool(string _name)
{
- write("(declare-const |" + _name + "| Bool)");
+ if (!m_constants.count(_name))
+ {
+ m_constants.insert(_name);
+ write("(declare-const |" + _name + "| Bool)");
+ }
}
void SMTLib2Interface::addAssertion(Expression const& _expr)
diff --git a/libsolidity/formal/SMTLib2Interface.h b/libsolidity/formal/SMTLib2Interface.h
index 61071fe5..eb876a7f 100644
--- a/libsolidity/formal/SMTLib2Interface.h
+++ b/libsolidity/formal/SMTLib2Interface.h
@@ -30,6 +30,7 @@
#include <string>
#include <vector>
#include <cstdio>
+#include <set>
namespace dev
{
@@ -68,6 +69,8 @@ private:
ReadCallback::Callback m_queryCallback;
std::vector<std::string> m_accumulatedOutput;
+ std::set<std::string> m_constants;
+ std::set<std::string> m_functions;
};
}