<commit_before>/*
 *  JavaSMT is an API wrapper for a collection of SMT solvers.
 *  This file is part of JavaSMT.
 *
 *  Copyright (C) 2007-2016  <NAME>
 *  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.
 */
/*
 * 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.CanIgnoreReturnValue;
import javax.annotation.CheckReturnValue;
import javax.annotation.Nullable;
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_INITIAL_LOWER = 1;
  public static final int MSAT_INITIAL_UPPER = 2;
  public static final int MSAT_FINAL_LOWER = 3;
  public static final int MSAT_FINAL_UPPER = 4;
  public static final int MSAT_FINAL_ERROR = 5;

  /** 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_FLOOR = 9; // < floor function
  public static final int MSAT_TAG_LEQ = 10; // < arithmetic <=
  public static final int MSAT_TAG_EQ = 11; // < equality
  public static final int MSAT_TAG_ITE = 12; // < term-level if-then-else
  public static final int MSAT_TAG_INT_MOD_CONGR = 13; // < integer modular congruence
  public static final int MSAT_TAG_BV_CONCAT = 14; // < BV concatenation
  public static final int MSAT_TAG_BV_EXTRACT = 15; // < BV selection
  public static final int MSAT_TAG_BV_NOT = 16; // < BV bitwise not
  public static final int MSAT_TAG_BV_AND = 17; // < BV bitwise and
  public static final int MSAT_TAG_BV_OR = 18; // < BV bitwise or
  public static final int MSAT_TAG_BV_XOR = 19; // < BV bitwise xor
  public static final int MSAT_TAG_BV_ULT = 20; // < BV unsigned <
  public static final int MSAT_TAG_BV_SLT = 21; // < BV signed <
  public static final int MSAT_TAG_BV_ULE = 22; // < BV unsigned <=
  public static final int MSAT_TAG_BV_SLE = 23; // < BV signed <
  public static final int MSAT_TAG_BV_COMP = 24; // < BV bit comparison
  public static final int MSAT_TAG_BV_NEG = 25; // < BV unary minus
  public static final int MSAT_TAG_BV_ADD = 26; // < BV addition
  public static final int MSAT_TAG_BV_SUB = 27; // < BV subtraction
  public static final int MSAT_TAG_BV_MUL = 28; // < BV multiplication
  public static final int MSAT_TAG_BV_UDIV = 29; // < BV unsigned division
  public static final int MSAT_TAG_BV_SDIV = 30; // < BV signed division
  public static final int MSAT_TAG_BV_UREM = 31; // < BV unsigned remainder
  public static final int MSAT_TAG_BV_SREM = 32; // < BV signed remainder
  public static final int MSAT_TAG_BV_LSHL = 33; // < BV logical left shift
  public static final int MSAT_TAG_BV_LSHR = 34; // < BV logical right shift
  public static final int MSAT_TAG_BV_ASHR = 35; // < BV arithmetic right shift
  public static final int MSAT_TAG_BV_ROL = 36; // < BV rotate left
  public static final int MSAT_TAG_BV_ROR = 37; // < BV rotate right
  public static final int MSAT_TAG_BV_ZEXT = 38; // < BV zero extension
  public static final int MSAT_TAG_BV_SEXT = 39; // < BV sign extension
  public static final int MSAT_TAG_ARRAY_READ = 40; // < Array read/select operation
  public static final int MSAT_TAG_ARRAY_WRITE = 41; // < Array write/store operation
  public static final int MSAT_TAG_ARRAY_CONST = 42; // < Constant arrays
  public static final int MSAT_TAG_FP_EQ = 43; // < FP IEEE equality
  public static final int MSAT_TAG_FP_LT = 44; // < FP <
  public static final int MSAT_TAG_FP_LE = 45; // < FP <=
  public static final int MSAT_TAG_FP_NEG = 46; // < FP unary minus
  public static final int MSAT_TAG_FP_ADD = 47; // < FP addition
  public static final int MSAT_TAG_FP_SUB = 48; // < FP subtraction
  public static final int MSAT_TAG_FP_MUL = 49; // < FP multiplication
  public static final int MSAT_TAG_FP_DIV = 50; // < FP division
  public static final int MSAT_TAG_FP_SQRT = 51; // < FP square root
  public static final int MSAT_TAG_FP_ABS = 52; // < FP absolute value
  public static final int MSAT_TAG_FP_MIN = 53; // < FP min
  public static final int MSAT_TAG_FP_MAX = 54; // < FP max
  public static final int MSAT_TAG_FP_CAST = 55; // < FP format conversion
  public static final int MSAT_TAG_FP_ROUND_TO_INT = 56; // < FP round to integer
  public static final int MSAT_TAG_FP_FROM_SBV = 57; // < FP conversion from a signed BV
  public static final int MSAT_TAG_FP_FROM_UBV = 58; // < FP conversion from an unsigned BV
  public static final int MSAT_TAG_FP_TO_BV = 59; // < FP conversion to BV
  public static final int MSAT_TAG_FP_AS_IEEEBV = 60; // < FP as IEEE BV (access to the bits)
  public static final int MSAT_TAG_FP_ISNAN = 61; // < FP check for NaN
  public static final int MSAT_TAG_FP_ISINF = 62; // < FP check for infinity
  public static final int MSAT_TAG_FP_ISZERO = 63; // < FP check for zero
  public static final int MSAT_TAG_FP_ISSUBNORMAL = 64; // < FP check for subnormal
  public static final int MSAT_TAG_FP_ISNORMAL = 65; // < FP check for normal
  public static final int MSAT_TAG_FP_ISNEG = 66; // < FP check for negative
  public static final int MSAT_TAG_FP_ISPOS = 67; // < FP check for positive
  public static final int MSAT_TAG_FP_FROM_IEEEBV = 68; // < FP conversion from IEEE BV
  public static final int MSAT_TAG_INT_FROM_UBV = 69; // < Unsigned BV -> INT conversion
  public static final int MSAT_TAG_INT_FROM_SBV = 70; // < Signed BV -> INT conversion
  public static final int MSAT_TAG_INT_TO_BV = 71; // < INT -> BV conversion

  interface AllSatModelCallback {

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

  interface TerminationTest {
    boolean shouldTerminate() throws InterruptedException;
  }

  // wrappers for some of the 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<commit_msg>Fix forgotten adjustment of MSAT_TAG constants<commit_after>/*
 *  JavaSMT is an API wrapper for a collection of SMT solvers.
 *  This file is part of JavaSMT.
 *
 *  Copyright (C) 2007-2016  <NAME>
 *  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.
 */
/*
 * 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.CanIgnoreReturnValue;
import javax.annotation.CheckReturnValue;
import javax.annotation.Nullable;
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_INITIAL_LOWER = 1;
  public static final int MSAT_INITIAL_UPPER = 2;
  public static final int MSAT_FINAL_LOWER = 3;
  public static final int MSAT_FINAL_UPPER = 4;
  public static final int MSAT_FINAL_ERROR = 5;

  /** 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_BV = 60; // < FP conversion to BV
  public static final int MSAT_TAG_FP_AS_IEEEBV = 61; // < FP as IEEE BV (access to the bits)
  public static final int MSAT_TAG_FP_ISNAN = 62; // < FP check for NaN
  public static final int MSAT_TAG_FP_ISINF = 63; // < FP check for infinity
  public static final int MSAT_TAG_FP_ISZERO = 64; // < FP check for zero
  public static final int MSAT_TAG_FP_ISSUBNORMAL = 65; // < FP check for subnormal
  public static final int MSAT_TAG_FP_ISNORMAL = 66; // < FP check for normal
  public static final int MSAT_TAG_FP_ISNEG = 67; // < FP check for negative
  public static final int MSAT_TAG_FP_ISPOS = 68; // < FP check for positive
  public static final int MSAT_TAG_FP_FROM_IEEEBV = 69; // < FP conversion from IEEE BV
  public static final int MSAT_TAG_INT_FROM_UBV = 70; // < Unsigned BV -> INT conversion
  public static final int MSAT_TAG_INT_FROM_SBV = 71; // < Signed BV -> INT conversion
  public static final int MSAT_TAG_INT_TO_BV = 72; // < INT -> BV conversion

  interface AllSatModelCallback {

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

  interface TerminationTest {
    boolean shouldTerminate() throws InterruptedException;
  }

  // wrappers for some of the 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
{'fraction_non_alphanumeric': 0.07219186399514269, 'fraction_numerical': 0.020036429872495445, 'mean_word_length': 3.664684225431889, 'pattern_counts': {'":': 0, '<': 162, '<?xml version=': 0, '>': 11, 'https://': 0, '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': '678510', 'n_tokens_mistral': 5674, 'n_tokens_neox': 5086, 'n_words': 1942}