Описание тега quantifiers
В логике количественная оценка - это привязка переменной в пределах домена. Таким образом, переменная становится связанной оператором, называемым квантификатором.
2
ответа
Понимание квантификаторов
Я изучал Java Tutorial по квантификаторам. Существует различие, упомянутое среди различий между жадными, неохотными и притяжательными квантификаторами. Я не могу понять, в чем именно разница. Объяснение предоставляется следующим образом: Enter your …
31 янв '17 в 11:41
1
ответ
Квантификаторы и классы символов
Есть примеры и описания квантификаторов регулярных выражений в Java Tutorial. Жадный - съедает полную строку, затем отступает на один символ и пытается снова Regex: .*foo // greedy String to search: xfooxxxxxxfoo Found "xfooxxxxxxfoo" Неохотно - нач…
07 авг '14 в 19:44
1
ответ
Лучший способ создания экземпляра вложенного экзистенциального оператора в Coq
Предположим, у меня есть вложенное экзистенциальное утверждение H : exists ( a : A ) ( b : B ) ( c : C ) ... ( z : Z ), P a b c ... z в контексте. Как лучше всего создать экземпляр H и получить новую гипотезу H' : P a b c ... z? Делая это путем повт…
10 сен '14 в 08:06
0
ответов
Переписать код в Z3 с квантификаторами
Парни Я пишу модель, используя Microsft Z3, и мне нужно добавить следующие утверждения: (declare-const line (Array Int Int)) (assert (and (> (select line 1) 0) (< (select line 1) 4))) (assert (and (> (select line 2) 0) (< (select line 2)…
07 апр '13 в 22:45
0
ответов
Создание "имени пользователя" с использованием квантификаторов JavaScript?
Я только начинаю изучать Javascript. Теперь на мой вопрос. Я думаю, что это связано с квантификаторами, но я не уверен. Я должен написать регулярное выражение, которое будет соответствовать одному "имени пользователя" со следующими атрибутами: Должн…
03 ноя '16 в 17:52
1
ответ
Исключение квантификаторов z3 в синтаксисе SMTLIB
У меня есть следующий пример устранения квантификаторов с использованием z3py ниже. Однако я хотел бы переписать его с использованием синтаксиса SMTLIB (код ниже кода Python). Каким-то образом я не получил такой же вывод, как то, что я получил от Py…
06 июн '17 в 02:03
1
ответ
Разница между `Z3_mk_forall` и`Z3_mk_forall_const` в C API для Z3?
Я смущен 2 функциями. Кажется, что они принимают примерно один и тот же набор аргументов (один напрямую преобразуется в другой), и каждый возвращает AST. Функции делают то же самое? Если нет, то когда мне каждый нужен? Подписи 2: Z3_ast Z3_mk_forall…
23 июл '16 в 04:34
2
ответа
Как я могу получить доступ к буферам захвата в скобках с квантификаторами?
Как я могу получить доступ к буферам захвата в скобках с квантификаторами? #!/usr/local/bin/perl use warnings; use 5.014; my $string = '12 34 56 78 90'; say $string =~ s/(?:(\S+)\s){2}/$1,$2,/r; # Use of uninitialized value $2 in concatenation (.) o…
08 июл '11 в 11:48
1
ответ
Как точно определить и работать с жадными или неохотными квантификаторами?
Дано: import java.util.regex.*; class Regex2 { public static void main (String args[]) { Pattern p = Pattern.compile(args[0]); Matcher m = p.matcher (args [1]); boolean b = false; while (m. find()) { System.out.print(m.start() + m.group()); } } } вы…
04 июн '13 в 09:49
2
ответа
Как использовать Z3 в формулах с квантификаторами над множествами?
У меня есть простые формулы с квантификаторами над наборами массивов, Z3(4.3.2) возвращает "неизвестно". (assert (forall ((a (Array Int Int)) (b (Array Int Int))) (=> (forall ((i Int)) (= (select a i) (select b i))) (= a b)))) (check-sat) Подробн…
08 окт '13 в 10:35
6
ответов
Perl REGEX Вопрос
Как программист PHP, плохо знакомый с Perl, работающий через 'Программирование на Perl', я натолкнулся на следующее регулярное выражение: /^(.*?): (.*)$/; Это регулярное выражение предназначено для анализа заголовка письма и вставки его в хеш. Загол…
19 май '11 в 17:38
3
ответа
Как выразить это предложение с помощью квантификаторов и логических операторов
Вот предложение: Есть самый короткий человек, но нет самого высокого человека.
21 сен '15 в 14:10
3
ответа
Два жадных квантификатора в одном и том же регулярном выражении
Если у меня есть неизвестная строка структуры: "stuff I don't care about THING different stuff I don't care about THING ... THING even more stuff I don't care about THING stuff I care about" Я хочу запечатлеть "вещи, которые меня волнуют", которые в…
24 июл '18 в 21:18
1
ответ
Показать, какие шаблоны Z3 выводит для квантификаторов
Я хотел бы посмотреть, какие шаблоны Z3 использует для некоторых квантификаторов в моих формулах. Этот комментарий предполагает, что это возможно, но я не смог найти больше деталей. Как мне заставить Z3 распечатать эту информацию?
24 авг '17 в 16:10
2
ответа
Как запомнить количественные выражения регулярных выражений?
У меня проблемы с запоминанием количественных показателей, т.е. я знаю, что они все значат, но есть ли у кого-нибудь простой способ вспомнить, какой из них обозначает какой? ? The question mark indicates there is zero or one of the preceding element…
23 фев '14 в 01:25
2
ответа
Группы и квантификаторы {m,n}
Можно ли использовать квантификаторы с группами? Например. Я хочу сопоставить что-то вроде: 11% 09% аа% з.ы.% g1% 8b%... Шаблон: 2 буквы или цифры (смешанные или нет) и%, заканчивающийся строкой... <?php echo preg_match('~^([a-z]+[0-9]+){2}%$~', …
23 май '13 в 14:07
4
ответа
Почему не работает "жадный" режим RegExp?
Я не понимаю поведение. У меня есть такой пример, нужно ловить html комментарий. var str = '.. <!--My -- comment test--> '; var regex1 = /<!--[.]*-->/g; var regex2 = /<!--.*-->/g; alert(str.match(regex1)); // null alert(str.match(r…
03 фев '12 в 17:46
1
ответ
Универсальный и экзистенциальный квантификатор в прологе
Как я могу реализовать следующие правила в прологе. Я пишу предложение "Нет, пауки не млекопитающие" как экзистенциальное и универсальное: ¬∃x(mammals(X) ∧ spider(X) ) //It is not the case that mammals are spider ∀X(mammals(X) ⇒ ¬spider(X)) //All ma…
29 янв '15 в 16:38
2
ответа
В чем разница между этими двумя регулярными выражениями? (Понимание? Квантор)
В книге Eloquent JavaScript, глава 9: Регулярные выражения в разделе "Анализ файла INI", есть пример, который включает в себя регулярное выражение, которое я вообще не улавливаю. Автор пытается разобрать следующий контент: searchengine=http://www.go…
19 авг '16 в 15:01
1
ответ
Переменные типа Scoped требуют явных указаний. Зачем?
Если вы хотите использовать переменные типа GHC с лексической областью, вы также должны использовать явное универсальное количественное определение. То есть вы должны добавить forall объявления к сигнатурам типов ваших функций: {-# LANGUAGE Explicit…
04 апр '13 в 01:03