src/expr/proof_rule.cpp

   1 /*********************                                                        */
   2 /*! \file proof_rule.cpp
   3  ** \verbatim
   4  ** Top contributors (to current version):
   5  **   Haniel Barbosa, Andrew Reynolds
   6  ** This file is part of the CVC4 project.
   7  ** Copyright (c) 2009-2020 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.\endverbatim
  11  **
  12  ** \brief Implementation of proof rule
  13  **/
  14
  15 #include "expr/proof_rule.h"
  16
  17 #include <iostream>
  18
  19 namespace CVC4 {
  20
  21 const char* toString(PfRule id)
  22 {
  23   switch (id)
  24   {
  25     //================================================= Core rules
  26     case PfRule::ASSUME: return "ASSUME";
  27     case PfRule::SCOPE: return "SCOPE";
  28     case PfRule::SUBS: return "SUBS";
  29     case PfRule::REWRITE: return "REWRITE";
  30     case PfRule::MACRO_SR_EQ_INTRO: return "MACRO_SR_EQ_INTRO";
  31     case PfRule::MACRO_SR_PRED_INTRO: return "MACRO_SR_PRED_INTRO";
  32     case PfRule::MACRO_SR_PRED_ELIM: return "MACRO_SR_PRED_ELIM";
  33     case PfRule::MACRO_SR_PRED_TRANSFORM: return "MACRO_SR_PRED_TRANSFORM";
  34     case PfRule::THEORY_REWRITE: return "THEORY_REWRITE";
  35     case PfRule::REMOVE_TERM_FORMULA_AXIOM: return "REMOVE_TERM_FORMULA_AXIOM";
  36     //================================================= Trusted rules
  37     case PfRule::PREPROCESS: return "PREPROCESS";
  38     case PfRule::PREPROCESS_LEMMA: return "PREPROCESS_LEMMA";
  39     case PfRule::THEORY_PREPROCESS: return "THEORY_PREPROCESS";
  40     case PfRule::THEORY_PREPROCESS_LEMMA: return "THEORY_PREPROCESS_LEMMA";
  41     case PfRule::WITNESS_AXIOM: return "WITNESS_AXIOM";
  42     //================================================= Boolean rules
  43     case PfRule::SPLIT: return "SPLIT";
  44     case PfRule::EQ_RESOLVE: return "EQ_RESOLVE";
  45     case PfRule::AND_ELIM: return "AND_ELIM";
  46     case PfRule::AND_INTRO: return "AND_INTRO";
  47     case PfRule::NOT_OR_ELIM: return "NOT_OR_ELIM";
  48     case PfRule::IMPLIES_ELIM: return "IMPLIES_ELIM";
  49     case PfRule::NOT_IMPLIES_ELIM1: return "NOT_IMPLIES_ELIM1";
  50     case PfRule::NOT_IMPLIES_ELIM2: return "NOT_IMPLIES_ELIM2";
  51     case PfRule::EQUIV_ELIM1: return "EQUIV_ELIM1";
  52     case PfRule::EQUIV_ELIM2: return "EQUIV_ELIM2";
  53     case PfRule::NOT_EQUIV_ELIM1: return "NOT_EQUIV_ELIM1";
  54     case PfRule::NOT_EQUIV_ELIM2: return "NOT_EQUIV_ELIM2";
  55     case PfRule::XOR_ELIM1: return "XOR_ELIM1";
  56     case PfRule::XOR_ELIM2: return "XOR_ELIM2";
  57     case PfRule::NOT_XOR_ELIM1: return "NOT_XOR_ELIM1";
  58     case PfRule::NOT_XOR_ELIM2: return "NOT_XOR_ELIM2";
  59     case PfRule::ITE_ELIM1: return "ITE_ELIM1";
  60     case PfRule::ITE_ELIM2: return "ITE_ELIM2";
  61     case PfRule::NOT_ITE_ELIM1: return "NOT_ITE_ELIM1";
  62     case PfRule::NOT_ITE_ELIM2: return "NOT_ITE_ELIM2";
  63     case PfRule::CONTRA: return "CONTRA";
  64     //================================================= De Morgan rules
  65     case PfRule::NOT_AND: return "NOT_AND";
  66     //================================================= CNF rules
  67     case PfRule::CNF_AND_POS: return "CNF_AND_POS";
  68     case PfRule::CNF_AND_NEG: return "CNF_AND_NEG";
  69     case PfRule::CNF_OR_POS: return "CNF_OR_POS";
  70     case PfRule::CNF_OR_NEG: return "CNF_OR_NEG";
  71     case PfRule::CNF_IMPLIES_POS: return "CNF_IMPLIES_POS";
  72     case PfRule::CNF_IMPLIES_NEG1: return "CNF_IMPLIES_NEG1";
  73     case PfRule::CNF_IMPLIES_NEG2: return "CNF_IMPLIES_NEG2";
  74     case PfRule::CNF_EQUIV_POS1: return "CNF_EQUIV_POS1";
  75     case PfRule::CNF_EQUIV_POS2: return "CNF_EQUIV_POS2";
  76     case PfRule::CNF_EQUIV_NEG1: return "CNF_EQUIV_NEG1";
  77     case PfRule::CNF_EQUIV_NEG2: return "CNF_EQUIV_NEG2";
  78     case PfRule::CNF_XOR_POS1: return "CNF_XOR_POS1";
  79     case PfRule::CNF_XOR_POS2: return "CNF_XOR_POS2";
  80     case PfRule::CNF_XOR_NEG1: return "CNF_XOR_NEG1";
  81     case PfRule::CNF_XOR_NEG2: return "CNF_XOR_NEG2";
  82     case PfRule::CNF_ITE_POS1: return "CNF_ITE_POS1";
  83     case PfRule::CNF_ITE_POS2: return "CNF_ITE_POS2";
  84     case PfRule::CNF_ITE_POS3: return "CNF_ITE_POS3";
  85     case PfRule::CNF_ITE_NEG1: return "CNF_ITE_NEG1";
  86     case PfRule::CNF_ITE_NEG2: return "CNF_ITE_NEG2";
  87     case PfRule::CNF_ITE_NEG3: return "CNF_ITE_NEG3";
  88     //================================================= Equality rules
  89     case PfRule::REFL: return "REFL";
  90     case PfRule::SYMM: return "SYMM";
  91     case PfRule::TRANS: return "TRANS";
  92     case PfRule::CONG: return "CONG";
  93     case PfRule::TRUE_INTRO: return "TRUE_INTRO";
  94     case PfRule::TRUE_ELIM: return "TRUE_ELIM";
  95     case PfRule::FALSE_INTRO: return "FALSE_INTRO";
  96     case PfRule::FALSE_ELIM: return "FALSE_ELIM";
  97     case PfRule::HO_APP_ENCODE: return "HO_APP_ENCODE";
  98     case PfRule::HO_CONG: return "HO_CONG";
  99     //================================================= Quantifiers rules
 100     case PfRule::WITNESS_INTRO: return "WITNESS_INTRO";
 101     case PfRule::EXISTS_INTRO: return "EXISTS_INTRO";
 102     case PfRule::SKOLEMIZE: return "SKOLEMIZE";
 103     case PfRule::INSTANTIATE: return "INSTANTIATE";
 104     //================================================= String rules
 105     case PfRule::CONCAT_EQ: return "CONCAT_EQ";
 106     case PfRule::CONCAT_UNIFY: return "CONCAT_UNIFY";
 107     case PfRule::CONCAT_CONFLICT: return "CONCAT_CONFLICT";
 108     case PfRule::CONCAT_SPLIT: return "CONCAT_SPLIT";
 109     case PfRule::CONCAT_CSPLIT: return "CONCAT_CSPLIT";
 110     case PfRule::CONCAT_LPROP: return "CONCAT_LPROP";
 111     case PfRule::CONCAT_CPROP: return "CONCAT_CPROP";
 112     case PfRule::STRING_DECOMPOSE: return "STRING_DECOMPOSE";
 113     case PfRule::STRING_LENGTH_POS: return "STRING_LENGTH_POS";
 114     case PfRule::STRING_LENGTH_NON_EMPTY: return "STRING_LENGTH_NON_EMPTY";
 115     case PfRule::STRING_REDUCTION: return "STRING_REDUCTION";
 116     case PfRule::STRING_EAGER_REDUCTION: return "STRING_EAGER_REDUCTION";
 117     case PfRule::RE_INTER: return "RE_INTER";
 118     case PfRule::RE_UNFOLD_POS: return "RE_UNFOLD_POS";
 119     case PfRule::RE_UNFOLD_NEG: return "RE_UNFOLD_NEG";
 120     case PfRule::RE_UNFOLD_NEG_CONCAT_FIXED:
 121       return "RE_UNFOLD_NEG_CONCAT_FIXED";
 122     case PfRule::RE_ELIM: return "RE_ELIM";
 123     case PfRule::STRING_CODE_INJ: return "STRING_CODE_INJ";
 124     case PfRule::STRING_SEQ_UNIT_INJ: return "STRING_SEQ_UNIT_INJ";
 125     case PfRule::STRING_TRUST: return "STRING_TRUST";
 126     //================================================= Arith rules
 127     case PfRule::ARITH_SCALE_SUM_UPPER_BOUNDS: return "ARITH_SCALE_SUM_UPPER_BOUNDS";
 128     case PfRule::ARITH_TRICHOTOMY: return "ARITH_TRICHOTOMY";
 129     case PfRule::INT_TIGHT_LB: return "INT_TIGHT_LB";
 130     case PfRule::INT_TIGHT_UB: return "INT_TIGHT_UB";
 131     case PfRule::INT_TRUST: return "INT_TRUST";
 132     case PfRule::ARITH_OP_ELIM_AXIOM: return "ARITH_OP_ELIM_AXIOM";
 133     //================================================= Unknown rule
 134     case PfRule::UNKNOWN: return "UNKNOWN";
 135     default: return "?";
 136   }
 137 }
 138
 139 std::ostream& operator<<(std::ostream& out, PfRule id)
 140 {
 141   out << toString(id);
 142   return out;
 143 }
 144
 145 size_t PfRuleHashFunction::operator()(PfRule id) const
 146 {
 147   return static_cast<size_t>(id);
 148 }
 149
 150 }  // namespace CVC4