1

我有以下 Z3 超时的简单示例：

(set-option :produce-models true) 
(define-fun T_0 (($in1 Real) ($in2 Real)
  ($out Real) ($assms Bool) ($prop Bool)) Bool 
   (and (= $assms (< $in1 $in2)) 
        (= $prop (=> $assms (and (< $in1 $out) (< $out $in2))))))

(declare-fun $in1$0 () Real)
(declare-fun $in2$0 () Real)
(declare-fun $out$0 () Real)
(declare-fun $assms$0 () Bool)

(assert (forall (($out$0 Real) ($assms$0 Bool)) 
           (not (and (T_0 $in1$0 $in2$0 $out$0 $assms$0 true)))))
(check-sat)

现在，如果我们简化断言，传播相等性，z3 立即返回 UNSAT（如预期的那样）：

(define-fun T_1 (($in1 Real) ($in2 Real)
    ($out Real) ($prop Bool)) Bool 
      (and  (= $prop (=> (< $in1 $in2) (and (< $in1 $out) (< $out $in2))))))
(declare-fun $in1$0 () Real)
(declare-fun $in2$0 () Real)
(declare-fun $out$0 () Real)
(assert (forall (($out$0 Real) ($assms$0 Bool)) 
           (not (and (T_1 $in1$0 $in2$0 $out$0 true)))))
(check-sat)

这个例子似乎表明 Z3 不会在量词下传播等式。例如，以下断言有效（产生 UNSAT）：

 (assert (forall (($out$0 Real)) 
     (and (not (= true (=> (< $in1$0 $in2$0) 
          (and (< $in1$0 $out$0) (< $out$0 $in2$0))))))))

有什么方法可以让 z3 传播等式，或者选择另一种使用该等式的搜索策略？

4

0 回答 0