简而言之,我需要能够遍历Z3_ast树并访问与其节点相关的数据.似乎无法找到有关如何做到这一点的任何文档/示例.任何指针都会有所帮助.
最后,我需要将smt2lib类型的公式解析为Z3,将一些变量变为常量替换,然后在数据结构中重现公式,该数据结构与另一个不相关的SMT sovler兼容(具体来说,我不认为有关misral的详细信息)对于这个问题很重要但有趣的是它没有命令行界面,我可以在其中提供文本公式.它只有一个C API).我已经想过要以mistral的格式生成公式,我需要遍历Z3_ast树并以所需的格式重建公式.我似乎无法找到任何演示如何执行此操作的文档/示例.任何指针都会有所帮助.
我正在使用Z3的python api来做一些增量求解.我迭代地将约束推送到求解器,同时使用solver.push()命令检查每个步骤的不可满足性.我想了解Z3是否会使用先前约束的学习引理或者在使用新添加的约束求解时先前获得的满意解.我从不使用solver.pop()命令.在哪里可以获得有关如何使用先前迭代中完成的工作的更多详细信息？