diff options
| author | Leonardo Alt <leonardoaltt@gmail.com> | 2018-04-07 00:01:40 +0800 |
|---|---|---|
| committer | Alex Beregszaszi <alex@rtfs.hu> | 2018-04-17 19:26:58 +0800 |
| commit | ae3350ae0320d140a427d2fa318e7002745a73a5 (patch) | |
| tree | e4da5e3619baa56b09509004c58b1b5d12594e48 /libsolidity/formal/SolverInterface.h | |
| parent | 842fd0cd2cef3c11c392b7820e178fd0d034fa07 (diff) | |
| download | dexon-solidity-ae3350ae0320d140a427d2fa318e7002745a73a5.tar.gz dexon-solidity-ae3350ae0320d140a427d2fa318e7002745a73a5.tar.zst dexon-solidity-ae3350ae0320d140a427d2fa318e7002745a73a5.zip | |
[SMTChecker] Integration with CVC4
Diffstat (limited to 'libsolidity/formal/SolverInterface.h')
| -rw-r--r-- | libsolidity/formal/SolverInterface.h | 20 |
1 files changed, 20 insertions, 0 deletions
diff --git a/libsolidity/formal/SolverInterface.h b/libsolidity/formal/SolverInterface.h index 0bdebb6c..e127bb55 100644 --- a/libsolidity/formal/SolverInterface.h +++ b/libsolidity/formal/SolverInterface.h @@ -65,6 +65,26 @@ public: Expression& operator=(Expression const&) = default; Expression& operator=(Expression&&) = default; + bool hasCorrectArity() const + { + static std::map<std::string, unsigned> const operatorsArity{ + {"ite", 3}, + {"not", 1}, + {"and", 2}, + {"or", 2}, + {"=", 2}, + {"<", 2}, + {"<=", 2}, + {">", 2}, + {">=", 2}, + {"+", 2}, + {"-", 2}, + {"*", 2}, + {"/", 2} + }; + return operatorsArity.count(name) && operatorsArity.at(name) == arguments.size(); + } + static Expression ite(Expression _condition, Expression _trueValue, Expression _falseValue) { solAssert(_trueValue.sort == _falseValue.sort, ""); |