近期因为科研工作需要，将原本以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;

1. 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) == 0for i in range(numberofVariables)]))
# 多输入函数
smtFunction2 = Function('smtFunction2', IntSort(), IntSort(), IntSort())
# 相比于cpp，无需担心数据类型
smtOptimize.add(And([smtFunction2(i, i) == 0for 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())

9. 感谢你看到这里！