- smt
应用基于 SAT 的 SMT 求解器（最通用的默认策略）。
- sat
使用 SAT 求解器尝试解决问题（处理纯布尔逻辑问题的基础）。
- lia
内置策略：求解线性整数算术（LIA）问题。
- lra
内置策略：求解线性实数算术（LRA）问题。
- qfbv
内置策略：求解量词自由的位向量（QF_BV）问题。
- simplify
应用简化规则（基础预处理步骤）。
- solve-eqs
解方程并消除变量（通过代数方法简化问题）。
- propagate-values
传播常量值（通过常量折叠简化表达式）。
- nnf
将目标转换为否定范式（标准化逻辑结构）。
- tseitin-cnf
通过 Tseitin 编码将目标转换为 CNF（便于 SAT 求解）。
- qe
应用量词消除（处理存在量词问题）。
- qffp
尝试解决量词自由的浮点（QF_FP）问题。
- nra
内置策略：解决非线性实数算术（NRA）问题。
- fpa2bv
将浮点数转换为位向量（处理浮点问题的常用方法）。
- propagate-bv-bounds
传播位向量边界（通过简化隐含或矛盾的边界）。
- bit-blast
将位向量表达式规约为 SAT 问题（位向量求解的核心步骤）。
- ctx-solver-simplify
基于求解器的上下文相关简化（动态优化断言集）。
- qe-light
轻量级量词消除（快速处理简单量词）。
- horn
应用 Horn 子句求解策略（用于约束逻辑编程）。
- nlsat
使用非线性算术求解器尝试解决问题（针对非线性片段）。
- default
未指定逻辑时的默认策略（综合使用多种战术）。
- skip
空操作战术（占位或调试用）。
- fail
始终失败的战术（用于控制流程）。
基础求解器
| 方法名 | 描述 |
|---|
smt | 应用基于 SAT 的 SMT 求解器（默认综合策略，支持多逻辑片段） |
sat | 使用 SAT 求解器解决纯布尔逻辑问题 |
default | 未指定逻辑时的默认策略（组合多种战术） |
psmt | 并行 SMT 策略（提升大规模问题求解速度） |
fail | 始终失败的战术（用于策略组合控制） |
skip | 空操作战术（占位或调试用） |
算术与线性求解
| 方法名 | 描述 |
|---|
lia | 求解线性整数算术（LIA）问题 |
lra | 求解线性实数算术（LRA）问题 |
nra | 求解非线性实数算术（NRA）问题 |
lira | 求解混合线性整数/实数算术（LIRA）问题 |
qflia | 求解量词自由的线性整数算术（QF_LIA）问题 |
qflra | 求解量词自由的线性实数算术（QF_LRA）问题 |
qfnia | 求解量词自由的非线性整数算术（QF_NIA）问题 |
nlsat | 使用非线性算术求解器（处理多项式约束） |
diff-neq | 专用求解器：处理仅含差值不等式（如 x - y ≠ k）的整数算术问题 |
位向量（BV）处理
| 方法名 | 描述 |
|---|
qfbv | 求解量词自由的位向量（QF_BV）问题 |
bit-blast | 将位向量表达式转换为 SAT 问题（核心位向量求解步骤） |
bv1-blast | 将位向量降维为 1-bit 位向量（仅支持等值、提取和连接操作） |
propagate-bv-bounds | 传播位向量边界（通过简化隐含或矛盾的约束） |
max-bv-sharing | 最大化位向量表达式共享（优化加法器/乘法器等电路结构） |
reduce-bv-size | 通过不等式减少位向量宽度 |
ackermannize_bv | 对位向量实例执行阿克曼化（消除函数应用依赖） |
qfufbv | 求解含未解释函数的量词自由位向量（QF_UFBV）问题 |
浮点数（FP）处理
| 方法名 | 描述 |
|---|
fpa2bv | 将浮点数转换为位向量（FP 问题的经典编码方法） |
qffp | 求解量词自由的浮点（QF_FP）问题 |
qffplra | 求解量词自由的浮点 + 线性实数算术（QF_FPLRA）问题 |
qffpbv | 求解量词自由的浮点 + 位向量（QF_FPBV）问题 |
量词处理
| 方法名 | 描述 |
|---|
qe | 完全量词消除（处理存在量词） |
qe-light | 轻量级量词消除（快速处理简单量词） |
qe2 | 基于 QSAT 的量词消除 |
qe_rec | 递归应用 QSAT 量词消除 |
qsat | 应用 QSAT 求解器（支持含量词的非线性问题） |
预处理与简化
| 方法名 | 描述 |
|---|
simplify | 通用表达式简化（如常量折叠、代数规则应用） |
solve-eqs | 解方程并消除变量（通过代数方法简化问题） |
propagate-values | 传播常量值（替换已知变量值） |
nnf | 将目标转换为否定范式（标准化逻辑结构） |
tseitin-cnf | 通过 Tseitin 编码转换为 CNF（支持量词忽略的 CNF 生成） |
ctx-solver-simplify | 动态上下文相关简化（基于当前断言集优化表达式） |
elim-and | 将逻辑与（AND）转换为或（OR）和非（NOT）的组合 |
purify-arith | 消除冗余算术运算符（如 -, ^, mod） |
特殊问题策略
| 方法名 | 描述 |
|---|
horn | 处理 Horn 子句（用于递归约束或程序验证） |
subpaving | 子空间划分模块测试（用于非线性实数约束） |
card2bv | 将伪布尔约束转换为位向量 |
lia2pb | 将受限整数变量转换为 0-1 变量序列 |
recover-01 | 从布尔变量中恢复 0-1 整数变量 |
qfaufbv | 求解含数组和未解释函数的位向量（QF_AUFBV）问题 |
高级逻辑处理
| 方法名 | 描述 |
|---|
dt2bv | 将有限域数据类型替换为位向量 |
elim-term-ite | 通过引入辅助变量消除条件表达式（if-then-else） |
macro-finder | 识别和应用宏（等价替换） |
quasi-macros | 识别和应用拟宏（部分等价替换） |
special-relations | 检测并替换特殊关系（如偏序、传递闭包） |
并行与本地搜索
| 方法名 | 描述 |
|---|
psat | 并行 SAT 求解器（加速布尔问题求解） |
qfbv-sls | 随机本地搜索策略（用于 QF_BV 问题的启发式求解） |
sls-smt | 本地搜索策略（尝试解决通用 SMT 问题） |
调试与统计
| 方法名 | 描述 |
|---|
collect-statistics | 收集统计信息（如变量数、约束数） |
solver-subsumption | 移除被蕴含的断言（简化问题集） |
sat-preprocess | SAT 预处理（子句消解、常量传播、2-SAT 化简） |