aboutsummaryrefslogtreecommitdiffstats
path: root/libsolidity/formal/Z3Interface.h
diff options
context:
space:
mode:
authorchriseth <chris@ethereum.org>2018-12-03 22:48:03 +0800
committerGitHub <noreply@github.com>2018-12-03 22:48:03 +0800
commitc8a2cb62832afb2dc09ccee6fd42c1516dfdb981 (patch)
tree7977e9dcbbc215088c05b847f849871ef5d4ae66 /libsolidity/formal/Z3Interface.h
parent1d4f565a64988a3400847d2655ca24f73f234bc6 (diff)
parent590be1d84cea9850ce69b68be3dc5294b39041e5 (diff)
downloaddexon-solidity-c8a2cb62832afb2dc09ccee6fd42c1516dfdb981.tar
dexon-solidity-c8a2cb62832afb2dc09ccee6fd42c1516dfdb981.tar.gz
dexon-solidity-c8a2cb62832afb2dc09ccee6fd42c1516dfdb981.tar.bz2
dexon-solidity-c8a2cb62832afb2dc09ccee6fd42c1516dfdb981.tar.lz
dexon-solidity-c8a2cb62832afb2dc09ccee6fd42c1516dfdb981.tar.xz
dexon-solidity-c8a2cb62832afb2dc09ccee6fd42c1516dfdb981.tar.zst
dexon-solidity-c8a2cb62832afb2dc09ccee6fd42c1516dfdb981.zip
Merge pull request #5571 from ethereum/develop
Version 0.5.1
Diffstat (limited to 'libsolidity/formal/Z3Interface.h')
-rw-r--r--libsolidity/formal/Z3Interface.h9
1 files changed, 5 insertions, 4 deletions
diff --git a/libsolidity/formal/Z3Interface.h b/libsolidity/formal/Z3Interface.h
index 84880ff3..86e1badd 100644
--- a/libsolidity/formal/Z3Interface.h
+++ b/libsolidity/formal/Z3Interface.h
@@ -40,16 +40,17 @@ public:
void push() override;
void pop() override;
- void declareFunction(std::string _name, Sort _domain, Sort _codomain) override;
- void declareInteger(std::string _name) override;
- void declareBool(std::string _name) override;
+ void declareVariable(std::string const& _name, Sort const& _sort) override;
void addAssertion(Expression const& _expr) override;
std::pair<CheckResult, std::vector<std::string>> check(std::vector<Expression> const& _expressionsToEvaluate) override;
private:
+ void declareFunction(std::string const& _name, Sort const& _sort);
+
z3::expr toZ3Expr(Expression const& _expr);
- z3::sort z3Sort(smt::Sort _sort);
+ z3::sort z3Sort(smt::Sort const& _sort);
+ z3::sort_vector z3Sort(std::vector<smt::SortPointer> const& _sorts);
z3::context m_context;
z3::solver m_solver;