diff options
Diffstat (limited to 'libsolidity/formal/SMTChecker.h')
| -rw-r--r-- | libsolidity/formal/SMTChecker.h | 6 |
1 files changed, 6 insertions, 0 deletions
diff --git a/libsolidity/formal/SMTChecker.h b/libsolidity/formal/SMTChecker.h index a7f955dd..869c9c50 100644 --- a/libsolidity/formal/SMTChecker.h +++ b/libsolidity/formal/SMTChecker.h @@ -83,6 +83,7 @@ private: void inlineFunctionCall(FunctionCall const&); void defineSpecialVariable(std::string const& _name, Expression const& _expr, bool _increaseIndex = false); + void defineUninterpretedFunction(std::string const& _name, std::vector<smt::Sort> const& _domain, smt::Sort _codomain); /// Division expression in the given type. Requires special treatment because /// of rounding for signed division. @@ -193,6 +194,11 @@ private: std::unordered_map<Expression const*, std::shared_ptr<SymbolicVariable>> m_expressions; std::unordered_map<VariableDeclaration const*, std::shared_ptr<SymbolicVariable>> m_variables; std::unordered_map<std::string, std::shared_ptr<SymbolicVariable>> m_specialVariables; + /// Stores the declaration of an Uninterpreted Function. + std::unordered_map<std::string, smt::Expression> m_uninterpretedFunctions; + /// Stores the instances of an Uninterpreted Function applied to arguments. + /// Used to retrieve models. + std::vector<Expression const*> m_uninterpretedTerms; std::vector<smt::Expression> m_pathConditions; ErrorReporter& m_errorReporter; std::shared_ptr<Scanner> m_scanner; |