问题标签 [quantifiers]

如何显示量词消除的结果？
z3 似乎对以下输入感到满意

但它返回的结果与输出相同。

谢谢

我有 asp.net 应用程序，其中以以下方式创建字符串。

我知道原因是因为 *, +, ?, {num, num} 是“贪婪的量词”

但是有没有办法使用相同的字符串创建正则表达式，或者是否可以用其他字符替换这些贪婪的量词？

我不想改变我的字符串。

最小示例代码：

这是我要完成的工作的一些背景知识： IntegralAsType 通过防止将两个具有不同模数的数字相加来确保编译时的类型安全。ZqBasic 是 Zq 类型的内部表示，还有其他类型，这就是 Zq 被这样定义的原因。目标是获得一个对内部表示透明的系统。

我的问题是 changeBase 函数。我在'p'类型上使用了显式forall，但我仍然得到一个“由于使用值而产生的约束中的模糊类型变量a0（IntegralAsType a0）”

我对为什么会收到此错误感到困惑。特别是在上一篇文章中，我得到了类似“zqBasic”函数的帮助，它似乎与 changeBase 函数具有相同的设置。我通过添加显式量词“forall qa”修复了 zqBasic 中的模棱两可的变量错误。如果没有这个量词，我会得到一个模棱两可的类型变量错误。我明白为什么我需要量词，但我不明白为什么它似乎对 changeBase 没有帮助。

谢谢

(∀u∃va(u,v)) ∧ (∀x∃ya(x,y)) 的 skolemized 形式是什么？

我不确定，因为可能有不同的 perenex 范式：

• ∀u∃v ∀x∃y (a(u,v) ∧ a(x,y))
• ∀u∀x ∃v∃y (a(u,v) ∧ a(x,y))
• …</li>

会有不同的 skolemized 形式如下：

• ∀u ∀x (a(u,f(u)) ∧ a(x,g(u,x)))
• ∀u∀x (a(u,f(u,x)) ∧ a(x,g(u,x)))

在我看来，它们并不等同于彼此。还是我在这里错了？

正则表达式有问题吗？Firebug 只是说“无效的量词”。就是这样，没有更多的信息。

输入可以是 1. 或 2. 或两者的组合。

1. 顺序的

我为此使用的正则表达式是 (startLoop.+?endLoop)+? 将每个循环块作为我的匹配器组。这适用于我每次访问 setSomething 并更改它的顺序情况。

1. 嵌套

我写了类似 (startLoop.+?startLoop)+? 但这只能让我访问 setSomething1.1

我无法想出一个正则表达式来让我访问 setSomething 无论输入具有什么类型的循环结构。

感谢你的帮助。

我有以下 javascript 代码：

我invalid quantifier在/?rows.*?.... 使用测试字符串在http://www.pagecolumn.com/tool/regtest.htm上测试时，同样的正则表达式有效

?srt=acc_pay&showfileCL=yes&shownotaryCL=yes&showclientCL=no&showborrowerCL=yes&shownotaryStatusCL=yes&showclientStatusCL=yes&showbillCL=yes&showfeeCL=yes&showtotalCL=yes&dir=asc&closureDate=12/01/2011&closureDate2=12/31/2011&sort=notarystart&='tablename&=' 'xyz'）

在这个字符串中，上面的正则表达式应该匹配：

行=任何东西

实际上我什/?至不需要让它工作，但如果我不把它放到我的javascript中，它就像它甚至不是正则表达式......我对正则表达式时期很糟糕，所以这个让我很漂亮使困惑。这个错误是我在 Firefox 的错误控制台中得到的唯一一个错误。

编辑

使用我在上面发布的链接，似乎前导/尝试匹配实际的正斜杠，而不是仅仅将代码标记为正则表达式语句的开头。所以?它在那里，所以如果它与任何东西都不匹配/，它仍然会继续。

解析度

好的，所以最后，我不得不将我的正则表达式更改为：

/rows=.*(?=\&?)/g

这匹配了单词“rows=”，后跟任何内容，直到它碰到一个＆符号或文本用完。

我不明白这种行为。我有这样的例子，需要捕捉 html 评论。

第二个正则表达式regex2工作正常，准确输出所需内容。首秀null。而且我不明白其中的区别。正则表达式<!--[.]*-->和<!--.*-->含义相同 - “在<!--将除换行符之外的任何字符从 0 到尽可能多并以-->”结尾之后。但是对于第二个它有效，而对于第一个则无效。为什么？

UPD。我已阅读评论并有更新。

所以可以使用有限的匹配变量来匹配任何东西。那么应该使用哪种方式正确使用 RegExps 呢？有[]没有他们？无法区分，两者都给出正确的输出。

我正在尝试使用具有特定量词的字符类创建一个正则表达式，该量词是一个变量，例如：

这工作如下（没有变量）：

但是，它与带引号的模式而不是斜线分隔的模式没有相同的功能，如下所示：

编辑：为了更清楚，我添加了一个摘要问题，该问题在下面得到了回答： 如何使用带引号的字符串的插值变量创建正则表达式？

虽然我更喜欢使用插值，但它似乎不可用（至少在这种情况下），也没有必要。

我还尝试想出一种方法来连接/加入一些正则表达式文字以达到相同的结果，但对于这个用例却无法这样做。

作为旁注 - 我熟悉 perl 中的这种类型的正则表达式：

可以如下使用：

根据提供的建议/答案，我创建了一个示例货币字符串原型，如下所示：