z3 - ( :var 0) in z3 Quantifier's body-6ren

z3 - ( :var 0) in z3 Quantifier's body

转载作者：行者123 更新时间：2023-12-04 18:34:42

25

4

当我得到 Z3 OCaml API 的量词主体时，例如一个字符串为的量词

(exists ((u_1 Int)) (= u_1 x5))

通过 Quantifier.get_body，我获得了表达式

(= (:var 0) x5)

我猜这个表达式中的 (:var 0) 是将 u_1 重命名为一个新变量，但我不知道表达式 (:var 0) 的类型是什么以及当我们将它匹配回 u_1 时想要从其主体及其绑定(bind)变量重建量词。

谁能提出解决方案？非常感谢。

最佳答案

我得到了解决方案。表达式 e

(:var 0)

是 VAR_AST 的表达式。您可以通过以下方式查看

AST.is_var (Expr.ast_of_expr e)

然后，您可以通过

获取其索引，例如 0

Quantifier.get_index e

使用索引，您可以轻松地将表达式 e 与其绑定(bind)变量相匹配。请注意，量词的绑定(bind)变量列表可以通过以下方式获得

Quantifier.get_bound_variable_names

关于z3 - ( :var 0) in z3 Quantifier's body，我们在Stack Overflow上找到一个类似的问题： https://stackoverflow.com/questions/39836076/

25

4

0

文章推荐： sql - 插入的数据未使用直接查询显示在 Oracle 数据库中

文章推荐： qt - QAbstractTableModel::insertRows() 的基本用法

文章推荐： url - 回调中的 ShareThis 设置属性不起作用

文章推荐： javascript - RxJS 减少一个 ReplaySubject

php - Mysql SELECT WHERE $VAR IN $VAR,$VAR,$VAR
这个问题已经有答案了: Can I bind an array to an IN() condition in a PDO query? (23 个回答) 已关闭 5 年前。任何人都可以看到我如何在
linux - "var=${var:-word}"和 "var=${var:=word}"有什么区别？
我阅读了关于此的 bash 手册页，但我不明白其中的区别。我对它们进行了测试，它们似乎产生了完全相同的结果。如果值不是通过命令行参数设置的，我想设置一个变量的默认值。 #!/bin/bash var
PHP/MySQL SET var = var - var
我为我的网站开了一家商店，并让它运行起来，但我意识到它无法正确购买商品。换句话说，您不会走进一家商店，拿起一件商品，购买，再次购买，购买，再次购买，等等，以获得想要的数量。你一次捕获他们。我的网站缺少
c - 将 &var 传递给 *var 和将 var 传递给 var 有什么区别？
基本上，我想知道为什么会这样(将列表的内存地址作为参数传递): void init_lista (elemPtr *list) { *list = NULL; } int main(){
javascript - "+var === +var"在内部如何工作以验证 var 是否为数字？
看到这个问题:Is there a (built-in) way in JavaScript to check if a string is a valid number?还有这个:jsperf ，其
java正则表达式用{var}次{var}px替换{var}px
我有以下字符串: 我想用正则表达式替换所有后面有 px 的数字，并用 X 乘以它们的值。 (X 是一个变量)。所以如果X=3，结果就是请注意 X 必须是我将检索到函数的变量最佳答案以下代码
java - while (var != var)
这个问题在这里已经有了答案: 关闭 13 年前。同时 (var != var) System.out.println("循环.."); 执行它..如何声明..var
java - "var &= expr"的行为不像 "var = var && expr"
我只是好奇。我想知道表达式是否有特定原因 var &= expr 行为方式与不同 var = var && expr. 看起来第一个表达式中的表达式正在执行，而不管 var 上的 false 值。我
ruby - 为什么 Ruby 为 "var = var + 1"而不是 "var = var + 0"创建一个新对象？
我有这个 Ruby 代码: var1 = 10 puts var1.object_id var1 = var1 + 0 puts var1.object_id var1 = var1 + 1 puts
c++ - 如何从 `var (*)(void*, var)` 中获取 C 指针(如 `boost::function` )？
这个问题在这里已经有了答案: 关闭 10 年前。 Possible Duplicate: demote boost::function to a plain function pointer 所以我
javascript - 将 var 分配给临时 var 不会阻止原始 var 发生变化
好吧，堆栈溢出，我花了几个小时来解决 javascript 中的问题(在 NodeJS 服务器中编写)，但我真的不明白。这就是发生的事情: var data = {x: 50}; var temp
php - 鉴于 $var = 1，$var = $var === 0 为何不返回 false？
首先，我在这里处理 1 和 0，我很清楚 1 == true 和 0 == false。但是我很好奇为什么这不起作用: $var = 1; echo $var; /* 1 */ $var = $var
bash - Bash shell 中的 ${var}、 "$var"和 "${var}"之间有什么区别？
标题说的是什么:将变量封装在 {}、"" 或 "{}"中是什么意思？我无法在网上找到关于此的任何解释 - 除了使用不会产生任何结果的符号外，我无法引用它们。这是一个例子: declare -a gr
javascript - 我如何在 $(var).*** var ="#tag",html jquery 中发送 var
我需要将信息发送到我的 Html。例如 $(document).ready(function() { var = "'#"+result.tag+"'" // var = '#tag_dinamy
linux - bash 脚本 : combine var=$(. ..) 和 var=${var%%...} 行？
是否可能，如果可以，如何将以下表达式转换为一行？ DEV=$(lsblk -no KNAME,MODEL | grep 'ModelNAME') DEV=${DEV%%'ModelNAME'} 简单的
php - isset($var) == "Test"和 isset($var) && $var == 'Test"有什么区别
isset($var) == "Test" 和 isset($var) && $var == 'Test" 有什么区别？最佳答案这里是一个简短的例子: $var = "Chuck Test"; v
php - isset($var) == "Test"和 isset($var) && $var == 'Test"有什么区别
isset($var) == "Test" 和 isset($var) && $var == 'Test" 有什么区别？最佳答案这里是一个简短的例子: $var = "Chuck Test"; v
javascript - 正则表达式匹配 : b: and c: in [Object a:var b:var c:var];
如果我有一个字符串:[Object a:var b:var c:var]; 如何将 a:、b: 和 c: 与正则表达式匹配？我试过:\[.+\s+(.+:).+\] 但它不适用于 a、b 和 c，它
c++ - 使用 "if (var = 0 || var == 0)"语句将 var 更改为 1
这个问题在这里已经有了答案: Why does this if-statement combining assignment and an equality check return true? (
Powershell - if $var -like $var*
我正在 Powershell 中使用 SCSM，但遇到了 if 语句的问题。我有一个函数，它根据作为变量传递给函数的条件收集数据。例子: $JMLs1 = collectTickets -crit

首页

博学

6Ren·AI

商城

z3 - ( :var 0) in z3 Quantifier's body