Explain IntIntFun and merge assertion.

This commit is contained in:
chriseth 2017-11-22 17:12:22 +01:00
parent 762d591a47
commit 0e2a9658d2

View File

@ -44,7 +44,9 @@ enum class CheckResult
enum class Sort enum class Sort
{ {
Int, Bool, IntIntFun Int,
Bool,
IntIntFun // Function of one Int returning a single Int
}; };
/// C++ representation of an SMTLIB2 expression. /// C++ representation of an SMTLIB2 expression.
@ -120,8 +122,10 @@ public:
} }
Expression operator()(Expression _a) const Expression operator()(Expression _a) const
{ {
solAssert(sort == Sort::IntIntFun, "Attempted function application to non-function."); solAssert(
solAssert(arguments.empty(), "Attempted function application to non-function."); sort == Sort::IntIntFun && arguments.empty(),
"Attempted function application to non-function."
);
return Expression(name, _a, Sort::Int); return Expression(name, _a, Sort::Int);
} }