|
clingo
|
All Classes Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros Groups
|
clingo
|
#include <solver.h>
Classes | |
| struct | DBInfo |
Public Types | |
| typedef PodVector< Constraint * > ::type | ConstraintDB |
| typedef const ConstraintDB & | DBRef |
| typedef SingleOwnerPtr < DecisionHeuristic > | Heuristic |
Public Member Functions | |
| const SharedContext * | sharedContext () const |
| Returns a pointer to the shared context object of this solver. More... | |
| SatPreprocessor * | satPrepro () const |
| Returns a pointer to the sat-preprocessor used by this solver. More... | |
| const SolverParams & | configuration () const |
| Returns the configuration for this object. More... | |
| const SolveParams & | searchConfig () const |
| Returns the solve parameters for this object. More... | |
| const Heuristic & | heuristic () const |
| uint32 | id () const |
| Heuristic & | heuristic () |
| VarInfo | varInfo (Var v) const |
| const SymbolTable & | symbolTable () const |
| Literal | tagLiteral () const |
| void | add (Constraint *c) |
| Adds the problem constraint c to the solver. More... | |
| bool | add (const ClauseRep &c, bool isNew=true) |
| Adds a suitable representation of the given clause to the solver. More... | |
| bool | allowImplicit (const ClauseRep &c) const |
| Returns whether c can be stored in the shared short implication graph. More... | |
| PostPropagator * | getPost (uint32 prio) const |
| Returns the post propagator with the given priority or 0 if no such post propagator exists. More... | |
| bool | addPost (PostPropagator *p) |
| Adds p as post propagator to this solver. More... | |
| void | removePost (PostPropagator *p) |
| Removes p from the solver's list of post propagators. More... | |
CDNL-functions. | |
| ValueRep | search (SearchLimits &limit, double randf=0.0) |
| Searches for a model as long as the given limit is not reached. More... | |
| ValueRep | search (uint64 maxC, uint32 maxL, bool local=false, double rp=0.0) |
| bool | pushRoot (const LitVec &path) |
| Adds path to the current root-path and adjusts the root-level accordingly. More... | |
| bool | pushRoot (Literal p) |
| void | setEnumerationConstraint (Constraint *c) |
| void | pushRootLevel (uint32 i=1) |
| Moves the root-level i levels down (i.e. away from the top-level). More... | |
| bool | popRootLevel (uint32 i=1, LitVec *popped=0, bool aux=true) |
| Moves the root-level i levels up (i.e. towards the top-level). More... | |
| void | clearStopConflict () |
| Removes a previously set stop conflict and restores the root level. More... | |
| uint32 | rootLevel () const |
| Returns the current root level. More... | |
| bool | clearAssumptions () |
| Removes any implications made between the top-level and the root-level. More... | |
| void | addLearnt (LearntConstraint *c, uint32 size, ConstraintType type) |
| Adds the learnt constraint c to the solver. More... | |
| void | addLearnt (LearntConstraint *c, uint32 size) |
| uint32 | receive (SharedLiterals **out, uint32 maxOut) const |
| Tries to receive at most maxOut clauses. More... | |
| SharedLiterals * | distribute (const Literal *lits, uint32 size, const ClauseInfo &extra) |
| Distributes the clause in lits via the distributor. More... | |
| void | restart () |
| Returns to the maximum of rootLevel() and backtrackLevel() and increases the number of restarts. More... | |
| void | setBacktrackLevel (uint32 dl) |
| Sets the backtracking level to dl. More... | |
| uint32 | backtrackLevel () const |
| Returns the current backtracking level. More... | |
| bool | splittable () const |
| Returns whether the solver can split-off work. More... | |
| bool | split (LitVec &out) |
| Tries to split-off disjoint work from the solver's currrent guiding path and returns it in out. More... | |
| void | copyGuidingPath (LitVec &out) |
| Copies the solver's currrent guiding path to gp. More... | |
| bool | simplify () |
| If called on top-level, removes SAT-clauses + Constraints for which Constraint::simplify returned true. More... | |
| void | shuffleOnNextSimplify () |
| Shuffle constraints upon next simplification. More... | |
| Var | pushTagVar (bool pushToRoot) |
| Requests a special aux variable for tagging conditional knowledge. More... | |
| void | removeConditional () |
| Removes all conditional knowledge, i.e. all previously tagged learnt clauses. More... | |
| void | strengthenConditional () |
| Resolves all tagged clauses with the tag literal and thereby strengthens the learnt db. More... | |
| bool | force (const Literal &p, const Antecedent &a) |
| Sets the literal p to true and schedules p for propagation. More... | |
| bool | force (const Literal &p, const Antecedent &a, uint32 data) |
| bool | force (Literal p, uint32 dl, const Antecedent &r, uint32 d=UINT32_MAX) |
| Assigns p at dl because of r. More... | |
| bool | force (Literal p) |
| Assigns p as a fact at decision level 0. More... | |
| bool | assume (const Literal &p) |
| Assumes the literal p if possible. More... | |
| bool | decideNextBranch (double f=0.0) |
| Selects and assumes the next branching literal by calling the installed decision heuristic. More... | |
| void | setStopConflict () |
| Sets a conflict that forces the solver to terminate its search. More... | |
| bool | propagate () |
| bool | propagateUntil (PostPropagator *p) |
| bool | test (Literal p, PostPropagator *c) |
| Executes a one-step lookahead on p. More... | |
| uint32 | estimateBCP (const Literal &p, int maxRecursionDepth=5) const |
| Estimates the number of assignments following from setting p to true. More... | |
| uint32 | inDegree (WeightLitVec &out) |
| Computes the number of in-edges for each assigned literal. More... | |
| DBInfo | reduceLearnts (float remMax, const ReduceStrategy &rs=ReduceStrategy()) |
| Removes upto remMax percent of the learnt nogoods. More... | |
| bool | resolveConflict () |
| Resolves the active conflict using the selected strategy. More... | |
| bool | backtrack () |
| Backtracks the last decision and sets the backtrack-level to the resulting decision level. More... | |
| void | undoUntil (uint32 dl) |
| Undoes all assignments up to (but not including) decision level dl. More... | |
| uint32 | undoUntil (uint32 dl, bool popBtLevel) |
| Var | pushAuxVar () |
| Adds a new auxiliary variable to this solver. More... | |
| void | popAuxVar (uint32 num=UINT32_MAX) |
| Pops the num most recently added auxiliary variables from this solver. More... | |
Watch management | |
Functions for setting/removing watches.
| |
| uint32 | numWatches (Literal p) const |
| Returns the number of constraints watching the literal p. More... | |
| bool | hasWatch (Literal p, Constraint *c) const |
| Returns true if the constraint c watches the literal p. More... | |
| bool | hasWatch (Literal p, ClauseHead *c) const |
| GenericWatch * | getWatch (Literal p, Constraint *c) const |
| Returns c's watch-structure associated with p. More... | |
| void | addWatch (Literal p, Constraint *c, uint32 data=0) |
| Adds c to the watch-list of p. More... | |
| void | addWatch (Literal p, const ClauseWatch &w) |
| Adds w to the clause watch-list of p. More... | |
| void | removeWatch (const Literal &p, Constraint *c) |
| Removes c from p's watch-list. More... | |
| void | removeWatch (const Literal &p, ClauseHead *c) |
| void | addUndoWatch (uint32 dl, Constraint *c) |
| Adds c to the watch-list of decision-level dl. More... | |
| bool | removeUndoWatch (uint32 dl, Constraint *c) |
| Removes c from the watch-list of the decision level dl. More... | |
Misc functions | |
Low-level implementation functions. Use with care and only if you know what you are doing! | |
| bool | addPost (PostPropagator *p, bool init) |
| bool | setReason (Literal p, const Antecedent &x, uint32 data=UINT32_MAX) |
| Updates the reason for p being tue. More... | |
| void | requestData (Var v) |
| Request additional reason data slot for variable v. More... | |
| void | setPref (Var v, ValueSet::Value which, ValueRep to) |
| void | reason (Literal p, LitVec &out) |
| Returns the reason for p being true as a set of literals. More... | |
| uint32 | updateLearnt (Literal p, const Literal *first, const Literal *last, uint32 cLbd, bool forceUp=false) |
| Computes a new lbd for the antecedent of p given as the range [first, last). More... | |
| bool | ccMinimize (Literal p, CCMinRecursive *rec) const |
| Visitor function for antecedents used during conflict clause minimization. More... | |
| bool | learntLimit (const SearchLimits &x) const |
| Returns true if number of learnts exceeds x.learnts or the soft memory limit is exceeded. More... | |
| void * | allocSmall () |
| Allocates a small block (32-bytes) from the solver's small block pool. More... | |
| void | freeSmall (void *m) |
| Frees a small block previously allocated from the solver's small block pool. More... | |
| void | addLearntBytes (uint32 bytes) |
| void | freeLearntBytes (uint64 bytes) |
| uint32 | simplifyConflictClause (LitVec &cc, ClauseInfo &info, ClauseHead *rhs) |
| simplifies cc and returns finalizeConflictClause(cc, info); More... | |
| uint32 | finalizeConflictClause (LitVec &cc, ClauseInfo &info, uint32 ccRepMode=0) |
| uint32 | countLevels (const Literal *first, const Literal *last, uint32 maxLevels) |
| bool | hasLevel (uint32 dl) const |
| bool | frozenLevel (uint32 dl) const |
| void | markLevel (uint32 dl) |
| void | freezeLevel (uint32 dl) |
| void | unmarkLevel (uint32 dl) |
| void | unfreezeLevel (uint32 dl) |
| void | markSeen (Var v) |
| void | markSeen (Literal p) |
| void | clearSeen (Var v) |
Construction/Destruction/Setup | |
| class | SharedContext |
state inspection | |
Functions for inspecting the state of the solver & search.
| |
| SolverStrategies | strategy |
| RNG | rng |
| ValueVec | model |
| SolverStats | stats |
| uint32 | numProblemVars () const |
| Returns the number of problem variables. More... | |
| uint32 | numAuxVars () const |
| Returns the number of active solver-local aux variables. More... | |
| uint32 | numVars () const |
| Returns the number of solver variables, i.e. numProblemVars() + numAuxVars() More... | |
| bool | validVar (Var var) const |
| Returns true if var represents a valid variable in this solver. More... | |
| bool | auxVar (Var var) const |
| Returns true if var is a solver-local aux var. More... | |
| uint32 | numAssignedVars () const |
| Returns the number of assigned variables. More... | |
| uint32 | numFreeVars () const |
| Returns the number of free variables. More... | |
| ValueRep | value (Var v) const |
| Returns the value of v w.r.t the current assignment. More... | |
| ValueRep | topValue (Var v) const |
| Returns the value of v w.r.t the top level. More... | |
| ValueSet | pref (Var v) const |
| Returns the set of preferred values of v. More... | |
| bool | isTrue (Literal p) const |
| Returns true if p is true w.r.t the current assignment. More... | |
| bool | isFalse (Literal p) const |
| Returns true if p is false w.r.t the current assignment. More... | |
| Literal | trueLit (Var v) const |
| Returns the literal of v being true in the current assignment. More... | |
| uint32 | level (Var v) const |
| Returns the decision level on which v was assigned. More... | |
| bool | seen (Var v) const |
| Returns true if v is currently marked as seen. More... | |
| bool | seen (Literal p) const |
| Returns true if the literal p is currently marked as seen. More... | |
| uint32 | decisionLevel () const |
| Returns the current decision level. More... | |
| bool | validLevel (uint32 dl) const |
| uint32 | levelStart (uint32 dl) const |
| Returns the starting position of decision level dl in the trail. More... | |
| Literal | decision (uint32 dl) const |
| Returns the decision literal of the decision level dl. More... | |
| bool | hasConflict () const |
| Returns true, if the current assignment is conflicting. More... | |
| bool | hasStopConflict () const |
| uint32 | queueSize () const |
| Returns the number of (unprocessed) literals in the propagation queue. More... | |
| uint32 | numConstraints () const |
| Number of problem constraints in this solver. More... | |
| uint32 | numLearntConstraints () const |
| Returns the number of constraints that are currently in the solver's learnt database. More... | |
| const Antecedent & | reason (Literal p) const |
| Returns the reason for p being true. More... | |
| uint32 | reasonData (Literal p) const |
| Returns the additional reason data associated with p. More... | |
| const LitVec & | trail () const |
| Returns the current (partial) assignment as a set of true literals. More... | |
| const Assignment & | assignment () const |
| const LitVec & | conflict () const |
| Returns the current conflict as a set of literals. More... | |
| const LitVec & | conflictClause () const |
| Returns the most recently derived conflict clause. More... | |
| const LitVec & | symmetric () const |
| Returns the set of eliminated literals that are unconstraint w.r.t the last model. More... | |
| Constraint * | enumerationConstraint () const |
| Returns the enumeration constraint set by the enumerator used. More... | |
| DBRef | constraints () const |
| LearntConstraint & | getLearnt (uint32 idx) const |
| Returns the idx'th learnt constraint. More... | |
clasp's Solver class.
A Solver-object maintains the state and provides the functions necessary to implement our CDNL-algorithm.
The interface supports incremental solving (search under assumptions) as well as solution enumeration. To make this possible the solver maintains two special decision levels: the root-level and the backtrack-level.
The root-level is the lowest decision level to which a search can return. Conflicts on the root-level are non-resolvable and end a search - the root-level therefore acts as an artificial top-level during search. Incremental solving is then implemented by first adding a list of unit assumptions and second initializing the root-level to the current decision level. Once search terminates assumptions can be undone by calling clearAssumptions and a new a search can be started using different assumptions.
For model enumeration the solver maintains a backtrack-level which restricts backjumping in order to prevent repeating already enumerated solutions. The solver will never backjump above that level and conflicts on the backtrack-level are resolved by backtracking, i.e. flipping the corresponding decision literal.
| typedef PodVector<Constraint*>::type Clasp::Solver::ConstraintDB |
| typedef const ConstraintDB& Clasp::Solver::DBRef |
| void Clasp::Solver::add | ( | Constraint * | c | ) |
Adds the problem constraint c to the solver.
Problem constraints shall only be added to the master solver of a SharedContext object and only during the setup phase.
| bool Clasp::Solver::add | ( | const ClauseRep & | c, |
| bool | isNew = true |
||
| ) |
Adds a suitable representation of the given clause to the solver.
Depending on the type and size of the given clause, the function either adds a (learnt) constraint to this solver or an implication to the shared implication graph.
|
inline |
Adds the learnt constraint c to the solver.
|
inline |
|
inline |
|
inline |
Adds p as post propagator to this solver.
|
inline |
|
inline |
Adds c to the watch-list of decision-level dl.
Constraints in the watch-list of a decision level are notified when that decision level is about to be backtracked.
|
inline |
Adds c to the watch-list of p.
When p becomes true, c->propagate(p, data, *this) is called.
|
inline |
Adds w to the clause watch-list of p.
|
inline |
Allocates a small block (32-bytes) from the solver's small block pool.
|
inline |
Returns whether c can be stored in the shared short implication graph.
|
inline |
| bool Clasp::Solver::assume | ( | const Literal & | p | ) |
Assumes the literal p if possible.
If p is currently unassigned, sets p to true and starts a new decision level.
| p | The literal to assume. |
|
inline |
Returns true if var is a solver-local aux var.
| bool Clasp::Solver::backtrack | ( | ) |
Backtracks the last decision and sets the backtrack-level to the resulting decision level.
|
inline |
Returns the current backtracking level.
|
inline |
Visitor function for antecedents used during conflict clause minimization.
| bool Clasp::Solver::clearAssumptions | ( | ) |
Removes any implications made between the top-level and the root-level.
The function also resets the current backtrack-level and re-assigns learnt facts.
|
inline |
| void Clasp::Solver::clearStopConflict | ( | ) |
Removes a previously set stop conflict and restores the root level.
| const SolverParams & Clasp::Solver::configuration | ( | ) | const |
Returns the configuration for this object.
|
inline |
Returns the current conflict as a set of literals.
|
inline |
Returns the most recently derived conflict clause.
|
inline |
| void Clasp::Solver::copyGuidingPath | ( | LitVec & | out | ) |
Copies the solver's currrent guiding path to gp.
| [out] | gp | where to store the guiding path |
| bool Clasp::Solver::decideNextBranch | ( | double | f = 0.0 | ) |
Selects and assumes the next branching literal by calling the installed decision heuristic.
|
inline |
Returns the decision literal of the decision level dl.
|
inline |
Returns the current decision level.
| SharedLiterals * Clasp::Solver::distribute | ( | const Literal * | lits, |
| uint32 | size, | ||
| const ClauseInfo & | extra | ||
| ) |
Distributes the clause in lits via the distributor.
The function first calls the distribution strategy to decides whether the clause is a valid candidate for distribution. If so and a distributor was set, it distributes the clause and returns a handle to the now shared literals of the clause. Otherwise, it returns 0.
| owner | The solver that created the clause. |
| lits | The literals of the clause. |
| size | The number of literals in the clause. |
| extra | Additional information about the clause. |
|
inline |
Returns the enumeration constraint set by the enumerator used.
| uint32 Clasp::Solver::estimateBCP | ( | const Literal & | p, |
| int | maxRecursionDepth = 5 |
||
| ) | const |
Estimates the number of assignments following from setting p to true.
| uint32 Clasp::Solver::finalizeConflictClause | ( | LitVec & | cc, |
| ClauseInfo & | info, | ||
| uint32 | ccRepMode = 0 |
||
| ) |
|
inline |
Sets the literal p to true and schedules p for propagation.
Setting a literal p to true means assigning the appropriate value to p's variable. That is: value_false if p is a negative literal and value_true if p is a positive literal.
| p | The literal that should become true. |
| a | The reason for the literal to become true or 0 if no reason exists. |
This is an overloaded member function, provided for convenience. It differs from the above function only in what argument(s) it accepts.
|
inline |
|
inline |
Assigns p at dl because of r.
|
inline |
Assigns p as a fact at decision level 0.
|
inline |
|
inline |
Frees a small block previously allocated from the solver's small block pool.
|
inline |
|
inline |
|
inline |
Returns the idx'th learnt constraint.
| PostPropagator * Clasp::Solver::getPost | ( | uint32 | prio | ) | const |
Returns the post propagator with the given priority or 0 if no such post propagator exists.
| GenericWatch * Clasp::Solver::getWatch | ( | Literal | p, |
| Constraint * | c | ||
| ) | const |
Returns c's watch-structure associated with p.
|
inline |
Returns true, if the current assignment is conflicting.
|
inline |
|
inline |
| bool Clasp::Solver::hasWatch | ( | Literal | p, |
| Constraint * | c | ||
| ) | const |
Returns true if the constraint c watches the literal p.
| bool Clasp::Solver::hasWatch | ( | Literal | p, |
| ClauseHead * | c | ||
| ) | const |
|
inline |
|
inline |
|
inline |
| uint32 Clasp::Solver::inDegree | ( | WeightLitVec & | out | ) |
Computes the number of in-edges for each assigned literal.
|
inline |
Returns true if p is false w.r.t the current assignment.
|
inline |
Returns true if p is true w.r.t the current assignment.
|
inline |
Returns true if number of learnts exceeds x.learnts or the soft memory limit is exceeded.
|
inline |
Returns the decision level on which v was assigned.
|
inline |
Returns the starting position of decision level dl in the trail.
|
inline |
|
inline |
|
inline |
|
inline |
Returns the number of assigned variables.
|
inline |
Returns the number of active solver-local aux variables.
| uint32 Clasp::Solver::numConstraints | ( | ) | const |
Number of problem constraints in this solver.
|
inline |
Returns the number of free variables.
The number of free variables is the number of vars that are neither assigned nor eliminated.
|
inline |
Returns the number of constraints that are currently in the solver's learnt database.
|
inline |
Returns the number of problem variables.
|
inline |
Returns the number of solver variables, i.e. numProblemVars() + numAuxVars()
| uint32 Clasp::Solver::numWatches | ( | Literal | p | ) | const |
Returns the number of constraints watching the literal p.
| void Clasp::Solver::popAuxVar | ( | uint32 | num = UINT32_MAX | ) |
Pops the num most recently added auxiliary variables from this solver.
| bool Clasp::Solver::popRootLevel | ( | uint32 | i = 1, |
| LitVec * | popped = 0, |
||
| bool | aux = true |
||
| ) |
Moves the root-level i levels up (i.e. towards the top-level).
The function removes all levels between the new root level and the current decision level, resets the current backtrack-level, and re-assigns any implied literals.
| i | Number of root decisions to pop. | |
| [out] | popped | Optional storage for popped root decisions. |
| filter | Whether or not aux variables should be added to popped. |
Returns the set of preferred values of v.
| bool Clasp::Solver::propagate | ( | ) |
Propagates all enqueued literals. If a conflict arises during propagation propagate returns false and the current conflict (as a set of literals) is stored in the solver's conflict variable.
|
inline |
Does unit propagation and calls x->propagateFixpoint(*this) for all post propagators x up to but not including p.
| Var Clasp::Solver::pushAuxVar | ( | ) |
Adds a new auxiliary variable to this solver.
Auxiliary variables are local to one solver and are not considered as part of the problem. They shall be added/used only during solving, i.e. after problem setup is completed.
| bool Clasp::Solver::pushRoot | ( | const LitVec & | path | ) |
Adds path to the current root-path and adjusts the root-level accordingly.
| bool Clasp::Solver::pushRoot | ( | Literal | p | ) |
|
inline |
Moves the root-level i levels down (i.e. away from the top-level).
The root-level is similar to the top-level in that it cannot be undone during search, i.e. the solver will not resolve conflicts that are on or above the root-level.
| Var Clasp::Solver::pushTagVar | ( | bool | pushToRoot | ) |
Requests a special aux variable for tagging conditional knowledge.
Once a tag variable t is set, learnt clauses containing ~t are tagged as "conditional". Conditional clauses are removed once t becomes unassigned or Solver::removeConditional() is called. Furthermore, calling Solver::strengthenConditional() removes ~t from conditional clauses and transforms them to unconditional knowledge.
|
inline |
Returns the number of (unprocessed) literals in the propagation queue.
|
inline |
Returns the reason for p being true.
Returns the reason for p being true as a set of literals.
|
inline |
Returns the additional reason data associated with p.
| uint32 Clasp::Solver::receive | ( | SharedLiterals ** | out, |
| uint32 | maxOut | ||
| ) | const |
Tries to receive at most maxOut clauses.
The function queries the distributor object for new clauses to be delivered to this solver. Clauses are stored in out.
| Solver::DBInfo Clasp::Solver::reduceLearnts | ( | float | remMax, |
| const ReduceStrategy & | rs = ReduceStrategy() |
||
| ) |
Removes upto remMax percent of the learnt nogoods.
| remMax | Fraction of nogoods to remove ([0.0,1.0]). |
| rs | Strategy to apply during nogood deletion. |
| void Clasp::Solver::removeConditional | ( | ) |
Removes all conditional knowledge, i.e. all previously tagged learnt clauses.
|
inline |
Removes p from the solver's list of post propagators.
| bool Clasp::Solver::removeUndoWatch | ( | uint32 | dl, |
| Constraint * | c | ||
| ) |
Removes c from the watch-list of the decision level dl.
| void Clasp::Solver::removeWatch | ( | const Literal & | p, |
| Constraint * | c | ||
| ) |
Removes c from p's watch-list.
| void Clasp::Solver::removeWatch | ( | const Literal & | p, |
| ClauseHead * | c | ||
| ) |
|
inline |
Request additional reason data slot for variable v.
| bool Clasp::Solver::resolveConflict | ( | ) |
Resolves the active conflict using the selected strategy.
If the SearchStrategy is set to learning, resolveConflict implements First-UIP learning and backjumping. Otherwise, it simply applies chronological backtracking.
|
inline |
Returns to the maximum of rootLevel() and backtrackLevel() and increases the number of restarts.
|
inline |
Returns the current root level.
| SatPreprocessor * Clasp::Solver::satPrepro | ( | ) | const |
Returns a pointer to the sat-preprocessor used by this solver.
| ValueRep Clasp::Solver::search | ( | SearchLimits & | limit, |
| double | randf = 0.0 |
||
| ) |
Searches for a model as long as the given limit is not reached.
The search function implements the CDNL-algorithm. It searches for a model as long as none of the limits given by limit is reached. The limits are updated during search.
| limit | Imposed limit on conflicts and number of learnt constraints. |
| randf | Pick next decision variable randomly with a probability of randf. |
|
inline |
| const SolveParams & Clasp::Solver::searchConfig | ( | ) | const |
Returns the solve parameters for this object.
|
inline |
Returns true if v is currently marked as seen.
Note: variables assigned on level 0 are always marked.
|
inline |
Returns true if the literal p is currently marked as seen.
|
inline |
Sets the backtracking level to dl.
| void Clasp::Solver::setEnumerationConstraint | ( | Constraint * | c | ) |
|
inline |
|
inline |
Updates the reason for p being tue.
| void Clasp::Solver::setStopConflict | ( | ) |
Sets a conflict that forces the solver to terminate its search.
|
inline |
Returns a pointer to the shared context object of this solver.
|
inline |
Shuffle constraints upon next simplification.
| bool Clasp::Solver::simplify | ( | ) |
If called on top-level, removes SAT-clauses + Constraints for which Constraint::simplify returned true.
| uint32 Clasp::Solver::simplifyConflictClause | ( | LitVec & | cc, |
| ClauseInfo & | info, | ||
| ClauseHead * | rhs | ||
| ) |
simplifies cc and returns finalizeConflictClause(cc, info);
| bool Clasp::Solver::split | ( | LitVec & | out | ) |
Tries to split-off disjoint work from the solver's currrent guiding path and returns it in out.
| bool Clasp::Solver::splittable | ( | ) | const |
Returns whether the solver can split-off work.
| void Clasp::Solver::strengthenConditional | ( | ) |
Resolves all tagged clauses with the tag literal and thereby strengthens the learnt db.
|
inline |
|
inline |
Returns the set of eliminated literals that are unconstraint w.r.t the last model.
|
inline |
| bool Clasp::Solver::test | ( | Literal | p, |
| PostPropagator * | c | ||
| ) |
Executes a one-step lookahead on p.
Assumes p and propagates this assumption. If propagations leads to a conflict, false is returned. Otherwise the assumption is undone and the function returns true.
| p | The literal to test. |
| c | The constraint that wants to test p (can be 0). |
Returns the value of v w.r.t the top level.
|
inline |
Returns the current (partial) assignment as a set of true literals.
Returns the literal of v being true in the current assignment.
| void Clasp::Solver::undoUntil | ( | uint32 | dl | ) |
Undoes all assignments up to (but not including) decision level dl.
| uint32 Clasp::Solver::undoUntil | ( | uint32 | dl, |
| bool | popBtLevel | ||
| ) |
Similar to undoUntil but optionally also pops the backtrack-level to dl if possible.
|
inline |
|
inline |
|
inline |
Computes a new lbd for the antecedent of p given as the range [first, last).
| p | A literal implied by [first, last) |
| [first,last) | The literals of a learnt nogood implying p. |
| cLbd | The current lbd of the learnt nogood. |
|
inline |
|
inline |
Returns true if var represents a valid variable in this solver.
Returns the value of v w.r.t the current assignment.
|
friend |
| ValueVec Clasp::Solver::model |
Stores the last model (if any).
| RNG Clasp::Solver::rng |
Random number generator for this object.
| SolverStats Clasp::Solver::stats |
Stores statistics about the solving process.
| SolverStrategies Clasp::Solver::strategy |
Strategies used by this object.
1.8.7
