Z3 作为替代 Datalog 引擎¶
https://blueprints.launchpad.net/congress/+spec/alternative-engine-z3
Z3 是微软开发的一个开源 Datalog 引擎。我们提议扩展 Congress，允许用户定义理论（即，产生新表并可供其他理论使用的规则集合），这些理论将由 Z3 引擎而不是现有的引擎处理。
问题描述¶
云运营商可能希望检查两台机器之间是否存在连接，或者它们是否被有效地隔离。这意味着理解流量如何路由（即，流量可能采取哪些路径）以及安全组和防火墙规则如何应用于这些路径。
以下是 Datalog 引擎解决此类问题所需的主要特性
递归：路由数据包意味着构建路径（链路路径、网络），而路径自然可以用递归方式描述。
对交换设备和防火墙中常见的 IP 地址和 IP 地址范围进行有效表示。
高效处理大量数据。
提议的变更¶
我们提议将微软开源自动定理证明器 Z3 集成到 Congress 中，作为替代的 Datalog 引擎。
Z3 理论将使用与标准理论相同的语法表达。但这些理论支持的 Datalog 语言将根据 Z3 在 Datalog 模式下支持的内容进行定制
如策略部分所述，一组不同且缩减的内置函数，
没有模态。
架构¶
概述¶
将引入一种新型理论，与经典的 NonRecursiveTheory 并存。Z3 理论将从其他理论中消耗数据，并使用 Z3 引擎应用规则。
将为每个分析器创建一个单一的 Z3 求解器实例，并在 Python 中抽象为 Z3 上下文对象。Z3 上下文将以 Z3 格式托管所有 Z3 理论的表。
Z3 理论应该可以从其他理论调用，特别是从常规的非递归理论调用。
Z3 理论可以使用来自其他理论的数据。Z3 理论使用的外部表将完全导入 Z3 上下文。
Z3 理论的编译将延迟到对这些理论进行查询时。我们将定期更新 Z3 引擎中外部表的表示，以保持同步。Z3 不支持撤销关系或规则，因此每次发生更改时都必须创建新的上下文。
类型检查¶
Z3 需要类型化的数据。类型检查将完全是隐式的，我们不会在语言中添加类型约束。
类型检查器将保留来自外部表的类型。如果变量根据不同的表应该具有两种不同的类型，它将引发错误。
类型检查器将尝试为出现在 Datalog 程序中的常量赋予最精确的类型，以使其与外部表兼容。例如，值 Ingress 通常被类型化为字符串（Str 类型），但在 Neutron 安全组的上下文中，它将被赋予 Direction 类型
为了能够为值提供两种表示形式，我们将引入显式转换器内置函数：builtin:cast(x, 'Direction', y, 'Str') 将类型为 Direction 的变量 x 转换为标准字符串类型的变量 y。它将实现为一个表，其中每一行都是相同对象在两种不同类型中的表示形式的配对。这些表将在编译程序中的常量和导入外部表时填充。
将使用相同的技巧来获得 IP 地址的位字段表示形式。
最后，类型检查器应该支持内置函数的一些通用多态性。例如，只要比较的对象类型相同，相等性和比较就应该起作用，属于给定整数子类型的两个项目的加法应该返回相同子类型中的一个项目。我们不计划支持用户定义的、多态的表。例如，以下规则是不明确的
add3(x,y,z,t) :- builtin:plus(x,y,u), builtin:plus(u,z,t)
可能希望在语言中添加类型约束来约束这些变量。
备选方案¶
我们可以尝试重新措辞理论以适应当前的引擎。例如，我们可以将递归调用展开到合理的深度（数据包具有 TTL）。不幸的是，此解决方案无法很好地扩展。展开递归调用实际上改变了程序的整体复杂性。使用 octant 进行的实验表明，当前引擎需要几分钟才能计算解决的一些问题，可以使用 octant 在十分之一秒内解决。
我们可以尝试将 Z3 算法合并到 Congress 引擎中：这将耗时且危险。Z3 使用非常高效的 C++ 数据结构来表示表，并且已经花费了十多年的时间来开发它。
我们可以使用另一个外部引擎：在某些情况下，另一个 Datalog 引擎可能是一个更好的候选者。具有显式数据类型的新的 Congress 架构旨在让多个引擎共享相同的数据池。Z3 的优势在于其整体效率及其专门为网络相关问题设计的的数据结构。
在某些情况下，我们可能希望拥有具有不同设置的多个 Z3 上下文。上下文定义了正在使用的 Z3 引擎的变体，并且不同的理论可能受益于不同的设置。
策略¶
以下是 Z3 策略的主要特征
添加了对递归规则的支持。
支持用于相等性/比较的内置谓词
支持基本的位算术（用于 IP 地址）。
用于将不透明的 IpAddress 转换为位字段并将 IpNetwork 转换为位字段对（掩码和地址）的新内置函数。
用于将存在于不同类型中的值从一种表示形式转换为另一种表示形式的内置函数。
后两种内置函数实际上将通过在同步数据源和程序时计算的表来实现。
这是一个验证两个网络是否通过路由器链连接，以及虚拟机是否附加到属于应保持隔离的两个网络集的示例策略
connect1(X) :- neutronv2:networks(id=X, name="N1")
connect2(X) :- neutronv2:networks(id=X, name="N2")
linked(X,Y) :-
neutronv2:ports(network_id=X, device_id=Z), neutronv2:routers(id=Z),
neutronv2:ports(network_id=Y, device_id=Z)
path(X,Y) :- linked(X,Y)
path(X,Y) :- path(X,Z), linked(Z,Y)
interco_error(X,Y) :- connect1(X), connect2(Y), path(X,Y)
network1(X) :- connect1(Y), path(Y, X)
network2(X) :- connect2(Y), path(Y, X)
double_attach(X) :-
nova:server(id=X),
neutronv2:ports(network_id=X, device_id=Y), network1(Y),
neutronv2:ports(network_id=X, device_id=Z), network2(Z)
策略动作¶
无。Z3 理论不支持操作。以后可能会添加支持。
数据源¶
独立于使用的数据源。
数据模型影响¶
无
REST API 影响¶
我们可能希望转向更原子的理论定义。理论是一个完整的程序，应该被视为一个完整的程序。动态添加和删除规则会使编译和类型检查变得不必要地复杂。
安全影响¶
无
通知影响¶
无
其他最终用户影响¶
对于 python-congressclient，创建新理论时，将添加一种新的替代方案：z3。
性能影响¶
行为良好的 Z3 理论将比等效的非递归理论快得多。但是，需要太多计算能力的程序可能更难在 Z3 引擎上中止。
其他部署者影响¶
Z3 不是 pypi 包。有一个非官方的 z3solver 包，但它有一些限制（不是最新版本，并且版本会发出大量虚假消息）。对于某些 Linux 发行版，没有可用的 Z3 预编译版本。在这些系统上必须从源代码编译 Z3。
由于所有这些限制，我们选择不将 z3 添加为要求。如果服务器上已部署 z3，则 z3theory 将可用。
开发者影响¶
无
实现¶
依赖项¶
此功能依赖于微软定理证明器 Z3。
测试¶
将使用 z3 库的模拟来进行单元测试。
对于集成测试，将添加新的设置到 devstack，以便可以从源代码安装 Z3（比较慢），或者直接从预编译版本部署（仅适用于 Ubuntu 14.04、16.04 和 Debian 8.10）。由于 python 包是全局部署的，如果 tempest 无法导入 python 包，则 tempest 可能会跳过 Z3 测试。
