Z3
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Properties Friends Macros Modules Pages
Data Structures | Typedefs | Enumerations
Package Microsoft.Z3

Data Structures

class  ApplyResult
 ApplyResult objects represent the result of an application of a tactic to a goal. It contains the subgoals that were produced. More...
 
class  AST
 The abstract syntax tree (AST) class. More...
 
class  ASTMap
 Map from AST to AST
 
class  ASTVector
 Vectors of ASTs.
 
class  Constructor
 Constructors are used for datatype sorts. More...
 
class  Context
 The main interaction with Z3 happens via the Context. More...
 
class  Expr
 Expressions are terms. More...
 
class  FuncDecl
 Function declarations. More...
 
class  FuncInterp
 A function interpretation is represented as a finite map and an 'else' value. Each entry in the finite map represents the value of a function given a set of arguments. More...
 
class  Goal
 A goal (aka problem). A goal is essentially a set of formulas, that can be solved and/or transformed using tactics and solvers. More...
 
class  Log
 Interaction logging for Z3.
 
class  Model
 A Model contains interpretations (assignments) of constants and functions. More...
 
class  Native
 
class  Params
 A ParameterSet represents a configuration in the form of Symbol/value pairs. More...
 
class  Pattern
 Patterns comprise a list of terms. The list should be non-empty. If the list comprises of more than one term, it is also called a multi-pattern. More...
 
class  Probe
 Probes are used to inspect a goal (aka problem) and collect information that may be used to decide which solver and/or preprocessing step will be used. The complete list of probes may be obtained using the procedures Context.NumProbes and Context.ProbeNames. It may also be obtained using the command (help-tactics) in the SMT 2.0 front-end. More...
 
class  Quantifier
 Quantifier expressions. More...
 
class  Solver
 Solvers. More...
 
class  Sort
 The Sort class implements type information for ASTs. More...
 
class  Statistics
 Objects of this class track statistical information about solvers. More...
 
class  Symbol
 Symbols are used to name several term and type constructors. More...
 
class  Tactic
 Tactics are the basic building block for creating custom solvers for specific problem domains. The complete list of tactics may be obtained using Context.NumTactics and Context.TacticNames. It may also be obtained using the command (help-tactics) in the SMT 2.0 front-end. More...
 
class  Version
 Version information.
 
class  Z3Exception
 The exception base class for error reporting from Z3 More...
 
class  Z3Object
 Internal base class for interfacing with native Z3 objects. Should not be used externally. More...
 

Typedefs

using Z3_config = System.IntPtr
 
using Z3_context = System.IntPtr
 
using Z3_ast = System.IntPtr
 
using Z3_app = System.IntPtr
 
using Z3_sort = System.IntPtr
 
using Z3_func_decl = System.IntPtr
 
using Z3_pattern = System.IntPtr
 
using Z3_model = System.IntPtr
 
using Z3_literals = System.IntPtr
 
using Z3_constructor = System.IntPtr
 
using Z3_constructor_list = System.IntPtr
 
using Z3_theory = System.IntPtr
 
using Z3_theory_data = System.IntPtr
 
using Z3_solver = System.IntPtr
 
using Z3_goal = System.IntPtr
 
using Z3_tactic = System.IntPtr
 
using Z3_params = System.IntPtr
 
using Z3_probe = System.IntPtr
 
using Z3_stats = System.IntPtr
 
using Z3_ast_vector = System.IntPtr
 
using Z3_ast_map = System.IntPtr
 
using Z3_apply_result = System.IntPtr
 
using Z3_func_interp = System.IntPtr
 
using Z3_func_entry = System.IntPtr
 
using Z3_fixedpoint = System.IntPtr
 
using Z3_param_descrs = System.IntPtr
 
using Z3_rcf_num = System.IntPtr
 

Enumerations

enum  Z3_lbool { Z3_L_TRUE = 1, Z3_L_UNDEF = 0, Z3_L_FALSE = -1 }
 Z3_lbool More...
 
enum  Z3_symbol_kind { Z3_INT_SYMBOL = 0, Z3_STRING_SYMBOL = 1 }
 Z3_symbol_kind More...
 
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
}
 Z3_parameter_kind More...
 
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
}
 Z3_sort_kind More...
 
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
}
 Z3_ast_kind More...
 
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_INTERP = 268, 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
}
 Z3_decl_kind More...
 
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
}
 Z3_param_kind More...
 
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 }
 Z3_ast_print_mode More...
 
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
}
 Z3_error_code More...
 
enum  Z3_goal_prec { Z3_GOAL_UNDER = 1, Z3_GOAL_PRECISE = 0, Z3_GOAL_UNDER_OVER = 3, Z3_GOAL_OVER = 2 }
 Z3_goal_prec More...
 
enum  Status { UNSATISFIABLE = -1, UNKNOWN = 0, SATISFIABLE = 1 }
 Status values. More...
 

Typedef Documentation

using Z3_app = System.IntPtr

Definition at line 14 of file Native.cs.

using Z3_apply_result = System.IntPtr

Definition at line 32 of file Native.cs.

using Z3_ast = System.IntPtr

Definition at line 13 of file Native.cs.

using Z3_ast_map = System.IntPtr

Definition at line 31 of file Native.cs.

using Z3_ast_vector = System.IntPtr

Definition at line 30 of file Native.cs.

using Z3_config = System.IntPtr

Definition at line 11 of file Native.cs.

using Z3_constructor = System.IntPtr

Definition at line 20 of file Native.cs.

using Z3_constructor_list = System.IntPtr

Definition at line 21 of file Native.cs.

using Z3_context = System.IntPtr

Definition at line 12 of file Native.cs.

using Z3_fixedpoint = System.IntPtr

Definition at line 35 of file Native.cs.

using Z3_func_decl = System.IntPtr

Definition at line 16 of file Native.cs.

using Z3_func_entry = System.IntPtr

Definition at line 34 of file Native.cs.

using Z3_func_interp = System.IntPtr

Definition at line 33 of file Native.cs.

using Z3_goal = System.IntPtr

Definition at line 25 of file Native.cs.

using Z3_literals = System.IntPtr

Definition at line 19 of file Native.cs.

using Z3_model = System.IntPtr

Definition at line 18 of file Native.cs.

using Z3_param_descrs = System.IntPtr

Definition at line 36 of file Native.cs.

using Z3_params = System.IntPtr

Definition at line 27 of file Native.cs.

using Z3_pattern = System.IntPtr

Definition at line 17 of file Native.cs.

using Z3_probe = System.IntPtr

Definition at line 28 of file Native.cs.

using Z3_rcf_num = System.IntPtr

Definition at line 37 of file Native.cs.

using Z3_solver = System.IntPtr

Definition at line 24 of file Native.cs.

using Z3_sort = System.IntPtr

Definition at line 15 of file Native.cs.

using Z3_stats = System.IntPtr

Definition at line 29 of file Native.cs.

using Z3_tactic = System.IntPtr

Definition at line 26 of file Native.cs.

using Z3_theory = System.IntPtr

Definition at line 22 of file Native.cs.

using Z3_theory_data = System.IntPtr

Definition at line 23 of file Native.cs.

Enumeration Type Documentation

enum Status

Status values.

Enumerator
UNSATISFIABLE 

Used to signify an unsatisfiable status.

UNKNOWN 

Used to signify an unknown status.

SATISFIABLE 

Used to signify a satisfiable status.

Definition at line 27 of file Status.cs.

28  {
32  UNSATISFIABLE = -1,
33 
37  UNKNOWN = 0,
38 
42  SATISFIABLE = 1
43  }
Used to signify a satisfiable status.
Used to signify an unknown status.
Used to signify an unsatisfiable status.

Z3_ast_kind

Enumerator
Z3_VAR_AST 
Z3_SORT_AST 
Z3_QUANTIFIER_AST 
Z3_UNKNOWN_AST 
Z3_FUNC_DECL_AST 
Z3_NUMERAL_AST 
Z3_APP_AST 

Definition at line 48 of file Enumerations.cs.

48  {
49  Z3_VAR_AST = 2,
50  Z3_SORT_AST = 4,
52  Z3_UNKNOWN_AST = 1000,
53  Z3_FUNC_DECL_AST = 5,
54  Z3_NUMERAL_AST = 0,
55  Z3_APP_AST = 1,
56  }

Z3_ast_print_mode

Enumerator
Z3_PRINT_SMTLIB2_COMPLIANT 
Z3_PRINT_SMTLIB_COMPLIANT 
Z3_PRINT_SMTLIB_FULL 
Z3_PRINT_LOW_LEVEL 

Definition at line 227 of file Enumerations.cs.

Z3_decl_kind

Enumerator
Z3_OP_LABEL 
Z3_OP_PR_REWRITE 
Z3_OP_UNINTERPRETED 
Z3_OP_SUB 
Z3_OP_ZERO_EXT 
Z3_OP_ADD 
Z3_OP_IS_INT 
Z3_OP_BREDOR 
Z3_OP_BNOT 
Z3_OP_BNOR 
Z3_OP_PR_CNF_STAR 
Z3_OP_RA_JOIN 
Z3_OP_LE 
Z3_OP_SET_UNION 
Z3_OP_PR_UNDEF 
Z3_OP_BREDAND 
Z3_OP_LT 
Z3_OP_RA_UNION 
Z3_OP_BADD 
Z3_OP_BUREM0 
Z3_OP_OEQ 
Z3_OP_PR_MODUS_PONENS 
Z3_OP_RA_CLONE 
Z3_OP_REPEAT 
Z3_OP_RA_NEGATION_FILTER 
Z3_OP_BSMOD0 
Z3_OP_BLSHR 
Z3_OP_BASHR 
Z3_OP_PR_UNIT_RESOLUTION 
Z3_OP_ROTATE_RIGHT 
Z3_OP_ARRAY_DEFAULT 
Z3_OP_PR_PULL_QUANT 
Z3_OP_PR_APPLY_DEF 
Z3_OP_PR_REWRITE_STAR 
Z3_OP_IDIV 
Z3_OP_PR_GOAL 
Z3_OP_PR_IFF_TRUE 
Z3_OP_LABEL_LIT 
Z3_OP_BOR 
Z3_OP_PR_SYMMETRY 
Z3_OP_TRUE 
Z3_OP_SET_COMPLEMENT 
Z3_OP_CONCAT 
Z3_OP_PR_NOT_OR_ELIM 
Z3_OP_IFF 
Z3_OP_BSHL 
Z3_OP_PR_TRANSITIVITY 
Z3_OP_SGT 
Z3_OP_RA_WIDEN 
Z3_OP_PR_DEF_INTRO 
Z3_OP_NOT 
Z3_OP_PR_QUANT_INTRO 
Z3_OP_UGT 
Z3_OP_DT_RECOGNISER 
Z3_OP_SET_INTERSECT 
Z3_OP_BSREM 
Z3_OP_RA_STORE 
Z3_OP_SLT 
Z3_OP_ROTATE_LEFT 
Z3_OP_PR_NNF_NEG 
Z3_OP_PR_REFLEXIVITY 
Z3_OP_ULEQ 
Z3_OP_BIT1 
Z3_OP_BIT0 
Z3_OP_EQ 
Z3_OP_BMUL 
Z3_OP_ARRAY_MAP 
Z3_OP_STORE 
Z3_OP_PR_HYPOTHESIS 
Z3_OP_RA_RENAME 
Z3_OP_AND 
Z3_OP_TO_REAL 
Z3_OP_PR_NNF_POS 
Z3_OP_PR_AND_ELIM 
Z3_OP_MOD 
Z3_OP_BUDIV0 
Z3_OP_PR_TRUE 
Z3_OP_BNAND 
Z3_OP_PR_ELIM_UNUSED_VARS 
Z3_OP_RA_FILTER 
Z3_OP_FD_LT 
Z3_OP_RA_EMPTY 
Z3_OP_DIV 
Z3_OP_ANUM 
Z3_OP_MUL 
Z3_OP_UGEQ 
Z3_OP_BSREM0 
Z3_OP_PR_TH_LEMMA 
Z3_OP_BXOR 
Z3_OP_DISTINCT 
Z3_OP_PR_IFF_FALSE 
Z3_OP_BV2INT 
Z3_OP_EXT_ROTATE_LEFT 
Z3_OP_PR_PULL_QUANT_STAR 
Z3_OP_BSUB 
Z3_OP_PR_ASSERTED 
Z3_OP_BXNOR 
Z3_OP_EXTRACT 
Z3_OP_PR_DER 
Z3_OP_DT_CONSTRUCTOR 
Z3_OP_GT 
Z3_OP_BUREM 
Z3_OP_IMPLIES 
Z3_OP_SLEQ 
Z3_OP_GE 
Z3_OP_BAND 
Z3_OP_ITE 
Z3_OP_AS_ARRAY 
Z3_OP_RA_SELECT 
Z3_OP_CONST_ARRAY 
Z3_OP_BSDIV 
Z3_OP_OR 
Z3_OP_PR_HYPER_RESOLVE 
Z3_OP_AGNUM 
Z3_OP_PR_PUSH_QUANT 
Z3_OP_BSMOD 
Z3_OP_PR_IFF_OEQ 
Z3_OP_INTERP 
Z3_OP_PR_LEMMA 
Z3_OP_SET_SUBSET 
Z3_OP_SELECT 
Z3_OP_RA_PROJECT 
Z3_OP_BNEG 
Z3_OP_UMINUS 
Z3_OP_REM 
Z3_OP_TO_INT 
Z3_OP_PR_QUANT_INST 
Z3_OP_SGEQ 
Z3_OP_POWER 
Z3_OP_XOR3 
Z3_OP_RA_IS_EMPTY 
Z3_OP_CARRY 
Z3_OP_DT_ACCESSOR 
Z3_OP_PR_TRANSITIVITY_STAR 
Z3_OP_PR_NNF_STAR 
Z3_OP_PR_COMMUTATIVITY 
Z3_OP_ULT 
Z3_OP_BSDIV0 
Z3_OP_SET_DIFFERENCE 
Z3_OP_INT2BV 
Z3_OP_XOR 
Z3_OP_PR_MODUS_PONENS_OEQ 
Z3_OP_BNUM 
Z3_OP_BUDIV 
Z3_OP_PR_MONOTONICITY 
Z3_OP_PR_DEF_AXIOM 
Z3_OP_FALSE 
Z3_OP_EXT_ROTATE_RIGHT 
Z3_OP_PR_DISTRIBUTIVITY 
Z3_OP_SIGN_EXT 
Z3_OP_PR_SKOLEMIZE 
Z3_OP_BCOMP 
Z3_OP_RA_COMPLEMENT 

Definition at line 59 of file Enumerations.cs.

59  {
60  Z3_OP_LABEL = 1792,
61  Z3_OP_PR_REWRITE = 1294,
62  Z3_OP_UNINTERPRETED = 2051,
63  Z3_OP_SUB = 519,
64  Z3_OP_ZERO_EXT = 1058,
65  Z3_OP_ADD = 518,
66  Z3_OP_IS_INT = 528,
67  Z3_OP_BREDOR = 1061,
68  Z3_OP_BNOT = 1051,
69  Z3_OP_BNOR = 1054,
70  Z3_OP_PR_CNF_STAR = 1315,
71  Z3_OP_RA_JOIN = 1539,
72  Z3_OP_LE = 514,
73  Z3_OP_SET_UNION = 773,
74  Z3_OP_PR_UNDEF = 1280,
75  Z3_OP_BREDAND = 1062,
76  Z3_OP_LT = 516,
77  Z3_OP_RA_UNION = 1540,
78  Z3_OP_BADD = 1028,
79  Z3_OP_BUREM0 = 1039,
80  Z3_OP_OEQ = 267,
81  Z3_OP_PR_MODUS_PONENS = 1284,
82  Z3_OP_RA_CLONE = 1548,
83  Z3_OP_REPEAT = 1060,
85  Z3_OP_BSMOD0 = 1040,
86  Z3_OP_BLSHR = 1065,
87  Z3_OP_BASHR = 1066,
89  Z3_OP_ROTATE_RIGHT = 1068,
90  Z3_OP_ARRAY_DEFAULT = 772,
91  Z3_OP_PR_PULL_QUANT = 1296,
92  Z3_OP_PR_APPLY_DEF = 1310,
93  Z3_OP_PR_REWRITE_STAR = 1295,
94  Z3_OP_IDIV = 523,
95  Z3_OP_PR_GOAL = 1283,
96  Z3_OP_PR_IFF_TRUE = 1305,
97  Z3_OP_LABEL_LIT = 1793,
98  Z3_OP_BOR = 1050,
99  Z3_OP_PR_SYMMETRY = 1286,
100  Z3_OP_TRUE = 256,
101  Z3_OP_SET_COMPLEMENT = 776,
102  Z3_OP_CONCAT = 1056,
103  Z3_OP_PR_NOT_OR_ELIM = 1293,
104  Z3_OP_IFF = 263,
105  Z3_OP_BSHL = 1064,
106  Z3_OP_PR_TRANSITIVITY = 1287,
107  Z3_OP_SGT = 1048,
108  Z3_OP_RA_WIDEN = 1541,
109  Z3_OP_PR_DEF_INTRO = 1309,
110  Z3_OP_NOT = 265,
111  Z3_OP_PR_QUANT_INTRO = 1290,
112  Z3_OP_UGT = 1047,
113  Z3_OP_DT_RECOGNISER = 2049,
114  Z3_OP_SET_INTERSECT = 774,
115  Z3_OP_BSREM = 1033,
116  Z3_OP_RA_STORE = 1536,
117  Z3_OP_SLT = 1046,
118  Z3_OP_ROTATE_LEFT = 1067,
119  Z3_OP_PR_NNF_NEG = 1313,
120  Z3_OP_PR_REFLEXIVITY = 1285,
121  Z3_OP_ULEQ = 1041,
122  Z3_OP_BIT1 = 1025,
123  Z3_OP_BIT0 = 1026,
124  Z3_OP_EQ = 258,
125  Z3_OP_BMUL = 1030,
126  Z3_OP_ARRAY_MAP = 771,
127  Z3_OP_STORE = 768,
128  Z3_OP_PR_HYPOTHESIS = 1302,
129  Z3_OP_RA_RENAME = 1545,
130  Z3_OP_AND = 261,
131  Z3_OP_TO_REAL = 526,
132  Z3_OP_PR_NNF_POS = 1312,
133  Z3_OP_PR_AND_ELIM = 1292,
134  Z3_OP_MOD = 525,
135  Z3_OP_BUDIV0 = 1037,
136  Z3_OP_PR_TRUE = 1281,
137  Z3_OP_BNAND = 1053,
139  Z3_OP_RA_FILTER = 1543,
140  Z3_OP_FD_LT = 1549,
141  Z3_OP_RA_EMPTY = 1537,
142  Z3_OP_DIV = 522,
143  Z3_OP_ANUM = 512,
144  Z3_OP_MUL = 521,
145  Z3_OP_UGEQ = 1043,
146  Z3_OP_BSREM0 = 1038,
147  Z3_OP_PR_TH_LEMMA = 1318,
148  Z3_OP_BXOR = 1052,
149  Z3_OP_DISTINCT = 259,
150  Z3_OP_PR_IFF_FALSE = 1306,
151  Z3_OP_BV2INT = 1072,
152  Z3_OP_EXT_ROTATE_LEFT = 1069,
154  Z3_OP_BSUB = 1029,
155  Z3_OP_PR_ASSERTED = 1282,
156  Z3_OP_BXNOR = 1055,
157  Z3_OP_EXTRACT = 1059,
158  Z3_OP_PR_DER = 1300,
159  Z3_OP_DT_CONSTRUCTOR = 2048,
160  Z3_OP_GT = 517,
161  Z3_OP_BUREM = 1034,
162  Z3_OP_IMPLIES = 266,
163  Z3_OP_SLEQ = 1042,
164  Z3_OP_GE = 515,
165  Z3_OP_BAND = 1049,
166  Z3_OP_ITE = 260,
167  Z3_OP_AS_ARRAY = 778,
168  Z3_OP_RA_SELECT = 1547,
169  Z3_OP_CONST_ARRAY = 770,
170  Z3_OP_BSDIV = 1031,
171  Z3_OP_OR = 262,
172  Z3_OP_PR_HYPER_RESOLVE = 1319,
173  Z3_OP_AGNUM = 513,
174  Z3_OP_PR_PUSH_QUANT = 1298,
175  Z3_OP_BSMOD = 1035,
176  Z3_OP_PR_IFF_OEQ = 1311,
177  Z3_OP_INTERP = 268,
178  Z3_OP_PR_LEMMA = 1303,
179  Z3_OP_SET_SUBSET = 777,
180  Z3_OP_SELECT = 769,
181  Z3_OP_RA_PROJECT = 1542,
182  Z3_OP_BNEG = 1027,
183  Z3_OP_UMINUS = 520,
184  Z3_OP_REM = 524,
185  Z3_OP_TO_INT = 527,
186  Z3_OP_PR_QUANT_INST = 1301,
187  Z3_OP_SGEQ = 1044,
188  Z3_OP_POWER = 529,
189  Z3_OP_XOR3 = 1074,
190  Z3_OP_RA_IS_EMPTY = 1538,
191  Z3_OP_CARRY = 1073,
192  Z3_OP_DT_ACCESSOR = 2050,
194  Z3_OP_PR_NNF_STAR = 1314,
195  Z3_OP_PR_COMMUTATIVITY = 1307,
196  Z3_OP_ULT = 1045,
197  Z3_OP_BSDIV0 = 1036,
198  Z3_OP_SET_DIFFERENCE = 775,
199  Z3_OP_INT2BV = 1071,
200  Z3_OP_XOR = 264,
202  Z3_OP_BNUM = 1024,
203  Z3_OP_BUDIV = 1032,
204  Z3_OP_PR_MONOTONICITY = 1289,
205  Z3_OP_PR_DEF_AXIOM = 1308,
206  Z3_OP_FALSE = 257,
207  Z3_OP_EXT_ROTATE_RIGHT = 1070,
209  Z3_OP_SIGN_EXT = 1057,
210  Z3_OP_PR_SKOLEMIZE = 1316,
211  Z3_OP_BCOMP = 1063,
212  Z3_OP_RA_COMPLEMENT = 1546,
213  }

Z3_error_code

Enumerator
Z3_INVALID_PATTERN 
Z3_MEMOUT_FAIL 
Z3_NO_PARSER 
Z3_OK 
Z3_INVALID_ARG 
Z3_EXCEPTION 
Z3_IOB 
Z3_INTERNAL_FATAL 
Z3_INVALID_USAGE 
Z3_FILE_ACCESS_ERROR 
Z3_SORT_ERROR 
Z3_PARSER_ERROR 
Z3_DEC_REF_ERROR 

Definition at line 235 of file Enumerations.cs.

Z3_goal_prec

Enumerator
Z3_GOAL_UNDER 
Z3_GOAL_PRECISE 
Z3_GOAL_UNDER_OVER 
Z3_GOAL_OVER 

Definition at line 252 of file Enumerations.cs.

252  {
253  Z3_GOAL_UNDER = 1,
254  Z3_GOAL_PRECISE = 0,
255  Z3_GOAL_UNDER_OVER = 3,
256  Z3_GOAL_OVER = 2,
257  }
enum Z3_lbool

Z3_lbool

Enumerator
Z3_L_TRUE 
Z3_L_UNDEF 
Z3_L_FALSE 

Definition at line 10 of file Enumerations.cs.

10  {
11  Z3_L_TRUE = 1,
12  Z3_L_UNDEF = 0,
13  Z3_L_FALSE = -1,
14  }

Z3_param_kind

Enumerator
Z3_PK_BOOL 
Z3_PK_SYMBOL 
Z3_PK_OTHER 
Z3_PK_INVALID 
Z3_PK_UINT 
Z3_PK_STRING 
Z3_PK_DOUBLE 

Definition at line 216 of file Enumerations.cs.

216  {
217  Z3_PK_BOOL = 1,
218  Z3_PK_SYMBOL = 3,
219  Z3_PK_OTHER = 5,
220  Z3_PK_INVALID = 6,
221  Z3_PK_UINT = 0,
222  Z3_PK_STRING = 4,
223  Z3_PK_DOUBLE = 2,
224  }

Z3_parameter_kind

Enumerator
Z3_PARAMETER_FUNC_DECL 
Z3_PARAMETER_DOUBLE 
Z3_PARAMETER_SYMBOL 
Z3_PARAMETER_INT 
Z3_PARAMETER_AST 
Z3_PARAMETER_SORT 
Z3_PARAMETER_RATIONAL 

Definition at line 23 of file Enumerations.cs.

Z3_sort_kind

Enumerator
Z3_BV_SORT 
Z3_FINITE_DOMAIN_SORT 
Z3_ARRAY_SORT 
Z3_UNKNOWN_SORT 
Z3_RELATION_SORT 
Z3_REAL_SORT 
Z3_INT_SORT 
Z3_UNINTERPRETED_SORT 
Z3_BOOL_SORT 
Z3_DATATYPE_SORT 

Definition at line 34 of file Enumerations.cs.

Z3_symbol_kind

Enumerator
Z3_INT_SYMBOL 
Z3_STRING_SYMBOL 

Definition at line 17 of file Enumerations.cs.

17  {
18  Z3_INT_SYMBOL = 0,
19  Z3_STRING_SYMBOL = 1,
20  }