Frédéric Besson
Frédéric Besson
When set, the list of hypotheses needed by lia,nia,lra,nra proofs are printed. It should be safe to clear them and therefore speed-up proof search. - [x] Added **changelog**. - [...
The PR makes a minimal modification to the proof-search of `tauto` so that `axioms` are checked for each time a new formula is generated. + This may avoid performing a...
This PR makes substantial changes to `lra` so that is can handle Mixed Integer Linear Programs (MILP) i.e. goals where variables range over either R or Z. This requires several...