Termtools August 2022

termtools@lists.rwth-aachen.de

8 participants
4 discussions

survey: what software for SAT/SMT encoding (for termination analysis)

by Johannes Waldmann

Dear all, 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 https://hackage.haskell.org/package/ersatz-0.4.12/docs/src/Ersatz.Problem.h… ) 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 https://hackage.haskell.org/package/smtlib2-1.0/docs/Language-SMTLib2.html 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) https://gitlab.imn.htwk-leipzig.de/waldmann/pure-matchbox/-/blob/457-find-a… 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?

2 years

time-outs/stack-overflows when checking certificates (SRS std)

by Johannes Waldmann

Dear Akihisa, for SRS-Standard (certified), for several benchmarks, example ICFP_2010/4991.xml, these results are displayed: - matchbox: "YES (without \checkmark)" https://www.starexec.org/starexec/services/jobs/pairs/567222906/stdout/1?li… - ttt2: "post-processor error" (post processor timeout after 15 min) https://www.starexec.org/starexec/services/jobs/pairs/567222903/log 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 - Johannes.

2 years, 1 month

WST 2022: option for virtual participation

by Cynthia Kop

Dear all, 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. Zoom data: * Thursday: o https://radbouduniversity.zoom.us/j/85852431972?pwd=Y1ZwY1RPeUU2MzUwWU9lNXZ… (09:00--16:30 Haifa time; the meeting opens a bit earlier for setting up and testing) o Meeting ID: 858 5243 1972 Passcode: 928647 * Friday: o https://radbouduniversity.zoom.us/j/89259808849?pwd=eHF2a1BWTWwrR3pmOS9tbzB… (10:00--15:30 Haifa time) o Meeting ID: 892 5980 8849 o Passcode: 792570 Hope to see you there! Cynthia. ** 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.

2 years, 1 month

First run

by YAMADA, Akihisa

Dear all, some jobs of the first run have been started. Please monitor via: https://termcomp.github.io/Y2022/ (Not all jobs because of the popular permission problems.) Good luck! Akihisa

2 years, 1 month

2024

2023

2022

2021

2020

Termtools August 2022