diff options
Diffstat (limited to 'src/proof/proof_rule.cpp')
| -rw-r--r-- | src/proof/proof_rule.cpp | 42 |
1 files changed, 1 insertions, 41 deletions
diff --git a/src/proof/proof_rule.cpp b/src/proof/proof_rule.cpp index 676fa6a63..def57532d 100644 --- a/src/proof/proof_rule.cpp +++ b/src/proof/proof_rule.cpp @@ -121,47 +121,7 @@ const char* toString(PfRule id) case PfRule::ARRAYS_TRUST: return "ARRAYS_TRUST"; //================================================= Bit-Vector rules case PfRule::BV_BITBLAST: return "BV_BITBLAST"; - case PfRule::BV_BITBLAST_CONST: return "BV_BITBLAST_CONST"; - case PfRule::BV_BITBLAST_VAR: return "BV_BITBLAST_VAR"; - case PfRule::BV_BITBLAST_EQUAL: return "BV_BITBLAST_EQUAL"; - case PfRule::BV_BITBLAST_ULT: return "BV_BITBLAST_ULT"; - case PfRule::BV_BITBLAST_ULE: return "BV_BITBLAST_ULE"; - case PfRule::BV_BITBLAST_UGT: return "BV_BITBLAST_UGT"; - case PfRule::BV_BITBLAST_UGE: return "BV_BITBLAST_UGE"; - case PfRule::BV_BITBLAST_SLT: return "BV_BITBLAST_SLT"; - case PfRule::BV_BITBLAST_SLE: return "BV_BITBLAST_SLE"; - case PfRule::BV_BITBLAST_SGT: return "BV_BITBLAST_SGT"; - case PfRule::BV_BITBLAST_SGE: return "BV_BITBLAST_SGE"; - case PfRule::BV_BITBLAST_NOT: return "BV_BITBLAST_NOT"; - case PfRule::BV_BITBLAST_CONCAT: return "BV_BITBLAST_CONCAT"; - case PfRule::BV_BITBLAST_AND: return "BV_BITBLAST_AND"; - case PfRule::BV_BITBLAST_OR: return "BV_BITBLAST_OR"; - case PfRule::BV_BITBLAST_XOR: return "BV_BITBLAST_XOR"; - case PfRule::BV_BITBLAST_XNOR: return "BV_BITBLAST_XNOR"; - case PfRule::BV_BITBLAST_NAND: return "BV_BITBLAST_NAND"; - case PfRule::BV_BITBLAST_NOR: return "BV_BITBLAST_NOR"; - case PfRule::BV_BITBLAST_COMP: return "BV_BITBLAST_COMP"; - case PfRule::BV_BITBLAST_MULT: return "BV_BITBLAST_MULT"; - case PfRule::BV_BITBLAST_ADD: return "BV_BITBLAST_ADD"; - case PfRule::BV_BITBLAST_SUB: return "BV_BITBLAST_SUB"; - case PfRule::BV_BITBLAST_NEG: return "BV_BITBLAST_NEG"; - case PfRule::BV_BITBLAST_UDIV: return "BV_BITBLAST_UDIV"; - case PfRule::BV_BITBLAST_UREM: return "BV_BITBLAST_UREM"; - case PfRule::BV_BITBLAST_SDIV: return "BV_BITBLAST_SDIV"; - case PfRule::BV_BITBLAST_SREM: return "BV_BITBLAST_SREM"; - case PfRule::BV_BITBLAST_SMOD: return "BV_BITBLAST_SMOD"; - case PfRule::BV_BITBLAST_SHL: return "BV_BITBLAST_SHL"; - case PfRule::BV_BITBLAST_LSHR: return "BV_BITBLAST_LSHR"; - case PfRule::BV_BITBLAST_ASHR: return "BV_BITBLAST_ASHR"; - case PfRule::BV_BITBLAST_ULTBV: return "BV_BITBLAST_ULTBV"; - case PfRule::BV_BITBLAST_SLTBV: return "BV_BITBLAST_SLTBV"; - case PfRule::BV_BITBLAST_ITE: return "BV_BITBLAST_ITE"; - case PfRule::BV_BITBLAST_EXTRACT: return "BV_BITBLAST_EXTRACT"; - case PfRule::BV_BITBLAST_REPEAT: return "BV_BITBLAST_REPEAT"; - case PfRule::BV_BITBLAST_ZERO_EXTEND: return "BV_BITBLAST_ZERO_EXTEND"; - case PfRule::BV_BITBLAST_SIGN_EXTEND: return "BV_BITBLAST_SIGN_EXTEND"; - case PfRule::BV_BITBLAST_ROTATE_RIGHT: return "BV_BITBLAST_ROTATE_RIGHT"; - case PfRule::BV_BITBLAST_ROTATE_LEFT: return "BV_BITBLAST_ROTATE_LEFT"; + case PfRule::BV_BITBLAST_STEP: return "BV_BITBLAST_STEP"; case PfRule::BV_EAGER_ATOM: return "BV_EAGER_ATOM"; //================================================= Datatype rules case PfRule::DT_UNIF: return "DT_UNIF"; |