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

[Tim King]

Dear Zachary,

Are you interested in extracting a set of UTVPI literals or extracting the
original problem over UTVPI literals including the input propositional
structure? If it is the latter, Dejan and Alerbto's suggestions are both
really good.

Given how you phrased this, I am guessing you want a set of literals. If
so, what kinds of sets of literals are you interested in? Does this only
include input problems that happen to already be equivalent to a set of
literals? Or is the UTVPI subset of literals that are sent to a theory
solver in a DPLL(T) combination interesting enough? There are a couple of
other possible choices. It all depends on what you want to be testing.

-Tim

PS. Look into QF_IDL. Those are guaranteed to be translatable into UTVPI.
For QF_LIA, you'll need to implement a filter of some kind.

On Mon, Jan 23, 2017 at 12:32 AM Alberto Griggio <griggio at fbk.eu> wrote:

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