开发工具【免费下载链接】z3The Z3 Theorem Prover项目地址https://gitcode.com/gh_mirrors/z3/z3点击查看免费下载Z3 是由微软研究院开发的高性能 SMTSatisfiability Modulo Theories求解器而本仓库的src/api/go目录为其提供了完整的 Go 语言绑定。本文以该目录下的 README.md 为骨架结合绑定源码、CMake 集成与示例程序系统讲解如何在 Go 项目中创建上下文、构造表达式、求解约束、读取模型并覆盖位向量、浮点、数组、字符串、正则、代数数据类型、Tactic、Optimize、Fixedpoint 等全部能力模块同时深入剖析 CGO 内存管理与线程安全细节。一、绑定总览能力矩阵与文件布局Go 绑定通过 CGO 对 Z3 的 C API头文件位于 src/api/z3.h进行薄封装把 C 风格的句柄操作转换为符合 Go 习惯的面向对象接口。绑定包自身位于 src/api/go 目录包声明为package z3模块路径为github.com/Z3Prover/z3/src/api/go见 src/api/go/go.mod要求 Go 1.20。核心文件分布如下文件职责z3.go基础类型Context/Config/Symbol/AST/Sort/Expr/FuncDecl、布尔与算术运算、量化器、Lambda、类型变量、全局参数arith.go整数/实数算术扩展bitvec.go位向量全部运算fp.goIEEE 754 浮点运算与舍入模式array.goSelect/Store 等数组操作seq.go序列与字符串操作relations.go正则表达式操作datatype.go代数数据类型solver.goSolver 与 Modeloptimize.go优化求解fixedpoint.go不动点求解Datalog/CHCtactic.goTactic 与 Goalpropagator.go用户传播器user propagatorspacer.goSpacer 引擎相关log.go交互日志simplifier.go简化器功能覆盖范围包括核心类型Context、Config、Symbol、AST、Sort、Expr、FuncDecl、Solver 操作、模型提取与求值、布尔逻辑And/Or/Not/Implies/Iff/Xor、算术Add/Sub/Mul/Div/Mod 及比较、位向量、浮点、数组、序列/字符串、正则表达式、量化器Forall/Exists、函数声明与应用、Tactic/Goal/Probe、代数数据类型、参数配置、Optimize 优化求解以及 FixedpointDatalog/CHC。二、构建与安装从 Z3 源码到可用的 Go 包2.1 前置条件Go 1.20 或更高版本go.mod 中明确声明已构建并安装的 Z3 库libz3启用 CGO绑定依赖cgo编译时需要 C 编译器gcc/clang/MSVC必要时显式设置CGO_ENABLED1Z3 API 头文件可访问绑定源码通过#cgo CFLAGS: -I${SRCDIR}/..自动包含 src/api 目录见 z3.go外部构建时通常仍需显式指定头文件路径。2.2 使用 CMake 构建 Z3 并启用 Go 绑定仓库根目录的 CMake 工程通过Z3_BUILD_GO_BINDINGS选项控制 Go 绑定的安装与测试目标见 src/api/go/CMakeLists.txtcmake -S . -B build -DZ3_BUILD_GO_BINDINGSON cmake --build build --parallel该 CMakeLists 是一个“占位集成”文件绑定本身由 Go 工具链直接构建CMake 负责三件事将z3.go、solver.go、go.mod、README.md安装到${CMAKE_INSTALL_LIBDIR}/go/src/github.com/Z3Prover/z3/go在 Windows 上提醒需要将libz3.dll放入PATH检测到 Go 时生成go-bindings与test-go-examples两个自定义目标分别以CGO_CFLAGS-Isrc/api、CGO_LDFLAGS-Lbuild -lz3执行go build -v与go run basic_example.go见 src/api/go/CMakeLists.txt。2.3 手动配置 CGO 环境Linux/macOS 与 Windows在 examples/go 目录下运行示例前需要让 CGO 找到头文件与共享库Windows 上PATH需指向 DLL 所在目录通常为build\Releasecd examples/go # 库路径Linux/macOS export LD_LIBRARY_PATH../../build:$LD_LIBRARY_PATH export CGO_CFLAGS-I../../src/api export CGO_LDFLAGS-L../../build -lz3 # 运行示例 go run basic_example.goREM Windows set PATH..\..\build\Release;%PATH% set CGO_CFLAGS-I..\..\src\api set CGO_LDFLAGS-L..\..\build\Release -lz3 go run basic_example.go从实现上看z3.go 中的指令#cgo CFLAGS: -I${SRCDIR}/..与#cgo LDFLAGS: -lz3已经提供了默认值CGO_CFLAGS/CGO_LDFLAGS环境变量则用于在开发阶段覆盖默认值指向尚未安装的本地构建产物。2.4 常见故障排查undefined reference to Z3_*Z3 未构建或库不在链接路径检查CGO_LDFLAGS的-L路径Windows 下确认 DLL 在PATH中cannot find packageCGO_CFLAGS未包含 Z3 API 头文件目录src/api或缺少 src/api/go/go.modCGO 编译错误确认CGO_ENABLED1、已安装 C 编译器、头文件可访问。三、快速上手第一个 Go 求解程序绑定包的使用模式高度一致先建 Context再构造表达式最后交给 Solver 求解并从 Model 中取回结果。以下是 README.md 提供的最小可运行示例package main import ( fmt github.com/Z3Prover/z3/src/api/go ) func main() { // 创建上下文 ctx : z3.NewContext() // 创建变量 x : ctx.MkIntConst(x) y : ctx.MkIntConst(y) // 创建约束x y 10 x y ten : ctx.MkInt(10, ctx.MkIntSort()) eq : ctx.MkEq(ctx.MkAdd(x, y), ten) gt : ctx.MkGt(x, y) // 创建求解器并检查 solver : ctx.NewSolver() solver.Assert(eq) solver.Assert(gt) if solver.Check() z3.Satisfiable { model : solver.Model() if xVal, ok : model.Eval(x, true); ok { fmt.Println(x , xVal.String()) } if yVal, ok : model.Eval(y, true); ok { fmt.Println(y , yVal.String()) } } }其中几个关键 API 的底层实现值得注意NewContext()z3.go内部调用Z3_mk_context_rc创建引用计数上下并随即调用Z3_enable_concurrent_dec_ref以支持并发 GC 期间的引用释放然后通过runtime.SetFinalizer在上下文被回收时调用Z3_del_contextCheck()solver.go直接映射 C APIZ3_solver_check返回值被转换为Status枚举Unsatisfiable(-1)、Unknown(0)、Satisfiable(1)其String()分别输出unsat/unknown/sat见 solver.goEval(expr, modelCompletion)solver.go封装Z3_model_eval当modelCompletion为true时Z3 会为未解释常量补全赋值避免求值返回失败。examples/go/basic_example.go 给出了更完整的四个场景x 0的简单求解、x y 10 ∧ x - y 2的方程组、(p ∨ q) ∧ (¬p ∨ ¬q)的布尔可满足性以及a 0 ∧ a 0的不可满足判定输出Status: unsat并演示了solver.Reset()在同一求解器上复用。四、表达式构造 API 参考所有表达式构造函数都以Mk*前缀命名挂在*Context上表达式对象*Expr的String()返回 SMT 风格的字符串表示Z3_ast_to_string。4.1 Context 与基础类型NewContext()创建默认配置的上下文NewContextWithConfig(cfg *Config)以指定配置创建上下文SetParam(key, value string)设置上下文/全局参数底层为Z3_update_param_valueNewConfig()/(*Config).SetParamValue(id, value string)创建并配置 Config 对象再传给NewContextWithConfig。4.2 变量与常量方法说明MkBoolConst(name string)创建布尔变量MkIntConst(name string)创建整数变量MkRealConst(name string)创建实数变量MkInt(value int, sort *Sort)创建整数常量sort通常为ctx.MkIntSort()MkReal(num, den int)创建有理数常量num/denMkConst(name *Symbol, sort *Sort)通用常量构造z3.goMkNumeral(numeral string, sort *Sort)从字符串创建数字MkBoolConst的实现是MkStringSymbol(name)MkConst(sym, MkBoolSort())见 z3.go理解这一点后遇到需要任意 sort 的变量时可自行组合MkConst。4.3 布尔运算MkAnd(exprs ...*Expr)/MkOr(exprs ...*Expr)合取/析取变参支持任意多个子式MkAnd()空参返回trueMkOr()空参返回false单参直接返回自身见 z3.goMkNot(expr *Expr)否定MkImplies(lhs, rhs *Expr)蕴含MkIff(lhs, rhs *Expr)当且仅当MkXor(lhs, rhs *Expr)异或。4.4 算术运算MkAdd(exprs ...*Expr)/MkSub(exprs ...*Expr)/MkMul(exprs ...*Expr)加减乘MkDiv(lhs, rhs *Expr)除法MkMod(lhs, rhs *Expr)模运算MkRem(lhs, rhs *Expr)余数。4.5 比较运算MkEq相等、MkDistinct(exprs ...*Expr)两两不同、MkLt/MkLe/MkGt/MkGe小于/小于等于/大于/大于等于。MkDistinct在参数少于两个时直接返回true见 z3.go。4.6 伪布尔约束除了 README 列出的基础运算z3.go 还提供了伪布尔/基数约束MkAtMost(args, k)p1...pn ≤ k、MkAtLeast(args, k)、MkPBLe(args, coeffs, k)、MkPBGe、MkPBEq。后三者要求args与coeffs长度一致否则直接panic。五、求解器与模型5.1 Solver 核心操作NewSolver()在当前上下文创建求解器Z3_mk_solverAssert(constraint *Expr)加入约束Z3_solver_assertCheck()返回Satisfiable/Unsatisfiable/Unknown三态Model()可满足时返回模型不可满足时返回nilPush()/Pop(n uint)回溯点管理Reset()清空所有断言。除此之外solver.go 还暴露了大量实用方法高级检查CheckAssumptions(assumptions ...*Expr)带假设检查用于提取 unsat core、GetConsequences(assumptions, variables)在假设下推导变量必然取值、Cube(vars, cutoff)提取文字合取立方诊断信息ReasonUnknown()unknown的原因、GetStatistics()求解统计、GetHelp()可用参数说明、GetParamDescrs()、Units()/NonUnits()单元/非单元子句、Trail()/TrailLevels()决策路径与层级、CongruenceRoot/Next/Explain同余类遍历与解释主要适用于 SimpleSolver输入输出FromFile(filename)/FromString(str)解析并断言 SMT-LIB2 公式、Dimacs(includeNames bool)导出 DIMACS CNF其他AssertAndTrack、UnsatCore()、GetProof()不可满足证明、Translate(target)跨上下文复制、SetInitialValue(variable, value)初始值提示加速搜索、SolveFor(...)、ImportModelConverter(...)、AddSimplifier(...)。5.2 Model 操作Eval(expr *Expr, modelCompletion bool)在模型中求值表达式成功返回(表达式, true)失败返回(nil, false)NumConsts()/NumFuncs()模型中的常量/函数解释数量String()模型完整字符串表示进阶GetConstDecl(i)/GetFuncDecl(i)、GetConstInterp(decl)、GetFuncInterp(decl)函数插值FuncInterp支持NumEntries/GetElse/GetEntry/AddEntry/SetElse条目FuncEntry支持GetValue/GetNumArgs/GetArg、HasInterp(decl)、SortUniverse(sort)未解释 sort 的论域、Translate(target)。5.3 一个可复用的求解模板综合 examples/go/basic_example.go 的写法推荐如下模板含假设与 unsat corectx : z3.NewContext() solver : ctx.NewSolver() // ... solver.Assert(...) ... assumption : ctx.MkBoolConst(assumption) status : solver.CheckAssumptions(assumption) switch status { case z3.Satisfiable: m : solver.Model() // m.Eval(expr, true) case z3.Unsatisfiable: core : solver.UnsatCore() // 需要启用 unsat core 生成 case z3.Unknown: fmt.Println(solver.ReasonUnknown()) }六、理论模块深入位向量、浮点、数组与字符串6.1 位向量Bit-vectors排序与常量MkBvSort(sz uint)、MkBVConst(name string, size uint)、MkBV(value, size)见 examples/go/advanced_example.go 中ctx.MkBV(255, 8)的用法算术MkBVAdd/MkBVSub/MkBVMul/MkBvUDiv无符号除/MkBvSDiv有符号除位运算MkBVAnd/MkBVOr/MkBvXor/MkBvNot移位MkBvShl逻辑左移/MkBvLShr逻辑右移/MkBvAShr算术右移比较无符号MkBvULT/ULE/UGT/UGE、有符号MkBvSLT/SLE/SGT/SGE切片与拼接MkConcat(lhs, rhs)、MkExtract(high, low uint, expr)、MkSignExt(i, expr)、MkZeroExt(i, expr)。示例来自 examples/go/advanced_example.gox y 255 x y其中x, y为 8 位位向量x : ctx.MkBVConst(x, 8) y : ctx.MkBVConst(y, 8) solver.Assert(ctx.MkEq(ctx.MkBVAdd(x, y), ctx.MkBV(255, 8))) solver.Assert(ctx.MkBVUGT(x, y))6.2 浮点IEEE 754排序MkFPSort(ebits, sbits uint)自定义指数/尾数位宽快捷方法MkFPSort16/32/64/128()舍入模式排序MkFPRoundingModeSort()特殊值MkFPInf/MkFPNaN/MkFPZero(sort, negative bool)注意 advanced_example.go 中MkFPZero(fpSort, false)表示正零算术均需舍入模式参数MkFPAdd(rm, lhs, rhs)/MkFPSub/MkFPMul/MkFPDiv一元操作MkFPNeg/MkFPAbs/MkFPSqrt比较MkFPLT/GT/LE/GE/Eq谓词MkFPIsNaN/MkFPIsInf/MkFPIsZero。示例来自 advanced_example.gofpSort : ctx.MkFPSort32() a : ctx.MkConst(ctx.MkStringSymbol(a), fpSort) b : ctx.MkConst(ctx.MkStringSymbol(b), fpSort) rm : ctx.MkConst(ctx.MkStringSymbol(rm), ctx.MkFPRoundingModeSort()) solver.Assert(ctx.MkFPGT(ctx.MkFPAdd(rm, a, b), ctx.MkFPZero(fpSort, false)))6.3 数组绑定支持 Select取值、Store写值与常量数组构造相关实现位于 src/api/go/array.go。6.4 序列与字符串排序MkStringSort()、MkSeqSort(elemSort *Sort)常量MkString(value string)操作MkSeqConcat(exprs ...*Expr)拼接、MkSeqLength(seq)长度、MkSeqPrefix/Suffix/Contains前缀/后缀/包含、MkSeqAt(seq, index)取元素、MkSeqExtract(seq, offset, length)子串、MkStrToInt/IntToStr类型转换。示例来自 advanced_example.go约束s1 contains hello length(s1) 20 s2 s1 worlds1 : ctx.MkConst(ctx.MkStringSymbol(s1), ctx.MkStringSort()) hello : ctx.MkString(hello) solver.Assert(ctx.MkSeqContains(s1, hello)) solver.Assert(ctx.MkLt(ctx.MkSeqLength(s1), ctx.MkInt(20, ctx.MkIntSort()))) solver.Assert(ctx.MkEq(s2, ctx.MkSeqConcat(s1, ctx.MkString( world))))七、正则表达式与代数数据类型7.1 正则表达式正则操作全部围绕“字符串-正则”二元关系展开实现在 src/api/go/relations.go排序MkReSort(seqSort *Sort)构造MkToRe(seq)字符串转正则、MkReStarKleene 星号零次或多次、MkRePlus一次或多次、MkReOption零次或一次、MkRePower(re, n)恰好 n 次、MkReLoop(re, lo, hi)限定次数区间、MkReConcat拼接、MkReUnion并/或、MkReIntersect交、MkReComplement补、MkReDiff(a, b)差、MkReEmpty/Full/Allchar特殊正则、MkReRange(lo, hi)字符区间匹配MkInRe(seq, re)字符串匹配正则的谓词替换MkSeqReplaceRe/ReAll(seq, re, replacement)。完整示例见 advanced_example.go构造正则(a|b)*c并断言字符串匹配reA : ctx.MkToRe(ctx.MkString(a)) reB : ctx.MkToRe(ctx.MkString(b)) reC : ctx.MkToRe(ctx.MkString(c)) aOrB : ctx.MkReUnion(reA, reB) regex : ctx.MkReConcat(ctx.MkReStar(aOrB), ctx.MkRePlus(reC)) solver.Assert(ctx.MkInRe(str, regex)) solver.Assert(ctx.MkLt(ctx.MkSeqLength(str), ctx.MkInt(10, ctx.MkIntSort())))7.2 代数数据类型MkConstructor(name, recognizer string, ...)创建构造器MkDatatypeSort(name string, constructors []*Constructor)创建数据类型MkDatatypeSorts(names []string, ...)互递归数据类型MkTupleSort(name string, fieldNames []string, fieldSorts []*Sort)元组返回 sort、构造器与投影函数见 advanced_example.go 的Point{x, y}例子MkEnumSort(name string, enumNames []string)枚举返回常量声明列表见Color{Red, Green, Blue}例子MkListSort(name string, elemSort *Sort)列表返回 sort 及 nil/cons/head/tail 等声明见 advanced_example.go 的IntList例子。示例创建cons(1, cons(2, nil))并断言head(list) 1intSort : ctx.MkIntSort() listSort, nilDecl, consDecl, _, _, headDecl, _ : ctx.MkListSort(IntList, intSort) nilList : ctx.MkApp(nilDecl) list12 : ctx.MkApp(consDecl, ctx.MkInt(1, intSort), ctx.MkApp(consDecl, ctx.MkInt(2, intSort), nilList)) listVar : ctx.MkConst(ctx.MkStringSymbol(mylist), listSort) solver.Assert(ctx.MkEq(listVar, list12)) solver.Assert(ctx.MkEq(ctx.MkApp(headDecl, listVar), ctx.MkInt(1, intSort)))八、Tactic 与 Probe目标驱动的策略求解8.1 Tactic 组合子Tactic 通过名字创建可组合成复杂求解策略见 src/api/go/tactic.goMkTactic(name string)按名称创建策略如simplify、qfbvMkGoal(models, unsatCores, proofs bool)创建目标三个布尔参数分别开启模型/unsat core/证明生成Apply(g *Goal)将策略作用于目标返回ApplyResult可查询NumSubgoals()、Subgoal(i)AndThen(t2 *Tactic)顺序组合OrElse(t2 *Tactic)先试t失败则回退t2Repeat(max uint)反复应用至多max次TacticWhen(p *Probe, t *Tactic)/TacticCond(p *Probe, t1, t2 *Tactic)条件策略额外提供TacticFail()/TacticSkip()。示例来自 advanced_example.gogoal : ctx.MkGoal(true, false, false) goal.Assert(ctx.MkGt(p, ctx.MkInt(0, ctx.MkIntSort()))) goal.Assert(ctx.MkEq(ctx.MkAdd(p, q), ctx.MkInt(10, ctx.MkIntSort()))) tactic : ctx.MkTactic(simplify) result : tactic.Apply(goal) fmt.Printf(Tactic produced %d subgoals\n, result.NumSubgoals()) fmt.Println(Simplified goal:, result.Subgoal(0).String())8.2 Probe 操作MkProbe(name string)按名创建探针对目标性质做布尔判定如规模、理论特征等(*Probe).Apply(g *Goal)在目标上求值Lt/Gt/Le/Ge/Eq(p2 *Probe)探针数值比较And/Or/Not(...)探针组合子。九、Optimize最大/最小化目标求解Optimize 上下文在可满足性之外还支持目标函数优化MaxSMT实现在 src/api/go/optimize.goNewOptimize()创建优化上下文Assert(constraint *Expr)加入硬约束AssertSoft(constraint *Expr, weight, group string)加入带权重的软约束MaxSMT返回目标句柄Maximize(expr *Expr)/Minimize(expr *Expr)加入最大化/最小化目标返回目标句柄uint索引Check(assumptions ...*Expr)检查并求解最优值Model()获取最优模型GetLower(index uint)/GetUpper(index uint)目标下界/上界Push()/Pop()回溯Assertions()/Objectives()查询断言与目标UnsatCore()不可满足核心。示例来自 advanced_example.gox y ≤ 10, x ≥ 0, y ≥ 0下最大化x 2yopt : ctx.NewOptimize() opt.Assert(ctx.MkLe(ctx.MkAdd(xOpt, yOpt), tenOpt)) opt.Assert(ctx.MkGe(xOpt, zeroOpt)) opt.Assert(ctx.MkGe(yOpt, zeroOpt)) objHandle : opt.Maximize(ctx.MkAdd(xOpt, ctx.MkMul(twoOpt, yOpt))) if opt.Check() z3.Satisfiable { model : opt.Model() // model.Eval(xOpt, true) ... upper : opt.GetUpper(objHandle) // 最优值 }十、Fixedpoint 与 Quantifier不动点求解与量词10.1 FixedpointDatalog/CHCNewFixedpoint()创建不动点求解器RegisterRelation(funcDecl *FuncDecl)注册谓词AddRule(rule *Expr, name *Symbol)添加 Horn 子句AddFact(pred *FuncDecl, args []int)添加表事实Query(query *Expr)查询约束QueryRelations(relations []*FuncDecl)查询关系GetAnswer()获取满足实例或证明Push()/Pop()回溯。10.2 Quantifier 与 LambdaMkQuantifier(isForall bool, weight int, sorts, names, body, patterns)创建量词要求 sorts 与 names 长度一致否则 panicMkQuantifierConst(isForall bool, weight int, bound, body, patterns)以常量作为约束变量创建量词便捷方法MkForall(bound []*Expr, body *Expr)/MkExists(...)z3.go权重为 0、无 pattern查询IsUniversal()/IsExistential()、GetNumBound()、GetBoundName(idx)/GetBoundSort(idx)、GetBody()、GetNumPatterns()/GetPattern(idx)、GetWeight()LambdaMkLambda(sorts, names, body)/MkLambdaConst(bound, body)查询接口与量词一致复用Z3_get_quantifier_*系列 C API。此外绑定还支持MkTypeVariable(name *Symbol)创建多态类型变量 sort用于多态函数与数据类型见 z3.go。十一、内存管理与线程安全11.1 自动引用计数Finalizer 机制绑定通过runtime.SetFinalizer自动管理 Z3 引用计数见 z3.go 的包注释与各类型构造函数。每个包装对象Context、Sort、Expr、FuncDecl、Solver、Model、Optimize、Tactic等创建时都对底层 C 句柄调用*_inc_ref并在 finalizer 中调用对应的*_dec_ref。例如newExpr创建时Z3_inc_ref回收时Z3_dec_refz3.goNewSolver创建时Z3_solver_inc_ref回收时Z3_solver_dec_refsolver.goNewOptimize同理optimize.go。你不需要也不应该手动调用inc_ref/dec_ref。但要注意finalizer 在 Go 垃圾回收阶段才运行因此资源释放并非即时发生。为了在并发 GC 场景下安全地执行 decref绑定在创建上下文时调用了Z3_enable_concurrent_dec_ref见 z3.go这是 README 明确强调的并发安全关键点。11.2 线程安全约束Z3 上下文不是线程安全的。README 明确要求每个 goroutine 应使用自己的 Context或在对共享上下文访问时加合适的同步mutex 等。这与 Z3 C API 的线程模型一致——一个Context同一时刻只允许单线程访问。十二、日志与全局参数12.1 交互日志src/api/go/log.goOpenLog(filename string)打开交互日志CloseLog()关闭日志AppendLog(s string)追加内容IsLogOpen()查询日志是否打开。日志记录了 C API 调用序列可用于回放调试Z3 提供z3_replayer机制见 src/api/z3_replayer.cpp。12.2 全局参数z3.goSetGlobalParam(id, value string)设置全局参数Z3_global_param_setGetGlobalParam(id string) (string, bool)读取全局参数第二个返回值表示参数是否存在ResetAllGlobalParams()重置所有全局参数为默认值。十三、示例程序与预期输出仓库在 examples/go 提供了三个可直接运行的示例文件内容basic_example.go基础整数约束、方程组、布尔逻辑、不可满足判定advanced_example.go进阶位向量、浮点、字符串、列表数据类型、Tactic、枚举、元组、正则、Optimizenew_api_example.go新 API 特性演示运行basic_example.go的预期输出完整版见 examples/go/README.md节选Z3 Go Bindings - Basic Example Example 1: Solving x 0 Satisfiable! x 1 Example 2: Solving x y 10 ∧ x - y 2 Satisfiable! x 6 y 4 Example 3: Boolean satisfiability Satisfiable! p false q true Example 4: Checking unsatisfiability Status: unsat十四、综合示例把各部分串起来下面结合本文介绍的模块构造一个同时使用位向量、正则、Optimize 与 Tactic 的完整程序示意package main import ( fmt github.com/Z3Prover/z3/src/api/go ) func main() { ctx : z3.NewContext() // 1) 位向量求解 8 位 x y 255 且 x y无符号 x : ctx.MkBVConst(x, 8) y : ctx.MkBVConst(y, 8) solver : ctx.NewSolver() solver.Assert(ctx.MkEq(ctx.MkBVAdd(x, y), ctx.MkBV(255, 8))) solver.Assert(ctx.MkBVUGT(x, y)) if solver.Check() z3.Satisfiable { m : solver.Model() vx, _ : m.Eval(x, true) vy, _ : m.Eval(y, true) fmt.Println(bv:, vx.String(), vy.String()) } // 2) 字符串 正则(a|b)*c 且长度 10 solver.Reset() str : ctx.MkConst(ctx.MkStringSymbol(str), ctx.MkStringSort()) re : ctx.MkReConcat( ctx.MkReStar(ctx.MkReUnion(ctx.MkToRe(ctx.MkString(a)), ctx.MkToRe(ctx.MkString(b)))), ctx.MkRePlus(ctx.MkToRe(ctx.MkString(c))), ) solver.Assert(ctx.MkInRe(str, re)) solver.Assert(ctx.MkLt(ctx.MkSeqLength(str), ctx.MkInt(10, ctx.MkIntSort()))) if solver.Check() z3.Satisfiable { m : solver.Model() v, _ : m.Eval(str, true) fmt.Println(regex match:, v.String()) } // 3) Optimize最大化 x 2y约束 x y 10, x, y 0 opt : ctx.NewOptimize() xo : ctx.MkIntConst(xo) yo : ctx.MkIntConst(yo) opt.Assert(ctx.MkLe(ctx.MkAdd(xo, yo), ctx.MkInt(10, ctx.MkIntSort()))) opt.Assert(ctx.MkGe(xo, ctx.MkInt(0, ctx.MkIntSort()))) opt.Assert(ctx.MkGe(yo, ctx.MkInt(0, ctx.MkIntSort()))) h : opt.Maximize(ctx.MkAdd(xo, ctx.MkMul(ctx.MkInt(2, ctx.MkIntSort()), yo))) if opt.Check() z3.Satisfiable { fmt.Println(optimal x2y , opt.GetUpper(h).String()) } }十五、许可证与参与贡献Z3 采用 MIT 许可证完整文本见仓库根目录 LICENSE.txt。Go 绑定作为仓库的一部分遵循相同许可。Bug 报告与代码贡献欢迎提交到主 Z3 仓库本文所述全部 API 的权威来源是 src/api/go/README.md 与各 Go 源文件运行示例与排障指南可进一步参考 examples/go/README.md。赞分享开发工具【免费下载链接】z3The Z3 Theorem Prover项目地址https://gitcode.com/gh_mirrors/z3/z3点击查看免费下载相关推荐go-ole用 Go 语言免 cgo 调用 Windows COM 的绑定库实战指南go ole用 Go 语言免 cgo 调用 Windows COM 的绑定库实战指南 导读 go ole 是 Go 语言编写的 Windows COMCom云原生容器运行时Go-SQLite3基于Wazero的无CGO SQLite绑定Go SQLite3基于Wazero的无CGO SQLite绑定 项目介绍 Go SQLite3 是一个基于 Wazero 的 SQLite 绑定库完全避免数据库嵌入式数据库后端Go 语言 WMI 编程实战基于 yusufpapurcu/wmi 的 WQL 查询接口详解Go 语言 WMI 编程实战基于 yusufpapurcu/wmi 的 WQL 查询接口详解 导读 本文围绕 scan4all 项目 vendor 目录下所携网络安全漏洞扫描渗透测试应用安全创作声明：本文部分内容由AI辅助生成（AIGC），仅供参考