Z3检查python字符串可满足性 [英] Z3 check python string satisfiability

问题描述

有没有办法检查像'p或p这样的python字符串的可满足性->如果您事先不知道变量名称，则 Z3 中的 p' ?例如我见过这个:

Is there a way to check satisfiability of a python string like 'p or p -> p' in Z3 if you do not know the variable names before hand? For example I have seen this:

p = Bool('p')
solve(Implies(Or(p, p), p))

但是我无法提前定义 Z3 中的变量，因为该命题是作为字符串提供给我的.我怎样才能用 z3 做到这一点?

However I cannot define the variables in Z3 in advance because the proposition is given to me as a string. How can I do this with z3?

我也看过 python 的 eval 函数，但似乎我也需要在之前的 z3 中定义变量名

I have also seen python's eval function but it seems I need to have the variable names defined in z3 of that prior too

推荐答案

一些需要思考的问题:该字符串的含义是什么?如果它有语法错误怎么办?你如何辨别什么是有效的运算符/变量?您是否只允许布尔值或其他类型?运算符的分组、优先级和结合性如何?

Some questions to ponder: What would be the meaning of that string? What if it has syntax-errors in it? How do you discern what are the valid operators/variables? Do you allow just booleans, or other sorts as well? What about grouping, precedence, and associativity of operators?

归根结底，如果你想直接从一个字符串开始，你真的别无选择，只能同意这些字符串含义的语法和语义.唯一的方法是为这些字符串编写一个解析器，然后解释"字符串.这导致了 z3 上下文.

Bottom line, if you want to go directly from a string, you really have no choice but to agree on a syntax and a semantics of what those strings mean. And the only way to do that is to write a parser for those strings, and "interpret" that result in the z3 context.

一种选择是坚持"到 SMTLib，即要求您的输入是格式正确的 SMTLib 脚本.如果您选择此选项，那么 z3 已经为它们提供了一个可以轻松使用的内置解析器.请参阅此处:https://z3prover.github.io/api/html/namespacez3py.html#a09fe122cbfbc6d3fa30a79850b2a2414 但我很确定你会发现这很丑陋而且不是你想要的.但这是唯一的开箱即用"解决方案.

One choice is to "stick" to SMTLib, i.e., ask your input to be well-formatted SMTLib scripts. If you go with this choice, then z3 already have a built-in parser for them that you can readily use. See here: https://z3prover.github.io/api/html/namespacez3py.html#a09fe122cbfbc6d3fa30a79850b2a2414 But I'm pretty sure you'll find this rather ugly and not quite what you wanted. But this is the only "out-of-the-box" solution.

处理这个问题的正确方法是编写一个基于布尔表达式的基本解析器，其语法(以及某种程度上的语义)你可以自由定义你想要的任何方式.此外，这并不是一件特别困难的事情.如果您在 Python 中执行此操作，则可以使用 ply (https://www.dabeaz.com/ply/)，或者使用手写的递归下降解析器(https://www.booleanworld.com/building-recursive-descent-parsers-definitive-guide/).

The proper way to handle this issue is to write a basic parser over boolean-expressions, whose syntax (and to some extent semantics) you'll have freedom to define however way you want. Also, this isn't a particularly difficult thing to do. If you're doing this in Python, you can use ply (https://www.dabeaz.com/ply/), or go with a hand-written recursive-descent parser (https://www.booleanworld.com/building-recursive-descent-parsers-definitive-guide/).

随意探索并提出更多问题；如果是关于在 Python 中解析字符串，请确保适当地标记它们；与 z3/z3py 真的无关.

Feel free to explore and ask further questions; though make sure to tag them appropriately if it's about parsing strings in Python; which really have nothing to do with z3/z3py.

这篇关于Z3检查python字符串可满足性的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！