z3 - 优文库

z3

0热度

1回答

我不知道什么是最好的方式来一笔转换文件或类似产品成为SMT-lib2表达式，专门用于解决与Z3（或甚至metitarski）。我认为会有一个量词的显而易见的方法，但我在创建它时遇到了麻烦，并且在许多使用情况下，这样的总和可能具有exprLB和exprUB的常量，这意味着我希望某种策略会简单地将其展开成为一个长长的添加序列，使用量词可能会使这变得更加困难。例如，一个相当微不足道的战术转换成

3热度

1回答

SMT解决方案与自定义理论？

我在做一些验证工作，我已经将常规树语法作为基础理论。 Z3允许您定义自己的东西与未解释的函数，但是，如果您的决策过程是递归的，那么这种方法并不适用。他们曾经允许使用插件，但我认为这已经被删除了。我想知道，有没有人有一个体面的SMT解决方案的建议，让你写定制理论的决策程序？

1热度

1回答

解析和存储表达式涉及数组

我有两个整数算术表达式涉及文件中的数组。将每个表达式存储到内存中的最佳方式是什么？因此等价公式在语法上等价。比较那里的结构我们可以找到等价。要检查等价性，首先比较那里的结构，如果它们相同，那么它们是等价的，否则使用SMT解算器。 Ex。 a [i + 2] +5和a [i + 3-1] + 4 + 1是等价的。现在我代表一个[i] = b [i] + z就如同wr（a，i，rd（b，i）+ z）

2热度

1回答

Z3PY方程，大小限制

我的工作Z3PY我想知道如何限制一个公式的计算规模 v0 = Int('v0') const = 0x12345678 I wrote this : s.add((const*(v0 + const*(func(v0*const) - v0)) - v0) == somevalueof64bits) 我的问题是，“（常量*（V0计算+ const *（func（v0 *

2热度

1回答

如何从Eclipse插件链接Z3 build，编译为Java？

我有一个完美的适用于Java的Z3构建系统。我想从Eclipse插件中调用它。我尝试了几种方法，但其中没有一种为我工作。这些方法是：添加Z3建立作为外部类文件夹 How to Use External Class Files in an Eclipse Project Exception in thread "main" java.lang.UnsatisfiedLinkError: no li

3热度

2回答

Z3 Prover返回错误的解决方案

我试图用Python中的Z3 Thoerem Prover解决方程。但我得到的解决方案是错误的。 from z3 import * solv = Solver() x = Int("x") y = Int("y") z = Int("z") s = Solver() s.add(x/(y+z)+y/(x+z)+z/(x+y)==10, x>0, y>0, z>0) s.add()

2热度

1回答

Z3和浮点系数

我是用一个小的多目标整数规划问题，玩的解释：在Z3（使用Python绑定），我们可以很优雅地说明这一点： from z3 import * x1,x2 = Ints('x1 x2') z1,z2 = Reals('z1 z2') opt = Optimize() opt.set(priority='pareto') opt.add(x1 >= 0, x2 >=0, x1 <= 2,

2热度

1回答

Z3中的部分定义

我试图在Z3中定义成对关系（在下面的代码中称为C）（使用数组定义）之间的parthood关系。我写了3个断言来定义反身性，传递性和反对称性，但Z3返回“未知”，我不明白为什么。 (define-sort Set() (Array Int Bool)) (declare-rel C (Set Set)) ; reflexivity (assert (forall ((X Set)) (C

1热度

1回答

无法为z3py提取Z3 EnumSort的值

我正在尝试将问题编码到Z3中，并且我希望为“三态”布尔值（即，带有true,false和unknown的布尔值）建模。这里是我怎么也仿照它： #!/usr/bin/env python import z3 from collections import OrderedDict TristateValues = ["True", "False", "Unknown"] Tristate

2热度

1回答

Equalvalent数组存储记录

一个数组可以存储一个新的值，并在这样做返回一个新的数组。我知道我可以使用MkApp函数来访问记录的选择器，然后如何替换记录的值？我使用的是.NET绑定，但随着问题的例子，这里是一些SMT： (declare-datatypes (T1 T2) ((Pair (mk-pair (first T1) (second T2))))) (declare-const p1 (Pair Int Int))