; COMMAND-LINE: --sygus-inst --no-check-models
(set-info :smt-lib-version 2.6)
(set-logic UFNIA)
(set-info :source |
Generated by: Mathias Preiner
Generated on: 2019-03-22
Application: Verifying bit-vector rewrite rule candidates independent from bit-width.
Target solver: CVC4, Z3, Vampire
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 p2 (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 (p2 l)) 2))
(define-fun int_all_but_msb ((k Int) (a Int)) Int (mod a (p2 (- k 1))))
(define-fun intmax ((k Int)) Int (- (p2 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) (- (p2 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 (- (p2 k) a) (p2 k)))
(define-fun intnot ((k Int) (a Int)) Int (- (intmax k) a))
(define-fun intmins ((k Int)) Int (p2 (- 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 (p2 b)) (p2 k)))
(define-fun intlshr ((k Int) (a Int) (b Int)) Int (intmodtotal k (intudivtotal k a (p2 b)) (p2 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 (p2 m)) b))
(define-fun intadd ((k Int) (a Int) (b Int) ) Int (intmodtotal k (+ a b) (p2 k)))
(define-fun intmul ((k Int) (a Int) (b Int)) Int (intmodtotal k (* a b) (p2 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 p2_base_cases () Bool (and (= (p2 0) 1) (= (p2 1) 2) (= (p2 2) 4) (= (p2 3) 8) ) )
;qf axioms
(define-fun p2_ax () Bool p2_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)

; helpers
(define-fun is_bv_width ((k Int)) Bool
 (and
  (> k 0)
  (and_ax k)
  (or_ax k)
  (xor_ax k)
 )
)

(define-fun is_bv_var ((k Int) (x Int)) Bool (in_range k x))


; problem start
(assert p2_ax)
(assert (not (forall ((s Int) (t Int) (k Int))
  (=>
   (and (is_bv_var k s) (is_bv_var k t) (is_bv_width k))
   (= (intshl k (intor k t (intnot k t)) t) (intshl k (intnot k (intlshr k s s)) t))
  )
 )
))
(set-info :status unknown)
(check-sat)
(exit)