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

[SMTChecker] Keep a copy of assertions that are added to the solvers

Browse Source
This commit is contained in:
Leonardo Alt 2019-06-04 14:43:26 +02:00
parent 95e6b2e40d
commit 31ef421fff
2 changed files with 21 additions and 0 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

16
libsolidity/formal/SMTPortfolio.cpp
View File

@ -43,18 +43,21 @@ SMTPortfolio::SMTPortfolio(map<h256, string> const& _smtlib2Responses)
void SMTPortfolio::reset()
{
m_assertions.clear();
for (auto const& s: m_solvers)
s->reset();
}
void SMTPortfolio::push()
{
m_assertions.push_back(Expression(true));
for (auto const& s: m_solvers)
s->push();
}
void SMTPortfolio::pop()
{
m_assertions.pop_back();
for (auto const& s: m_solvers)
s->pop();
}
@ -67,10 +70,23 @@ void SMTPortfolio::declareVariable(string const& _name, Sort const& _sort)
void SMTPortfolio::addAssertion(Expression const& _expr)
{
if (m_assertions.empty())
m_assertions.push_back(_expr);
else
m_assertions.back() = _expr && move(m_assertions.back());
for (auto const& s: m_solvers)
s->addAssertion(_expr);
}
Expression SMTPortfolio::assertions()
{
if (m_assertions.empty())
return Expression(true);
return m_assertions.back();
}
/*
* Broadcasts the SMT query to all solvers and returns a single result.
* This comment explains how this result is decided.

5
libsolidity/formal/SMTPortfolio.h
View File

@ -52,6 +52,9 @@ public:
void declareVariable(std::string const&, Sort const&) override;
void addAssertion(Expression const& _expr) override;
Expression assertions();
std::pair<CheckResult, std::vector<std::string>> check(std::vector<Expression> const& _expressionsToEvaluate) override;
std::vector<std::string> unhandledQueries() override;
@ -60,6 +63,8 @@ private:
static bool solverAnswered(CheckResult result);
std::vector<std::unique_ptr<smt::SolverInterface>> m_solvers;
std::vector<Expression> m_assertions;
};
}