ProofRule and ProofRewriteRule

Enum ProofRule captures the reasoning steps performed by the SAT solver, the theory solvers and the preprocessor. It represents the inference rules used to derive conclusions within a proof.

Enum ProofRewriteRule pertains to rewrites performed on terms. These identifiers are arguments of the proof rules THEORY_REWRITE and DSL_REWRITE.

class cvc5.ProofRule(*values)

The ProofRule enum

ABSORB = 7

ACI_NORM = 6

ALETHE_RULE = 165

ALPHA_EQUIV = 96

AND_ELIM = 31

AND_INTRO = 32

ARITH_MULT_ABS_COMPARISON = 124

ARITH_MULT_NEG = 134

ARITH_MULT_POS = 133

ARITH_MULT_SIGN = 132

ARITH_MULT_TANGENT = 135

ARITH_POLY_NORM = 130

ARITH_POLY_NORM_REL = 131

ARITH_REDUCTION = 129

ARITH_SUM_UB = 125

ARITH_TRANS_EXP_APPROX_ABOVE_NEG = 141

ARITH_TRANS_EXP_APPROX_ABOVE_POS = 142

ARITH_TRANS_EXP_APPROX_BELOW = 143

ARITH_TRANS_EXP_NEG = 137

ARITH_TRANS_EXP_POSITIVITY = 138

ARITH_TRANS_EXP_SUPER_LIN = 139

ARITH_TRANS_EXP_ZERO = 140

ARITH_TRANS_PI = 136

ARITH_TRANS_SINE_APPROX_ABOVE_NEG = 149

ARITH_TRANS_SINE_APPROX_ABOVE_POS = 150

ARITH_TRANS_SINE_APPROX_BELOW_NEG = 151

ARITH_TRANS_SINE_APPROX_BELOW_POS = 152

ARITH_TRANS_SINE_BOUNDS = 144

ARITH_TRANS_SINE_SHIFT = 145

ARITH_TRANS_SINE_SYMMETRY = 146

ARITH_TRANS_SINE_TANGENT_PI = 148

ARITH_TRANS_SINE_TANGENT_ZERO = 147

ARITH_TRICHOTOMY = 128

ARRAYS_EXT = 86

ARRAYS_READ_OVER_WRITE = 83

ARRAYS_READ_OVER_WRITE_1 = 85

ARRAYS_READ_OVER_WRITE_CONTRA = 84

ASSUME = 0

BV_BITBLAST_STEP = 88

BV_EAGER_ATOM = 89

BV_POLY_NORM = 90

BV_POLY_NORM_EQ = 91

CHAIN_M_RESOLUTION = 25

CHAIN_RESOLUTION = 22

CNF_AND_NEG = 51

CNF_AND_POS = 50

CNF_EQUIV_NEG1 = 59

CNF_EQUIV_NEG2 = 60

CNF_EQUIV_POS1 = 57

CNF_EQUIV_POS2 = 58

CNF_IMPLIES_NEG1 = 55

CNF_IMPLIES_NEG2 = 56

CNF_IMPLIES_POS = 54

CNF_ITE_NEG1 = 68

CNF_ITE_NEG2 = 69

CNF_ITE_NEG3 = 70

CNF_ITE_POS1 = 65

CNF_ITE_POS2 = 66

CNF_ITE_POS3 = 67

CNF_OR_NEG = 53

CNF_OR_POS = 52

CNF_XOR_NEG1 = 63

CNF_XOR_NEG2 = 64

CNF_XOR_POS1 = 61

CNF_XOR_POS2 = 62

CONCAT_CPROP = 108

CONCAT_CSPLIT = 106

CONCAT_EQ = 103

CONCAT_LPROP = 107

CONCAT_SPLIT = 105

CONCAT_UNIFY = 104

CONG = 74

CONTRA = 30

DISTINCT_VALUES = 5

DRAT_REFUTATION = 19

DSL_REWRITE = 13

DT_SPLIT = 92

ENCODE_EQ_INTRO = 12

EQUIV_ELIM1 = 37

EQUIV_ELIM2 = 38

EQ_RESOLVE = 27

EVALUATE = 4

EXISTS_STRING_LENGTH = 98

FACTORING = 23

FALSE_ELIM = 80

FALSE_INTRO = 79

FF_EXHAUST_BRANCH = 162

FF_FIELD_POLYS = 154

FF_IDEAL_GENERATOR = 156

FF_IDEAL_MONIC = 160

FF_IDEAL_REDUCE_DOWN = 157

FF_IDEAL_REDUCE_UP = 158

FF_IDEAL_SPOLY = 159

FF_IDEAL_ZERO = 155

FF_ONE_UNSAT = 163

FF_POLY_CONVERSION = 153

FF_ROOT_BRANCH = 161

HO_APP_ENCODE = 81

HO_CONG = 82

IMPLIES_ELIM = 34

INSTANTIATE = 95

INT_TIGHT_LB = 127

INT_TIGHT_UB = 126

ITE_ELIM1 = 45

ITE_ELIM2 = 46

ITE_EQ = 15

LFSC_RULE = 164

MACRO_ARITH_SCALE_SUM_UB = 123

MACRO_BV_BITBLAST = 87

MACRO_REWRITE = 3

MACRO_SR_EQ_INTRO = 8

MACRO_SR_PRED_ELIM = 10

MACRO_SR_PRED_INTRO = 9

MACRO_SR_PRED_TRANSFORM = 11

MACRO_STRING_INFERENCE = 122

MODUS_PONENS = 28

NARY_CONG = 75

NOT_AND = 49

NOT_EQUIV_ELIM1 = 39

NOT_EQUIV_ELIM2 = 40

NOT_IMPLIES_ELIM1 = 35

NOT_IMPLIES_ELIM2 = 36

NOT_ITE_ELIM1 = 47

NOT_ITE_ELIM2 = 48

NOT_NOT_ELIM = 29

NOT_OR_ELIM = 33

NOT_XOR_ELIM1 = 43

NOT_XOR_ELIM2 = 44

PAIRWISE_CONG = 76

QUANT_VAR_REORDERING = 97

REFL = 71

REORDERING = 24

RESOLUTION = 21

RE_CONCAT = 115

RE_INTER = 114

RE_UNFOLD_NEG = 117

RE_UNFOLD_NEG_CONCAT_FIXED = 118

RE_UNFOLD_POS = 116

SAT_EXTERNAL_PROVE = 20

SAT_REFUTATION = 18

SCOPE = 1

SETS_EXT = 100

SETS_FILTER_DOWN = 102

SETS_FILTER_UP = 101

SETS_SINGLETON_INJ = 99

SKOLEMIZE = 94

SKOLEM_INTRO = 93

SPLIT = 26

STRING_CODE_INJ = 119

STRING_DECOMPOSE = 109

STRING_EAGER_REDUCTION = 113

STRING_EXT = 121

STRING_LENGTH_NON_EMPTY = 111

STRING_LENGTH_POS = 110

STRING_REDUCTION = 112

STRING_SEQ_UNIT_INJ = 120

SUBS = 2

SYMM = 72

THEORY_REWRITE = 14

TRANS = 73

TRUE_ELIM = 78

TRUE_INTRO = 77

TRUST = 16

TRUST_THEORY_REWRITE = 17

UNKNOWN = 166

XOR_ELIM1 = 41

XOR_ELIM2 = 42

class cvc5.ProofRewriteRule(*values)

The ProofRewriteRule enum

ARITH_ABS_EQ = 122

ARITH_ABS_INT_GT = 123

ARITH_ABS_REAL_GT = 124

ARITH_COSECENT_ELIM = 525

ARITH_COSINE_ELIM = 522

ARITH_COTANGENT_ELIM = 526

ARITH_DIVISIBLE_ELIM = 121

ARITH_DIV_TOTAL_ZERO_INT = 95

ARITH_DIV_TOTAL_ZERO_REAL = 94

ARITH_ELIM_GT = 104

ARITH_ELIM_INT_GT = 106

ARITH_ELIM_INT_LT = 107

ARITH_ELIM_LEQ = 108

ARITH_ELIM_LT = 105

ARITH_EQ_ELIM_INT = 114

ARITH_EQ_ELIM_REAL = 113

ARITH_GEQ_ITE_LIFT = 125

ARITH_GEQ_NORM1_INT = 111

ARITH_GEQ_NORM1_REAL = 112

ARITH_GEQ_TIGHTEN = 110

ARITH_INT_DIV_TOTAL = 96

ARITH_INT_DIV_TOTAL_NEG = 99

ARITH_INT_DIV_TOTAL_ONE = 97

ARITH_INT_DIV_TOTAL_ZERO = 98

ARITH_INT_EQ_CONFLICT = 119

ARITH_INT_GEQ_TIGHTEN = 120

ARITH_INT_MOD_TOTAL = 100

ARITH_INT_MOD_TOTAL_NEG = 103

ARITH_INT_MOD_TOTAL_ONE = 101

ARITH_INT_MOD_TOTAL_ZERO = 102

ARITH_LEQ_ITE_LIFT = 126

ARITH_LEQ_NORM = 109

ARITH_MAX_GEQ1 = 129

ARITH_MAX_GEQ2 = 130

ARITH_MIN_LT1 = 127

ARITH_MIN_LT2 = 128

ARITH_MOD_OVER_MOD = 117

ARITH_MOD_OVER_MOD_1 = 116

ARITH_MOD_OVER_MOD_MULT = 118

ARITH_PI_NOT_INT = 527

ARITH_POW_ELIM = 13

ARITH_SECENT_ELIM = 524

ARITH_SINE_PI2 = 521

ARITH_SINE_ZERO = 520

ARITH_STRING_PRED_ENTAIL = 11

ARITH_STRING_PRED_SAFE_APPROX = 12

ARITH_TANGENT_ELIM = 523

ARITH_TO_INT_ELIM_TO_REAL = 115

ARRAYS_EQ_RANGE_EXPAND = 22

ARRAYS_SELECT_CONST = 19

ARRAY_READ_OVER_WRITE = 131

ARRAY_READ_OVER_WRITE2 = 132

ARRAY_READ_OVER_WRITE_SPLIT = 135

ARRAY_STORE_OVERWRITE = 133

ARRAY_STORE_SELF = 134

ARRAY_STORE_SWAP = 136

BETA_REDUCE = 16

BOOL_AND_CONF = 149

BOOL_AND_CONF2 = 150

BOOL_AND_DE_MORGAN = 155

BOOL_DOUBLE_NOT_ELIM = 137

BOOL_DUAL_IMPL_EQ = 148

BOOL_EQ_FALSE = 141

BOOL_EQ_NREFL = 142

BOOL_EQ_TRUE = 140

BOOL_IMPLIES_DE_MORGAN = 154

BOOL_IMPLIES_OR_DISTRIB = 157

BOOL_IMPL_ELIM = 147

BOOL_IMPL_FALSE1 = 143

BOOL_IMPL_FALSE2 = 144

BOOL_IMPL_TRUE1 = 145

BOOL_IMPL_TRUE2 = 146

BOOL_NOT_EQ_ELIM1 = 165

BOOL_NOT_EQ_ELIM2 = 166

BOOL_NOT_FALSE = 139

BOOL_NOT_ITE_ELIM = 177

BOOL_NOT_TRUE = 138

BOOL_NOT_XOR_ELIM = 164

BOOL_OR_AND_DISTRIB = 156

BOOL_OR_DE_MORGAN = 153

BOOL_OR_TAUT = 151

BOOL_OR_TAUT2 = 152

BOOL_XOR_COMM = 162

BOOL_XOR_ELIM = 163

BOOL_XOR_FALSE = 160

BOOL_XOR_NREFL = 159

BOOL_XOR_REFL = 158

BOOL_XOR_TRUE = 161

BV_AND_CONCAT_PULLUP = 269

BV_AND_CONCAT_PULLUP2 = 272

BV_AND_CONCAT_PULLUP3 = 275

BV_AND_SIMPLIFY_1 = 201

BV_AND_SIMPLIFY_2 = 202

BV_ASHR_BY_CONST_0 = 266

BV_ASHR_BY_CONST_1 = 267

BV_ASHR_BY_CONST_2 = 268

BV_ASHR_ZERO = 304

BV_BITWISE_SLICING = 62

BV_COMMUTATIVE_ADD = 218

BV_COMMUTATIVE_COMP = 212

BV_COMMUTATIVE_XOR = 211

BV_COMP_ELIMINATE = 232

BV_CONCAT_EXTRACT_MERGE = 186

BV_CONCAT_MERGE_CONST = 217

BV_EQ_EXTRACT_ELIM1 = 193

BV_EQ_EXTRACT_ELIM2 = 194

BV_EQ_EXTRACT_ELIM3 = 195

BV_EQ_NOT_SOLVE = 223

BV_EQ_XOR_SOLVE = 222

BV_EXTRACT_CONCAT_1 = 189

BV_EXTRACT_CONCAT_2 = 190

BV_EXTRACT_CONCAT_3 = 191

BV_EXTRACT_CONCAT_4 = 192

BV_EXTRACT_EXTRACT = 187

BV_EXTRACT_MULT_LEADING_BIT = 295

BV_EXTRACT_NOT = 196

BV_EXTRACT_SIGN_EXTEND_1 = 197

BV_EXTRACT_SIGN_EXTEND_2 = 198

BV_EXTRACT_SIGN_EXTEND_3 = 199

BV_EXTRACT_WHOLE = 188

BV_ITE_CONST_CHILDREN_1 = 251

BV_ITE_CONST_CHILDREN_2 = 252

BV_ITE_EQUAL_CHILDREN = 250

BV_ITE_EQUAL_COND_1 = 253

BV_ITE_EQUAL_COND_2 = 254

BV_ITE_EQUAL_COND_3 = 255

BV_ITE_MERGE_ELSE_ELSE = 259

BV_ITE_MERGE_ELSE_IF = 257

BV_ITE_MERGE_THEN_ELSE = 258

BV_ITE_MERGE_THEN_IF = 256

BV_ITE_WIDTH_ONE = 220

BV_ITE_WIDTH_ONE_NOT = 221

BV_LSHR_BY_CONST_0 = 263

BV_LSHR_BY_CONST_1 = 264

BV_LSHR_BY_CONST_2 = 265

BV_LSHR_ZERO = 303

BV_LT_SELF = 285

BV_MERGE_SIGN_EXTEND_1 = 307

BV_MERGE_SIGN_EXTEND_2 = 308

BV_MULT_POW2_1 = 292

BV_MULT_POW2_2 = 293

BV_MULT_POW2_2B = 294

BV_MULT_SLT_MULT_1 = 209

BV_MULT_SLT_MULT_2 = 210

BV_NAND_ELIMINATE = 237

BV_NEGO_ELIMINATE = 249

BV_NOR_ELIMINATE = 238

BV_NOT_IDEMP = 281

BV_NOT_NEQ = 215

BV_NOT_ULT = 291

BV_NOT_XOR = 200

BV_OR_CONCAT_PULLUP = 270

BV_OR_CONCAT_PULLUP2 = 273

BV_OR_CONCAT_PULLUP3 = 276

BV_OR_SIMPLIFY_1 = 203

BV_OR_SIMPLIFY_2 = 204

BV_REDAND_ELIMINATE = 230

BV_REDOR_ELIMINATE = 229

BV_REPEAT_ELIM = 63

BV_ROTATE_LEFT_ELIMINATE_1 = 233

BV_ROTATE_LEFT_ELIMINATE_2 = 234

BV_ROTATE_RIGHT_ELIMINATE_1 = 235

BV_ROTATE_RIGHT_ELIMINATE_2 = 236

BV_SADDO_ELIMINATE = 243

BV_SDIVO_ELIMINATE = 244

BV_SDIV_ELIMINATE = 240

BV_SGE_ELIMINATE = 227

BV_SGT_ELIMINATE = 226

BV_SHL_BY_CONST_0 = 260

BV_SHL_BY_CONST_1 = 261

BV_SHL_BY_CONST_2 = 262

BV_SHL_ZERO = 302

BV_SIGN_EXTEND_ELIMINATE_0 = 214

BV_SIGN_EXTEND_EQ_CONST_1 = 309

BV_SIGN_EXTEND_EQ_CONST_2 = 310

BV_SIGN_EXTEND_ULT_CONST_1 = 315

BV_SIGN_EXTEND_ULT_CONST_2 = 316

BV_SIGN_EXTEND_ULT_CONST_3 = 317

BV_SIGN_EXTEND_ULT_CONST_4 = 318

BV_SLE_ELIMINATE = 228

BV_SLE_SELF = 289

BV_SMOD_ELIMINATE = 245

BV_SMULO_ELIM = 61

BV_SREM_ELIMINATE = 246

BV_SSUBO_ELIMINATE = 248

BV_SUB_ELIMINATE = 219

BV_UADDO_ELIMINATE = 242

BV_UDIV_ONE = 298

BV_UDIV_POW2_NOT_ONE = 296

BV_UDIV_ZERO = 297

BV_UGE_ELIMINATE = 225

BV_UGT_ELIMINATE = 224

BV_UGT_UREM = 305

BV_ULE_ELIMINATE = 231

BV_ULE_MAX = 290

BV_ULE_SELF = 286

BV_ULE_ZERO = 287

BV_ULT_ADD_ONE = 208

BV_ULT_ONE = 306

BV_ULT_ONES = 216

BV_ULT_SELF = 284

BV_ULT_ZERO_1 = 282

BV_ULT_ZERO_2 = 283

BV_UMULO_ELIM = 60

BV_UREM_ONE = 300

BV_UREM_POW2_NOT_ONE = 299

BV_UREM_SELF = 301

BV_USUBO_ELIMINATE = 247

BV_XNOR_ELIMINATE = 239

BV_XOR_CONCAT_PULLUP = 271

BV_XOR_CONCAT_PULLUP2 = 274

BV_XOR_CONCAT_PULLUP3 = 277

BV_XOR_DUPLICATE = 278

BV_XOR_NOT = 280

BV_XOR_ONES = 279

BV_XOR_SIMPLIFY_1 = 205

BV_XOR_SIMPLIFY_2 = 206

BV_XOR_SIMPLIFY_3 = 207

BV_ZERO_EXTEND_ELIMINATE = 241

BV_ZERO_EXTEND_ELIMINATE_0 = 213

BV_ZERO_EXTEND_EQ_CONST_1 = 311

BV_ZERO_EXTEND_EQ_CONST_2 = 312

BV_ZERO_EXTEND_ULT_CONST_1 = 313

BV_ZERO_EXTEND_ULT_CONST_2 = 314

BV_ZERO_ULE = 288

DISTINCT_BINARY_ELIM = 511

DISTINCT_CARD_CONFLICT = 2

DISTINCT_ELIM = 1

DISTINCT_FALSE = 14

DISTINCT_TRUE = 15

DT_COLLAPSE_SELECTOR = 41

DT_COLLAPSE_TESTER = 42

DT_COLLAPSE_TESTER_SINGLETON = 43

DT_COLLAPSE_UPDATER = 48

DT_CONS_EQ = 45

DT_CONS_EQ_CLASH = 46

DT_CYCLE = 47

DT_INST = 40

DT_MATCH_ELIM = 50

DT_UPDATER_ELIM = 49

EQ_COND_DEQ = 509

EQ_ITE_LIFT = 510

EQ_REFL = 507

EQ_SYMM = 508

EXISTS_ELIM = 23

INT_TO_BV_ELIM = 4

ITE_ELSE_FALSE = 169

ITE_ELSE_LOOKAHEAD = 183

ITE_ELSE_LOOKAHEAD_NOT_SELF = 175

ITE_ELSE_LOOKAHEAD_SELF = 173

ITE_ELSE_NEG_LOOKAHEAD = 185

ITE_ELSE_TRUE = 171

ITE_EQ_BRANCH = 181

ITE_EXPAND = 176

ITE_FALSE_COND = 179

ITE_NEG_BRANCH = 167

ITE_NOT_COND = 180

ITE_THEN_FALSE = 170

ITE_THEN_LOOKAHEAD = 182

ITE_THEN_LOOKAHEAD_NOT_SELF = 174

ITE_THEN_LOOKAHEAD_SELF = 172

ITE_THEN_NEG_LOOKAHEAD = 184

ITE_THEN_TRUE = 168

ITE_TRUE_COND = 178

LAMBDA_ELIM = 17

MACRO_ARITH_INT_EQ_CONFLICT = 8

MACRO_ARITH_INT_GEQ_TIGHTEN = 9

MACRO_ARITH_STRING_PRED_ENTAIL = 10

MACRO_ARRAYS_NORMALIZE_CONSTANT = 21

MACRO_ARRAYS_NORMALIZE_OP = 20

MACRO_BOOL_BV_INVERT_SOLVE = 7

MACRO_BOOL_EQ_CONST_EQ = 6

MACRO_BOOL_NNF_NORM = 5

MACRO_BV_AND_OR_XOR_CONCAT_PULLUP = 55

MACRO_BV_AND_SIMPLIFY = 53

MACRO_BV_CONCAT_CONSTANT_MERGE = 58

MACRO_BV_CONCAT_EXTRACT_MERGE = 57

MACRO_BV_EQ_SOLVE = 59

MACRO_BV_EXTRACT_CONCAT = 51

MACRO_BV_MULT_SLT_MULT = 56

MACRO_BV_OR_SIMPLIFY = 52

MACRO_BV_XOR_SIMPLIFY = 54

MACRO_DT_CONS_EQ = 44

MACRO_LAMBDA_CAPTURE_AVOID = 18

MACRO_QUANT_DT_VAR_EXPAND = 34

MACRO_QUANT_ELIM_SHADOW = 25

MACRO_QUANT_MERGE_PRENEX = 26

MACRO_QUANT_MINISCOPE = 29

MACRO_QUANT_PARTITION_CONNECTED_FV = 35

MACRO_QUANT_PRENEX = 28

MACRO_QUANT_REWRITE_BODY = 39

MACRO_QUANT_VAR_ELIM_EQ = 36

MACRO_QUANT_VAR_ELIM_INEQ = 38

MACRO_RE_INTER_UNION_CONST_ELIM = 76

MACRO_RE_INTER_UNION_INCLUSION = 83

MACRO_STR_COMPONENT_CTN = 73

MACRO_STR_CONST_NCTN_CONCAT = 74

MACRO_STR_EQ_LEN_UNIFY = 66

MACRO_STR_EQ_LEN_UNIFY_PREFIX = 65

MACRO_STR_IN_RE_INCLUSION = 75

MACRO_STR_SPLIT_CTN = 67

MACRO_STR_STRIP_ENDPOINTS = 68

MACRO_SUBSTR_STRIP_SYM_LENGTH = 91

NONE = 0

QUANT_DT_SPLIT = 33

QUANT_MERGE_PRENEX = 27

QUANT_MINISCOPE_AND = 30

QUANT_MINISCOPE_ITE = 32

QUANT_MINISCOPE_OR = 31

QUANT_UNUSED_VARS = 24

QUANT_VAR_ELIM_EQ = 37

RE_ALL_ELIM = 455

RE_CONCAT_MERGE = 464

RE_CONCAT_STAR_REPEAT = 461

RE_CONCAT_STAR_SUBSUME1 = 462

RE_CONCAT_STAR_SUBSUME2 = 463

RE_CONCAT_STAR_SWAP = 460

RE_DIFF_ELIM = 457

RE_EQ_ELIM = 82

RE_INTER_ALL = 467

RE_INTER_CSTRING = 478

RE_INTER_CSTRING_NEG = 479

RE_INTER_INCLUSION = 84

RE_IN_COMP = 500

RE_IN_CSTRING = 499

RE_IN_EMPTY = 496

RE_IN_SIGMA = 497

RE_IN_SIGMA_STAR = 498

RE_LOOP_ELIM = 81

RE_LOOP_NEG = 477

RE_OPT_ELIM = 456

RE_PLUS_ELIM = 458

RE_RANGE_EMP = 472

RE_RANGE_NON_SINGLETON_1 = 473

RE_RANGE_NON_SINGLETON_2 = 474

RE_RANGE_REFL = 471

RE_REPEAT_ELIM = 459

RE_STAR_EMP = 469

RE_STAR_NONE = 468

RE_STAR_STAR = 470

RE_STAR_UNION_CHAR = 475

RE_STAR_UNION_DROP_EMP = 476

RE_UNION_ALL = 465

RE_UNION_CONST_ELIM = 466

RE_UNION_INCLUSION = 85

SEQ_EVAL_OP = 77

SEQ_LEN_REV = 483

SEQ_LEN_UNIT = 493

SEQ_NTH_UNIT = 494

SEQ_REV_CONCAT = 485

SEQ_REV_REV = 484

SEQ_REV_UNIT = 495

SETS_CARD_EMP = 531

SETS_CARD_MINUS = 530

SETS_CARD_SINGLETON = 528

SETS_CARD_UNION = 529

SETS_CHOOSE_SINGLETON = 334

SETS_EQ_SINGLETON_EMP = 319

SETS_EVAL_OP = 92

SETS_INSERT_ELIM = 93

SETS_INTER_COMM = 324

SETS_INTER_EMP1 = 325

SETS_INTER_EMP2 = 326

SETS_INTER_MEMBER = 331

SETS_IS_EMPTY_ELIM = 336

SETS_IS_SINGLETON_ELIM = 337

SETS_MEMBER_EMP = 321

SETS_MEMBER_SINGLETON = 320

SETS_MINUS_EMP1 = 327

SETS_MINUS_EMP2 = 328

SETS_MINUS_MEMBER = 332

SETS_MINUS_SELF = 335

SETS_SUBSET_ELIM = 322

SETS_UNION_COMM = 323

SETS_UNION_EMP1 = 329

SETS_UNION_EMP2 = 330

SETS_UNION_MEMBER = 333

STR_AT_ELIM = 385

STR_CONCAT_CLASH = 355

STR_CONCAT_CLASH2 = 357

STR_CONCAT_CLASH2_REV = 358

STR_CONCAT_CLASH_REV = 356

STR_CONCAT_UNIFY = 359

STR_CONCAT_UNIFY_BASE = 361

STR_CONCAT_UNIFY_BASE_REV = 362

STR_CONCAT_UNIFY_REV = 360

STR_CONTAINS_CHAR = 384

STR_CONTAINS_CONCAT_FIND = 379

STR_CONTAINS_CONCAT_FIND_CONTRA = 380

STR_CONTAINS_EMP = 383

STR_CONTAINS_LEQ_LEN_EQ = 382

STR_CONTAINS_REFL = 378

STR_CONTAINS_REPL_CHAR = 439

STR_CONTAINS_REPL_SELF = 441

STR_CONTAINS_REPL_SELF_TGT_CHAR = 440

STR_CONTAINS_REPL_TGT = 442

STR_CONTAINS_SPLIT_CHAR = 381

STR_CTN_MULTISET_SUBSET = 64

STR_EQ_CTN_FALSE = 338

STR_EQ_CTN_FULL_FALSE1 = 339

STR_EQ_CTN_FULL_FALSE2 = 340

STR_EQ_LEN_FALSE = 341

STR_EQ_REPL_EMP_TGT_NEMP = 490

STR_EQ_REPL_LEN_ONE_EMP_PREFIX = 489

STR_EQ_REPL_NEMP_SRC_EMP = 491

STR_EQ_REPL_NO_CHANGE = 487

STR_EQ_REPL_SELF_EMP = 486

STR_EQ_REPL_SELF_SRC = 492

STR_EQ_REPL_TGT_EQ_LEN = 488

STR_FROM_INT_NO_CTN_NONDIGIT = 431

STR_INDEXOF_CONTAINS_CONCAT_PRE = 409

STR_INDEXOF_CONTAINS_PRE = 408

STR_INDEXOF_EQ_IRR = 411

STR_INDEXOF_FIND_EMP = 410

STR_INDEXOF_NO_CONTAINS = 405

STR_INDEXOF_OOB = 406

STR_INDEXOF_OOB2 = 407

STR_INDEXOF_RE_EMP_RE = 413

STR_INDEXOF_RE_EVAL = 78

STR_INDEXOF_RE_NONE = 412

STR_INDEXOF_SELF = 404

STR_IN_RE_CONCAT_STAR_CHAR = 88

STR_IN_RE_CONSUME = 87

STR_IN_RE_CONTAINS = 504

STR_IN_RE_EVAL = 86

STR_IN_RE_FROM_INT_DIG_RANGE = 506

STR_IN_RE_FROM_INT_NEMP_DIG_RANGE = 505

STR_IN_RE_INTER_ELIM = 502

STR_IN_RE_RANGE_ELIM = 503

STR_IN_RE_SIGMA = 89

STR_IN_RE_SIGMA_STAR = 90

STR_IN_RE_UNION_ELIM = 501

STR_IS_DIGIT_ELIM = 423

STR_LEN_CONCAT_REC = 401

STR_LEN_EQ_ZERO_BASE = 403

STR_LEN_EQ_ZERO_CONCAT_REC = 402

STR_LEN_REPLACE_ALL_INV = 351

STR_LEN_REPLACE_INV = 350

STR_LEN_SUBSTR_IN_RANGE = 354

STR_LEN_UPDATE_INV = 352

STR_LEQ_CONCAT_BASE_1 = 428

STR_LEQ_CONCAT_BASE_2 = 429

STR_LEQ_CONCAT_FALSE = 426

STR_LEQ_CONCAT_TRUE = 427

STR_LEQ_EMPTY = 424

STR_LEQ_EMPTY_EQ = 425

STR_LT_ELIM = 430

STR_OVERLAP_ENDPOINTS_CTN = 70

STR_OVERLAP_ENDPOINTS_INDEXOF = 71

STR_OVERLAP_ENDPOINTS_REPLACE = 72

STR_OVERLAP_SPLIT_CTN = 69

STR_PREFIXOF_ELIM = 363

STR_PREFIXOF_EQ = 365

STR_PREFIXOF_ONE = 367

STR_REPLACE_ALL_EMPTY = 396

STR_REPLACE_ALL_ID = 397

STR_REPLACE_ALL_NO_CONTAINS = 395

STR_REPLACE_ALL_SELF = 398

STR_REPLACE_DUAL_CTN = 434

STR_REPLACE_DUAL_CTN_FALSE = 435

STR_REPLACE_EMPTY = 392

STR_REPLACE_EMP_CTN_SRC = 437

STR_REPLACE_FIND_BASE = 390

STR_REPLACE_FIND_FIRST_CONCAT = 391

STR_REPLACE_FIND_PRE = 394

STR_REPLACE_ID = 387

STR_REPLACE_NO_CONTAINS = 389

STR_REPLACE_ONE_PRE = 393

STR_REPLACE_PREFIX = 388

STR_REPLACE_RE_ALL_EVAL = 80

STR_REPLACE_RE_ALL_NONE = 400

STR_REPLACE_RE_EVAL = 79

STR_REPLACE_RE_NONE = 399

STR_REPLACE_SELF = 386

STR_REPLACE_SELF_CTN_SIMP = 436

STR_REPL_REPL_DUAL_ITE1 = 452

STR_REPL_REPL_DUAL_ITE2 = 453

STR_REPL_REPL_DUAL_SELF = 451

STR_REPL_REPL_LEN_ID = 443

STR_REPL_REPL_LOOKAHEAD_ID_SIMP = 454

STR_REPL_REPL_SRC_INV_NO_CTN1 = 448

STR_REPL_REPL_SRC_INV_NO_CTN2 = 449

STR_REPL_REPL_SRC_INV_NO_CTN3 = 450

STR_REPL_REPL_SRC_SELF = 447

STR_REPL_REPL_SRC_TGT_NO_CTN = 444

STR_REPL_REPL_TGT_NO_CTN = 446

STR_REPL_REPL_TGT_SELF = 445

STR_SUBSTR_CHAR_START_EQ_LEN = 438

STR_SUBSTR_COMBINE1 = 369

STR_SUBSTR_COMBINE2 = 370

STR_SUBSTR_COMBINE3 = 371

STR_SUBSTR_COMBINE4 = 372

STR_SUBSTR_CONCAT1 = 373

STR_SUBSTR_CONCAT2 = 374

STR_SUBSTR_CTN = 433

STR_SUBSTR_CTN_CONTRA = 432

STR_SUBSTR_EMPTY_RANGE = 343

STR_SUBSTR_EMPTY_START = 344

STR_SUBSTR_EMPTY_START_NEG = 345

STR_SUBSTR_EMPTY_STR = 342

STR_SUBSTR_EQ_EMPTY = 347

STR_SUBSTR_EQ_EMPTY_LEQ_LEN = 349

STR_SUBSTR_FULL = 376

STR_SUBSTR_FULL_EQ = 377

STR_SUBSTR_LEN_INCLUDE = 480

STR_SUBSTR_LEN_INCLUDE_PRE = 481

STR_SUBSTR_LEN_NORM = 482

STR_SUBSTR_REPLACE = 375

STR_SUBSTR_SUBSTR_START_GEQ_LEN = 346

STR_SUBSTR_Z_EQ_EMPTY_LEQ = 348

STR_SUFFIXOF_ELIM = 364

STR_SUFFIXOF_EQ = 366

STR_SUFFIXOF_ONE = 368

STR_TO_INT_CONCAT_NEG_ONE = 422

STR_TO_LOWER_CONCAT = 414

STR_TO_LOWER_FROM_INT = 420

STR_TO_LOWER_LEN = 418

STR_TO_LOWER_UPPER = 416

STR_TO_UPPER_CONCAT = 415

STR_TO_UPPER_FROM_INT = 421

STR_TO_UPPER_LEN = 419

STR_TO_UPPER_LOWER = 417

STR_UPDATE_IN_FIRST_CONCAT = 353

UBV_TO_INT_ELIM = 3

UF_BV2NAT_GEQ_ELIM = 516

UF_BV2NAT_INT2BV = 512

UF_BV2NAT_INT2BV_EXTEND = 513

UF_BV2NAT_INT2BV_EXTRACT = 514

UF_INT2BV_BV2NAT = 515

UF_INT2BV_BVULE_EQUIV = 518

UF_INT2BV_BVULT_EQUIV = 517

UF_SBV_TO_INT_ELIM = 519