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, 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 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.