SMT Z3 C++版本简易教程（以python版本为对照）
近期因为科研工作需要，将原本以python实现的z3项目以c++重写，由于缺少c++版本的相关教程，花费了较多时间，故在完成当前项目后制作该简易教程（仅包含个人理解和个人在开发过程中遇到的困难之处），供读者参考。我会将python版本（下称，python中）和c++版本（下称，cpp中）的实现做简单的对比，供读者理解。相关的配置，请参考：https://blog.csdn.net/a1010451170/article/details/129373950。c++版本的官方例子可以参考：https://github.com/Z3Prover/z3/blob/master/examples/c%2B%2B/example.cpp。
0. 初始设置
python版本需要首先安装z3-solver包，并from z3 import *。cpp版本需要#include "z3++.h"，方便起见，在下面叙述中，使用：
using std::vector;
using z3::context;
using z3::solver;
using z3::expr;
using z3::optimize;
using z3::func_decl;
using z3::function;
using z3::expr_vector;
using z3::sum;
using z3::mk_and;context 与 optimize
cpp版本中，一个核心概念是context，需要显式创建context，并且其余与z3相关的数据结构均依赖该context实体存在，而python中则不需要显示创建context。
当我们的项目需要设置优化的目标时，cpp中：
context smtContext; // 创建context实体
optimize smtOptimize(smtContext); // 创建优化器python中：
smtOptimize = Optimize(); # 创建优化器2. 创建int型的变量
在cpp中，需要指明该变量的数据类型，该类型为expr，且需要结合context创建，cpp中：
expr a = smtContext.int_const("nameofTheVariable"); // 创建名为“nameofTheVariable”的int型变量python中只需调用Int()函数即可，
a = Int('nameofTheVariable') # 创建名为“nameofTheVariable”的int型变量3. 创建int变量的数组
在cpp中，有专有的数据结构expr_vector来存储若干个expr实体，创建包含若干个expr的数组：
// 一维数组
expr_vector listVariables(smtContext);
for(int i = 0; i < numberofVariables; i++){
listVariables.push_back(
smtContext.int_const(
("variable_" + std::to_string(i)).c_str()));
}
// 二维数组
vector<expr_vector> listListVariables;
for(int i = 0; i < numberofVariables; i++){
expr_vector tmp(smtContext);
for(int j = 0; j < numberNumberofVariables; j++){
tmp.push_back(
smtContext.int_const(
("variable_" + std::to_string(i)
+ "_" + std::to_string(j)).c_str()));
}
listListVariables.push_back(tmp);
}
// 访问数组中的元素
expr a = listListVariables[i][j];若创建一维数组，可以直接使用expr_vector数据结构，若创建更高维的数组，可以使用cpp中默认的vector （是否有默认的高维数组的创建方法暂时不得而知，不过上述代码中使用vector进行管理仍是可行的）。对于元素的访问，可以使用vector中的[]操作符。这里需要注意的一点是，smtContext.int_const的参数类型为char const*，因此，在构建完成字符串后，需要使用.c_str()方法转化为char const*类型。
在python中，
listListVariables = [[Int('variable_%s_%s' % (i, j))
for j in range(numberNumberofVariables)]
for i in range(numberofVariables)]4. 创建and expression
在建立constraints时，经常需要建立若干个expr的and关系，在cpp中需要使用z3::mk_and与z3::expr_vector：
expr_vector tmp_and(smtContext); // 创建expr_vector
for(int i = 0; i < numberofVariables; i++){
tmp_and.push_back(listVariables[i] >= 0); // 将expr实体添加到 expr_vector 中
}
smtOptimize.add(mk_and(tmp_and)); // 使用mk_and创建若干expr的and关系，并加入到optimize中若要继续创建更多的上述关系，可以重用tmp_and:
tmp_and.resize(0); // 重置tmp_and中的数据 （清空）
for(int i = 0; i < numberofVariables; i++){
// 连接两个expr，可以使用&&
tmp_and.push_back(listVariables[i] >= 0 && listVariables[i] <= 1);
}
smtOptimize.add(mk_and(tmp_and));其中，若要清除tmp_and中的数据可以使用tmp_and.resize(0)方法，tmp_and本身不提供类似于常规vector的clear()方法。此外，如果简单连接两个（或多个，个数已知）expr，可以使用&&符号。
python中，使用And() 方法：
# And() 的参数为一个数组，由[x for x in range()]方法创建，相当于cpp中的for循环
smtOptimize.add(And([listVariables[i] >= 0
for i in range(numberofVariables)]))5. 使用Function
cpp中创建函数需要使用function()方法，对于单输入函数：
z3::sort z3Int = smtContext.int_sort(); // function的参数类型以z3内部的参数类型指定，因此该处使用context.int_sort
// 创建仅包含一个输入的function
func_decl smtFunction1 = function("smtFunction1", // 函数名
z3Int, // 输入参数的类型
z3Int); // 输出参数的类型
// 添加constraints，该例子中令对于给定的输入，函数返回给定的输出
for(int i = 0; i < numberofVariables; i++){
// 对于单输入函数，其参数可以为cpp中的int类型，z3会自动完成转换
smtOptimize.add(smtFunction1(i) == 0);
// 也可以直接使用int_sort类型的数据
smtOptimize.add(smtFunction1(listVariables[i]) == 0);
}对于多输入的函数：
// 创建包含多个输入参数的function
func_decl smtFunction2 = function("smtFunction2", // 函数名
z3Int, // 第一个输入参数的类型
z3Int, // 第二个输入参数的类型
z3Int); // 输出参数的类型
for(int i = 0; i < numberofVariables; i++){
// 可以直接使用int_sort类型的数据
smtOptimize.add(smtFunction2(listVariables[i], listVariables[i]) == 0);
// 对于多输入函数，需要显式地将cpp中的int类型数据转化为z3中的int_sort类型
// 需要使用context.num_val(int, int_sort)方法
smtOptimize.add(smtFunction2(smtContext.num_val(i, z3Int),
smtContext.num_val(i, z3Int)) == 0);
}需要注意的是，对于多输入函数，需要将cpp中的int类型数据显式地转换为int_sort类型，可以使用方法context.num_val(int, int_sort)。
在python中，无需担心数据类型：
# 单输入函数
smtFunction1 = Function('smtFunction1', IntSort(), IntSort())
smtOptimize.add(And([smtFunction1(i) == 0
for i in range(numberofVariables)]))
# 多输入函数
smtFunction2 = Function('smtFunction2', IntSort(), IntSort(), IntSort())
# 相比于cpp，无需担心数据类型
smtOptimize.add(And([smtFunction2(i, i) == 0
for i in range(numberofVariables)]))6. 使用sum，计算若干变量的和
当需要计算多个变量的累加和时，可以使用z3提供的sum函数，在cpp中：
expr_vector tmp_sum(smtContext); // 创建expr_vector用以存放待加的各变量
for(int i = 0; i < numberofVariables; i++){
tmp_sum.push_back(listVariables[i]); // 将变量加入expr_vector中
}
smtOptimize.add(sum(tmp_sum) == 0); // 使用sum函数计算各变量的和python中，可以使用Sum()方法，
smtOptimize.add(Sum([listVariables[i]
for i in range(numberofVariables)]) == 0)7. 添加优化目标
在cpp中，
expr toBeOptimized = smtContext.int_const("toBeOptimized");
smtOptimize.maximize(toBeOptimized);
smtOptimize.minimize(toBeOptimized);在python中，
toBeOptimized = Int('toBeOptimized')
smtOptimize.maximize(toBeOptimized)
smtOptimize.minimize(toBeOptimized)8. 求解，获取模型，并输出变量的值
上述过程建立了SMT模型，接下来需要进行模型的求解，以及输出所求得的值，在cpp中，
if(smtOptimize.check() == z3::sat) { // 使用check()方法进行求解，若返回值为z3::sat则有解
z3::model m = smtOptimize.get_model(); // 使用get_model()方法获取模型
cout << "The value of toBeOptimized: " <<
m.eval(toBeOptimized).get_numeral_int() << endl; // 使用model.eval(expr).get_numeral_int()方法获取模型中某变量的值
}其中，最需要注意的点是要使用get_numeral_int()方法，通过使用该方法可以获得expr真正的值，如果不使用该方法而是仅仅使用model.eval(expr)，其返回值应为0/1，以表示该expr的真假值。
python中，基本结构与cpp版本相同，需要注意的是，需要使用as_long()方法获得变量的真实值，
if smtOptimize.check() == sat:
m = smtOptimize.model()
print(m.evaluate(toBeOptimized).as_long())