cerc-io/solidity
15
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 #4603 from ethereum/smtlib2

Browse Source 
[SMTLib2] Fix repeated declarations
This commit is contained in:
Alex Beregszaszi 2018-08-02 12:04:58 +01:00 committed by GitHub
commit 6003ed2abd
No known key found for this signature in database
GPG Key ID: 4AEE18F83AFDEB23
4 changed files with 44 additions and 18 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

13
libsolidity/formal/CVC4Interface.cpp
View File

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

37
libsolidity/formal/SMTLib2Interface.cpp
View File

@ -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)

3
libsolidity/formal/SMTLib2Interface.h
View File

@ -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;
};
}

9
libsolidity/formal/Z3Interface.cpp
View File

@ -53,17 +53,20 @@ void Z3Interface::pop()
void Z3Interface::declareFunction(string _name, Sort _domain, Sort _codomain)
{
m_functions.insert({_name, m_context.function(_name.c_str(), z3Sort(_domain), z3Sort(_codomain))});
if (!m_functions.count(_name))
m_functions.insert({_name, m_context.function(_name.c_str(), z3Sort(_domain), z3Sort(_codomain))});
}
void Z3Interface::declareInteger(string _name)
{
m_constants.insert({_name, m_context.int_const(_name.c_str())});
if (!m_constants.count(_name))
m_constants.insert({_name, m_context.int_const(_name.c_str())});
}
void Z3Interface::declareBool(string _name)
{
m_constants.insert({_name, m_context.bool_const(_name.c_str())});
if (!m_constants.count(_name))
m_constants.insert({_name, m_context.bool_const(_name.c_str())});
}
void Z3Interface::addAssertion(Expression const& _expr)