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

/*
 * This file was automatically generated by extract_java_stub.py
 * Wrapper for the MathSAT API for Java
 */
package org.sosy_lab.java_smt.solvers.mathsat5;

import com.google.common.base.Strings;
import com.google.common.collect.ImmutableSet;
import com.google.errorprone.annotations.CheckReturnValue;
import org.sosy_lab.java_smt.api.SolverException;

@SuppressWarnings({"unused", "checkstyle:methodname", "checkstyle:parametername"})
class Mathsat5NativeApi {
  private Mathsat5NativeApi() {}

  // msat_result
  private static final int MSAT_UNKNOWN = -1;
  private static final int MSAT_UNSAT = 0;
  private static final int MSAT_SAT = 1;

  // msat_truth_value
  public static final int MSAT_UNDEF = -1;
  public static final int MSAT_FALSE = 0;
  public static final int MSAT_TRUE = 1;

  /** OptiMathSAT codes for queries on objective items. */
  public static final int MSAT_OPTIMUM = 0;

  public static final int MSAT_FINAL_LOWER = 1;
  public static final int MSAT_FINAL_UPPER = 2;
  public static final int MSAT_FINAL_ERROR = 3;

  /** OptiMathSAT objective type, either minimize or maximize. */
  public static final int MSAT_OBJECTIVE_MINIMIZE = -1;

  public static final int MSAT_OBJECTIVE_MAXIMIZE = 1;

  /** MathSAT tags. */
  public static final int MSAT_TAG_ERROR = -1;

  public static final int MSAT_TAG_UNKNOWN = 0;
  public static final int MSAT_TAG_TRUE = 1; // < the Boolean constant True
  public static final int MSAT_TAG_FALSE = 2; // < the Boolean constant False
  public static final int MSAT_TAG_AND = 3; // < the AND Boolean connective
  public static final int MSAT_TAG_OR = 4; // < the OR Boolean connective
  public static final int MSAT_TAG_NOT = 5; // < the NOT Boolean connective
  public static final int MSAT_TAG_IFF = 6; // < the IFF Boolean connective
  public static final int MSAT_TAG_PLUS = 7; // < arithmetic addition
  public static final int MSAT_TAG_TIMES = 8; // < arithmetic multiplication
  public static final int MSAT_TAG_DIVIDE = 9; // < arithmetic multiplication
  public static final int MSAT_TAG_FLOOR = 10; // < floor function
  public static final int MSAT_TAG_LEQ = 11; // < arithmetic <=
  public static final int MSAT_TAG_EQ = 12; // < equality
  public static final int MSAT_TAG_ITE = 13; // < term-level if-then-else
  public static final int MSAT_TAG_INT_MOD_CONGR = 14; // < integer modular congruence
  public static final int MSAT_TAG_BV_CONCAT = 15; // < BV concatenation
  public static final int MSAT_TAG_BV_EXTRACT = 16; // < BV selection
  public static final int MSAT_TAG_BV_NOT = 17; // < BV bitwise not
  public static final int MSAT_TAG_BV_AND = 18; // < BV bitwise and
  public static final int MSAT_TAG_BV_OR = 19; // < BV bitwise or
  public static final int MSAT_TAG_BV_XOR = 20; // < BV bitwise xor
  public static final int MSAT_TAG_BV_ULT = 21; // < BV unsigned <
  public static final int MSAT_TAG_BV_SLT = 22; // < BV signed <
  public static final int MSAT_TAG_BV_ULE = 23; // < BV unsigned <=
  public static final int MSAT_TAG_BV_SLE = 24; // < BV signed <
  public static final int MSAT_TAG_BV_COMP = 25; // < BV bit comparison
  public static final int MSAT_TAG_BV_NEG = 26; // < BV unary minus
  public static final int MSAT_TAG_BV_ADD = 27; // < BV addition
  public static final int MSAT_TAG_BV_SUB = 28; // < BV subtraction
  public static final int MSAT_TAG_BV_MUL = 29; // < BV multiplication
  public static final int MSAT_TAG_BV_UDIV = 30; // < BV unsigned division
  public static final int MSAT_TAG_BV_SDIV = 31; // < BV signed division
  public static final int MSAT_TAG_BV_UREM = 32; // < BV unsigned remainder
  public static final int MSAT_TAG_BV_SREM = 33; // < BV signed remainder
  public static final int MSAT_TAG_BV_LSHL = 34; // < BV logical left shift
  public static final int MSAT_TAG_BV_LSHR = 35; // < BV logical right shift
  public static final int MSAT_TAG_BV_ASHR = 36; // < BV arithmetic right shift
  public static final int MSAT_TAG_BV_ROL = 37; // < BV rotate left
  public static final int MSAT_TAG_BV_ROR = 38; // < BV rotate right
  public static final int MSAT_TAG_BV_ZEXT = 39; // < BV zero extension
  public static final int MSAT_TAG_BV_SEXT = 40; // < BV sign extension
  public static final int MSAT_TAG_ARRAY_READ = 41; // < Array read/select operation
  public static final int MSAT_TAG_ARRAY_WRITE = 42; // < Array write/store operation
  public static final int MSAT_TAG_ARRAY_CONST = 43; // < Constant arrays
  public static final int MSAT_TAG_FP_EQ = 44; // < FP IEEE equality
  public static final int MSAT_TAG_FP_LT = 45; // < FP <
  public static final int MSAT_TAG_FP_LE = 46; // < FP <=
  public static final int MSAT_TAG_FP_NEG = 47; // < FP unary minus
  public static final int MSAT_TAG_FP_ADD = 48; // < FP addition
  public static final int MSAT_TAG_FP_SUB = 49; // < FP subtraction
  public static final int MSAT_TAG_FP_MUL = 50; // < FP multiplication
  public static final int MSAT_TAG_FP_DIV = 51; // < FP division
  public static final int MSAT_TAG_FP_SQRT = 52; // < FP square root
  public static final int MSAT_TAG_FP_ABS = 53; // < FP absolute value
  public static final int MSAT_TAG_FP_MIN = 54; // < FP min
  public static final int MSAT_TAG_FP_MAX = 55; // < FP max
  public static final int MSAT_TAG_FP_CAST = 56; // < FP format conversion
  public static final int MSAT_TAG_FP_ROUND_TO_INT = 57; // < FP round to integer
  public static final int MSAT_TAG_FP_FROM_SBV = 58; // < FP conversion from a signed BV
  public static final int MSAT_TAG_FP_FROM_UBV = 59; // < FP conversion from an unsigned BV
  public static final int MSAT_TAG_FP_TO_SBV = 60; // < FP conversion to BV
  public static final int MSAT_TAG_FP_TO_UBV = 61; // < FP conversion to BV
  public static final int MSAT_TAG_FP_AS_IEEEBV = 62; // < FP as IEEE BV (access to the bits)
  public static final int MSAT_TAG_FP_ISNAN = 63; // < FP check for NaN
  public static final int MSAT_TAG_FP_ISINF = 64; // < FP check for infinity
  public static final int MSAT_TAG_FP_ISZERO = 65; // < FP check for zero
  public static final int MSAT_TAG_FP_ISSUBNORMAL = 66; // < FP check for subnormal
  public static final int MSAT_TAG_FP_ISNORMAL = 67; // < FP check for normal
  public static final int MSAT_TAG_FP_ISNEG = 68; // < FP check for negative
  public static final int MSAT_TAG_FP_ISPOS = 69; // < FP check for positive
  public static final int MSAT_TAG_FP_FROM_IEEEBV = 70; // < FP conversion from IEEE BV
  public static final int MSAT_TAG_INT_FROM_UBV = 71; // < Unsigned BV -> INT conversion
  public static final int MSAT_TAG_INT_FROM_SBV = 72; // < Signed BV -> INT conversion
  public static final int MSAT_TAG_INT_TO_BV = 73; // < INT -> BV conversion
  public static final int MSAT_TAG_PI = 74; // Pi constant
  public static final int MSAT_TAG_EXP = 75; // Exponential function
  public static final int MSAT_TAG_SIN = 76; // Sine function
  public static final int MSAT_TAG_LOG = 77; // Natural logarithm function
  public static final int MSAT_TAG_POW = 78;
  public static final int MSAT_TAG_ASIN = 79;
  public static final int MSAT_TAG_FORALL = 80;
  public static final int MSAT_TAG_EXISTS = 81;

  interface AllSatModelCallback {

    void callback(long[] model) throws InterruptedException;
  }

  interface TerminationCallback {
    boolean shouldTerminate() throws InterruptedException;
  }

  // wrappers for some native methods with a different number of arguments
  public static int msat_all_sat(long e, long[] important, AllSatModelCallback func)
      throws InterruptedException {

    return msat_all_sat(e, important, important.length, func);
  }

  /**
   * Solve environment and check for satisfiability. Return true if sat, false if unsat.
   *
   * @throws SolverException if a mathsat problem occured
   * @throws IllegalStateException in all other problematic cases
   */
  public static boolean msat_check_sat(long e)
      throws InterruptedException, IllegalStateException, SolverException {
    return processSolveResult(e, msat_solve(e));
  }

  public static boolean msat_check_sat_with_assumptions(long e, long[] assumptions)
      throws InterruptedException, IllegalStateException, SolverException {
    return processSolveResult(e, msat_solve_with_assumptions(e, assumptions, assumptions.length));
  }

  private static final ImmutableSet<String> ALLOWED_SOLVE_FAILURE_MESSAGES =
      ImmutableSet.of(
          "unsupported",
          "unimplemented",
          "can't produce proofs",
          "non-integer model value",
          "build_model: too many iterations",
          "eager fp solver does not support proof generation",
          "FP<->BV combination unsupported by the current configuration");

  private static boolean processSolveResult(long e, int resultCode)
      throws IllegalStateException, SolverException {
    switch (resultCode) {
      case MSAT_SAT:
        return true;
      case MSAT_UNSAT:
        return false;
      default:
        String msg = Strings.emptyToNull(msat_last_error_message(e));

        if (ALLOWED_SOLVE_FAILURE_MESSAGES.contains(msg)) {
          // This is not a bug in our code, but a problem of MathSAT
          throw new SolverException(msg);
        }

        String code = (resultCode == MSAT_UNKNOWN) ? "\"unknown\"" : String.valueOf(resultCode);
        throw new IllegalStateException(
            "msat_solve returned " + code + (msg != null ? ": " + msg : ""));
    }
  }

  static class NamedTermsWrapper {
    final long[] terms;
    final String[] names;

    NamedTermsWrapper(long[] pTerms, String[] pNames) {
      terms = pTerms;
      names = pNames;
    }
  }

  public static long msat_get_interpolant(long e, int[] groups_of_a) {
    return msat_get_interpolant(e, groups_of_a, groups_of_a.length);
  }

  /*
   * Environment creation
   */
  public static native long msat_create_config();

  public static native void msat_destroy_config(long cfg);

  public static native long msat_create_env(long cfg);

  public static native long msat_create_shared_env(long cfg, long sibling);

  public static native void msat_destroy_env(long e);

  @CheckReturnValue
  private static native int msat_set_option(long cfg, String option, String value);

  public static void msat_set_option_checked(long cfg, String option, String value)
      throws IllegalArgumentException {
    int retval = msat_set_option(cfg, option, value);
    if (retval != 0) {
      throw new IllegalArgumentException(
          "Could not set Mathsat option \"" + option + "=" + value + "\", error code " + retval);
    }
  }

  public static native long msat_get_bool_type(long e);

  public static native long msat_get_rational_type(long e);

  public static native long msat_get_integer_type(long e);

  public static native long msat_get_bv_type(long e, int size);

  public static native long msat_get_array_type(long e, long itp, long etp);

  public static native long msat_get_array_index_type(long e, long t);

  public static native long msat_get_array_element_type(long e, long t);

  public static native long msat_get_fp_type(long e, int exp_with, int mant_with);

  public static native long msat_get_fp_roundingmode_type(long e);

  public static native long msat_get_simple_type(long e, String name);

  public static native long msat_get_function_type(
      long e, long[] paramTypes, int size, long returnType);

  public static native long msat_get_enum_type(long e, String name, int size, String[] elements);

  public static native boolean msat_is_bool_type(long e, long t);

  public static native boolean msat_is_rational_type(long e, long t);

  public static native boolean msat_is_integer_type(long e, long t);

  public static native boolean msat_is_bv_type(long e, long t);

  public static native int msat_get_bv_type_size(long e, long t);

  public static native boolean msat_is_array_type(long e, long t);

  public static native boolean msat_is_fp_type(long e, long t);

  public static native int msat_get_fp_type_exp_width(long e, long t);

  public static native int msat_get_fp_type_mant_width(long e, long t);

  public static native boolean msat_is_fp_roundingmode_type(long e, long t);

  public static native boolean msat_is_enum_type(long e, long t);

  public static native long[] msat_get_enum_constants(long e, long t);

  public static native boolean msat_type_equals(long t1, long t2);

  public static native String msat_type_repr(long t);

  public static native long msat_declare_function(long e, String name, long t);

  /*
   * Term creation
   */
  public static native long msat_make_true(long e);

  public static native long msat_make_false(long e);

  public static native long msat_make_iff(long e, long t1, long t2);

  public static native long msat_make_or(long e, long t1, long t2);

  public static native long msat_make_and(long e, long t1, long t2);

  public static native long msat_make_not(long e, long t1);

  public static native long msat_make_equal(long e, long t1, long t2);

  public static native long msat_make_eq(long e, long t1, long t2);

  public static native long msat_make_leq(long e, long t1, long t2);

  public static native long msat_make_plus(long e, long t1, long t2);

  public static native long msat_make_times(long e, long t1, long t2);

  public static native long msat_make_divide(long e, long t1, long t2);

  public static native long msat_make_floor(long e, long t);

  public static native long msat_make_pi(long e);

  public static native long msat_make_exp(long e, long t);

  public static native long msat_make_sin(long e, long t);

  public static native long msat_make_log(long e, long t);

  public static native long msat_make_pow(long e, long tb, long te);

  public static native long msat_make_asin(long e, long t);

  public static native long msat_make_number(long e, String num_rep);

  public static native long msat_make_int_number(long e, int value);

  public static native long msat_make_int_modular_congruence(
      long e, String modulo, long t1, long t2);

  public static native long msat_make_term_ite(long e, long c, long tt, long te);

  public static native long msat_make_constant(long e, long var);

  public static native long msat_make_uf(long e, long func, long[] args);

  public static native long msat_make_array_read(long e, long arr, long idx);

  public static native long msat_make_array_write(long e, long arr, long idx, long elem);

  public static native long msat_make_array_const(long e, long arrayType, long elem);

  public static native long msat_make_int_to_bv(long e, int width, long t);

  public static native long msat_make_int_from_ubv(long e, long t);

  public static native long msat_make_int_from_sbv(long e, long t);

  public static native long msat_make_forall(long e, long var, long body);

  public static native long msat_make_exists(long e, long var, long body);

  public static native long msat_make_variable(long e, String name, long type);

  public static long msat_existentially_quantify(long env, long term, long[] args) {
    return msat_existentially_quantify(env, term, args, args.length);
  }

  public static native long msat_existentially_quantify(long e, long t, long[] args, int n);

  public static native long msat_make_bv_number(long e, String numRep, int width, int base);

  public static native long msat_make_bv_int_number(long e, int value, int width);

  public static native long msat_make_bv_concat(long e, long t1, long t2);

  /**
   * Returns a term representing the selection of t[msb:lsb].
   *
   * @param e The environment of the definition
   * @param msb The most significant bit of the selection.
   * @param lsb The least significant bit of the selection.
   * @param t The argument.
   * @return a term representing the selection of t[msb:lsb].
   */
  public static native long msat_make_bv_extract(long e, int msb, int lsb, long t);

  public static native long msat_make_bv_or(long e, long t1, long t2);

  public static native long msat_make_bv_xor(long e, long t1, long t2);

  public static native long msat_make_bv_and(long e, long t1, long t2);

  public static native long msat_make_bv_not(long e, long t);

  public static native long msat_make_bv_lshl(long e, long t1, long t2);

  public static native long msat_make_bv_lshr(long e, long t1, long t2);

  public static native long msat_make_bv_ashr(long e, long t1, long t2);

  public static native long msat_make_bv_zext(long e, int amount, long t);

  public static native long msat_make_bv_sext(long e, int amount, long t);

  public static native long msat_make_bv_plus(long e, long t1, long t2);

  public static native long msat_make_bv_minus(long e, long t1, long t2);

  public static native long msat_make_bv_neg(long e, long t);

  public static native long msat_make_bv_times(long e, long t1, long t2);

  public static native long msat_make_bv_udiv(long e, long t1, long t2);

  public static native long msat_make_bv_urem(long e, long t1, long t2);

  public static native long msat_make_bv_sdiv(long e, long t1, long t2);

  public static native long msat_make_bv_srem(long e, long t1, long t2);

  public static native long msat_make_bv_ult(long e, long t1, long t2);

  public static native long msat_make_bv_uleq(long e, long t1, long t2);

  public static native long msat_make_bv_slt(long e, long t1, long t2);

  public static native long msat_make_bv_sleq(long e, long t1, long t2);

  public static native long msat_make_bv_rol(long e, int size, long t);

  public static native long msat_make_bv_ror(long e, int size, long t);

  public static native long msat_make_bv_comp(long e, long t1, long t2);

  public static native long msat_make_fp_roundingmode_nearest_even(long e);

  public static native long msat_make_fp_roundingmode_zero(long e);

  public static native long msat_make_fp_roundingmode_plus_inf(long e);

  public static native long msat_make_fp_roundingmode_minus_inf(long e);

  public static native long msat_make_fp_equal(long e, long t1, long t2);

  public static native long msat_make_fp_lt(long e, long t1, long t2);

  public static native long msat_make_fp_leq(long e, long t1, long t2);

  public static native long msat_make_fp_neg(long e, long t);

  public static native long msat_make_fp_plus(long e, long rounding, long t1, long t2);

  public static native long msat_make_fp_minus(long e, long rounding, long t1, long t2);

  public static native long msat_make_fp_times(long e, long rounding, long t1, long t2);

  public static native long msat_make_fp_div(long e, long rounding, long t1, long t2);

  public static native long msat_make_fp_sqrt(long e, long rounding, long t);

  public static native long msat_make_fp_abs(long e, long t);

  public static native long msat_make_fp_max(long e, long t1, long t2);

  public static native long msat_make_fp_min(long e, long t1, long t2);

  public static native long msat_make_fp_round_to_int(long e, long rounding, long t);

  public static native long msat_make_fp_cast(
      long e, long exp_w, long mant_w, long rounding, long t);

  public static native long msat_make_fp_to_sbv(long e, long width, long rounding, long t);

  public static native long msat_make_fp_to_ubv(long e, long width, long rounding, long t);

  public static native long msat_make_fp_from_sbv(
      long e, long exp_w, long mant_w, long rounding, long t);

  public static native long msat_make_fp_from_ubv(
      long e, long exp_w, long mant_w, long rounding, long t);

  public static native long msat_make_fp_as_ieeebv(long e, long t);

  public static native long msat_make_fp_from_ieeebv(long e, long exp_w, long mant_w, long t);

  public static native long msat_make_fp_isnan(long e, long t);

  public static native long msat_make_fp_isinf(long e, long t);

  public static native long msat_make_fp_iszero(long e, long t);

  public static native long msat_make_fp_issubnormal(long e, long t);

  public static native long msat_make_fp_isnormal(long e, long t);

  public static native long msat_make_fp_isneg(long e, long t);

  public static native long msat_make_fp_ispos(long e, long t);

  public static native long msat_make_fp_plus_inf(long e, long exp_w, long mant_w);

  public static native long msat_make_fp_minus_inf(long e, long exp_w, long mant_w);

  public static native long msat_make_fp_nan(long e, long exp_w, long mant_w);

  public static native long msat_make_fp_rat_number(
      long e, String numRep, long exp_w, long mant_w, long rounding);

  public static native long msat_make_fp_bits_number(
      long e, String bitRep, long exp_w, long mant_w);

  /**
   * Creates a term from a declaration and a list of arguments.
   *
   * <p>Precondition: The length of {@code args} should be equal to the arity of {@code d}
   *
   * @param e msat_env The environment in which to create the term
   * @param d msat_decl The declaration
   * @param args msat_term[] The arguments
   * @return msat_term The created term, or a t s.t. ::MSAT_ERROR_TERM(t) is true in case of errors.
   */
  public static native long msat_make_term(long e, long d, long[] args);

  public static native long msat_make_copy_from(long e, long t, long src);

  public static native long msat_apply_substitution(long e, long t, int s, long[] from, long[] to);

  public static long msat_simplify(long env, long formula, long[] to_protect) {
    return msat_simplify(env, formula, to_protect, to_protect.length);
  }

  public static native long msat_simplify(
      long e, long formula, long[] to_protect, int num_to_protect);

  /*
   * Term access and navigation
   */
  public static native int msat_term_id(long t);

  public static native int msat_term_arity(long t);

  public static native long msat_term_get_arg(long t, int n);

  public static native long msat_term_get_type(long t);

  public static native boolean msat_term_is_true(long e, long t);

  public static native boolean msat_term_is_false(long e, long t);

  public static native boolean msat_term_is_boolean_constant(long e, long t);

  public static native boolean msat_term_is_atom(long e, long t);

  public static native boolean msat_term_is_number(long e, long t);

  public static native boolean msat_term_is_and(long e, long t);

  public static native boolean msat_term_is_or(long e, long t);

  public static native boolean msat_term_is_not(long e, long t);

  public static native boolean msat_term_is_iff(long e, long t);

  public static native boolean msat_term_is_term_ite(long e, long t);

  public static native boolean msat_term_is_constant(long e, long t);

  public static native boolean msat_term_is_uf(long e, long t);

  public static native boolean msat_term_is_equal(long e, long t);

  public static native boolean msat_term_is_leq(long e, long t);

  public static native boolean msat_term_is_plus(long e, long t);

  public static native boolean msat_term_is_times(long e, long t);

  public static native boolean msat_term_is_divide(long e, long t);

  public static native boolean msat_term_is_floor(long e, long t);

  public static native boolean msat_term_is_pi(long e, long t);

  public static native boolean msat_term_is_exp(long e, long t);

  public static native boolean msat_term_is_sin(long e, long t);

  public static native boolean msat_term_is_log(long e, long t);

  public static native boolean msat_term_is_pow(long e, long t);

  public static native boolean msat_term_is_asin(long e, long t);

  public static native boolean msat_term_is_array_read(long e, long t);

  public static native boolean msat_term_is_array_write(long e, long t);

  public static native boolean msat_term_is_array_const(long e, long t);

  public static native boolean msat_term_is_int_to_bv(long e, long t);

  public static native boolean msat_term_is_int_from_ubv(long e, long t);

  public static native boolean msat_term_is_int_from_sbv(long e, long t);

  public static native boolean msat_term_is_bv_concat(long e, long t);

  public static native boolean msat_term_is_bv_extract(long e, long t);

  public static native boolean msat_term_is_bv_or(long e, long t);

  public static native boolean msat_term_is_bv_xor(long e, long t);

  public static native boolean msat_term_is_bv_and(long e, long t);

  public static native boolean msat_term_is_bv_not(long e, long t);

  public static native boolean msat_term_is_bv_plus(long e, long t);

  public static native boolean msat_term_is_bv_minus(long e, long t);

  public static native boolean msat_term_is_bv_times(long e, long t);

  public static native boolean msat_term_is_bv_neg(long e, long t);

  public static native boolean msat_term_is_bv_udiv(long e, long t);

  public static native boolean msat_term_is_bv_urem(long e, long t);

  public static native boolean msat_term_is_bv_sdiv(long e, long t);

  public static native boolean msat_term_is_bv_srem(long e, long t);

  public static native boolean msat_term_is_bv_ult(long e, long t);

  public static native boolean msat_term_is_bv_uleq(long e, long t);

  public static native boolean msat_term_is_bv_slt(long e, long t);

  public static native boolean msat_term_is_bv_sleq(long e, long t);

  public static native boolean msat_term_is_bv_lshl(long e, long t);

  public static native boolean msat_term_is_bv_lshr(long e, long t);

  public static native boolean msat_term_is_bv_ashr(long e, long t);

  public static native boolean msat_term_is_bv_zext(long e, long t);

  public static native boolean msat_term_is_bv_sext(long e, long t);

  public static native boolean msat_term_is_bv_rol(long e, long t);

  public static native boolean msat_term_is_bv_ror(long e, long t);

  public static native boolean msat_term_is_bv_comp(long e, long t);

  public static native boolean msat_term_is_quantifier(long e, long t);

  public static native boolean msat_term_is_forall(long e, long t);

  public static native boolean msat_term_is_exists(long e, long t);

  public static native boolean msat_term_is_variable(long e, long t);

  // public static native int msat_visit_term(long e, msat_visit_term_callback func)
  public static native long msat_find_decl(long e, String symbol);

  /**
   * Returns the declaration associated to {@code t} (if any).
   *
   * <p>If {@code t} is not a constant or a function application, the returned value \a ret will be
   * s.t. MSAT_ERROR_DECL(ret) is true
   *
   * @param t msat_term The term for which to retrieve the declaration
   * @return msat_decl If {@code t} is a constant, its declaration is returned; if it is an uif, the
   *     declaration of the function is returned; otherwise, a {@code ret} s.t. MSAT_ERROR_DECL(ret)
   *     is true is returned
   */
  public static native long msat_term_get_decl(long t);

  public static native int msat_decl_id(long d);

  public static native long msat_decl_get_return_type(long d);

  /**
   * @param env msat_env
   * @param d msat_decl
   * @return msat_symbol_tag
   */
  public static native int msat_decl_get_tag(long env, long d);

  public static native int msat_decl_get_arity(long d);

  public static native long msat_decl_get_arg_type(long d, int n);

  public static native String msat_decl_repr(long d);

  public static native String msat_decl_get_name(long d);

  public static native String msat_term_repr(long t);

  /*
   * Parsing and writing formulas.
   */
  public static native long msat_from_string(long e, String data);

  public static native long msat_from_smtlib1(long e, String data);

  public static native long msat_from_smtlib2(long e, String data);

  public static native String msat_to_smtlib1(long e, long t);

  public static native String msat_to_smtlib2(long e, long t);

  public static native String msat_to_smtlib2_term(long e, long t);

  public static native String msat_named_list_to_smtlib2(long e, NamedTermsWrapper w);

  public static native NamedTermsWrapper msat_named_list_from_smtlib2(long e, String s);

  /*
   * Problem solving
   */
  public static native void msat_push_backtrack_point(long e);

  public static native void msat_pop_backtrack_point(long e);

  public static native int msat_num_backtrack_points(long e);

  public static native void msat_reset_env(long e);

  public static native void msat_assert_formula(long e, long formula);

  // public static native int msat_add_preferred_for_branching(long e, long termBoolvar);
  // public static native int msat_clear_preferred_for_branching(long e)
  private static native int msat_solve(long e) throws InterruptedException;

  private static native int msat_solve_with_assumptions(
      long e, long[] assumptions, int numAssumptions) throws InterruptedException;

  private static native int msat_all_sat(
      long e, long[] important, int num_important, AllSatModelCallback func)
      throws InterruptedException;

  public static native long[] msat_get_asserted_formulas(long e);

  public static native long[] msat_get_theory_lemmas(long e);

  /*
   * Interpolation
   */
  public static native int msat_create_itp_group(long e);

  public static native void msat_set_itp_group(long e, int group);

  private static native long msat_get_interpolant(long e, int[] groups_of_a, int n);

  /*
   * Model computation
   */
  public static native long msat_get_model_value(long e, long term);

  public static native long msat_get_model(long e);

  public static native void msat_destroy_model(long model);

  public static native long msat_model_create_iterator(long model);

  /**
   * Evaluates the input term in the given model.
   *
   * @param model msat_model The model used for the evaluation.
   * @param term msat_term The term to evaluate.
   * @return the value for {@code t} in {@code m}. Use MSAT_ERROR_TERM() to check for errors.
   */
  public static native long msat_model_eval(long model, long term);

  private static native long msat_create_model_iterator(long e);

  public static native boolean msat_model_iterator_has_next(long i);

  public static native boolean msat_model_iterator_next(long i, long[] t, long[] v);

  public static native void msat_destroy_model_iterator(long i);

  /*
   * Unsat core computation
   */
  public static native long[] msat_get_unsat_assumptions(long e);

  public static native long[] msat_get_unsat_core(long e);

  /*
   * Special functions
   */
  public static native long msat_set_termination_callback(long e, TerminationCallback callback);

  public static native void msat_free_termination_callback(long t);

  public static native String msat_get_version();

  public static native String msat_get_version_id();

  public static native String msat_last_error_message(long e);

  /* Optimization **/

  /*
   * OptiMathSAT - environment creation
   */

  public static native long msat_create_opt_env(long cfg);

  public static native long msat_create_shared_opt_env(long cfg, long sibling);

  /*
   * OptiMathSAT - objectives creation
   */

  /**
   * Create new objective 'min(term)' with optional optimization local interval [lower, upper[. Push
   * onto the stack using assert_objective.
   *
   * @param e msat_env The environment in which to operate.
   * @param term msat_term The term to be minimized.
   */
  public static native long msat_make_minimize(long e, long term);

  public static native long msat_make_minimize_signed(long e, long term);

  /**
   * Create the new objective 'max(term)' with optional optimization local interval ]local, upper].
   * Push onto the stack using assert_objective .
   *
   * @param e msat_env The environment in which to operate.
   * @param term msat_term The term to be maximized.
   */
  public static native long msat_make_maximize(long e, long term);

  public static native long msat_make_maximize_signed(long e, long term);

  /**
   * Create the new objective 'min(max(term0), ..., max(termN))' with optional optimization local
   * interval ]lower, upper]. Push onto the stack using assert_objective
   *
   * @param e msat_env The environment in which to operate.
   * @param len size_t The size of terms.
   * @param terms msat_term[] The array of terms to be optimized.
   */
  public static native long msat_make_minmax(long e, int len, long[] terms);

  public static native long msat_make_minmax_signed(long e, int len, long[] terms);

  /**
   * Create the new objective 'max(min(term0), ..., min(termN))' with optional optimization local
   * interval [lower, upper[. Push onto the stack using assert_objective
   *
   * @param e msat_env The environment in which to operate.
   * @param len size_t The size of terms.
   * @param terms msat_term[] The array of terms to be optimized.
   */
  public static native long msat_make_maxmin(long e, int len, long[] terms);

  public static native long msat_make_maxmin_signed(long e, int len, long[] terms);

  /**
   * \brief Associate a weight to a term declaration with respect to a MaxSMT group identified by a
   * common id label. Assert-soft constraints are ineffective unless the id label is used by an
   * objective that is pushed on the stack.
   *
   * <p>\param e msat_env The environment in which to operate. \param term msat_term The term to
   * which a weight is attached. \param weight msat_term The weight of not satisfying this
   * soft-clause. \param upper The MaxSMT sum onto which the weight contribution is added.
   */
  public static native void msat_assert_soft_formula(long e, long term, long weight, String id);

  /**
   * Returns general search statistics.
   *
   * @param e msat_env The environment in which to operate.
   * @return A string which provides some search statistics information on the search.
   */
  public static native String msat_get_search_stats(long e);

  /*
   * OptiMathSAT - objective stack iterator
   */

  /**
   * Creates an objective iterator NOTE: an objective iterator, and any of its references, should
   * only be instantiated after a ::msat_solve call, and prior to any further
   * push/pop/assert_formula action. Otherwise, the behaviour is undefined.
   *
   * @param e msat_env The environment in use
   * @return msat_objective_iterator an iterator for the current objectives
   */
  public static native long msat_create_objective_iterator(long e);

  /**
   * Checks whether {@code i} can be incremented.
   *
   * @param i msat_objective_iterator An objective iterator
   * @return nonzero if \a i can be incremented, zero otherwise
   */
  public static native int msat_objective_iterator_has_next(long i);

  /**
   * Returns the next objective, and increments the given iterator.
   *
   * @param i msat_objective_iterator The objective iterator to increment.
   * @param o msat_objective* Output value for the next objective in the stack.
   * @return nonzero in case of error.
   */
  public static native int msat_objective_iterator_next(long i, long[] o);

  /**
   * Destroys an objective iterator.
   *
   * @param i msat_objective_iterator the iterator to destroy.
   */
  public static native void msat_destroy_objective_iterator(long i);

  /*
   * OptiMathSAT - functions for objective state inspection
   */

  /**
   * Returns the optimization search state of the given objective.
   *
   * @param e msat_env The environment in which to operate.
   * @param o msat_objective The objective.
   * @return msat_result ::MSAT_SAT if objective has a solution, ::MSAT_UNSAT if objective is
   *     unsatisfiable, and ::MSAT_UNKNOWN if there was some error or if satisfiability/optimality
   *     could not be determined.
   */
  public static native int msat_objective_result(long e, long o);

  /**
   * Returns the term which is optimized by the objective.
   *
   * @param e msat_env The environment in which to operate.
   * @param o msat_objective The objective.
   * @return msat_term representation of the objective function
   */
  public static native long msat_objective_get_term(long e, long o);

  /**
   * Returns the objective optimization type (min or max).
   *
   * @param e msat_env The environment in which to operate.
   * @param o msat_objective The objective.
   * @return msat_objective_type ::MSAT_OBJECTIVE_MINIMIZE or ::MSAT_OBJECTIVE_MAXIMIZE
   */
  public static native long msat_objective_get_type(long e, long o);

  /**
   * Load into memory the model associated with the given objective, provided that it is
   * satisfiable.
   *
   * @param e msat_env The environment in which to operate.
   * @param o msat_objective The objective providing the model.
   */
  public static native void msat_load_objective_model(long e, long o);

  /**
   * Returns optimization search statistics.
   *
   * @return A string which provides some search statistics information on the optimization search
   *     of the given objective. The string must be deallocated by the user with ::msat_free().
   */
  public static native String msat_objective_get_search_stats(long e, long o);

  /**
   * Determines if the given objective value is unbounded.
   *
   * @param e msat_env The environment in which to operate.
   * @param o msat_objective The objective providing the value.
   * @param i msat_objective_value The objective field to be tested.
   * @return 1 if unbounded, 0 if not, -1 on error.
   */
  public static native int msat_objective_value_is_unbounded(long e, long o, int i);

  /**
   * Determines if the given objective value is +INF.
   *
   * @param e msat_env The environment in which to operate.
   * @param o msat_objective The objective providing the value.
   * @param i msat_objective_value The objective field to be tested.
   * @return 1 if +INF, 0 if not, -1 on error.
   */
  public static native int msat_objective_value_is_plus_inf(long e, long o, int i);

  /**
   * Determines if the given objective value is -INF.
   *
   * @param e msat_env The environment in which to operate.
   * @param o msat_objective The objective providing the value.
   * @param i msat_objective_value The objective field to be tested.
   * @return 1 if -INF, 0 if not, -1 on error.
   */
  public static native int msat_objective_value_is_minus_inf(long e, long o, int i);

  /**
   * Determines if the given objective value is strict, (e.g. if term(i) = k and strict(i) = TRUE,
   * then actual value of 'i' is k+epsilon, with epsilon being any small positive value).
   *
   * @param e msat_env The environment in which to operate.
   * @param o msat_objective The objective providing the value.
   * @param i msat_objective_value The objective field to be tested.
   * @return 1 if strict, 0 if not, -1 on error.
   */
  public static native int msat_objective_value_is_strict(long e, long o, int i);

  /**
   * Returns term representation of the given objective value. NOTE: the representation IS imprecise
   * if objective value is strict.
   *
   * @param e msat_env The environment in which to operate.
   * @param o msat_objective The objective providing the value.
   * @param i msat_objective_value The objective field to retrieve.
   * @param fin The symbol / positive value representing infinity. If equal to NULL
   *     (MSAT_ERROR_TERM), OptiMathSAT picks his own value.
   * @param eps The symbol / positive value representing epsilon. If equal to NULL
   *     (MSAT_ERROR_TERM), OptiMathSAT picks his own value.
   * @return msat_term term associated to the objective value, or msat_error_term on error.
   */
  public static native long msat_objective_value_term(long e, long o, int i, long fin, long eps);

  /**
   * Performs garbage collection on the given environment.
   *
   * <p>This function will perform garbage collection on the given environment. All the internal
   * caches of the environment will be cleared (including those in the active solvers and
   * preprocessors). If the environment is not shared, all the terms that are not either in {@code
   * tokeep} or in the current asserted formulas will be deleted.
   *
   * @param env msat_env The environment in which to operate.
   * @param tokeep List of terms to not delete.
   * @param num_tokeep Size of the {@code tokeep} array.
   * @return zero on success, nonzero on error.
   */
  private static native int msat_gc_env(long env, long[] tokeep, int num_tokeep);

  /**
   * Push objective on stack.
   *
   * @param e msat_env The environment in which to operate.
   * @param o msat_objective to push on the stack
   */
  public static native void msat_assert_objective(long e, long o);
}
