The first goal of this repository is to have a library to manipulate systems of divisibility constraints over linear (diophantine) polynomials conjoined with equations and inequalities.
- Normalization of such formulas (based on "On the Complexity of Linear Arithmetic with Divisibility", by Joël Ouaknine, Antonia Lechner and Ben Worrell.)
- Solvers for normalized formulas (based on the same work mentioned above, and an alternative one based on "Integer Programming with GCD Constraints", by Rémy Défossez, Christoph Haase, Alessio Mansutti, and Guillermo A. Pérez.)
- We are only encoding systems, so no disjunctions.
- Variables are quantified over the integers for now. This is a bit off since after an affine change of variables we go to natural numbers instead. To remediate this, we are asking that a system of linear constraints is always given to represent that domain of the variables explicitly. (That is, working on a system of divisibilities with no further constraints implicitly tells the library that we have changed from integers to naturals as domain.)
- Everything is tuples (of tuples).
- We don't encode Ax = b but rather Ax - b = 0 and the last "coefficient" is the constant in the polynomial. Similar weirdness applies to inequalities.
Given a system of divisibilities and linear constraints, we can implement Lipshitz' transformation into increasing normal form if we have:
- A way of obtaining a (hybrid) semilinear representation of the solutions of a system of linear equations---which can be used to update the system of divisibilities via an affine change of variables while not increasing the number of variables
- A way of enumerating the sign of the left-hand sides of divisibility constraints, towards obtaining left-hand sides with all positive coefficients, and adding them as inequalities to then remove them via the method described above
- A way of obtaining a finite representation of the module of the primitive polynomials of the left-hand sides. In short, (see Section C.1 from the extended version of the cited SODA paper) we get a finite spanning set of the module.
- A way of checking whether a given system is increasing for a given (semantic) order over the variables, based on the representation above. For this, we can compare the Hermite normal form (HNF) of matrices spanning (1) the Z-module generated by the primitive form and (2) the intersection of the modules of the primitive polynomials and the relevant set of polynomials. (For an algorithm to compute the intersection of modules, see Chapter 2 from H. Cohen's A Course in Computational Algebraic Number Theory. Flint implements HNF algorithms based on LLL.)
- An algorithm to deal with a witness of nonincreasingness to split (disjuntively) into subformulas with less variables (Key for termination: each subformulas has to have strictly less variables)
- A recursive-style algorithm to keep finding nonincreasing subformulas to treat with the procedure above.
- ...
For now, Z3 and flint