我有一个只有以下数据类型声明的上下文： EnumSort signal = ctx.mkEnumSort("signal", "red", "yellow", "green"); 我想要的是获得上述声明的等效我尝试为这个上下文创建一个求解器，然后执行solver.toString()，但它不会打印任何内容，除非我在断言中使用此声明。
浏览 8提问于2019-06-09得票数 0
回答已采纳
1回答
有没有一种方法可以像在Python中那样以人类可读的形式打印AST？我想要一些像这样的东西而不是
(and (= x 3) (> (f 3) 2)
浏览 2提问于2013-04-23得票数 1
回答已采纳
我试图使用Z3 API为python找到一个最优的解决方案。我使用set_option("verbose", 1)打印Z3在检查sat时生成的语句。它打印的语句之一是pb.conflict语句。这些声明意味着什么？还有，和它一起打印的两个数字是什么？
浏览 0提问于2018-11-02得票数 1
回答已采纳
1回答
我正在为一个项目使用z3 Java API。对于一些例子，它需要花费太多的时间来解决。我已经等了好几个小时了，还是不能解决这个问题。我不知道它会不会解决。但是当我将Solver::toString的输出打印到一个文件中时，z3二进制在一秒钟内就解决了这个问题。我尝试了一些策略和参数，但没有帮助。这里有一个例子(列表理论)：
API和二进制的版本都是4.8.0。我在64位的Ubunt
浏览 1提问于2018-08-16得票数 0
我在Java中使用Z3。在我的SMT 2文件中，有几个变量：(declare-fun x1 () Bool)我希望获得所有这些变量，并将它们存储在一个从z3分发的示例中，我发现了从SMT-LIB1文件中解析声明的API SMTLIBDecls，但是对于SMT-LIB2却没有类似的SMTLIBDecls。我怎样才能得到这些声明？
谢谢。
浏览 2提问于2014-05-12得票数 2
回答已采纳
1回答
在我使用Z3 for Java的当前项目中，我遇到了一些性能问题:基本上，我当前的大部分约束非常简单:例如：(f(x) = 2 && f(y) <= 3) || f(x) <=5
我使用的是由整个项目共享的静态上下文和求解器实例如果我用同样的ctx实例产生数十亿次的费用，这会成为一个问题吗？何时是调用ctx.Dispose()的最佳时机，还是管理ctx的最佳方法是什么
浏览 0提问于2014-06-12得票数 2
回答已采纳
1回答
我想使用Z3对位向量进行推理。此外，对于可满足性的判定，我还需要比特向量的符号表示，以便我可以根据需要对它们应用自己的计算。例如：
.期望的输出
浏览 4提问于2014-04-22得票数 2
1回答
回到过去的日子(即。去年)，我们曾经能够使用理论插件作为一种实现自定义简化器的方法。Z3文档甚至包含了。
我的问题很简单:有没有办法用Z3 4.x实现同样的目标？特别是，我感兴趣的是一种为Z3提供基本术语的外部计算评估的方法。
浏览 2提问于2012-12-10得票数 2
回答已采纳
我想问一下，如何下载使用Java的稳定版本的Z3？在codeplex的主分支中，源不包含目录src/api/java。
这是存在于一些分支，如cade24或rc和其他。我不知道该选哪一个。
浏览 1提问于2014-10-23得票数 1
回答已采纳
1回答
用Python简化方程
、、、、
我正在学习如何在Python中使用表达式时完成一些任务。
I希望能够简化/减少包含中间变量的方程组。假设我有方程(A = B && C)和(C = D || E)。在z3中，它们将表示为(Bool('A') == And(Bool('B'), Bool('C'))和(Bool('C') == Or(Bool('D'), Bool('E'))。是否有一些函数或一系列函数可用于生成简化和简化的
浏览 1提问于2019-10-23得票数 1
回答已采纳
比特掩码0xaaaaaaaaaaaaaaaaL (16a's)在kotlin的范围或范围内。如果我有Android Sutdio自动转换从Java，它转换为-0x5555555555555556L，即1010101010101010101010101010101010101010101010101010101010101100xaaaaaaaaaaaaaaaaL在Java中工作得很好。我需要一个解释，为什么它成为-0x5555555555555556L在科特林。另一个问题是，kotlin是如何代表负面长的？它不是
浏览 10提问于2021-08-13得票数 3
回答已采纳
我可以使用z3从命令行运行(string)查询，可以指定smt.string_solver=z3str3，也可以不指定smt.string_solver=z3str3：如何通过API指定相同的内容？我试过用以下方式打印战术名称：/* [0] Context */
/***************
浏览 1提问于2018-06-12得票数 0
回答已采纳
我无法打印/显示作为Z3模型的一部分返回的set对象。我看不到任何真正打印出来的方法。标准的ToString()方法只是简单地说它是一个数组，显示模型表明该集合是使用查询函数在内部表示的。我想我可以遍历集合的查询函数表示，但这对我来说似乎不太好，如果Z3中集合的表示发生变化，就会破坏我的代码。API中是否有我遗漏<em
浏览 0提问于2013-04-11得票数 1
回答已采纳
2回答
如何读取和打印文本文件中的内容？ String NAME= st.nextElement().toString=null) }
错误:未报告的异常<
浏览 0提问于2012-11-17得票数 0
1回答
对于我的任务，我要在一个扩展Number的层次结构中创建5个类。我要为每个类创建加、减、乘和除的方法，每个类都有两个参数和一个返回类型。我该如何解决这个问题？
浏览 0提问于2011-11-09得票数 3
回答已采纳
2回答
我想要从z3得到的解决方案，而不是使用let语句进行简化。(<= (- x.1 11) 0)))) (<= (- x.1 9) 0))) (= (- (+ x.1 2) x) 0))))有没有办法告诉Z3不要把一些复杂的表达式提取到let语句中？如果我不使用let语句就能得到扁平化的结果，那么对我来说解析结果会更容易。
浏览 0提问于2012-11-20得票数 5
回答已采纳
在关于这个问题的一个评论中提到了这一点：想知道是否有一种强制Object.toString而不是MyClass.toString的方法。例如，类似于这件事能轻易做到吗？我们使用的是java8
浏览 0提问于2019-05-27得票数 3
回答已采纳
4回答
在Java语言中，我知道每当我们打印对象引用时，内部都会调用toString()。默认情况下，toString()将以"classname@hashcode“的格式打印。
浏览 63提问于2017-03-09得票数 4
回答已采纳
云服务器
对象存储
ICP备案
云点播
实时音视频
腾讯云开发者
Copyright © 2013 - 2026 Tencent Cloud. All Rights Reserved. 腾讯云 版权所有
深圳市腾讯计算机系统有限公司 ICP备案/许可证号：粤B2-20090059 
粤公网安备44030502008569号
腾讯云计算（北京）有限责任公司 京ICP证150476号 | 京ICP备11018762号