smt 相关问题

可满足性模数理论（SMT）是逻辑公式的决策问题，与经典的一阶逻辑中表达的背景理论的组合相等。

Z3：如何办理协会或会员资格？

我对解决 Z3 中的调度问题感兴趣，这需要以下内容：有多个类别：C1、C2、C3... 和多名学生：S1、S2、S3... 每个学生都需要恰好在一个

set z3 smt

回答 1 投票 0

使用 Z3 进行的简化并没有像预期的那样简化

在我的应用程序中，我想使用 Z3 求解器简化公式。我知道普通的简化策略不够强大，所以我使用 ctx-solver-simplify。然而，即使这样的策略也不能

z3 smt

回答 1 投票 0

如何使用 z3 库将经过优化的 SMT 模型转换为由 cvc4 等不同求解器识别的 .smt2 文件？

我想使用文件.smt2中的z3库转换用python编写的SMT模型，以获得可以从不同求解器（例如cvc4-solver）运行的文件。问题是我的模型...

optimization z3 smt cvc4 smt-lib

回答 2 投票 0

有从Python-Z3到Z3/smt2的解析器吗？

我正在使用Z3的Python API，因为方便，但有时我需要将Python结果转换为Z3/smt2的可读输入。例如，每当我执行量词消除时...

z3 smt z3py quantifiers

回答 1 投票 0

减少最大位向量大小的等价公式

是否有可能将 .smt2 公式转换为等效公式，以这样的方式重写它，即每个 (declare-const a (_ BitVec 256)) 将转换为一组 (declare-const a0 (_ BitVec .. .

z3 smt

回答 1 投票 0

Z3 Python Mod Int 问题

我想使用 Z3 打印小于 20 的素数。以下程序打印 2、3、5 和 7，但不打印 11、13、17 或 19。尽管 isPrime(11)、isPrime(13)、isPrime(17) 或 isPrime(...

python z3 smt sat

回答 1 投票 0

如果一个理论在存在片段中是可判定的，这是否意味着有一个（终止）方法来获得满意的证人？

我担心是否有算法（例如，在 SMT 求解器中实现）保证终止给出存在公式模型的任务；以同样的方式他们保证

z3 smt quantifiers first-order-logic

回答 0 投票 0

CVC5 表示“未知”给定编码为 TPTP 的归纳数据类型，尝试为构造函数找到模型

（编辑：请参阅下面的更短的失败示例！）下面的 TPTP 问题是我从精益 4 到 TPTP 的翻译产生的。归纳类型被翻译成一堆打字声明......

types smt sat

回答 0 投票 0

将 true 分配给除 one 之外的所有变量

我有一个变量列表，我想向 z3 求解器添加约束，例如所有变量都应该是 False，除了一个变量应该是 True .. a,b,c,d= Bool('a,b,c,d') s = 求解器() 所有变量=[...

z3 solver smt z3py sat

回答 1 投票 0

实数理论决策程序的实现

是否有实数一阶理论的实现？我知道柯林斯存在一种基于圆柱代数分解的技术，但我不知道任何定理证明者......

z3 smt theorem-proving cvc4

回答 1 投票 0

用z3py寻找集合中的最小元素数。

练习。找出Z的最小元素数，加起来是4285。其中Z = { w(i): w(n) - n^2 - n + 1, i = 1,2,...,30 }。我创建了一个解决方案： def f(t): return t ** 2 - t + 1 opt ...

python z3 solver smt z3py

回答 2 投票 0

Z3中浮点值的Sum()

我想写一些东西来求解一个可变数量的浮点变量给予预期的平均值。然而，当我试图运行我的代码时，我得到了这个异常。z3.z3types.Z3Exception:......。

python z3 smt

回答 1 投票 0

逐步减弱Maxsat的实力

我有一个关于MaxSat的想法，并且已经用MSU3实现了一个天真的Maxsat求解器，同时用minisat APIs实现了顺序编码，我想知道是否有办法加快这个求解器的速度。I ...

smt constraint-programming sat satisfiability sat-solvers

回答 1 投票 2

如何将Z3的AST翻译成ASM代码？[非公开]

有一个例子： mov edi, dword ptr [0x7fc70000] add edi, 0x11 sub edi, 0x33F0B753 经过Z3简化，我得到了(内存0x7FC70000是符号化的)： bvadd (_ bv3423553726 32) MEM_0x7FC70000 ....

assembly compiler-construction z3 smt triton

回答 1 投票 0

exist-expression中seq.nth的奇怪行为。

在这个上运行z3 (assert (< (seq.nth (seq.unit 0) 0)))(check-sat)的结果是UNSAT，但是运行(assert (existence ((x Int))(< (seq.nth (seq.unit 0) x) 0))) (check-sat) (get-model) ...

z3 smt

回答 1 投票 0

调整Z3量化器实例的指南（带SMT-LIB接口）。

我试图在机器生成的问题上调整z3，这些问题是不可满足的，包含与证明无关的断言，不相关的断言包含量化器，z3无法找到 ...

z3 smt

回答 1 投票 0

微软Z3获得相关作业

如何只获取z3可满足性检查后使用的变量的相关值赋值？比如说我有多个断言作为约束条件给Z3 Sat Solver，... ...

java z3 smt sat

回答 1 投票 0

在smtlib中定义列表concat

我根据Haskell定义了自己的列表concat版本，如下所示：（声明数据类型（（MyList 1））（（par（T）（（cons（head T）（tail（MyList T））））（nil）））））（声明一个有趣的my-concat（（...

z3 smt z3py

回答 1 投票 0

是否可以通过CVC4 C ++ API解析SMT-LIB2字符串？

我有一个可以动态生成SMT-LIB格式的表达式的程序，我正在尝试将这些表达式连接到CVC4以测试可满足性并获取模型。我想知道是否有...

smt cvc4

回答 1 投票 0

是否有增量式Max-SMT求解器？

我正在处理位向量数组的问题，该数组在不同时间尺度上对不同时间序列数据之间的逻辑关系进行编码，以生成具有任意属性的合成数据。我...

constraints z3 smt sat

回答 1 投票 1

最新问题

© www.soinside.com 2019 - 2024. All rights reserved.