Z3
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Properties Friends Macros Groups 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  ConstructorList
 Lists of constructors More...
 
class  Context
 The main interaction with Z3 happens via the Context. More...
 
class  DecRefQueue
 
class  DecRefQueueContracts
 
class  Expr
 Expressions are terms. More...
 
class  BoolExpr
 Boolean expressions More...
 
class  ArithExpr
 Arithmetic expressions (int/real) More...
 
class  IntExpr
 Int expressions More...
 
class  RealExpr
 Real expressions More...
 
class  BitVecExpr
 Bit-vector expressions More...
 
class  ArrayExpr
 Array expressions More...
 
class  DatatypeExpr
 Datatype expressions 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  IntNum
 Integer Numerals More...
 
class  RatNum
 Rational Numerals More...
 
class  BitVecNum
 Bit-vector numerals More...
 
class  AlgebraicNum
 Algebraic numbers More...
 
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  BoolSort
 A Boolean sort. More...
 
class  ArithSort
 An arithmetic sort, i.e., Int or Real. More...
 
class  IntSort
 An Integer sort More...
 
class  RealSort
 A real sort More...
 
class  BitVecSort
 Bit-vector sorts. More...
 
class  ArraySort
 Array sorts. More...
 
class  DatatypeSort
 Datatype sorts. More...
 
class  UninterpretedSort
 Uninterpreted Sorts More...
 
class  TupleSort
 Tuple sorts. More...
 
class  EnumSort
 Enumeration sorts. More...
 
class  ListSort
 List sorts. More...
 
class  RelationSort
 Relation sorts. More...
 
class  FiniteDomainSort
 Finite domain sorts. More...
 
class  SetSort
 Set sorts. 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  IntSymbol
 Numbered symbols More...
 
class  StringSymbol
 Named symbols 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
 

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_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_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.

{
UNSATISFIABLE = -1,
UNKNOWN = 0,
SATISFIABLE = 1
}

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.

Z3_ast_print_mode

Enumerator:
Z3_PRINT_SMTLIB2_COMPLIANT 
Z3_PRINT_SMTLIB_COMPLIANT 
Z3_PRINT_SMTLIB_FULL 
Z3_PRINT_LOW_LEVEL 

Definition at line 226 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_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.

{
Z3_OP_LABEL = 1792,
Z3_OP_SUB = 519,
Z3_OP_ADD = 518,
Z3_OP_IS_INT = 528,
Z3_OP_BREDOR = 1061,
Z3_OP_BNOT = 1051,
Z3_OP_BNOR = 1054,
Z3_OP_RA_JOIN = 1539,
Z3_OP_LE = 514,
Z3_OP_BREDAND = 1062,
Z3_OP_LT = 516,
Z3_OP_BADD = 1028,
Z3_OP_BUREM0 = 1039,
Z3_OP_OEQ = 267,
Z3_OP_REPEAT = 1060,
Z3_OP_BSMOD0 = 1040,
Z3_OP_BLSHR = 1065,
Z3_OP_BASHR = 1066,
Z3_OP_IDIV = 523,
Z3_OP_PR_GOAL = 1283,
Z3_OP_BOR = 1050,
Z3_OP_TRUE = 256,
Z3_OP_CONCAT = 1056,
Z3_OP_IFF = 263,
Z3_OP_BSHL = 1064,
Z3_OP_SGT = 1048,
Z3_OP_NOT = 265,
Z3_OP_UGT = 1047,
Z3_OP_BSREM = 1033,
Z3_OP_SLT = 1046,
Z3_OP_ULEQ = 1041,
Z3_OP_BIT1 = 1025,
Z3_OP_BIT0 = 1026,
Z3_OP_EQ = 258,
Z3_OP_BMUL = 1030,
Z3_OP_STORE = 768,
Z3_OP_AND = 261,
Z3_OP_MOD = 525,
Z3_OP_BUDIV0 = 1037,
Z3_OP_PR_TRUE = 1281,
Z3_OP_BNAND = 1053,
Z3_OP_FD_LT = 1549,
Z3_OP_DIV = 522,
Z3_OP_ANUM = 512,
Z3_OP_MUL = 521,
Z3_OP_UGEQ = 1043,
Z3_OP_BSREM0 = 1038,
Z3_OP_BXOR = 1052,
Z3_OP_BV2INT = 1072,
Z3_OP_BSUB = 1029,
Z3_OP_BXNOR = 1055,
Z3_OP_EXTRACT = 1059,
Z3_OP_PR_DER = 1300,
Z3_OP_GT = 517,
Z3_OP_BUREM = 1034,
Z3_OP_SLEQ = 1042,
Z3_OP_GE = 515,
Z3_OP_BAND = 1049,
Z3_OP_ITE = 260,
Z3_OP_BSDIV = 1031,
Z3_OP_OR = 262,
Z3_OP_AGNUM = 513,
Z3_OP_BSMOD = 1035,
Z3_OP_SELECT = 769,
Z3_OP_BNEG = 1027,
Z3_OP_UMINUS = 520,
Z3_OP_REM = 524,
Z3_OP_TO_INT = 527,
Z3_OP_SGEQ = 1044,
Z3_OP_POWER = 529,
Z3_OP_XOR3 = 1074,
Z3_OP_CARRY = 1073,
Z3_OP_ULT = 1045,
Z3_OP_BSDIV0 = 1036,
Z3_OP_INT2BV = 1071,
Z3_OP_XOR = 264,
Z3_OP_BNUM = 1024,
Z3_OP_BUDIV = 1032,
Z3_OP_FALSE = 257,
Z3_OP_BCOMP = 1063,
}

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 234 of file Enumerations.cs.

Z3_goal_prec

Enumerator:
Z3_GOAL_UNDER 
Z3_GOAL_PRECISE 
Z3_GOAL_UNDER_OVER 
Z3_GOAL_OVER 

Definition at line 251 of file Enumerations.cs.

enum Z3_lbool

Z3_lbool

Enumerator:
Z3_L_TRUE 
Z3_L_UNDEF 
Z3_L_FALSE 

Definition at line 10 of file Enumerations.cs.

{
Z3_L_TRUE = 1,
Z3_L_FALSE = -1,
}

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 215 of file Enumerations.cs.

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.