Dear Johannes, (hope it's still in time.) NaTT requires an SMT solver that can read SMT-LIB 2.0 queries via stdin, e.g. and by default, "z3 -smt2 -in". The communication doesn't go via filesystem and I don't feel need for making API calls. The theory is usually QF-LR(I)A. Coefficients are usually (ite b 0 1) or (ite b 1 2), linearized by distribution. Probably more importantly, NaTT uses incremental feature (push/pop). Above are described in a publication: https://doi.org/10.1007/978-3-319-08918-8_32, and later presented at WST: https://akihisayamada.github.io/NaTT2016.pptx It also does a partly lazy encoding, so that x in (x && false) etc. will not be fully generated. Best, Akihisa On 8/16/2022 9: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 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