Can we use ite expression in Z3 fixed-point query

Question

I modified the edge and path example in the z3 fixed-point tutorial

(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)

This runs fine without any problem.

But if I change this to a functionally equivalent script with an ite expression, I get back errors.

This is updated script using 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) 

I get back the following errors:

(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

I have tried to create a new relation iteRel to simulate the effect of ite expression without any success.

(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)

The would make q3 unsat.

Is there any workaround to use ite expression in z3 fixed-points? I need to use them together in my dynamic symbolic execution engine. Thank you very much in advance!

Answer 1

First of all, for applications where you depend on stratified negation it is better to stick with finite domains because stratified negation is not defined for integer domains etc.

You can define arbitrary formulas using horn clauses and stratified negation: The way to do it is to provide a name for sub-formulas and then rules that define the sub-formula. For example, if you want to define (ite (P x) (Q y) (R z)), then introduce the predicate (ITEPQR x y) with the following rules:

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

The only way you should be able to use ite expressions is if they don't contain any of the defined predicates. That is, they ite expressions are over bound variables and interpreted functions (over bit-vectors).