/*
 *  CPAchecker is a tool for configurable software verification.
 *  This file is part of CPAchecker.
 *
 *  Copyright (C) 2007-2014  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.
 *
 *
 *  CPAchecker web page:
 *    http://cpachecker.sosy-lab.org
 */
package org.sosy_lab.solver.smtInterpol;

import org.sosy_lab.solver.api.ArrayFormula;
import org.sosy_lab.solver.api.Formula;
import org.sosy_lab.solver.api.FormulaType;
import org.sosy_lab.solver.api.FormulaType.ArrayFormulaType;
import org.sosy_lab.solver.basicimpl.FormulaCreator;

import de.uni_freiburg.informatik.ultimate.logic.Sort;
import de.uni_freiburg.informatik.ultimate.logic.Term;

class SmtInterpolFormulaCreator extends FormulaCreator<Term, Sort, SmtInterpolEnvironment> {

  SmtInterpolFormulaCreator(SmtInterpolEnvironment env) {
    super(env, env.getBooleanSort(), env.getIntegerSort(), env.getRealSort());
  }

  @Override
  public FormulaType<?> getFormulaType(Term pFormula) {
    if (SmtInterpolUtil.isBoolean(pFormula)) {
      return FormulaType.BooleanType;
    } else if (SmtInterpolUtil.hasIntegerType(pFormula)) {
      return FormulaType.IntegerType;
    } else if (SmtInterpolUtil.hasRationalType(pFormula)) {
      return FormulaType.RationalType;
    }
    throw new IllegalArgumentException("Unknown formula type");
  }

  @SuppressWarnings("unchecked")
  @Override
  public <T extends Formula> FormulaType<T> getFormulaType(T pFormula) {
    if (pFormula instanceof ArrayFormula<?,?>) {
      FormulaType<T> arrayIndexType = getArrayFormulaIndexType(
          (ArrayFormula<T, T>) pFormula);
      FormulaType<T> arrayElementType = getArrayFormulaElementType(
          (ArrayFormula<T, T>) pFormula);
      return (FormulaType<T>)new ArrayFormulaType<>(arrayIndexType,
          arrayElementType);
    }

    return super.getFormulaType(pFormula);
  }

  @Override
  public Term makeVariable(Sort type, String varName) {
    SmtInterpolEnvironment env = getEnv();
    env.declareFun(varName, new Sort[]{}, type);
    return env.term(varName);
  }

  @Override
  public Sort getBitvectorType(int pBitwidth) {
    throw new UnsupportedOperationException("Bitvector theory is not supported by SmtInterpol");
  }

  @Override
  public Sort getFloatingPointType(FormulaType.FloatingPointType type) {
    throw new UnsupportedOperationException("FloatingPoint theory is not supported by SmtInterpol");
  }

  @Override
  public Sort getArrayType(Sort pIndexType, Sort pElementType) {
    return getEnv().getTheory().getSort("Array", pIndexType, pElementType);
  }
}

@@ -1144,67 +1144,253 @@
 gic.
-Sort;%0Aimport de.uni_freiburg.informatik.ultimate.logic.Term
+ApplicationTerm;%0Aimport de.uni_freiburg.informatik.ultimate.logic.Sort;%0Aimport de.uni_freiburg.informatik.ultimate.logic.Term;%0Aimport de.uni_freiburg.informatik.ultimate.logic.TermVariable;%0Aimport de.uni_freiburg.informatik.ultimate.logic.Theory
 ;%0A%0Ac
@@ -1675,16 +1675,22 @@
 ulaType(
+final 
 Term pFo
@@ -1988,72 +1988,1046 @@
    %7D
-%0A    throw new IllegalArgumentException(%22Unknown formula type%22);
+ else if (SmtInterpolUtil.hasArrayType(pFormula))%7B%0A      Sort%5B%5D argumentSorts = pFormula.getSort().getArguments();%0A      assert argumentSorts.length == 2 : %22Array sort has to have two arguments,%22%0A          + %22 one for index type and one for element type!%22;%0A%0A      return new FormulaType.ArrayFormulaType%3C%3E(%0A          getFormulaTypeOfSort(argumentSorts%5B0%5D),%0A          getFormulaTypeOfSort(argumentSorts%5B1%5D));%0A    %7D%0A    throw new IllegalArgumentException(%22Unknown formula type%22);%0A  %7D%0A%0A  private FormulaType%3C?%3E getFormulaTypeOfSort(final Sort pSort) %7B%0A    final Theory theory = getEnv().getTheory();%0A    final Sort integer = theory.getNumericSort();%0A    final Sort rational = theory.getRealSort();%0A    final Sort bool = theory.getBooleanSort();%0A%0A    if (pSort == integer) %7B%0A      return FormulaType.IntegerType;%0A    %7D else if (pSort == rational) %7B%0A      return FormulaType.RationalType;%0A    %7D else if (pSort == bool) %7B%0A      return FormulaType.BooleanType;%0A    %7D else %7B%0A      throw new IllegalArgumentException(%22Unknown formula type%22);%0A    %7D
 %0A  %7D

Get an array formula type when using SMTInterpol.