// This file is part of JavaSMT,
// an API wrapper for a collection of SMT solvers:
// https://github.com/sosy-lab/java-smt
//
// SPDX-FileCopyrightText: 2021 Dirk Beyer <https://www.sosy-lab.org>
//
// SPDX-License-Identifier: Apache-2.0

package org.sosy_lab.java_smt.test;

import org.junit.Before;
import org.junit.Test;
import org.junit.runner.RunWith;
import org.junit.runners.Parameterized;
import org.junit.runners.Parameterized.Parameter;
import org.junit.runners.Parameterized.Parameters;
import org.sosy_lab.java_smt.SolverContextFactory.Solvers;
import org.sosy_lab.java_smt.api.ArrayFormula;
import org.sosy_lab.java_smt.api.BooleanFormula;
import org.sosy_lab.java_smt.api.FormulaType;
import org.sosy_lab.java_smt.api.FormulaType.ArrayFormulaType;
import org.sosy_lab.java_smt.api.NumeralFormula.IntegerFormula;
import org.sosy_lab.java_smt.api.SolverException;

/** Tests Arrays for all solvers that support it. */
@RunWith(Parameterized.class)
public class ArrayFormulaManagerTest extends SolverBasedTest0 {

  @Parameters(name = "{0}")
  public static Object[] getAllSolvers() {
    return Solvers.values();
  }

  @Parameter(0)
  public Solvers solver;

  @Override
  protected Solvers solverToUse() {
    return solver;
  }

  @Before
  public void init() {
    requireArrays();
  }

  @Test
  public void uniqueType() throws SolverException, InterruptedException {
    requireIntegers();

    // (arr2 = store(arr1, 4, 2)) & !(select(arr2, 4) = 2)
    ArrayFormulaType<IntegerFormula, IntegerFormula> type =
        FormulaType.getArrayType(FormulaType.IntegerType, FormulaType.IntegerType);
    IntegerFormula num2 = imgr.makeNumber(2);
    IntegerFormula num4 = imgr.makeNumber(4);
    ArrayFormula<IntegerFormula, IntegerFormula> arr1 = amgr.makeArray("arr1", type);
    ArrayFormula<IntegerFormula, IntegerFormula> arr2 = amgr.makeArray("arr2", type);
    BooleanFormula query =
        bmgr.and(
            amgr.equivalence(arr2, amgr.store(arr1, num4, num2)),
            bmgr.not(imgr.equal(num2, amgr.select(arr2, num4))));
    assertThatFormula(query).isUnsatisfiable();
  }
}

@@ -270,16 +270,146 @@
 .test;%0A%0A
+import static org.sosy_lab.java_smt.api.FormulaType.IntegerType;%0Aimport static org.sosy_lab.java_smt.api.FormulaType.StringType;%0A%0A
 import o
@@ -425,16 +425,16 @@
 Before;%0A
-
 import o
@@ -999,16 +999,64 @@
 ception;
+%0Aimport org.sosy_lab.java_smt.api.StringFormula;
 %0A%0A/** Te
@@ -1733,28 +1733,16 @@
 rayType(
-FormulaType.
 IntegerT
@@ -1746,28 +1746,16 @@
 erType, 
-FormulaType.
 IntegerT
@@ -2135,16 +2135,16 @@
 num2)),%0A
-
         
@@ -2252,11 +2252,815 @@
 e();%0A  %7D
+%0A%0A  /*%0A   *  Test whether or not String Arrays are possible%0A   */%0A  @Test%0A  public void basicStringTypeTest() throws SolverException, InterruptedException %7B%0A    requireStrings();%0A%0A    // (arr2 = store(arr1, %22four%22, %22two%22)) & !(select(arr2, %22four%22) = %22two%22)%0A    StringFormula num2 = smgr.makeString(%22two%22);%0A    StringFormula num4 = smgr.makeString(%22four%22);%0A    ArrayFormula%3CStringFormula, StringFormula%3E arr1 =%0A        amgr.makeArray(%22arr1%22, StringType, StringType);%0A    ArrayFormula%3CStringFormula, StringFormula%3E arr2 =%0A        amgr.makeArray(%22arr2%22, StringType, StringType);%0A    BooleanFormula query =%0A        bmgr.and(%0A            amgr.equivalence(arr2, amgr.store(arr1, num4, num2)),%0A            bmgr.not(smgr.equal(num2, amgr.select(arr2, num4))));%0A    assertThatFormula(query).isUnsatisfiable();%0A  %7D
 %0A%7D%0A

Add a basic String Array test