출력을 16 진수 형식으로 출력하는 방법

Question

이 Boolector 프로그램 인쇄 출력을 2 진 형식으로 출력합니다. 하지만 16 진수 형식이 필요합니다. boolector에서 16 진수 형식을 인쇄하는 방법.

(set-logic QF_BV) 
(set-info :smt-lib-version 2.0) 

(declare-const val1 (_ BitVec 16)) 
(declare-const val2 (_ BitVec 16)) 

(declare-const gen_mul (_ BitVec 16)) 
(declare-const eval1 (_ BitVec 32)) 
(declare-const eval2 (_ BitVec 32)) 
(declare-const org_mul (_ BitVec 32)) 
(declare-const rem17 (_ BitVec 32)) 
(declare-const res (_ BitVec 16)) 

(assert (= gen_mul (bvmul val1 val2))) 
(assert (= eval1 (concat #x0000 val1))) 
(assert (= eval2 (concat #x0000 val2))) 
(assert (= org_mul (bvmul eval1 eval2))) 
(assert (= rem17 (bvurem org_mul #x00010001))) 
(assert (= res ((_ extract 15 0) rem17))) 
(assert (= val1 #xb621)) 
(assert (= val2 #xd620)) 
(check-sat) 

(get-value (val1)) 
(get-value (val2)) 
(get-value (org_mul)) 
(get-value (gen_mul)) 
(get-value (eval1)) 
(get-value (eval2)) 
(get-value (org_mul)) 
(get-value (rem17)) 
(get-value (res)) 
(exit) 

실행 : ./boolector의 ex.smt2

Answer 1

Boolector (적어도 버전 2.2.0) 진수 출력을 강제로 -x, --hex 옵션을 갖는다. 비트 벡터의 크기가 4의 배수가 아니면 이러한 옵션을 무시할 수 있습니다.