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

Replace implies by =>

Browse Source
This commit is contained in:
Leo Alt 2021-05-18 19:15:08 +02:00
parent daea5f886d
commit b57b8daf0a
3 changed files with 4 additions and 4 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

2
libsmtutil/CVC4Interface.cpp
View File

@ -170,7 +170,7 @@ 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") else if (n == "=>")
return m_context.mkExpr(CVC4::kind::IMPLIES, arguments[0], arguments[1]); 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]);

4
libsmtutil/SolverInterface.h
View File

@ -86,7 +86,7 @@ public:
{"not", 1}, {"not", 1},
{"and", 2}, {"and", 2},
{"or", 2}, {"or", 2},
{"implies", 2}, {"=>", 2},
{"=", 2}, {"=", 2},
{"<", 2}, {"<", 2},
{"<=", 2}, {"<=", 2},
@ -126,7 +126,7 @@ public:
static Expression implies(Expression _a, Expression _b) static Expression implies(Expression _a, Expression _b)
{ {
return Expression( return Expression(
"implies", "=>",
std::move(_a), std::move(_a),
std::move(_b), std::move(_b),
Kind::Bool Kind::Bool

2
libsmtutil/Z3Interface.cpp
View File

@ -189,7 +189,7 @@ 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") else if (n == "=>")
return z3::implies(arguments[0], arguments[1]); return z3::implies(arguments[0], arguments[1]);
else if (n == "=") else if (n == "=")
return arguments[0] == arguments[1]; return arguments[0] == arguments[1];