Class Antecedent¶
- Defined in File structures.h
Class Documentation¶
-
class
Antecedent¶ Antecedent can be either a clause or a literal.
Public Functions
-
Antecedent()¶ Creates an empty antecedent clause with ID zero.
-
Antecedent(const ClauseOfs cl_ofs)¶ Shifts the clause offset by 1 to the left and then adds 1.
- Parameters
cl_ofs: Clause offset.
-
bool
isAClause() const¶ Checks if the antecendent is a clause. This is done by checking if the least significant bit is a 0b0 or a 0b1.
- Return
- True if the antecedent is a clause. False if it is a literal.
-
ClauseOfs
asCl() const¶ Returns the antecedent information formatted as a clause
- Return
- Antecedent clause
-
LiteralID
asLit()¶ Returns the antecedent information formatted as a literal.
- Return
- Antecedent literal
-
bool
isAnt() const¶ MT - A NON-Antecedent will only be A NOT_A_CLAUSE Clause Id
Checks whether this is an actual antecedent.
- Return
- true if the this is not a true antecendent (i.e., the value equals 1).
-