Connect++ 0.6.0
A fast, readable connection prover for first-order logic.
Loading...
Searching...
No Matches
Public Member Functions | Public Attributes | List of all members
InferenceItem Struct Reference

Full representation of inferences, beyond just the name. More...

#include <InferenceItem.hpp>

Collaboration diagram for InferenceItem:
Collaboration graph
[legend]

Public Member Functions

 InferenceItem ()
 Constructor - probably unused.
 
 InferenceItem (InferenceItemType)
 Constructor - probably unused.
 
 InferenceItem (InferenceItemType, ClauseNum)
 Constructor - probably unused.
 
 InferenceItem (InferenceItemType, const Literal &, LitNum)
 Constructor - probably unused.
 
 InferenceItem (InferenceItemType, const Literal &, LitNum, size_t)
 Constructor for lemmata.
 
 InferenceItem (InferenceItemType, const Literal &, LitNum, ClauseNum, LitNum, size_t, size_t)
 Constructor for extensions.
 
 InferenceItem (InferenceItemType, const Literal &, LitNum, ClauseNum, LitNum, const Substitution &, size_t)
 Constructor for reductions.
 

Public Attributes

InferenceItemType T
 What kind of inference is this?
 
Literal L
 The Literal that is used to make the inference.
 
LitNum Lindex
 The index of the literal within the clause being used.
 
ClauseNum C_2
 For extensions, the number of the clause for which a fresh copy is being made.
 
LitNum Lprime
 The index of the literal in C_2 being used.
 
Substitution sigma
 A copy of the substitution that makes the rule applicable. This may or may not be reusable, depending on the specific implementation. As of V0.5.0 extensions need to recompute it.
 
size_t index_in_path
 The index in the path of the literal being used.
 
size_t index_in_lemmata
 For certification, you want to know which element of the lemmata list was used when the Lemma rule was employed.
 
size_t index_in_LC_index
 Estensions are performance-critical. We store the index into the literal_clause_index, and the second index giving us the relevant pair.
 
size_t index_to_LC
 Estensions are performance-critical. We store the index into the literal_clause_index, and the second index giving us the relevant pair.
 

Detailed Description

Full representation of inferences, beyond just the name.

The nomenclature here deliberately mimics that used in many of the publications describing the method, in an attempt to maintain readability.

As these are mostly used just to store information as the stack representing the proof is built, the methods are mostly just constructors.

Definition at line 61 of file InferenceItem.hpp.

Constructor & Destructor Documentation

◆ InferenceItem() [1/7]

InferenceItem::InferenceItem ( )

Constructor - probably unused.

Definition at line 51 of file InferenceItem.cpp.

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{}
InferenceItem::Lindex
LitNum Lindex
The index of the literal within the clause being used.
Definition InferenceItem.hpp:73
InferenceItem::index_in_lemmata
size_t index_in_lemmata
For certification, you want to know which element of the lemmata list was used when the Lemma rule wa...
Definition InferenceItem.hpp:98
InferenceItem::index_in_path
size_t index_in_path
The index in the path of the literal being used.
Definition InferenceItem.hpp:93
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::index_to_LC
size_t index_to_LC
Estensions are performance-critical. We store the index into the literal_clause_index,...
Definition InferenceItem.hpp:110
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::index_in_LC_index
size_t index_in_LC_index
Estensions are performance-critical. We store the index into the literal_clause_index,...
Definition InferenceItem.hpp:104
InferenceItem::T
InferenceItemType T
What kind of inference is this?
Definition InferenceItem.hpp:65

◆ InferenceItem() [2/7]

InferenceItem::InferenceItem ( InferenceItemType _T)

Constructor - probably unused.

Definition at line 64 of file InferenceItem.cpp.

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{}

◆ InferenceItem() [3/7]

InferenceItem::InferenceItem ( InferenceItemType _T,
ClauseNum _C_2 )

Constructor - probably unused.

Definition at line 78 of file InferenceItem.cpp.

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{}

◆ InferenceItem() [4/7]

InferenceItem::InferenceItem ( InferenceItemType _T,
const Literal & _L,
LitNum _Lindex )

Constructor - probably unused.

Definition at line 93 of file InferenceItem.cpp.

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{}

◆ InferenceItem() [5/7]

InferenceItem::InferenceItem ( InferenceItemType _T,
const Literal & _L,
LitNum _Lindex,
size_t _index_in_lemmata )

Constructor for lemmata.

The last parameter is for index_in_lemmata.

Definition at line 109 of file InferenceItem.cpp.

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{}

◆ InferenceItem() [6/7]

InferenceItem::InferenceItem ( InferenceItemType _T,
const Literal & _L,
LitNum _Lindex,
ClauseNum _C_2,
LitNum _LPrime,
size_t _LC_i,
size_t _LC )

Constructor for extensions.

Definition at line 126 of file InferenceItem.cpp.

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{}

◆ InferenceItem() [7/7]

InferenceItem::InferenceItem ( InferenceItemType _T,
const Literal & _L,
LitNum _Lindex,
ClauseNum _C_2,
LitNum _LPrime,
const Substitution & _sigma,
size_t _index_in_path )

Constructor for reductions.

Definition at line 146 of file InferenceItem.cpp.

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{}

Member Data Documentation

◆ C_2

ClauseNum InferenceItem::C_2

For extensions, the number of the clause for which a fresh copy is being made.

Definition at line 78 of file InferenceItem.hpp.

◆ index_in_LC_index

size_t InferenceItem::index_in_LC_index

Estensions are performance-critical. We store the index into the literal_clause_index, and the second index giving us the relevant pair.

Definition at line 104 of file InferenceItem.hpp.

◆ index_in_lemmata

size_t InferenceItem::index_in_lemmata

For certification, you want to know which element of the lemmata list was used when the Lemma rule was employed.

Definition at line 98 of file InferenceItem.hpp.

◆ index_in_path

size_t InferenceItem::index_in_path

The index in the path of the literal being used.

Definition at line 93 of file InferenceItem.hpp.

◆ index_to_LC

size_t InferenceItem::index_to_LC

Estensions are performance-critical. We store the index into the literal_clause_index, and the second index giving us the relevant pair.

Definition at line 110 of file InferenceItem.hpp.

◆ L

Literal InferenceItem::L

The Literal that is used to make the inference.

Definition at line 69 of file InferenceItem.hpp.

◆ Lindex

LitNum InferenceItem::Lindex

The index of the literal within the clause being used.

Definition at line 73 of file InferenceItem.hpp.

◆ Lprime

LitNum InferenceItem::Lprime

The index of the literal in C_2 being used.

Definition at line 82 of file InferenceItem.hpp.

◆ sigma

Substitution InferenceItem::sigma

A copy of the substitution that makes the rule applicable. This may or may not be reusable, depending on the specific implementation. As of V0.5.0 extensions need to recompute it.

Definition at line 89 of file InferenceItem.hpp.

◆ T

InferenceItemType InferenceItem::T

What kind of inference is this?

Definition at line 65 of file InferenceItem.hpp.

The documentation for this struct was generated from the following files: