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

[Alberto Griggio]

Dear Zachary,

> 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.

I would not recommend that parser, in fact. It was meant more for solver
developers than for users, and it is way overkill for the task you want
to solve.

Besides what Dejan said, I think you can take a look at pySMT
(www.pysmt.org), which offers many shortcuts that should let you write a
translator in a few lines of Python code.

Alberto