问题标签 [quantifiers]

量词的x?意思a single or no occurance of x。

为了方便起见，我发布了一个test harness用于将正则表达式与字符串匹配的内容。

a?与 string 相比，我对 regex 感到困惑ababaaaab。

程序的输出是：

我对b的感到困惑。

“正则表达式 a? 不是专门寻找字母“b”；它只是寻找字母“a”的存在（或不存在）。如果量词允许匹配“a”零次，那么任何在不是“a”的输入字符串中将显示为零长度匹配。”

参考

问题：-

第一行是可以理解的，我确实理解存在 b 或任何非 a 是不存在 a 或 0 出现 a，因此应该导致匹配。但是在索引1和2之间没有a（即b的出现）。那么为什么索引1和1之间的文本“”匹配（换句话说，为什么我们得到一个零长度在这里匹配）。根据我的推理，它应该在索引 1 和 2 之间。

量词a?应该匹配a single or no occurrence of a。给定的程序使用java.util.regex包将正则表达式与字符串匹配。

我的问题是关于模式匹配的程序/结果的输出：

程序的输出：-

Enter your regex: a? Enter input string to search: a I found the text "a" starting at index 0 and ending at index 1. I found the text "" starting at index 1 and ending at index 1.

问题：-

它应该匹配一个或零个出现的 a。那么它不应该匹配 a zero-length ""（即缺席/零次出现a）starting and ending at index 0，然后匹配a starting at index 0and ending at index 0，然后匹配 a"" starting and ending at index 1吗？我认为应该。

这样，似乎matcher一直在寻找a'sthough-out 字符串，然后当确定没有更多a's （那是end字符串的？）时，它会寻找zero occurrence/ 不存在a? 我认为这会很乏味，而且情况并非如此。但是它应该在匹配开始于和结束于starting and ending at 0之前找到一个“” ？index 0index 1

程序：-

我正在尝试匹配分号之前的数字，但我不能在我的后视中使用量词，所以我不知道如何使这项工作。

字符串（是的，“item[##]”和“=”之间有制表符空格）

我想要 13、13、7 和 2

这是我当前的正则表达式，显然不起作用：

如果出现 3 次或更多，我需要替换最后一个斜杠。如果我们有这样的路径"/foo/bar/"，它应该变成"/foo/bar". "/foo/"但是不应该触及这样的路径。

我用转义的斜杠 ( \/) 和量词 ( {3,}) 进行了尝试：

然而，这个正则表达式只匹配紧跟在另一个之后的斜杠："/foo/bar///"

有什么想法可以解决这个问题吗？也许有正面/负面lookahead的？

http://www.regexr.com/393pm

可视化：

感谢Fede、Avinash Raj和Amal Murali！由于性能很重要，@Fede 是赢家：http: //jsperf.com/match-last-slash-if-there-are-at-least-nth-occurrences

为什么当我将 2 和 4 放在括号中时，此函数在连字符前取 3 位，在连字符后取 5 位？请帮助..

Java教程中有正则表达式量词的示例和描述。

贪婪 - 吃完完整的字符串，然后退后一个字符，然后再试一次

不情愿 - 从头开始​​，然后一次吃一个角色

占有 - 吃掉整个字符串，尝试一次匹配

他们没问题，我理解他们，但是有人可以向我解释当正则表达式更改为字符类时会发生什么？还有其他规则吗？

我正在为 Python 开发一个抽象代数库，当我意识到很多肮脏的工作只是构造循环以对应于带有量词的逻辑表达式。然后我意识到，虽然在 Python 中实现逻辑量化函数可能很困难，但在 Haskell 或其他语言中会更容易。

现在我有量词，只要属性只涉及一个被量化的变量，并且只有当你量化的关系具有三个变量时，克服这些障碍似乎是困难的部分。

例如，该语句∀x ∃y (x < y)会导致问题，但没问题∀x (x = 2) ∃y (y < 3)。

是否有任何现有的 Haskell 库可以实现这样的值级逻辑量词？很难搜索，因为每当我按照“逻辑量词 Haskell”进行搜索时，我都会得到很多关于类型量词的东西，这不是我想要的。

我唯一能找到的是一个forAllin Test.QuickCheck，这并不带有“存在”。

我有以下 Z3 超时的简单示例：

现在，如果我们简化断言，传播相等性，z3 立即返回 UNSAT（如预期的那样）：

这个例子似乎表明 Z3 不会在量词下传播等式。例如，以下断言有效（产生 UNSAT）：

有什么方法可以让 z3 传播等式，或者选择另一种使用该等式的搜索策略？

考虑以下 SMT-LIB 代码：

试图断言公理bar成立，即

失败（Z3 4.3.2 - 构建哈希码 47ac5c06333b）：

问题 1：为什么 Z3 只实例化limited-G但不limited-F实例化bar（这将证明断言）？

问题 2：评论任何（无用的）断言foo，limited-F或limited-G允许 Z3 证明断言 - 为什么会这样？（取决于注释的内容，仅bar或bar和limited-F被实例化。）

如果它与观察到的行为有关：我想设置smt.case_split为3（我的配置遵循 MSR 的Boogie工具省略的配置），但 Z3 给了我WARNING: auto configuration (option AUTO_CONFIG) must be disabled to use option CASE_SPLIT=3, 4 or 5，尽管(set-option :auto_config false).

假设我在上下文中有一个假设H : forall ( x : X ), P x和一个变量。x : X我想执行通用实例化并获得一个新的假设H' : P x。做到这一点最无痛的方法是什么？显然apply H in x不起作用。assert ( P x )其次是apply Hdoes，但如果P很复杂，它会变得非常混乱。

有一个类似的问题似乎有些相关。不过，不确定它是否可以在这里应用。