diff options
| author | Leonardo Alt <leonardoaltt@gmail.com> | 2017-12-14 00:59:36 +0800 |
|---|---|---|
| committer | Leonardo Alt <leonardoaltt@gmail.com> | 2017-12-14 00:59:36 +0800 |
| commit | a1e296e3928b90c9a575e5e816abc566bba35493 (patch) | |
| tree | 5e4222a5001633931bc4ecc181d0e5705f7c4dd6 /libsolidity/formal/SMTChecker.h | |
| parent | 2af4d7c7dd3379d8956907413258cea884c80794 (diff) | |
| download | dexon-solidity-a1e296e3928b90c9a575e5e816abc566bba35493.tar.gz dexon-solidity-a1e296e3928b90c9a575e5e816abc566bba35493.tar.zst dexon-solidity-a1e296e3928b90c9a575e5e816abc566bba35493.zip | |
[SMTChecker] Helper functions to add an expression to the solver conjoined with or implied by the current path conditions
Diffstat (limited to 'libsolidity/formal/SMTChecker.h')
| -rw-r--r-- | libsolidity/formal/SMTChecker.h | 4 |
1 files changed, 4 insertions, 0 deletions
diff --git a/libsolidity/formal/SMTChecker.h b/libsolidity/formal/SMTChecker.h index 7f990b97..539221cc 100644 --- a/libsolidity/formal/SMTChecker.h +++ b/libsolidity/formal/SMTChecker.h @@ -152,6 +152,10 @@ private: void popPathCondition(); /// Returns the conjunction of all path conditions or True if empty smt::Expression currentPathConditions(); + /// Conjoin the current path conditions with the given parameter and add to the solver + void addPathConjoinedExpression(smt::Expression const& _e); + /// Add to the solver: the given expression implied by the current path conditions + void addPathImpliedExpression(smt::Expression const& _e); std::shared_ptr<smt::SolverInterface> m_interface; std::shared_ptr<VariableUsage> m_variableUsage; |