是否可以将一位的位向量转换为SMTLib2中的布尔变量?

qsp

我想要一个布尔变量来测试例如位向量的第三位是否为0。位向量理论允许提取1位作为位向量,但不能提取布尔类型。我想知道我是否可以做这个演员。谢谢。

===更新===

如果我的问题不清楚,对不起。但是尼古拉·比约纳(Nikolaj Bjorner)的答案是如何测试位向量的某个位。虽然我想将位向量的第一位的值分配给变量。我尝试将示例修改如下:

(declare-fun x () (_ BitVec 5))
(declare-fun bit0 () Bool)
(assert (= (= #b1 ((_ extract 0 0) x)) bit0 ))
(check-sat)

z3抱怨:

(error "line 2 column 25: invalid declaration, builtin symbol bit0")
(error "line 3 column 44: invalid function application, sort mismatch on argument at position 2")

我需要该变量bit0供以后使用。你能给我一个提示吗?谢谢。

尼古拉·比约纳(Nikolaj Bjorner)

在第三位的提取与值为1(和一位)的位向量之间创建相等。

例如,

(declare-const x (_ BitVec 5))
(assert (= #b1 ((_ extract 2 2) x)))
(check-sat)
(get-model)

产生

sat
(model
  (define-fun x () (_ BitVec 5)
    #b00100)
)

本文收集自互联网,转载请注明来源。

如有侵权,请联系[email protected] 删除。

编辑于
0

我来说两句

0条评论
登录后参与评论

相关文章

来自分类Dev

是否可以将0作为整数变量的第一位存储

来自分类Dev

如何将一位数的整数数组转换为 2 位或更多位

来自分类Dev

更新位向量的一位

来自分类Dev

将float转换为至少有一位小数的字符串(javascript)

来自分类Dev

Python:将一位数字十进制转换为十六进制

来自分类Dev

z3Py:将BoolRef转换为一位BitVecRef

来自分类Dev

(Java)将符号的字符串转换为一位整数数组

来自分类Dev

将一位数字代码转换为完整的单词代码python

来自分类Dev

是否可以在C中创建长度为一位的数据类型

来自分类Dev

R中的XML转换,最后一位

来自分类Dev

是否可以将总位数相同的一种类型的位域转换为另一种类型的位域?

来自分类Dev

如何检查整数中是否只设置了一位?

来自分类Dev

将4位整数转换为布尔值列表

来自分类Dev

在Powershell中是否可以将字节数组转换为8位有符号整数数组?

来自分类Dev

将数据转换为2位小数

来自分类Dev

将金额转换为2位小数

来自分类Dev

python将一位数字的日期和月份转换为两位数

来自分类Dev

将Java布尔表达式转换为SMTlib

来自分类Dev

位操作;将16位值转换为16个布尔值的数组?C语言

来自分类Dev

将数字增加一位

来自分类Dev

将int位转换为float位

来自分类Dev

SMTLIB2 / Z3中的多态函数

来自分类Dev

从4位小数转换为2位

来自分类Dev

仅更改文件中的一位

来自分类Dev

在SQL Server中将时间结果转换为一位数值

来自分类Dev

从R中数值向量的每个元素中提取第一位数字

来自分类Dev

列出向量中的所有一位数字差异

来自分类Dev

在向量中的同一位置插入多个元素

来自分类Dev

设置一位与将逻辑一位写入之间有什么区别?

Related 相关文章

热门标签

归档