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

Merge pull request #6892 from ethereum/smt_implies

Browse Source 
[SMTChecker] Use smtlib's implies instead of !a or b
This commit is contained in:
Leonardo 2019-06-04 17:59:54 +02:00 committed by GitHub
commit 76f509aca1
No known key found for this signature in database
GPG Key ID: 4AEE18F83AFDEB23
4 changed files with 13 additions and 3 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

2
libsolidity/formal/CVC4Interface.cpp
View File

@ -145,6 +145,8 @@ CVC4::Expr CVC4Interface::toCVC4Expr(Expression const& _expr)
return arguments[0].andExpr(arguments[1]); return arguments[0].andExpr(arguments[1]);
else if (n == "or") else if (n == "or")
return arguments[0].orExpr(arguments[1]); return arguments[0].orExpr(arguments[1]);
else if (n == "implies")
return m_context.mkExpr(CVC4::kind::IMPLIES, arguments[0], arguments[1]);
else if (n == "=") else if (n == "=")
return m_context.mkExpr(CVC4::kind::EQUAL, arguments[0], arguments[1]); return m_context.mkExpr(CVC4::kind::EQUAL, arguments[0], arguments[1]);
else if (n == "<") else if (n == "<")

8
libsolidity/formal/SolverInterface.h
View File

@ -133,6 +133,7 @@ public:
{"not", 1}, {"not", 1},
{"and", 2}, {"and", 2},
{"or", 2}, {"or", 2},
{"implies", 2},
{"=", 2}, {"=", 2},
{"<", 2}, {"<", 2},
{"<=", 2}, {"<=", 2},
@ -160,7 +161,12 @@ public:
static Expression implies(Expression _a, Expression _b) static Expression implies(Expression _a, Expression _b)
{ {
return !std::move(_a) || std::move(_b); return Expression(
"implies",
std::move(_a),
std::move(_b),
Kind::Bool
);
} }
/// select is the SMT representation of an array index access. /// select is the SMT representation of an array index access.

2
libsolidity/formal/Z3Interface.cpp
View File

@ -144,6 +144,8 @@ z3::expr Z3Interface::toZ3Expr(Expression const& _expr)
return arguments[0] && arguments[1]; return arguments[0] && arguments[1];
else if (n == "or") else if (n == "or")
return arguments[0] || arguments[1]; return arguments[0] || arguments[1];
else if (n == "implies")
return z3::implies(arguments[0], arguments[1]);
else if (n == "=") else if (n == "=")
return arguments[0] == arguments[1]; return arguments[0] == arguments[1];
else if (n == "<") else if (n == "<")

4
test/libsolidity/smtCheckerTestsJSON/multi.json
View File

@ -3,8 +3,8 @@
{ {
"smtlib2responses": "smtlib2responses":
{ {
"0x092d52dc5c2b54c1909592f7b3c8efedfd87afc0223ce421a24a1cc7905006b4": "sat\n((|EVALEXPR_0| 1))\n", "0x0a0e9583fd983e7ce82e96bd95f7c0eb831e2dd3ce3364035e30bf1d22823b34": "sat\n((|EVALEXPR_0| 1))\n",
"0x8faacfc008b6f2278b5927ff22d76832956dfb46b3c21a64fab96583c241b88f": "unsat\n", "0x15353582486fb1dac47801edbb366ae40a59ef0191ebe7c09ca32bdabecc2f1a": "unsat\n",
"0xa66d08de30c873ca7d0e7e9e426f278640e0ee463a1aed2e4e80baee916b6869": "sat\n((|EVALEXPR_0| 0))\n" "0xa66d08de30c873ca7d0e7e9e426f278640e0ee463a1aed2e4e80baee916b6869": "sat\n((|EVALEXPR_0| 0))\n"
} }
} }