1 /********************* */
2 /*! \file proof_rule.cpp
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
12 ** \brief Implementation of proof rule
15 #include "expr/proof_rule.h"
21 const char* toString(PfRule id
)
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 //================================================= Boolean rules
35 case PfRule::SPLIT
: return "SPLIT";
36 case PfRule::AND_ELIM
: return "AND_ELIM";
37 case PfRule::AND_INTRO
: return "AND_INTRO";
38 case PfRule::NOT_OR_ELIM
: return "NOT_OR_ELIM";
39 case PfRule::IMPLIES_ELIM
: return "IMPLIES_ELIM";
40 case PfRule::NOT_IMPLIES_ELIM1
: return "NOT_IMPLIES_ELIM1";
41 case PfRule::NOT_IMPLIES_ELIM2
: return "NOT_IMPLIES_ELIM2";
42 case PfRule::EQUIV_ELIM1
: return "EQUIV_ELIM1";
43 case PfRule::EQUIV_ELIM2
: return "EQUIV_ELIM2";
44 case PfRule::NOT_EQUIV_ELIM1
: return "NOT_EQUIV_ELIM1";
45 case PfRule::NOT_EQUIV_ELIM2
: return "NOT_EQUIV_ELIM2";
46 case PfRule::XOR_ELIM1
: return "XOR_ELIM1";
47 case PfRule::XOR_ELIM2
: return "XOR_ELIM2";
48 case PfRule::NOT_XOR_ELIM1
: return "NOT_XOR_ELIM1";
49 case PfRule::NOT_XOR_ELIM2
: return "NOT_XOR_ELIM2";
50 case PfRule::ITE_ELIM1
: return "ITE_ELIM1";
51 case PfRule::ITE_ELIM2
: return "ITE_ELIM2";
52 case PfRule::NOT_ITE_ELIM1
: return "NOT_ITE_ELIM1";
53 case PfRule::NOT_ITE_ELIM2
: return "NOT_ITE_ELIM2";
54 case PfRule::CONTRA
: return "CONTRA";
55 //================================================= De Morgan rules
56 case PfRule::NOT_AND
: return "NOT_AND";
57 //================================================= CNF rules
58 case PfRule::CNF_AND_POS
: return "CNF_AND_POS";
59 case PfRule::CNF_AND_NEG
: return "CNF_AND_NEG";
60 case PfRule::CNF_OR_POS
: return "CNF_OR_POS";
61 case PfRule::CNF_OR_NEG
: return "CNF_OR_NEG";
62 case PfRule::CNF_IMPLIES_POS
: return "CNF_IMPLIES_POS";
63 case PfRule::CNF_IMPLIES_NEG1
: return "CNF_IMPLIES_NEG1";
64 case PfRule::CNF_IMPLIES_NEG2
: return "CNF_IMPLIES_NEG2";
65 case PfRule::CNF_EQUIV_POS1
: return "CNF_EQUIV_POS1";
66 case PfRule::CNF_EQUIV_POS2
: return "CNF_EQUIV_POS2";
67 case PfRule::CNF_EQUIV_NEG1
: return "CNF_EQUIV_NEG1";
68 case PfRule::CNF_EQUIV_NEG2
: return "CNF_EQUIV_NEG2";
69 case PfRule::CNF_XOR_POS1
: return "CNF_XOR_POS1";
70 case PfRule::CNF_XOR_POS2
: return "CNF_XOR_POS2";
71 case PfRule::CNF_XOR_NEG1
: return "CNF_XOR_NEG1";
72 case PfRule::CNF_XOR_NEG2
: return "CNF_XOR_NEG2";
73 case PfRule::CNF_ITE_POS1
: return "CNF_ITE_POS1";
74 case PfRule::CNF_ITE_POS2
: return "CNF_ITE_POS2";
75 case PfRule::CNF_ITE_POS3
: return "CNF_ITE_POS3";
76 case PfRule::CNF_ITE_NEG1
: return "CNF_ITE_NEG1";
77 case PfRule::CNF_ITE_NEG2
: return "CNF_ITE_NEG2";
78 case PfRule::CNF_ITE_NEG3
: return "CNF_ITE_NEG3";
79 //================================================= Equality rules
80 case PfRule::REFL
: return "REFL";
81 case PfRule::SYMM
: return "SYMM";
82 case PfRule::TRANS
: return "TRANS";
83 case PfRule::CONG
: return "CONG";
84 case PfRule::TRUE_INTRO
: return "TRUE_INTRO";
85 case PfRule::TRUE_ELIM
: return "TRUE_ELIM";
86 case PfRule::FALSE_INTRO
: return "FALSE_INTRO";
87 case PfRule::FALSE_ELIM
: return "FALSE_ELIM";
88 //================================================= Quantifiers rules
89 case PfRule::WITNESS_INTRO
: return "WITNESS_INTRO";
90 case PfRule::EXISTS_INTRO
: return "EXISTS_INTRO";
91 case PfRule::SKOLEMIZE
: return "SKOLEMIZE";
92 case PfRule::INSTANTIATE
: return "INSTANTIATE";
93 //================================================= Unknown rule
94 case PfRule::UNKNOWN
: return "UNKNOWN";
99 std::ostream
& operator<<(std::ostream
& out
, PfRule id
)