blob: 339b4f582554f2e05b05d826a947f1e840d164aa (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
|
/********************* */
/*! \file proof_rule.cpp
** \verbatim
** Top contributors (to current version):
** Andrew Reynolds
** This file is part of the CVC4 project.
** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS
** in the top-level source directory) and their institutional affiliations.
** All rights reserved. See the file COPYING in the top-level source
** directory for licensing information.\endverbatim
**
** \brief Implementation of proof rule
**/
#include "expr/proof_rule.h"
#include <iostream>
namespace CVC4 {
const char* toString(PfRule id)
{
switch (id)
{
//================================================= Core rules
case PfRule::ASSUME: return "ASSUME";
case PfRule::SCOPE: return "SCOPE";
case PfRule::SUBS: return "SUBS";
case PfRule::REWRITE: return "REWRITE";
case PfRule::MACRO_SR_EQ_INTRO: return "MACRO_SR_EQ_INTRO";
case PfRule::MACRO_SR_PRED_INTRO: return "MACRO_SR_PRED_INTRO";
case PfRule::MACRO_SR_PRED_ELIM: return "MACRO_SR_PRED_ELIM";
case PfRule::MACRO_SR_PRED_TRANSFORM: return "MACRO_SR_PRED_TRANSFORM";
//================================================= Boolean rules
case PfRule::SPLIT: return "SPLIT";
case PfRule::AND_ELIM: return "AND_ELIM";
case PfRule::AND_INTRO: return "AND_INTRO";
case PfRule::NOT_OR_ELIM: return "NOT_OR_ELIM";
case PfRule::IMPLIES_ELIM: return "IMPLIES_ELIM";
case PfRule::NOT_IMPLIES_ELIM1: return "NOT_IMPLIES_ELIM1";
case PfRule::NOT_IMPLIES_ELIM2: return "NOT_IMPLIES_ELIM2";
case PfRule::EQUIV_ELIM1: return "EQUIV_ELIM1";
case PfRule::EQUIV_ELIM2: return "EQUIV_ELIM2";
case PfRule::NOT_EQUIV_ELIM1: return "NOT_EQUIV_ELIM1";
case PfRule::NOT_EQUIV_ELIM2: return "NOT_EQUIV_ELIM2";
case PfRule::XOR_ELIM1: return "XOR_ELIM1";
case PfRule::XOR_ELIM2: return "XOR_ELIM2";
case PfRule::NOT_XOR_ELIM1: return "NOT_XOR_ELIM1";
case PfRule::NOT_XOR_ELIM2: return "NOT_XOR_ELIM2";
case PfRule::ITE_ELIM1: return "ITE_ELIM1";
case PfRule::ITE_ELIM2: return "ITE_ELIM2";
case PfRule::NOT_ITE_ELIM1: return "NOT_ITE_ELIM1";
case PfRule::NOT_ITE_ELIM2: return "NOT_ITE_ELIM2";
case PfRule::CONTRA: return "CONTRA";
//================================================= De Morgan rules
case PfRule::NOT_AND: return "NOT_AND";
//================================================= CNF rules
case PfRule::CNF_AND_POS: return "CNF_AND_POS";
case PfRule::CNF_AND_NEG: return "CNF_AND_NEG";
case PfRule::CNF_OR_POS: return "CNF_OR_POS";
case PfRule::CNF_OR_NEG: return "CNF_OR_NEG";
case PfRule::CNF_IMPLIES_POS: return "CNF_IMPLIES_POS";
case PfRule::CNF_IMPLIES_NEG1: return "CNF_IMPLIES_NEG1";
case PfRule::CNF_IMPLIES_NEG2: return "CNF_IMPLIES_NEG2";
case PfRule::CNF_EQUIV_POS1: return "CNF_EQUIV_POS1";
case PfRule::CNF_EQUIV_POS2: return "CNF_EQUIV_POS2";
case PfRule::CNF_EQUIV_NEG1: return "CNF_EQUIV_NEG1";
case PfRule::CNF_EQUIV_NEG2: return "CNF_EQUIV_NEG2";
case PfRule::CNF_XOR_POS1: return "CNF_XOR_POS1";
case PfRule::CNF_XOR_POS2: return "CNF_XOR_POS2";
case PfRule::CNF_XOR_NEG1: return "CNF_XOR_NEG1";
case PfRule::CNF_XOR_NEG2: return "CNF_XOR_NEG2";
case PfRule::CNF_ITE_POS1: return "CNF_ITE_POS1";
case PfRule::CNF_ITE_POS2: return "CNF_ITE_POS2";
case PfRule::CNF_ITE_POS3: return "CNF_ITE_POS3";
case PfRule::CNF_ITE_NEG1: return "CNF_ITE_NEG1";
case PfRule::CNF_ITE_NEG2: return "CNF_ITE_NEG2";
case PfRule::CNF_ITE_NEG3: return "CNF_ITE_NEG3";
//================================================= Equality rules
case PfRule::REFL: return "REFL";
case PfRule::SYMM: return "SYMM";
case PfRule::TRANS: return "TRANS";
case PfRule::CONG: return "CONG";
case PfRule::TRUE_INTRO: return "TRUE_INTRO";
case PfRule::TRUE_ELIM: return "TRUE_ELIM";
case PfRule::FALSE_INTRO: return "FALSE_INTRO";
case PfRule::FALSE_ELIM: return "FALSE_ELIM";
//================================================= Quantifiers rules
case PfRule::WITNESS_INTRO: return "WITNESS_INTRO";
case PfRule::EXISTS_INTRO: return "EXISTS_INTRO";
case PfRule::SKOLEMIZE: return "SKOLEMIZE";
case PfRule::INSTANTIATE: return "INSTANTIATE";
//================================================= Unknown rule
case PfRule::UNKNOWN: return "UNKNOWN";
default: return "?";
}
}
std::ostream& operator<<(std::ostream& out, PfRule id)
{
out << toString(id);
return out;
}
} // namespace CVC4
|
