[SMT-LIB] Extracting UTVPI Constraint Systems from SMT-LIB Benchmarks

[Zachary Santer]

I have implemented two algorithms for solving Unit Two Variable per
Inequality (+/- x_i {+/- x_j} <= c, c ϵ Z) constraint systems, for the
purposes of comparing them against one another empirically.

I designed a simple input file format that would allow UTVPI constraint
equations to be written normally, mainly for ease of testing. This format
also required minimal modifications to UTVPI constraint system files
generated by a random generator provided by Dr. Peter Stuckey.

I am interested in testing with real-world UTVPI constraint systems.
However, I have struggled to find a source for such systems. It has been
recommended that I extract the subset of systems within the QF_LIA
benchmarks that are purely UTVPI.

Even given the SMT-LIB 2 Lexer/Parser
<https://es-static.fbk.eu/people/griggio/misc/smtlib2parser.html> linked in
the site, this appears to be a rather daunting task.

Any guidance would be appreciated.

Regards,
Zachary Santer