mirror of
https://github.com/ethereum/solidity
synced 2023-10-03 13:03:40 +00:00
111 lines
3.0 KiB
C++
111 lines
3.0 KiB
C++
/*
|
|
This file is part of solidity.
|
|
|
|
solidity is free software: you can redistribute it and/or modify
|
|
it under the terms of the GNU General Public License as published by
|
|
the Free Software Foundation, either version 3 of the License, or
|
|
(at your option) any later version.
|
|
|
|
solidity is distributed in the hope that it will be useful,
|
|
but WITHOUT ANY WARRANTY; without even the implied warranty of
|
|
MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
|
|
GNU General Public License for more details.
|
|
|
|
You should have received a copy of the GNU General Public License
|
|
along with solidity. If not, see <http://www.gnu.org/licenses/>.
|
|
*/
|
|
|
|
#include <libsmtutil/Z3CHCInterface.h>
|
|
|
|
#include <libsolutil/CommonIO.h>
|
|
|
|
using namespace std;
|
|
using namespace solidity;
|
|
using namespace solidity::smtutil;
|
|
|
|
Z3CHCInterface::Z3CHCInterface():
|
|
m_z3Interface(make_unique<Z3Interface>()),
|
|
m_context(m_z3Interface->context()),
|
|
m_solver(*m_context)
|
|
{
|
|
// These need to be set globally.
|
|
z3::set_param("rewriter.pull_cheap_ite", true);
|
|
z3::set_param("rlimit", Z3Interface::resourceLimit);
|
|
|
|
// Spacer options.
|
|
// These needs to be set in the solver.
|
|
// https://github.com/Z3Prover/z3/blob/master/src/muz/base/fp_params.pyg
|
|
z3::params p(*m_context);
|
|
// These are useful for solving problems with arrays and loops.
|
|
// Use quantified lemma generalizer.
|
|
p.set("fp.spacer.q3.use_qgen", true);
|
|
p.set("fp.spacer.mbqi", false);
|
|
// Ground pobs by using values from a model.
|
|
p.set("fp.spacer.ground_pobs", false);
|
|
m_solver.set(p);
|
|
}
|
|
|
|
void Z3CHCInterface::declareVariable(string const& _name, SortPointer const& _sort)
|
|
{
|
|
smtAssert(_sort, "");
|
|
m_z3Interface->declareVariable(_name, _sort);
|
|
}
|
|
|
|
void Z3CHCInterface::registerRelation(Expression const& _expr)
|
|
{
|
|
m_solver.register_relation(m_z3Interface->functions().at(_expr.name));
|
|
}
|
|
|
|
void Z3CHCInterface::addRule(Expression const& _expr, string const& _name)
|
|
{
|
|
z3::expr rule = m_z3Interface->toZ3Expr(_expr);
|
|
if (m_z3Interface->constants().empty())
|
|
m_solver.add_rule(rule, m_context->str_symbol(_name.c_str()));
|
|
else
|
|
{
|
|
z3::expr_vector variables(*m_context);
|
|
for (auto const& var: m_z3Interface->constants())
|
|
variables.push_back(var.second);
|
|
z3::expr boundRule = z3::forall(variables, rule);
|
|
m_solver.add_rule(boundRule, m_context->str_symbol(_name.c_str()));
|
|
}
|
|
}
|
|
|
|
pair<CheckResult, vector<string>> Z3CHCInterface::query(Expression const& _expr)
|
|
{
|
|
CheckResult result;
|
|
vector<string> values;
|
|
try
|
|
{
|
|
z3::expr z3Expr = m_z3Interface->toZ3Expr(_expr);
|
|
switch (m_solver.query(z3Expr))
|
|
{
|
|
case z3::check_result::sat:
|
|
{
|
|
result = CheckResult::SATISFIABLE;
|
|
// TODO retrieve model.
|
|
break;
|
|
}
|
|
case z3::check_result::unsat:
|
|
{
|
|
result = CheckResult::UNSATISFIABLE;
|
|
// TODO retrieve invariants.
|
|
break;
|
|
}
|
|
case z3::check_result::unknown:
|
|
{
|
|
result = CheckResult::UNKNOWN;
|
|
break;
|
|
}
|
|
}
|
|
// TODO retrieve model / invariants
|
|
}
|
|
catch (z3::exception const&)
|
|
{
|
|
result = CheckResult::ERROR;
|
|
values.clear();
|
|
}
|
|
|
|
return make_pair(result, values);
|
|
}
|