diff options
Diffstat (limited to 'libsolidity/formal/Z3Interface.cpp')
| -rw-r--r-- | libsolidity/formal/Z3Interface.cpp | 12 |
1 files changed, 11 insertions, 1 deletions
diff --git a/libsolidity/formal/Z3Interface.cpp b/libsolidity/formal/Z3Interface.cpp index 0d59a3c7..bb0d6f6f 100644 --- a/libsolidity/formal/Z3Interface.cpp +++ b/libsolidity/formal/Z3Interface.cpp @@ -72,21 +72,28 @@ void Z3Interface::addAssertion(Expression const& _expr) pair<CheckResult, vector<string>> Z3Interface::check(vector<Expression> const& _expressionsToEvaluate) { +// cout << "---------------------------------" << endl; +// cout << m_solver << endl; CheckResult result; switch (m_solver.check()) { case z3::check_result::sat: result = CheckResult::SAT; + cout << "sat" << endl; break; case z3::check_result::unsat: result = CheckResult::UNSAT; + cout << "unsat" << endl; break; case z3::check_result::unknown: result = CheckResult::UNKNOWN; + cout << "unknown" << endl; break; default: solAssert(false, ""); } +// cout << "---------------------------------" << endl; + vector<string> values; if (result != CheckResult::UNSAT) @@ -107,6 +114,7 @@ z3::expr Z3Interface::toZ3Expr(Expression const& _expr) arguments.push_back(toZ3Expr(arg)); static map<string, unsigned> arity{ + {"ite", 3}, {"not", 1}, {"and", 2}, {"or", 2}, @@ -135,7 +143,9 @@ z3::expr Z3Interface::toZ3Expr(Expression const& _expr) } assert(arity.count(n) && arity.at(n) == arguments.size()); - if (n == "not") + if (n == "ite") + return z3::ite(arguments[0], arguments[1], arguments[2]); + else if (n == "not") return !arguments[0]; else if (n == "and") return arguments[0] && arguments[1]; |