1

我在z3定点教程中修改了边缘和路径示例

(set-option :fixedpoint.engine datalog)
(define-sort s () (_ BitVec 3))
(declare-rel edge (s s))
(declare-rel path (s s))
(declare-var a s)
(declare-var b s)
(declare-var c s)

(rule (=> (edge a b) (path a b)))
(rule (=> (and (path a b) (path b c)) (path a c)))

(rule (edge #b001 #b010))
(rule (edge #b001 #b011))
(rule (edge #b010 #b100))

(declare-rel q1 ())
(declare-rel q2 ())
(declare-rel q3 (s))
(rule (=> (path #b001 #b100) q1))
(rule (=> (path #b011 #b100) q2))
(rule (=> (and (path #b001 b) (path #b010 b)) (q3 b))); I modified this rule by adding a conjunct in the antecedent

(query q1)
(query q2)
(query q3 :print-answer true)

这运行良好，没有任何问题。

但是，如果我将其更改为具有 ite 表达式的功能等效脚本，则会返回错误。

这是使用 ite 更新的脚本：

(set-option :fixedpoint.engine datalog)
(define-sort s () (_ BitVec 3))
(declare-rel edge (s s))
(declare-rel path (s s))
(declare-var a s)
(declare-var b s)
(declare-var c s)

(rule (=> (edge a b) (path a b)))
(rule (=> (and (path a b) (path b c)) (path a c)))

(rule (edge #b001 #b010))
(rule (edge #b001 #b011))
(rule (edge #b010 #b100))

(declare-rel q1 ())
(declare-rel q2 ())
(declare-rel q3 (s))
(rule (=> (path #b001 #b100) q1))
(rule (=> (path #b011 #b100) q2))
(rule (=> (and (path #b001 b) (not (= (ite (path #b010 b) 1 0) 0))) (q3 b))) ; I added ite expression here

(query q1)
(query q2)
(query q3 :print-answer true)

我得到以下错误：

(error "query failed: Rule contains nested predicates q3(#0) :- path(#b001,#0), (not (= (ite (path #b010 (:var 0)) 1 0) 0)). ") 
unknown 
(error "query failed: Rule contains nested predicates q3(#0) :- path(#b001,#0), (not (= (ite (path #b010 (:var 0)) 1 0) 0)). ") 
unknown 
(error "query failed: Rule contains nested predicates q3(#0) :- path(#b001,#0), (not (= (ite (path #b010 (:var 0)) 1 0) 0)). ") 
unknown

我试图创建一个新的关系iteRel来模拟ite表达式的效果，但没有任何成功。

(set-option :fixedpoint.engine datalog)
(define-sort s () (_ BitVec 3))
(declare-rel edge (s s))
(declare-rel path (s s))
(declare-var a s)
(declare-var b s)
(declare-var c s)

(rule (=> (edge a b) (path a b)))
(rule (=> (and (path a b) (path b c)) (path a c)))

(rule (edge #b001 #b010))
(rule (edge #b001 #b011))
(rule (edge #b010 #b100))

(declare-rel q1 ())
(declare-rel q2 ())
(declare-rel q3 (s))

(declare-rel iteRel (s s Int Int Int))

(rule (forall ((x s) (y s) (z1 Int) (z2 Int))
  (=> (and (iteRel x y z1 z2 z1))
     (path x y)) 
))

(rule (=> (path #b001 #b100) q1))
(rule (=> (path #b011 #b100) q2))
(rule (=> (and (path #b001 b) (iteRel #b010 b 1 0 1)) (q3 b)))

(query q1)
(query q2)
(query q3 :print-answer true)

这将使第三季度不满意。

是否有任何解决方法可以在 z3 定点中使用 ite 表达式？我需要在我的动态符号执行引擎中一起使用它们。非常感谢您！

4

1 回答 1

1

首先，对于依赖分层否定的应用程序，最好坚持使用有限域，因为没有为整数域等定义分层否定。

您可以使用角子句和分层否定来定义任意公式：这样做的方法是为子公式提供名称，然后提供定义子公式的规则。例如，如果要定义(ite (P x) (Q y) (R z))，则引入谓词(ITEPQR xy)，规则如下：

   (rule (=> (and (P x) (Q y)) (ITEPQR x y)))
   (rule (=> (and (not (P x)) (R y)) (ITEPQR x y)))

您应该能够使用 ite 表达式的唯一方法是它们不包含任何已定义的谓词。也就是说，它们的表达式是过度绑定变量和解释函数（通过位向量）。

于 2016-03-20T23:41:39.250 回答