z3

    0热度

    1回答

    在Z3Py中发出实际的号码

    在Z3Py中给出像Real('x')这样的实际号码，我该如何获得其楼层或天花板？等同地，我该如何整理它？我发现to_int是SMT规范中的一件事，但我不知道如何从Python中调用它。
    z3 z3py 2017-05-12

    0热度

    1回答

    Z3求解差异逻辑的Python API

    我一直在试图做这样的事情在python： (set-option :smt.arith.solver 1) (declare-const x Int) (declare-const y Int) (assert (>= 10 x)) (assert (>= x (+ y 7))) (maximize (+ x y)) (check-sat) 我已经能够做到这一点的解算器（solve
    logic z3 smt z3py 2017-03-23

    6热度

    1回答

    Z3Py中的K-out-of约束

    我正在使用Z3 theorem prover（Z3Py）的Python绑定。我有N个布尔变量，x1，..，xN。我想表达这样一个约束，即它们中的N个应该是正确的。我该怎么做，在Z3Py？有没有内置的支持？我查看了在线文档，但Z3Py docs没有提及任何API。我知道我可以分别表示至少有一个是真的（assert Or（x1，..，xN）），并且至多有一个是真的（assert Not（And） （x
    z3 z3py sat 2017-03-28

    1热度

    1回答

    在使用C++ API加载smt2文件后向Z3添加断言

    我正尝试使用C++/C API for z3（v4.5.1）加载smt2文件，然后使用API​​添加断言，数据类型以及在smt2文件中声明的函数。 这里是我做的一个文件加载到求解一个例子： solver loadBackgroundTheoryFile(context& c, string filename) { Z3_ast ast = Z3_parse_smtlib2_file(c,
    z3 2017-04-04

    1热度

    1回答

    这个简单的Z3证明为什么这么慢？

    以下Z3代码超时的在线REPL： ; I want a function (declare-fun f (Int) Int) ; I want it to be linear (assert (forall ((a Int) (b Int)) ( = (+ (f a) (f b)) (f (+ a b)) ))) ; I want f(2) == 4 (assert (=
    z3 2017-04-06

    0热度

    1回答

    嵌套存储操作的有效方式

    在Most efficient way to represent memory buffers in Z3关于如何使嵌套存储操作更高效的问题被回答为可以用选择替换（嵌套）存储操作，如(assert (= (select A i1) v1))。但是，我需要商店操作，因为之前的约束必须用新的约束来替换。 例如：下面的约束模拟以下组件的程序： mov qword ptr [rax], rbx mov
    z3 2017-05-26

    0热度

    2回答

    在Z3中声明大小未知的矩阵

    我知道我可以在Z3中声明一个z3.Real的矩阵，通过单独声明它的元素（可能通过列表理解）。有没有办法来表示一个未知大小的矩阵？ 例如，考虑下面的例子： 在图像滤波，给定的size [X,Y]的图像I和滤波器核的size [M,N]K，图像I和滤波器内核K是I*K之间的卷积。我想Z3来证明（或反驳）存在任何大小的过滤器F1和F2，例如I*K == I*F1*F2。 问题本身是完全组成的，可能没有意
    z3 z3py 2017-04-14

    1热度

    1回答

    如何在Z3py公式中正确使用ZeroExt（n，a）？

    我想找出隐藏在二进制文件中的keygen算法的密码。所以，我提取从组件式和翻译（正确地，希望）在一个小Python脚本来解决它： #!/usr/bin/env python from z3 import * # Password initialization pwd = BitVecs('pwd0 pwd1 pwd2 pwd3 pwd4 pwd5', 8) # Internal sta
    z3 smt z3py 2017-04-19

    1热度

    1回答

    z3中的相互递归数据类型及其与内置类型的交互

    我目前正在尝试使用Z3为具有多态列表的无类型语言编码简单程序逻辑。 据我所知，从the Z3 tutorial by Moura and Bjorner，不可能“嵌套在其他类型，如数组内的递归数据类型定义”。 因此，假设我有以下OCaml的类型： type value = | Num of float | String of string | List of valu
    logic ocaml z3 smt recursive-datastructures 2017-04-24

    1热度

    1回答

    z3py：如何在z3py中设置使用的逻辑？

    使用下面的代码： import z3 solver = z3.Solver(ctx=z3.Context()) #solver = z3.Solver() Direction = z3.Datatype('Direction') Direction.declare('up') Direction.declare('down') Direction = Direction.creat
    z3 z3py 2017-04-27
最新问题