Dear Johannes, LoAT has a custom, minimalistic interface for SMT solvers [1]. Currently, there are two implementations, based on the C(++) APIs of Z3 and Yices (there was a third one for CVC4 in the past, and I plan to integrate CVC5 in the future). It uses the logics QF_LIA, QF_NIA, and QF_NIA + exponentials (which is not yet standardized, as far as I know, but Z3 can at least handle the trivial cases). Yices is used for QF_LIA and Z3 is used for QF_NIA. For managing resources, I use Z3's timeout parameter, and Yices is called in its own thread and stopped via the corresponding API-call (yices_stop_search) when the timeout expires. For QF_NIA, that does not work reliably, which is one of the reasons why LoAT uses Z3 instead of Yices for QF_NIA. The majority of the SMT calls are needed to check satisfiability of the guards of transitions (to remove inapplicable transitions which arise due to LoAT's underapproximations), and to check the preconditions of LoAT's loop acceleration and non-termination techniques [2,3]. Best Florian [1] https://github.com/LoAT-developers/LoAT/blob/master/src/smt/smt.hpp [2] https://link.springer.com/chapter/10.1007/978-3-030-45190-5_4 [3] https://arxiv.org/abs/2111.13952 On 8/16/22 14:29, 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 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-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 to termtools-leave@lists.rwth-aachen.de