Merge requests · waldmann / Matchbox SRS Termination

Resolve "find arctic matrices via SMT encoding (QF_LRA)"

!41 · created Aug 15, 2022 by waldmann
- Merged
updated Aug 26, 2022
Resolve "re-visit SMT solver interfaces"

!40 · created Aug 14, 2022 by waldmann
SMT
- Merged
updated Aug 15, 2022
Resolve "(re)implement CPF output"

!39 · created May 15, 2022 by waldmann
certification
- Merged
updated May 19, 2022
Resolve "KBO should use SRS compression"

!38 · created May 02, 2022 by waldmann
- Merged
updated May 02, 2022
Resolve "implement special matrix shapes"

!37 · created May 01, 2022 by waldmann
- Merged
updated May 01, 2022
Resolve "reduce number of nonzero matrix entries"

!36 · created Apr 30, 2022 by waldmann
SAT
- Merged
updated May 01, 2022
Resolve "draw graph of (sparse) matrix interpretation"

!35 · created Apr 30, 2022 by waldmann
- Merged
updated Apr 30, 2022
Resolve "plot graph of proof search steps"

!34 · created Apr 19, 2022 by waldmann
- Merged
updated Apr 23, 2022
Resolve "finding relative loops"

!33 · created Apr 19, 2022 by waldmann
nontermination
- Merged
updated Apr 19, 2022
strat

!32 · created Mar 16, 2022 by waldmann
- Merged
updated Mar 16, 2022
Resolve "SAT encoding for loops"

!31 · created Mar 12, 2022 by waldmann
- Merged
updated Mar 16, 2022
Resolve "use leancheck.Tiers for lazy enumeration of transport system candidates"

!30 · created Feb 08, 2022 by waldmann
- Merged
updated Feb 10, 2022
Unbounded bits

!28 · created Jan 30, 2022 by waldmann
- Merged
updated Jan 30, 2022
Draft: Resolve "benchmarking pqueue"

!27 · created Dec 10, 2021 by waldmann
- Merged
updated Dec 11, 2021
Draft: Resolve "test runs (TPDB) on starexec"

!21 · created May 31, 2021 by waldmann
TC21
- Merged
- 1
updated Sep 16, 2021
epsilons (for rfc mb approx) are fully working, merge into master

!25 · created Sep 16, 2021 by waldmann
- Merged
updated Sep 16, 2021
Resolve "early cut-off for too many tiles/tiled rules"

!20 · created May 29, 2021 by waldmann
- Merged
updated May 30, 2021
fix #322

!18 · created May 26, 2021 by waldmann
- Merged
updated May 26, 2021
Resolve "DP transform: make "guard $ not $ Q.isStrictSuffixOf r' $ lhs u" on/offable"

!17 · created Apr 30, 2021 by waldmann
- Merged
updated May 04, 2021
Resolve "parameter optimisation"

!13 · created Mar 20, 2021 by waldmann
- Merged
updated Apr 24, 2021