Connect++ 0.4.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, const Substitution &)
 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.
 
size_t index_in_path
 The index in the path of the literal being usedd.
 
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.
 

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{}
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:96
InferenceItem::index_in_path
size_t index_in_path
The index in the path of the literal being usedd.
Definition InferenceItem.hpp:91
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() [2/7]

InferenceItem::InferenceItem ( InferenceItemType _T)

Constructor - probably unused.

Definition at line 62 of file InferenceItem.cpp.

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

◆ InferenceItem() [3/7]

InferenceItem::InferenceItem ( InferenceItemType _T,
ClauseNum _C_2 )

Constructor - probably unused.

Definition at line 74 of file InferenceItem.cpp.

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

◆ InferenceItem() [4/7]

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

Constructor - probably unused.

Definition at line 87 of file InferenceItem.cpp.

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

◆ 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 101 of file InferenceItem.cpp.

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

◆ InferenceItem() [6/7]

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

Constructor for extensions.

Definition at line 116 of file InferenceItem.cpp.

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

◆ 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 133 of file InferenceItem.cpp.

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

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_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 96 of file InferenceItem.hpp.

◆ index_in_path

size_t InferenceItem::index_in_path

The index in the path of the literal being usedd.

Definition at line 91 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.

Definition at line 87 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: