aboutsummaryrefslogtreecommitdiffstats
path: root/libsolidity/formal/SolverInterface.h
diff options
context:
space:
mode:
authorchriseth <chris@ethereum.org>2018-02-14 12:00:41 +0800
committerGitHub <noreply@github.com>2018-02-14 12:00:41 +0800
commit3155dd8058672ce8f04bc2c0f2536cb549067d0a (patch)
tree7ddb56e276c74db30671eb17ffdde5eda027142d /libsolidity/formal/SolverInterface.h
parentc4cbbb054b5ed3b8ceaa21ee5b47b0704762ff40 (diff)
parentef8292c6bb337d3c4b27836da6732b85021d1c5d (diff)
downloaddexon-solidity-3155dd8058672ce8f04bc2c0f2536cb549067d0a.tar
dexon-solidity-3155dd8058672ce8f04bc2c0f2536cb549067d0a.tar.gz
dexon-solidity-3155dd8058672ce8f04bc2c0f2536cb549067d0a.tar.bz2
dexon-solidity-3155dd8058672ce8f04bc2c0f2536cb549067d0a.tar.lz
dexon-solidity-3155dd8058672ce8f04bc2c0f2536cb549067d0a.tar.xz
dexon-solidity-3155dd8058672ce8f04bc2c0f2536cb549067d0a.tar.zst
dexon-solidity-3155dd8058672ce8f04bc2c0f2536cb549067d0a.zip
Merge pull request #3503 from ethereum/develop
Merge develop into release for v0.4.20.
Diffstat (limited to 'libsolidity/formal/SolverInterface.h')
-rw-r--r--libsolidity/formal/SolverInterface.h9
1 files changed, 9 insertions, 0 deletions
diff --git a/libsolidity/formal/SolverInterface.h b/libsolidity/formal/SolverInterface.h
index c9adf863..88487310 100644
--- a/libsolidity/formal/SolverInterface.h
+++ b/libsolidity/formal/SolverInterface.h
@@ -72,6 +72,11 @@ public:
}, _trueValue.sort);
}
+ static Expression implies(Expression _a, Expression _b)
+ {
+ return !std::move(_a) || std::move(_b);
+ }
+
friend Expression operator!(Expression _a)
{
return Expression("not", std::move(_a), Sort::Bool);
@@ -120,6 +125,10 @@ public:
{
return Expression("*", std::move(_a), std::move(_b), Sort::Int);
}
+ friend Expression operator/(Expression _a, Expression _b)
+ {
+ return Expression("/", std::move(_a), std::move(_b), Sort::Int);
+ }
Expression operator()(Expression _a) const
{
solAssert(