Connect++ 0.4.0
A fast, readable connection prover for first-order logic.
Loading...
Searching...
No Matches
InferenceItem.cpp
1/*
2
3Copyright © 2023-24 Sean Holden. All rights reserved.
4
5*/
6/*
7
8This file is part of Connect++.
9
10Connect++ is free software: you can redistribute it and/or modify it
11under the terms of the GNU General Public License as published by the
12Free Software Foundation, either version 3 of the License, or (at your
13option) any later version.
14
15Connect++ is distributed in the hope that it will be useful, but WITHOUT
16ANY WARRANTY; without even the implied warranty of MERCHANTABILITY or
17FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public License for
18more details.
19
20You should have received a copy of the GNU General Public License along
21with Connect++. If not, see <https://www.gnu.org/licenses/>.
22
23*/
24
25#include "InferenceItem.hpp"
26
27//----------------------------------------------------------------------
28ostream& operator<<(ostream& out, const InferenceItemType& inf) {
29 switch (inf) {
30 case InferenceItemType::Start:
31 out << "Start inference";
32 break;
33 case InferenceItemType::Reduction:
34 out << "Reduction inference";
35 break;
36 case InferenceItemType::Extension:
37 out << "Extension inference";
38 break;
39 case InferenceItemType::Axiom:
40 out << "Axiom inference";
41 break;
42 case InferenceItemType::Lemma:
43 out << "Lemma inference";
44 break;
45 default:
46 break;
47 }
48 return out;
49}
50//----------------------------------------------------------------------
51InferenceItem::InferenceItem()
52: T(InferenceItemType::None)
53, L()
54, Lindex(0)
55, C_2(0)
56, Lprime(0)
57, sigma()
58, index_in_path(0)
59, index_in_lemmata(0)
60{}
61//----------------------------------------------------------------------
62InferenceItem::InferenceItem(
63 InferenceItemType _T)
64: T(_T)
65, L()
66, Lindex(0)
67, C_2(0)
68, Lprime(0)
69, sigma()
70, index_in_path(0)
71, index_in_lemmata(0)
72{}
73//----------------------------------------------------------------------
74InferenceItem::InferenceItem
75(InferenceItemType _T,
76ClauseNum _C_2)
77: T(_T)
78, L()
79, Lindex(0)
80, C_2(_C_2)
81, Lprime(0)
82, sigma()
83, index_in_path(0)
84, index_in_lemmata(0)
85{}
86//----------------------------------------------------------------------
87InferenceItem::InferenceItem(
88 InferenceItemType _T,
89 const Literal& _L,
90 LitNum _Lindex)
91: T(_T)
92, L(_L)
93, Lindex(_Lindex)
94, C_2(0)
95, Lprime(0)
96, sigma()
97, index_in_path(0)
98, index_in_lemmata(0)
99{}
100//----------------------------------------------------------------------
101InferenceItem::InferenceItem(
102 InferenceItemType _T,
103 const Literal& _L,
104 LitNum _Lindex,
105 size_t _index_in_lemmata)
106: T(_T)
107, L(_L)
108, Lindex(_Lindex)
109, C_2(0)
110, Lprime(0)
111, sigma()
112, index_in_path(0)
113, index_in_lemmata(_index_in_lemmata)
114{}
115//----------------------------------------------------------------------
116InferenceItem::InferenceItem(
117 InferenceItemType _T,
118 const Literal& _L,
119 LitNum _Lindex,
120 ClauseNum _C_2,
121 LitNum _LPrime,
122 const Substitution& _sigma)
123: T(_T)
124, L(_L)
125, Lindex(_Lindex)
126, C_2(_C_2)
127, Lprime(_LPrime)
128, sigma(_sigma)
129, index_in_path(0)
130, index_in_lemmata(0)
131{}
132//----------------------------------------------------------------------
133InferenceItem::InferenceItem(
134 InferenceItemType _T,
135 const Literal& _L,
136 LitNum _Lindex,
137 ClauseNum _C_2,
138 LitNum _LPrime,
139 const Substitution& _sigma,
140 size_t _index_in_path)
141: T(_T)
142, L(_L)
143, Lindex(_Lindex)
144, C_2(_C_2)
145, Lprime(_LPrime)
146, sigma(_sigma)
147, index_in_path(_index_in_path)
148, index_in_lemmata(0)
149{}
150//----------------------------------------------------------------------
151ostream& operator<<(ostream& out, const InferenceItem& si) {
152 out << "Inference Item: ";
153 switch (si.T) {
154 case InferenceItemType::Start:
155 out << "Start: clause number = "
156 << to_string(si.C_2);
157 break;
158 case InferenceItemType::Reduction:
159 out << "Reduction: L = " << si.L << " index = "
160 << to_string(si.Lindex);
161 out << " Substitution: " << si.sigma;
162 break;
163 case InferenceItemType::Extension:
164 out << "Extension: L = " << si.L << " C_2 = "
165 << to_string(si.C_2)
166 << " L' = " << to_string(si.Lprime);
167 out << " Substitution: " << si.sigma;
168 break;
169 case InferenceItemType::Axiom:
170 out << "Axiom";
171 break;
172 case InferenceItemType::Lemma:
173 out << "Lemma: L = " << si.L << " index = "
174 << to_string(si.Lindex);
175 break;
176 default:
177 break;
178 };
179 return out;
180}
Literal
Basic representation of literals, bundling together (pointers to) a Predicate, a collection of argume...
Definition Literal.hpp:50
Substitution
General representation of a substitution.
Definition Substitution.hpp:57
InferenceItem
Full representation of inferences, beyond just the name.
Definition InferenceItem.hpp:61
InferenceItem::Lindex
LitNum Lindex
The index of the literal within the clause being used.
Definition InferenceItem.hpp:73
InferenceItem::Lprime
LitNum Lprime
The index of the literal in C_2 being used.
Definition InferenceItem.hpp:82
InferenceItem::sigma
Substitution sigma
A copy of the substitution that makes the rule applicable.
Definition InferenceItem.hpp:87
InferenceItem::L
Literal L
The Literal that is used to make the inference.
Definition InferenceItem.hpp:69
InferenceItem::C_2
ClauseNum C_2
For extensions, the number of the clause for which a fresh copy is being made.
Definition InferenceItem.hpp:78
InferenceItem::T
InferenceItemType T
What kind of inference is this?
Definition InferenceItem.hpp:65
InferenceItem::InferenceItem
InferenceItem()
Constructor - probably unused.
Definition InferenceItem.cpp:51