Commit 6947efa6 authored by Mathias Preiner's avatar Mathias Preiner

Squashed commit of the following:

commit 0590fcea
Author: Mathias Preiner <mathias.preiner@gmail.com>
Date:   Fri Apr 24 22:44:48 2020 -0700

    Move benchmarks from pending repository.
parent dea2db35
; (handcrafted file)
; proving equivalence of several 64-bit population count functions
; https://yurichev.com/news/20200416_popcount/
(set-info :smt-lib-version 2.6)
(set-logic QF_ABV)
(set-info :source |
Generated by: Dennis Yurichev
Generated on: 16-Apr-2020
Application: Proving equivalence of several 64-bit population count functions
Target solver: Boolector, Z3, CVC4
|)
(set-info :license "https://creativecommons.org/licenses/by/4.0/")
(set-info :category "crafted")
(set-info :status unsat)
(declare-fun c0 () (_ BitVec 64)) (assert (= c0 (_ bv0 64))) ; always 0
(declare-fun c1 () (_ BitVec 64)) (assert (= c1 (_ bv1 64))) ; always 1
(declare-fun naive_x () (_ BitVec 64))
(declare-fun naive_out () (_ BitVec 64))
; popcount64(): naive way:
; (x>>0)&1 + (x>>1)&1 + (x>>2)&1 + ...
(assert (= naive_out
(bvadd
(bvand (bvlshr naive_x (_ bv0 64)) (_ bv1 64))
(bvand (bvlshr naive_x (_ bv1 64)) (_ bv1 64))
(bvand (bvlshr naive_x (_ bv2 64)) (_ bv1 64))
(bvand (bvlshr naive_x (_ bv3 64)) (_ bv1 64))
(bvand (bvlshr naive_x (_ bv4 64)) (_ bv1 64))
(bvand (bvlshr naive_x (_ bv5 64)) (_ bv1 64))
(bvand (bvlshr naive_x (_ bv6 64)) (_ bv1 64))
(bvand (bvlshr naive_x (_ bv7 64)) (_ bv1 64))
(bvand (bvlshr naive_x (_ bv8 64)) (_ bv1 64))
(bvand (bvlshr naive_x (_ bv9 64)) (_ bv1 64))
(bvand (bvlshr naive_x (_ bv10 64)) (_ bv1 64))
(bvand (bvlshr naive_x (_ bv11 64)) (_ bv1 64))
(bvand (bvlshr naive_x (_ bv12 64)) (_ bv1 64))
(bvand (bvlshr naive_x (_ bv13 64)) (_ bv1 64))
(bvand (bvlshr naive_x (_ bv14 64)) (_ bv1 64))
(bvand (bvlshr naive_x (_ bv15 64)) (_ bv1 64))
(bvand (bvlshr naive_x (_ bv16 64)) (_ bv1 64))
(bvand (bvlshr naive_x (_ bv17 64)) (_ bv1 64))
(bvand (bvlshr naive_x (_ bv18 64)) (_ bv1 64))
(bvand (bvlshr naive_x (_ bv19 64)) (_ bv1 64))
(bvand (bvlshr naive_x (_ bv20 64)) (_ bv1 64))
(bvand (bvlshr naive_x (_ bv21 64)) (_ bv1 64))
(bvand (bvlshr naive_x (_ bv22 64)) (_ bv1 64))
(bvand (bvlshr naive_x (_ bv23 64)) (_ bv1 64))
(bvand (bvlshr naive_x (_ bv24 64)) (_ bv1 64))
(bvand (bvlshr naive_x (_ bv25 64)) (_ bv1 64))
(bvand (bvlshr naive_x (_ bv26 64)) (_ bv1 64))
(bvand (bvlshr naive_x (_ bv27 64)) (_ bv1 64))
(bvand (bvlshr naive_x (_ bv28 64)) (_ bv1 64))
(bvand (bvlshr naive_x (_ bv29 64)) (_ bv1 64))
(bvand (bvlshr naive_x (_ bv30 64)) (_ bv1 64))
(bvand (bvlshr naive_x (_ bv31 64)) (_ bv1 64))
(bvand (bvlshr naive_x (_ bv32 64)) (_ bv1 64))
(bvand (bvlshr naive_x (_ bv33 64)) (_ bv1 64))
(bvand (bvlshr naive_x (_ bv34 64)) (_ bv1 64))
(bvand (bvlshr naive_x (_ bv35 64)) (_ bv1 64))
(bvand (bvlshr naive_x (_ bv36 64)) (_ bv1 64))
(bvand (bvlshr naive_x (_ bv37 64)) (_ bv1 64))
(bvand (bvlshr naive_x (_ bv38 64)) (_ bv1 64))
(bvand (bvlshr naive_x (_ bv39 64)) (_ bv1 64))
(bvand (bvlshr naive_x (_ bv40 64)) (_ bv1 64))
(bvand (bvlshr naive_x (_ bv41 64)) (_ bv1 64))
(bvand (bvlshr naive_x (_ bv42 64)) (_ bv1 64))
(bvand (bvlshr naive_x (_ bv43 64)) (_ bv1 64))
(bvand (bvlshr naive_x (_ bv44 64)) (_ bv1 64))
(bvand (bvlshr naive_x (_ bv45 64)) (_ bv1 64))
(bvand (bvlshr naive_x (_ bv46 64)) (_ bv1 64))
(bvand (bvlshr naive_x (_ bv47 64)) (_ bv1 64))
(bvand (bvlshr naive_x (_ bv48 64)) (_ bv1 64))
(bvand (bvlshr naive_x (_ bv49 64)) (_ bv1 64))
(bvand (bvlshr naive_x (_ bv50 64)) (_ bv1 64))
(bvand (bvlshr naive_x (_ bv51 64)) (_ bv1 64))
(bvand (bvlshr naive_x (_ bv52 64)) (_ bv1 64))
(bvand (bvlshr naive_x (_ bv53 64)) (_ bv1 64))
(bvand (bvlshr naive_x (_ bv54 64)) (_ bv1 64))
(bvand (bvlshr naive_x (_ bv55 64)) (_ bv1 64))
(bvand (bvlshr naive_x (_ bv56 64)) (_ bv1 64))
(bvand (bvlshr naive_x (_ bv57 64)) (_ bv1 64))
(bvand (bvlshr naive_x (_ bv58 64)) (_ bv1 64))
(bvand (bvlshr naive_x (_ bv59 64)) (_ bv1 64))
(bvand (bvlshr naive_x (_ bv60 64)) (_ bv1 64))
(bvand (bvlshr naive_x (_ bv61 64)) (_ bv1 64))
(bvand (bvlshr naive_x (_ bv62 64)) (_ bv1 64))
(bvand (bvlshr naive_x (_ bv63 64)) (_ bv1 64))
)))
;int popcount64_table(uint64_t x)
;{
; uint64_t tbl[16]={0,1,1,2,1,2,2,3,1,2,2,3,2,3,3,4};
; uint64_t rt=0;
; rt=rt+tbl[(x>>(0*4))&0xf];
; rt=rt+tbl[(x>>(1*4))&0xf];
;...
; fill table of constants:
(declare-const tbl (Array (_ BitVec 64) (_ BitVec 64)))
(assert (= tbl (store tbl (_ bv0 64) (_ bv0 64))))
(assert (= tbl (store tbl (_ bv1 64) (_ bv1 64))))
(assert (= tbl (store tbl (_ bv2 64) (_ bv1 64))))
(assert (= tbl (store tbl (_ bv3 64) (_ bv2 64))))
(assert (= tbl (store tbl (_ bv4 64) (_ bv1 64))))
(assert (= tbl (store tbl (_ bv5 64) (_ bv2 64))))
(assert (= tbl (store tbl (_ bv6 64) (_ bv2 64))))
(assert (= tbl (store tbl (_ bv7 64) (_ bv3 64))))
(assert (= tbl (store tbl (_ bv8 64) (_ bv1 64))))
(assert (= tbl (store tbl (_ bv9 64) (_ bv2 64))))
(assert (= tbl (store tbl (_ bv10 64) (_ bv2 64))))
(assert (= tbl (store tbl (_ bv11 64) (_ bv3 64))))
(assert (= tbl (store tbl (_ bv12 64) (_ bv2 64))))
(assert (= tbl (store tbl (_ bv13 64) (_ bv3 64))))
(assert (= tbl (store tbl (_ bv14 64) (_ bv3 64))))
(assert (= tbl (store tbl (_ bv15 64) (_ bv4 64))))
(declare-fun tbl_x () (_ BitVec 64))
(declare-fun tbl_out () (_ BitVec 64))
; rt=rt+tbl[(x>>(0*4))&0xf];
; rt=rt+tbl[(x>>(1*4))&0xf];
; ...
(assert (= tbl_out
(bvadd
(select tbl (bvand (bvlshr tbl_x (_ bv0 64)) (_ bv15 64)))
(select tbl (bvand (bvlshr tbl_x (_ bv4 64)) (_ bv15 64)))
(select tbl (bvand (bvlshr tbl_x (_ bv8 64)) (_ bv15 64)))
(select tbl (bvand (bvlshr tbl_x (_ bv12 64)) (_ bv15 64)))
(select tbl (bvand (bvlshr tbl_x (_ bv16 64)) (_ bv15 64)))
(select tbl (bvand (bvlshr tbl_x (_ bv20 64)) (_ bv15 64)))
(select tbl (bvand (bvlshr tbl_x (_ bv24 64)) (_ bv15 64)))
(select tbl (bvand (bvlshr tbl_x (_ bv28 64)) (_ bv15 64)))
(select tbl (bvand (bvlshr tbl_x (_ bv32 64)) (_ bv15 64)))
(select tbl (bvand (bvlshr tbl_x (_ bv36 64)) (_ bv15 64)))
(select tbl (bvand (bvlshr tbl_x (_ bv40 64)) (_ bv15 64)))
(select tbl (bvand (bvlshr tbl_x (_ bv44 64)) (_ bv15 64)))
(select tbl (bvand (bvlshr tbl_x (_ bv48 64)) (_ bv15 64)))
(select tbl (bvand (bvlshr tbl_x (_ bv52 64)) (_ bv15 64)))
(select tbl (bvand (bvlshr tbl_x (_ bv56 64)) (_ bv15 64)))
(select tbl (bvand (bvlshr tbl_x (_ bv60 64)) (_ bv15 64)))
)))
(assert (= naive_x tbl_x)) (assert (not (= naive_out tbl_out)))
(check-sat)
(exit)
Markdown is supported
0%
or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment