我尝试使用pyparsing来解析这些逻辑表达式
x
FALSE
NOT x
(x + y <= 5) AND (y >= 10) OR NOT (z < 100 OR w)
(A=True OR NOT (G < 8) => S = J) => ((P = A) AND not (P = 1) AND (B = O)) => (S = T)
((P = T) AND NOT (K =J) AND (B = F)) => (S = O) AND
((P = T) OR (k and b => (8 + z <= 10)) AND NOT (a …鉴于这x,y,z = Ints('x y z') 和字符串一样s='x + y + 2*z = 5',是否有快速方法将s转换为z3表达式？如果它不可能那么似乎我必须做很多字符串操作来进行转换.
每当我org-plot/gnuplot在emacs org-mode中调用该命令时,我都会收到同样的错误Error running timer: (void-variable data-file).我在Debian Jessie中使用emacs 24.4.1以及在Mac Os上使用emacs 24.5.两个系统都有一个gnuplot的工作版本.我甚至在运行没有.emacs文件的emacs时尝试此命令,但仍然会收到同样的错误.
只是想知道z3py,我如何检查给定的常量表达式是变量还是值？例如
x = Int('x')
x_ = IntVal(7)
ColorVal, (White,Black) = EnumSort("ColorVal",["While","Black"])
mycolor = Const("mycolor",ColorVal)
所以x,mycolor都是变量而x_,True,False,White,Black都是值而不是变量.
z3py有is_var谓词,但出于不同的目的.如果我想将公式中的所有变量重命名为其他变量,这将非常有用.
在 Z3 Python 中，1)x = Const("x",IntSort()) 与 2)之间的区别是什么 x = Int("x") ？is_const 对两者都返回 true，并且它们都是 ArithRef。我认为 1) 适合定义一个常量，例如，x 是 3.14 和 2) 是创建一个变量。
是否有正确的方法来创建像 x = 3.14 这样的 const 变量（除了生成公式 x == 3.14）
如何检索枚举变量的值v ？例如，
vTyp, (val1,val2,val3) = EnumSort('vTyp',['val1','val2','val3'])
v = Const('my variable',vTyp)
现在，由于只是上面的变量v，我将如何检索值的列表 [val1,val2,val3]中v（这里val1,val3,val3是表达如上）？
我试过了，[v.sort().constructor(0), ...(1), ...(2)] 但是构造方法没有返回表达式。
我知道Z3对非线性算法有一些支持但是想知道扩展了什么？是否可以指定支持哪些类型的非线性算法,哪些不是(或者可能给予超时)？知道这些进展将帮助我尽早完成我的任务.
似乎不支持与电源相关的东西,如下所示
def pow2(x):
k=Int('k')
return Exists(k, And(k>=0,2**k==x))
prove(pow2(7))
failed to prove
即使使用 后，输出一组数字也不会给出相同的序列random.seed(myseed)。这只发生在 Python3 中，而不是 Python2 中（两者都在 Debian 稳定系统上）。这是一个错误还是我的代码有问题？
import random
seed=20.0
random.seed(seed)
print("seed: {}".format(seed))
test = [str(random.randint(0,1000)) for _ in range(10)]
print(', '.join(test))
ss = set(test)
print(', '.join(ss))
下面Python3 在每次运行时给出了不同的序列，但Python2 在所有运行中给出了相似的序列（如预期）。
$ python3 --version
Python 3.4.2
$ python2 --version
Python 2.7.9
#same sequences
$ python2 randtest.py
seed: 20.0
906, 686, 767, 905, 260, 636, 905, 873, 573, 169
906, 636, 905, 573, 767, 873, 260, 169, 686
$ python2 randtest.py
seed: 20.0
906, 686, 767, 905, …