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 = 125

ARITH_ABS_INT_GT = 126

ARITH_ABS_REAL_GT = 127

ARITH_COSECENT_ELIM = 528

ARITH_COSINE_ELIM = 525

ARITH_COTANGENT_ELIM = 529

ARITH_DIVISIBLE_ELIM = 124

ARITH_DIV_ELIM_TO_REAL1 = 117

ARITH_DIV_ELIM_TO_REAL2 = 118

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 = 128

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 = 122

ARITH_INT_GEQ_TIGHTEN = 123

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 = 129

ARITH_LEQ_NORM = 109

ARITH_MAX_GEQ1 = 132

ARITH_MAX_GEQ2 = 133

ARITH_MIN_LT1 = 130

ARITH_MIN_LT2 = 131

ARITH_MOD_OVER_MOD = 120

ARITH_MOD_OVER_MOD_1 = 119

ARITH_MOD_OVER_MOD_MULT = 121

ARITH_PI_NOT_INT = 530

ARITH_POW_ELIM = 13

ARITH_SECENT_ELIM = 527

ARITH_SINE_PI2 = 524

ARITH_SINE_ZERO = 523

ARITH_STRING_PRED_ENTAIL = 11

ARITH_STRING_PRED_SAFE_APPROX = 12

ARITH_TANGENT_ELIM = 526

ARITH_TO_INT_ELIM = 115

ARITH_TO_INT_ELIM_TO_REAL = 116

ARRAYS_EQ_RANGE_EXPAND = 22

ARRAYS_SELECT_CONST = 19

ARRAY_READ_OVER_WRITE = 134

ARRAY_READ_OVER_WRITE2 = 135

ARRAY_READ_OVER_WRITE_SPLIT = 138

ARRAY_STORE_OVERWRITE = 136

ARRAY_STORE_SELF = 137

ARRAY_STORE_SWAP = 139

BETA_REDUCE = 16

BOOL_AND_CONF = 152

BOOL_AND_CONF2 = 153

BOOL_AND_DE_MORGAN = 158

BOOL_DOUBLE_NOT_ELIM = 140

BOOL_DUAL_IMPL_EQ = 151

BOOL_EQ_FALSE = 144

BOOL_EQ_NREFL = 145

BOOL_EQ_TRUE = 143

BOOL_IMPLIES_DE_MORGAN = 157

BOOL_IMPLIES_OR_DISTRIB = 160

BOOL_IMPL_ELIM = 150

BOOL_IMPL_FALSE1 = 146

BOOL_IMPL_FALSE2 = 147

BOOL_IMPL_TRUE1 = 148

BOOL_IMPL_TRUE2 = 149

BOOL_NOT_EQ_ELIM1 = 168

BOOL_NOT_EQ_ELIM2 = 169

BOOL_NOT_FALSE = 142

BOOL_NOT_ITE_ELIM = 180

BOOL_NOT_TRUE = 141

BOOL_NOT_XOR_ELIM = 167

BOOL_OR_AND_DISTRIB = 159

BOOL_OR_DE_MORGAN = 156

BOOL_OR_TAUT = 154

BOOL_OR_TAUT2 = 155

BOOL_XOR_COMM = 165

BOOL_XOR_ELIM = 166

BOOL_XOR_FALSE = 163

BOOL_XOR_NREFL = 162

BOOL_XOR_REFL = 161

BOOL_XOR_TRUE = 164

BV_AND_CONCAT_PULLUP = 272

BV_AND_CONCAT_PULLUP2 = 275

BV_AND_CONCAT_PULLUP3 = 278

BV_AND_SIMPLIFY_1 = 204

BV_AND_SIMPLIFY_2 = 205

BV_ASHR_BY_CONST_0 = 269

BV_ASHR_BY_CONST_1 = 270

BV_ASHR_BY_CONST_2 = 271

BV_ASHR_ZERO = 307

BV_BITWISE_SLICING = 62

BV_COMMUTATIVE_ADD = 221

BV_COMMUTATIVE_COMP = 215

BV_COMMUTATIVE_XOR = 214

BV_COMP_ELIMINATE = 235

BV_CONCAT_EXTRACT_MERGE = 189

BV_CONCAT_MERGE_CONST = 220

BV_EQ_EXTRACT_ELIM1 = 196

BV_EQ_EXTRACT_ELIM2 = 197

BV_EQ_EXTRACT_ELIM3 = 198

BV_EQ_NOT_SOLVE = 226

BV_EQ_XOR_SOLVE = 225

BV_EXTRACT_CONCAT_1 = 192

BV_EXTRACT_CONCAT_2 = 193

BV_EXTRACT_CONCAT_3 = 194

BV_EXTRACT_CONCAT_4 = 195

BV_EXTRACT_EXTRACT = 190

BV_EXTRACT_MULT_LEADING_BIT = 298

BV_EXTRACT_NOT = 199

BV_EXTRACT_SIGN_EXTEND_1 = 200

BV_EXTRACT_SIGN_EXTEND_2 = 201

BV_EXTRACT_SIGN_EXTEND_3 = 202

BV_EXTRACT_WHOLE = 191

BV_ITE_CONST_CHILDREN_1 = 254

BV_ITE_CONST_CHILDREN_2 = 255

BV_ITE_EQUAL_CHILDREN = 253

BV_ITE_EQUAL_COND_1 = 256

BV_ITE_EQUAL_COND_2 = 257

BV_ITE_EQUAL_COND_3 = 258

BV_ITE_MERGE_ELSE_ELSE = 262

BV_ITE_MERGE_ELSE_IF = 260

BV_ITE_MERGE_THEN_ELSE = 261

BV_ITE_MERGE_THEN_IF = 259

BV_ITE_WIDTH_ONE = 223

BV_ITE_WIDTH_ONE_NOT = 224

BV_LSHR_BY_CONST_0 = 266

BV_LSHR_BY_CONST_1 = 267

BV_LSHR_BY_CONST_2 = 268

BV_LSHR_ZERO = 306

BV_LT_SELF = 288

BV_MERGE_SIGN_EXTEND_1 = 310

BV_MERGE_SIGN_EXTEND_2 = 311

BV_MULT_POW2_1 = 295

BV_MULT_POW2_2 = 296

BV_MULT_POW2_2B = 297

BV_MULT_SLT_MULT_1 = 212

BV_MULT_SLT_MULT_2 = 213

BV_NAND_ELIMINATE = 240

BV_NEGO_ELIMINATE = 252

BV_NOR_ELIMINATE = 241

BV_NOT_IDEMP = 284

BV_NOT_NEQ = 218

BV_NOT_ULT = 294

BV_NOT_XOR = 203

BV_OR_CONCAT_PULLUP = 273

BV_OR_CONCAT_PULLUP2 = 276

BV_OR_CONCAT_PULLUP3 = 279

BV_OR_SIMPLIFY_1 = 206

BV_OR_SIMPLIFY_2 = 207

BV_REDAND_ELIMINATE = 233

BV_REDOR_ELIMINATE = 232

BV_REPEAT_ELIM = 63

BV_ROTATE_LEFT_ELIMINATE_1 = 236

BV_ROTATE_LEFT_ELIMINATE_2 = 237

BV_ROTATE_RIGHT_ELIMINATE_1 = 238

BV_ROTATE_RIGHT_ELIMINATE_2 = 239

BV_SADDO_ELIMINATE = 246

BV_SDIVO_ELIMINATE = 247

BV_SDIV_ELIMINATE = 243

BV_SGE_ELIMINATE = 230

BV_SGT_ELIMINATE = 229

BV_SHL_BY_CONST_0 = 263

BV_SHL_BY_CONST_1 = 264

BV_SHL_BY_CONST_2 = 265

BV_SHL_ZERO = 305

BV_SIGN_EXTEND_ELIMINATE_0 = 217

BV_SIGN_EXTEND_EQ_CONST_1 = 312

BV_SIGN_EXTEND_EQ_CONST_2 = 313

BV_SIGN_EXTEND_ULT_CONST_1 = 318

BV_SIGN_EXTEND_ULT_CONST_2 = 319

BV_SIGN_EXTEND_ULT_CONST_3 = 320

BV_SIGN_EXTEND_ULT_CONST_4 = 321

BV_SLE_ELIMINATE = 231

BV_SLE_SELF = 292

BV_SMOD_ELIMINATE = 248

BV_SMULO_ELIM = 61

BV_SREM_ELIMINATE = 249

BV_SSUBO_ELIMINATE = 251

BV_SUB_ELIMINATE = 222

BV_UADDO_ELIMINATE = 245

BV_UDIV_ONE = 301

BV_UDIV_POW2_NOT_ONE = 299

BV_UDIV_ZERO = 300

BV_UGE_ELIMINATE = 228

BV_UGT_ELIMINATE = 227

BV_UGT_UREM = 308

BV_ULE_ELIMINATE = 234

BV_ULE_MAX = 293

BV_ULE_SELF = 289

BV_ULE_ZERO = 290

BV_ULT_ADD_ONE = 211

BV_ULT_ONE = 309

BV_ULT_ONES = 219

BV_ULT_SELF = 287

BV_ULT_ZERO_1 = 285

BV_ULT_ZERO_2 = 286

BV_UMULO_ELIM = 60

BV_UREM_ONE = 303

BV_UREM_POW2_NOT_ONE = 302

BV_UREM_SELF = 304

BV_USUBO_ELIMINATE = 250

BV_XNOR_ELIMINATE = 242

BV_XOR_CONCAT_PULLUP = 274

BV_XOR_CONCAT_PULLUP2 = 277

BV_XOR_CONCAT_PULLUP3 = 280

BV_XOR_DUPLICATE = 281

BV_XOR_NOT = 283

BV_XOR_ONES = 282

BV_XOR_SIMPLIFY_1 = 208

BV_XOR_SIMPLIFY_2 = 209

BV_XOR_SIMPLIFY_3 = 210

BV_ZERO_EXTEND_ELIMINATE = 244

BV_ZERO_EXTEND_ELIMINATE_0 = 216

BV_ZERO_EXTEND_EQ_CONST_1 = 314

BV_ZERO_EXTEND_EQ_CONST_2 = 315

BV_ZERO_EXTEND_ULT_CONST_1 = 316

BV_ZERO_EXTEND_ULT_CONST_2 = 317

BV_ZERO_ULE = 291

DISTINCT_BINARY_ELIM = 514

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 = 512

EQ_ITE_LIFT = 513

EQ_REFL = 510

EQ_SYMM = 511

EXISTS_ELIM = 23

INT_TO_BV_ELIM = 4

ITE_ELSE_FALSE = 172

ITE_ELSE_LOOKAHEAD = 186

ITE_ELSE_LOOKAHEAD_NOT_SELF = 178

ITE_ELSE_LOOKAHEAD_SELF = 176

ITE_ELSE_NEG_LOOKAHEAD = 188

ITE_ELSE_TRUE = 174

ITE_EQ_BRANCH = 184

ITE_EXPAND = 179

ITE_FALSE_COND = 182

ITE_NEG_BRANCH = 170

ITE_NOT_COND = 183

ITE_THEN_FALSE = 173

ITE_THEN_LOOKAHEAD = 185

ITE_THEN_LOOKAHEAD_NOT_SELF = 177

ITE_THEN_LOOKAHEAD_SELF = 175

ITE_THEN_NEG_LOOKAHEAD = 187

ITE_THEN_TRUE = 171

ITE_TRUE_COND = 181

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 = 458

RE_CONCAT_MERGE = 467

RE_CONCAT_STAR_REPEAT = 464

RE_CONCAT_STAR_SUBSUME1 = 465

RE_CONCAT_STAR_SUBSUME2 = 466

RE_CONCAT_STAR_SWAP = 463

RE_DIFF_ELIM = 460

RE_EQ_ELIM = 82

RE_INTER_ALL = 470

RE_INTER_CSTRING = 481

RE_INTER_CSTRING_NEG = 482

RE_INTER_INCLUSION = 84

RE_IN_COMP = 503

RE_IN_CSTRING = 502

RE_IN_EMPTY = 499

RE_IN_SIGMA = 500

RE_IN_SIGMA_STAR = 501

RE_LOOP_ELIM = 81

RE_LOOP_NEG = 480

RE_OPT_ELIM = 459

RE_PLUS_ELIM = 461

RE_RANGE_EMP = 475

RE_RANGE_NON_SINGLETON_1 = 476

RE_RANGE_NON_SINGLETON_2 = 477

RE_RANGE_REFL = 474

RE_REPEAT_ELIM = 462

RE_STAR_EMP = 472

RE_STAR_NONE = 471

RE_STAR_STAR = 473

RE_STAR_UNION_CHAR = 478

RE_STAR_UNION_DROP_EMP = 479

RE_UNION_ALL = 468

RE_UNION_CONST_ELIM = 469

RE_UNION_INCLUSION = 85

SEQ_EVAL_OP = 77

SEQ_LEN_REV = 486

SEQ_LEN_UNIT = 496

SEQ_NTH_UNIT = 497

SEQ_REV_CONCAT = 488

SEQ_REV_REV = 487

SEQ_REV_UNIT = 498

SETS_CARD_EMP = 534

SETS_CARD_MINUS = 533

SETS_CARD_SINGLETON = 531

SETS_CARD_UNION = 532

SETS_CHOOSE_SINGLETON = 337

SETS_EQ_SINGLETON_EMP = 322

SETS_EVAL_OP = 92

SETS_INSERT_ELIM = 93

SETS_INTER_COMM = 327

SETS_INTER_EMP1 = 328

SETS_INTER_EMP2 = 329

SETS_INTER_MEMBER = 334

SETS_IS_EMPTY_ELIM = 339

SETS_IS_SINGLETON_ELIM = 340

SETS_MEMBER_EMP = 324

SETS_MEMBER_SINGLETON = 323

SETS_MINUS_EMP1 = 330

SETS_MINUS_EMP2 = 331

SETS_MINUS_MEMBER = 335

SETS_MINUS_SELF = 338

SETS_SUBSET_ELIM = 325

SETS_UNION_COMM = 326

SETS_UNION_EMP1 = 332

SETS_UNION_EMP2 = 333

SETS_UNION_MEMBER = 336

STR_AT_ELIM = 388

STR_CONCAT_CLASH = 358

STR_CONCAT_CLASH2 = 360

STR_CONCAT_CLASH2_REV = 361

STR_CONCAT_CLASH_REV = 359

STR_CONCAT_UNIFY = 362

STR_CONCAT_UNIFY_BASE = 364

STR_CONCAT_UNIFY_BASE_REV = 365

STR_CONCAT_UNIFY_REV = 363

STR_CONTAINS_CHAR = 387

STR_CONTAINS_CONCAT_FIND = 382

STR_CONTAINS_CONCAT_FIND_CONTRA = 383

STR_CONTAINS_EMP = 386

STR_CONTAINS_LEQ_LEN_EQ = 385

STR_CONTAINS_REFL = 381

STR_CONTAINS_REPL_CHAR = 442

STR_CONTAINS_REPL_SELF = 444

STR_CONTAINS_REPL_SELF_TGT_CHAR = 443

STR_CONTAINS_REPL_TGT = 445

STR_CONTAINS_SPLIT_CHAR = 384

STR_CTN_MULTISET_SUBSET = 64

STR_EQ_CTN_FALSE = 341

STR_EQ_CTN_FULL_FALSE1 = 342

STR_EQ_CTN_FULL_FALSE2 = 343

STR_EQ_LEN_FALSE = 344

STR_EQ_REPL_EMP_TGT_NEMP = 493

STR_EQ_REPL_LEN_ONE_EMP_PREFIX = 492

STR_EQ_REPL_NEMP_SRC_EMP = 494

STR_EQ_REPL_NO_CHANGE = 490

STR_EQ_REPL_SELF_EMP = 489

STR_EQ_REPL_SELF_SRC = 495

STR_EQ_REPL_TGT_EQ_LEN = 491

STR_FROM_INT_NO_CTN_NONDIGIT = 434

STR_INDEXOF_CONTAINS_CONCAT_PRE = 412

STR_INDEXOF_CONTAINS_PRE = 411

STR_INDEXOF_EQ_IRR = 414

STR_INDEXOF_FIND_EMP = 413

STR_INDEXOF_NO_CONTAINS = 408

STR_INDEXOF_OOB = 409

STR_INDEXOF_OOB2 = 410

STR_INDEXOF_RE_EMP_RE = 416

STR_INDEXOF_RE_EVAL = 78

STR_INDEXOF_RE_NONE = 415

STR_INDEXOF_SELF = 407

STR_IN_RE_CONCAT_STAR_CHAR = 88

STR_IN_RE_CONSUME = 87

STR_IN_RE_CONTAINS = 507

STR_IN_RE_EVAL = 86

STR_IN_RE_FROM_INT_DIG_RANGE = 509

STR_IN_RE_FROM_INT_NEMP_DIG_RANGE = 508

STR_IN_RE_INTER_ELIM = 505

STR_IN_RE_RANGE_ELIM = 506

STR_IN_RE_SIGMA = 89

STR_IN_RE_SIGMA_STAR = 90

STR_IN_RE_UNION_ELIM = 504

STR_IS_DIGIT_ELIM = 426

STR_LEN_CONCAT_REC = 404

STR_LEN_EQ_ZERO_BASE = 406

STR_LEN_EQ_ZERO_CONCAT_REC = 405

STR_LEN_REPLACE_ALL_INV = 354

STR_LEN_REPLACE_INV = 353

STR_LEN_SUBSTR_IN_RANGE = 357

STR_LEN_UPDATE_INV = 355

STR_LEQ_CONCAT_BASE_1 = 431

STR_LEQ_CONCAT_BASE_2 = 432

STR_LEQ_CONCAT_FALSE = 429

STR_LEQ_CONCAT_TRUE = 430

STR_LEQ_EMPTY = 427

STR_LEQ_EMPTY_EQ = 428

STR_LT_ELIM = 433

STR_OVERLAP_ENDPOINTS_CTN = 70

STR_OVERLAP_ENDPOINTS_INDEXOF = 71

STR_OVERLAP_ENDPOINTS_REPLACE = 72

STR_OVERLAP_SPLIT_CTN = 69

STR_PREFIXOF_ELIM = 366

STR_PREFIXOF_EQ = 368

STR_PREFIXOF_ONE = 370

STR_REPLACE_ALL_EMPTY = 399

STR_REPLACE_ALL_ID = 400

STR_REPLACE_ALL_NO_CONTAINS = 398

STR_REPLACE_ALL_SELF = 401

STR_REPLACE_DUAL_CTN = 437

STR_REPLACE_DUAL_CTN_FALSE = 438

STR_REPLACE_EMPTY = 395

STR_REPLACE_EMP_CTN_SRC = 440

STR_REPLACE_FIND_BASE = 393

STR_REPLACE_FIND_FIRST_CONCAT = 394

STR_REPLACE_FIND_PRE = 397

STR_REPLACE_ID = 390

STR_REPLACE_NO_CONTAINS = 392

STR_REPLACE_ONE_PRE = 396

STR_REPLACE_PREFIX = 391

STR_REPLACE_RE_ALL_EVAL = 80

STR_REPLACE_RE_ALL_NONE = 403

STR_REPLACE_RE_EVAL = 79

STR_REPLACE_RE_NONE = 402

STR_REPLACE_SELF = 389

STR_REPLACE_SELF_CTN_SIMP = 439

STR_REPL_REPL_DUAL_ITE1 = 455

STR_REPL_REPL_DUAL_ITE2 = 456

STR_REPL_REPL_DUAL_SELF = 454

STR_REPL_REPL_LEN_ID = 446

STR_REPL_REPL_LOOKAHEAD_ID_SIMP = 457

STR_REPL_REPL_SRC_INV_NO_CTN1 = 451

STR_REPL_REPL_SRC_INV_NO_CTN2 = 452

STR_REPL_REPL_SRC_INV_NO_CTN3 = 453

STR_REPL_REPL_SRC_SELF = 450

STR_REPL_REPL_SRC_TGT_NO_CTN = 447

STR_REPL_REPL_TGT_NO_CTN = 449

STR_REPL_REPL_TGT_SELF = 448

STR_SUBSTR_CHAR_START_EQ_LEN = 441

STR_SUBSTR_COMBINE1 = 372

STR_SUBSTR_COMBINE2 = 373

STR_SUBSTR_COMBINE3 = 374

STR_SUBSTR_COMBINE4 = 375

STR_SUBSTR_CONCAT1 = 376

STR_SUBSTR_CONCAT2 = 377

STR_SUBSTR_CTN = 436

STR_SUBSTR_CTN_CONTRA = 435

STR_SUBSTR_EMPTY_RANGE = 346

STR_SUBSTR_EMPTY_START = 347

STR_SUBSTR_EMPTY_START_NEG = 348

STR_SUBSTR_EMPTY_STR = 345

STR_SUBSTR_EQ_EMPTY = 350

STR_SUBSTR_EQ_EMPTY_LEQ_LEN = 352

STR_SUBSTR_FULL = 379

STR_SUBSTR_FULL_EQ = 380

STR_SUBSTR_LEN_INCLUDE = 483

STR_SUBSTR_LEN_INCLUDE_PRE = 484

STR_SUBSTR_LEN_NORM = 485

STR_SUBSTR_REPLACE = 378

STR_SUBSTR_SUBSTR_START_GEQ_LEN = 349

STR_SUBSTR_Z_EQ_EMPTY_LEQ = 351

STR_SUFFIXOF_ELIM = 367

STR_SUFFIXOF_EQ = 369

STR_SUFFIXOF_ONE = 371

STR_TO_INT_CONCAT_NEG_ONE = 425

STR_TO_LOWER_CONCAT = 417

STR_TO_LOWER_FROM_INT = 423

STR_TO_LOWER_LEN = 421

STR_TO_LOWER_UPPER = 419

STR_TO_UPPER_CONCAT = 418

STR_TO_UPPER_FROM_INT = 424

STR_TO_UPPER_LEN = 422

STR_TO_UPPER_LOWER = 420

STR_UPDATE_IN_FIRST_CONCAT = 356

UBV_TO_INT_ELIM = 3

UF_BV2NAT_GEQ_ELIM = 519

UF_BV2NAT_INT2BV = 515

UF_BV2NAT_INT2BV_EXTEND = 516

UF_BV2NAT_INT2BV_EXTRACT = 517

UF_INT2BV_BV2NAT = 518

UF_INT2BV_BVULE_EQUIV = 521

UF_INT2BV_BVULT_EQUIV = 520

UF_SBV_TO_INT_ELIM = 522