Stores a reference to the constraint that implied a literal. More...
#include <constraint.h>
Public Types | |
| enum | Type { generic_constraint = 0, ternary_constraint = 1, binary_constraint = 2 } |
Public Member Functions | |
| Antecedent () | |
| Creates a null Antecedent. | |
| Antecedent (const Literal &p) | |
| Creates an Antecedent from the literal p. | |
| Antecedent (const Literal &p, const Literal &q) | |
| Creates an Antecedent from the literals p and q. | |
| Antecedent (Constraint *con) | |
| Creates an Antecedent from the Constraint con. | |
| uint64 | asUint () const |
| uint64 & | asUint () |
| Constraint * | constraint () const |
| Extracts the constraint-pointer stored in this object. | |
| Literal | firstLiteral () const |
| Extracts the first literal stored in this object. | |
| bool | isNull () const |
| Returns true if this antecedent does not refer to any constraint. | |
| bool | learnt () const |
| Returns true if the antecedent is a learnt nogood. | |
| template<class S > | |
| bool | minimize (S &s, Literal p, CCMinRecursive *rec) const |
| bool | operator== (const Constraint *con) const |
| Returns true iff the antecedent refers to the constraint con. | |
| void | reason (Solver &s, Literal p, LitVec &lits) const |
| Returns the reason for p. | |
| Literal | secondLiteral () const |
| Extracts the second literal stored in this object. | |
| Type | type () const |
| Returns the antecedent's type. | |
Static Public Member Functions | |
| static bool | checkPlatformAssumptions () |
| Checks whether the imlementation-assumptions hold on this platform. | |
Private Attributes | |
| uint64 | data_ |
Stores a reference to the constraint that implied a literal.
Stores a reference to the constraint that implied a certain literal or null if the literal has no antecedent (i.e. is a decision literal or a top-level fact).
The class stores all three representations in one 64-bit integer and makes the following platform assumptions:
These assumptions are not guaranteed by the C++ Standard but should nontheless hold on most 32- and 64-bit platforms.
From the 64-bits the first 2-bits encode the type stored:
Definition at line 399 of file constraint.h.
Definition at line 401 of file constraint.h.
| Clasp::Antecedent::Antecedent | ( | ) | [inline] |
Creates a null Antecedent.
Definition at line 406 of file constraint.h.
| Clasp::Antecedent::Antecedent | ( | const Literal & | p | ) | [inline] |
Creates an Antecedent from the literal p.
Definition at line 412 of file constraint.h.
| Clasp::Antecedent::Antecedent | ( | const Literal & | p, |
| const Literal & | q | ||
| ) | [inline] |
Creates an Antecedent from the literals p and q.
Definition at line 422 of file constraint.h.
| Clasp::Antecedent::Antecedent | ( | Constraint * | con | ) | [inline] |
Creates an Antecedent from the Constraint con.
Definition at line 433 of file constraint.h.
| uint64 Clasp::Antecedent::asUint | ( | ) | const [inline] |
Definition at line 518 of file constraint.h.
| uint64& Clasp::Antecedent::asUint | ( | ) | [inline] |
Definition at line 519 of file constraint.h.
| bool Clasp::Antecedent::checkPlatformAssumptions | ( | ) | [static] |
Checks whether the imlementation-assumptions hold on this platform.
throws PlatformError on error
Definition at line 59 of file constraint.cpp.
| Constraint* Clasp::Antecedent::constraint | ( | ) | const [inline] |
Extracts the constraint-pointer stored in this object.
Definition at line 454 of file constraint.h.
| Literal Clasp::Antecedent::firstLiteral | ( | ) | const [inline] |
Extracts the first literal stored in this object.
Definition at line 463 of file constraint.h.
| bool Clasp::Antecedent::isNull | ( | ) | const [inline] |
Returns true if this antecedent does not refer to any constraint.
Definition at line 438 of file constraint.h.
| bool Clasp::Antecedent::learnt | ( | ) | const [inline] |
Returns true if the antecedent is a learnt nogood.
Definition at line 448 of file constraint.h.
| bool Clasp::Antecedent::minimize | ( | S & | s, |
| Literal | p, | ||
| CCMinRecursive * | rec | ||
| ) | const [inline] |
Definition at line 495 of file constraint.h.
| bool Clasp::Antecedent::operator== | ( | const Constraint * | con | ) | const [inline] |
Returns true iff the antecedent refers to the constraint con.
Definition at line 508 of file constraint.h.
| void Clasp::Antecedent::reason | ( | Solver & | s, |
| Literal | p, | ||
| LitVec & | lits | ||
| ) | const [inline] |
| Literal Clasp::Antecedent::secondLiteral | ( | ) | const [inline] |
Extracts the second literal stored in this object.
Definition at line 472 of file constraint.h.
| Type Clasp::Antecedent::type | ( | ) | const [inline] |
Returns the antecedent's type.
Definition at line 443 of file constraint.h.
uint64 Clasp::Antecedent::data_ [private] |
Definition at line 521 of file constraint.h.