cerc-io/solidity
16
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

Rewrite using SMTLIB2 interface.

Browse Source
This commit is contained in:
chriseth 2017-07-10 18:13:38 +02:00
parent 1ece7bf443
commit df848859da
4 changed files with 233 additions and 63 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

96
libsolidity/formal/SMTCheckerImpl.cpp
View File

@ -25,7 +25,6 @@ using namespace dev;
using namespace dev::solidity; using namespace dev::solidity;
SMTCheckerImpl::SMTCheckerImpl(ErrorReporter& _errorReporter): SMTCheckerImpl::SMTCheckerImpl(ErrorReporter& _errorReporter):
m_solver(m_context),
m_errorReporter(_errorReporter) m_errorReporter(_errorReporter)
{ {
} }
@ -39,7 +38,7 @@ void SMTCheckerImpl::analyze(SourceUnit const& _source)
pragmaFound = true; pragmaFound = true;
if (pragmaFound) if (pragmaFound)
{ {
m_solver.reset(); m_interface.reset();
m_currentSequenceCounter.clear(); m_currentSequenceCounter.clear();
_source.accept(*this); _source.accept(*this);
} }
@ -69,14 +68,14 @@ bool SMTCheckerImpl::visit(FunctionDefinition const& _function)
); );
// TODO actually we probably also have to reset all local variables and similar things. // TODO actually we probably also have to reset all local variables and similar things.
m_currentFunction = &_function; m_currentFunction = &_function;
m_solver.push(); m_interface.push();
return true; return true;
} }
void SMTCheckerImpl::endVisit(FunctionDefinition const&) void SMTCheckerImpl::endVisit(FunctionDefinition const&)
{ {
// TOOD we could check for "reachability", i.e. satisfiability here. // TOOD we could check for "reachability", i.e. satisfiability here.
m_solver.pop(); m_interface.pop();
m_currentFunction = nullptr; m_currentFunction = nullptr;
} }
@ -90,7 +89,7 @@ void SMTCheckerImpl::endVisit(VariableDeclarationStatement const& _varDecl)
else if (knownVariable(*_varDecl.declarations()[0]) && _varDecl.initialValue()) else if (knownVariable(*_varDecl.declarations()[0]) && _varDecl.initialValue())
// TODO more checks? // TODO more checks?
// TODO add restrictions about type (might be assignment from smaller type) // TODO add restrictions about type (might be assignment from smaller type)
m_solver.add(newValue(*_varDecl.declarations()[0]) == expr(*_varDecl.initialValue())); m_interface.addAssertion(newValue(*_varDecl.declarations()[0]) == expr(*_varDecl.initialValue()));
else else
m_errorReporter.warning( m_errorReporter.warning(
_varDecl.location(), _varDecl.location(),
@ -120,7 +119,7 @@ void SMTCheckerImpl::endVisit(Assignment const& _assignment)
if (knownVariable(*decl)) if (knownVariable(*decl))
// TODO more checks? // TODO more checks?
// TODO add restrictions about type (might be assignment from smaller type) // TODO add restrictions about type (might be assignment from smaller type)
m_solver.add(newValue(*decl) == expr(_assignment.rightHandSide())); m_interface.addAssertion(newValue(*decl) == expr(_assignment.rightHandSide()));
else else
m_errorReporter.warning( m_errorReporter.warning(
_assignment.location(), _assignment.location(),
@ -142,7 +141,7 @@ void SMTCheckerImpl::endVisit(TupleExpression const& _tuple)
"Assertion checker does not yet implement tules and inline arrays." "Assertion checker does not yet implement tules and inline arrays."
); );
else else
m_solver.add(expr(_tuple) == expr(*_tuple.components()[0])); m_interface.addAssertion(expr(_tuple) == expr(*_tuple.components()[0]));
} }
void SMTCheckerImpl::endVisit(BinaryOperation const& _op) void SMTCheckerImpl::endVisit(BinaryOperation const& _op)
@ -170,13 +169,13 @@ void SMTCheckerImpl::endVisit(FunctionCall const& _funCall)
solAssert(args.size() == 1, ""); solAssert(args.size() == 1, "");
solAssert(args[0]->annotation().type->category() == Type::Category::Bool, ""); solAssert(args[0]->annotation().type->category() == Type::Category::Bool, "");
checkCondition(!(expr(*args[0])), _funCall.location(), "Assertion violation"); checkCondition(!(expr(*args[0])), _funCall.location(), "Assertion violation");
m_solver.add(expr(*args[0])); m_interface.addAssertion(expr(*args[0]));
} }
else if (funType.kind() == FunctionType::Kind::Require) else if (funType.kind() == FunctionType::Kind::Require)
{ {
solAssert(args.size() == 1, ""); solAssert(args.size() == 1, "");
solAssert(args[0]->annotation().type->category() == Type::Category::Bool, ""); solAssert(args[0]->annotation().type->category() == Type::Category::Bool, "");
m_solver.add(expr(*args[0])); m_interface.addAssertion(expr(*args[0]));
checkCondition(!(expr(*args[0])), _funCall.location(), "Unreachable code"); checkCondition(!(expr(*args[0])), _funCall.location(), "Unreachable code");
// TODO is there something meaningful we can check here? // TODO is there something meaningful we can check here?
// We can check whether the condition is always fulfilled or never fulfilled. // We can check whether the condition is always fulfilled or never fulfilled.
@ -189,7 +188,7 @@ void SMTCheckerImpl::endVisit(Identifier const& _identifier)
solAssert(decl, ""); solAssert(decl, "");
if (dynamic_cast<IntegerType const*>(_identifier.annotation().type.get())) if (dynamic_cast<IntegerType const*>(_identifier.annotation().type.get()))
{ {
m_solver.add(expr(_identifier) == currentValue(*decl)); m_interface.addAssertion(expr(_identifier) == currentValue(*decl));
return; return;
} }
else if (FunctionType const* fun = dynamic_cast<FunctionType const*>(_identifier.annotation().type.get())) else if (FunctionType const* fun = dynamic_cast<FunctionType const*>(_identifier.annotation().type.get()))
@ -214,7 +213,7 @@ void SMTCheckerImpl::endVisit(Literal const& _literal)
if (RationalNumberType const* rational = dynamic_cast<RationalNumberType const*>(&type)) if (RationalNumberType const* rational = dynamic_cast<RationalNumberType const*>(&type))
solAssert(!rational->isFractional(), ""); solAssert(!rational->isFractional(), "");
m_solver.add(expr(_literal) == m_context.int_val(type.literalValue(&_literal).str().c_str())); m_interface.addAssertion(expr(_literal) == smt::Expression(type.literalValue(&_literal)));
} }
else else
m_errorReporter.warning( m_errorReporter.warning(
@ -235,10 +234,10 @@ void SMTCheckerImpl::arithmeticOperation(BinaryOperation const& _op)
{ {
solAssert(_op.annotation().commonType, ""); solAssert(_op.annotation().commonType, "");
solAssert(_op.annotation().commonType->category() == Type::Category::Integer, ""); solAssert(_op.annotation().commonType->category() == Type::Category::Integer, "");
z3::expr left(expr(_op.leftExpression())); smt::Expression left(expr(_op.leftExpression()));
z3::expr right(expr(_op.rightExpression())); smt::Expression right(expr(_op.rightExpression()));
Token::Value op = _op.getOperator(); Token::Value op = _op.getOperator();
z3::expr value( smt::Expression value(
op == Token::Add ? left + right : op == Token::Add ? left + right :
op == Token::Sub ? left - right : op == Token::Sub ? left - right :
/*op == Token::Mul*/ left * right /*op == Token::Mul*/ left * right
@ -261,7 +260,7 @@ void SMTCheckerImpl::arithmeticOperation(BinaryOperation const& _op)
&value &value
); );
m_solver.add(expr(_op) == value); m_interface.addAssertion(expr(_op) == value);
break; break;
} }
default: default:
@ -277,10 +276,10 @@ void SMTCheckerImpl::compareOperation(BinaryOperation const& _op)
solAssert(_op.annotation().commonType, ""); solAssert(_op.annotation().commonType, "");
if (_op.annotation().commonType->category() == Type::Category::Integer) if (_op.annotation().commonType->category() == Type::Category::Integer)
{ {
z3::expr left(expr(_op.leftExpression())); smt::Expression left(expr(_op.leftExpression()));
z3::expr right(expr(_op.rightExpression())); smt::Expression right(expr(_op.rightExpression()));
Token::Value op = _op.getOperator(); Token::Value op = _op.getOperator();
z3::expr value = ( smt::Expression value = (
op == Token::Equal ? (left == right) : op == Token::Equal ? (left == right) :
op == Token::NotEqual ? (left != right) : op == Token::NotEqual ? (left != right) :
op == Token::LessThan ? (left < right) : op == Token::LessThan ? (left < right) :
@ -289,7 +288,7 @@ void SMTCheckerImpl::compareOperation(BinaryOperation const& _op)
/*op == Token::GreaterThanOrEqual*/ (left >= right) /*op == Token::GreaterThanOrEqual*/ (left >= right)
); );
// TODO: check that other values for op are not possible. // TODO: check that other values for op are not possible.
m_solver.add(expr(_op) == value); m_interface.addAssertion(expr(_op) == value);
} }
else else
m_errorReporter.warning( m_errorReporter.warning(
@ -305,9 +304,9 @@ void SMTCheckerImpl::booleanOperation(BinaryOperation const& _op)
if (_op.annotation().commonType->category() == Type::Category::Bool) if (_op.annotation().commonType->category() == Type::Category::Bool)
{ {
if (_op.getOperator() == Token::And) if (_op.getOperator() == Token::And)
m_solver.add(expr(_op) == expr(_op.leftExpression()) && expr(_op.rightExpression())); m_interface.addAssertion(expr(_op) == expr(_op.leftExpression()) && expr(_op.rightExpression()));
else else
m_solver.add(expr(_op) == expr(_op.leftExpression()) || expr(_op.rightExpression())); m_interface.addAssertion(expr(_op) == expr(_op.leftExpression()) || expr(_op.rightExpression()));
} }
else else
m_errorReporter.warning( m_errorReporter.warning(
@ -317,33 +316,32 @@ void SMTCheckerImpl::booleanOperation(BinaryOperation const& _op)
} }
void SMTCheckerImpl::checkCondition( void SMTCheckerImpl::checkCondition(
z3::expr _condition, smt::Expression _condition,
SourceLocation const& _location, SourceLocation const& _location,
string const& _description, string const& _description,
string const& _additionalValueName, string const& _additionalValueName,
z3::expr* _additionalValue smt::Expression* _additionalValue
) )
{ {
m_solver.push(); m_interface.push();
m_solver.add(_condition); m_interface.addAssertion(_condition);
switch (m_solver.check()) switch (m_interface.check())
{ {
case z3::check_result::sat: case smt::CheckResult::SAT:
{ {
std::ostringstream message; std::ostringstream message;
message << _description << " happens here"; message << _description << " happens here";
if (m_currentFunction) if (m_currentFunction)
{ {
message << " for:\n"; message << " for:\n";
z3::model m = m_solver.get_model();
if (_additionalValue) if (_additionalValue)
message << " " << _additionalValueName << " = " << m.eval(*_additionalValue) << "\n"; message << " " << _additionalValueName << " = " << m_interface.eval(*_additionalValue) << "\n";
for (auto const& param: m_currentFunction->parameters()) for (auto const& param: m_currentFunction->parameters())
if (knownVariable(*param)) if (knownVariable(*param))
message << " " << param->name() << " = " << m.eval(currentValue(*param)) << "\n"; message << " " << param->name() << " = " << m_interface.eval(currentValue(*param)) << "\n";
for (auto const& var: m_currentFunction->localVariables()) for (auto const& var: m_currentFunction->localVariables())
if (knownVariable(*var)) if (knownVariable(*var))
message << " " << var->name() << " = " << m.eval(currentValue(*var)) << "\n"; message << " " << var->name() << " = " << m_interface.eval(currentValue(*var)) << "\n";
// message << m << endl; // message << m << endl;
// message << m_solver << endl; // message << m_solver << endl;
} }
@ -352,13 +350,13 @@ void SMTCheckerImpl::checkCondition(
m_errorReporter.warning(_location, message.str()); m_errorReporter.warning(_location, message.str());
break; break;
} }
case z3::check_result::unsat: case smt::CheckResult::UNSAT:
break; break;
case z3::check_result::unknown: case smt::CheckResult::UNKNOWN:
m_errorReporter.warning(_location, _description + " might happen here."); m_errorReporter.warning(_location, _description + " might happen here.");
break; break;
} }
m_solver.pop(); m_interface.pop();
} }
void SMTCheckerImpl::createVariable(VariableDeclaration const& _varDecl, bool _setToZero) void SMTCheckerImpl::createVariable(VariableDeclaration const& _varDecl, bool _setToZero)
@ -368,13 +366,13 @@ void SMTCheckerImpl::createVariable(VariableDeclaration const& _varDecl, bool _s
solAssert(m_currentSequenceCounter.count(&_varDecl) == 0, ""); solAssert(m_currentSequenceCounter.count(&_varDecl) == 0, "");
solAssert(m_z3Variables.count(&_varDecl) == 0, ""); solAssert(m_z3Variables.count(&_varDecl) == 0, "");
m_currentSequenceCounter[&_varDecl] = 0; m_currentSequenceCounter[&_varDecl] = 0;
m_z3Variables.emplace(&_varDecl, m_context.function(uniqueSymbol(_varDecl).c_str(), m_context.int_sort(), m_context.int_sort())); m_z3Variables.emplace(&_varDecl, m_interface.newFunction(uniqueSymbol(_varDecl), smt::Sort::Int, smt::Sort::Int));
if (_setToZero) if (_setToZero)
m_solver.add(currentValue(_varDecl) == 0); m_interface.addAssertion(currentValue(_varDecl) == 0);
else else
{ {
m_solver.add(currentValue(_varDecl) >= minValue(*intType)); m_interface.addAssertion(currentValue(_varDecl) >= minValue(*intType));
m_solver.add(currentValue(_varDecl) <= maxValue(*intType)); m_interface.addAssertion(currentValue(_varDecl) <= maxValue(*intType));
} }
} }
else else
@ -399,30 +397,30 @@ bool SMTCheckerImpl::knownVariable(Declaration const& _decl)
return m_currentSequenceCounter.count(&_decl); return m_currentSequenceCounter.count(&_decl);
} }
z3::expr SMTCheckerImpl::currentValue(Declaration const& _decl) smt::Expression SMTCheckerImpl::currentValue(Declaration const& _decl)
{ {
solAssert(m_currentSequenceCounter.count(&_decl), ""); solAssert(m_currentSequenceCounter.count(&_decl), "");
return var(_decl)(m_currentSequenceCounter.at(&_decl)); return var(_decl)(m_currentSequenceCounter.at(&_decl));
} }
z3::expr SMTCheckerImpl::newValue(const Declaration& _decl) smt::Expression SMTCheckerImpl::newValue(const Declaration& _decl)
{ {
solAssert(m_currentSequenceCounter.count(&_decl), ""); solAssert(m_currentSequenceCounter.count(&_decl), "");
m_currentSequenceCounter[&_decl]++; m_currentSequenceCounter[&_decl]++;
return currentValue(_decl); return currentValue(_decl);
} }
z3::expr SMTCheckerImpl::minValue(IntegerType const& _t) smt::Expression SMTCheckerImpl::minValue(IntegerType const& _t)
{ {
return m_context.int_val(_t.minValue().str().c_str()); return m_interface.newInteger(_t.minValue());
} }
z3::expr SMTCheckerImpl::maxValue(IntegerType const& _t) smt::Expression SMTCheckerImpl::maxValue(IntegerType const& _t)
{ {
return m_context.int_val(_t.maxValue().str().c_str()); return m_interface.newInteger(_t.maxValue());
} }
z3::expr SMTCheckerImpl::expr(Expression const& _e) smt::Expression SMTCheckerImpl::expr(Expression const& _e)
{ {
if (!m_z3Expressions.count(&_e)) if (!m_z3Expressions.count(&_e))
{ {
@ -433,14 +431,14 @@ z3::expr SMTCheckerImpl::expr(Expression const& _e)
{ {
if (RationalNumberType const* rational = dynamic_cast<RationalNumberType const*>(_e.annotation().type.get())) if (RationalNumberType const* rational = dynamic_cast<RationalNumberType const*>(_e.annotation().type.get()))
solAssert(!rational->isFractional(), ""); solAssert(!rational->isFractional(), "");
m_z3Expressions.emplace(&_e, m_context.int_const(uniqueSymbol(_e).c_str())); m_z3Expressions.emplace(&_e, m_interface.newInteger(uniqueSymbol(_e)));
break; break;
} }
case Type::Category::Integer: case Type::Category::Integer:
m_z3Expressions.emplace(&_e, m_context.int_const(uniqueSymbol(_e).c_str())); m_z3Expressions.emplace(&_e, m_interface.newInteger(uniqueSymbol(_e)));
break; break;
case Type::Category::Bool: case Type::Category::Bool:
m_z3Expressions.emplace(&_e, m_context.bool_const(uniqueSymbol(_e).c_str())); m_z3Expressions.emplace(&_e, m_interface.newBool(uniqueSymbol(_e)));
break; break;
default: default:
solAssert(false, "Type not implemented."); solAssert(false, "Type not implemented.");
@ -449,7 +447,7 @@ z3::expr SMTCheckerImpl::expr(Expression const& _e)
return m_z3Expressions.at(&_e); return m_z3Expressions.at(&_e);
} }
z3::func_decl SMTCheckerImpl::var(Declaration const& _decl) smt::Expression SMTCheckerImpl::var(Declaration const& _decl)
{ {
solAssert(m_z3Variables.count(&_decl), ""); solAssert(m_z3Variables.count(&_decl), "");
return m_z3Variables.at(&_decl); return m_z3Variables.at(&_decl);

26
libsolidity/formal/SMTCheckerImpl.h
View File

@ -18,8 +18,7 @@
#pragma once #pragma once
#include <libsolidity/ast/ASTVisitor.h> #include <libsolidity/ast/ASTVisitor.h>
#include <libsolidity/formal/SMTLib2Interface.h>
#include <z3++.h>
#include <map> #include <map>
#include <string> #include <string>
@ -60,11 +59,11 @@ private:
void booleanOperation(BinaryOperation const& _op); void booleanOperation(BinaryOperation const& _op);
void checkCondition( void checkCondition(
z3::expr _condition, smt::Expression _condition,
SourceLocation const& _location, SourceLocation const& _location,
std::string const& _description, std::string const& _description,
std::string const& _additionalValueName = "", std::string const& _additionalValueName = "",
z3::expr* _additionalValue = nullptr smt::Expression* _additionalValue = nullptr
); );
void createVariable(VariableDeclaration const& _varDecl, bool _setToZero); void createVariable(VariableDeclaration const& _varDecl, bool _setToZero);
@ -72,24 +71,23 @@ private:
std::string uniqueSymbol(Declaration const& _decl); std::string uniqueSymbol(Declaration const& _decl);
std::string uniqueSymbol(Expression const& _expr); std::string uniqueSymbol(Expression const& _expr);
bool knownVariable(Declaration const& _decl); bool knownVariable(Declaration const& _decl);
z3::expr currentValue(Declaration const& _decl); smt::Expression currentValue(Declaration const& _decl);
z3::expr newValue(Declaration const& _decl); smt::Expression newValue(Declaration const& _decl);
z3::expr minValue(IntegerType const& _t); smt::Expression minValue(IntegerType const& _t);
z3::expr maxValue(IntegerType const& _t); smt::Expression maxValue(IntegerType const& _t);
/// Returns the z3 expression corresponding to the AST node. Creates a new expression /// Returns the z3 expression corresponding to the AST node. Creates a new expression
/// if it does not exist yet. /// if it does not exist yet.
z3::expr expr(Expression const& _e); smt::Expression expr(Expression const& _e);
/// Returns the z3 function declaration corresponding to the given variable. /// Returns the z3 function declaration corresponding to the given variable.
/// The function takes one argument which is the "sequence number". /// The function takes one argument which is the "sequence number".
z3::func_decl var(Declaration const& _decl); smt::Expression var(Declaration const& _decl);
z3::context m_context; smt::SMTLib2Interface m_interface;
z3::solver m_solver;
std::map<Declaration const*, int> m_currentSequenceCounter; std::map<Declaration const*, int> m_currentSequenceCounter;
std::map<Expression const*, z3::expr> m_z3Expressions; std::map<Expression const*, smt::Expression> m_z3Expressions;
std::map<Declaration const*, z3::func_decl> m_z3Variables; std::map<Declaration const*, smt::Expression> m_z3Variables;
ErrorReporter& m_errorReporter; ErrorReporter& m_errorReporter;
FunctionDefinition const* m_currentFunction = nullptr; FunctionDefinition const* m_currentFunction = nullptr;

24
libsolidity/formal/SMTLib2Interface.cpp Normal file
View File

@ -0,0 +1,24 @@
/*
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 <libsolidity/formal/SMTLib2Interface.h>
using namespace std;
using namespace dev;
using namespace dev::solidity::smt;

150
libsolidity/formal/SMTLib2Interface.h Normal file
View File

@ -0,0 +1,150 @@
/*
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/>.
*/
#pragma once
#include <map>
#include <string>
#include <vector>
#include <libdevcore/Common.h>
namespace dev
{
namespace solidity
{
namespace smt
{
enum class CheckResult
{
SAT, UNSAT, UNKNOWN
};
enum class Sort
{
Int, Bool
};
class Expression
{
friend class SMTLib2Interface;
/// Manual constructor, should only be used by SMTLib2Interface and the class itself.
Expression(std::string _name, std::vector<Expression> _arguments):
m_name(std::move(_name)), m_arguments(std::move(_arguments)) {}
public:
Expression(size_t _number): m_name(std::to_string(_number)) {}
Expression(u256 const& _number): m_name(std::to_string(_number)) {}
Expression(Expression const& _other) = default;
Expression(Expression&& _other) = default;
Expression& operator=(Expression const& _other) = default;
Expression& operator=(Expression&& _other) = default;
friend Expression operator!(Expression _a)
{
return Expression("not", _a);
}
friend Expression operator&&(Expression _a, Expression _b)
{
return Expression("and", _a, _b);
}
friend Expression operator||(Expression _a, Expression _b)
{
return Expression("or", _a, _b);
}
friend Expression operator==(Expression _a, Expression _b)
{
return Expression("=", _a, _b);
}
friend Expression operator!=(Expression _a, Expression _b)
{
return !(_a == _b);
}
friend Expression operator<(Expression _a, Expression _b)
{
return Expression("<", std::move(_a), std::move(_b));
}
friend Expression operator<=(Expression _a, Expression _b)
{
return Expression("<=", std::move(_a), std::move(_b));
}
friend Expression operator>(Expression _a, Expression _b)
{
return Expression(">", std::move(_a), std::move(_b));
}
friend Expression operator>=(Expression _a, Expression _b)
{
return Expression(">=", std::move(_a), std::move(_b));
}
friend Expression operator+(Expression _a, Expression _b)
{
return Expression("+", std::move(_a), std::move(_b));
}
friend Expression operator-(Expression _a, Expression _b)
{
return Expression("-", std::move(_a), std::move(_b));
}
friend Expression operator*(Expression _a, Expression _b)
{
return Expression("*", std::move(_a), std::move(_b));
}
std::string toSExpr() const
{
std::string sexpr = "(" + m_name;
for (auto const& arg: m_arguments)
sexpr += " " + arg.toSExpr();
sexpr += ")";
return sexpr;
}
private:
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)}) {}
std::string const m_name;
std::vector<Expression> const m_arguments;
};
class SMTLib2Interface
{
public:
void reset();
void push();
void pop();
Expression newFunction(std::string _name, Sort _domain, Sort _codomain);
Expression newInteger(std::string _name);
Expression newBool(std::string _name);
void addAssertion(Expression _expr);
CheckResult check();
std::string eval(Expression _expr);
};
}
}
}