/*
 *  JavaSMT is an API wrapper for a collection of SMT solvers.
 *  This file is part of JavaSMT.
 *
 *  Copyright (C) 2007-2019  Dirk Beyer
 *  All rights reserved.
 *
 *  Licensed under the Apache License, Version 2.0 (the "License");
 *  you may not use this file except in compliance with the License.
 *  You may obtain a copy of the License at
 *
 *      http://www.apache.org/licenses/LICENSE-2.0
 *
 *  Unless required by applicable law or agreed to in writing, software
 *  distributed under the License is distributed on an "AS IS" BASIS,
 *  WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
 *  See the License for the specific language governing permissions and
 *  limitations under the License.
 */
package org.sosy_lab.java_smt.solvers.boolector;

import static org.junit.Assert.assertEquals;

import com.google.common.collect.ImmutableMap;
import java.util.Map;
import org.junit.After;
import org.junit.AssumptionViolatedException;
import org.junit.Before;
import org.junit.BeforeClass;
import org.junit.Test;
import org.sosy_lab.common.NativeLibraries;

public class BoolectorNativeApiTest {

  private long btor;

  @BeforeClass
  public static void loadMathsat() {
    try {
      NativeLibraries.loadLibrary("boolector");
    } catch (UnsatisfiedLinkError e) {
      throw new AssumptionViolatedException("Boolector is not available", e);
    }
  }

  @Before
  public void createEnvironment() {
    btor = BtorJNI.boolector_new();
  }

  @After
  public void freeEnvironment() {
    BtorJNI.boolector_delete(btor);
  }

  // some options have a different name in the API that their internal representation.
  // TODO why?
  private static final Map<String, String> ALLOWED_DIFFS =
      ImmutableMap.<String, String>builder()
          .put("BTOR_OPT_ACKERMANNIZE", "BTOR_OPT_ACKERMANN")
          .put("BTOR_OPT_QUANT_DUAL", "BTOR_OPT_QUANT_DUAL_SOLVER")
          .put("BTOR_OPT_QUANT_SYNTHLIMIT", "BTOR_OPT_QUANT_SYNTH_LIMIT")
          .put("BTOR_OPT_QUANT_SYNTHQI", "BTOR_OPT_QUANT_SYNTH_QI")
          .put("BTOR_OPT_QUANT_MS", "BTOR_OPT_QUANT_MINISCOPE")
          .put("BTOR_OPT_DEFAULT_CADICAL", "BTOR_OPT_DEFAULT_TO_CADICAL")
          .put("BTOR_OPT_QUANT_SYNTHCOMPLETE", "BTOR_OPT_QUANT_SYNTH_ITE_COMPLETE")
          .build();

  @Test
  public void optionNameTest() {
    // check whether our enum is identical to Boolector's internal enum
    for (BtorOption option : BtorOption.values()) {
      String optName = BtorJNI.boolector_get_opt_lng(btor, option.getValue());
      String converted = "BTOR_OPT_" + optName.replace("-", "_").replace(":", "_").toUpperCase();
      assertEquals(option.name(), ALLOWED_DIFFS.getOrDefault(converted, converted));
    }
  }
}

@@ -1088,16 +1088,95 @@
 braries;
+%0Aimport org.sosy_lab.java_smt.solvers.boolector.BoolectorEnvironment.SatSolver;
 %0A%0Apublic
@@ -1274,15 +1274,8 @@
 load
-Mathsat
 () %7B
@@ -2789,11 +2789,560 @@
    %7D%0A  %7D
+%0A%0A  @Test%0A  public void satSolverTest() %7B%0A    // check whether all sat solvers are available%0A    for (SatSolver satSolver : SatSolver.values()) %7B%0A      long btor1 = BtorJNI.boolector_new();%0A      BtorJNI.boolector_set_sat_solver(btor1, satSolver.name());%0A      long newVar = BtorJNI.boolector_var(btor1, BtorJNI.boolector_bool_sort(btor1), %22x%22);%0A      BtorJNI.boolector_assert(btor1, newVar);%0A      int result = BtorJNI.boolector_sat(btor1);%0A      assertEquals(BtorJNI.BTOR_RESULT_SAT_get(), result);%0A      BtorJNI.boolector_delete(btor1);%0A    %7D%0A  %7D
 %0A%7D%0A

add test for background sat solvers.