@@ -0,0 +1,2295 @@
+/*%0A *  JavaSMT is an API wrapper for a collection of SMT solvers.%0A *  This file is part of JavaSMT.%0A *%0A *  Copyright (C) 2007-2019  Dirk Beyer%0A *  All rights reserved.%0A *%0A *  Licensed under the Apache License, Version 2.0 (the %22License%22);%0A *  you may not use this file except in compliance with the License.%0A *  You may obtain a copy of the License at%0A *%0A *      http://www.apache.org/licenses/LICENSE-2.0%0A *%0A *  Unless required by applicable law or agreed to in writing, software%0A *  distributed under the License is distributed on an %22AS IS%22 BASIS,%0A *  WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.%0A *  See the License for the specific language governing permissions and%0A *  limitations under the License.%0A */%0Apackage org.sosy_lab.java_smt.solvers.yices2;%0A%0Aimport static org.sosy_lab.java_smt.solvers.yices2.Yices2NativeApi.yices_exists;%0Aimport static org.sosy_lab.java_smt.solvers.yices2.Yices2NativeApi.yices_forall;%0A%0Aimport com.google.common.primitives.Ints;%0Aimport java.util.List;%0Aimport org.sosy_lab.java_smt.api.SolverException;%0Aimport org.sosy_lab.java_smt.basicimpl.AbstractQuantifiedFormulaManager;%0Aimport org.sosy_lab.java_smt.basicimpl.FormulaCreator;%0A%0Apublic class Yices2QuantifiedFormulaManager%0A    extends AbstractQuantifiedFormulaManager%3CInteger, Integer, Long, Integer%3E %7B%0A%0A  protected Yices2QuantifiedFormulaManager(%0A      FormulaCreator%3CInteger, Integer, Long, Integer%3E pCreator) %7B%0A    super(pCreator);%0A    // TODO Auto-generated constructor stub%0A  %7D%0A%0A  @Override%0A  protected Integer eliminateQuantifiers(Integer pExtractInfo)%0A      throws SolverException, InterruptedException %7B%0A    // TODO Auto-generated method stub%0A    throw new UnsupportedOperationException(%22Yices does not support eliminating Quantifiers.%22);%0A  %7D%0A%0A  @Override%0A  public Integer mkQuantifier(Quantifier pQ, List%3CInteger%3E pVars, Integer pBody) %7B%0A    // TODO Auto-generated method stub%0A    if (pVars.isEmpty()) %7B%0A      throw new IllegalArgumentException(%22Empty variable list for Quantifier.%22);%0A    %7D else %7B%0A      int%5B%5D terms = Ints.toArray(pVars);%0A      if (pQ == Quantifier.FORALL) %7B%0A        return yices_forall(terms.length, terms, pBody);%0A      %7D else if (pQ == Quantifier.EXISTS) %7B%0A        return yices_exists(terms.length, terms, pBody);%0A      %7D%0A    %7D%0A    return null;%0A  %7D%0A%0A%7D%0A

Add QuantifiedFormulaManager (not yet active)