问题标签 [quantifiers]

I'm experimenting with quantifier elimination tactic for formulas of enumerated types. I'd like to know if there are any ways of increasing the performance by adjusting the solver somehow. After a brief glance over the source code I concluded that there seem to be different strategies for quantifier elimination (e.g. qe_lite.cpp), but they are not exposed as parameters of the qe tactic. In my case formulas have a simple propositional structure, sometimes quantified variables even don't occur in the formula, but the procedure can be called several thousands of times. So I guess, my questions are the following:

1. Does Z3 have some sort of caching for quantifier elimination (application mode?), that would allow to process a bunch of similar or identical formulas faster?
2. Can I guide Z3 to use different approaches for quantifier elimination on finite domain formulas, so I can see which one works better for me?
3. It would be interesting to know which approach is generally used in Z3 to eliminate quantifiers for formulas over finite domain types. Is it performed just by a substitution + simplification, or some more elaborate techniques are used?

Thank you.

来自 GLib 参考手册，“正则表达式语法”部分，“原子分组和所有格量词”小节：

考虑\d+foo应用于字符串时的模式123456bar：在匹配所有 6 位数字然后未能匹配“foo”之后，匹配器的正常操作是再次尝试仅匹配 \d+ 项目的 5 位数字，然后再匹配 4，依此类推在最终失败之前。

如果我们在前面的示例中使用(?>\d+)foo（称为原子分组），匹配器会在第一次未能匹配“foo”时立即放弃。

当原子组的子模式只是单个重复项时，如上例所示，可以使用更简单的表示法，称为“占有量词”：\d++foo

我的问题是：有什么理由为什么没有星号（*）重复运算符的等价物？

Java 中的示例：

异常堆栈跟踪是：

我必须用几行搜索许多文件，这些行的电话号码正好是十位数。行示例：

所以我期待这些线路：

我正在使用下一个 grep 指令进行搜索：

grep '^telephoneNumber: [0-9]\{10\}$' file.txt

它在 Ubuntu、OpenSuse 和 Cygwin 中运行良好，但是当我在 Solaris 中运行它时，它不匹配，如果删除$模式末尾的"

有什么建议么？

是否可以将量词与组一起使用？

例如。我想匹配类似的东西：

• 11%
• 09%
• %
• %
• g1%
• 8b% ...

模式是：2个字母或数字（混合或不混合）和一个以%结尾的字符串...

我知道，这个例子没有太多意义。一个简单的 [list]{m,n} 可以解决这个问题。尽可能简单地得到答案。

鉴于：

命令行表达式是：

结果是什么？

SCJP 书对正则表达式、模式和匹配器的解释非常可怕，令人难以置信。无论如何，我非常了解大部分基础知识，并查看了有关贪婪和不情愿量词的 Sun/Oracle 文档。我理解这些概念，但对一些事情感到模糊：

“贪婪”量词的物理符号究竟是什么？它只是一个*，吗？或 + ？如果是这样，有人可以根据这本书详细解释这个答案是如何变成 E 的吗？当我自己运行它时，我得到了答案：2334！

在这里我们会使用一个贪婪的量词对吗？这将消耗整个字符串，然后回溯并连续查找零个或多个数字。因此，如果贪心，“完整字符串”将连续包含 2 个数字，并且根据该定义仅执行 .find() 一次（即 m.start = 0 ， m.group = "ab34ef"）！

谢谢你们的帮助。

我正在阅读 K.Sierra 并发现以下句子：

贪心量词实际上确实读取了整个源数据，然后它向后（从右边）工作，直到找到最右边的匹配。此时，它包括从源数据中较早的所有内容，直到并包括作为最右边匹配的一部分的数据。

现在，假设我们有如下来源：

和模式：proj1([^,])*

为什么它与整个文本不匹配？贪婪它应该匹配最右边的“proj1.java”并且返回的匹配应该是最右边匹配之前的整个源？相反，它返回：

鉴于此正则表达式：

以及用于匹配的输入字符串：

结果是xbbbx从索引 0 开始到索引 5 结束的匹配文本。

但是，只需更改最后一个字母xZ但是，通过仅将正则表达式和字符串中，我们得到这个正则表达式：

和这个输入字符串：

结果是：找不到匹配项。

为什么单个字母的变化会导致这种行为变化？

我最近一直在研究正则表达式，并发现该?运算符使*, +, 或?惰性。我的问题是它是如何做到的？*?例如是一个特殊的运算符，还是对?有影响*？换句话说，正则表达式*?本身是否识别为一个运算符，或者正则表达式是否识别*?为两个单独的运算符*和?？如果*?是被识别为两个独立的运营商的情况，这对使其变得懒惰有什么?影响。*如果?意味着 the*是可选的，这不应该意味着*根本不需要存在。如果是这样，那么在声明中.*?正则表达式不会只匹配单独的字母和整个字符串而不是较短的字符串吗？请解释一下，我很想了解。非常感谢。

I'm looking to make a regex with an operator that applies to a whole word. For example, I want the word hello to be optional. Instead of having h?e?l?l?o?, I am wondering if it is possible to write something like (hello)?*.

*Note that (hello)? does not work for my case since I do not want hello to be returned in the matches.

我刚刚在http://regexcrossword.com/上做了有趣的正则表达式填字游戏- 发现我不明白量化组的含义，例如 (.)+ 或 (.)*

让我试试http://ole.michelsen.dk/tools/regex.html，它提供了 JavaScript 和 PHP 正则表达式引擎：

要匹配的字符串是“Trololo！” （不带引号）。（如果打开“全局匹配”改变了某些东西，它会作为初始版本添加，即 JS'，因为它在 PHP 模式下没有改变任何东西。）

有什么规范的答案吗？这是什么语义？