Datalog 입력 형식을 사용하여 Z3의 BitVec에서 1을 센다

데이터 로그 입력 형식을 사용하여 Z3의 BitVec에서 1로 설정된 비트 수를 계산하는 간단한 방법이 있습니까?

$ z3 -h  # most of the lines below omited for clarity
Input format:
  -dl         use parser for Datalog input format.

이 질문에 대해 현재 허용되는 답변 : SMT 2 입력 형식을 사용하여 Z3의 BitVec에서 1을 계산 하면 SMT 2 입력 형식으로 수행 할 수있는 좋은 방법이 없음을 나타냅니다.

이 질문에 대해 현재 허용되는 답변 : Z3의 비트 벡터에있는 모든 비트의 합 은 Python에서이를 수행하는 방법을 보여줍니다.