|
clingo
|
All Classes Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros Groups
|
clingo
|
Base class for learnt constraints. More...
#include <constraint.h>
Public Member Functions | |
| LearntConstraint () | |
| ConstraintType | type () const |
| Returns the type of this learnt constraint. More... | |
| virtual bool | locked (const Solver &s) const =0 |
| virtual Activity | activity () const |
| Returns the activity of the constraint. More... | |
| virtual void | decreaseActivity () |
| Asks the constraint to decrease its activity. More... | |
| virtual void | resetActivity (Activity hint) |
| Asks the constraint to reset its activity. More... | |
| virtual uint32 | isOpen (const Solver &s, const TypeSet &t, LitVec &freeLits)=0 |
| Shall return 0 if either !t.inSet(type()) or this constraint is satisfied w.r.t the current assignment. More... | |
 Public Member Functions inherited from Clasp::Constraint | |
| Constraint () | |
| virtual Constraint * | cloneAttach (Solver &other)=0 |
| Returns a clone of this and adds necessary watches to the given solver. More... | |
| virtual void | destroy (Solver *s=0, bool detach=false) |
| Default is to call delete this. More... | |
| virtual PropResult | propagate (Solver &s, Literal p, uint32 &data)=0 |
| virtual void | reason (Solver &s, Literal p, LitVec &lits)=0 |
| virtual bool | minimize (Solver &s, Literal p, CCMinRecursive *rec) |
| virtual void | undoLevel (Solver &s) |
| Called when the solver undid a decision level watched by this constraint. More... | |
| virtual bool | simplify (Solver &s, bool reinit=false) |
| virtual uint32 | estimateComplexity (const Solver &s) const |
| Returns an estimate of the constraint's complexity relative to a clause (complexity = 1). More... | |
| virtual ClauseHead * | clause () |
| Shall return this if constraint is a clause, otherwise 0. More... | |
| virtual bool | valid (Solver &s) |
| Shall return whether the constraint is valid (i.e. not conflicting) w.r.t the current assignment in s. More... | |
Protected Member Functions | |
| ~LearntConstraint () | |
| Protected Member Functions inherited from Clasp::Constraint | |
| virtual | ~Constraint () |
Base class for learnt constraints.
Base class for constraints that can be learnt during search. A learnt constraint is a constraint with the difference that it can be created and deleted dynamically during the search-process and is subject to nogood-deletion. Typical examples are conflict clauses which are created during conflict analysis and loop formulas which are created during unfounded-set checks.
A learnt constraint must additionally define the method locked in order to tell a solver if the constraint can be safely deleted or not. Furthermore whenever a solver needs to delete some learnt constraints it will first delete those with a low activity. A learnt constraint may therefore bump its activity whenever it sees fit in order to delay its deletion.
| Clasp::LearntConstraint::LearntConstraint | ( | ) |
|
protected |
|
virtual |
Returns the activity of the constraint.
Reimplemented in Clasp::LoopFormula, and Clasp::ClauseHead.
|
virtual |
Asks the constraint to decrease its activity.
Reimplemented in Clasp::LoopFormula, and Clasp::ClauseHead.
|
pure virtual |
Shall return 0 if either !t.inSet(type()) or this constraint is satisfied w.r.t the current assignment.
If this constraint is currently not satisfied and t.inSet(type()), shall return type() and freeLits shall contain all currently unassigned literals of this constraint.
Implemented in Clasp::mt::SharedLitsClause, Clasp::LoopFormula, and Clasp::Clause.
|
pure virtual |
Shall return true if this constraint can't be deleted because it currently implies one ore more literals and false otherwise.
Implemented in Clasp::LoopFormula, and Clasp::ClauseHead.
|
virtual |
Asks the constraint to reset its activity.
Reimplemented in Clasp::LoopFormula, and Clasp::ClauseHead.
|
virtual |
Returns the type of this learnt constraint.
Reimplemented from Clasp::Constraint.
Reimplemented in Clasp::ClauseHead.
1.8.7