Sat solver on top of regex matcher • Hacker News Board

Re: Sat solver on top of regex matcher

#41

Post by ColinWright » Mon, Jun 22, 2020, 8:40 PM UTC

sacado2 wrote: post #40

ColinWright wrote: post #39

Earlier quoted context omitted.

As always, with all these things, there's a non-zero chance that I've mis-spoken myself somewhere. I'm going to "think out loud" on this so people can follow the thought processes. > I read it the other way: OK ... > all CNF instances can be rewritten as regexp + backreferences, By CNF you are referring to instances of the SAT problem. So yes, if you have an instance of the SAT problem, it can be re-written as an ins…

> we observe that checking an alleged regex+backtrack solution is a polynomial task That's the point I missed at first. That's good news, because I was pretty sure perl regex were accidentally Turing complete, I don't know why.

Cool.

This sort of thing can be really tough to follow because it's all deeply intertwungle. Glad I got it right.

Cheers!

Re: Sat solver on top of regex matcher

#42

Post by lifthrasiir » Tue, Jun 23, 2020, 1:50 AM UTC

hansvm wrote: post #30

lifthrasiir wrote: post #11

Earlier quoted context omitted.

The common case of only two pairs of quotes is indeed regular, but if you want to support either all Unicode quotes (about 60 pairs of them) or C++11 raw string literals `R"delim(...)delim"` (intrinsically not regular) you are out of luck.

For any finite set of quotation character pairs you can get away with a strategy like `(left_char1)[^right_char1] (right_char1)|(left_char2)[^right_char2] (right_char2)|...`. Escape characters aren't much harder to accommodate.

Of course, but you are out of luck in terms of complexity. (Colloquial) regular expressions lack any kind of abstractions.

Re: Sat solver on top of regex matcher

#43

Post by awirth » Tue, Jun 23, 2020, 2:49 AM UTC

awirth wrote: post #2

This reduction is really cool. I love reductions like this. Is there a general consensus to use "regular expression" to refer to the actual regular ones and "regex" to refer to the non-regular variants?

Too late to edit, but out of curiosity I re-implemented this to use the PCRE JIT (in PHP) to see what kind of speedup it would provide: https://gist.github.com/allanlw/69df509519335b88db886d48503a...

Timings for fred.cnf on my machine:

python: 0m53.744s

PHP (no PCRE JIT): (hits backtrack limit in 1m15.994s)

PHP (PCRE JIT): 0m20.109s

Re: Sat solver on top of regex matcher

#44

Post by Thorrez » Tue, Jun 23, 2020, 5:53 AM UTC

sacado2 wrote: post #15

Thorrez wrote: post #7

Earlier quoted context omitted.

Backreferences don't really help with those problems. > Won't work if you're already in a string This doesn't make sense. How can you search for a string if you're already in a string? I can't think of a realistic situation where that would be useful or even really possible. > or if there are escaped quotes in the string. Solvable: '(\'|\\|[^\'])*'|"(\"|\\|[^\"])*" > Also won't work if you have two or more double quo…

> This doesn't make sense. How can you search for a string if you're already in a string? I can't think of a realistic situation where that would be useful or even really possible. query = "select * from table where name like \"%foo\""

Interesting. Although in that situation I think it would be easier to find the outer string, then unescape it, then find the inner string.

Although if you want to do it with pure regex, it can be done without backreferences too, although it would be exponentially large as you get more and more levels of nesting, whereas with backreferences I think it would only get quadratically large.

Re: Sat solver on top of regex matcher

#45

Post by hansvm » Tue, Jun 23, 2020, 3:13 PM UTC

lifthrasiir wrote: post #42

hansvm wrote: post #30

Earlier quoted context omitted.

For any finite set of quotation character pairs you can get away with a strategy like `(left_char1)[^right_char1] (right_char1)|(left_char2)[^right_char2] (right_char2)|...`. Escape characters aren't much harder to accommodate.

Of course, but you are out of luck in terms of complexity. (Colloquial) regular expressions lack any kind of abstractions.

Absolutely. I don't for a moment think they're the right tool for the job.

They are fairly powerful in terms of what they're capable of parsing however (not enough for an arbitrary html document, but enough to handle the hairier situations in this thread that people thought they couldn't), and that does mean that a regular expression generator can handle all of those situations as well and potentially be much more readable.

If I found myself writing code like this I'd still want to reach for a better parsing technology, but you can use other languages to add abstractions to regex. Here's a Python3.6+ example assuming any desired backslashes have already been applied:

  '|'.join(rf'{a}[^{b}]*{b}' for a,b in pairs)

Re: Sat solver on top of regex matcher

#46

Post by throw681158 » Wed, Jun 24, 2020, 6:31 AM UTC

Thorrez wrote: post #7

throw681158 wrote: post #4

Earlier quoted context omitted.

Won't work if you're already in a string, or if there are escaped quotes in the string. Also won't work if you have two or more double quoted strings that both contain an apostrophe.

Backreferences don't really help with those problems. > Won't work if you're already in a string This doesn't make sense. How can you search for a string if you're already in a string? I can't think of a realistic situation where that would be useful or even really possible. > or if there are escaped quotes in the string. Solvable: '(\'|\\|[^\'])*'|"(\"|\\|[^\"])*" > Also won't work if you have two or more double quo…

Re: already in a string, one of the primary uses of regex is to search from point in a text editor. So, cursor is in a string and you want to find the next string. Regex won't work on its own, you generally need more semantic information to differentiate opening & closing quotes (unless you can use local context from that particular language to infer it).

But more broadly, any situation where you search from a non-zero index has this problem.

I'm surprised your example works in Python. Is that a property of Python's parser, or all regex matchers?

Re: Sat solver on top of regex matcher

#47

Post by throw681158 » Wed, Jun 24, 2020, 6:59 AM UTC

bottled_poe wrote: post #14

throw681158 wrote: post #4

Earlier quoted context omitted.

Won't work if you're already in a string, or if there are escaped quotes in the string. Also won't work if you have two or more double quoted strings that both contain an apostrophe.

That wasn’t specified in the requirements

Good point.

Re: Sat solver on top of regex matcher

#48

Post by Thorrez » Thu, Jun 25, 2020, 4:47 AM UTC

throw681158 wrote: post #46

Thorrez wrote: post #7

Earlier quoted context omitted.

Backreferences don't really help with those problems. > Won't work if you're already in a string This doesn't make sense. How can you search for a string if you're already in a string? I can't think of a realistic situation where that would be useful or even really possible. > or if there are escaped quotes in the string. Solvable: '(\'|\\|[^\'])*'|"(\"|\\|[^\"])*" > Also won't work if you have two or more double quo…

Re: already in a string, one of the primary uses of regex is to search from point in a text editor. So, cursor is in a string and you want to find the next string. Regex won't work on its own, you generally need more semantic information to differentiate opening & closing quotes (unless you can use local context from that particular language to infer it). But more broadly, any situation where you search from a non-ze…

> Regex won't work on its own, you generally need more semantic information

Yeah, I agree. My point was that regex won't work, regardless of if you have backreferences or not. So backreferences won't help.

> But more broadly, any situation where you search from a non-zero index has this problem.

I'm not sure I understand that. A lot of regex libraries let you specify a start index. It won't take into account data from before the start index though (regex doesn't really do that, regardless of backreferences). If your regex library doesn't support passing in a start index, you can just take a substring starting at that index, then search the substring.

I don't think Python is really special. Python's findall() is just a convenience function that does a loop finding a match, then finding another match that starts after the first match, etc. Most languages provide a way to find the end point of the most recent match, and then you can just write the loop yourself to start the next search at that point.

Re: Sat solver on top of regex matcher

#49

Post by b2gills » Fri, Jun 26, 2020, 4:02 PM UTC

Thorrez wrote: post #7

throw681158 wrote: post #4

Earlier quoted context omitted.

Won't work if you're already in a string, or if there are escaped quotes in the string. Also won't work if you have two or more double quoted strings that both contain an apostrophe.

Backreferences don't really help with those problems. > Won't work if you're already in a string This doesn't make sense. How can you search for a string if you're already in a string? I can't think of a realistic situation where that would be useful or even really possible. > or if there are escaped quotes in the string. Solvable: '(\'|\\|[^\'])*'|"(\"|\\|[^\"])*" > Also won't work if you have two or more double quo…

Raku allows strings inside of strings. Of course it does this by way of embedded closures.

    "abc{ "def" }"

Which allows it to be arbitrarily deep.

    "a{ "b{ "c{ "d{ "e{ "f" }g" }h" }i" }j" }k"
    → "abcdefghijk"

This can be handy to generate the correct string.

    my $count = 3;
    "I went to $count place{ "s" if $count ≠ 1 } today"

Re: Sat solver on top of regex matcher

#50

Post by Thorrez » Sat, Jun 27, 2020, 3:24 AM UTC

b2gills wrote: post #49

Thorrez wrote: post #7

Earlier quoted context omitted.

Backreferences don't really help with those problems. > Won't work if you're already in a string This doesn't make sense. How can you search for a string if you're already in a string? I can't think of a realistic situation where that would be useful or even really possible. > or if there are escaped quotes in the string. Solvable: '(\'|\\|[^\'])*'|"(\"|\\|[^\"])*" > Also won't work if you have two or more double quo…

Raku allows strings inside of strings. Of course it does this by way of embedded closures. "abc{ "def" }" Which allows it to be arbitrarily deep. "a{ "b{ "c{ "d{ "e{ "f" }g" }h" }i" }j" }k" → "abcdefghijk" This can be handy to generate the correct string. my $count = 3; "I went to $count place{ "s" if $count ≠ 1 } today"

Interesting, thanks for pointing out a use case. But I don't think backreferences will help with that, it needs to be parsed by something more powerful than a regex.

And that example reminds me that Bash can do something similar:

    echo "$(echo "$(echo "$(echo "hi")")")"