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]
数组写入WITHx_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)BVXORBVXOR(t1, t2)
按位与非 (NAND)BVNANDBVNAND(t1, t2)
按位或非 (NOR)BVNORBVNOR(t1, t2)
按位同或 (XNOR)BVXNORBVXNOR(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 进行按位同或操作。

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

算术函数

名称符号示例
比特向量加法BVPLUSBVPLUS(n,t1,t2,…,tm)
比特向量乘法BVMULTBVMULT(n,t1,t2)
比特向量减法BVSUBBVSUB(n,t1,t2)
比特向量一元减法BVUMINUSBVUMINUS(t1)
比特向量除法BVDIVBVDIV(n,t1,t2)，其中 t1 是被除数，t2 是除数
有符号比特向量除法SBDIVSBDIV(n,t1,t2)，其中 t1 是被除数，t2 是除数
比特向量模运算BVMODBVMOD(n,t1,t2)，其中 t1 是被除数，t2 是除数
有符号比特向量模运算SBVMODSBVMOD(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)BVLTBVLT(t1,t2)
大于 (Greater Than)BVGTBVGT(t1,t2)
小于或等于 (Less Than Or Equal To)BVLEBVLE(t1,t2)
大于或等于 (Greater Than Or Equal To)BVGEBVGE(t1,t2)
有符号小于 (Signed Less Than)SBVLTSBVLT(t1,t2)
有符号大于 (Signed Greater Than)SBVGTSBVGT(t1,t2)
有符号小于或等于 (Signed Less Than Or Equal To)SBVLESBVLE(t1,t2)
有符号大于或等于 (Signed Greater Than Or Equal To)SBVGESBVGE(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))ANDNOT(BVLT(x,y))ANDBVLE(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 中使用不同的操作，包括谓词、算术操作和移位函数。通过这些操作，可以对比特向量进行复杂的计算和验证。

本文来自互联网用户投稿，该文观点仅代表作者本人，不代表本站立场。本站仅提供信息存储空间服务，不拥有所有权，不承担相关法律责任。如若转载，请注明出处：http://www.mzph.cn/diannao/47457.shtml

如若内容造成侵权/违法违规/事实不符，请联系多彩编程网进行投诉反馈email:809451989@qq.com，一经查实，立即删除！

相关文章

pytorch学习（四）绘制loss和correct曲线

pytorch学习（四）绘制loss和correct曲线

这一次学习的时候静态绘制loss和correct曲线&#xff0c;也就是在模型训练完成后&#xff0c;对统计的数据进行绘制。 以minist数据训练为例子 import torch from torch import nn from torch.utils.data import DataLoader from torchvision import datasets from torchvisi…
阅读更多...
python+pygame实现扫雷游戏之二

python+pygame实现扫雷游戏之二

接pythonpygame实现扫雷游戏之一&#xff0c;继续写游戏局的类&#xff1a; 五、 mineblock.py # -*- coding: utf-8 -*- import randomfrom blockstatus import * from mine import *# 9*9-10 16*16-40 30*16-99 30*24-** # BLOCK_WIDTH 30 # BLOCK_HEIGHT 16 # MIN…
阅读更多...
【zabbix6监控java-tomcat全流程】

【zabbix6监控java-tomcat全流程】

目录 一、监控主机安装zabbix-server1、zabbix的安装2、配置数据库3、为zabbix server配置数据库4、启动服务,web界面安装 二、被监控主机安装tomcat1、安装JDK2、安装tomcat 三、zabbix的服务端安装zabbix-java-gateway四、被监控主机tomcat的配置五、web界面添加主机 一、监控…
阅读更多...
使用 Web APi - MediaRecorder 获取麦克风资源，报错：Cannot find name ‘MediaRecorder‘ 的解决方法

使用 Web APi - MediaRecorder 获取麦克风资源，报错：Cannot find name ‘MediaRecorder‘ 的解决方法

目录 一、背景&#xff1a; 二、具体解决方法 一、背景&#xff1a; angular 调用 MediaRecorder 来使用麦克风获取声音&#xff0c;&#xff08;具体要求&#xff1a;angular 前端 按键调用 麦克风&#xff0c;松开按键生成音频文件&#xff09;代码如下&#xff08;来自通…
阅读更多...
【树莓派3B+】控制引脚输出高低电平

【树莓派3B+】控制引脚输出高低电平

前言一、安装RPI.GPIO库二、编写简单的输出高低电平的程序三、运行程序总结 前言 首先检查一下自己的板子有没有带库 我这个是有的。 ok&#xff0c;正式进入步骤 一、安装RPI.GPIO库 如果还没有安装RPi.GPIO库&#xff0c;可以通过以下命令在树莓派上安装&#xff1a; p…
阅读更多...
Ubuntu20.04从零开搭PX4MavrosGazebo环境并测试

Ubuntu20.04从零开搭PX4MavrosGazebo环境并测试

仅仅是个人搭建记录 参考链接&#xff1a; https://zhuanlan.zhihu.com/p/686439920 仿真平台基础配置&#xff08;对应PX4 1.13版&#xff09; 语雀 mkdir -p ~/tzb/catkin_ws/src mkdir -p ~/tzb/catkin_ws/scripts cd catkin_ws && catkin init catkin build cd…
阅读更多...
数据结构day2

数据结构day2

一、思维导图 内存分配 二、课后习题 分文件编译 //sys.h #ifndef TEST_H #define TEST_H #define MAX_SIZE 100//定义学生类型 typedef struct Stu {char name[20]; //姓名int age; //年龄double score; //分数 }stu;//定义班级类型 typedef struct Class {struct …
阅读更多...
Postman实战案例：从零开始设计API测试流程

Postman实战案例：从零开始设计API测试流程

Postman实战案例&#xff1a;从零开始设计API测试流程 API测试在现代软件开发中至关重要。Postman作为一款强大的API测试工具&#xff0c;不仅提供了直观的用户界面&#xff0c;还支持自动化测试、环境配置和脚本编写。本文将从零开始&#xff0c;详细介绍如何使用Postman设计…
阅读更多...
php在服务器上部署可视化运维工具详细列表

php在服务器上部署可视化运维工具详细列表

如果你的项目很小&#xff0c;可以用宝塔。但对于并发大的服务器管理&#xff0c;选择适合的工具非常重要。 目录 以下是一些免费且适合高并发管理的服务器管理工具推荐&#xff1a; 1Panel&#xff1a; Portainer&#xff1a; Webmin&#xff1a; Cockpit&#xff1a; …
阅读更多...
实战：详解Spring创建bean的流程（图解+示例+源码）

实战：详解Spring创建bean的流程（图解+示例+源码）

概叙 这篇主要总结Spring中bean的创建过程&#xff0c;主要分为加载bean信息–>实例化bean–>属性填充–>初始化阶段–>后置处理等步骤&#xff0c;且每个步骤Spring做的事情都很多&#xff0c;这块源码还是很值得我们都去看一看的。而Spring中Bean的声明周期其实…
阅读更多...
GEO数据挖掘从数据下载处理质控到差异分析全流程分析步骤指南

GEO数据挖掘从数据下载处理质控到差异分析全流程分析步骤指南

0. 综合的教学视频介绍 GEO数据库挖掘分析作图全流程每晚11点在线教学直播录屏回放视频&#xff1a; https://www.bilibili.com/video/BV1rm42157CT/ GEO数据从下载到各种挖掘分析全流程详解&#xff1a; https://www.bilibili.com/video/BV1nm42157ii/ 一篇今年近期发表的转…
阅读更多...
捷配总结的SMT工厂安全防静电规则

捷配总结的SMT工厂安全防静电规则

SMT工厂须熟记的安全防静电规则&#xff01; 安全对于我们非常重要&#xff0c;特别是我们这种SMT加工厂&#xff0c;通常我们所讲的安全是指人身安全。 但这里我们须树立一个较为全面的安全常识就是在强调人身安全的同时亦必须注意设备、产品的安全。 电气&#xff1a; 怎样预…
阅读更多...
IDEA 调试 Ja-Netfilter

IDEA 调试 Ja-Netfilter

首先本地需要有两款IDEA 可以是相同版本&#xff0c;也可以是不同版本。反正要有两个&#xff0c;一个用来调试代码&#xff0c;一个启动。 移除原有ja-netfiler 打开你的ja-netfiler的vmoptions目录&#xff0c;修改其中的idea.vmoptions文件。移除最后一行-javaagent ...参…
阅读更多...
分享 .NET EF6 查询并返回树形结构数据的 2 个思路和具体实现方法

分享 .NET EF6 查询并返回树形结构数据的 2 个思路和具体实现方法

前言 树形结构是一种很常见的数据结构&#xff0c;类似于现实生活中的树的结构&#xff0c;具有根节点、父子关系和层级结构。 所谓根节点&#xff0c;就是整个树的起始节点。 节点则是树中的元素&#xff0c;每个节点可以有零个或多个子节点&#xff0c;节点按照层级排列&a…
阅读更多...
有效应对服务器遭受CC攻击的策略与实践

有效应对服务器遭受CC攻击的策略与实践

分布式拒绝服务&#xff08;DDoS&#xff09;攻击&#xff0c;尤其是其中的HTTP洪水攻击或称为CC攻击&#xff08;Challenge Collapsar&#xff09;&#xff0c;是当今互联网安全领域的一大挑战。这种攻击通过大量合法的请求占用大量网络资源&#xff0c;导致服务器无法正常响应…
阅读更多...
数据可视化入门

数据可视化入门

文章目录 1. 数据可视化的发展历史1.1 古代与中世纪1.2 18世纪与19世纪1.3 20世纪1.4 21世纪 2. 数据可视化技术基础2.1 数据收集2.2 数据清洗2.3 数据加工 3. 图表库的选型3.1 常见图表库3.2 常用图表库 4. 数据可视化实战4.1 案例&#xff1a;使用Matplotlib和Seaborn进行数据…
阅读更多...
AI智能名片S2B2C商城小程序在社群去中心化管理中的应用与价值深度探索

AI智能名片S2B2C商城小程序在社群去中心化管理中的应用与价值深度探索

摘要&#xff1a;随着互联网技术的飞速发展&#xff0c;社群经济作为一种新兴的商业模式&#xff0c;正逐渐成为企业与用户之间建立深度连接、促进商业增长的重要途径。本文深入探讨了AI智能名片S2B2C商城小程序在社群去中心化管理中的应用&#xff0c;通过详细分析社群去中心化…
阅读更多...
【DGL系列】DGLGraph.out_edges简介

【DGL系列】DGLGraph.out_edges简介

转载请注明出处&#xff1a;小锋学长生活大爆炸[xfxuezhagn.cn] 如果本文帮助到了你&#xff0c;欢迎[点赞、收藏、关注]哦~ 目录 函数说明 用法示例 示例 1: 获取所有边的源节点和目标节点 示例 2: 获取特定节点的出边 示例 3: 获取所有边的边ID 示例 4: 获取所有信息&a…
阅读更多...
中国机器视觉行业上市公司市场竞争格局分析

中国机器视觉行业上市公司市场竞争格局分析

中国机器视觉产业上市公司汇总&#xff1a;分布在各产业链环节 机器视觉就是用机器来代替人眼做测量和判断的系统&#xff0c;机器检测相较于人工视觉检测优势明显。目前&#xff0c;我国机器视觉产业的上市公司数量较多&#xff0c;分布在各产业链环节。具体包括&#xff1a;…
阅读更多...
LeetCode-返回链表倒数第K个节点、链表的回文结构，相交链表

LeetCode-返回链表倒数第K个节点、链表的回文结构，相交链表

一、返回链表倒数第k个节点 . - 力扣&#xff08;LeetCode&#xff09; 本体思路参展寻找中间节点的方法&#xff0c;寻找中间节点是定义快慢指针&#xff0c;快指针每次走两步&#xff0c;慢指针每次走一步&#xff0c;当快指针为空或者快指针的下一个节点是空时&#xff0c;…
阅读更多...
最新文章

Copyright @ 2022~2023