ocaml-re icon indicating copy to clipboard operation
ocaml-re copied to clipboard

`witness` looks buggy

Open cshardin opened this issue 5 years ago • 2 comments

The witness function in core.ml can generate strings that don't match the expression, because it ignores the semantics of things like eow. Minimal example:

let t = Re.seq [ Re.eow; Re.str "foo" ] in
let witness = Re.witness t in
assert (not (Re.execp (Re.compile t) witness)) (* assertion succeeds but shouldn't *)

(For me personally this is low priority since I don't need that function. I just happened to notice it looked buggy.)

cshardin avatar Jul 29 '20 20:07 cshardin

It does ignore things like eow. I'm not quite sure how we would handle that ...

Drup avatar Aug 18 '20 17:08 Drup

I think fixing it is nontrivial. If nothing else, you could represent as a nondeterministic finite automaton (NFA) and then do a traversal that marks every accessible state with a witness for how to get into that state, and if that traversal hits an accepting state you have your witness.

The right "fix" might just be to change the doc comment for witness to make weaker claims about the semantics.

cshardin avatar Aug 18 '20 19:08 cshardin