GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/expr/proof_rule.cpp Lines: 22 169 13.0 %
Date: 2021-03-23 Branches: 16 153 10.5 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file proof_rule.cpp
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Andrew Reynolds, Haniel Barbosa, Gereon Kremer
6
 ** This file is part of the CVC4 project.
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.\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
142137
const char* toString(PfRule id)
22
{
23
142137
  switch (id)
24
  {
25
    //================================================= Core rules
26
31368
    case PfRule::ASSUME: return "ASSUME";
27
31368
    case PfRule::SCOPE: return "SCOPE";
28
    case PfRule::SUBS: return "SUBS";
29
    case PfRule::REWRITE: return "REWRITE";
30
    case PfRule::EVALUATE: return "EVALUATE";
31
    case PfRule::MACRO_SR_EQ_INTRO: return "MACRO_SR_EQ_INTRO";
32
    case PfRule::MACRO_SR_PRED_INTRO: return "MACRO_SR_PRED_INTRO";
33
    case PfRule::MACRO_SR_PRED_ELIM: return "MACRO_SR_PRED_ELIM";
34
31366
    case PfRule::MACRO_SR_PRED_TRANSFORM: return "MACRO_SR_PRED_TRANSFORM";
35
    case PfRule::REMOVE_TERM_FORMULA_AXIOM: return "REMOVE_TERM_FORMULA_AXIOM";
36
    //================================================= Trusted rules
37
    case PfRule::THEORY_LEMMA: return "THEORY_LEMMA";
38
    case PfRule::THEORY_REWRITE: return "THEORY_REWRITE";
39
    case PfRule::PREPROCESS: return "PREPROCESS";
40
    case PfRule::PREPROCESS_LEMMA: return "PREPROCESS_LEMMA";
41
    case PfRule::THEORY_PREPROCESS: return "THEORY_PREPROCESS";
42
    case PfRule::THEORY_PREPROCESS_LEMMA: return "THEORY_PREPROCESS_LEMMA";
43
    case PfRule::THEORY_EXPAND_DEF: return "THEORY_EXPAND_DEF";
44
    case PfRule::WITNESS_AXIOM: return "WITNESS_AXIOM";
45
    case PfRule::TRUST_REWRITE: return "TRUST_REWRITE";
46
    case PfRule::TRUST_SUBS: return "TRUST_SUBS";
47
    case PfRule::TRUST_SUBS_MAP: return "TRUST_SUBS_MAP";
48
    //================================================= Boolean rules
49
    case PfRule::RESOLUTION: return "RESOLUTION";
50
    case PfRule::CHAIN_RESOLUTION: return "CHAIN_RESOLUTION";
51
    case PfRule::FACTORING: return "FACTORING";
52
    case PfRule::REORDERING: return "REORDERING";
53
    case PfRule::MACRO_RESOLUTION: return "MACRO_RESOLUTION";
54
    case PfRule::SPLIT: return "SPLIT";
55
    case PfRule::EQ_RESOLVE: return "EQ_RESOLVE";
56
    case PfRule::MODUS_PONENS: return "MODUS_PONENS";
57
    case PfRule::NOT_NOT_ELIM: return "NOT_NOT_ELIM";
58
    case PfRule::CONTRA: return "CONTRA";
59
    case PfRule::AND_ELIM: return "AND_ELIM";
60
    case PfRule::AND_INTRO: return "AND_INTRO";
61
    case PfRule::NOT_OR_ELIM: return "NOT_OR_ELIM";
62
    case PfRule::IMPLIES_ELIM: return "IMPLIES_ELIM";
63
    case PfRule::NOT_IMPLIES_ELIM1: return "NOT_IMPLIES_ELIM1";
64
    case PfRule::NOT_IMPLIES_ELIM2: return "NOT_IMPLIES_ELIM2";
65
    case PfRule::EQUIV_ELIM1: return "EQUIV_ELIM1";
66
    case PfRule::EQUIV_ELIM2: return "EQUIV_ELIM2";
67
    case PfRule::NOT_EQUIV_ELIM1: return "NOT_EQUIV_ELIM1";
68
    case PfRule::NOT_EQUIV_ELIM2: return "NOT_EQUIV_ELIM2";
69
    case PfRule::XOR_ELIM1: return "XOR_ELIM1";
70
    case PfRule::XOR_ELIM2: return "XOR_ELIM2";
71
    case PfRule::NOT_XOR_ELIM1: return "NOT_XOR_ELIM1";
72
    case PfRule::NOT_XOR_ELIM2: return "NOT_XOR_ELIM2";
73
    case PfRule::ITE_ELIM1: return "ITE_ELIM1";
74
    case PfRule::ITE_ELIM2: return "ITE_ELIM2";
75
    case PfRule::NOT_ITE_ELIM1: return "NOT_ITE_ELIM1";
76
    case PfRule::NOT_ITE_ELIM2: return "NOT_ITE_ELIM2";
77
    //================================================= De Morgan rules
78
    case PfRule::NOT_AND: return "NOT_AND";
79
    //================================================= CNF rules
80
    case PfRule::CNF_AND_POS: return "CNF_AND_POS";
81
    case PfRule::CNF_AND_NEG: return "CNF_AND_NEG";
82
    case PfRule::CNF_OR_POS: return "CNF_OR_POS";
83
    case PfRule::CNF_OR_NEG: return "CNF_OR_NEG";
84
    case PfRule::CNF_IMPLIES_POS: return "CNF_IMPLIES_POS";
85
    case PfRule::CNF_IMPLIES_NEG1: return "CNF_IMPLIES_NEG1";
86
    case PfRule::CNF_IMPLIES_NEG2: return "CNF_IMPLIES_NEG2";
87
    case PfRule::CNF_EQUIV_POS1: return "CNF_EQUIV_POS1";
88
    case PfRule::CNF_EQUIV_POS2: return "CNF_EQUIV_POS2";
89
    case PfRule::CNF_EQUIV_NEG1: return "CNF_EQUIV_NEG1";
90
    case PfRule::CNF_EQUIV_NEG2: return "CNF_EQUIV_NEG2";
91
    case PfRule::CNF_XOR_POS1: return "CNF_XOR_POS1";
92
    case PfRule::CNF_XOR_POS2: return "CNF_XOR_POS2";
93
    case PfRule::CNF_XOR_NEG1: return "CNF_XOR_NEG1";
94
    case PfRule::CNF_XOR_NEG2: return "CNF_XOR_NEG2";
95
    case PfRule::CNF_ITE_POS1: return "CNF_ITE_POS1";
96
    case PfRule::CNF_ITE_POS2: return "CNF_ITE_POS2";
97
    case PfRule::CNF_ITE_POS3: return "CNF_ITE_POS3";
98
    case PfRule::CNF_ITE_NEG1: return "CNF_ITE_NEG1";
99
    case PfRule::CNF_ITE_NEG2: return "CNF_ITE_NEG2";
100
    case PfRule::CNF_ITE_NEG3: return "CNF_ITE_NEG3";
101
    //================================================= Equality rules
102
2
    case PfRule::REFL: return "REFL";
103
3
    case PfRule::SYMM: return "SYMM";
104
3
    case PfRule::TRANS: return "TRANS";
105
3
    case PfRule::CONG: return "CONG";
106
3
    case PfRule::TRUE_INTRO: return "TRUE_INTRO";
107
    case PfRule::TRUE_ELIM: return "TRUE_ELIM";
108
3
    case PfRule::FALSE_INTRO: return "FALSE_INTRO";
109
3
    case PfRule::FALSE_ELIM: return "FALSE_ELIM";
110
    case PfRule::HO_APP_ENCODE: return "HO_APP_ENCODE";
111
    case PfRule::HO_CONG: return "HO_CONG";
112
    //================================================= Array rules
113
    case PfRule::ARRAYS_READ_OVER_WRITE: return "ARRAYS_READ_OVER_WRITE";
114
    case PfRule::ARRAYS_READ_OVER_WRITE_CONTRA:
115
      return "ARRAYS_READ_OVER_WRITE_CONTRA";
116
    case PfRule::ARRAYS_READ_OVER_WRITE_1: return "ARRAYS_READ_OVER_WRITE_1";
117
    case PfRule::ARRAYS_EXT: return "ARRAYS_EXT";
118
    case PfRule::ARRAYS_TRUST: return "ARRAYS_TRUST";
119
    //================================================= Bit-Vector rules
120
    case PfRule::BV_BITBLAST: return "BV_BITBLAST";
121
    case PfRule::BV_EAGER_ATOM: return "BV_EAGER_ATOM";
122
    //================================================= Datatype rules
123
    case PfRule::DT_UNIF: return "DT_UNIF";
124
    case PfRule::DT_INST: return "DT_INST";
125
    case PfRule::DT_COLLAPSE: return "DT_COLLAPSE";
126
    case PfRule::DT_SPLIT: return "DT_SPLIT";
127
    case PfRule::DT_CLASH: return "DT_CLASH";
128
    case PfRule::DT_TRUST: return "DT_TRUST";
129
    //================================================= Quantifiers rules
130
    case PfRule::SKOLEM_INTRO: return "SKOLEM_INTRO";
131
    case PfRule::EXISTS_INTRO: return "EXISTS_INTRO";
132
    case PfRule::SKOLEMIZE: return "SKOLEMIZE";
133
    case PfRule::INSTANTIATE: return "INSTANTIATE";
134
    //================================================= String rules
135
    case PfRule::CONCAT_EQ: return "CONCAT_EQ";
136
    case PfRule::CONCAT_UNIFY: return "CONCAT_UNIFY";
137
    case PfRule::CONCAT_CONFLICT: return "CONCAT_CONFLICT";
138
    case PfRule::CONCAT_SPLIT: return "CONCAT_SPLIT";
139
    case PfRule::CONCAT_CSPLIT: return "CONCAT_CSPLIT";
140
    case PfRule::CONCAT_LPROP: return "CONCAT_LPROP";
141
    case PfRule::CONCAT_CPROP: return "CONCAT_CPROP";
142
    case PfRule::STRING_DECOMPOSE: return "STRING_DECOMPOSE";
143
    case PfRule::STRING_LENGTH_POS: return "STRING_LENGTH_POS";
144
    case PfRule::STRING_LENGTH_NON_EMPTY: return "STRING_LENGTH_NON_EMPTY";
145
    case PfRule::STRING_REDUCTION: return "STRING_REDUCTION";
146
    case PfRule::STRING_EAGER_REDUCTION: return "STRING_EAGER_REDUCTION";
147
    case PfRule::RE_INTER: return "RE_INTER";
148
    case PfRule::RE_UNFOLD_POS: return "RE_UNFOLD_POS";
149
    case PfRule::RE_UNFOLD_NEG: return "RE_UNFOLD_NEG";
150
    case PfRule::RE_UNFOLD_NEG_CONCAT_FIXED:
151
      return "RE_UNFOLD_NEG_CONCAT_FIXED";
152
    case PfRule::RE_ELIM: return "RE_ELIM";
153
    case PfRule::STRING_CODE_INJ: return "STRING_CODE_INJ";
154
    case PfRule::STRING_SEQ_UNIT_INJ: return "STRING_SEQ_UNIT_INJ";
155
    case PfRule::STRING_TRUST: return "STRING_TRUST";
156
    //================================================= Arith rules
157
31366
    case PfRule::ARITH_SCALE_SUM_UPPER_BOUNDS: return "ARITH_SCALE_SUM_UPPER_BOUNDS";
158
1444
    case PfRule::ARITH_TRICHOTOMY: return "ARITH_TRICHOTOMY";
159
239
    case PfRule::INT_TIGHT_LB: return "INT_TIGHT_LB";
160
14966
    case PfRule::INT_TIGHT_UB: return "INT_TIGHT_UB";
161
    case PfRule::INT_TRUST: return "INT_TRUST";
162
    case PfRule::ARITH_MULT_SIGN: return "ARITH_MULT_SIGN";
163
    case PfRule::ARITH_MULT_POS: return "ARITH_MULT_POS";
164
    case PfRule::ARITH_MULT_NEG: return "ARITH_MULT_NEG";
165
    case PfRule::ARITH_MULT_TANGENT: return "ARITH_MULT_TANGENT";
166
    case PfRule::ARITH_OP_ELIM_AXIOM: return "ARITH_OP_ELIM_AXIOM";
167
    case PfRule::ARITH_TRANS_PI: return "ARITH_TRANS_PI";
168
    case PfRule::ARITH_TRANS_EXP_NEG: return "ARITH_TRANS_EXP_NEG";
169
    case PfRule::ARITH_TRANS_EXP_POSITIVITY:
170
      return "ARITH_TRANS_EXP_POSITIVITY";
171
    case PfRule::ARITH_TRANS_EXP_SUPER_LIN: return "ARITH_TRANS_EXP_SUPER_LIN";
172
    case PfRule::ARITH_TRANS_EXP_ZERO: return "ARITH_TRANS_EXP_ZERO";
173
    case PfRule::ARITH_TRANS_EXP_APPROX_ABOVE_NEG:
174
      return "ARITH_TRANS_EXP_APPROX_ABOVE_NEG";
175
    case PfRule::ARITH_TRANS_EXP_APPROX_ABOVE_POS:
176
      return "ARITH_TRANS_EXP_APPROX_ABOVE_POS";
177
    case PfRule::ARITH_TRANS_EXP_APPROX_BELOW:
178
      return "ARITH_TRANS_EXP_APPROX_BELOW";
179
    case PfRule::ARITH_TRANS_SINE_BOUNDS: return "ARITH_TRANS_SINE_BOUNDS";
180
    case PfRule::ARITH_TRANS_SINE_SHIFT: return "ARITH_TRANS_SINE_SHIFT";
181
    case PfRule::ARITH_TRANS_SINE_SYMMETRY: return "ARITH_TRANS_SINE_SYMMETRY";
182
    case PfRule::ARITH_TRANS_SINE_TANGENT_ZERO:
183
      return "ARITH_TRANS_SINE_TANGENT_ZERO";
184
    case PfRule::ARITH_TRANS_SINE_TANGENT_PI:
185
      return "ARITH_TRANS_SINE_TANGENT_PI";
186
    case PfRule::ARITH_TRANS_SINE_APPROX_ABOVE_NEG:
187
      return "ARITH_TRANS_SINE_APPROX_ABOVE_NEG";
188
    case PfRule::ARITH_TRANS_SINE_APPROX_ABOVE_POS:
189
      return "ARITH_TRANS_SINE_APPROX_ABOVE_POS";
190
    case PfRule::ARITH_TRANS_SINE_APPROX_BELOW_NEG:
191
      return "ARITH_TRANS_SINE_APPROX_BELOW_NEG";
192
    case PfRule::ARITH_TRANS_SINE_APPROX_BELOW_POS:
193
      return "ARITH_TRANS_SINE_APPROX_BELOW_POS";
194
    case PfRule::ARITH_NL_CAD_DIRECT: return "ARITH_NL_CAD_DIRECT";
195
    case PfRule::ARITH_NL_CAD_RECURSIVE: return "ARITH_NL_CAD_RECURSIVE";
196
    //================================================= Unknown rule
197
    case PfRule::UNKNOWN: return "UNKNOWN";
198
    default: return "?";
199
  }
200
}
201
202
142133
std::ostream& operator<<(std::ostream& out, PfRule id)
203
{
204
142133
  out << toString(id);
205
142133
  return out;
206
}
207
208
2035507
size_t PfRuleHashFunction::operator()(PfRule id) const
209
{
210
2035507
  return static_cast<size_t>(id);
211
}
212
213
26685
}  // namespace CVC4