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

[Dejan Jovanović]

Hi Zachary,

When I was doing work on QF_NRA I wrote a bunch of converters from smtlib
to other tools. It's was written using cvc4 infrastructure and it shouldn't
be too hard to mimic for your purpose.

You can find the code in the cvc4 examples directory

https://github.com/CVC4/CVC4/tree/master/examples/nra-translate

Hope it helps.

Dejan

On Sat, Jan 21, 2017 at 6:16 PM Zachary Santer <zsanter at mix.wvu.edu> wrote:

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
_______________________________________________
SMT-LIB mailing list
SMT-LIB at cs.nyu.edu
http://www.cs.nyu.edu/mailman/listinfo/smt-lib