aboutsummaryrefslogtreecommitdiffstats
path: root/libsolidity/formal
diff options
context:
space:
mode:
Diffstat (limited to 'libsolidity/formal')
-rw-r--r--libsolidity/formal/CVC4Interface.cpp1
-rw-r--r--libsolidity/formal/CVC4Interface.h1
-rw-r--r--libsolidity/formal/SMTChecker.cpp122
-rw-r--r--libsolidity/formal/SMTChecker.h17
-rw-r--r--libsolidity/formal/SMTLib2Interface.cpp8
-rw-r--r--libsolidity/formal/SMTLib2Interface.h11
-rw-r--r--libsolidity/formal/SMTPortfolio.h3
-rw-r--r--libsolidity/formal/SolverInterface.h21
-rw-r--r--libsolidity/formal/SymbolicTypes.cpp23
-rw-r--r--libsolidity/formal/SymbolicTypes.h2
-rw-r--r--libsolidity/formal/SymbolicVariables.cpp11
-rw-r--r--libsolidity/formal/SymbolicVariables.h18
-rw-r--r--libsolidity/formal/Z3Interface.cpp1
-rw-r--r--libsolidity/formal/Z3Interface.h2
14 files changed, 189 insertions, 52 deletions
diff --git a/libsolidity/formal/CVC4Interface.cpp b/libsolidity/formal/CVC4Interface.cpp
index de5e4430..e7c8f015 100644
--- a/libsolidity/formal/CVC4Interface.cpp
+++ b/libsolidity/formal/CVC4Interface.cpp
@@ -18,7 +18,6 @@
#include <libsolidity/formal/CVC4Interface.h>
#include <liblangutil/Exceptions.h>
-
#include <libdevcore/CommonIO.h>
using namespace std;
diff --git a/libsolidity/formal/CVC4Interface.h b/libsolidity/formal/CVC4Interface.h
index bbe23855..89792364 100644
--- a/libsolidity/formal/CVC4Interface.h
+++ b/libsolidity/formal/CVC4Interface.h
@@ -18,7 +18,6 @@
#pragma once
#include <libsolidity/formal/SolverInterface.h>
-
#include <boost/noncopyable.hpp>
#if defined(__GLIBC__)
diff --git a/libsolidity/formal/SMTChecker.cpp b/libsolidity/formal/SMTChecker.cpp
index dc14f4c2..35c1e2f1 100644
--- a/libsolidity/formal/SMTChecker.cpp
+++ b/libsolidity/formal/SMTChecker.cpp
@@ -18,12 +18,10 @@
#include <libsolidity/formal/SMTChecker.h>
#include <libsolidity/formal/SMTPortfolio.h>
-
#include <libsolidity/formal/VariableUsage.h>
#include <libsolidity/formal/SymbolicTypes.h>
#include <liblangutil/ErrorReporter.h>
-
#include <libdevcore/StringUtils.h>
#include <boost/range/adaptor/map.hpp>
@@ -60,8 +58,7 @@ void SMTChecker::analyze(SourceUnit const& _source, shared_ptr<Scanner> const& _
bool SMTChecker::visit(ContractDefinition const& _contract)
{
for (auto _var : _contract.stateVariables())
- if (_var->type()->isValueType())
- createVariable(*_var);
+ createVariable(*_var);
return true;
}
@@ -94,9 +91,10 @@ bool SMTChecker::visit(FunctionDefinition const& _function)
m_uninterpretedTerms.clear();
resetStateVariables();
initializeLocalVariables(_function);
+ m_loopExecutionHappened = false;
+ m_arrayAssignmentHappened = false;
}
- m_loopExecutionHappened = false;
return true;
}
@@ -271,6 +269,11 @@ void SMTChecker::endVisit(Assignment const& _assignment)
assignment(decl, _assignment.rightHandSide(), _assignment.location());
defineExpr(_assignment, expr(_assignment.rightHandSide()));
}
+ else if (dynamic_cast<IndexAccess const*>(&_assignment.leftHandSide()))
+ {
+ arrayIndexAssignment(_assignment);
+ defineExpr(_assignment, expr(_assignment.rightHandSide()));
+ }
else
m_errorReporter.warning(
_assignment.location(),
@@ -459,6 +462,13 @@ void SMTChecker::visitGasLeft(FunctionCall const& _funCall)
m_interface->addAssertion(symbolicVar->currentValue() <= symbolicVar->valueAtIndex(index - 1));
}
+void SMTChecker::eraseArrayKnowledge()
+{
+ for (auto const& var: m_variables)
+ if (var.first->annotation().type->category() == Type::Category::Mapping)
+ newValue(*var.first);
+}
+
void SMTChecker::inlineFunctionCall(FunctionCall const& _funCall)
{
FunctionDefinition const* _funDef = nullptr;
@@ -532,7 +542,7 @@ void SMTChecker::abstractFunctionCall(FunctionCall const& _funCall)
for (auto const& arg: _funCall.arguments())
smtArguments.push_back(expr(*arg));
defineExpr(_funCall, (*m_expressions.at(&_funCall.expression()))(smtArguments));
- m_uninterpretedTerms.push_back(&_funCall);
+ m_uninterpretedTerms.insert(&_funCall);
setSymbolicUnknownValue(expr(_funCall), _funCall.annotation().type, *m_interface);
}
@@ -638,6 +648,74 @@ bool SMTChecker::visit(MemberAccess const& _memberAccess)
return true;
}
+void SMTChecker::endVisit(IndexAccess const& _indexAccess)
+{
+ shared_ptr<SymbolicVariable> array;
+ if (auto const& id = dynamic_cast<Identifier const*>(&_indexAccess.baseExpression()))
+ {
+ auto const& varDecl = dynamic_cast<VariableDeclaration const&>(*id->annotation().referencedDeclaration);
+ solAssert(knownVariable(varDecl), "");
+ array = m_variables[&varDecl];
+ }
+ else if (auto const& innerAccess = dynamic_cast<IndexAccess const*>(&_indexAccess.baseExpression()))
+ {
+ solAssert(knownExpr(*innerAccess), "");
+ array = m_expressions[innerAccess];
+ }
+ else
+ {
+ m_errorReporter.warning(
+ _indexAccess.location(),
+ "Assertion checker does not yet implement this expression."
+ );
+ return;
+ }
+
+ solAssert(array, "");
+ defineExpr(_indexAccess, smt::Expression::select(
+ array->currentValue(),
+ expr(*_indexAccess.indexExpression())
+ ));
+ setSymbolicUnknownValue(
+ expr(_indexAccess),
+ _indexAccess.annotation().type,
+ *m_interface
+ );
+ m_uninterpretedTerms.insert(&_indexAccess);
+}
+
+void SMTChecker::arrayAssignment()
+{
+ m_arrayAssignmentHappened = true;
+ eraseArrayKnowledge();
+}
+
+void SMTChecker::arrayIndexAssignment(Assignment const& _assignment)
+{
+ auto const& indexAccess = dynamic_cast<IndexAccess const&>(_assignment.leftHandSide());
+ if (auto const& id = dynamic_cast<Identifier const*>(&indexAccess.baseExpression()))
+ {
+ auto const& varDecl = dynamic_cast<VariableDeclaration const&>(*id->annotation().referencedDeclaration);
+ solAssert(knownVariable(varDecl), "");
+ smt::Expression store = smt::Expression::store(
+ m_variables[&varDecl]->currentValue(),
+ expr(*indexAccess.indexExpression()),
+ expr(_assignment.rightHandSide())
+ );
+ m_interface->addAssertion(newValue(varDecl) == store);
+ }
+ else if (dynamic_cast<IndexAccess const*>(&indexAccess.baseExpression()))
+ m_errorReporter.warning(
+ indexAccess.location(),
+ "Assertion checker does not yet implement assignments to multi-dimensional mappings or arrays."
+ );
+ else
+ m_errorReporter.warning(
+ _assignment.location(),
+ "Assertion checker does not yet implement this expression."
+ );
+}
+
void SMTChecker::defineGlobalVariable(string const& _name, Expression const& _expr, bool _increaseIndex)
{
if (!knownGlobalSymbol(_name))
@@ -803,6 +881,8 @@ void SMTChecker::assignment(VariableDeclaration const& _variable, smt::Expressio
checkUnderOverflow(_value, *intType, _location);
else if (dynamic_cast<AddressType const*>(type.get()))
checkUnderOverflow(_value, IntegerType(160), _location);
+ else if (dynamic_cast<MappingType const*>(type.get()))
+ arrayAssignment();
m_interface->addAssertion(newValue(_variable) == _value);
}
@@ -847,12 +927,19 @@ void SMTChecker::checkCondition(
}
for (auto const& var: m_variables)
{
- expressionsToEvaluate.emplace_back(currentValue(*var.first));
- expressionNames.push_back(var.first->name());
+ if (var.first->type()->isValueType())
+ {
+ expressionsToEvaluate.emplace_back(currentValue(*var.first));
+ expressionNames.push_back(var.first->name());
+ }
}
for (auto const& var: m_globalContext)
{
- if (smtKind(var.second->type()->category()) != smt::Kind::Function)
+ auto const& type = var.second->type();
+ if (
+ type->isValueType() &&
+ smtKind(type->category()) != smt::Kind::Function
+ )
{
expressionsToEvaluate.emplace_back(var.second->currentValue());
expressionNames.push_back(var.first);
@@ -860,8 +947,11 @@ void SMTChecker::checkCondition(
}
for (auto const& uf: m_uninterpretedTerms)
{
- expressionsToEvaluate.emplace_back(expr(*uf));
- expressionNames.push_back(m_scanner->sourceAt(uf->location()));
+ if (uf->annotation().type->isValueType())
+ {
+ expressionsToEvaluate.emplace_back(expr(*uf));
+ expressionNames.push_back(m_scanner->sourceAt(uf->location()));
+ }
}
}
smt::CheckResult result;
@@ -873,6 +963,12 @@ void SMTChecker::checkCondition(
loopComment =
"\nNote that some information is erased after the execution of loops.\n"
"You can re-introduce information using require().";
+ if (m_arrayAssignmentHappened)
+ loopComment +=
+ "\nNote that array aliasing is not supported,"
+ " therefore all mapping information is erased after"
+ " a mapping local variable/parameter is assigned.\n"
+ "You can re-introduce information using require().";
switch (result)
{
@@ -1006,7 +1102,11 @@ void SMTChecker::initializeFunctionCallParameters(FunctionDefinition const& _fun
solAssert(funParams.size() == _callArgs.size(), "");
for (unsigned i = 0; i < funParams.size(); ++i)
if (createVariable(*funParams[i]))
+ {
m_interface->addAssertion(_callArgs[i] == newValue(*funParams[i]));
+ if (funParams[i]->annotation().type->category() == Type::Category::Mapping)
+ m_arrayAssignmentHappened = true;
+ }
for (auto const& variable: _function.localVariables())
if (createVariable(*variable))
diff --git a/libsolidity/formal/SMTChecker.h b/libsolidity/formal/SMTChecker.h
index 9f8c04ab..f14d2ac0 100644
--- a/libsolidity/formal/SMTChecker.h
+++ b/libsolidity/formal/SMTChecker.h
@@ -22,13 +22,11 @@
#include <libsolidity/formal/SymbolicVariables.h>
#include <libsolidity/ast/ASTVisitor.h>
-
#include <libsolidity/interface/ReadFile.h>
-
#include <liblangutil/Scanner.h>
-#include <unordered_map>
#include <string>
+#include <unordered_map>
#include <vector>
namespace langutil
@@ -79,6 +77,7 @@ private:
void endVisit(Literal const& _node) override;
void endVisit(Return const& _node) override;
bool visit(MemberAccess const& _node) override;
+ void endVisit(IndexAccess const& _node) override;
void arithmeticOperation(BinaryOperation const& _op);
void compareOperation(BinaryOperation const& _op);
@@ -96,6 +95,14 @@ private:
void defineGlobalVariable(std::string const& _name, Expression const& _expr, bool _increaseIndex = false);
void defineGlobalFunction(std::string const& _name, Expression const& _expr);
+ /// Handles the side effects of assignment
+ /// to variable of some SMT array type
+ /// while aliasing is not supported.
+ void arrayAssignment();
+ /// Handles assignment to SMT array index.
+ void arrayIndexAssignment(Assignment const& _assignment);
+ /// Erases information about SMT arrays.
+ void eraseArrayKnowledge();
/// Division expression in the given type. Requires special treatment because
/// of rounding for signed division.
@@ -203,14 +210,16 @@ private:
std::shared_ptr<smt::SolverInterface> m_interface;
std::shared_ptr<VariableUsage> m_variableUsage;
bool m_loopExecutionHappened = false;
+ bool m_arrayAssignmentHappened = false;
/// An Expression may have multiple smt::Expression due to
/// repeated calls to the same function.
std::unordered_map<Expression const*, std::shared_ptr<SymbolicVariable>> m_expressions;
std::unordered_map<VariableDeclaration const*, std::shared_ptr<SymbolicVariable>> m_variables;
std::unordered_map<std::string, std::shared_ptr<SymbolicVariable>> m_globalContext;
/// Stores the instances of an Uninterpreted Function applied to arguments.
+ /// These may be direct application of UFs or Array index access.
/// Used to retrieve models.
- std::vector<Expression const*> m_uninterpretedTerms;
+ std::set<Expression const*> m_uninterpretedTerms;
std::vector<smt::Expression> m_pathConditions;
langutil::ErrorReporter& m_errorReporter;
std::shared_ptr<langutil::Scanner> m_scanner;
diff --git a/libsolidity/formal/SMTLib2Interface.cpp b/libsolidity/formal/SMTLib2Interface.cpp
index 3cfa01b1..a23dbe55 100644
--- a/libsolidity/formal/SMTLib2Interface.cpp
+++ b/libsolidity/formal/SMTLib2Interface.cpp
@@ -17,22 +17,20 @@
#include <libsolidity/formal/SMTLib2Interface.h>
-#include <liblangutil/Exceptions.h>
#include <libsolidity/interface/ReadFile.h>
-
+#include <liblangutil/Exceptions.h>
#include <libdevcore/Keccak256.h>
-#include <boost/algorithm/string/predicate.hpp>
#include <boost/algorithm/string/join.hpp>
+#include <boost/algorithm/string/predicate.hpp>
#include <boost/filesystem/operations.hpp>
-#include <cstdio>
+#include <array>
#include <fstream>
#include <iostream>
#include <memory>
#include <stdexcept>
#include <string>
-#include <array>
using namespace std;
using namespace dev;
diff --git a/libsolidity/formal/SMTLib2Interface.h b/libsolidity/formal/SMTLib2Interface.h
index 55fc4096..d0bf4702 100644
--- a/libsolidity/formal/SMTLib2Interface.h
+++ b/libsolidity/formal/SMTLib2Interface.h
@@ -19,20 +19,17 @@
#include <libsolidity/formal/SolverInterface.h>
-#include <liblangutil/Exceptions.h>
#include <libsolidity/interface/ReadFile.h>
-
-#include <libdevcore/FixedHash.h>
-
+#include <liblangutil/Exceptions.h>
#include <libdevcore/Common.h>
+#include <libdevcore/FixedHash.h>
#include <boost/noncopyable.hpp>
-
+#include <cstdio>
#include <map>
+#include <set>
#include <string>
#include <vector>
-#include <cstdio>
-#include <set>
namespace dev
{
diff --git a/libsolidity/formal/SMTPortfolio.h b/libsolidity/formal/SMTPortfolio.h
index 7f5ba37e..8c38bd2e 100644
--- a/libsolidity/formal/SMTPortfolio.h
+++ b/libsolidity/formal/SMTPortfolio.h
@@ -19,13 +19,10 @@
#include <libsolidity/formal/SolverInterface.h>
-
#include <libsolidity/interface/ReadFile.h>
-
#include <libdevcore/FixedHash.h>
#include <boost/noncopyable.hpp>
-
#include <map>
#include <vector>
diff --git a/libsolidity/formal/SolverInterface.h b/libsolidity/formal/SolverInterface.h
index 4a4b3fb1..6e0b17ac 100644
--- a/libsolidity/formal/SolverInterface.h
+++ b/libsolidity/formal/SolverInterface.h
@@ -17,18 +17,16 @@
#pragma once
-#include <liblangutil/Exceptions.h>
#include <libsolidity/interface/ReadFile.h>
-
+#include <liblangutil/Exceptions.h>
#include <libdevcore/Common.h>
#include <libdevcore/Exceptions.h>
#include <boost/noncopyable.hpp>
-
+#include <cstdio>
#include <map>
#include <string>
#include <vector>
-#include <cstdio>
namespace dev
{
@@ -80,6 +78,8 @@ struct FunctionSort: public Sort
[&](SortPointer _a, SortPointer _b) { return *_a == *_b; }
))
return false;
+ solAssert(codomain, "");
+ solAssert(_otherFunction->codomain, "");
return *codomain == *_otherFunction->codomain;
}
@@ -99,6 +99,10 @@ struct ArraySort: public Sort
return false;
auto _otherArray = dynamic_cast<ArraySort const*>(&_other);
solAssert(_otherArray, "");
+ solAssert(_otherArray->domain, "");
+ solAssert(_otherArray->range, "");
+ solAssert(domain, "");
+ solAssert(range, "");
return *domain == *_otherArray->domain && *range == *_otherArray->range;
}
@@ -161,8 +165,9 @@ public:
static Expression select(Expression _array, Expression _index)
{
solAssert(_array.sort->kind == Kind::Array, "");
- auto const& arraySort = dynamic_cast<ArraySort const*>(_array.sort.get());
+ std::shared_ptr<ArraySort> arraySort = std::dynamic_pointer_cast<ArraySort>(_array.sort);
solAssert(arraySort, "");
+ solAssert(_index.sort, "");
solAssert(*arraySort->domain == *_index.sort, "");
return Expression(
"select",
@@ -176,14 +181,16 @@ public:
static Expression store(Expression _array, Expression _index, Expression _element)
{
solAssert(_array.sort->kind == Kind::Array, "");
- auto const& arraySort = dynamic_cast<ArraySort const*>(_array.sort.get());
+ std::shared_ptr<ArraySort> arraySort = std::dynamic_pointer_cast<ArraySort>(_array.sort);
solAssert(arraySort, "");
+ solAssert(_index.sort, "");
+ solAssert(_element.sort, "");
solAssert(*arraySort->domain == *_index.sort, "");
solAssert(*arraySort->range == *_element.sort, "");
return Expression(
"store",
std::vector<Expression>{std::move(_array), std::move(_index), std::move(_element)},
- _array.sort
+ arraySort
);
}
diff --git a/libsolidity/formal/SymbolicTypes.cpp b/libsolidity/formal/SymbolicTypes.cpp
index 3cfaa271..269bff73 100644
--- a/libsolidity/formal/SymbolicTypes.cpp
+++ b/libsolidity/formal/SymbolicTypes.cpp
@@ -18,7 +18,6 @@
#include <libsolidity/formal/SymbolicTypes.h>
#include <libsolidity/ast/Types.h>
-
#include <memory>
using namespace std;
@@ -52,13 +51,19 @@ smt::SortPointer dev::solidity::smtSort(Type const& _type)
}
case smt::Kind::Array:
{
- solUnimplementedAssert(false, "Invalid type");
+ if (isMapping(_type.category()))
+ {
+ auto mapType = dynamic_cast<MappingType const*>(&_type);
+ solAssert(mapType, "");
+ return make_shared<smt::ArraySort>(smtSort(*mapType->keyType()), smtSort(*mapType->valueType()));
+ }
+ // TODO Solidity array
+ return make_shared<smt::Sort>(smt::Kind::Int);
}
default:
// Abstract case.
return make_shared<smt::Sort>(smt::Kind::Int);
}
- solAssert(false, "Invalid type");
}
vector<smt::SortPointer> dev::solidity::smtSort(vector<TypePointer> const& _types)
@@ -77,6 +82,8 @@ smt::Kind dev::solidity::smtKind(Type::Category _category)
return smt::Kind::Bool;
else if (isFunction(_category))
return smt::Kind::Function;
+ else if (isMapping(_category))
+ return smt::Kind::Array;
// Abstract case.
return smt::Kind::Int;
}
@@ -84,7 +91,8 @@ smt::Kind dev::solidity::smtKind(Type::Category _category)
bool dev::solidity::isSupportedType(Type::Category _category)
{
return isNumber(_category) ||
- isBool(_category);
+ isBool(_category) ||
+ isMapping(_category);
}
bool dev::solidity::isSupportedTypeDeclaration(Type::Category _category)
@@ -130,6 +138,8 @@ pair<bool, shared_ptr<SymbolicVariable>> dev::solidity::newSymbolicVariable(
else
var = make_shared<SymbolicIntVariable>(type, _uniqueName, _solver);
}
+ else if (isMapping(_type.category()))
+ var = make_shared<SymbolicMappingVariable>(type, _uniqueName, _solver);
else
solAssert(false, "");
return make_pair(abstract, var);
@@ -183,6 +193,11 @@ bool dev::solidity::isFunction(Type::Category _category)
return _category == Type::Category::Function;
}
+bool dev::solidity::isMapping(Type::Category _category)
+{
+ return _category == Type::Category::Mapping;
+}
+
smt::Expression dev::solidity::minValue(IntegerType const& _type)
{
return smt::Expression(_type.minValue());
diff --git a/libsolidity/formal/SymbolicTypes.h b/libsolidity/formal/SymbolicTypes.h
index 2c568f5b..35c7bb8d 100644
--- a/libsolidity/formal/SymbolicTypes.h
+++ b/libsolidity/formal/SymbolicTypes.h
@@ -19,7 +19,6 @@
#include <libsolidity/formal/SolverInterface.h>
#include <libsolidity/formal/SymbolicVariables.h>
-
#include <libsolidity/ast/AST.h>
#include <libsolidity/ast/Types.h>
@@ -48,6 +47,7 @@ bool isAddress(Type::Category _category);
bool isNumber(Type::Category _category);
bool isBool(Type::Category _category);
bool isFunction(Type::Category _category);
+bool isMapping(Type::Category _category);
/// Returns a new symbolic variable, according to _type.
/// Also returns whether the type is abstract or not,
diff --git a/libsolidity/formal/SymbolicVariables.cpp b/libsolidity/formal/SymbolicVariables.cpp
index 997635af..c4fc81da 100644
--- a/libsolidity/formal/SymbolicVariables.cpp
+++ b/libsolidity/formal/SymbolicVariables.cpp
@@ -18,7 +18,6 @@
#include <libsolidity/formal/SymbolicVariables.h>
#include <libsolidity/formal/SymbolicTypes.h>
-
#include <libsolidity/ast/AST.h>
using namespace std;
@@ -127,3 +126,13 @@ smt::Expression SymbolicFunctionVariable::operator()(vector<smt::Expression> _ar
{
return m_declaration(_arguments);
}
+
+SymbolicMappingVariable::SymbolicMappingVariable(
+ TypePointer _type,
+ string const& _uniqueName,
+ smt::SolverInterface& _interface
+):
+ SymbolicVariable(move(_type), _uniqueName, _interface)
+{
+ solAssert(isMapping(m_type->category()), "");
+}
diff --git a/libsolidity/formal/SymbolicVariables.h b/libsolidity/formal/SymbolicVariables.h
index 6754ee07..86abf4f1 100644
--- a/libsolidity/formal/SymbolicVariables.h
+++ b/libsolidity/formal/SymbolicVariables.h
@@ -17,12 +17,9 @@
#pragma once
-#include <libsolidity/formal/SSAVariable.h>
-
#include <libsolidity/formal/SolverInterface.h>
-
+#include <libsolidity/formal/SSAVariable.h>
#include <libsolidity/ast/Types.h>
-
#include <memory>
namespace dev
@@ -143,5 +140,18 @@ private:
smt::Expression m_declaration;
};
+/**
+ * Specialization of SymbolicVariable for Mapping
+ */
+class SymbolicMappingVariable: public SymbolicVariable
+{
+public:
+ SymbolicMappingVariable(
+ TypePointer _type,
+ std::string const& _uniqueName,
+ smt::SolverInterface& _interface
+ );
+};
+
}
}
diff --git a/libsolidity/formal/Z3Interface.cpp b/libsolidity/formal/Z3Interface.cpp
index cb01dc61..4cbc3271 100644
--- a/libsolidity/formal/Z3Interface.cpp
+++ b/libsolidity/formal/Z3Interface.cpp
@@ -18,7 +18,6 @@
#include <libsolidity/formal/Z3Interface.h>
#include <liblangutil/Exceptions.h>
-
#include <libdevcore/CommonIO.h>
using namespace std;
diff --git a/libsolidity/formal/Z3Interface.h b/libsolidity/formal/Z3Interface.h
index 86e1badd..ee4d1551 100644
--- a/libsolidity/formal/Z3Interface.h
+++ b/libsolidity/formal/Z3Interface.h
@@ -18,9 +18,7 @@
#pragma once
#include <libsolidity/formal/SolverInterface.h>
-
#include <boost/noncopyable.hpp>
-
#include <z3++.h>
namespace dev
generated by cgit v1.2.3 (git 2.25.1) at 2025-01-31 06:18:44 +0800