Dear all,
I am preparing my course at ISR 22 about "constraint programming for analysis of rewriting". (plan: https://www.imn.htwk-leipzig.de/%7Ewaldmann/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?
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/%7Ealbert/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/%7Ewaldmann/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
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/%7Ewaldmann/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
Dear Johannes, dear all,
- how do you write the constraints
In AProVE, arithmetic constraints are created programmatically and represented using recursive data structures, without an explicit intermediate language. These data structures are then either exported to SMT-LIB2 strings or bit-blasted to propositional formulas.
For RPO, a dedicated propositional encoding is used:
Michael Codish, Jürgen Giesl, Peter Schneider-Kamp, René Thiemann: SAT Solving for Termination Proofs with Recursive Path Orders and Dependency Pairs. J. Autom. Reason. 49(1): 53-93 (2012)
http://verify.rwth-aachen.de/giesl/papers/RPO-Journal-distribute.pdf
The representation of propositional formulas allows for arbitrary nesting of connectives. Formula construction uses structural hashing (aka sharing of subformulas), implemented via suitable instances of the Factory pattern. Formulas are converted to CNF via the implementation of Tseitin's equisatisfiable encoding in SAT4J.
- what logics do you use
Beyond propositional logic:
-- QF_NIA is used for arithmetic interpretations that are at least as expressive as linear polynomial interpretations (max-polynomials, matrix interpretations, non-linear polynomials, ...); carriers of these interpretations are the naturals, the integers, and the non-negative rationals.
Solved via bit-blasting with structural hashing/sharing of subformulas and several simplifications during formula construction, using the encoding in
Carsten Fuhs, Jürgen Giesl, Aart Middeldorp, Peter Schneider-Kamp, René Thiemann, Harald Zankl: SAT Solving for Termination Analysis with Polynomial Interpretations. SAT 2007: 340-354
https://www.dcs.bbk.ac.uk/%7Ecarsten/papers/SAT07-satpolo.pdf
Experiments with Z3 v3.2 in 2011 (for a talk at a Z3 workshop) showed that solving QF_NIA formulas from the search for linear polynomial interpretations with /unbounded/ arithmetic variables was very slow.
However, adding constraints a_i <= N for variables a_i and small values for a constant bound N led to a performance that was only slightly worse than that of AProVE's dedicated SAT encoding for the same bound N. QF_NIA has the benefit over QF_BV that no overflow-related issues can occur, and internally SMT solvers can make use of the bound N.
(Rerunning such experiments with /current/ versions of Z3, Yices, CVC5, ... might be interesting.)
-- QF_LIA is used for linear polynomials with hard-coded coefficient 1, where only the additive weight is needed, and for KBO following the encoding in
Harald Zankl, Nao Hirokawa, Aart Middeldorp: KBO Orientability. J. Autom. Reason. 43(2): 173-201 (2009)
http://cl-informatik.uibk.ac.at/users/hzankl/new/publications/ZA09_01.pdf
-- Quantifier-free arctic naturals/integers (as pointed out earlier, closely related to QF_LIA/QF_LRA, but with an additional -\infty value) are used in the search for arctic matrix interpretations. AProVE uses a variant of the unary order encoding described in Section 5.3 of
Carsten Fuhs: SAT encodings: from constraint-based termination analysis to circuit synthesis. RWTH Aachen University, 2012, pp. 1-188
http://sunsite.informatik.rwth-aachen.de/Publications/AIB/2011/2011-17.pdf
- how do you manage the (external) solver process
-- External solvers called via Java API: SAT4J, SMTInterpol.
For quick queries on very small inputs (e.g., checking validity of conditional polynomial constraints from concrete max-polynomial interpretations or checking effectiveness of a semantic labelling), SAT4J is used - the overhead of spawning an external process is avoided.
This matters in particular for JVM-based termination tools: creating a new process first makes a copy of the parent process - with all its used memory - and only then runs the called program, with undesired effects (even if the process copy is actually created lazily by the OS):
https://www.tapatalk.com/groups/starexec/strange-memouts-t106.html
In this sense, for "heavy-duty" constraint solving in a competitive setting, also systems-level considerations matter.
-- External solvers used as processes: MiniSat, Yices, Z3.
MiniSat 2.2 is arguably not the most recent solver (last update in 2008?), so improvements via (suitably configured) more modern SAT solvers may be possible. According to Section 4 of
Emre Yolcu, Scott Aaronson, Marijn J. H. Heule: An Automated Approach to the Collatz Conjecture. CADE 2021: 468-484
https://link.springer.com/content/pdf/10.1007/978-3-030-79876-5_27.pdf
a suitable configuration for modern solvers may be to change the solver's branching behaviour from phase-saving (default in many recent solvers) to negative branching (default in MiniSat - always try 'false' before 'true').
AProVE kills external processes on OS level if either their timer (configured in the strategy language) has elapsed or separate progress in the termination proof makes the remaining computation by the process unnecessary: for example, when AProVE searches for an RPO and a polynomial interpretation with two running MiniSat instances in parallel, and an RPO that simplifies the termination problem is found, then the search for a polynomial interpretation, along with its MiniSat process, are aborted immediately. Being able to abort computations immediately, also in a parallel setting, is a motivation to use external processes rather than a solver API.
An overview of AProVE's constraint solving automation via SAT and SMT solving with further pointers is available in Section 4 of
Jürgen Giesl, Cornelius Aschermann, Marc Brockschmidt, Fabian Emmes, Florian Frohn, Carsten Fuhs, Jera Hensel, Carsten Otto, Martin Plücker, Peter Schneider-Kamp, Thomas Ströder, Stephanie Swiderski, René Thiemann: Analyzing Program Termination and Complexity Automatically with AProVE. J. Autom. Reason. 58(1): 3-31 (2017)
https://www.dcs.bbk.ac.uk/%7Ecarsten/papers/JAR-AProVE.pdf
Best regards,
Carsten
On 16/08/2022 13: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/%7Ewaldmann/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
WARNING: This email originated from outside of Birkbeck. Do not click links or open attachments unless you recognise the sender. Under testing so any comments sg@dcs.bbk.ac.uk
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/%7Ewaldmann/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
Dear all,
thank-you very much for the information you sent on SAT/SMT for termination.
That's certainly more than enough for my course at ISR (very short course - I will cover some fundamentals, but for details, I can refer students to this mailing list thread)
I cannot give an review of all the answers (I have to read up on some of the papers that were cited, e.g., on incremental SMT solving in NaTT) but just some small observations/comments
(Carsten, on AProVE)
* improvements via (suitably configured) more modern SAT solvers may be possible.
Yes. E.g., Kissat has lots of parameters, and provides a uniform interface (command line and API) My optimizer computed this https://gitlab.imn.htwk-leipzig.de/waldmann/pure-matchbox/-/blob/master/stra... but the search space is huge, and my optimizer is naive See also https://github.com/arminbiere/kissat/issues/25 There's room for at least one Bachelor's thesis here.
* AProVE kills external processes on OS level ...
I struggle with this (cf. https://github.com/yav/simple-smt/issues/21) but this may be a Haskell/libraries problem (lazy IO). Stopping Kissat via API just works. (I think it sets some flag that the solver's main loop checks often enough.)
(Akihisa, on NaTT)
* Coefficients are usually (ite b 0 1) or (ite b 1 2),
Interesting! So it's actually a finite-domain constraint. There are classical (non-SMT) solvers for these, e.g. https://www.gecode.org/ Did any-one try this? Possibly via the mini/flatzinc language? https://www.minizinc.org/doc-2.6.4/en/part_4_reference.html
Best regards, Johannes.
Dear Johannes,
- Coefficients are usually (ite b 0 1) or (ite b 1 2),
Interesting! So it's actually a finite-domain constraint.
no, I mean constant parts are left unbounded. Interpretations look like (ite b 0 1) * x + (ite b 0 1) * y + w
Best, Akihisa
termtools@lists.rwth-aachen.de