加快Z3对特定QF_LRA实例的处理

Question

我在QF_LRA中遇到了一个问题，这个问题由MathSAT5 (unsat，<5分钟)解决得非常快，但是Z3似乎没有什么进展(即使在7天之后也没有结果)。这能通过Z3中的一些设置来解决吗？

它包含了(大致)这5种类型的许多子句：

(assert (or (< p47a2 p8a2) (< (+ p47a0 p47a2) (+ p8a0 p8a2)) (< (+ p47a0 p47a2 p47a3) (+ p8a0 p8a2 p8a3)) (and (= p47a2 p8a2) (= (+ p47a0 p47a2) (+ p8a0 p8a2)) (= (+ p47a0 p47a2 p47a3) (+ p8a0 p8a2 p8a3)))))
(assert (= 1.0 (+ p3887a0 p3887a1 p3887a2 p3887a3)))
(assert (>= p1715a0 0.0))    
(assert (= p133a2 p133a1))
(assert (or (= p379a1 0.0) (= p379a2 0.0)))

完整的问题实例可以从这里以SMT2格式下载。

用MathSAT解决这个问题的关键是设置

preprocessor.simplification=8

它支持全局重写规则(除了SMT 2015竞赛的应用程序跟踪设置)。

在Z3中有类似的东西我可以尝试吗？或者对你建议我执行的编码进行预处理/优化？我是相对较新的SMT，因此，任何帮助/指导将不胜感激。

首先，让Z3来解决这个实例是很好的。作为下一步，我也想提取一个unsat核心，如果这是重要的提示。

非常感谢！！

Answer 1

将(check-sat)替换为

(check-sat-using (then simplify solve-eqs (! smt :case_split 0 :relevancy 0 :auto_config false :restart_strategy 2)) :print_model true)

Z3马上就解决了。但是，您可以找到更好的配置这里。