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. More... | |
class | ASTVector |
Vectors of ASTs. More... | |
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... | |
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... |
enum Status |
enum Z3_ast_kind |
Z3_ast_kind.
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_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, }
enum Z3_ast_print_mode |
Z3_ast_print_mode.
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_PRINT_SMTLIB2_COMPLIANT = 3, Z3_PRINT_SMTLIB_COMPLIANT = 2, Z3_PRINT_SMTLIB_FULL = 0, Z3_PRINT_LOW_LEVEL = 1, }
enum Z3_decl_kind |
Z3_decl_kind.
Definition at line 59 of file Enumerations.cs.
{ 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, }
enum Z3_error_code |
Z3_error_code.
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_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, }
enum Z3_goal_prec |
Z3_goal_prec.
Definition at line 252 of file Enumerations.cs.
{ Z3_GOAL_UNDER = 1, Z3_GOAL_PRECISE = 0, Z3_GOAL_UNDER_OVER = 3, Z3_GOAL_OVER = 2, }
enum Z3_lbool |
Z3_lbool.
Definition at line 10 of file Enumerations.cs.
{ Z3_L_TRUE = 1, Z3_L_UNDEF = 0, Z3_L_FALSE = -1, }
enum Z3_param_kind |
Z3_param_kind.
Definition at line 216 of file Enumerations.cs.
{ 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, }
enum Z3_parameter_kind |
Z3_parameter_kind.
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_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, }
enum Z3_sort_kind |
Z3_sort_kind.
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_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, }
enum Z3_symbol_kind |
Z3_symbol_kind.
Definition at line 17 of file Enumerations.cs.
{ Z3_INT_SYMBOL = 0, Z3_STRING_SYMBOL = 1, }