mirror of
https://github.com/ethereum/solidity
synced 2023-10-03 13:03:40 +00:00
Merge pull request #3234 from ethereum/sortsForExpressions
Introduce sorts for smt expressions.
This commit is contained in:
commit
a7136dbc16
@ -64,8 +64,6 @@ void SMTLib2Interface::pop()
|
||||
|
||||
Expression SMTLib2Interface::newFunction(string _name, Sort _domain, Sort _codomain)
|
||||
{
|
||||
solAssert(!m_variables.count(_name), "");
|
||||
m_variables[_name] = SMTVariableType::Function;
|
||||
write(
|
||||
"(declare-fun |" +
|
||||
_name +
|
||||
@ -80,16 +78,12 @@ Expression SMTLib2Interface::newFunction(string _name, Sort _domain, Sort _codom
|
||||
|
||||
Expression SMTLib2Interface::newInteger(string _name)
|
||||
{
|
||||
solAssert(!m_variables.count(_name), "");
|
||||
m_variables[_name] = SMTVariableType::Integer;
|
||||
write("(declare-const |" + _name + "| Int)");
|
||||
return SolverInterface::newInteger(move(_name));
|
||||
}
|
||||
|
||||
Expression SMTLib2Interface::newBool(string _name)
|
||||
{
|
||||
solAssert(!m_variables.count(_name), "");
|
||||
m_variables[_name] = SMTVariableType::Bool;
|
||||
write("(declare-const |" + _name + "| Bool)");
|
||||
return SolverInterface::newBool(std::move(_name));
|
||||
}
|
||||
@ -151,9 +145,8 @@ string SMTLib2Interface::checkSatAndGetValuesCommand(vector<Expression> const& _
|
||||
for (size_t i = 0; i < _expressionsToEvaluate.size(); i++)
|
||||
{
|
||||
auto const& e = _expressionsToEvaluate.at(i);
|
||||
solAssert(m_variables.count(e.name), "");
|
||||
solAssert(m_variables[e.name] == SMTVariableType::Integer, "");
|
||||
command += "(declare-const |EVALEXPR_" + to_string(i) + "| Int)\n";
|
||||
solAssert(e.sort == Sort::Int || e.sort == Sort::Bool, "Invalid sort for expression to evaluate.");
|
||||
command += "(declare-const |EVALEXPR_" + to_string(i) + "| " + (e.sort == Sort::Int ? "Int" : "Bool") + "\n";
|
||||
command += "(assert (= |EVALEXPR_" + to_string(i) + "| " + toSExpr(e) + "))\n";
|
||||
}
|
||||
command += "(check-sat)\n";
|
||||
|
@ -68,14 +68,6 @@ private:
|
||||
|
||||
ReadCallback::Callback m_queryCallback;
|
||||
std::vector<std::string> m_accumulatedOutput;
|
||||
|
||||
enum class SMTVariableType {
|
||||
Function,
|
||||
Integer,
|
||||
Bool
|
||||
};
|
||||
|
||||
std::map<std::string,SMTVariableType> m_variables;
|
||||
};
|
||||
|
||||
}
|
||||
|
@ -44,7 +44,9 @@ enum class CheckResult
|
||||
|
||||
enum class Sort
|
||||
{
|
||||
Int, Bool
|
||||
Int,
|
||||
Bool,
|
||||
IntIntFun // Function of one Int returning a single Int
|
||||
};
|
||||
|
||||
/// C++ representation of an SMTLIB2 expression.
|
||||
@ -52,10 +54,10 @@ class Expression
|
||||
{
|
||||
friend class SolverInterface;
|
||||
public:
|
||||
explicit Expression(bool _v): name(_v ? "true" : "false") {}
|
||||
Expression(size_t _number): name(std::to_string(_number)) {}
|
||||
Expression(u256 const& _number): name(_number.str()) {}
|
||||
Expression(bigint const& _number): name(_number.str()) {}
|
||||
explicit Expression(bool _v): name(_v ? "true" : "false"), sort(Sort::Bool) {}
|
||||
Expression(size_t _number): name(std::to_string(_number)), sort(Sort::Int) {}
|
||||
Expression(u256 const& _number): name(_number.str()), sort(Sort::Int) {}
|
||||
Expression(bigint const& _number): name(_number.str()), sort(Sort::Int) {}
|
||||
|
||||
Expression(Expression const&) = default;
|
||||
Expression(Expression&&) = default;
|
||||
@ -64,26 +66,27 @@ public:
|
||||
|
||||
static Expression ite(Expression _condition, Expression _trueValue, Expression _falseValue)
|
||||
{
|
||||
solAssert(_trueValue.sort == _falseValue.sort, "");
|
||||
return Expression("ite", std::vector<Expression>{
|
||||
std::move(_condition), std::move(_trueValue), std::move(_falseValue)
|
||||
});
|
||||
}, _trueValue.sort);
|
||||
}
|
||||
|
||||
friend Expression operator!(Expression _a)
|
||||
{
|
||||
return Expression("not", std::move(_a));
|
||||
return Expression("not", std::move(_a), Sort::Bool);
|
||||
}
|
||||
friend Expression operator&&(Expression _a, Expression _b)
|
||||
{
|
||||
return Expression("and", std::move(_a), std::move(_b));
|
||||
return Expression("and", std::move(_a), std::move(_b), Sort::Bool);
|
||||
}
|
||||
friend Expression operator||(Expression _a, Expression _b)
|
||||
{
|
||||
return Expression("or", std::move(_a), std::move(_b));
|
||||
return Expression("or", std::move(_a), std::move(_b), Sort::Bool);
|
||||
}
|
||||
friend Expression operator==(Expression _a, Expression _b)
|
||||
{
|
||||
return Expression("=", std::move(_a), std::move(_b));
|
||||
return Expression("=", std::move(_a), std::move(_b), Sort::Bool);
|
||||
}
|
||||
friend Expression operator!=(Expression _a, Expression _b)
|
||||
{
|
||||
@ -91,52 +94,56 @@ public:
|
||||
}
|
||||
friend Expression operator<(Expression _a, Expression _b)
|
||||
{
|
||||
return Expression("<", std::move(_a), std::move(_b));
|
||||
return Expression("<", std::move(_a), std::move(_b), Sort::Bool);
|
||||
}
|
||||
friend Expression operator<=(Expression _a, Expression _b)
|
||||
{
|
||||
return Expression("<=", std::move(_a), std::move(_b));
|
||||
return Expression("<=", std::move(_a), std::move(_b), Sort::Bool);
|
||||
}
|
||||
friend Expression operator>(Expression _a, Expression _b)
|
||||
{
|
||||
return Expression(">", std::move(_a), std::move(_b));
|
||||
return Expression(">", std::move(_a), std::move(_b), Sort::Bool);
|
||||
}
|
||||
friend Expression operator>=(Expression _a, Expression _b)
|
||||
{
|
||||
return Expression(">=", std::move(_a), std::move(_b));
|
||||
return Expression(">=", std::move(_a), std::move(_b), Sort::Bool);
|
||||
}
|
||||
friend Expression operator+(Expression _a, Expression _b)
|
||||
{
|
||||
return Expression("+", std::move(_a), std::move(_b));
|
||||
return Expression("+", std::move(_a), std::move(_b), Sort::Int);
|
||||
}
|
||||
friend Expression operator-(Expression _a, Expression _b)
|
||||
{
|
||||
return Expression("-", std::move(_a), std::move(_b));
|
||||
return Expression("-", std::move(_a), std::move(_b), Sort::Int);
|
||||
}
|
||||
friend Expression operator*(Expression _a, Expression _b)
|
||||
{
|
||||
return Expression("*", std::move(_a), std::move(_b));
|
||||
return Expression("*", std::move(_a), std::move(_b), Sort::Int);
|
||||
}
|
||||
Expression operator()(Expression _a) const
|
||||
{
|
||||
solAssert(arguments.empty(), "Attempted function application to non-function.");
|
||||
return Expression(name, _a);
|
||||
solAssert(
|
||||
sort == Sort::IntIntFun && arguments.empty(),
|
||||
"Attempted function application to non-function."
|
||||
);
|
||||
return Expression(name, _a, Sort::Int);
|
||||
}
|
||||
|
||||
std::string const name;
|
||||
std::vector<Expression> const arguments;
|
||||
Sort sort;
|
||||
|
||||
private:
|
||||
/// Manual constructor, should only be used by SolverInterface and this class itself.
|
||||
Expression(std::string _name, std::vector<Expression> _arguments):
|
||||
name(std::move(_name)), arguments(std::move(_arguments)) {}
|
||||
Expression(std::string _name, std::vector<Expression> _arguments, Sort _sort):
|
||||
name(std::move(_name)), arguments(std::move(_arguments)), sort(_sort) {}
|
||||
|
||||
explicit Expression(std::string _name):
|
||||
Expression(std::move(_name), std::vector<Expression>{}) {}
|
||||
Expression(std::string _name, Expression _arg):
|
||||
Expression(std::move(_name), std::vector<Expression>{std::move(_arg)}) {}
|
||||
Expression(std::string _name, Expression _arg1, Expression _arg2):
|
||||
Expression(std::move(_name), std::vector<Expression>{std::move(_arg1), std::move(_arg2)}) {}
|
||||
explicit Expression(std::string _name, Sort _sort):
|
||||
Expression(std::move(_name), std::vector<Expression>{}, _sort) {}
|
||||
Expression(std::string _name, Expression _arg, Sort _sort):
|
||||
Expression(std::move(_name), std::vector<Expression>{std::move(_arg)}, _sort) {}
|
||||
Expression(std::string _name, Expression _arg1, Expression _arg2, Sort _sort):
|
||||
Expression(std::move(_name), std::vector<Expression>{std::move(_arg1), std::move(_arg2)}, _sort) {}
|
||||
};
|
||||
|
||||
DEV_SIMPLE_EXCEPTION(SolverError);
|
||||
@ -149,20 +156,21 @@ public:
|
||||
virtual void push() = 0;
|
||||
virtual void pop() = 0;
|
||||
|
||||
virtual Expression newFunction(std::string _name, Sort /*_domain*/, Sort /*_codomain*/)
|
||||
virtual Expression newFunction(std::string _name, Sort _domain, Sort _codomain)
|
||||
{
|
||||
solAssert(_domain == Sort::Int && _codomain == Sort::Int, "Function sort not supported.");
|
||||
// Subclasses should do something here
|
||||
return Expression(std::move(_name), {});
|
||||
return Expression(std::move(_name), {}, Sort::IntIntFun);
|
||||
}
|
||||
virtual Expression newInteger(std::string _name)
|
||||
{
|
||||
// Subclasses should do something here
|
||||
return Expression(std::move(_name), {});
|
||||
return Expression(std::move(_name), {}, Sort::Int);
|
||||
}
|
||||
virtual Expression newBool(std::string _name)
|
||||
{
|
||||
// Subclasses should do something here
|
||||
return Expression(std::move(_name), {});
|
||||
return Expression(std::move(_name), {}, Sort::Bool);
|
||||
}
|
||||
|
||||
virtual void addAssertion(Expression const& _expr) = 0;
|
||||
|
Loading…
Reference in New Issue
Block a user