我们可以在Z3定点查询中使用ite表达式吗答案

【问题标题】：Can we use ite expression in Z3 fixed-point query我们可以在Z3定点查询中使用ite表达式吗
【发布时间】：2016-03-20 22:46:28
【问题描述】：

我在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 表达式有什么解决方法吗？我需要在我的动态符号执行引擎中一起使用它们。非常感谢您！

【问题讨论】：

标签： z3 z3-fixedpoint

【解决方案1】：

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

您可以使用 horn 子句和分层否定：方法是提供一个名称对于子公式，然后是定义子公式的规则。例如，如果要定义(ite (P x) (Q y) (R z))，则引入谓词(ITEPQR x y)，规则如下：

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

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

【讨论】：