Connect++ 0.6.1
A fast, readable connection prover for first-order logic.
Loading...
Searching...
No Matches
InferenceItem.cpp
1/*
2
3Copyright © 2023-25 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(InferenceItemType _T)
65: T(_T)
66, L()
67, Lindex(0)
68, C_2(0)
69, Lprime(0)
70, sigma()
71, index_in_path(0)
72, index_in_lemmata(0)
73, index_in_LC_index(0)
74, index_to_LC(0)
75{}
76//----------------------------------------------------------------------
77InferenceItem::InferenceItem(InferenceItemType _T, ClauseNum _C_2)
78: T(_T)
79, L()
80, Lindex(0)
81, C_2(_C_2)
82, Lprime(0)
83, sigma()
84, index_in_path(0)
85, index_in_lemmata(0)
86, index_in_LC_index(0)
87, index_to_LC(0)
88{}
89//----------------------------------------------------------------------
90InferenceItem::InferenceItem(InferenceItemType _T, const Literal& _L,
91 LitNum _Lindex)
92: T(_T)
93, L(_L)
94, Lindex(_Lindex)
95, C_2(0)
96, Lprime(0)
97, sigma()
98, index_in_path(0)
99, index_in_lemmata(0)
100, index_in_LC_index(0)
101, index_to_LC(0)
102{}
103//----------------------------------------------------------------------
104InferenceItem::InferenceItem(InferenceItemType _T, const Literal& _L,
105 LitNum _Lindex, 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, index_in_LC_index(0)
115, index_to_LC(0)
116{}
117//----------------------------------------------------------------------
118InferenceItem::InferenceItem(InferenceItemType _T, const Literal& _L,
119 LitNum _Lindex, ClauseNum _C_2, LitNum _LPrime, size_t _LC_i, size_t _LC)
120: T(_T)
121, L(_L)
122, Lindex(_Lindex)
123, C_2(_C_2)
124, Lprime(_LPrime)
125, sigma()
126, index_in_path(0)
127, index_in_lemmata(0)
128, index_in_LC_index(_LC_i)
129, index_to_LC(_LC)
130{}
131//----------------------------------------------------------------------
132InferenceItem::InferenceItem(InferenceItemType _T, const Literal& _L,
133 LitNum _Lindex, ClauseNum _C_2, LitNum _LPrime, const Substitution& _sigma,
134 size_t _index_in_path)
135: T(_T)
136, L(_L)
137, Lindex(_Lindex)
138, C_2(_C_2)
139, Lprime(_LPrime)
140, sigma(_sigma)
141, index_in_path(_index_in_path)
142, index_in_lemmata(0)
143{}
144//----------------------------------------------------------------------
145ostream& operator<<(ostream& out, const InferenceItem& si) {
146 out << "Inference Item: ";
147 switch (si.T) {
148 case InferenceItemType::Start:
149 out << "Start: clause number = "
150 << to_string(si.C_2);
151 break;
152 case InferenceItemType::Reduction:
153 out << "Reduction: L = " << si.L << " index = "
154 << to_string(si.Lindex);
155 out << " Substitution: " << si.sigma;
156 break;
157 case InferenceItemType::Extension:
158 out << "Extension: L = " << si.L << " C_2 = "
159 << to_string(si.C_2)
160 << " L' = " << to_string(si.Lprime);
161 out << " Substitution: " << si.sigma;
162 break;
163 case InferenceItemType::Axiom:
164 out << "Axiom";
165 break;
166 case InferenceItemType::Lemma:
167 out << "Lemma: L = " << si.L << " index = "
168 << to_string(si.Lindex);
169 break;
170 default:
171 break;
172 };
173 return out;
174}
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.
Definition InferenceItem.cpp:51