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

Add fuzzer test.

Browse Source
This commit is contained in:
Bhargava Shastry 2022-02-16 14:13:00 +01:00
parent ea50fee663
commit e2b86d605d
1 changed files with 22 additions and 0 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

22
test/libsolutil/LP.cpp
View File

@ -51,6 +51,11 @@ public:
return LinearExpression::factorForVariable(variableIndex(_name), 1); return LinearExpression::factorForVariable(variableIndex(_name), 1);
} }
LinearExpression variable(string const& _name, rational _value)
{
return LinearExpression::factorForVariable(variableIndex(_name), _value);
}
/// Adds the constraint "_lhs <= _rhs". /// Adds the constraint "_lhs <= _rhs".
void addLEConstraint(LinearExpression _lhs, LinearExpression _rhs, set<size_t> _reason = {}) void addLEConstraint(LinearExpression _lhs, LinearExpression _rhs, set<size_t> _reason = {})
{ {
@ -110,6 +115,14 @@ public:
BOOST_CHECK_MESSAGE(suppliedReason == _reason, "Reasons are different"); BOOST_CHECK_MESSAGE(suppliedReason == _reason, "Reasons are different");
} }
void sat()
{
auto [result, model] = m_solver.check(m_solvingState);
for (auto const& [var, value]: model)
cout << var << " = " << value << endl;
BOOST_REQUIRE(result == LPResult::Feasible);
}
protected: protected:
size_t variableIndex(string const& _name) size_t variableIndex(string const& _name)
{ {
@ -131,6 +144,15 @@ protected:
BOOST_FIXTURE_TEST_SUITE(LP, LPTestFramework, *boost::unit_test::label("nooptions")) BOOST_FIXTURE_TEST_SUITE(LP, LPTestFramework, *boost::unit_test::label("nooptions"))
BOOST_AUTO_TEST_CASE(fuzzer)
{
auto x = variable("x", -6);
auto y = variable("y", -6);
// expected result: -6x -6y = 8 is unsat since x >= 0 and y >= 0 are implied
addEQConstraint(x + y, constant(8));
sat();
}
BOOST_AUTO_TEST_CASE(basic) BOOST_AUTO_TEST_CASE(basic)
{ {
auto x = variable("x"); auto x = variable("x");