src/expr/proof_rule.cpp

   1 /******************************************************************************
   2  * Top contributors (to current version):
   3  *   Andrew Reynolds, Haniel Barbosa, Gereon Kremer
   4  *
   5  * This file is part of the cvc5 project.
   6  *
   7  * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
   8  * in the top-level source directory and their institutional affiliations.
   9  * All rights reserved.  See the file COPYING in the top-level source
  10  * directory for licensing information.
  11  * ****************************************************************************
  12  *
  13  * Implementation of proof rule.
  14  */
  15
  16 #include "expr/proof_rule.h"
  17
  18 #include <iostream>
  19
  20 namespace cvc5 {
  21
  22 const char* toString(PfRule id)
  23 {
  24   switch (id)
  25   {
  26     //================================================= Core rules
  27     case PfRule::ASSUME: return "ASSUME";
  28     case PfRule::SCOPE: return "SCOPE";
  29     case PfRule::SUBS: return "SUBS";
  30     case PfRule::REWRITE: return "REWRITE";
  31     case PfRule::EVALUATE: return "EVALUATE";
  32     case PfRule::MACRO_SR_EQ_INTRO: return "MACRO_SR_EQ_INTRO";
  33     case PfRule::MACRO_SR_PRED_INTRO: return "MACRO_SR_PRED_INTRO";
  34     case PfRule::MACRO_SR_PRED_ELIM: return "MACRO_SR_PRED_ELIM";
  35     case PfRule::MACRO_SR_PRED_TRANSFORM: return "MACRO_SR_PRED_TRANSFORM";
  36     case PfRule::REMOVE_TERM_FORMULA_AXIOM: return "REMOVE_TERM_FORMULA_AXIOM";
  37     //================================================= Trusted rules
  38     case PfRule::THEORY_LEMMA: return "THEORY_LEMMA";
  39     case PfRule::THEORY_REWRITE: return "THEORY_REWRITE";
  40     case PfRule::PREPROCESS: return "PREPROCESS";
  41     case PfRule::PREPROCESS_LEMMA: return "PREPROCESS_LEMMA";
  42     case PfRule::THEORY_PREPROCESS: return "THEORY_PREPROCESS";
  43     case PfRule::THEORY_PREPROCESS_LEMMA: return "THEORY_PREPROCESS_LEMMA";
  44     case PfRule::THEORY_EXPAND_DEF: return "THEORY_EXPAND_DEF";
  45     case PfRule::WITNESS_AXIOM: return "WITNESS_AXIOM";
  46     case PfRule::TRUST_REWRITE: return "TRUST_REWRITE";
  47     case PfRule::TRUST_SUBS: return "TRUST_SUBS";
  48     case PfRule::TRUST_SUBS_MAP: return "TRUST_SUBS_MAP";
  49     //================================================= Boolean rules
  50     case PfRule::RESOLUTION: return "RESOLUTION";
  51     case PfRule::CHAIN_RESOLUTION: return "CHAIN_RESOLUTION";
  52     case PfRule::FACTORING: return "FACTORING";
  53     case PfRule::REORDERING: return "REORDERING";
  54     case PfRule::MACRO_RESOLUTION: return "MACRO_RESOLUTION";
  55     case PfRule::SPLIT: return "SPLIT";
  56     case PfRule::EQ_RESOLVE: return "EQ_RESOLVE";
  57     case PfRule::MODUS_PONENS: return "MODUS_PONENS";
  58     case PfRule::NOT_NOT_ELIM: return "NOT_NOT_ELIM";
  59     case PfRule::CONTRA: return "CONTRA";
  60     case PfRule::AND_ELIM: return "AND_ELIM";
  61     case PfRule::AND_INTRO: return "AND_INTRO";
  62     case PfRule::NOT_OR_ELIM: return "NOT_OR_ELIM";
  63     case PfRule::IMPLIES_ELIM: return "IMPLIES_ELIM";
  64     case PfRule::NOT_IMPLIES_ELIM1: return "NOT_IMPLIES_ELIM1";
  65     case PfRule::NOT_IMPLIES_ELIM2: return "NOT_IMPLIES_ELIM2";
  66     case PfRule::EQUIV_ELIM1: return "EQUIV_ELIM1";
  67     case PfRule::EQUIV_ELIM2: return "EQUIV_ELIM2";
  68     case PfRule::NOT_EQUIV_ELIM1: return "NOT_EQUIV_ELIM1";
  69     case PfRule::NOT_EQUIV_ELIM2: return "NOT_EQUIV_ELIM2";
  70     case PfRule::XOR_ELIM1: return "XOR_ELIM1";
  71     case PfRule::XOR_ELIM2: return "XOR_ELIM2";
  72     case PfRule::NOT_XOR_ELIM1: return "NOT_XOR_ELIM1";
  73     case PfRule::NOT_XOR_ELIM2: return "NOT_XOR_ELIM2";
  74     case PfRule::ITE_ELIM1: return "ITE_ELIM1";
  75     case PfRule::ITE_ELIM2: return "ITE_ELIM2";
  76     case PfRule::NOT_ITE_ELIM1: return "NOT_ITE_ELIM1";
  77     case PfRule::NOT_ITE_ELIM2: return "NOT_ITE_ELIM2";
  78     //================================================= De Morgan rules
  79     case PfRule::NOT_AND: return "NOT_AND";
  80     //================================================= CNF rules
  81     case PfRule::CNF_AND_POS: return "CNF_AND_POS";
  82     case PfRule::CNF_AND_NEG: return "CNF_AND_NEG";
  83     case PfRule::CNF_OR_POS: return "CNF_OR_POS";
  84     case PfRule::CNF_OR_NEG: return "CNF_OR_NEG";
  85     case PfRule::CNF_IMPLIES_POS: return "CNF_IMPLIES_POS";
  86     case PfRule::CNF_IMPLIES_NEG1: return "CNF_IMPLIES_NEG1";
  87     case PfRule::CNF_IMPLIES_NEG2: return "CNF_IMPLIES_NEG2";
  88     case PfRule::CNF_EQUIV_POS1: return "CNF_EQUIV_POS1";
  89     case PfRule::CNF_EQUIV_POS2: return "CNF_EQUIV_POS2";
  90     case PfRule::CNF_EQUIV_NEG1: return "CNF_EQUIV_NEG1";
  91     case PfRule::CNF_EQUIV_NEG2: return "CNF_EQUIV_NEG2";
  92     case PfRule::CNF_XOR_POS1: return "CNF_XOR_POS1";
  93     case PfRule::CNF_XOR_POS2: return "CNF_XOR_POS2";
  94     case PfRule::CNF_XOR_NEG1: return "CNF_XOR_NEG1";
  95     case PfRule::CNF_XOR_NEG2: return "CNF_XOR_NEG2";
  96     case PfRule::CNF_ITE_POS1: return "CNF_ITE_POS1";
  97     case PfRule::CNF_ITE_POS2: return "CNF_ITE_POS2";
  98     case PfRule::CNF_ITE_POS3: return "CNF_ITE_POS3";
  99     case PfRule::CNF_ITE_NEG1: return "CNF_ITE_NEG1";
 100     case PfRule::CNF_ITE_NEG2: return "CNF_ITE_NEG2";
 101     case PfRule::CNF_ITE_NEG3: return "CNF_ITE_NEG3";
 102     //================================================= Equality rules
 103     case PfRule::REFL: return "REFL";
 104     case PfRule::SYMM: return "SYMM";
 105     case PfRule::TRANS: return "TRANS";
 106     case PfRule::CONG: return "CONG";
 107     case PfRule::TRUE_INTRO: return "TRUE_INTRO";
 108     case PfRule::TRUE_ELIM: return "TRUE_ELIM";
 109     case PfRule::FALSE_INTRO: return "FALSE_INTRO";
 110     case PfRule::FALSE_ELIM: return "FALSE_ELIM";
 111     case PfRule::HO_APP_ENCODE: return "HO_APP_ENCODE";
 112     case PfRule::HO_CONG: return "HO_CONG";
 113     //================================================= Array rules
 114     case PfRule::ARRAYS_READ_OVER_WRITE: return "ARRAYS_READ_OVER_WRITE";
 115     case PfRule::ARRAYS_READ_OVER_WRITE_CONTRA:
 116       return "ARRAYS_READ_OVER_WRITE_CONTRA";
 117     case PfRule::ARRAYS_READ_OVER_WRITE_1: return "ARRAYS_READ_OVER_WRITE_1";
 118     case PfRule::ARRAYS_EXT: return "ARRAYS_EXT";
 119     case PfRule::ARRAYS_TRUST: return "ARRAYS_TRUST";
 120     //================================================= Bit-Vector rules
 121     case PfRule::BV_BITBLAST: return "BV_BITBLAST";
 122     case PfRule::BV_BITBLAST_CONST: return "BV_BITBLAST_CONST";
 123     case PfRule::BV_BITBLAST_VAR: return "BV_BITBLAST_VAR";
 124     case PfRule::BV_BITBLAST_EQUAL: return "BV_BITBLAST_EQUAL";
 125     case PfRule::BV_BITBLAST_ULT: return "BV_BITBLAST_ULT";
 126     case PfRule::BV_BITBLAST_ULE: return "BV_BITBLAST_ULE";
 127     case PfRule::BV_BITBLAST_UGT: return "BV_BITBLAST_UGT";
 128     case PfRule::BV_BITBLAST_UGE: return "BV_BITBLAST_UGE";
 129     case PfRule::BV_BITBLAST_SLT: return "BV_BITBLAST_SLT";
 130     case PfRule::BV_BITBLAST_SLE: return "BV_BITBLAST_SLE";
 131     case PfRule::BV_BITBLAST_SGT: return "BV_BITBLAST_SGT";
 132     case PfRule::BV_BITBLAST_SGE: return "BV_BITBLAST_SGE";
 133     case PfRule::BV_BITBLAST_NOT: return "BV_BITBLAST_NOT";
 134     case PfRule::BV_BITBLAST_CONCAT: return "BV_BITBLAST_CONCAT";
 135     case PfRule::BV_BITBLAST_AND: return "BV_BITBLAST_AND";
 136     case PfRule::BV_BITBLAST_OR: return "BV_BITBLAST_OR";
 137     case PfRule::BV_BITBLAST_XOR: return "BV_BITBLAST_XOR";
 138     case PfRule::BV_BITBLAST_XNOR: return "BV_BITBLAST_XNOR";
 139     case PfRule::BV_BITBLAST_NAND: return "BV_BITBLAST_NAND";
 140     case PfRule::BV_BITBLAST_NOR: return "BV_BITBLAST_NOR";
 141     case PfRule::BV_BITBLAST_COMP: return "BV_BITBLAST_COMP";
 142     case PfRule::BV_BITBLAST_MULT: return "BV_BITBLAST_MULT";
 143     case PfRule::BV_BITBLAST_PLUS: return "BV_BITBLAST_PLUS";
 144     case PfRule::BV_BITBLAST_SUB: return "BV_BITBLAST_SUB";
 145     case PfRule::BV_BITBLAST_NEG: return "BV_BITBLAST_NEG";
 146     case PfRule::BV_BITBLAST_UDIV: return "BV_BITBLAST_UDIV";
 147     case PfRule::BV_BITBLAST_UREM: return "BV_BITBLAST_UREM";
 148     case PfRule::BV_BITBLAST_SDIV: return "BV_BITBLAST_SDIV";
 149     case PfRule::BV_BITBLAST_SREM: return "BV_BITBLAST_SREM";
 150     case PfRule::BV_BITBLAST_SMOD: return "BV_BITBLAST_SMOD";
 151     case PfRule::BV_BITBLAST_SHL: return "BV_BITBLAST_SHL";
 152     case PfRule::BV_BITBLAST_LSHR: return "BV_BITBLAST_LSHR";
 153     case PfRule::BV_BITBLAST_ASHR: return "BV_BITBLAST_ASHR";
 154     case PfRule::BV_BITBLAST_ULTBV: return "BV_BITBLAST_ULTBV";
 155     case PfRule::BV_BITBLAST_SLTBV: return "BV_BITBLAST_SLTBV";
 156     case PfRule::BV_BITBLAST_ITE: return "BV_BITBLAST_ITE";
 157     case PfRule::BV_BITBLAST_EXTRACT: return "BV_BITBLAST_EXTRACT";
 158     case PfRule::BV_BITBLAST_REPEAT: return "BV_BITBLAST_REPEAT";
 159     case PfRule::BV_BITBLAST_ZERO_EXTEND: return "BV_BITBLAST_ZERO_EXTEND";
 160     case PfRule::BV_BITBLAST_SIGN_EXTEND: return "BV_BITBLAST_SIGN_EXTEND";
 161     case PfRule::BV_BITBLAST_ROTATE_RIGHT: return "BV_BITBLAST_ROTATE_RIGHT";
 162     case PfRule::BV_BITBLAST_ROTATE_LEFT: return "BV_BITBLAST_ROTATE_LEFT";
 163     case PfRule::BV_EAGER_ATOM: return "BV_EAGER_ATOM";
 164     //================================================= Datatype rules
 165     case PfRule::DT_UNIF: return "DT_UNIF";
 166     case PfRule::DT_INST: return "DT_INST";
 167     case PfRule::DT_COLLAPSE: return "DT_COLLAPSE";
 168     case PfRule::DT_SPLIT: return "DT_SPLIT";
 169     case PfRule::DT_CLASH: return "DT_CLASH";
 170     case PfRule::DT_TRUST: return "DT_TRUST";
 171     //================================================= Quantifiers rules
 172     case PfRule::SKOLEM_INTRO: return "SKOLEM_INTRO";
 173     case PfRule::EXISTS_INTRO: return "EXISTS_INTRO";
 174     case PfRule::SKOLEMIZE: return "SKOLEMIZE";
 175     case PfRule::INSTANTIATE: return "INSTANTIATE";
 176     //================================================= String rules
 177     case PfRule::CONCAT_EQ: return "CONCAT_EQ";
 178     case PfRule::CONCAT_UNIFY: return "CONCAT_UNIFY";
 179     case PfRule::CONCAT_CONFLICT: return "CONCAT_CONFLICT";
 180     case PfRule::CONCAT_SPLIT: return "CONCAT_SPLIT";
 181     case PfRule::CONCAT_CSPLIT: return "CONCAT_CSPLIT";
 182     case PfRule::CONCAT_LPROP: return "CONCAT_LPROP";
 183     case PfRule::CONCAT_CPROP: return "CONCAT_CPROP";
 184     case PfRule::STRING_DECOMPOSE: return "STRING_DECOMPOSE";
 185     case PfRule::STRING_LENGTH_POS: return "STRING_LENGTH_POS";
 186     case PfRule::STRING_LENGTH_NON_EMPTY: return "STRING_LENGTH_NON_EMPTY";
 187     case PfRule::STRING_REDUCTION: return "STRING_REDUCTION";
 188     case PfRule::STRING_EAGER_REDUCTION: return "STRING_EAGER_REDUCTION";
 189     case PfRule::RE_INTER: return "RE_INTER";
 190     case PfRule::RE_UNFOLD_POS: return "RE_UNFOLD_POS";
 191     case PfRule::RE_UNFOLD_NEG: return "RE_UNFOLD_NEG";
 192     case PfRule::RE_UNFOLD_NEG_CONCAT_FIXED:
 193       return "RE_UNFOLD_NEG_CONCAT_FIXED";
 194     case PfRule::RE_ELIM: return "RE_ELIM";
 195     case PfRule::STRING_CODE_INJ: return "STRING_CODE_INJ";
 196     case PfRule::STRING_SEQ_UNIT_INJ: return "STRING_SEQ_UNIT_INJ";
 197     case PfRule::STRING_TRUST: return "STRING_TRUST";
 198     //================================================= Arith rules
 199     case PfRule::MACRO_ARITH_SCALE_SUM_UB:
 200       return "ARITH_SCALE_SUM_UPPER_BOUNDS";
 201     case PfRule::ARITH_SUM_UB: return "ARITH_SUM_UB";
 202     case PfRule::ARITH_TRICHOTOMY: return "ARITH_TRICHOTOMY";
 203     case PfRule::INT_TIGHT_LB: return "INT_TIGHT_LB";
 204     case PfRule::INT_TIGHT_UB: return "INT_TIGHT_UB";
 205     case PfRule::INT_TRUST: return "INT_TRUST";
 206     case PfRule::ARITH_MULT_SIGN: return "ARITH_MULT_SIGN";
 207     case PfRule::ARITH_MULT_POS: return "ARITH_MULT_POS";
 208     case PfRule::ARITH_MULT_NEG: return "ARITH_MULT_NEG";
 209     case PfRule::ARITH_MULT_TANGENT: return "ARITH_MULT_TANGENT";
 210     case PfRule::ARITH_OP_ELIM_AXIOM: return "ARITH_OP_ELIM_AXIOM";
 211     case PfRule::ARITH_TRANS_PI: return "ARITH_TRANS_PI";
 212     case PfRule::ARITH_TRANS_EXP_NEG: return "ARITH_TRANS_EXP_NEG";
 213     case PfRule::ARITH_TRANS_EXP_POSITIVITY:
 214       return "ARITH_TRANS_EXP_POSITIVITY";
 215     case PfRule::ARITH_TRANS_EXP_SUPER_LIN: return "ARITH_TRANS_EXP_SUPER_LIN";
 216     case PfRule::ARITH_TRANS_EXP_ZERO: return "ARITH_TRANS_EXP_ZERO";
 217     case PfRule::ARITH_TRANS_EXP_APPROX_ABOVE_NEG:
 218       return "ARITH_TRANS_EXP_APPROX_ABOVE_NEG";
 219     case PfRule::ARITH_TRANS_EXP_APPROX_ABOVE_POS:
 220       return "ARITH_TRANS_EXP_APPROX_ABOVE_POS";
 221     case PfRule::ARITH_TRANS_EXP_APPROX_BELOW:
 222       return "ARITH_TRANS_EXP_APPROX_BELOW";
 223     case PfRule::ARITH_TRANS_SINE_BOUNDS: return "ARITH_TRANS_SINE_BOUNDS";
 224     case PfRule::ARITH_TRANS_SINE_SHIFT: return "ARITH_TRANS_SINE_SHIFT";
 225     case PfRule::ARITH_TRANS_SINE_SYMMETRY: return "ARITH_TRANS_SINE_SYMMETRY";
 226     case PfRule::ARITH_TRANS_SINE_TANGENT_ZERO:
 227       return "ARITH_TRANS_SINE_TANGENT_ZERO";
 228     case PfRule::ARITH_TRANS_SINE_TANGENT_PI:
 229       return "ARITH_TRANS_SINE_TANGENT_PI";
 230     case PfRule::ARITH_TRANS_SINE_APPROX_ABOVE_NEG:
 231       return "ARITH_TRANS_SINE_APPROX_ABOVE_NEG";
 232     case PfRule::ARITH_TRANS_SINE_APPROX_ABOVE_POS:
 233       return "ARITH_TRANS_SINE_APPROX_ABOVE_POS";
 234     case PfRule::ARITH_TRANS_SINE_APPROX_BELOW_NEG:
 235       return "ARITH_TRANS_SINE_APPROX_BELOW_NEG";
 236     case PfRule::ARITH_TRANS_SINE_APPROX_BELOW_POS:
 237       return "ARITH_TRANS_SINE_APPROX_BELOW_POS";
 238     case PfRule::ARITH_NL_CAD_DIRECT: return "ARITH_NL_CAD_DIRECT";
 239     case PfRule::ARITH_NL_CAD_RECURSIVE: return "ARITH_NL_CAD_RECURSIVE";
 240     //================================================= Unknown rule
 241     case PfRule::UNKNOWN: return "UNKNOWN";
 242     default: return "?";
 243   }
 244 }
 245
 246 std::ostream& operator<<(std::ostream& out, PfRule id)
 247 {
 248   out << toString(id);
 249   return out;
 250 }
 251
 252 size_t PfRuleHashFunction::operator()(PfRule id) const
 253 {
 254   return static_cast<size_t>(id);
 255 }
 256
 257 }  // namespace cvc5