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

package org.sosy_lab.java_smt.solvers.cvc5;

import com.google.common.base.Preconditions;
import io.github.cvc5.Solver;
import java.util.Set;
import java.util.concurrent.atomic.AtomicBoolean;
import java.util.function.Consumer;
import org.sosy_lab.common.ShutdownNotifier;
import org.sosy_lab.common.log.LogManager;
import org.sosy_lab.java_smt.SolverContextFactory.Solvers;
import org.sosy_lab.java_smt.api.FloatingPointRoundingMode;
import org.sosy_lab.java_smt.api.InterpolatingProverEnvironment;
import org.sosy_lab.java_smt.api.OptimizationProverEnvironment;
import org.sosy_lab.java_smt.api.ProverEnvironment;
import org.sosy_lab.java_smt.api.SolverContext;
import org.sosy_lab.java_smt.basicimpl.AbstractNumeralFormulaManager.NonLinearArithmetic;
import org.sosy_lab.java_smt.basicimpl.AbstractSolverContext;

public final class CVC5SolverContext extends AbstractSolverContext {

  // creator is final, except after closing, then null.
  private CVC5FormulaCreator creator;
  private Solver solver;
  private final ShutdownNotifier shutdownNotifier;
  private final int randomSeed;
  private final AtomicBoolean isAnyStackAlive = new AtomicBoolean(false);
  private boolean closed = false;

  private CVC5SolverContext(
      CVC5FormulaCreator creator,
      CVC5FormulaManager manager,
      ShutdownNotifier pShutdownNotifier,
      Solver solver,
      int pRandomSeed) {
    super(manager);
    this.creator = creator;
    shutdownNotifier = pShutdownNotifier;
    randomSeed = pRandomSeed;
    this.solver = solver;
  }

  // CVC5 loads itself when creating a solver
  @SuppressWarnings({"unused", "resource"})
  public static SolverContext create(
      LogManager pLogger,
      ShutdownNotifier pShutdownNotifier,
      int randomSeed,
      NonLinearArithmetic pNonLinearArithmetic,
      FloatingPointRoundingMode pFloatingPointRoundingMode,
      Consumer<String> pLoader) {

    pLoader.accept("cvc5jni");
    // Solver is the central class for creating expressions/terms/formulae.
    // Also, creating a solver statically loads CVC5. We have to do it before CVC5 does it correctly
    // though.
    Solver newSolver = new Solver();

    // set common options.
    newSolver.setOption("seed", String.valueOf(randomSeed));
    newSolver.setOption("produce-models", "true");
    newSolver.setOption("finite-model-find", "true");
    newSolver.setOption("sets-ext", "true");
    newSolver.setOption("output-language", "smtlib2");
    // Set Strings option to enable all String features (such as lessOrEquals)
    newSolver.setOption("strings-exp", "true");
    newSolver.setOption("produce-unsat-cores", "true");
    // Neither simplification, arith-rewrite-equalities, pb-rewrites provide rewrites of trivial
    // formulas only
    // Note: with solver.getOptionNames() you can get all options

    CVC5FormulaCreator pCreator = new CVC5FormulaCreator(newSolver);

    // Create managers
    CVC5UFManager functionTheory = new CVC5UFManager(pCreator);
    CVC5BooleanFormulaManager booleanTheory = new CVC5BooleanFormulaManager(pCreator);
    CVC5IntegerFormulaManager integerTheory =
        new CVC5IntegerFormulaManager(pCreator, pNonLinearArithmetic);
    CVC5RationalFormulaManager rationalTheory =
        new CVC5RationalFormulaManager(pCreator, pNonLinearArithmetic);
    CVC5BitvectorFormulaManager bitvectorTheory =
        new CVC5BitvectorFormulaManager(pCreator, booleanTheory);

    CVC5FloatingPointFormulaManager fpTheory =
        new CVC5FloatingPointFormulaManager(pCreator, pFloatingPointRoundingMode);

    CVC5QuantifiedFormulaManager qfTheory = new CVC5QuantifiedFormulaManager(pCreator);

    CVC5ArrayFormulaManager arrayTheory = new CVC5ArrayFormulaManager(pCreator);
    CVC5SLFormulaManager slTheory = new CVC5SLFormulaManager(pCreator);
    CVC5StringFormulaManager strTheory = new CVC5StringFormulaManager(pCreator);
    CVC5FormulaManager manager =
        new CVC5FormulaManager(
            pCreator,
            functionTheory,
            booleanTheory,
            integerTheory,
            rationalTheory,
            bitvectorTheory,
            fpTheory,
            qfTheory,
            arrayTheory,
            slTheory,
            strTheory);

    return new CVC5SolverContext(pCreator, manager, pShutdownNotifier, newSolver, randomSeed);
  }

  @Override
  public String getVersion() {
    // TODO: Check if this is correct or if there is no version info.
    return solver.getOptionInfo("version").toString();
  }

  @Override
  public void close() {
    if (creator != null) {
      closed = true;
      solver.close();
      creator = null;
    }
  }

  @Override
  public Solvers getSolverName() {
    return Solvers.CVC5;
  }

  @Override
  public ProverEnvironment newProverEnvironment0(Set<ProverOptions> pOptions) {
    Preconditions.checkState(!closed, "solver context is already closed");
    return new CVC5TheoremProver(
        creator,
        shutdownNotifier,
        randomSeed,
        pOptions,
        getFormulaManager().getBooleanFormulaManager(),
        solver,
        isAnyStackAlive);
  }

  @Override
  protected boolean supportsAssumptionSolving() {
    return false;
  }

  @Override
  protected InterpolatingProverEnvironment<?> newProverEnvironmentWithInterpolation0(
      Set<ProverOptions> pOptions) {
    Preconditions.checkState(!closed, "solver context is already closed");
    // Unsat Core and interpolation may not be active both at once!
    solver.setOption("produce-unsat-cores", "false");
    solver.setOption("produce-interpolants", "true");
    return new CVC5InterpolatingProver(
        creator,
        shutdownNotifier,
        randomSeed,
        pOptions,
        getFormulaManager().getBooleanFormulaManager(),
        solver,
        isAnyStackAlive);
  }

  @Override
  protected OptimizationProverEnvironment newOptimizationProverEnvironment0(
      Set<ProverOptions> pSet) {
    throw new UnsupportedOperationException("CVC5 does not support optimization");
  }
}

@@ -1429,16 +1429,188 @@
 = false;
+%0A  // CVC5 does not like changing options after a stack was used. We remember what the last stack was%0A  // with this.%0A  private boolean wasInterpolationStackBefore = false;
 %0A%0A  priv
@@ -5781,24 +5781,66 @@
 y closed%22);%0A
+    if (!wasInterpolationStackBefore) %7B%0A  
     // Unsat
@@ -5895,24 +5895,26 @@
 t once!%0A    
+  
 solver.setOp
@@ -5951,24 +5951,26 @@
 alse%22);%0A    
+  
 solver.setOp
@@ -6003,24 +6003,72 @@
 %22, %22true%22);%0A
+      wasInterpolationStackBefore = true;%0A    %7D%0A
     return n

Allow the creation of the same stack again after closing (CVC5 does not allow option changes after using any stack on that context, remember what stack we made so that we don't have to change the options for the same stack)