[Question]: Meaning of function ending with "0" in uninterpreted function.

[hagozaebii]

Hi, recently, I solved this formula using z3.

(set-info :smt-lib-version 2.6)
(set-logic QF_UFNIA)
(set-info :source |
Generated by: Yoni Zohar
Generated on: 2019-03-18
Application: verifying invertibility conditions
Target solver: CVC4, z3
Publications: "Towards Bit-Width-Independent Proofs in SMT Solvers " by A. Niemetz, M. Preiner, A. Reynolds, Y. Zohar, C. Barrett, and C. Tinelli, CADE-27 (2019).
|)
(set-info :license "https://creativecommons.org/licenses/by/4.0/")
(set-info :category "crafted")
;;(set-info :status sat)

(declare-fun pow2 (Int) Int)
(declare-fun intand (Int Int Int) Int)
(declare-fun intor (Int Int Int) Int)
(declare-fun intxor (Int Int Int) Int)
(define-fun bitof ((k Int) (l Int) (a Int)) Int (mod (div a (pow2 l)) 2))
(define-fun int_all_but_msb ((k Int) (a Int)) Int (mod a (pow2 (- k 1))))
(define-fun intmax ((k Int)) Int (- (pow2 k) 1))
(define-fun intmin ((k Int)) Int 0)
(define-fun in_range ((k Int) (x Int)) Bool (and (>= x 0) (<= x (intmax k))))
(define-fun intudivtotal ((k Int) (a Int) (b Int)) Int (ite (= b 0) (- (pow2 k) 1) (div a b) ))
(define-fun intmodtotal ((k Int) (a Int) (b Int)) Int (ite (= b 0) a (mod a b)))
(define-fun intneg ((k Int) (a Int)) Int (intmodtotal k (- (pow2 k) a) (pow2 k)))
(define-fun intnot ((k Int) (a Int)) Int (- (intmax k) a))
(define-fun intmins ((k Int)) Int (pow2 (- k 1)))
(define-fun intmaxs ((k Int)) Int (intnot k (intmins k)))
(define-fun intshl ((k Int) (a Int) (b Int)) Int (intmodtotal k (* a (pow2 b)) (pow2 k)))
(define-fun intlshr ((k Int) (a Int) (b Int)) Int (intmodtotal k (intudivtotal k a (pow2 b)) (pow2 k)))
(define-fun intashr ((k Int) (a Int) (b Int) ) Int (ite (= (bitof k (- k 1) a) 0) (intlshr k a b) (intnot k (intlshr k (intnot k a) b))))
(define-fun intconcat ((k Int) (m Int) (a Int) (b Int)) Int (+ (* a (pow2 m)) b))
(define-fun intadd ((k Int) (a Int) (b Int) ) Int (intmodtotal k (+ a b) (pow2 k)))
(define-fun intmul ((k Int) (a Int) (b Int)) Int (intmodtotal k (* a b) (pow2 k)))
(define-fun intsub ((k Int) (a Int) (b Int)) Int (intadd k a (intneg k b)))
(define-fun unsigned_to_signed ((k Int) (x Int)) Int (- (* 2 (int_all_but_msb k x)) x))
(define-fun intslt ((k Int) (a Int) (b Int)) Bool (< (unsigned_to_signed k a) (unsigned_to_signed k b)) )
(define-fun intsgt ((k Int) (a Int) (b Int)) Bool (> (unsigned_to_signed k a) (unsigned_to_signed k b)) )
(define-fun intsle ((k Int) (a Int) (b Int)) Bool (<= (unsigned_to_signed k a) (unsigned_to_signed k b)) )
(define-fun intsge ((k Int) (a Int) (b Int)) Bool (>= (unsigned_to_signed k a) (unsigned_to_signed k b)) )
(define-fun pow2_base_cases () Bool (and (= (pow2 0) 1) (= (pow2 1) 2) (= (pow2 2) 4) (= (pow2 3) 8) ) )
;qf axioms
(define-fun pow2_ax () Bool pow2_base_cases)
(define-fun and_ax ((k Int)) Bool true)
(define-fun or_ax ((k Int)) Bool true)
(define-fun xor_ax ((k Int)) Bool true)
(define-fun l ((k Int) (x Int) (s Int) (t Int)) Bool  (intsgt k (intudivtotal k s x) t))
(define-fun SC ((k Int) (s Int) (t Int)) Bool (and (=> (intsge k s 0) (intsgt k s t)) (=> (intslt k s 0) (intsgt k (intlshr k s 1) t))))

(declare-fun k () Int)
(declare-fun s () Int)
(declare-fun t () Int)

;<BEGIN_RTL>
;skolemized x for the right-to-left direction
(declare-fun x0 () Int)
(assert (in_range k x0))

(define-fun not_right_to_left ((k Int) (s Int) (t Int)) Bool (and (l k x0 s t) (not (SC k s t))))

(define-fun assertion_rtl () Bool (not_right_to_left k s t))
;<END_RTL>

;general assertions
(assert (>= k 1))
(assert (in_range k s))
(assert (in_range k t))
(assert pow2_ax)

(assert assertion_rtl)

(check-sat)
(get-model)

and I got a result as follows:

sat
(
  (define-fun k () Int
    18)
  (define-fun assertion_rtl () Bool
    (let ((a!1 (ite (= x0 0) (- (pow2 k) 1) (div s x0)))
      (a!3 (* 2 (mod t (pow2 (- k 1)))))
      (a!4 (* 2 (mod s (pow2 (- k 1)))))
      (a!5 (* 2 (mod 0 (pow2 (- k 1)))))
      (a!6 (ite (= (pow2 1) 0) (- (pow2 k) 1) (div s (pow2 1)))))
(let ((a!2 (* 2 (mod a!1 (pow2 (- k 1)))))
      (a!7 (ite (= (pow2 k) 0) a!6 (mod a!6 (pow2 k)))))
(let ((a!8 (* 2 (mod a!7 (pow2 (- k 1))))))
(let ((a!9 (and (=> (>= (- a!4 s) (- a!5 0)) (> (- a!4 s) (- a!3 t)))
                (=> (< (- a!4 s) (- a!5 0)) (> (- a!8 a!7) (- a!3 t))))))
  (and (> (- a!2 a!1) (- a!3 t)) (not a!9)))))))
  (define-fun pow2_base_cases () Bool
    (and (= (pow2 0) 1) (= (pow2 1) 2) (= (pow2 2) 4) (= (pow2 3) 8)))
  (define-fun x0 () Int
    4)
  (define-fun s () Int
    18)
  (define-fun t () Int
    2)
  (define-fun pow2_ax () Bool
    (and (= (pow2 0) 1) (= (pow2 1) 2) (= (pow2 2) 4) (= (pow2 3) 8)))
  (define-fun pow2 ((x!0 Int)) Int
    (ite (= x!0 0) 1
    (ite (= x!0 1) 2
    (ite (= x!0 2) 4
    (ite (= x!0 3) 8
    (ite (= x!0 17) 0
      19))))))
  (define-fun div0 ((x!0 Int) (x!1 Int)) Int
    (ite (and (= x!0 18) (= x!1 4)) 4
      0))
  (define-fun mod0 ((x!0 Int) (x!1 Int)) Int
    (ite (and (= x!0 18) (= x!1 4)) 2
    (ite (and (= x!0 4) (= x!1 0)) 13
    (ite (and (= x!0 0) (= x!1 0)) 0
    (ite (and (= x!0 18) (= x!1 0)) 17
    (ite (and (= x!0 9) (= x!1 19)) 9
    (ite (and (= x!0 9) (= x!1 0)) 10
      11)))))))
  (define-fun intand ((x!0 Int) (x!1 Int) (x!2 Int)) Int
    0)
  (define-fun intor ((x!0 Int) (x!1 Int) (x!2 Int)) Int
    0)
  (define-fun intxor ((x!0 Int) (x!1 Int) (x!2 Int)) Int
    0)
)

I found that there were div0 and mod0 even though there were no functions like that. I guess those were from div and mod used in other uninterpreted functions (e.g. bitof). If it is true, I am curious about why the model has to have values about div and mod. I think div and mod mean functions defined in smtlibv2. Why does z3 interpret those functions like uninterpreted functions?

Thanks for your time!

[NikolajBjorner]

div0 and mod0 are the functions that give meaning to div and mod when the second argument is 0. div/mod are uninterpreted when the second argument is 0. To represent the meaning at 0 z3 introduces uninterpreted functions that can be used in models. The interpreted functions are not used in models. You will have the axiom (div0 x 0) = (div x 0) enforced.