Add QF_BV benchmark for DataPlane DFA Synthesis

[chenxiaoqino]

Dear SMT-LIB benchmarks maintainers,

I would like to submit a set of benchmarks resulting from some workload we encountered when we use SMT solvers in our paper. In particular, we are surprised to find different SMT solvers exhibits 10x-100x speed difference on these inputs, hence they should be a pretty good addition to the benchmark :)

The problem definition is to find an isomorphic mapping for a state machine (DFA) so that different states and transition symbols are mapped to different bit vectors, and the bit vectors satisfy certain arithmetic relations corresponding to the DFA transition rules.

I have marked some quickly solvable cases to sat; the other cases are incrementally harder (marked unknown), but in our experiments about 20% of them can be solved (sat) under 20-30 minutes.

I have used dolmen to check the files.

Thanks for maintaining the benchmark!

(This was a copy of the original PR in the 2022 repository.)

[m-fleury]

Is it expected that the folder is called StringMatcing`and not StringMatching? (just nitpicking, sorry...)

[chenxiaoqino]

Thanks for catching the typo! Fixed it...

[hansjoergschurr]

Thank you very much for your benchmark contribution. I will merge them now. We will run some solvers on them to see if anything unexpected happens (such as errors in the status). If everything goes well the benchmarks will be included in the next release.