我正在编写一个研究工具,我最近从使用"print"语句切换到使用Python内置的记录器功能.我推断,这将允许我为用户提供将输出转储到文件的选项,除了将其转储到屏幕上.
到现在为止还挺好.我在Python中的代码部分使用"logger.info"和"logger.error"转储到屏幕和文件."logger"是模块范围的记录器.这部分就像一个魅力.
但是,在几个点上,我使用"subprocess.call"通过shell运行可执行文件.所以,在整个代码中,我有类似的行
proc = subprocess.call(command)
此命令的输出将一如既往地打印到屏幕,但不会转储到用户指定的文件.
一种可能的选择是打开文件管道:
proc = subprocess.call(command, stdout=f, stderr=subprocess.OUTPUT)
但那只会转储到文件而不是屏幕.
基本上,我的问题归结为:有没有办法可以利用我现有的记录器,而不必为subprocess.call专门构建文件的另一个处理程序？(也许是通过将输出重定向到记录器？)或者这是不可能的,考虑到当前的设置？如果是后者,我该如何改进设置？
(哦,如果日志记录是"实时"的话会很棒,这样来自可执行文件的消息会在收到时记录下来.)
谢谢你的帮助!:)
我目前正在研究将通过C程序的“路径”转换为相应的SMT查询以测试该路径的可行性的代码。我有创建SMT-LIB v1.2查询的工作代码，该代码使用Z3 2.11和QF_AUFBV逻辑来解决查询。我目前正在将此代码移植到Z3 4.3，以利用此后可能发生的任何速度提升，尤其是因为我以前的代码似乎花很长时间（大约22分钟）处理仅向其分配24个值的查询一个三维数组，并检查数组中某个位置的值。
但是，似乎QF_AUFBV逻辑（从SMT-LIB v2.0标准开始）不再支持多维数组，或者不再支持其值也是数组的数组（可能更深）。一旦从查询中删除“（set-logic QF_AUFBV）”行，Z3 4.3就可以处理该查询，但是仍然需要很长时间。
我想知道是否有人知道为什么在SMT-LIB v2.0标准中停止了对多维数组的支持，以及我可以使用哪些替代逻辑。我还想知道，当我删除指定QF_AUFBV理论的那一行时，Z3到底在使用什么逻辑。
谢谢！
我正在使用Z3的Python API,试图在我正在编写的研究工具中包含对它的支持.我有一个关于使用Python接口提取不可满足核心的问题.
我有以下简单查询:
(set-option :produce-unsat-cores true)
(assert (! (not (= (_ bv0 32) (_ bv0 32))) :named __constraint0))
(check-sat)
(get-unsat-core)
(exit)
通过z3可执行文件(对于Z3 4.1)运行此查询,我收到了预期的结果:
unsat
(__constraint0)
对于Z3 4.3,我获得了一个分段错误:
unsat
Segmentation fault
这不是主要问题,尽管这是一个有趣的观察.然后我将查询(在文件中)修改为
(assert (! (not (= (_ bv0 32) (_ bv0 32))) :named __constraint0))
(exit)
使用文件处理程序,我将此文件的内容(在变量`queryStr'中)传递给以下Python代码:
import z3
...
solver = z3.Solver()
solver.reset()
solver.add(z3.parse_smt2_string(queryStr))
querySatResult = solver.check()
if querySatResult == z3.sat:
...
elif querySatResult == z3.unsat:
print solver.unsat_core()
我从`unsat_core'函数接收空列表:[].我是否正确使用此功能？该函数的文档字符串表明我应该做类似的事情
solver.add(z3.Implies(p1, z3.Not(0 == 0)))
但是,我想知道是否仍然可以按原样使用查询,因为它符合SMT-LIB v2.0标准(我相信),以及我是否遗漏了一些明显的东西.