QF_NIA benchmarks submission

Dear maintainers,

Here is a submission of benchmarks, in incremental mode for QF_NIA logic.

Our goal is to find optimums for some equations described in a picture compression standards.

For example consider this computation for an inverse discrete cosinus transform :

iDCT2_B2(int src[], int dst[], int line, int iSkipLine, int iSkipLine2) { 
  auto maxLineIdx = line - iSkipLine;
  auto maxColIdx = 2 - iSkipLine2;
  for (int i = 0; i < maxLineIdx; i++) {
    for (int k = 0; k < maxColIdx; k++) {
      dst[i * 2 + (0)] += src[k * line + i] * DCT2P2[k * 2];
    }
  }
  for (int i = 0; i < maxLineIdx; i++) { 
    for (int k = 0; k < maxColIdx; k++) { 
      dst[i * 2 + (0 + 1)] += src[k * line + i] * DCT2P2[k * 2 + 1];
    } 
  } 
}

We want to find the input src[] that maximizes src[k * line + i] * DCT2P2[k * 2 + (0)], the input src[] that maximizes src[k * line + i] * DCT2P2[k * 2 + 1], and finally the input src[] that globally maximizes each element of dst[] at the end of the process.

They are not shown here, but there are some constraints on input src[] (in this case, each element of src[] shall be in [-131072; 131071]). There might be as well some constraints on dst[], or any intermediate variable.

We represent such issues with SMT problems, and try to maximize by successively checking if a solution greater than a given threshold exists.

For the previous example, to find input that maximize dst[0], we first test (dst[0] ⩾ MAX_BOUND / 2) && (dst[0] ⩽ MAX_BOUND). Then depending on the result, we test either (dst[0] ⩾ MAX_BOUND / 4) && (dst[0] ⩽ MAX_BOUND / 2) or (dst[0] ⩾ 3 * MAX_BOUND / 4) && (dst[0] ⩽ MAX_BOUND).


                                                                          ┌───► ...
                                SAT    ┌───────────────────────────────┐  │
                                ┌─────►│(dst[0] ⩾ 3 * MAX_BOUND / 4) &&├──┤
┌────────────────────────────┐  │      │(dst[0] ⩽ MAX_BOUND            │  │
│(dst[0] ⩾ MAX_BOUND / 2) && │  │      └───────────────────────────────┘  └───► ...
│(dst[0] ⩽ MAX_BOUND)        ├──┤
└────────────────────────────┘  │
                                │      ┌───────────────────────────────┐  ┌───► ...
                                └─────►│(dst[0] ⩾ MAX_BOUND / 4) &&    │  │
                               UNSAT   │(dst[0] ⩽ MAX_BOUND / 2)       ├──┤
                                       └───────────────────────────────┘  │
                                                                          └───► ...

SMT-LIB / benchmark-submission-2023

QF_NIA benchmarks submission #12