// 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.solvers.cvc5;

import edu.stanford.CVC4.Expr;
import edu.stanford.CVC4.Kind;
import edu.stanford.CVC4.vectorExpr;
import io.github.cvc5.api.Solver;
import io.github.cvc5.api.Sort;
import io.github.cvc5.api.Term;
import java.util.List;
import org.sosy_lab.java_smt.api.SolverException;
import org.sosy_lab.java_smt.basicimpl.AbstractQuantifiedFormulaManager;
import org.sosy_lab.java_smt.basicimpl.FormulaCreator;
import org.sosy_lab.java_smt.solvers.cvc4.CVC4FormulaCreator;

public class CVC5QuantifiedFormulaManager
    extends AbstractQuantifiedFormulaManager<Term, Sort, Solver, Term> {

  private final Solver solver;

  protected CVC5QuantifiedFormulaManager(FormulaCreator<Term, Sort, Solver, Term> pFormulaCreator) {
    super(pFormulaCreator);

    solver = pFormulaCreator.getEnv();
  }

  /*
   * (non-Javadoc) CVC4s quantifier support is dependent on the options used.
   * Without any options it tends to run infenitly on many theories or examples.
   * There are 2 options improving this: full-saturate-quant and sygus-inst.
   * full-saturate-quant is activated in JavaSMT per default.
   * You can try combinations of them, or just one if a query is not solveable.
   * More info on full-saturate-quant: Enables "enumerative instantiation",
   * see: https://homepage.divms.uiowa.edu/~ajreynol/tacas18.pdf
   * More info on sygus-inst: Enables syntax-guided instantiation,
   * see https://homepage.divms.uiowa.edu/~ajreynol/tacas21.pdf
   * This approach tends to work well when the quantified formula involves
   * theories (e.g. strings) where more traditional quantifier instantiation
   * heuristics do not apply.
   * This applies to CVC4 and CVC5!
   */
  @Override
  protected Term eliminateQuantifiers(Expr pExtractInfo)
      throws SolverException, InterruptedException {
    Expr eliminated = pExtractInfo;
    // The first bool is for partial or full elimination. true is full
    // The second bool (optional; 2 methods) is whether to output warnings or not, such as when an
    // unexpected logic is used.
    try {
      eliminated = smtEngine.doQuantifierElimination(pExtractInfo, true);
    } catch (RuntimeException e) {
      // quantifier elimination failed, simply return the input
    }
    // We don't delete it in the prover.close(), is there a reason for that?
    smtEngine.delete();
    return eliminated;
  }

  /*
   * Makes the quantifier entered in CVC4. Note that CVC4 uses bound variables in quantified
   * formulas instead of the normal free vars. We create a bound copy for every var and substitute
   * the free var for the bound var in the body Formula. Note that CVC4 uses their internal Lists
   * for the variable list in quantifiers.
   */
  @Override
  public Term mkQuantifier(Quantifier pQ, List<Expr> pVars, Expr pBody) {
    if (pVars.isEmpty()) {
      throw new IllegalArgumentException("Empty variable list for quantifier.");
    } else {
      // CVC4 uses its own lists for quantifier that may only have bound vars
      vectorExpr vec = new vectorExpr();
      Expr substBody = pBody;
      // every free needs a bound copy. As the internal Id is different for every variable, even
      // with the same name, this is fine.
      for (Expr var : pVars) {
        Expr boundCopy = ((CVC4FormulaCreator) formulaCreator).makeBoundCopy(var);
        vec.add(boundCopy);
        substBody = substBody.substitute(var, boundCopy);
      }
      Expr quantifiedVars = exprManager.mkExpr(Kind.BOUND_VAR_LIST, vec);

      Kind quant = pQ == Quantifier.EXISTS ? Kind.EXISTS : Kind.FORALL;
      return exprManager.mkExpr(quant, quantifiedVars, substBody);
    }
  }
}

@@ -289,98 +289,31 @@
 ort 
-edu.stanford.CVC4.Expr;%0Aimport edu.stanford.CVC4.Kind;%0Aimport edu.stanford.CVC4.vectorExpr
+io.github.cvc5.api.Kind
 ;%0Aim
@@ -408,16 +408,44 @@
 i.Term;%0A
+import java.util.ArrayList;%0A
 import j
@@ -640,70 +640,8 @@
 tor;
-%0Aimport org.sosy_lab.java_smt.solvers.cvc4.CVC4FormulaCreator;
 %0A%0Apu
@@ -1889,20 +1889,20 @@
 tifiers(
-Expr
+Term
  pExtrac
@@ -1965,20 +1965,20 @@
 n %7B%0A    
-Expr
+Term
  elimina
@@ -2001,211 +2001,8 @@
 fo;%0A
-    // The first bool is for partial or full elimination. true is full%0A    // The second bool (optional; 2 methods) is whether to output warnings or not, such as when an%0A    // unexpected logic is used.%0A
     
@@ -2031,19 +2031,17 @@
  = s
-mtEngine.do
+olver.get
 Quan
@@ -2074,14 +2074,8 @@
 Info
-, true
 );%0A 
@@ -2182,109 +2182,8 @@
   %7D%0A
-    // We don't delete it in the prover.close(), is there a reason for that?%0A    smtEngine.delete();%0A
     
@@ -2609,20 +2609,20 @@
 Q, List%3C
-Expr
+Term
 %3E pVars,
@@ -2622,20 +2622,20 @@
  pVars, 
-Expr
+Term
  pBody) 
@@ -2767,117 +2767,46 @@
     
-// CVC4 uses its own lists for quantifier that may only have
+List%3CTerm%3E
  bound
- vars%0A      vectorExpr vec = new vectorExpr
+Vars = new ArrayList%3C%3E
 ();%0A
@@ -2811,20 +2811,20 @@
 ;%0A      
-Expr
+Term
  substBo
@@ -2986,20 +2986,20 @@
    for (
-Expr
+Term
  var : p
@@ -3014,20 +3014,20 @@
         
-Expr
+Term
  boundCo
@@ -3036,17 +3036,17 @@
  = ((CVC
-4
+5
 FormulaC
@@ -3097,19 +3097,25 @@
         
-vec
+boundVars
 .add(bou
@@ -3192,82 +3192,8 @@
    %7D
-%0A      Expr quantifiedVars = exprManager.mkExpr(Kind.BOUND_VAR_LIST, vec);
 %0A%0A  
@@ -3272,41 +3272,128 @@
     
-return exprManag
+Term boundVarsList = solver.mkTerm(Kind.VARIABLE_LIST, (Term%5B%5D) boundVars.toArray());%0A      return solv
 er.mk
-Expr
+Term
 (quant, 
 quan
@@ -3392,22 +3392,21 @@
 nt, 
-quantifie
+boun
 dVars
+List
 , su

Add CVC5 quantified formula manager