Yices2NativeApi { public static native int yices_rational32(int num, int den); private  Yices2NativeApi(); static native void yices_init(); static native void yices_exit(); static native void yices_reset(); static native void free_string(long stringPtr); static native int yices_get_version(); static native int yices_get_major_version(); static native int yices_get_patch_level(); static native long yices_new_config(); static native void yices_free_config(long cfg); static native void yices_set_config(long cfg, String option, String value); static native int yices_default_config_for_logic(long cfg, String logic); static native long yices_new_context(long cfg); static native void yices_free_context(long ctx); static native void yices_context_enable_option(long ctx, String option); static native void yices_context_disable_option(long ctx, String option); static native long yices_new_param_record(); static native int yices_set_param(long record, String name, String value); static native void yices_default_params_for_context(long ctx, long record); static native void yices_free_param_record(long record); static native int yices_bool_type(); static native int yices_int_type(); static native int yices_real_type(); static native int yices_bv_type(int size); static native int yices_function_type(int n, int[] dom, int range); static native boolean yices_type_is_bool(int t); static native boolean yices_type_is_int(int t); static native boolean yices_type_is_real(int t); static native boolean yices_type_is_arithmetic(int t); static native boolean yices_type_is_bitvector(int t); static native boolean yices_type_is_function(int t); static native boolean yices_test_subtype(int t1, int t2); static native boolean yices_compatible_types(int t1, int t2); static native int yices_bvtype_size(int t); static native int yices_type_num_children(int t); static native int yices_type_child(int t, int index); static native int[] yices_type_children(int t); static native int yices_new_uninterpreted_term(int type); static native int yices_new_variable(int type); static native int yices_constant(int type, int index); static native int yices_ite(int t_if, int t_then, int t_else); static native int yices_eq(int t_1, int t_2); static native int yices_neq(int t_1, int t_2); static native int yices_distinct(int size, int[] terms); static native int yices_application(int t, int size, int[] terms); static native int yices_update(int t1, int size, int[] terms, int t2); static native int yices_forall(int size, int[] terms, int t); static native int yices_exists(int size, int[] terms, int t); static native int yices_lambda(int size, int[] terms, int t); static native int yices_true(); static native int yices_false(); static native int yices_not(int t); static native int yices_and(int n, int[] arg); static native int yices_and2(int t1, int t2); static native int yices_and3(int t1, int t2, int t3); static native int yices_or(int n, int[] arg); static native int yices_or2(int t1, int t2); static native int yices_or3(int t1, int t2, int t3); static native int yices_xor(int n, int[] arg); static native int yices_xor2(int t1, int t2); static native int yices_xor3(int t1, int t2, int t3); static native int yices_iff(int t1, int t2); static native int yices_implies(int t1, int t2); static native int yices_zero(); static native int yices_int32(int value); static native int yices_int64(long val); static native int yices_rational32(int num, int den); static native int yices_rational64(long num, long den); static native int yices_parse_rational(String val); static native int yices_parse_float(String val); static native int yices_add(int t1, int t2); static native int yices_sub(int t1, int t2); static native int yices_neg(int t); static native int yices_mul(int t1, int t2); static native int yices_square(int t); static native int yices_power(int t, int power); static native int yices_division(int t1, int t2); static native int yices_sum(int size, int[] terms); static native int yices_product(int size, int[] terms); static native int yices_poly_int32(int size, int[] coeff, int[] terms); static native int yices_poly_int64(int size, long[] coeff, int[] terms); static native int yices_abs(int t); static native int yices_floor(int t); static native int yices_ceil(int t); static native int yices_idiv(int t1, int t2); static native int yices_imod(int t1, int t2); static native int yices_arith_eq_atom(int t1, int t2); static native int yices_arith_neq_atom(int t1, int t2); static native int yices_arith_geq_atom(int t1, int t2); static native int yices_arith_leq_atom(int t1, int t2); static native int yices_arith_gt_atom(int t1, int t2); static native int yices_arith_lt_atom(int t1, int t2); static native int yices_arith_eq0_atom(int t); static native int yices_arith_neq0_atom(int t); static native int yices_arith_geq0_atom(int t); static native int yices_arith_leq0_atom(int t); static native int yices_arith_gt0_atom(int t); static native int yices_arith_lt0_atom(int t); static native int yices_divides_atom(int t1, int t2); static native int yices_is_int_atom(int t); static native int yices_bvconst_uint32(int size, int value); static native int yices_bvcinst_uint64(int size, long value); static native int yices_bvconst_int32(int size, int value); static native int yices_bvconst_int64(int size, long value); static native int yices_bvconst_zero(int size); static native int yices_bvconst_one(int size); static native int yices_bvconst_minus_one(int size); static native int yices_bvconst_from_array(int size, int[] values); static native int yices_parse_bvbin(String value); static native int yices_parse_bvhex(String value); static native int yices_bvadd(int t1, int t2); static native int yices_bvsub(int t1, int t2); static native int yices_bvneg(int t); static native int yices_bvmul(int t1, int t2); static native int yices_bvsquare(int t); static native int yices_bvpower(int t, int power); static native int yices_bvsum(int size, int[] terms); static native int yices_bvproduct(int size, int[] terms); static native int yices_bvdiv(int t1, int t2); static native int yices_bvrem(int t1, int t2); static native int yices_bvsdiv(int t1, int t2); static native int yices_bvsrem(int t1, int t2); static native int yices_bvsmod(int t1, int t2); static native int yices_bvnot(int t); static native int yices_bvand(int size, int[] terms); static native int yices_bvand2(int t1, int t2); static native int yices_bvand3(int t1, int t2, int t3); static native int yices_bvor(int size, int[] terms); static native int yices_bvor2(int t1, int t2); static native int yices_bvor3(int t1, int t2, int t3); static native int yices_bvxor(int size, int[] terms); static native int yices_bvxor2(int t1, int t2); static native int yices_bvxor3(int t1, int t2, int t3); static native int yices_bvnand(int t1, int t2); static native int yices_bvnor(int t1, int t2); static native int yices_bvxnor(int t1, int t2); static native int yices_shift_left0(int t, int shift); static native int yices_shift_left1(int t, int shift); static native int yices_shift_right0(int t, int shift); static native int yices_shift_right1(int t, int shift); static native int yices_ashift_right(int t, int shift); static native int yices_rotate_left(int t, int shift); static native int yices_rotate_right(int t, int shift); static native int yices_bvshl(int t1, int t2); static native int yices_bvlshr(int t1, int t2); static native int yices_bvashr(int t1, int t2); static native int yices_bvextract(int t, int limit1, int limit2); static native int yices_bitextract(int t, int pos); static native int yices_bvconcat(int size, int[] terms); static native int yices_bvconcat2(int t1, int t2); static native int yices_bvrepeat(int t, int times); static native int yices_sign_extend(int t, int times); static native int yices_zero_extend(int t, int times); static native int yices_redand(int t); static native int yices_redor(int t); static native int yices_redcomp(int t1, int t2); static native int yices_bvarray(int size, int[] terms); static native int yices_bveq_atom(int t1, int t2); static native int yices_bvneq_atom(int t1, int t2); static native int yices_bvge_atom(int t1, int t2); static native int yices_bvgt_atom(int t1, int t2); static native int yices_bvle_atom(int t1, int t2); static native int yices_bvlt_atom(int t1, int t2); static native int yices_bvsge_atom(int t1, int t2); static native int yices_bvsgt_atom(int t1, int t2); static native int yices_bvsle_atom(int t1, int t2); static native int yices_bvslt_atom(int t1, int t2); static native int yices_type_of_term(int t); static native boolean yices_term_is_bool(int t); static native boolean yices_term_is_int(int t); static native boolean yices_term_is_real(int t); static native boolean yices_term_is_arithmetic(int t); static native boolean yices_term_is_bitvector(int t); static native boolean yices_term_is_function(int t); static native int yices_term_bitsize(int t); static native boolean yices_term_is_ground(int t); static native boolean yices_term_is_atomic(int t); static native boolean yices_term_is_composite(int t); static native boolean yices_term_is_projection(int t); static native boolean yices_term_is_sum(int t); static native boolean yices_term_is_bvsum(int t); static native boolean yices_term_is_product(int t); static native int yices_term_constructor(int t); static native int yices_term_num_children(int t); static native int yices_term_child(int t, int index); static native int yices_proj_index(int t); static native int yices_proj_arg(int t); static native boolean yices_bool_const_value(int t); static native int[] yices_bv_const_value(int t, int bitsize); static native String yices_rational_const_value(int t); static native String[] yices_sum_component(int t, int i); static native int[] yices_bvsum_component(int t, int i, int bitsize); static native int[] yices_product_component(int t, int i); static native int yices_context_status(long ctx); static native void yices_assert_formula(long ctx, int f); static native void yices_assert_formulas(long ctx, int size, int[] formulas); static native int yices_check_context(long ctx, long params); static native void yices_stop_search(long ctx); static native void yices_reset_context(long ctx); static native int yices_assert_blocking_clause(long ctx); static native void yices_push(long ctx); static native void yices_pop(long ctx); static native int yices_check_context_with_assumptions(
      long ctx, long params, int size, int[] terms); static native int[] yices_get_unsat_core(long ctx); static boolean yices_check_sat(long ctx, long params); static boolean yices_check_sat_with_assumptions(
      long ctx, long params, int size, int[] assumptions); static native long yices_get_model(long ctx, int keepSubst); static native long yices_model_from_map(int size, int[] var, int[] constant); static native int[] yices_def_terms(long model); static native void yices_free_model(long model); static native int[] yices_get_value(long m, int t); static native int yices_val_bitsize(long m, int id, int tag); static native int yices_val_function_arity(long m, int id, int tag); static native boolean yices_val_get_bool(long m, int id, int tag); static native String yices_val_get_mpq(long m, int id, int tag); static native int[] yices_val_get_bv(long m, int id, int size, int tag); static native int[] yices_val_expand_function(long m, int id, int tag); static native int[] yices_val_expand_mapping(long m, int id, int arity, int tag); static native int yices_get_value_as_term(long m, int t); static native void yices_set_term_name(int t, String name); static native String yices_get_term_name(int t); static native int yices_get_term_by_name(String name); static String yices_term_to_string(int t); static String yices_type_to_string(int t); static String yices_model_to_string(long m); static native int yices_parse_term(String t); static native int yices_subst_term(int size, int[] from, int[] to, int t); static int yices_named_variable(int type, String name); static native int yices_is_thread_safe(); static native int yices_check_formula(int term, String logic, long model, String delegate); static native int yices_check_formulas(
      int[] terms, int n, String logic, long model, String delegate); static native int yices_has_delegate(String delegate); static native int yices_val_function_type(long model, int id, int tag); static native int[] yices_model_term_support(long model, int term); static final int YICES_STATUS_IDLE; static final int YICES_STATUS_SEARCHING; static final int YICES_STATUS_UNKNOWN; static final int YICES_STATUS_SAT; static final int YICES_STATUS_UNSAT; static final int YICES_STATUS_INTERRUPTED; static final int YICES_STATUS_ERROR; static final int YICES_CONSTRUCTOR_ERROR; static final int YICES_BOOL_CONST; static final int YICES_ARITH_CONST; static final int YICES_BV_CONST; static final int YICES_SCALAR_CONST; static final int YICES_VARIABLE; static final int YICES_UNINTERPRETED_TERM; static final int YICES_ITE_TERM; static final int YICES_APP_TERM; static final int YICES_UPDATE_TERM; static final int YICES_TUPLE_TERM; static final int YICES_EQ_TERM; static final int YICES_DISTINCT_TERM; static final int YICES_FORALL_TERM; static final int YICES_LAMBDA_TERM; static final int YICES_NOT_TERM; static final int YICES_OR_TERM; static final int YICES_XOR_TERM; static final int YICES_BV_ARRAY; static final int YICES_BV_DIV; static final int YICES_BV_REM; static final int YICES_BV_SDIV; static final int YICES_BV_SREM; static final int YICES_BV_SMOD; static final int YICES_BV_SHL; static final int YICES_BV_LSHR; static final int YICES_BV_ASHR; static final int YICES_BV_GE_ATOM; static final int YICES_BV_SGE_ATOM; static final int YICES_ARITH_GE_ATOM; static final int YICES_ARITH_ROOT_ATOM; static final int YICES_ABS; static final int YICES_CEIL; static final int YICES_FLOOR; static final int YICES_RDIV; static final int YICES_IDIV; static final int YICES_IMOD; static final int YICES_IS_INT_ATOM; static final int YICES_DIVIDES_ATOM; static final int YICES_SELECT_TERM; static final int YICES_BIT_TERM; static final int YICES_BV_SUM; static final int YICES_ARITH_SUM; static final int YICES_POWER_PRODUCT; static final int YICES_AND; static final int YICES_BV_MUL; static final int YVAL_UNKNOWN; static final int YVAL_BOOL; static final int YVAL_RATIONAL; static final int YVAL_ALGEBRAIC; static final int YVAL_BV; static final int YVAL_SCALAR; static final int YVAL_TUPLE; static final int YVAL_FUNCTION; static final int YVAL_MAPPING; }
@Test(expected = IllegalArgumentException.class) public void rationalError() { int rat = yices_rational32(1, 0); System.out.println(rat); }
@Test public void negativeRationalError() { int rat = yices_rational32(1, -5); System.out.println(rat); }