我在UFBV查询上运行Z3.目前查询包含2个调用check-sat.如果放在Z3 push 1之后check-sat在30秒内解决查询.如果不放任何东西push 1- Z3在200秒内解决它.有趣.任何具体原因还是巧合？
Z3 3.x有一种基于战术和战术的"战略规范语言".我还没有"广告",因为它正在进行中.这个幻灯片中描述了基本思想.我们为每个逻辑都有不同的内置策略.策略通常不支持增量求解,因为它们可能应用使用"封闭世界"假设的转换.例如,我们有将0-1线性整数算法映射到SAT的转换.每当Z3检测到用户"想要"增量求解(例如,多个check-sat命令push和pop命令)时,它就会切换到通用求解器.在未来的版本中,我们将提供更多用于控制Z3行为的功能.
顺便说一句,如果你有两个连续的(check-sat) (check-sat)命令,Z3不一定进入增量模式.只有在两个呼叫之间存在assert或push命令时才会进入.
现在,假设您的查询格式为:(check-sat) <assertions> (check-sat),并且您的第二个查询属于表单(check-sat) <assertions> (push) (check-sat).在这两种情况下,Z3将在第二种情况下处于增量模式(check-sat).但是,行为仍然不一样.增量求解"编译"的断言公式的内部格式,如果其行为影响push的命令已被执行.例如,只有在没有用户范围的情况下,它才会使用更有效的二进制子句编码.根据用户范围,我的意思是push命令数量 - pop命令数量.这样做是因为在更有效的编码中使用的数据结构没有有效的撤销/反向操作.
| 归档时间： |
|
| 查看次数： |
865 次 |
| 最近记录： |