Dear Johannes, in MU-TERM, we generate first-order formulae that are translated into constraints following this article (interpretations are given for function symbols and relations): https://link.springer.com/article/10.1007/s10817-017-9419-3 all this process from the generation of the fist-order formulae to the application of the Farkas' Lemma is implemented using MU-TERM internal libraries. We translate these constraints from our internal format to SMTLIB2 format using the logic QF_NIA and setting the variables into the Int domain. The result is a ByteString that is sent to a temporary file and an external call is executed. The result is stored in a new temporary file that is parsed by MU-TERM. When we want to use finite rational domains (for example, if we want only 1, 1/2 and 2 as coefficients), we still use nlsol (in this case, relations are interpreted in the classical way): https://www.cs.upc.edu/~albert/nonlinear.html Hope it helps. Best, Raúl. On 8/16/2022 2:29 PM, Johannes Waldmann wrote:
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.ht... ) 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 intohttps://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-ar...
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? _______________________________________________ Termtools mailing list --termtools@lists.rwth-aachen.de To unsubscribe send an email totermtools-leave@lists.rwth-aachen.de -- Raúl Gutiérrez
UNIVERSIDAD POLITÉCNICA DE MADRID <https://www.upm.es/> Raúl Gutiérrez Profesor Ayudante Doctor Departamento de Lenguajes y Sistemas Informáticos e Ingeniería de Software Campus de Montegancedo. 28660, Boadilla del Monte, Madrid SPAIN ✉ r.gutierrez@upm.es <mailto:r.gutierrez@upm.es> Aviso / Disclaimer <https://www.upm.es/disclaimer> 🌳 🌳 Piensa antes de imprimir.