cerc-io/solidity
11
0
Fork 0
mirror of https://github.com/ethereum/solidity synced 2023-10-03 13:03:40 +00:00
Code Issues Actions Packages Projects Releases Wiki Activity

Add SMTLogicException

Browse Source
This commit is contained in:
Leonardo Alt
2020-05-20 12:55:19 +02:00
parent 7a91c9b971
commit 25de3975ce
11 changed files with 127 additions and 99 deletions
Download Patch File Download Diff File Expand all files Collapse all files
libsmtutil/Z3Interface.cpp
+13 -14
View File
@@ -17,7 +17,6 @@
#include <libsmtutil/Z3Interface.h>
#include <liblangutil/Exceptions.h>
#include <libsolutil/CommonIO.h>
using namespace std;
@@ -50,7 +49,7 @@ void Z3Interface::pop()
void Z3Interface::declareVariable(string const& _name, SortPointer const& _sort)
{
solAssert(_sort, "");
smtAssert(_sort, "");
if (_sort->kind == Kind::Function)
declareFunction(_name, *_sort);
else if (m_constants.count(_name))
@@ -61,7 +60,7 @@ void Z3Interface::declareVariable(string const& _name, SortPointer const& _sort)
void Z3Interface::declareFunction(string const& _name, Sort const& _sort)
{
solAssert(_sort.kind == Kind::Function, "");
smtAssert(_sort.kind == Kind::Function, "");
FunctionSort fSort = dynamic_cast<FunctionSort const&>(_sort);
if (m_functions.count(_name))
m_functions.at(_name) = m_context.function(_name.c_str(), z3Sort(fSort.domain), z3Sort(*fSort.codomain));
@@ -124,7 +123,7 @@ z3::expr Z3Interface::toZ3Expr(Expression const& _expr)
return m_functions.at(n)(arguments);
else if (m_constants.count(n))
{
solAssert(arguments.empty(), "");
smtAssert(arguments.empty(), "");
return m_constants.at(n);
}
else if (arguments.empty())
@@ -136,7 +135,7 @@ z3::expr Z3Interface::toZ3Expr(Expression const& _expr)
else if (_expr.sort->kind == Kind::Sort)
{
auto sortSort = dynamic_pointer_cast<SortSort>(_expr.sort);
solAssert(sortSort, "");
smtAssert(sortSort, "");
return m_context.constant(n.c_str(), z3Sort(*sortSort->inner));
}
else
@@ -146,11 +145,11 @@ z3::expr Z3Interface::toZ3Expr(Expression const& _expr)
}
catch (z3::exception const& _e)
{
solAssert(false, _e.msg());
smtAssert(false, _e.msg());
}
}
solAssert(_expr.hasCorrectArity(), "");
smtAssert(_expr.hasCorrectArity(), "");
if (n == "ite")
return z3::ite(arguments[0], arguments[1], arguments[2]);
else if (n == "not")
@@ -188,9 +187,9 @@ z3::expr Z3Interface::toZ3Expr(Expression const& _expr)
else if (n == "const_array")
{
shared_ptr<SortSort> sortSort = std::dynamic_pointer_cast<SortSort>(_expr.arguments[0].sort);
solAssert(sortSort, "");
smtAssert(sortSort, "");
auto arraySort = dynamic_pointer_cast<ArraySort>(sortSort->inner);
solAssert(arraySort && arraySort->domain, "");
smtAssert(arraySort && arraySort->domain, "");
return z3::const_array(z3Sort(*arraySort->domain), arguments[1]);
}
else if (n == "tuple_get")
@@ -201,21 +200,21 @@ z3::expr Z3Interface::toZ3Expr(Expression const& _expr)
else if (n == "tuple_constructor")
{
auto constructor = z3::func_decl(m_context, Z3_get_tuple_sort_mk_decl(m_context, z3Sort(*_expr.sort)));
solAssert(constructor.arity() == arguments.size(), "");
smtAssert(constructor.arity() == arguments.size(), "");
z3::expr_vector args(m_context);
for (auto const& arg: arguments)
args.push_back(arg);
return constructor(args);
}
solAssert(false, "");
smtAssert(false, "");
}
catch (z3::exception const& _e)
{
solAssert(false, _e.msg());
smtAssert(false, _e.msg());
}
solAssert(false, "");
smtAssert(false, "");
}
z3::sort Z3Interface::z3Sort(Sort const& _sort)
@@ -256,7 +255,7 @@ z3::sort Z3Interface::z3Sort(Sort const& _sort)
default:
break;
}
solAssert(false, "");
smtAssert(false, "");
// Cannot be reached.
return m_context.int_sort();
}