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

Alberto Griggio griggio at fbk.eu
Mon Jan 23 03:30:54 EST 2017


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


More information about the SMT-LIB mailing list