Connect++ 0.6.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, index_in_LC_index(0)
61, index_to_LC(0)
62{}
63//----------------------------------------------------------------------
64InferenceItem::InferenceItem(
65 InferenceItemType _T)
66: T(_T)
67, L()
68, Lindex(0)
69, C_2(0)
70, Lprime(0)
71, sigma()
72, index_in_path(0)
73, index_in_lemmata(0)
74, index_in_LC_index(0)
75, index_to_LC(0)
76{}
77//----------------------------------------------------------------------
78InferenceItem::InferenceItem
79(InferenceItemType _T,
80ClauseNum _C_2)
81: T(_T)
82, L()
83, Lindex(0)
84, C_2(_C_2)
85, Lprime(0)
86, sigma()
87, index_in_path(0)
88, index_in_lemmata(0)
89, index_in_LC_index(0)
90, index_to_LC(0)
91{}
92//----------------------------------------------------------------------
93InferenceItem::InferenceItem(
94 InferenceItemType _T,
95 const Literal& _L,
96 LitNum _Lindex)
97: T(_T)
98, L(_L)
99, Lindex(_Lindex)
100, C_2(0)
101, Lprime(0)
102, sigma()
103, index_in_path(0)
104, index_in_lemmata(0)
105, index_in_LC_index(0)
106, index_to_LC(0)
107{}
108//----------------------------------------------------------------------
109InferenceItem::InferenceItem(
110 InferenceItemType _T,
111 const Literal& _L,
112 LitNum _Lindex,
113 size_t _index_in_lemmata)
114: T(_T)
115, L(_L)
116, Lindex(_Lindex)
117, C_2(0)
118, Lprime(0)
119, sigma()
120, index_in_path(0)
121, index_in_lemmata(_index_in_lemmata)
122, index_in_LC_index(0)
123, index_to_LC(0)
124{}
125//----------------------------------------------------------------------
126InferenceItem::InferenceItem(
127 InferenceItemType _T,
128 const Literal& _L,
129 LitNum _Lindex,
130 ClauseNum _C_2,
131 LitNum _LPrime,
132 size_t _LC_i,
133 size_t _LC)
134: T(_T)
135, L(_L)
136, Lindex(_Lindex)
137, C_2(_C_2)
138, Lprime(_LPrime)
139, sigma()
140, index_in_path(0)
141, index_in_lemmata(0)
142, index_in_LC_index(_LC_i)
143, index_to_LC(_LC)
144{}
145//----------------------------------------------------------------------
146InferenceItem::InferenceItem(
147 InferenceItemType _T,
148 const Literal& _L,
149 LitNum _Lindex,
150 ClauseNum _C_2,
151 LitNum _LPrime,
152 const Substitution& _sigma,
153 size_t _index_in_path)
154: T(_T)
155, L(_L)
156, Lindex(_Lindex)
157, C_2(_C_2)
158, Lprime(_LPrime)
159, sigma(_sigma)
160, index_in_path(_index_in_path)
161, index_in_lemmata(0)
162{}
163//----------------------------------------------------------------------
164ostream& operator<<(ostream& out, const InferenceItem& si) {
165 out << "Inference Item: ";
166 switch (si.T) {
167 case InferenceItemType::Start:
168 out << "Start: clause number = "
169 << to_string(si.C_2);
170 break;
171 case InferenceItemType::Reduction:
172 out << "Reduction: L = " << si.L << " index = "
173 << to_string(si.Lindex);
174 out << " Substitution: " << si.sigma;
175 break;
176 case InferenceItemType::Extension:
177 out << "Extension: L = " << si.L << " C_2 = "
178 << to_string(si.C_2)
179 << " L' = " << to_string(si.Lprime);
180 out << " Substitution: " << si.sigma;
181 break;
182 case InferenceItemType::Axiom:
183 out << "Axiom";
184 break;
185 case InferenceItemType::Lemma:
186 out << "Lemma: L = " << si.L << " index = "
187 << to_string(si.Lindex);
188 break;
189 default:
190 break;
191 };
192 return out;
193}
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. This may or may not be reusable,...
Definition InferenceItem.hpp:89
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