<commit_before>// 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 <NAME> <https://www.sosy-lab.org>
//
// SPDX-License-Identifier: Apache-2.0

package org.sosy_lab.java_smt.solvers.boolector;

import static com.google.common.base.Preconditions.checkArgument;

import com.google.common.base.Preconditions;
import com.google.common.collect.HashBasedTable;
import com.google.common.collect.ImmutableList;
import com.google.common.collect.Table;
import com.google.common.primitives.Longs;
import java.math.BigInteger;
import java.util.ArrayList;
import java.util.HashMap;
import java.util.List;
import org.sosy_lab.java_smt.api.ArrayFormula;
import org.sosy_lab.java_smt.api.BitvectorFormula;
import org.sosy_lab.java_smt.api.BooleanFormula;
import org.sosy_lab.java_smt.api.Formula;
import org.sosy_lab.java_smt.api.FormulaType;
import org.sosy_lab.java_smt.api.FormulaType.ArrayFormulaType;
import org.sosy_lab.java_smt.api.FormulaType.FloatingPointType;
import org.sosy_lab.java_smt.api.FunctionDeclarationKind;
import org.sosy_lab.java_smt.api.visitors.FormulaVisitor;
import org.sosy_lab.java_smt.basicimpl.FormulaCreator;
import org.sosy_lab.java_smt.basicimpl.FunctionDeclarationImpl;
import org.sosy_lab.java_smt.solvers.boolector.BoolectorFormula.BoolectorArrayFormula;
import org.sosy_lab.java_smt.solvers.boolector.BoolectorFormula.BoolectorBitvectorFormula;
import org.sosy_lab.java_smt.solvers.boolector.BoolectorFormula.BoolectorBooleanFormula;

public class BoolectorFormulaCreator extends FormulaCreator<Long, Long, Long, Long> {

  // Boolector can give back 'x' for an arbitrary value that we change to this
  private static final char ARBITRARY_VALUE = '1';

  /** Maps a name and a variable or function type to a concrete formula node. */
  private final Table<String, Long, Long> nameFormulaCache = HashBasedTable.create();

  /*  Experiment: remember all variables, arrays and ufs in this map by their name.
   *  Reconstruct a model based on the smt-lib2 and this map.
   *  If this works, remove the nameFormulaCache and make this the vars cache.
   */
  private final HashMap<String, Long> nameFormulaMap = new HashMap<>();
  private final HashMap<Long, List<Long>> ufArgumentsSortMap = new HashMap<>();
  // Possibly we need to split this up into vars, ufs, and arrays

  BoolectorFormulaCreator(Long btor) {
    super(btor, BtorJNI.boolector_bool_sort(btor), null, null);
  }

  @SuppressWarnings("unchecked")
  @Override
  public <T extends Formula> FormulaType<T> getFormulaType(T pFormula) {
    if (pFormula instanceof BitvectorFormula) {
      long sort = BtorJNI.boolector_get_sort(getEnv(), extractInfo(pFormula));
      checkArgument(
          BtorJNI.boolector_is_bitvec_sort(getEnv(), sort),
          "BitvectorFormula with type missmatch: %s",
          pFormula);
      return (FormulaType<T>)
          FormulaType.getBitvectorTypeWithSize(
              BtorJNI.boolector_get_width(getEnv(), extractInfo(pFormula)));
    } else if (pFormula instanceof ArrayFormula<?, ?>) {
      FormulaType<T> arrayIndexType = getArrayFormulaIndexType((ArrayFormula<T, T>) pFormula);
      FormulaType<T> arrayElementType = getArrayFormulaElementType((ArrayFormula<T, T>) pFormula);
      return (FormulaType<T>) FormulaType.getArrayType(arrayIndexType, arrayElementType);
    }
    return super.getFormulaType(pFormula);
  }

  @Override
  public Long extractInfo(Formula pT) {
    return BoolectorFormulaManager.getBtorTerm(pT);
  }

  @Override
  public FormulaType<?> getFormulaType(Long pFormula) {
    long sort = BtorJNI.boolector_get_sort(getEnv(), pFormula);
    // Careful, Boolector interprets nearly everything as a fun!
    if (!BtorJNI.boolector_is_array_sort(getEnv(), sort)
        && !BtorJNI.boolector_is_bitvec_sort(getEnv(), sort)
        && BtorJNI.boolector_is_fun_sort(getEnv(), sort)) {
      sort = BtorJNI.boolector_fun_get_codomain_sort(getEnv(), pFormula);
    }
    return getFormulaTypeFromSortAndFormula(pFormula, sort);
  }

  /**
   * Returns the proper FormulaType for the sort entered.
   *
   * @param pFormula Some Boolector node. Either the node of the sort, or its parent. Only has to be
   *     accurate for arrays.
   * @param sort The actual sort you want the FormulaType of.
   * @return FormulaType for the sort.
   */
  private FormulaType<?> getFormulaTypeFromSortAndFormula(Long pFormula, Long sort) {
    if (BtorJNI.boolector_is_array_sort(getEnv(), sort)) {
      int indexWidth = BtorJNI.boolector_get_index_width(getEnv(), pFormula);
      int elementWidth = BtorJNI.boolector_get_width(getEnv(), pFormula);
      return FormulaType.getArrayType(
          FormulaType.getBitvectorTypeWithSize(indexWidth),
          FormulaType.getBitvectorTypeWithSize(elementWidth));
    } else if (BtorJNI.boolector_is_bitvec_sort(getEnv(), sort)) {
      int width = BtorJNI.boolector_bitvec_sort_get_width(getEnv(), sort);
      if (width == 1) {
        return FormulaType.BooleanType;
      } else {
        return FormulaType.getBitvectorTypeWithSize(width);
      }
    }
    throw new IllegalArgumentException("Unknown formula type for " + pFormula);
  }

  @SuppressWarnings("unchecked")
  @Override
  public <T extends Formula> T encapsulate(FormulaType<T> pType, Long pTerm) {
    assert pType.equals(getFormulaType(pTerm))
        : String.format(
            "Trying to encapsulate formula of type %s as %s", getFormulaType(pTerm), pType);
    if (pType.isBooleanType()) {
      return (T) new BoolectorBooleanFormula(pTerm, getEnv());
    } else if (pType.isArrayType()) {
      ArrayFormulaType<?, ?> arrFt = (ArrayFormulaType<?, ?>) pType;
      return (T)
          new BoolectorArrayFormula<>(
              pTerm, arrFt.getIndexType(), arrFt.getElementType(), getEnv());
    } else if (pType.isBitvectorType()) {
      return (T) new BoolectorBitvectorFormula(pTerm, getEnv());
    }
    throw new IllegalArgumentException(
        "Cannot create formulas of type " + pType + " in Boolector.");
  }

  @Override
  public BooleanFormula encapsulateBoolean(Long pTerm) {
    assert getFormulaType(pTerm).isBooleanType()
        : "Unexpected formula type for Boolean formula: " + getFormulaType(pTerm);
    return new BoolectorBooleanFormula(pTerm, getEnv());
  }

  @Override
  public BitvectorFormula encapsulateBitvector(Long pTerm) {
    assert getFormulaType(pTerm).isBitvectorType()
        : "Unexpected formula type for BV formula: " + getFormulaType(pTerm);
    return new BoolectorBitvectorFormula(pTerm, getEnv());
  }

  @Override
  @SuppressWarnings("MethodTypeParameterName")
  protected <TI extends Formula, TE extends Formula> ArrayFormula<TI, TE> encapsulateArray(
      Long pTerm, FormulaType<TI> pIndexType, FormulaType<TE> pElementType) {
    System.out.println("assert array");
    assert getFormulaType(pTerm).isArrayType()
        : "Unexpected formula type for array formula: " + getFormulaType(pTerm);
    return new BoolectorArrayFormula<>(pTerm, pIndexType, pElementType, getEnv());
  }

  @Override
  public Long getBitvectorType(int pBitwidth) {<commit_msg>Remove debug print<commit_after>// 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 <NAME> <https://www.sosy-lab.org>
//
// SPDX-License-Identifier: Apache-2.0

package org.sosy_lab.java_smt.solvers.boolector;

import static com.google.common.base.Preconditions.checkArgument;

import com.google.common.base.Preconditions;
import com.google.common.collect.HashBasedTable;
import com.google.common.collect.ImmutableList;
import com.google.common.collect.Table;
import com.google.common.primitives.Longs;
import java.math.BigInteger;
import java.util.ArrayList;
import java.util.HashMap;
import java.util.List;
import org.sosy_lab.java_smt.api.ArrayFormula;
import org.sosy_lab.java_smt.api.BitvectorFormula;
import org.sosy_lab.java_smt.api.BooleanFormula;
import org.sosy_lab.java_smt.api.Formula;
import org.sosy_lab.java_smt.api.FormulaType;
import org.sosy_lab.java_smt.api.FormulaType.ArrayFormulaType;
import org.sosy_lab.java_smt.api.FormulaType.FloatingPointType;
import org.sosy_lab.java_smt.api.FunctionDeclarationKind;
import org.sosy_lab.java_smt.api.visitors.FormulaVisitor;
import org.sosy_lab.java_smt.basicimpl.FormulaCreator;
import org.sosy_lab.java_smt.basicimpl.FunctionDeclarationImpl;
import org.sosy_lab.java_smt.solvers.boolector.BoolectorFormula.BoolectorArrayFormula;
import org.sosy_lab.java_smt.solvers.boolector.BoolectorFormula.BoolectorBitvectorFormula;
import org.sosy_lab.java_smt.solvers.boolector.BoolectorFormula.BoolectorBooleanFormula;

public class BoolectorFormulaCreator extends FormulaCreator<Long, Long, Long, Long> {

  // Boolector can give back 'x' for an arbitrary value that we change to this
  private static final char ARBITRARY_VALUE = '1';

  /** Maps a name and a variable or function type to a concrete formula node. */
  private final Table<String, Long, Long> nameFormulaCache = HashBasedTable.create();

  /*  Experiment: remember all variables, arrays and ufs in this map by their name.
   *  Reconstruct a model based on the smt-lib2 and this map.
   *  If this works, remove the nameFormulaCache and make this the vars cache.
   */
  private final HashMap<String, Long> nameFormulaMap = new HashMap<>();
  private final HashMap<Long, List<Long>> ufArgumentsSortMap = new HashMap<>();
  // Possibly we need to split this up into vars, ufs, and arrays

  BoolectorFormulaCreator(Long btor) {
    super(btor, BtorJNI.boolector_bool_sort(btor), null, null);
  }

  @SuppressWarnings("unchecked")
  @Override
  public <T extends Formula> FormulaType<T> getFormulaType(T pFormula) {
    if (pFormula instanceof BitvectorFormula) {
      long sort = BtorJNI.boolector_get_sort(getEnv(), extractInfo(pFormula));
      checkArgument(
          BtorJNI.boolector_is_bitvec_sort(getEnv(), sort),
          "BitvectorFormula with type missmatch: %s",
          pFormula);
      return (FormulaType<T>)
          FormulaType.getBitvectorTypeWithSize(
              BtorJNI.boolector_get_width(getEnv(), extractInfo(pFormula)));
    } else if (pFormula instanceof ArrayFormula<?, ?>) {
      FormulaType<T> arrayIndexType = getArrayFormulaIndexType((ArrayFormula<T, T>) pFormula);
      FormulaType<T> arrayElementType = getArrayFormulaElementType((ArrayFormula<T, T>) pFormula);
      return (FormulaType<T>) FormulaType.getArrayType(arrayIndexType, arrayElementType);
    }
    return super.getFormulaType(pFormula);
  }

  @Override
  public Long extractInfo(Formula pT) {
    return BoolectorFormulaManager.getBtorTerm(pT);
  }

  @Override
  public FormulaType<?> getFormulaType(Long pFormula) {
    long sort = BtorJNI.boolector_get_sort(getEnv(), pFormula);
    // Careful, Boolector interprets nearly everything as a fun!
    if (!BtorJNI.boolector_is_array_sort(getEnv(), sort)
        && !BtorJNI.boolector_is_bitvec_sort(getEnv(), sort)
        && BtorJNI.boolector_is_fun_sort(getEnv(), sort)) {
      sort = BtorJNI.boolector_fun_get_codomain_sort(getEnv(), pFormula);
    }
    return getFormulaTypeFromSortAndFormula(pFormula, sort);
  }

  /**
   * Returns the proper FormulaType for the sort entered.
   *
   * @param pFormula Some Boolector node. Either the node of the sort, or its parent. Only has to be
   *     accurate for arrays.
   * @param sort The actual sort you want the FormulaType of.
   * @return FormulaType for the sort.
   */
  private FormulaType<?> getFormulaTypeFromSortAndFormula(Long pFormula, Long sort) {
    if (BtorJNI.boolector_is_array_sort(getEnv(), sort)) {
      int indexWidth = BtorJNI.boolector_get_index_width(getEnv(), pFormula);
      int elementWidth = BtorJNI.boolector_get_width(getEnv(), pFormula);
      return FormulaType.getArrayType(
          FormulaType.getBitvectorTypeWithSize(indexWidth),
          FormulaType.getBitvectorTypeWithSize(elementWidth));
    } else if (BtorJNI.boolector_is_bitvec_sort(getEnv(), sort)) {
      int width = BtorJNI.boolector_bitvec_sort_get_width(getEnv(), sort);
      if (width == 1) {
        return FormulaType.BooleanType;
      } else {
        return FormulaType.getBitvectorTypeWithSize(width);
      }
    }
    throw new IllegalArgumentException("Unknown formula type for " + pFormula);
  }

  @SuppressWarnings("unchecked")
  @Override
  public <T extends Formula> T encapsulate(FormulaType<T> pType, Long pTerm) {
    assert pType.equals(getFormulaType(pTerm))
        : String.format(
            "Trying to encapsulate formula of type %s as %s", getFormulaType(pTerm), pType);
    if (pType.isBooleanType()) {
      return (T) new BoolectorBooleanFormula(pTerm, getEnv());
    } else if (pType.isArrayType()) {
      ArrayFormulaType<?, ?> arrFt = (ArrayFormulaType<?, ?>) pType;
      return (T)
          new BoolectorArrayFormula<>(
              pTerm, arrFt.getIndexType(), arrFt.getElementType(), getEnv());
    } else if (pType.isBitvectorType()) {
      return (T) new BoolectorBitvectorFormula(pTerm, getEnv());
    }
    throw new IllegalArgumentException(
        "Cannot create formulas of type " + pType + " in Boolector.");
  }

  @Override
  public BooleanFormula encapsulateBoolean(Long pTerm) {
    assert getFormulaType(pTerm).isBooleanType()
        : "Unexpected formula type for Boolean formula: " + getFormulaType(pTerm);
    return new BoolectorBooleanFormula(pTerm, getEnv());
  }

  @Override
  public BitvectorFormula encapsulateBitvector(Long pTerm) {
    assert getFormulaType(pTerm).isBitvectorType()
        : "Unexpected formula type for BV formula: " + getFormulaType(pTerm);
    return new BoolectorBitvectorFormula(pTerm, getEnv());
  }

  @Override
  @SuppressWarnings("MethodTypeParameterName")
  protected <TI extends Formula, TE extends Formula> ArrayFormula<TI, TE> encapsulateArray(
      Long pTerm, FormulaType<TI> pIndexType, FormulaType<TE> pElementType) {
    assert getFormulaType(pTerm).isArrayType()
        : "Unexpected formula type for array formula: " + getFormulaType(pTerm);
    return new BoolectorArrayFormula<>(pTerm, pIndexType, pElementType, getEnv());
  }

  @Override
  public Long getBitvectorType(int pBitwidth) {
{'fraction_non_alphanumeric': 0.10317848410757946, 'fraction_numerical': 0.00125742228431715, 'mean_word_length': 4.355780022446689, 'pattern_counts': {'":': 0, '<': 63, '<?xml version=': 0, '>': 63, 'https://': 4, 'lorem ipsum': 0, 'www.': 2, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 0, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
{'dir': 'git-commits-cleaned', 'id': '4671882', 'n_tokens_mistral': 4684, 'n_tokens_neox': 4739, 'n_words': 1020}