z3 相关问题

Z3是Microsoft Research开发的高性能定理证明器。

Z3优化中的间隙公差控制

我想使用z3优化类来获得次优的结果，同时仍然能够控制我离最优结果有多远。我正在使用C ++ API。例如，CPLEX具有...

optimization z3

回答 1 投票 1

我们可以提取z3使用的当前策略，然后类似地配置另一个实例吗？

我想在设置特定逻辑时重复使用/激活的策略，但是我需要避免使用set-logic。因此，有什么方法可以让Z3在...

回答 1 投票 0

使用MAXSMT进行增量学习

我们可以在z3中以增量方式使用MaxSMT求解器的先前解决方案（优化）吗？另外，是否有任何方法可以在优化程序上打印出软断言？

z3 smt

回答 1 投票 0

这些条款的等效horn条款是什么？

我正在使用Z3和扩展的SMT-LIB2语法来解决我的horn子句。我知道horn子句的头应该是未解释的谓词；但是，我不知道应该如何重写以下内容...

z3 z3-fixedpoint horn

回答 1 投票 0

为什么Z3对这些号角子句返回“未知”

我正在使用Z3解决我的horn子句。在Horn子句的主体中，未解释的谓词应为肯定。但是，我需要否定一些未解释的谓词。我看过一些...

z3 z3-fixedpoint

回答 1 投票 0

cpp中z3的编译和执行命令？

＃include #include #include“ mainProj.cpp”使用命名空间std;使用名称空间z3; int main（）{上下文c; tactic t = tactic（c，“ bit-blast”）; expr x = c .... ] >>

c++ z3 smt

回答 1 投票 0

检查一阶逻辑是否满足要求的工具/语言？

通常，一阶逻辑是不确定的。但是，可以确定一些一阶逻辑片段，例如Monadic逻辑，BSR片段，分隔片段。有解决SAT / SMT问题的工具...

z3 first-order-logic satisfiability sat-solvers

回答 1 投票 1

z3中有实值计算的问题

我正在研究一个我想根据某些约束来学习真实参数的问题。以下是代码片段：s = Solver（）def logistic_function（x，y）：out = y [0] for i in ...

z3 smt

回答 1 投票 0

为什么Python是64位时，为什么不能在Windows上使用pip安装angr-z3？

它说模块机器类型不匹配；为什么？（注意：这是一个自我解答的问题；请参阅下文。）

python pip 64-bit z3 angr

回答 1 投票 1

SMT-LIB基准

我想对一些SMT求解器进行基准测试，而SMT-LIB Benchmark存储库[1,2]似乎是一个不错的起点。但是，链接已关闭至少几天。有人知道吗...

z3 smt bitvector

回答 2 投票 2

z3py处函数“ from_file（）”的问题

假定我们具有以下文件：func.smt（声明数据类型（T）（（（AVL leafA（nodeA（val T）（alt Int）（izq AVL）（der AVL）））））espec.smt （declare-const t（AVL Int））和...

z3 solver z3py

回答 1 投票 0

有什么方法可以使Z3使用多核（多线程）解决大问题？

我正尝试从商用求解器转到Z3，以解决大整数可满足性问题。 “大”是指我要求解的模型具有约300,000个整数和300,000个（...

optimization z3 smt

回答 1 投票 1

Z3中定义变量和常量的宏

我想在Z3中拥有可以定义变量和常量的宏。我无法弄清楚如何使用该语言，因此我正在使用cpp（c预处理器）来执行此操作。例如，我有：＃...

macros c-preprocessor z3

回答 1 投票 2

unzip z3解算器失败

我正在尝试在非root用户的远程Linux服务器上安装z3，我已将ubuntu匹配发行版下载到服务器上的主目录中，当我解压缩它时，我没有得到所有文件夹...] >

ubuntu server z3

回答 1 投票 0

z3模型的NoneType输出

我正在使用MaxSMT来找到一组软约束和硬约束的解决方案。超时为600秒，我从求解器得到的模型输出对于所有参数都是Nonetype。我...

z3 smt

回答 1 投票 0

z3解算器：使用“ parseSMTLIB2String”与“ rise4fun在线工具”获得不同的结果

我正在使用z3开发Java程序，但是当我使用“ parseSMTLIB2String”方法与在线工具rise4fun测试非常简单的编码时，得到了不同的结果。以下是我用于测试的编码：...

java z3

回答 1 投票 1

Z3Py：创建未解释类型的常量列表

我有一个未解释的排序A sortA = DeclareSort（'A'）和一个函数foo：foo = Function（'foo'，sortA，sortA，BoolSort（））现在，我想定义一个排序为A的常量列表。我的尝试是：X = [...

z3 z3py

回答 1 投票 0

在SMT的定义中包含断言

我想捕获事实事实断言。 int f（x）{if（x == 1）返回1; else {assert（x> 0）;返回2; }} int g（x）{assert（x> 5）; ...

z3 smt

回答 1 投票 1

如何将IntVector转换为z3py中的Int

我正在使用z3py，并且我有一个大小为3的IntVector。我需要将IntVector中的每个数字解析为一个整数。意思是，如果我有一个IntVector，它具有这样的约束：myIntVector = ...

python z3 smt z3py

回答 1 投票 1

在z3py中使用BitVec数组

我正在尝试使用z3中的Array类型解决问题。因为我需要使用BitVec类型，所以我将数组声明为：numbers = [BitVec（chr（i），8）for range（0，4）中的i]然后：s = Solver（）s ....

python z3 z3py

回答 1 投票 0

z3 相关问题

最新问题