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.

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.html#generateLiteral
)
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-arctic-matrices-via-smt-encoding-qf_lra/src/Matchbox/Matrix/Remove.hs#L654

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