mirror of
https://github.com/Z3Prover/z3
synced 2025-04-30 12:25:51 +00:00
Java API: Removed auto-generated files.
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
This commit is contained in:
Christoph M. Wintersteiger
parent
9a79511458
commit
11ffbab0bd
11 changed files with 0 additions and 2728 deletions
|
|
@ -1,33 +0,0 @@
|
|||
/**
|
||||
* Automatically generated file
|
||||
**/
|
||||
|
||||
package com.Microsoft.Z3.Enumerations;
|
||||
|
||||
/**
|
||||
* Z3_ast_kind
|
||||
**/
|
||||
public enum Z3_ast_kind {
|
||||
Z3_VAR_AST (2),
|
||||
Z3_SORT_AST (4),
|
||||
Z3_QUANTIFIER_AST (3),
|
||||
Z3_UNKNOWN_AST (1000),
|
||||
Z3_FUNC_DECL_AST (5),
|
||||
Z3_NUMERAL_AST (0),
|
||||
Z3_APP_AST (1);
|
||||
|
||||
private final int intValue;
|
||||
|
||||
Z3_ast_kind(int v) {
|
||||
this.intValue = v;
|
||||
}
|
||||
|
||||
public static final Z3_ast_kind fromInt(int v) {
|
||||
for (Z3_ast_kind k: values())
|
||||
if (k.intValue == v) return k;
|
||||
return values()[0];
|
||||
}
|
||||
|
||||
public final int toInt() { return this.intValue; }
|
||||
}
|
||||
|
||||
|
|
@ -1,30 +0,0 @@
|
|||
/**
|
||||
* Automatically generated file
|
||||
**/
|
||||
|
||||
package com.Microsoft.Z3.Enumerations;
|
||||
|
||||
/**
|
||||
* Z3_ast_print_mode
|
||||
**/
|
||||
public enum Z3_ast_print_mode {
|
||||
Z3_PRINT_SMTLIB2_COMPLIANT (3),
|
||||
Z3_PRINT_SMTLIB_COMPLIANT (2),
|
||||
Z3_PRINT_SMTLIB_FULL (0),
|
||||
Z3_PRINT_LOW_LEVEL (1);
|
||||
|
||||
private final int intValue;
|
||||
|
||||
Z3_ast_print_mode(int v) {
|
||||
this.intValue = v;
|
||||
}
|
||||
|
||||
public static final Z3_ast_print_mode fromInt(int v) {
|
||||
for (Z3_ast_print_mode k: values())
|
||||
if (k.intValue == v) return k;
|
||||
return values()[0];
|
||||
}
|
||||
|
||||
public final int toInt() { return this.intValue; }
|
||||
}
|
||||
|
||||
|
|
@ -1,178 +0,0 @@
|
|||
/**
|
||||
* Automatically generated file
|
||||
**/
|
||||
|
||||
package com.Microsoft.Z3.Enumerations;
|
||||
|
||||
/**
|
||||
* Z3_decl_kind
|
||||
**/
|
||||
public enum Z3_decl_kind {
|
||||
Z3_OP_LABEL (1792),
|
||||
Z3_OP_PR_REWRITE (1294),
|
||||
Z3_OP_UNINTERPRETED (2051),
|
||||
Z3_OP_SUB (519),
|
||||
Z3_OP_ZERO_EXT (1058),
|
||||
Z3_OP_ADD (518),
|
||||
Z3_OP_IS_INT (528),
|
||||
Z3_OP_BREDOR (1061),
|
||||
Z3_OP_BNOT (1051),
|
||||
Z3_OP_BNOR (1054),
|
||||
Z3_OP_PR_CNF_STAR (1315),
|
||||
Z3_OP_RA_JOIN (1539),
|
||||
Z3_OP_LE (514),
|
||||
Z3_OP_SET_UNION (773),
|
||||
Z3_OP_PR_UNDEF (1280),
|
||||
Z3_OP_BREDAND (1062),
|
||||
Z3_OP_LT (516),
|
||||
Z3_OP_RA_UNION (1540),
|
||||
Z3_OP_BADD (1028),
|
||||
Z3_OP_BUREM0 (1039),
|
||||
Z3_OP_OEQ (267),
|
||||
Z3_OP_PR_MODUS_PONENS (1284),
|
||||
Z3_OP_RA_CLONE (1548),
|
||||
Z3_OP_REPEAT (1060),
|
||||
Z3_OP_RA_NEGATION_FILTER (1544),
|
||||
Z3_OP_BSMOD0 (1040),
|
||||
Z3_OP_BLSHR (1065),
|
||||
Z3_OP_BASHR (1066),
|
||||
Z3_OP_PR_UNIT_RESOLUTION (1304),
|
||||
Z3_OP_ROTATE_RIGHT (1068),
|
||||
Z3_OP_ARRAY_DEFAULT (772),
|
||||
Z3_OP_PR_PULL_QUANT (1296),
|
||||
Z3_OP_PR_APPLY_DEF (1310),
|
||||
Z3_OP_PR_REWRITE_STAR (1295),
|
||||
Z3_OP_IDIV (523),
|
||||
Z3_OP_PR_GOAL (1283),
|
||||
Z3_OP_PR_IFF_TRUE (1305),
|
||||
Z3_OP_LABEL_LIT (1793),
|
||||
Z3_OP_BOR (1050),
|
||||
Z3_OP_PR_SYMMETRY (1286),
|
||||
Z3_OP_TRUE (256),
|
||||
Z3_OP_SET_COMPLEMENT (776),
|
||||
Z3_OP_CONCAT (1056),
|
||||
Z3_OP_PR_NOT_OR_ELIM (1293),
|
||||
Z3_OP_IFF (263),
|
||||
Z3_OP_BSHL (1064),
|
||||
Z3_OP_PR_TRANSITIVITY (1287),
|
||||
Z3_OP_SGT (1048),
|
||||
Z3_OP_RA_WIDEN (1541),
|
||||
Z3_OP_PR_DEF_INTRO (1309),
|
||||
Z3_OP_NOT (265),
|
||||
Z3_OP_PR_QUANT_INTRO (1290),
|
||||
Z3_OP_UGT (1047),
|
||||
Z3_OP_DT_RECOGNISER (2049),
|
||||
Z3_OP_SET_INTERSECT (774),
|
||||
Z3_OP_BSREM (1033),
|
||||
Z3_OP_RA_STORE (1536),
|
||||
Z3_OP_SLT (1046),
|
||||
Z3_OP_ROTATE_LEFT (1067),
|
||||
Z3_OP_PR_NNF_NEG (1313),
|
||||
Z3_OP_PR_REFLEXIVITY (1285),
|
||||
Z3_OP_ULEQ (1041),
|
||||
Z3_OP_BIT1 (1025),
|
||||
Z3_OP_BIT0 (1026),
|
||||
Z3_OP_EQ (258),
|
||||
Z3_OP_BMUL (1030),
|
||||
Z3_OP_ARRAY_MAP (771),
|
||||
Z3_OP_STORE (768),
|
||||
Z3_OP_PR_HYPOTHESIS (1302),
|
||||
Z3_OP_RA_RENAME (1545),
|
||||
Z3_OP_AND (261),
|
||||
Z3_OP_TO_REAL (526),
|
||||
Z3_OP_PR_NNF_POS (1312),
|
||||
Z3_OP_PR_AND_ELIM (1292),
|
||||
Z3_OP_MOD (525),
|
||||
Z3_OP_BUDIV0 (1037),
|
||||
Z3_OP_PR_TRUE (1281),
|
||||
Z3_OP_BNAND (1053),
|
||||
Z3_OP_PR_ELIM_UNUSED_VARS (1299),
|
||||
Z3_OP_RA_FILTER (1543),
|
||||
Z3_OP_FD_LT (1549),
|
||||
Z3_OP_RA_EMPTY (1537),
|
||||
Z3_OP_DIV (522),
|
||||
Z3_OP_ANUM (512),
|
||||
Z3_OP_MUL (521),
|
||||
Z3_OP_UGEQ (1043),
|
||||
Z3_OP_BSREM0 (1038),
|
||||
Z3_OP_PR_TH_LEMMA (1318),
|
||||
Z3_OP_BXOR (1052),
|
||||
Z3_OP_DISTINCT (259),
|
||||
Z3_OP_PR_IFF_FALSE (1306),
|
||||
Z3_OP_BV2INT (1072),
|
||||
Z3_OP_EXT_ROTATE_LEFT (1069),
|
||||
Z3_OP_PR_PULL_QUANT_STAR (1297),
|
||||
Z3_OP_BSUB (1029),
|
||||
Z3_OP_PR_ASSERTED (1282),
|
||||
Z3_OP_BXNOR (1055),
|
||||
Z3_OP_EXTRACT (1059),
|
||||
Z3_OP_PR_DER (1300),
|
||||
Z3_OP_DT_CONSTRUCTOR (2048),
|
||||
Z3_OP_GT (517),
|
||||
Z3_OP_BUREM (1034),
|
||||
Z3_OP_IMPLIES (266),
|
||||
Z3_OP_SLEQ (1042),
|
||||
Z3_OP_GE (515),
|
||||
Z3_OP_BAND (1049),
|
||||
Z3_OP_ITE (260),
|
||||
Z3_OP_AS_ARRAY (778),
|
||||
Z3_OP_RA_SELECT (1547),
|
||||
Z3_OP_CONST_ARRAY (770),
|
||||
Z3_OP_BSDIV (1031),
|
||||
Z3_OP_OR (262),
|
||||
Z3_OP_PR_HYPER_RESOLVE (1319),
|
||||
Z3_OP_AGNUM (513),
|
||||
Z3_OP_PR_PUSH_QUANT (1298),
|
||||
Z3_OP_BSMOD (1035),
|
||||
Z3_OP_PR_IFF_OEQ (1311),
|
||||
Z3_OP_PR_LEMMA (1303),
|
||||
Z3_OP_SET_SUBSET (777),
|
||||
Z3_OP_SELECT (769),
|
||||
Z3_OP_RA_PROJECT (1542),
|
||||
Z3_OP_BNEG (1027),
|
||||
Z3_OP_UMINUS (520),
|
||||
Z3_OP_REM (524),
|
||||
Z3_OP_TO_INT (527),
|
||||
Z3_OP_PR_QUANT_INST (1301),
|
||||
Z3_OP_SGEQ (1044),
|
||||
Z3_OP_POWER (529),
|
||||
Z3_OP_XOR3 (1074),
|
||||
Z3_OP_RA_IS_EMPTY (1538),
|
||||
Z3_OP_CARRY (1073),
|
||||
Z3_OP_DT_ACCESSOR (2050),
|
||||
Z3_OP_PR_TRANSITIVITY_STAR (1288),
|
||||
Z3_OP_PR_NNF_STAR (1314),
|
||||
Z3_OP_PR_COMMUTATIVITY (1307),
|
||||
Z3_OP_ULT (1045),
|
||||
Z3_OP_BSDIV0 (1036),
|
||||
Z3_OP_SET_DIFFERENCE (775),
|
||||
Z3_OP_INT2BV (1071),
|
||||
Z3_OP_XOR (264),
|
||||
Z3_OP_PR_MODUS_PONENS_OEQ (1317),
|
||||
Z3_OP_BNUM (1024),
|
||||
Z3_OP_BUDIV (1032),
|
||||
Z3_OP_PR_MONOTONICITY (1289),
|
||||
Z3_OP_PR_DEF_AXIOM (1308),
|
||||
Z3_OP_FALSE (257),
|
||||
Z3_OP_EXT_ROTATE_RIGHT (1070),
|
||||
Z3_OP_PR_DISTRIBUTIVITY (1291),
|
||||
Z3_OP_SIGN_EXT (1057),
|
||||
Z3_OP_PR_SKOLEMIZE (1316),
|
||||
Z3_OP_BCOMP (1063),
|
||||
Z3_OP_RA_COMPLEMENT (1546);
|
||||
|
||||
private final int intValue;
|
||||
|
||||
Z3_decl_kind(int v) {
|
||||
this.intValue = v;
|
||||
}
|
||||
|
||||
public static final Z3_decl_kind fromInt(int v) {
|
||||
for (Z3_decl_kind k: values())
|
||||
if (k.intValue == v) return k;
|
||||
return values()[0];
|
||||
}
|
||||
|
||||
public final int toInt() { return this.intValue; }
|
||||
}
|
||||
|
||||
|
|
@ -1,39 +0,0 @@
|
|||
/**
|
||||
* Automatically generated file
|
||||
**/
|
||||
|
||||
package com.Microsoft.Z3.Enumerations;
|
||||
|
||||
/**
|
||||
* Z3_error_code
|
||||
**/
|
||||
public enum Z3_error_code {
|
||||
Z3_INVALID_PATTERN (6),
|
||||
Z3_MEMOUT_FAIL (7),
|
||||
Z3_NO_PARSER (5),
|
||||
Z3_OK (0),
|
||||
Z3_INVALID_ARG (3),
|
||||
Z3_EXCEPTION (12),
|
||||
Z3_IOB (2),
|
||||
Z3_INTERNAL_FATAL (9),
|
||||
Z3_INVALID_USAGE (10),
|
||||
Z3_FILE_ACCESS_ERROR (8),
|
||||
Z3_SORT_ERROR (1),
|
||||
Z3_PARSER_ERROR (4),
|
||||
Z3_DEC_REF_ERROR (11);
|
||||
|
||||
private final int intValue;
|
||||
|
||||
Z3_error_code(int v) {
|
||||
this.intValue = v;
|
||||
}
|
||||
|
||||
public static final Z3_error_code fromInt(int v) {
|
||||
for (Z3_error_code k: values())
|
||||
if (k.intValue == v) return k;
|
||||
return values()[0];
|
||||
}
|
||||
|
||||
public final int toInt() { return this.intValue; }
|
||||
}
|
||||
|
||||
|
|
@ -1,30 +0,0 @@
|
|||
/**
|
||||
* Automatically generated file
|
||||
**/
|
||||
|
||||
package com.Microsoft.Z3.Enumerations;
|
||||
|
||||
/**
|
||||
* Z3_goal_prec
|
||||
**/
|
||||
public enum Z3_goal_prec {
|
||||
Z3_GOAL_UNDER (1),
|
||||
Z3_GOAL_PRECISE (0),
|
||||
Z3_GOAL_UNDER_OVER (3),
|
||||
Z3_GOAL_OVER (2);
|
||||
|
||||
private final int intValue;
|
||||
|
||||
Z3_goal_prec(int v) {
|
||||
this.intValue = v;
|
||||
}
|
||||
|
||||
public static final Z3_goal_prec fromInt(int v) {
|
||||
for (Z3_goal_prec k: values())
|
||||
if (k.intValue == v) return k;
|
||||
return values()[0];
|
||||
}
|
||||
|
||||
public final int toInt() { return this.intValue; }
|
||||
}
|
||||
|
||||
|
|
@ -1,29 +0,0 @@
|
|||
/**
|
||||
* Automatically generated file
|
||||
**/
|
||||
|
||||
package com.Microsoft.Z3.Enumerations;
|
||||
|
||||
/**
|
||||
* Z3_lbool
|
||||
**/
|
||||
public enum Z3_lbool {
|
||||
Z3_L_TRUE (1),
|
||||
Z3_L_UNDEF (0),
|
||||
Z3_L_FALSE (-1);
|
||||
|
||||
private final int intValue;
|
||||
|
||||
Z3_lbool(int v) {
|
||||
this.intValue = v;
|
||||
}
|
||||
|
||||
public static final Z3_lbool fromInt(int v) {
|
||||
for (Z3_lbool k: values())
|
||||
if (k.intValue == v) return k;
|
||||
return values()[0];
|
||||
}
|
||||
|
||||
public final int toInt() { return this.intValue; }
|
||||
}
|
||||
|
||||
|
|
@ -1,33 +0,0 @@
|
|||
/**
|
||||
* Automatically generated file
|
||||
**/
|
||||
|
||||
package com.Microsoft.Z3.Enumerations;
|
||||
|
||||
/**
|
||||
* Z3_param_kind
|
||||
**/
|
||||
public enum Z3_param_kind {
|
||||
Z3_PK_BOOL (1),
|
||||
Z3_PK_SYMBOL (3),
|
||||
Z3_PK_OTHER (5),
|
||||
Z3_PK_INVALID (6),
|
||||
Z3_PK_UINT (0),
|
||||
Z3_PK_STRING (4),
|
||||
Z3_PK_DOUBLE (2);
|
||||
|
||||
private final int intValue;
|
||||
|
||||
Z3_param_kind(int v) {
|
||||
this.intValue = v;
|
||||
}
|
||||
|
||||
public static final Z3_param_kind fromInt(int v) {
|
||||
for (Z3_param_kind k: values())
|
||||
if (k.intValue == v) return k;
|
||||
return values()[0];
|
||||
}
|
||||
|
||||
public final int toInt() { return this.intValue; }
|
||||
}
|
||||
|
||||
|
|
@ -1,33 +0,0 @@
|
|||
/**
|
||||
* Automatically generated file
|
||||
**/
|
||||
|
||||
package com.Microsoft.Z3.Enumerations;
|
||||
|
||||
/**
|
||||
* Z3_parameter_kind
|
||||
**/
|
||||
public enum Z3_parameter_kind {
|
||||
Z3_PARAMETER_FUNC_DECL (6),
|
||||
Z3_PARAMETER_DOUBLE (1),
|
||||
Z3_PARAMETER_SYMBOL (3),
|
||||
Z3_PARAMETER_INT (0),
|
||||
Z3_PARAMETER_AST (5),
|
||||
Z3_PARAMETER_SORT (4),
|
||||
Z3_PARAMETER_RATIONAL (2);
|
||||
|
||||
private final int intValue;
|
||||
|
||||
Z3_parameter_kind(int v) {
|
||||
this.intValue = v;
|
||||
}
|
||||
|
||||
public static final Z3_parameter_kind fromInt(int v) {
|
||||
for (Z3_parameter_kind k: values())
|
||||
if (k.intValue == v) return k;
|
||||
return values()[0];
|
||||
}
|
||||
|
||||
public final int toInt() { return this.intValue; }
|
||||
}
|
||||
|
||||
|
|
@ -1,36 +0,0 @@
|
|||
/**
|
||||
* Automatically generated file
|
||||
**/
|
||||
|
||||
package com.Microsoft.Z3.Enumerations;
|
||||
|
||||
/**
|
||||
* Z3_sort_kind
|
||||
**/
|
||||
public enum Z3_sort_kind {
|
||||
Z3_BV_SORT (4),
|
||||
Z3_FINITE_DOMAIN_SORT (8),
|
||||
Z3_ARRAY_SORT (5),
|
||||
Z3_UNKNOWN_SORT (1000),
|
||||
Z3_RELATION_SORT (7),
|
||||
Z3_REAL_SORT (3),
|
||||
Z3_INT_SORT (2),
|
||||
Z3_UNINTERPRETED_SORT (0),
|
||||
Z3_BOOL_SORT (1),
|
||||
Z3_DATATYPE_SORT (6);
|
||||
|
||||
private final int intValue;
|
||||
|
||||
Z3_sort_kind(int v) {
|
||||
this.intValue = v;
|
||||
}
|
||||
|
||||
public static final Z3_sort_kind fromInt(int v) {
|
||||
for (Z3_sort_kind k: values())
|
||||
if (k.intValue == v) return k;
|
||||
return values()[0];
|
||||
}
|
||||
|
||||
public final int toInt() { return this.intValue; }
|
||||
}
|
||||
|
||||
|
|
@ -1,28 +0,0 @@
|
|||
/**
|
||||
* Automatically generated file
|
||||
**/
|
||||
|
||||
package com.Microsoft.Z3.Enumerations;
|
||||
|
||||
/**
|
||||
* Z3_symbol_kind
|
||||
**/
|
||||
public enum Z3_symbol_kind {
|
||||
Z3_INT_SYMBOL (0),
|
||||
Z3_STRING_SYMBOL (1);
|
||||
|
||||
private final int intValue;
|
||||
|
||||
Z3_symbol_kind(int v) {
|
||||
this.intValue = v;
|
||||
}
|
||||
|
||||
public static final Z3_symbol_kind fromInt(int v) {
|
||||
for (Z3_symbol_kind k: values())
|
||||
if (k.intValue == v) return k;
|
||||
return values()[0];
|
||||
}
|
||||
|
||||
public final int toInt() { return this.intValue; }
|
||||
}
|
||||
|
||||
File diff suppressed because it is too large
Load diff
Loading…
Add table
Add a link
Reference in a new issue