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

Add invariant to the solver results

Browse Source
This commit is contained in:
Leo Alt 2021-10-06 11:44:33 +02:00
parent fa48abf4f1
commit 9a87680d21
5 changed files with 13 additions and 12 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

5
libsmtutil/CHCSmtLib2Interface.cpp
View File

@ -87,7 +87,7 @@ void CHCSmtLib2Interface::addRule(Expression const& _expr, std::string const& /*
);
}
pair<CheckResult, CHCSolverInterface::CexGraph> CHCSmtLib2Interface::query(Expression const& _block)
tuple<CheckResult, Expression, CHCSolverInterface::CexGraph> CHCSmtLib2Interface::query(Expression const& _block)
{
string accumulated{};
swap(m_accumulatedOutput, accumulated);
@ -118,8 +118,7 @@ pair<CheckResult, CHCSolverInterface::CexGraph> CHCSmtLib2Interface::query(Expre
else
result = CheckResult::ERROR;
// TODO collect invariants or counterexamples.
return {result, {}};
return {result, Expression(true), {}};
}
void CHCSmtLib2Interface::declareVariable(string const& _name, SortPointer const& _sort)

4
libsmtutil/CHCSmtLib2Interface.h
View File

@ -44,7 +44,9 @@ public:
void addRule(Expression const& _expr, std::string const& _name) override;
std::pair<CheckResult, CexGraph> query(Expression const& _expr) override;
/// Takes a function application _expr and checks for reachability.
/// @returns solving result, an invariant, and counterexample graph, if possible.
std::tuple<CheckResult, Expression, CexGraph> query(Expression const& _expr) override;
void declareVariable(std::string const& _name, SortPointer const& _sort) override;

4
libsmtutil/CHCSolverInterface.h
View File

@ -54,8 +54,8 @@ public:
};
/// Takes a function application _expr and checks for reachability.
/// @returns solving result and a counterexample graph, if possible.
virtual std::pair<CheckResult, CexGraph> query(
/// @returns solving result, an invariant, and counterexample graph, if possible.
virtual std::tuple<CheckResult, Expression, CexGraph> query(
Expression const& _expr
) = 0;

10
libsmtutil/Z3CHCInterface.cpp
View File

@ -77,7 +77,7 @@ void Z3CHCInterface::addRule(Expression const& _expr, string const& _name)
}
}
pair<CheckResult, CHCSolverInterface::CexGraph> Z3CHCInterface::query(Expression const& _expr)
tuple<CheckResult, Expression, CHCSolverInterface::CexGraph> Z3CHCInterface::query(Expression const& _expr)
{
CheckResult result;
try
@ -93,15 +93,15 @@ pair<CheckResult, CHCSolverInterface::CexGraph> Z3CHCInterface::query(Expression
if (m_version >= tuple(4, 8, 8, 0))
{
auto proof = m_solver.get_answer();
return {result, cexGraph(proof)};
return {result, Expression(true), cexGraph(proof)};
}
break;
}
case z3::check_result::unsat:
{
result = CheckResult::UNSATISFIABLE;
// TODO retrieve invariants.
break;
auto invariants = m_z3Interface->fromZ3Expr(m_solver.get_answer());
return {result, move(invariants), {}};
}
case z3::check_result::unknown:
{
@ -125,7 +125,7 @@ pair<CheckResult, CHCSolverInterface::CexGraph> Z3CHCInterface::query(Expression
result = CheckResult::ERROR;
}
return {result, {}};
return {result, Expression(true), {}};
}
void Z3CHCInterface::setSpacerOptions(bool _preProcessing)

2
libsmtutil/Z3CHCInterface.h
View File

@ -43,7 +43,7 @@ public:
void addRule(Expression const& _expr, std::string const& _name) override;
std::pair<CheckResult, CexGraph> query(Expression const& _expr) override;
std::tuple<CheckResult, Expression, CexGraph> query(Expression const& _expr) override;
Z3Interface* z3Interface() const { return m_z3Interface.get(); }