1 /******************************************************************************
2 * Top contributors (to current version):
3 * Andrew Reynolds, Haniel Barbosa, Gereon Kremer
5 * This file is part of the cvc5 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.
11 * ****************************************************************************
13 * Implementation of proof rule.
16 #include "proof/proof_rule.h"
22 const char* toString(PfRule id
)
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 case PfRule::TRUST_SUBS_EQ
: return "TRUST_SUBS_EQ";
50 case PfRule::THEORY_INFERENCE
: return "THEORY_INFERENCE";
51 //================================================= Boolean rules
52 case PfRule::RESOLUTION
: return "RESOLUTION";
53 case PfRule::CHAIN_RESOLUTION
: return "CHAIN_RESOLUTION";
54 case PfRule::FACTORING
: return "FACTORING";
55 case PfRule::REORDERING
: return "REORDERING";
56 case PfRule::MACRO_RESOLUTION
: return "MACRO_RESOLUTION";
57 case PfRule::MACRO_RESOLUTION_TRUST
: return "MACRO_RESOLUTION_TRUST";
58 case PfRule::SPLIT
: return "SPLIT";
59 case PfRule::EQ_RESOLVE
: return "EQ_RESOLVE";
60 case PfRule::MODUS_PONENS
: return "MODUS_PONENS";
61 case PfRule::NOT_NOT_ELIM
: return "NOT_NOT_ELIM";
62 case PfRule::CONTRA
: return "CONTRA";
63 case PfRule::AND_ELIM
: return "AND_ELIM";
64 case PfRule::AND_INTRO
: return "AND_INTRO";
65 case PfRule::NOT_OR_ELIM
: return "NOT_OR_ELIM";
66 case PfRule::IMPLIES_ELIM
: return "IMPLIES_ELIM";
67 case PfRule::NOT_IMPLIES_ELIM1
: return "NOT_IMPLIES_ELIM1";
68 case PfRule::NOT_IMPLIES_ELIM2
: return "NOT_IMPLIES_ELIM2";
69 case PfRule::EQUIV_ELIM1
: return "EQUIV_ELIM1";
70 case PfRule::EQUIV_ELIM2
: return "EQUIV_ELIM2";
71 case PfRule::NOT_EQUIV_ELIM1
: return "NOT_EQUIV_ELIM1";
72 case PfRule::NOT_EQUIV_ELIM2
: return "NOT_EQUIV_ELIM2";
73 case PfRule::XOR_ELIM1
: return "XOR_ELIM1";
74 case PfRule::XOR_ELIM2
: return "XOR_ELIM2";
75 case PfRule::NOT_XOR_ELIM1
: return "NOT_XOR_ELIM1";
76 case PfRule::NOT_XOR_ELIM2
: return "NOT_XOR_ELIM2";
77 case PfRule::ITE_ELIM1
: return "ITE_ELIM1";
78 case PfRule::ITE_ELIM2
: return "ITE_ELIM2";
79 case PfRule::NOT_ITE_ELIM1
: return "NOT_ITE_ELIM1";
80 case PfRule::NOT_ITE_ELIM2
: return "NOT_ITE_ELIM2";
81 //================================================= De Morgan rules
82 case PfRule::NOT_AND
: return "NOT_AND";
83 //================================================= CNF rules
84 case PfRule::CNF_AND_POS
: return "CNF_AND_POS";
85 case PfRule::CNF_AND_NEG
: return "CNF_AND_NEG";
86 case PfRule::CNF_OR_POS
: return "CNF_OR_POS";
87 case PfRule::CNF_OR_NEG
: return "CNF_OR_NEG";
88 case PfRule::CNF_IMPLIES_POS
: return "CNF_IMPLIES_POS";
89 case PfRule::CNF_IMPLIES_NEG1
: return "CNF_IMPLIES_NEG1";
90 case PfRule::CNF_IMPLIES_NEG2
: return "CNF_IMPLIES_NEG2";
91 case PfRule::CNF_EQUIV_POS1
: return "CNF_EQUIV_POS1";
92 case PfRule::CNF_EQUIV_POS2
: return "CNF_EQUIV_POS2";
93 case PfRule::CNF_EQUIV_NEG1
: return "CNF_EQUIV_NEG1";
94 case PfRule::CNF_EQUIV_NEG2
: return "CNF_EQUIV_NEG2";
95 case PfRule::CNF_XOR_POS1
: return "CNF_XOR_POS1";
96 case PfRule::CNF_XOR_POS2
: return "CNF_XOR_POS2";
97 case PfRule::CNF_XOR_NEG1
: return "CNF_XOR_NEG1";
98 case PfRule::CNF_XOR_NEG2
: return "CNF_XOR_NEG2";
99 case PfRule::CNF_ITE_POS1
: return "CNF_ITE_POS1";
100 case PfRule::CNF_ITE_POS2
: return "CNF_ITE_POS2";
101 case PfRule::CNF_ITE_POS3
: return "CNF_ITE_POS3";
102 case PfRule::CNF_ITE_NEG1
: return "CNF_ITE_NEG1";
103 case PfRule::CNF_ITE_NEG2
: return "CNF_ITE_NEG2";
104 case PfRule::CNF_ITE_NEG3
: return "CNF_ITE_NEG3";
105 //================================================= Equality rules
106 case PfRule::REFL
: return "REFL";
107 case PfRule::SYMM
: return "SYMM";
108 case PfRule::TRANS
: return "TRANS";
109 case PfRule::CONG
: return "CONG";
110 case PfRule::TRUE_INTRO
: return "TRUE_INTRO";
111 case PfRule::TRUE_ELIM
: return "TRUE_ELIM";
112 case PfRule::FALSE_INTRO
: return "FALSE_INTRO";
113 case PfRule::FALSE_ELIM
: return "FALSE_ELIM";
114 case PfRule::HO_APP_ENCODE
: return "HO_APP_ENCODE";
115 case PfRule::HO_CONG
: return "HO_CONG";
116 //================================================= Array rules
117 case PfRule::ARRAYS_READ_OVER_WRITE
: return "ARRAYS_READ_OVER_WRITE";
118 case PfRule::ARRAYS_READ_OVER_WRITE_CONTRA
:
119 return "ARRAYS_READ_OVER_WRITE_CONTRA";
120 case PfRule::ARRAYS_READ_OVER_WRITE_1
: return "ARRAYS_READ_OVER_WRITE_1";
121 case PfRule::ARRAYS_EXT
: return "ARRAYS_EXT";
122 case PfRule::ARRAYS_TRUST
: return "ARRAYS_TRUST";
123 //================================================= Bit-Vector rules
124 case PfRule::BV_BITBLAST
: return "BV_BITBLAST";
125 case PfRule::BV_BITBLAST_STEP
: return "BV_BITBLAST_STEP";
126 case PfRule::BV_EAGER_ATOM
: return "BV_EAGER_ATOM";
127 //================================================= Datatype rules
128 case PfRule::DT_UNIF
: return "DT_UNIF";
129 case PfRule::DT_INST
: return "DT_INST";
130 case PfRule::DT_COLLAPSE
: return "DT_COLLAPSE";
131 case PfRule::DT_SPLIT
: return "DT_SPLIT";
132 case PfRule::DT_CLASH
: return "DT_CLASH";
133 case PfRule::DT_TRUST
: return "DT_TRUST";
134 //================================================= Quantifiers rules
135 case PfRule::SKOLEM_INTRO
: return "SKOLEM_INTRO";
136 case PfRule::EXISTS_INTRO
: return "EXISTS_INTRO";
137 case PfRule::SKOLEMIZE
: return "SKOLEMIZE";
138 case PfRule::INSTANTIATE
: return "INSTANTIATE";
139 case PfRule::QUANTIFIERS_PREPROCESS
: return "QUANTIFIERS_PREPROCESS";
140 //================================================= String rules
141 case PfRule::CONCAT_EQ
: return "CONCAT_EQ";
142 case PfRule::CONCAT_UNIFY
: return "CONCAT_UNIFY";
143 case PfRule::CONCAT_CONFLICT
: return "CONCAT_CONFLICT";
144 case PfRule::CONCAT_SPLIT
: return "CONCAT_SPLIT";
145 case PfRule::CONCAT_CSPLIT
: return "CONCAT_CSPLIT";
146 case PfRule::CONCAT_LPROP
: return "CONCAT_LPROP";
147 case PfRule::CONCAT_CPROP
: return "CONCAT_CPROP";
148 case PfRule::STRING_DECOMPOSE
: return "STRING_DECOMPOSE";
149 case PfRule::STRING_LENGTH_POS
: return "STRING_LENGTH_POS";
150 case PfRule::STRING_LENGTH_NON_EMPTY
: return "STRING_LENGTH_NON_EMPTY";
151 case PfRule::STRING_REDUCTION
: return "STRING_REDUCTION";
152 case PfRule::STRING_EAGER_REDUCTION
: return "STRING_EAGER_REDUCTION";
153 case PfRule::RE_INTER
: return "RE_INTER";
154 case PfRule::RE_UNFOLD_POS
: return "RE_UNFOLD_POS";
155 case PfRule::RE_UNFOLD_NEG
: return "RE_UNFOLD_NEG";
156 case PfRule::RE_UNFOLD_NEG_CONCAT_FIXED
:
157 return "RE_UNFOLD_NEG_CONCAT_FIXED";
158 case PfRule::RE_ELIM
: return "RE_ELIM";
159 case PfRule::STRING_CODE_INJ
: return "STRING_CODE_INJ";
160 case PfRule::STRING_SEQ_UNIT_INJ
: return "STRING_SEQ_UNIT_INJ";
161 case PfRule::STRING_TRUST
: return "STRING_TRUST";
162 //================================================= Arith rules
163 case PfRule::MACRO_ARITH_SCALE_SUM_UB
:
164 return "ARITH_SCALE_SUM_UPPER_BOUNDS";
165 case PfRule::ARITH_SUM_UB
: return "ARITH_SUM_UB";
166 case PfRule::ARITH_TRICHOTOMY
: return "ARITH_TRICHOTOMY";
167 case PfRule::INT_TIGHT_LB
: return "INT_TIGHT_LB";
168 case PfRule::INT_TIGHT_UB
: return "INT_TIGHT_UB";
169 case PfRule::INT_TRUST
: return "INT_TRUST";
170 case PfRule::ARITH_MULT_SIGN
: return "ARITH_MULT_SIGN";
171 case PfRule::ARITH_MULT_POS
: return "ARITH_MULT_POS";
172 case PfRule::ARITH_MULT_NEG
: return "ARITH_MULT_NEG";
173 case PfRule::ARITH_MULT_TANGENT
: return "ARITH_MULT_TANGENT";
174 case PfRule::ARITH_OP_ELIM_AXIOM
: return "ARITH_OP_ELIM_AXIOM";
175 case PfRule::ARITH_TRANS_PI
: return "ARITH_TRANS_PI";
176 case PfRule::ARITH_TRANS_EXP_NEG
: return "ARITH_TRANS_EXP_NEG";
177 case PfRule::ARITH_TRANS_EXP_POSITIVITY
:
178 return "ARITH_TRANS_EXP_POSITIVITY";
179 case PfRule::ARITH_TRANS_EXP_SUPER_LIN
: return "ARITH_TRANS_EXP_SUPER_LIN";
180 case PfRule::ARITH_TRANS_EXP_ZERO
: return "ARITH_TRANS_EXP_ZERO";
181 case PfRule::ARITH_TRANS_EXP_APPROX_ABOVE_NEG
:
182 return "ARITH_TRANS_EXP_APPROX_ABOVE_NEG";
183 case PfRule::ARITH_TRANS_EXP_APPROX_ABOVE_POS
:
184 return "ARITH_TRANS_EXP_APPROX_ABOVE_POS";
185 case PfRule::ARITH_TRANS_EXP_APPROX_BELOW
:
186 return "ARITH_TRANS_EXP_APPROX_BELOW";
187 case PfRule::ARITH_TRANS_SINE_BOUNDS
: return "ARITH_TRANS_SINE_BOUNDS";
188 case PfRule::ARITH_TRANS_SINE_SHIFT
: return "ARITH_TRANS_SINE_SHIFT";
189 case PfRule::ARITH_TRANS_SINE_SYMMETRY
: return "ARITH_TRANS_SINE_SYMMETRY";
190 case PfRule::ARITH_TRANS_SINE_TANGENT_ZERO
:
191 return "ARITH_TRANS_SINE_TANGENT_ZERO";
192 case PfRule::ARITH_TRANS_SINE_TANGENT_PI
:
193 return "ARITH_TRANS_SINE_TANGENT_PI";
194 case PfRule::ARITH_TRANS_SINE_APPROX_ABOVE_NEG
:
195 return "ARITH_TRANS_SINE_APPROX_ABOVE_NEG";
196 case PfRule::ARITH_TRANS_SINE_APPROX_ABOVE_POS
:
197 return "ARITH_TRANS_SINE_APPROX_ABOVE_POS";
198 case PfRule::ARITH_TRANS_SINE_APPROX_BELOW_NEG
:
199 return "ARITH_TRANS_SINE_APPROX_BELOW_NEG";
200 case PfRule::ARITH_TRANS_SINE_APPROX_BELOW_POS
:
201 return "ARITH_TRANS_SINE_APPROX_BELOW_POS";
202 case PfRule::ARITH_NL_CAD_DIRECT
: return "ARITH_NL_CAD_DIRECT";
203 case PfRule::ARITH_NL_CAD_RECURSIVE
: return "ARITH_NL_CAD_RECURSIVE";
204 //================================================= External rules
205 case PfRule::LFSC_RULE
: return "LFSC_RULE";
206 //================================================= Unknown rule
207 case PfRule::UNKNOWN
: return "UNKNOWN";
212 std::ostream
& operator<<(std::ostream
& out
, PfRule id
)
218 size_t PfRuleHashFunction::operator()(PfRule id
) const
220 return static_cast<size_t>(id
);