Extend the search with propagators for arbitrary theories. More...

Classes
class	Clingo::Trail
	A trail is a sequence of solver literals. More...

class	Clingo::Assignment
	Represents a (partial) assignment of a particular solver. More...

class	Clingo::PropagateControl
	Class to control a user-defined propagator. More...

class	Clingo::PropagateInit
	Object to initialize a user-defined propagator before each solving step. More...

class	Clingo::Propagator
	Interface for user-defined propagators. More...

class	Clingo::Heuristic
	Interface for user-defined propagators with a decision heuristic. More...

Enumerations
enum class	Clingo::PropagatorCheckMode : clingo_propagator_check_mode_t { PropagatorCheckMode::none = clingo_propagator_check_mode_none , PropagatorCheckMode::total = clingo_propagator_check_mode_total , PropagatorCheckMode::fixpoint = clingo_propagator_check_mode_fixpoint , PropagatorCheckMode::both = clingo_propagator_check_mode_both }
	Enumeration of propagator check modes. More...

enum class	Clingo::PropagatorUndoMode : clingo_propagator_undo_mode_t { PropagatorUndoMode::default_ = clingo_propagator_undo_mode_default , PropagatorUndoMode::always = clingo_propagator_undo_mode_always }
	Enumeration of propagator undo modes. More...

enum	Clingo::WeightConstraintType : clingo_weight_constraint_type_t { Clingo::implication_left = clingo_weight_constraint_type_implication_left , Clingo::implication_right = clingo_weight_constraint_type_implication_right , Clingo::equivalence = clingo_weight_constraint_type_equivalence }
	Enumeration of weight constraint types. More...

enum	Clingo::ClauseFlags : clingo_clause_type_t { Clingo::none = clingo_clause_type_learnt , Clingo::lock = clingo_clause_type_static , Clingo::tag = clingo_clause_type_volatile }
	Enumeration of clause flags. More...

Functions
	Clingo::CLINGO_ENABLE_BITSET_ENUM (ClauseFlags)
	Enable bitset enumeration for ClauseFlags.

Detailed Description

Extend the search with propagators for arbitrary theories.

Enumeration Type Documentation

Enumeration of clause flags.

Enumerator
none	The empty set of flags.
lock	Exempt the clause from deletion.
tag	Delete the clause at the end of the current solving step.

strong

Enumeration of propagator check modes.

Enumerator
none	Do not call check at all.
total	Call check on total assignments.
fixpoint	Call check on propagation fixpoints.
both	Call check on propagation fixpoints and total assignments.

strong

Enumeration of propagator undo modes.

Enumerator
default_	Call undo for non-empty change lists.
always	Also call undo for empty change lists.

Enumeration of weight constraint types.

Enumerator
implication_left	The weight constraint implies the literal.
implication_right	The literal implies the weight constraint.
equivalence	The weight constraint is equivalent to the literal.