From 01ce43e51ba8ced7f2e53f5e9f9e0ea6b718df64 Mon Sep 17 00:00:00 2001
From: Leonardo Alt <leo@ethereum.org>
Date: Wed, 21 Nov 2018 15:13:50 +0100
Subject: [SMTChecker] Refactor smt::Sort and its usage
---
libsolidity/formal/CVC4Interface.cpp | 14 ++---
libsolidity/formal/CVC4Interface.h | 6 +-
libsolidity/formal/SMTChecker.cpp | 4 +-
libsolidity/formal/SMTChecker.h | 2 +-
libsolidity/formal/SMTLib2Interface.cpp | 18 +++---
libsolidity/formal/SMTLib2Interface.h | 4 +-
libsolidity/formal/SMTPortfolio.cpp | 2 +-
libsolidity/formal/SMTPortfolio.h | 2 +-
libsolidity/formal/SolverInterface.h | 108 ++++++++++++++------------------
libsolidity/formal/SymbolicTypes.cpp | 18 +++++-
libsolidity/formal/SymbolicTypes.h | 4 +-
libsolidity/formal/Z3Interface.cpp | 14 ++---
libsolidity/formal/Z3Interface.h | 6 +-
13 files changed, 102 insertions(+), 100 deletions(-)
diff --git a/libsolidity/formal/CVC4Interface.cpp b/libsolidity/formal/CVC4Interface.cpp
index 11822927..6e17eef1 100644
--- a/libsolidity/formal/CVC4Interface.cpp
+++ b/libsolidity/formal/CVC4Interface.cpp
@@ -50,7 +50,7 @@ void CVC4Interface::pop()
m_solver.pop();
}
-void CVC4Interface::declareFunction(string _name, vector<Sort> const& _domain, Sort _codomain)
+void CVC4Interface::declareFunction(string _name, vector<SortPointer> const& _domain, Sort const& _codomain)
{
if (!m_functions.count(_name))
{
@@ -186,13 +186,13 @@ CVC4::Expr CVC4Interface::toCVC4Expr(Expression const& _expr)
return arguments[0];
}
-CVC4::Type CVC4Interface::cvc4Sort(Sort _sort)
+CVC4::Type CVC4Interface::cvc4Sort(Sort const& _sort)
{
- switch (_sort)
+ switch (_sort.kind)
{
- case Sort::Bool:
+ case Kind::Bool:
return m_context.booleanType();
- case Sort::Int:
+ case Kind::Int:
return m_context.integerType();
default:
break;
@@ -202,10 +202,10 @@ CVC4::Type CVC4Interface::cvc4Sort(Sort _sort)
return m_context.integerType();
}
-vector<CVC4::Type> CVC4Interface::cvc4Sort(vector<Sort> const& _sorts)
+vector<CVC4::Type> CVC4Interface::cvc4Sort(vector<SortPointer> const& _sorts)
{
vector<CVC4::Type> cvc4Sorts;
for (auto const& _sort: _sorts)
- cvc4Sorts.push_back(cvc4Sort(_sort));
+ cvc4Sorts.push_back(cvc4Sort(*_sort));
return cvc4Sorts;
}
diff --git a/libsolidity/formal/CVC4Interface.h b/libsolidity/formal/CVC4Interface.h
index 273dce23..f354c790 100644
--- a/libsolidity/formal/CVC4Interface.h
+++ b/libsolidity/formal/CVC4Interface.h
@@ -51,7 +51,7 @@ public:
void push() override;
void pop() override;
- void declareFunction(std::string _name, std::vector<Sort> const& _domain, Sort _codomain) override;
+ void declareFunction(std::string _name, std::vector<SortPointer> const& _domain, Sort const& _codomain) override;
void declareInteger(std::string _name) override;
void declareBool(std::string _name) override;
@@ -60,8 +60,8 @@ public:
private:
CVC4::Expr toCVC4Expr(Expression const& _expr);
- CVC4::Type cvc4Sort(smt::Sort _sort);
- std::vector<CVC4::Type> cvc4Sort(std::vector<smt::Sort> const& _sort);
+ CVC4::Type cvc4Sort(smt::Sort const& _sort);
+ std::vector<CVC4::Type> cvc4Sort(std::vector<smt::SortPointer> const& _sorts);
CVC4::ExprManager m_context;
CVC4::SmtEngine m_solver;
diff --git a/libsolidity/formal/SMTChecker.cpp b/libsolidity/formal/SMTChecker.cpp
index bbc78c0c..0a581fc0 100644
--- a/libsolidity/formal/SMTChecker.cpp
+++ b/libsolidity/formal/SMTChecker.cpp
@@ -416,7 +416,7 @@ void SMTChecker::visitGasLeft(FunctionCall const& _funCall)
void SMTChecker::visitBlockHash(FunctionCall const& _funCall)
{
string blockHash = "blockhash";
- defineUninterpretedFunction(blockHash, {smt::Sort::Int}, smt::Sort::Int);
+ defineUninterpretedFunction(blockHash, {make_shared<smt::Sort>(smt::Kind::Int)}, smt::Kind::Int);
auto const& arguments = _funCall.arguments();
solAssert(arguments.size() == 1, "");
defineExpr(_funCall, m_uninterpretedFunctions.at(blockHash)({expr(*arguments[0])}));
@@ -605,7 +605,7 @@ void SMTChecker::defineSpecialVariable(string const& _name, Expression const& _e
defineExpr(_expr, m_specialVariables.at(_name)->currentValue());
}
-void SMTChecker::defineUninterpretedFunction(string const& _name, vector<smt::Sort> const& _domain, smt::Sort _codomain)
+void SMTChecker::defineUninterpretedFunction(string const& _name, vector<smt::SortPointer> const& _domain, smt::Sort const& _codomain)
{
if (!m_uninterpretedFunctions.count(_name))
m_uninterpretedFunctions.emplace(_name, m_interface->newFunction(_name, _domain, _codomain));
diff --git a/libsolidity/formal/SMTChecker.h b/libsolidity/formal/SMTChecker.h
index 869c9c50..a641cb5f 100644
--- a/libsolidity/formal/SMTChecker.h
+++ b/libsolidity/formal/SMTChecker.h
@@ -83,7 +83,7 @@ private:
void inlineFunctionCall(FunctionCall const&);
void defineSpecialVariable(std::string const& _name, Expression const& _expr, bool _increaseIndex = false);
- void defineUninterpretedFunction(std::string const& _name, std::vector<smt::Sort> const& _domain, smt::Sort _codomain);
+ void defineUninterpretedFunction(std::string const& _name, std::vector<smt::SortPointer> const& _domain, smt::Sort const& _codomain);
/// Division expression in the given type. Requires special treatment because
/// of rounding for signed division.
diff --git a/libsolidity/formal/SMTLib2Interface.cpp b/libsolidity/formal/SMTLib2Interface.cpp
index 54542233..01386dda 100644
--- a/libsolidity/formal/SMTLib2Interface.cpp
+++ b/libsolidity/formal/SMTLib2Interface.cpp
@@ -64,12 +64,12 @@ void SMTLib2Interface::pop()
m_accumulatedOutput.pop_back();
}
-void SMTLib2Interface::declareFunction(string _name, vector<Sort> const& _domain, Sort _codomain)
+void SMTLib2Interface::declareFunction(string _name, vector<SortPointer> const& _domain, Sort const& _codomain)
{
// TODO Use domain and codomain as key as well
string domain("");
for (auto const& sort: _domain)
- domain += toSmtLibSort(sort) + ' ';
+ domain += toSmtLibSort(*sort) + ' ';
if (!m_functions.count(_name))
{
m_functions.insert(_name);
@@ -79,7 +79,7 @@ void SMTLib2Interface::declareFunction(string _name, vector<Sort> const& _domain
"| (" +
domain +
") " +
- (_codomain == Sort::Int ? "Int" : "Bool") +
+ (_codomain.kind == Kind::Int ? "Int" : "Bool") +
")"
);
}
@@ -143,13 +143,13 @@ string SMTLib2Interface::toSExpr(Expression const& _expr)
return sexpr;
}
-string SMTLib2Interface::toSmtLibSort(Sort _sort)
+string SMTLib2Interface::toSmtLibSort(Sort const& _sort)
{
- switch (_sort)
+ switch (_sort.kind)
{
- case Sort::Int:
+ case Kind::Int:
return "Int";
- case Sort::Bool:
+ case Kind::Bool:
return "Bool";
default:
solAssert(false, "Invalid SMT sort");
@@ -173,8 +173,8 @@ string SMTLib2Interface::checkSatAndGetValuesCommand(vector<Expression> const& _
for (size_t i = 0; i < _expressionsToEvaluate.size(); i++)
{
auto const& e = _expressionsToEvaluate.at(i);
- 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";
+ solAssert(e.sort->kind == Kind::Int || e.sort->kind == Kind::Bool, "Invalid sort for expression to evaluate.");
+ command += "(declare-const |EVALEXPR_" + to_string(i) + "| " + (e.sort->kind == Kind::Int ? "Int" : "Bool") + ")\n";
command += "(assert (= |EVALEXPR_" + to_string(i) + "| " + toSExpr(e) + "))\n";
}
command += "(check-sat)\n";
diff --git a/libsolidity/formal/SMTLib2Interface.h b/libsolidity/formal/SMTLib2Interface.h
index 08ad74da..b140f555 100644
--- a/libsolidity/formal/SMTLib2Interface.h
+++ b/libsolidity/formal/SMTLib2Interface.h
@@ -49,7 +49,7 @@ public:
void push() override;
void pop() override;
- void declareFunction(std::string _name, std::vector<Sort> const& _domain, Sort _codomain) override;
+ void declareFunction(std::string _name, std::vector<SortPointer> const& _domain, Sort const& _codomain) override;
void declareInteger(std::string _name) override;
void declareBool(std::string _name) override;
@@ -58,7 +58,7 @@ public:
private:
std::string toSExpr(Expression const& _expr);
- std::string toSmtLibSort(Sort _sort);
+ std::string toSmtLibSort(Sort const& _sort);
void write(std::string _data);
diff --git a/libsolidity/formal/SMTPortfolio.cpp b/libsolidity/formal/SMTPortfolio.cpp
index e1cde04c..e01a5acc 100644
--- a/libsolidity/formal/SMTPortfolio.cpp
+++ b/libsolidity/formal/SMTPortfolio.cpp
@@ -64,7 +64,7 @@ void SMTPortfolio::pop()
s->pop();
}
-void SMTPortfolio::declareFunction(string _name, vector<Sort> const& _domain, Sort _codomain)
+void SMTPortfolio::declareFunction(string _name, vector<SortPointer> const& _domain, Sort const& _codomain)
{
for (auto s : m_solvers)
s->declareFunction(_name, _domain, _codomain);
diff --git a/libsolidity/formal/SMTPortfolio.h b/libsolidity/formal/SMTPortfolio.h
index 50bd87d4..712fb545 100644
--- a/libsolidity/formal/SMTPortfolio.h
+++ b/libsolidity/formal/SMTPortfolio.h
@@ -49,7 +49,7 @@ public:
void push() override;
void pop() override;
- void declareFunction(std::string _name, std::vector<Sort> const& _domain, Sort _codomain) override;
+ void declareFunction(std::string _name, std::vector<SortPointer> const& _domain, Sort const& _codomain) override;
void declareInteger(std::string _name) override;
void declareBool(std::string _name) override;
diff --git a/libsolidity/formal/SolverInterface.h b/libsolidity/formal/SolverInterface.h
index a6618fb5..55c0a563 100644
--- a/libsolidity/formal/SolverInterface.h
+++ b/libsolidity/formal/SolverInterface.h
@@ -42,21 +42,32 @@ enum class CheckResult
SATISFIABLE, UNSATISFIABLE, UNKNOWN, CONFLICTING, ERROR
};
-enum class Sort
+enum class Kind
{
Int,
Bool
};
+struct Sort
+{
+ Sort(Kind _kind):
+ kind(_kind) {}
+ virtual ~Sort() = default;
+ Kind const kind;
+ bool operator==(Sort const& _other) const { return kind == _other.kind; }
+};
+using SortPointer = std::shared_ptr<Sort>;
+
+
/// C++ representation of an SMTLIB2 expression.
class Expression
{
friend class SolverInterface;
public:
- 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) {}
+ explicit Expression(bool _v): Expression(_v ? "true" : "false", Kind::Bool) {}
+ Expression(size_t _number): Expression(std::to_string(_number), Kind::Int) {}
+ Expression(u256 const& _number): Expression(_number.str(), Kind::Int) {}
+ Expression(bigint const& _number): Expression(_number.str(), Kind::Int) {}
Expression(Expression const&) = default;
Expression(Expression&&) = default;
@@ -85,7 +96,7 @@ public:
static Expression ite(Expression _condition, Expression _trueValue, Expression _falseValue)
{
- solAssert(_trueValue.sort == _falseValue.sort, "");
+ solAssert(*_trueValue.sort == *_falseValue.sort, "");
return Expression("ite", std::vector<Expression>{
std::move(_condition), std::move(_trueValue), std::move(_falseValue)
}, _trueValue.sort);
@@ -98,19 +109,19 @@ public:
friend Expression operator!(Expression _a)
{
- return Expression("not", std::move(_a), Sort::Bool);
+ return Expression("not", std::move(_a), Kind::Bool);
}
friend Expression operator&&(Expression _a, Expression _b)
{
- return Expression("and", std::move(_a), std::move(_b), Sort::Bool);
+ return Expression("and", std::move(_a), std::move(_b), Kind::Bool);
}
friend Expression operator||(Expression _a, Expression _b)
{
- return Expression("or", std::move(_a), std::move(_b), Sort::Bool);
+ return Expression("or", std::move(_a), std::move(_b), Kind::Bool);
}
friend Expression operator==(Expression _a, Expression _b)
{
- return Expression("=", std::move(_a), std::move(_b), Sort::Bool);
+ return Expression("=", std::move(_a), std::move(_b), Kind::Bool);
}
friend Expression operator!=(Expression _a, Expression _b)
{
@@ -118,35 +129,35 @@ public:
}
friend Expression operator<(Expression _a, Expression _b)
{
- return Expression("<", std::move(_a), std::move(_b), Sort::Bool);
+ return Expression("<", std::move(_a), std::move(_b), Kind::Bool);
}
friend Expression operator<=(Expression _a, Expression _b)
{
- return Expression("<=", std::move(_a), std::move(_b), Sort::Bool);
+ return Expression("<=", std::move(_a), std::move(_b), Kind::Bool);
}
friend Expression operator>(Expression _a, Expression _b)
{
- return Expression(">", std::move(_a), std::move(_b), Sort::Bool);
+ return Expression(">", std::move(_a), std::move(_b), Kind::Bool);
}
friend Expression operator>=(Expression _a, Expression _b)
{
- return Expression(">=", std::move(_a), std::move(_b), Sort::Bool);
+ return Expression(">=", std::move(_a), std::move(_b), Kind::Bool);
}
friend Expression operator+(Expression _a, Expression _b)
{
- return Expression("+", std::move(_a), std::move(_b), Sort::Int);
+ return Expression("+", std::move(_a), std::move(_b), Kind::Int);
}
friend Expression operator-(Expression _a, Expression _b)
{
- return Expression("-", std::move(_a), std::move(_b), Sort::Int);
+ return Expression("-", std::move(_a), std::move(_b), Kind::Int);
}
friend Expression operator*(Expression _a, Expression _b)
{
- return Expression("*", std::move(_a), std::move(_b), Sort::Int);
+ return Expression("*", std::move(_a), std::move(_b), Kind::Int);
}
friend Expression operator/(Expression _a, Expression _b)
{
- return Expression("/", std::move(_a), std::move(_b), Sort::Int);
+ return Expression("/", std::move(_a), std::move(_b), Kind::Int);
}
Expression operator()(std::vector<Expression> _arguments) const
{
@@ -154,36 +165,26 @@ public:
arguments.empty(),
"Attempted function application to non-function."
);
- switch (sort)
- {
- case Sort::Int:
- return Expression(name, std::move(_arguments), Sort::Int);
- case Sort::Bool:
- return Expression(name, std::move(_arguments), Sort::Bool);
- default:
- solAssert(
- false,
- "Attempted function application to invalid type."
- );
- break;
- }
+ return Expression(name, std::move(_arguments), sort);
}
std::string name;
std::vector<Expression> arguments;
- Sort sort;
+ SortPointer sort;
private:
- /// Manual constructor, should only be used by SolverInterface and this class itself.
- 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, 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) {}
+ /// Manual constructors, should only be used by SolverInterface and this class itself.
+ Expression(std::string _name, std::vector<Expression> _arguments, SortPointer _sort):
+ name(std::move(_name)), arguments(std::move(_arguments)), sort(std::move(_sort)) {}
+ Expression(std::string _name, std::vector<Expression> _arguments, Kind _kind):
+ Expression(std::move(_name), std::move(_arguments), std::make_shared<Sort>(_kind)) {}
+
+ explicit Expression(std::string _name, Kind _kind):
+ Expression(std::move(_name), std::vector<Expression>{}, _kind) {}
+ Expression(std::string _name, Expression _arg, Kind _kind):
+ Expression(std::move(_name), std::vector<Expression>{std::move(_arg)}, _kind) {}
+ Expression(std::string _name, Expression _arg1, Expression _arg2, Kind _kind):
+ Expression(std::move(_name), std::vector<Expression>{std::move(_arg1), std::move(_arg2)}, _kind) {}
};
DEV_SIMPLE_EXCEPTION(SolverError);
@@ -197,39 +198,26 @@ public:
virtual void push() = 0;
virtual void pop() = 0;
- virtual void declareFunction(std::string _name, std::vector<Sort> const& _domain, Sort _codomain) = 0;
- void declareFunction(std::string _name, Sort _domain, Sort _codomain)
- {
- declareFunction(std::move(_name), std::vector<Sort>{std::move(_domain)}, std::move(_codomain));
- }
- Expression newFunction(std::string _name, std::vector<Sort> const& _domain, Sort _codomain)
+ virtual void declareFunction(std::string _name, std::vector<SortPointer> const& _domain, Sort const& _codomain) = 0;
+ Expression newFunction(std::string _name, std::vector<SortPointer> const& _domain, Sort const& _codomain)
{
declareFunction(_name, _domain, _codomain);
// Subclasses should do something here
- switch (_codomain)
- {
- case Sort::Int:
- return Expression(std::move(_name), {}, Sort::Int);
- case Sort::Bool:
- return Expression(std::move(_name), {}, Sort::Bool);
- default:
- solAssert(false, "Function sort not supported.");
- break;
- }
+ return Expression(std::move(_name), {}, _codomain.kind);
}
virtual void declareInteger(std::string _name) = 0;
Expression newInteger(std::string _name)
{
// Subclasses should do something here
declareInteger(_name);
- return Expression(std::move(_name), {}, Sort::Int);
+ return Expression(std::move(_name), {}, Kind::Int);
}
virtual void declareBool(std::string _name) = 0;
Expression newBool(std::string _name)
{
// Subclasses should do something here
declareBool(_name);
- return Expression(std::move(_name), {}, Sort::Bool);
+ return Expression(std::move(_name), {}, Kind::Bool);
}
virtual void addAssertion(Expression const& _expr) = 0;
diff --git a/libsolidity/formal/SymbolicTypes.cpp b/libsolidity/formal/SymbolicTypes.cpp
index 78bf861b..a3b6e3a8 100644
--- a/libsolidity/formal/SymbolicTypes.cpp
+++ b/libsolidity/formal/SymbolicTypes.cpp
@@ -24,12 +24,24 @@
using namespace std;
using namespace dev::solidity;
-smt::Sort dev::solidity::smtSort(Type::Category _category)
+smt::SortPointer dev::solidity::smtSort(Type const& _type)
+{
+ switch (smtKind(_type.category()))
+ {
+ case smt::Kind::Int:
+ return make_shared<smt::Sort>(smt::Kind::Int);
+ case smt::Kind::Bool:
+ return make_shared<smt::Sort>(smt::Kind::Bool);
+ }
+ solAssert(false, "Invalid type");
+}
+
+smt::Kind dev::solidity::smtKind(Type::Category _category)
{
if (isNumber(_category))
- return smt::Sort::Int;
+ return smt::Kind::Int;
else if (isBool(_category))
- return smt::Sort::Bool;
+ return smt::Kind::Bool;
solAssert(false, "Invalid type");
}
diff --git a/libsolidity/formal/SymbolicTypes.h b/libsolidity/formal/SymbolicTypes.h
index 2639fcb9..c802c5b4 100644
--- a/libsolidity/formal/SymbolicTypes.h
+++ b/libsolidity/formal/SymbolicTypes.h
@@ -29,7 +29,9 @@ namespace solidity
{
/// Returns the SMT sort that models the Solidity type _type.
-smt::Sort smtSort(Type::Category _type);
+smt::SortPointer smtSort(Type const& _type);
+/// Returns the SMT kind that models the Solidity type type category _category.
+smt::Kind smtKind(Type::Category _category);
/// So far int, bool and address are supported.
/// Returns true if type is supported.
diff --git a/libsolidity/formal/Z3Interface.cpp b/libsolidity/formal/Z3Interface.cpp
index 2519e41b..09696aeb 100644
--- a/libsolidity/formal/Z3Interface.cpp
+++ b/libsolidity/formal/Z3Interface.cpp
@@ -51,7 +51,7 @@ void Z3Interface::pop()
m_solver.pop();
}
-void Z3Interface::declareFunction(string _name, vector<Sort> const& _domain, Sort _codomain)
+void Z3Interface::declareFunction(string _name, vector<SortPointer> const& _domain, Sort const& _codomain)
{
if (!m_functions.count(_name))
m_functions.insert({_name, m_context.function(_name.c_str(), z3Sort(_domain), z3Sort(_codomain))});
@@ -168,13 +168,13 @@ z3::expr Z3Interface::toZ3Expr(Expression const& _expr)
return arguments[0];
}
-z3::sort Z3Interface::z3Sort(Sort _sort)
+z3::sort Z3Interface::z3Sort(Sort const& _sort)
{
- switch (_sort)
+ switch (_sort.kind)
{
- case Sort::Bool:
+ case Kind::Bool:
return m_context.bool_sort();
- case Sort::Int:
+ case Kind::Int:
return m_context.int_sort();
default:
break;
@@ -184,10 +184,10 @@ z3::sort Z3Interface::z3Sort(Sort _sort)
return m_context.int_sort();
}
-z3::sort_vector Z3Interface::z3Sort(vector<Sort> const& _sorts)
+z3::sort_vector Z3Interface::z3Sort(vector<SortPointer> const& _sorts)
{
z3::sort_vector z3Sorts(m_context);
for (auto const& _sort: _sorts)
- z3Sorts.push_back(z3Sort(_sort));
+ z3Sorts.push_back(z3Sort(*_sort));
return z3Sorts;
}
diff --git a/libsolidity/formal/Z3Interface.h b/libsolidity/formal/Z3Interface.h
index 5eae618e..8c1fcf61 100644
--- a/libsolidity/formal/Z3Interface.h
+++ b/libsolidity/formal/Z3Interface.h
@@ -40,7 +40,7 @@ public:
void push() override;
void pop() override;
- void declareFunction(std::string _name, std::vector<Sort> const& _domain, Sort _codomain) override;
+ void declareFunction(std::string _name, std::vector<SortPointer> const& _domain, Sort const& _codomain) override;
void declareInteger(std::string _name) override;
void declareBool(std::string _name) override;
@@ -49,8 +49,8 @@ public:
private:
z3::expr toZ3Expr(Expression const& _expr);
- z3::sort z3Sort(smt::Sort _sort);
- z3::sort_vector z3Sort(std::vector<smt::Sort> const& _sort);
+ z3::sort z3Sort(smt::Sort const& _sort);
+ z3::sort_vector z3Sort(std::vector<smt::SortPointer> const& _sorts);
z3::context m_context;
z3::solver m_solver;
--
cgit v1.2.3