@@ -0,0 +1,2569 @@
+// This file is part of JavaSMT,%0A// an API wrapper for a collection of SMT solvers:%0A// https://github.com/sosy-lab/java-smt%0A//%0A// SPDX-FileCopyrightText: 2020 Dirk Beyer %3Chttps://www.sosy-lab.org%3E%0A//%0A// SPDX-License-Identifier: Apache-2.0%0A%0Apackage org.sosy_lab.java_smt.solvers.cvc5;%0A%0Aimport edu.stanford.CVC4.Expr;%0Aimport edu.stanford.CVC4.Kind;%0Aimport edu.stanford.CVC4.Type;%0Aimport java.math.BigDecimal;%0Aimport java.math.BigInteger;%0Aimport org.sosy_lab.java_smt.api.IntegerFormulaManager;%0Aimport org.sosy_lab.java_smt.api.NumeralFormula.IntegerFormula;%0Aimport org.sosy_lab.java_smt.basicimpl.AbstractNumeralFormulaManager.NonLinearArithmetic;%0A%0Apublic class CVC5IntegerFormulaManager%0A    extends CVC5NumeralFormulaManager%3CIntegerFormula, IntegerFormula%3E%0A    implements IntegerFormulaManager %7B%0A%0A  CVC5IntegerFormulaManager(CVC5FormulaCreator pCreator, NonLinearArithmetic pNonLinearArithmetic) %7B%0A    super(pCreator, pNonLinearArithmetic);%0A  %7D%0A%0A  @Override%0A  protected Type getNumeralType() %7B%0A    return getFormulaCreator().getIntegerType();%0A  %7D%0A%0A  @Override%0A  protected Expr makeNumberImpl(double pNumber) %7B%0A    return makeNumberImpl((long) pNumber);%0A  %7D%0A%0A  @Override%0A  protected Expr makeNumberImpl(BigDecimal pNumber) %7B%0A    return decimalAsInteger(pNumber);%0A  %7D%0A%0A  @Override%0A  public Expr divide(Expr pParam1, Expr pParam2) %7B%0A    return exprManager.mkExpr(Kind.INTS_DIVISION, pParam1, pParam2);%0A  %7D%0A%0A  @Override%0A  protected Expr modularCongruence(Expr pNumber1, Expr pNumber2, long pModulo) %7B%0A    return modularCongruence(pNumber1, pNumber2, BigInteger.valueOf(pModulo));%0A  %7D%0A%0A  @Override%0A  protected Expr modularCongruence(Expr pNumber1, Expr pNumber2, BigInteger pModulo) %7B%0A    // ((_ divisible n) x)   %3C==%3E   (= x (* n (div x n)))%0A    if (BigInteger.ZERO.compareTo(pModulo) %3C 0) %7B%0A      Expr n = makeNumberImpl(pModulo);%0A      Expr x = subtract(pNumber1, pNumber2);%0A      return exprManager.mkExpr(%0A          Kind.EQUAL,%0A          x,%0A          exprManager.mkExpr(Kind.MULT, n, exprManager.mkExpr(Kind.INTS_DIVISION, x, n)));%0A    %7D%0A    return exprManager.mkConst(true);%0A  %7D%0A%0A  @Override%0A  protected Expr makeNumberImpl(BigInteger pI) %7B%0A    return makeNumberImpl(pI.toString());%0A  %7D%0A%0A  @Override%0A  protected Expr makeNumberImpl(String pI) %7B%0A    if (!INTEGER_NUMBER.matcher(pI).matches()) %7B%0A      throw new NumberFormatException(%22number is not an integer value: %22 + pI);%0A    %7D%0A    return super.makeNumberImpl(pI);%0A  %7D%0A%0A  @Override%0A  protected Expr makeVariableImpl(String pI) %7B%0A    return formulaCreator.makeVariable(getFormulaCreator().getIntegerType(), pI);%0A  %7D%0A%7D%0A

Add incomplete CVC5IntegerFormulaManager