I am preparing my course at ISR 22
about "constraint programming for analysis of rewriting".
(plan: https://www.imn.htwk-leipzig.de/~waldmann/talk/22/isr/ )
If you are using SAT/SMT in your termination prover -
how do you actually do it?
- how do you write the constraints
- what logics do you use
- how do you manage the (external) solver process
Example answers for matchbox - see below.
I'd appreciate brief answers here on the list
(or in email, and I can later summarize back)
perhaps with pointers to source and publications.
If there are no (current) publications - then we could write one?
Thanks - Johannes.
For example - for matchbox, the constraints are really
QF_NIA (standard matrices) and QF_LRA (arctic)
but I am not writing them as such,
but instead I am using an (eager) bit-blasting translation to SAT,
with the Ersatz library. That library neatly solves the
memoization problem (with hidden unsafePerformIO
so I can write the constraints in a functional way
(e.g., unknown numbers, and matrices, are instances of Num,
so `sum` automatically works, etc.)
For actual SMT writing, a nicely typed embedded DSL is
but it seems unmaintained, and I found it hard to add patches
(necessary because of changes in SMTLIB format specs)
I recently looked into https://hackage.haskell.org/package/simple-smt
but it requires some ugly monadic code, cf. evaluate_rule(_arc)
For actual SMT solving - I found these problems:
- QF_NIA (polynomial integer arithmetic) is hopeless,
we could use QF_BV (bitvectors) instead
but their arithmetic operators are silently overflowing
(it's modular arithmetic) so it requires extra (Boolean) programming
- QF_LRA is nice, but for each arctic number, I need an extra Boolean
(to encode MinusInfinity)
in all, the Boolean aspect seems to dominate,
so I could bit-blast directly (which I do).
Perhaps it's time for an arctic theory solver ...
Oh, and another technical point - I prefer to call the solver
via its (C) API, instead of writing to file, and calling an external
process. It seems faster - and I can stop/kill the solver (process)
much more reliably. But - while the textual input/output format is
fixed, those binary interfaces require extra (solver-specific) code
that will bit-rot quickly. SAT solvers seem to settle on IPASIR,
perhaps there's a similar standard emerging for SMT?
for SRS-Standard (certified), for several benchmarks,
example ICFP_2010/4991.xml, these results are displayed:
- matchbox: "YES (without \checkmark)"
- ttt2: "post-processor error" (post processor timeout after 15 min)
these are logically the same thing?
(both did produce a certificate?)
Ah - noh, for matchbox, the certifier did not time-out,
but "certification-err Stack space overflow: current size 8388608..."
Locally, I am not getting this error (certification succeeds
in 50 seconds for matchbox' certificate, 55 seconds for ttt2's)
I am using ceta-postproc (contains CeTA-2.42) compiled with ghc-9.0.2
Following some requests, the workshop for termination will be held
tomorrow and Friday in a *hybrid* manner (with mostly live talks, but
the possibility for remote attendance). Hence, for those of you who are
not in Haifa, remote participation is possible, and we will do our best
to support as smooth an experience as possible.**
The program is available at
https://easychair.org/smart-program/FLoC2022/WST-index.html ; in short,
Thursday is dedicated to theory presentations, and Friday to tools and
the termination competition.
(09:00--16:30 Haifa time; the meeting opens a bit earlier for
setting up and testing)
o Meeting ID: 858 5243 1972
(10:00--15:30 Haifa time)
o Meeting ID: 892 5980 8849
o Passcode: 792570
Hope to see you there!
** Though this comes with a disclaimer: we can only offer our best
effort, like the other hybrid FLoC workshops. The local setup is not
geared towards hybrid, so it is very possible that there will be some
issues with the network, sound quality or screen sharing.