我正在编写一个python程序,它必须将大型命题公式转换成z3实例。例如,我的程序可以通过
a = my_atomic_proposition("a") # Bool
b = my_atomic_proposition("b", operator.ge, 42) # Real: c >= 42
c = my_atomic_proposition("c") # Bool
f = my_and(a, my_or(b, my_not(c)))
应转换为z3实例g
,即
请记住,我所说的公式大多包含100多个术语。在
跟帖
Z3 with string expressions我首先尝试构建自己的解析器(Leornardo de Moura在帖子中建议的选项1),它只是递归地遍历我所有的公式操作数,并在途中构建了z3实例。{I在上面描述的cd3>中递归地调用strings,速度非常慢。这个解决方案要快得多,但是,当我的公式变得太大(抛出一个MemoryError
)时就不起作用了。在
所以现在我要尝试第三个选项:使用z3.parse_smt2_string
从一个字符串创建z3实例(不是我上面使用的eval
的实例,它必须有不同的语法)。我将以某种方式进行类似于Z3_parse_smtlib_string usage issues中的操作。但是,我想知道我是否会像使用z3.parse_smt2_string
遇到类似的内存问题?从那时起,我可能会在投入太多精力之前寻找另一种方法。在
另外,如果有人对我如何实现我的目标有另一个想法(希望是更聪明的主意),我很乐意发表任何评论。谢谢你的帮助!在
编辑-MemoryError示例:
我将举例说明抛出MemoryError
的一个例子:假设我有以下公式作为字符串:
f = 'z3.Or(a___0,z3.And(True,z3.Or(a___1,z3.And(True,z3.Or(a___2,z3.And(True,z3.Or(a___3,z3.And(True,z3.Or(a___4,z3.And(True,z3.Or(a___5,z3.And(True,z3.Or(a___6,z3.And(True,z3.Or(a___7,z3.And(True,z3.Or(a___8,z3.And(True,z3.Or(a___9,z3.And(True,z3.Or(a___10,z3.And(True,z3.Or(a___11,z3.And(True,z3.Or(a___12,z3.And(True,z3.Or(a___13,z3.And(True,z3.Or(a___14,z3.And(True,z3.Or(a___15,z3.And(True,z3.Or(a___16,z3.And(True,z3.Or(a___17,z3.And(True,z3.Or(a___18,z3.And(True,z3.Or(a___19,z3.And(True,z3.Or(a___20,z3.And(True,z3.Or(a___21,z3.And(True,z3.Or(a___22,z3.And(True,z3.Or(a___23,z3.And(True,z3.Or(a___24,z3.And(True,z3.Or(a___25,z3.And(True,z3.Or(a___26,z3.And(True,z3.Or(a___27,z3.And(True,z3.Or(a___28,z3.And(True,z3.Or(a___29,z3.And(True,z3.Or(a___30,z3.And(True,z3.Or(a___31,z3.And(True,z3.Or(a___32,z3.And(True,z3.Or(a___33,z3.And(True,z3.Or(a___34,z3.And(True,z3.Or(a___35,z3.And(True,z3.Or(a___36,z3.And(True,z3.Or(a___37,z3.And(True,z3.Or(a___38,z3.And(True,z3.Or(a___39,z3.And(True,z3.Or(a___40,z3.And(True,z3.Or(a___41,z3.And(True,z3.Or(a___42,z3.And(True,z3.Or(a___43,z3.And(True,z3.Or(a___44,z3.And(True,z3.Or(a___45,z3.And(True,z3.Or(a___46,z3.And(True,z3.Or(a___47,z3.And(True,z3.Or(a___48,z3.And(True,z3.Or(a___49,z3.And(True,a___50))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))'
以及以下表示f
变量的字符串列表:
variables = ['a___2', 'a___31', 'a___34', 'a___46', 'a___29', 'a___12', 'a___9', 'a___32', 'a___41', 'a___24', 'a___38', 'a___23', 'a___19', 'a___50', 'a___3', 'a___6', 'a___35', 'a___28', 'a___13', 'a___16', 'a___0', 'a___33', 'a___36', 'a___40', 'a___45', 'a___10', 'a___39', 'a___43', 'a___22', 'a___27', 'a___7', 'a___49', 'a___21', 'a___17', 'a___1', 'a___4', 'a___37', 'a___44', 'a___11', 'a___14', 'a___30', 'a___42', 'a___47', 'a___8', 'a___26', 'a___48', 'a___20', 'a___25', 'a___5', 'a___15', 'a___18']
然后我按如下方式使用eval
:
# Declare z3 variables for all strings in my list 'variables'
for x in variables:
globals()[x] = z3.Bool(x)
# Create z3 object from string 'f'
z3f = eval(f)
并收到错误:
---------------------------------------------------------------------------
MemoryError Traceback (most recent call last)
<ipython-input-71-b7421db475e5> in <module>()
3 globals()[x] = z3.Bool(x)
4 # Create z3 object from string 'f'
----> 5 z3f = eval(f)
MemoryError:
对于类似但较短的f
,上面的代码可以正常工作。例如:
f = 'z3.Or(a___0,z3.And(True,z3.Or(a___1,z3.And(True,z3.Or(a___2,z3.And(True,z3.Or(a___3,z3.And(True,z3.Or(a___4,z3.And(True,z3.Or(a___5,z3.And(True,z3.Or(a___6,z3.And(True,z3.Or(a___7,z3.And(True,z3.Or(a___8,z3.And(True,z3.Or(a___9,z3.And(True,z3.Or(a___10,z3.And(True,z3.Or(a___11,z3.And(True,z3.Or(a___12,z3.And(True,z3.Or(a___13,z3.And(True,z3.Or(a___14,z3.And(True,z3.Or(a___15,z3.And(True,z3.Or(a___16,z3.And(True,z3.Or(a___17,z3.And(True,z3.Or(a___18,z3.And(True,z3.Or(a___19,z3.And(True,z3.Or(a___20,z3.And(True,z3.Or(a___21,z3.And(True,z3.Or(a___22,z3.And(True,z3.Or(a___23,z3.And(True,z3.Or(a___24,z3.And(True,z3.Or(a___25,z3.And(True,z3.Or(a___26,z3.And(True,z3.Or(a___27,z3.And(True,z3.Or(a___28,z3.And(True,z3.Or(a___29,z3.And(True,z3.Or(a___30,z3.And(True,z3.Or(a___31,z3.And(True,z3.Or(a___32,z3.And(True,z3.Or(a___33,z3.And(True,z3.Or(a___34,z3.And(True,z3.Or(a___35,z3.And(True,z3.Or(a___36,z3.And(True,z3.Or(a___37,z3.And(True,z3.Or(a___38,z3.And(True,z3.Or(a___39,z3.And(True,a___40))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))'
variables = ['a___2', 'a___31', 'a___34', 'a___29', 'a___12', 'a___9', 'a___32', 'a___24', 'a___38', 'a___23', 'a___19', 'a___3', 'a___6', 'a___35', 'a___28', 'a___13', 'a___16', 'a___0', 'a___33', 'a___36', 'a___40', 'a___10', 'a___39', 'a___22', 'a___27', 'a___7', 'a___21', 'a___17', 'a___1', 'a___4', 'a___37', 'a___11', 'a___14', 'a___30', 'a___8', 'a___26', 'a___20', 'a___25', 'a___5', 'a___15', 'a___18']
我收到:
z3f = Or(a___0,
And(True,
Or(a___1,
And(True,
Or(a___2,
And(True,
Or(a___3,
And(True,
Or(a___4,
And(True,
Or(a___5,
And(True,
Or(a___6,
And(True,
Or(a___7,
And(True,
Or(a___8,
And(True,
Or(a___9,
And(True,
Or(..., ...)))))))))))))))))))))
感谢您添加ec-m示例!在
这实际上是Python方面的一个问题。Python非常保守地限制了
eval(...)
的堆栈,显然在某些版本中它只能处理35个作用域(如Parser crashes for deeply nested list displays中所述)。深度嵌套lambda也存在类似的问题(请参见Python: nested lambdas — s_push: parser stack overflow Memory Error)。在通过切换到Z3的
parse_smt2_string
,可以避免这种类型的问题,这允许更大的堆栈。在相关问题 更多 >
编程相关推荐