aboutsummaryrefslogtreecommitdiffstats
path: root/libsolidity/formal/SolverInterface.h
diff options
context:
space:
mode:
authorwbt <wbt@users.noreply.github.com>2018-01-23 22:44:37 +0800
committerGitHub <noreply@github.com>2018-01-23 22:44:37 +0800
commit761eae2499b172334e5ea3e75573af99fae2a975 (patch)
tree3ec324015e8d97e9b7ca43cb4dcc3c46b1b3bf31 /libsolidity/formal/SolverInterface.h
parent7c69d88f937324b64ed8825f9e611e417421434b (diff)
parente5def2da3d9b6cffbff42e2c9e1941831d2fe5ea (diff)
downloaddexon-solidity-761eae2499b172334e5ea3e75573af99fae2a975.tar
dexon-solidity-761eae2499b172334e5ea3e75573af99fae2a975.tar.gz
dexon-solidity-761eae2499b172334e5ea3e75573af99fae2a975.tar.bz2
dexon-solidity-761eae2499b172334e5ea3e75573af99fae2a975.tar.lz
dexon-solidity-761eae2499b172334e5ea3e75573af99fae2a975.tar.xz
dexon-solidity-761eae2499b172334e5ea3e75573af99fae2a975.tar.zst
dexon-solidity-761eae2499b172334e5ea3e75573af99fae2a975.zip
Update from official repo
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(