CVC语言参考

声明

比特向量表达式（或术语）是由比特向量常量、比特向量变量以及下列函数构成的。在 STP 中，所有变量必须在使用之前声明。一个长度为 32 的比特向量变量的声明示例如下：

x : BITVECTOR(32); 

一个数组声明的示例如下：

x_arr : ARRAY BITVECTOR(32) OF BITVECTOR(5000); 

解释

在 STP（Satisfiability Modulo Theories）语言中，声明变量时需要明确其类型和长度。比特向量是一种常见的数据类型，用于表示固定长度的位（bits）序列。

• 比特向量变量声明:

  x : BITVECTOR(32); 

  这行代码声明了一个名为 x 的比特向量变量，长度为 32 位。BITVECTOR(32) 指定了该变量是一个 32 位的比特向量。

• 比特向量数组声明:

  x_arr : ARRAY BITVECTOR(32) OF BITVECTOR(5000); 

  这行代码声明了一个名为 x_arr 的数组变量。这个数组的每个元素是一个 32 位的比特向量，总共有 5000 个这样的元素。即，这是一个包含 5000 个 32 位比特向量的数组。

这些声明用于定义在 STP 中使用的变量，确保在使用之前每个变量的类型和大小都是明确的。

函数和术语

长度为 0 的比特向量变量（或术语）是不允许的。比特向量常量可以用二进制或十六进制格式表示。最右边的位称为最低有效位（LSB），最左边的位是最高有效位（MSB）。对于 n 位常量，LSB 的索引是 0，MSB 的索引是 n-1。这种约定自然延伸到所有比特向量表达式。以下是一些用二进制和十六进制表示的比特向量常量的示例：

0bin00001111101010000 0hex0F50 

STP 中的比特向量实现支持大量的函数和谓词。函数分为字级函数、位操作函数和算术函数。

解释
在 STP 中，比特向量有着明确的表示和操作规则：

• 比特向量常量表示:

  • 二进制格式: 以 0bin 开头，后面跟随一串二进制数字。例如，0bin00001111101010000 表示一个比特向量常量。
  • 十六进制格式: 以 0hex 开头，后面跟随一串十六进制数字。例如，0hex0F50 表示一个比特向量常量。

• 位的意义和索引:

  • 最低有效位（LSB）: 位于最右边，索引为 0。
  • 最高有效位（MSB）: 位于最左边，索引为 n-1，其中 n 是比特向量的长度。

这种表示方法使得比特向量的操作更加规范化和易于理解。STP 提供了丰富的函数和谓词来操作比特向量，涵盖了字级、位操作和算术等各类操作需求。这些函数使得用户可以方便地进行复杂的比特向量操作，从而实现更高效的计算和分析。

字级函数

名称	符号	示例
连接	@	t1@t2@…@tm
提取	[i:j]	x[31:26]
左移	<<	0bin0011 << 3 = 0bin0011000
右移	>>	x[24:17] >> 5，另一个例子: 0bin1000 >> 3 = 0bin0001
符号扩展	BVSX(bv,n)	BVSX(0bin100, 5) = 0bin11100
数组读取	[index]	x_arr[t1]
数组写入	WITH	x_arr WITH [index] := value

注释:

• 对于提取术语，记为 t[i:j]，n > i >= j >= 0，其中 n 是 t 的长度。
• 对于左移术语，t << k 等于在 t 后面追加 k 个 0。t << k 的长度是 n + k。
• 对于右移术语，记为 t >> k，该术语等于通过在 t 前面追加 k 个 0，并紧接 t[n-1:k] 得到的比特向量。t >> k 的长度是 n。

解释

在 STP 语言中，字级函数用于操作比特向量，通过不同的操作符可以实现连接、提取、移位等功能：

1. 连接 (@):

   • 将多个比特向量连接成一个更长的比特向量。
   • 示例：t1@t2@...@tm 将 t1、t2 直到 tm 连接成一个新的比特向量。

2. 提取 ([i:j]):

   • 从一个比特向量中提取指定范围的子向量。
   • 示例：x[31:26] 从 x 中提取第 31 到 26 位组成的新比特向量。

3. 左移 (<<):

   • 将比特向量向左移位，右边补 0。
   • 示例：0bin0011 << 3 = 0bin0011000 表示将 0bin0011 左移 3 位，得到 0bin0011000。

4. 右移 (>>):

   • 将比特向量向右移位，左边补 0。
   • 示例：x[24:17] >> 5 和 0bin1000 >> 3 = 0bin0001。

5. 符号扩展 (BVSX(bv,n)):

   • 将比特向量进行符号扩展到指定长度。
   • 示例：BVSX(0bin100, 5) = 0bin11100 表示将 0bin100 扩展为 5 位比特向量，符号位扩展。

6. 数组读取 ([index]):

   • 从数组中读取指定索引的元素。
   • 示例：x_arr[t1] 表示从数组 x_arr 中读取索引为 t1 的元素。

7. 数组写入 (WITH):

   • 向数组中指定索引位置写入新的值。
   • 示例：x_arr WITH [index] := value 表示向 x_arr 的 index 索引位置写入新的 value。

这些函数使得比特向量的操作更加灵活和强大，可以实现复杂的数据处理和计算需求。

按位函数

名称	符号	示例
按位与 (AND)	&	t1 & t2 & … & tm
按位或 (OR)	|	t1 | t2 | … | tm
按位非 (NOT)	~	~t1
按位异或 (XOR)	BVXOR	BVXOR(t1, t2)
按位与非 (NAND)	BVNAND	BVNAND(t1, t2)
按位或非 (NOR)	BVNOR	BVNOR(t1, t2)
按位同或 (XNOR)	BVXNOR	BVXNOR(t1, t2)

注意：所有按位函数的参数必须具有相同的长度。

解释

在 STP 语言中，按位函数用于对比特向量进行位级别的操作。这些操作包括与、或、非、异或、与非、或非和同或等。这些操作对比特向量的每一位进行操作，返回一个新的比特向量。

1. 按位与 (AND) (&):

   • 将多个比特向量按位进行与操作。
   • 示例：t1 & t2 & ... & tm 表示对 t1 到 tm 进行按位与操作。

2. 按位或 (OR) (|):

   • 将多个比特向量按位进行或操作。
   • 示例：t1 \| t2 \| ... \| tm 表示对 t1 到 tm 进行按位或操作。

3. 按位非 (NOT) (~):

   • 将比特向量按位进行取反操作。
   • 示例：~t1 表示对 t1 进行按位非操作，即取反。

4. 按位异或 (XOR) (BVXOR):

   • 将两个比特向量按位进行异或操作。
   • 示例：BVXOR(t1, t2) 表示对 t1 和 t2 进行按位异或操作。

5. 按位与非 (NAND) (BVNAND):

   • 将两个比特向量按位进行与非操作。
   • 示例：BVNAND(t1, t2) 表示对 t1 和 t2 进行按位与非操作。

6. 按位或非 (NOR) (BVNOR):

   • 将两个比特向量按位进行或非操作。
   • 示例：BVNOR(t1, t2) 表示对 t1 和 t2 进行按位或非操作。

7. 按位同或 (XNOR) (BVXNOR):

   • 将两个比特向量按位进行同或操作。
   • 示例：BVXNOR(t1, t2) 表示对 t1 和 t2 进行按位同或操作。

这些按位函数要求所有参与操作的比特向量长度相同，以确保操作的正确性。这些操作是比特向量处理中的基本操作，广泛应用于各种计算和逻辑处理场景。

算术函数

名称	符号	示例
比特向量加法	BVPLUS	BVPLUS(n,t1,t2,…,tm)
比特向量乘法	BVMULT	BVMULT(n,t1,t2)
比特向量减法	BVSUB	BVSUB(n,t1,t2)
比特向量一元减法	BVUMINUS	BVUMINUS(t1)
比特向量除法	BVDIV	BVDIV(n,t1,t2)，其中 t1 是被除数，t2 是除数
有符号比特向量除法	SBDIV	SBDIV(n,t1,t2)，其中 t1 是被除数，t2 是除数
比特向量模运算	BVMOD	BVMOD(n,t1,t2)，其中 t1 是被除数，t2 是除数
有符号比特向量模运算	SBVMOD	SBVMOD(n,t1,t2)，其中 t1 是被除数，t2 是除数

注释：

• 输出位的数量必须指定（单目减法除外）。
• 所有输入必须具有相同的长度。
• BVUMINUS(t) 是 BVPLUS(n,~t,0bin1) 的简写，其中 n 是 t 的长度。
• BVSUB(n,t1,t2) 是 BVPLUS(n,t1,BVUMINUS(t2)) 的简写。

STP 还支持条件术语，例如，IF cond THEN t1 ELSE t2 ENDIF，其中 cond 是布尔术语，t1 和 t2 可以是比特向量术语。这允许我们模拟多路复用器。一个示例是：

x, y : BITVECTOR(1); QUERY(x = (IF 0bin0 = x THEN y ELSE BVUMINUS(y) ENDIF)); 

解释
在 STP 语言中，算术函数用于对比特向量进行各种算术运算。这些函数包括加法、乘法、减法、除法和模运算等。

1. 比特向量加法 (BVPLUS):

   • 对多个比特向量进行加法操作。
   • 示例：BVPLUS(n,t1,t2,...,tm) 表示将 t1 到 tm 的比特向量相加，结果为 n 位。

2. 比特向量乘法 (BVMULT):

   • 对两个比特向量进行乘法操作。
   • 示例：BVMULT(n,t1,t2) 表示将 t1 和 t2 的比特向量相乘，结果为 n 位。

3. 比特向量减法 (BVSUB):

   • 对两个比特向量进行减法操作。
   • 示例：BVSUB(n,t1,t2) 表示 t1 减去 t2，结果为 n 位。

4. 比特向量一元减法 (BVUMINUS):

   • 对一个比特向量进行一元减法操作，即取反加一。
   • 示例：BVUMINUS(t1) 表示对 t1 进行一元减法操作。

5. 比特向量除法 (BVDIV):

   • 对两个比特向量进行除法操作。
   • 示例：BVDIV(n,t1,t2) 表示 t1 除以 t2，结果为 n 位，其中 t1 是被除数，t2 是除数。

6. 有符号比特向量除法 (SBDIV):

   • 对两个有符号比特向量进行除法操作。
   • 示例：SBDIV(n,t1,t2) 表示 t1 除以 t2，结果为 n 位，其中 t1 是被除数，t2 是除数。

7. 比特向量模运算 (BVMOD):

   • 对两个比特向量进行模运算。
   • 示例：BVMOD(n,t1,t2) 表示 t1 模 t2，结果为 n 位，其中 t1 是被除数，t2 是除数。

8. 有符号比特向量模运算 (SBVMOD):

   • 对两个有符号比特向量进行模运算。
   • 示例：SBVMOD(n,t1,t2) 表示 t1 模 t2，结果为 n 位，其中 t1 是被除数，t2 是除数。

这些函数要求所有输入比特向量的长度相同，并且通常需要指定输出的位数。这些算术操作在比特向量处理和计算中非常重要，提供了丰富的操作能力。此外，STP 还支持条件术语，使得逻辑控制和多路复用更加灵活。

谓词

以下是 STP 支持的谓词：

名称	符号	示例
相等 (Equality)	=	t1=t2
小于 (Less Than)	BVLT	BVLT(t1,t2)
大于 (Greater Than)	BVGT	BVGT(t1,t2)
小于或等于 (Less Than Or Equal To)	BVLE	BVLE(t1,t2)
大于或等于 (Greater Than Or Equal To)	BVGE	BVGE(t1,t2)
有符号小于 (Signed Less Than)	SBVLT	SBVLT(t1,t2)
有符号大于 (Signed Greater Than)	SBVGT	SBVGT(t1,t2)
有符号小于或等于 (Signed Less Than Or Equal To)	SBVLE	SBVLE(t1,t2)
有符号大于或等于 (Signed Greater Than Or Equal To)	SBVGE	SBVGE(t1,t2)

注释：

• STP 要求在原子公式中，如 x = y，x 和 y 必须是相同长度的表达式。STP 接受原子公式的布尔组合。

解释
在 STP 语言中，谓词用于比较比特向量。以下是支持的谓词及其作用：

1. 相等性 (Equality) (=):

   • 用于判断两个比特向量是否相等。
   • 示例：t1 = t2 表示 t1 和 t2 相等。

2. 小于 (Less Than) (BVLT):

   • 用于判断一个比特向量是否小于另一个比特向量。
   • 示例：BVLT(t1, t2) 表示 t1 小于 t2。

3. 大于 (Greater Than) (BVGT):

   • 用于判断一个比特向量是否大于另一个比特向量。
   • 示例：BVGT(t1, t2) 表示 t1 大于 t2。

4. 小于或等于 (Less Than Or Equal To) (BVLE):

   • 用于判断一个比特向量是否小于或等于另一个比特向量。
   • 示例：BVLE(t1, t2) 表示 t1 小于或等于 t2。

5. 大于或等于 (Greater Than Or Equal To) (BVGE):

   • 用于判断一个比特向量是否大于或等于另一个比特向量。
   • 示例：BVGE(t1, t2) 表示 t1 大于或等于 t2。

6. 有符号小于 (Signed Less Than) (SBVLT):

   • 用于判断一个有符号比特向量是否小于另一个有符号比特向量。
   • 示例：SBVLT(t1, t2) 表示有符号 t1 小于有符号 t2。

7. 有符号大于 (Signed Greater Than) (SBVGT):

   • 用于判断一个有符号比特向量是否大于另一个有符号比特向量。
   • 示例：SBVGT(t1, t2) 表示有符号 t1 大于有符号 t2。

8. 有符号小于或等于 (Signed Less Than Or Equal To) (SBVLE):

   • 用于判断一个有符号比特向量是否小于或等于另一个有符号比特向量。
   • 示例：SBVLE(t1, t2) 表示有符号 t1 小于或等于有符号 t2。

9. 有符号大于或等于 (Signed Greater Than Or Equal To) (SBVGE):

   • 用于判断一个有符号比特向量是否大于或等于另一个有符号比特向量。
   • 示例：SBVGE(t1, t2) 表示有符号 t1 大于或等于有符号 t2。

这些谓词用于在逻辑表达式中进行比特向量的比较操作，确保操作数具有相同的长度，并允许在布尔公式中进行组合使用。

注释

任何以 % 作为第一个字符的行都是注释。

解释

在 STP 语言中，注释是代码中的一部分，它不会被编译器执行，而是用来给人类阅读的。注释用于解释代码的功能、提供额外信息或备注。在 STP 中，如果一行的第一个字符是 %，那么这整行将被视为注释。这意味着：

• 这行文字不会被当作代码执行。
• 这行文字是为了帮助开发者理解代码或记录某些说明。

例如：

% This is a comment x : BITVECTOR(32); % This declares a 32-bit bitvector named x 

在上面的例子中，第一行和第二行的后半部分都是注释，用 % 开头，解释了代码的用途。

例子

示例 1：展示算术、字级和按位非操作

x : BITVECTOR(5); y : BITVECTOR(4); QUERY(     BVPLUS(9, x@0bin0000, (0bin000@(~y)@0bin11))[8:4]     =     BVPLUS(5, x, 0bin000@(~(y[3:2]))) ); 

1. x : BITVECTOR(5); - 声明一个5位的比特向量变量 x。
2. y : BITVECTOR(4); - 声明一个4位的比特向量变量 y。
3. QUERY(...) - 包含一个查询，验证表达式的等式是否成立。
4. BVPLUS(9, x@0bin0000, (0bin000@(~y)@0bin11))[8:4] - 进行比特向量加法运算，计算9位结果并提取其中的第8到第4位。
5. BVPLUS(5, x, 0bin000@(~(y[3:2]))) - 进行5位的比特向量加法运算。

示例 2：展示算术、字级和多路复用器术语

bv : BITVECTOR(10); a : BOOLEAN; QUERY(     (0bin01100000[5:3] = (0bin1111001@bv[0:0])[4:2])     AND     (         0bin1@(IF a THEN 0bin0 ELSE 0bin1 ENDIF)         =         (IF a THEN 0bin110 ELSE 0bin011 ENDIF)[1:0]     ) ); 

1. bv : BITVECTOR(10); - 声明一个10位的比特向量变量 bv。
2. a : BOOLEAN; - 声明一个布尔变量 a。
3. QUERY(...) - 包含一个查询，验证多个表达式的等式是否成立。
4. (0bin01100000[5:3] = (0bin1111001@bv[0:0])[4:2]) - 比较两个提取后的比特向量是否相等。
5. 0bin1@(IF a THEN 0bin0 ELSE 0bin1 ENDIF) - 使用多路复用器术语生成一个比特向量。
6. (IF a THEN 0bin110 ELSE 0bin011 ENDIF)[1:0] - 另一种多路复用器术语，提取其结果的低2位。

示例 3：展示按位操作

x, y, z, t, q : BITVECTOR(1024); ASSERT(x = ~x); ASSERT(x & y & t & z & q = ~x); ASSERT(x | y = t); ASSERT(BVXOR(x, ~x) = t); QUERY(FALSE); 

1. x, y, z, t, q : BITVECTOR(1024); - 声明五个1024位的比特向量变量 x, y, z, t, q。
2. ASSERT(x = ~x); - 断言 x 等于 x 的按位非操作结果（这个断言永远为假）。
3. ASSERT(x & y & t & z & q = ~x); - 断言五个比特向量按位与的结果等于 x 的按位非操作结果。
4. ASSERT(x | y = t); - 断言 x 和 y 的按位或操作结果等于 t。
5. ASSERT(BVXOR(x, ~x) = t); - 断言 x 和 x 的按位非操作结果的按位异或结果等于 t。
6. QUERY(FALSE); - 提交一个永远为假的查询，通常用于测试和验证目的。

示例 4：展示谓词和所有算术操作

x, y : BITVECTOR(8); ASSERT(x = 0hex05); ASSERT(y = 0bin00000101); QUERY(     (BVMULT(8,x,y) = BVMULT(8,y,x))     AND     NOT(BVLT(x,y))     AND     BVLE(BVSUB(8,x,y), BVPLUS(8, x, BVUMINUS(x)))     AND     (x = BVSUB(8, BVUMINUS(x), BVPLUS(8, x, 0hex01))) ); 

1. x, y : BITVECTOR(8); - 声明两个8位的比特向量变量 x 和 y。
2. ASSERT(x = 0hex05); - 断言 x 的值是十六进制的 05。
3. ASSERT(y = 0bin00000101); - 断言 y 的值是二进制的 00000101。
4. QUERY(...) - 包含一个查询，验证多个表达式的等式是否成立。
5. (BVMULT(8,x,y) = BVMULT(8,y,x)) - 断言 x 和 y 的乘积等于 y 和 x 的乘积。
6. NOT(BVLT(x,y)) - 断言 x 不小于 y。
7. BVLE(BVSUB(8,x,y), BVPLUS(8, x, BVUMINUS(x))) - 断言 x 减 y 的结果小于等于 x 加上 x 的按位非结果。
8. (x = BVSUB(8, BVUMINUS(x), BVPLUS(8, x, 0hex01))) - 断言 x 等于 x 的按位非结果减去 x 加上 0hex01 的结果。

示例 5：展示移位函数

x, y : BITVECTOR(8); z, t : BITVECTOR(12);  ASSERT(x = 0hexff); ASSERT(z = 0hexff0); QUERY(z = x << 4); 

1. x, y : BITVECTOR(8); - 声明两个8位的比特向量变量 x 和 y。
2. z, t : BITVECTOR(12); - 声明两个12位的比特向量变量 z 和 t。
3. ASSERT(x = 0hexff); - 断言 x 的值是十六进制的 ff。
4. ASSERT(z = 0hexff0); - 断言 z 的值是十六进制的 ff0。
5. QUERY(z = x << 4); - 查询 z 是否等于 x 左移4位的结果。

这些示例展示了如何在 STP 中使用不同的操作，包括谓词、算术操作和移位函数。通过这些操作，可以对比特向量进行复杂的计算和验证。