#include <integer.h>

Inheritance diagram for operations_research::sat::LazyReasonInterface:

Public Member Functions
	LazyReasonInterface ()=default

virtual	~LazyReasonInterface ()=default

virtual void	Explain (int id, IntegerValue propagation_slack, IntegerVariable var_to_explain, int trail_index, std::vector< Literal > literals_reason, std::vector< int > trail_indices_reason)=0

Detailed Description

Definition at line 750 of file integer.h.

Constructor & Destructor Documentation

◆ LazyReasonInterface()

operations_research::sat::LazyReasonInterface::LazyReasonInterface ( )

default

◆ ~LazyReasonInterface()

virtual operations_research::sat::LazyReasonInterface::~LazyReasonInterface ( )

virtualdefault

Member Function Documentation

◆ Explain()

virtual void operations_research::sat::LazyReasonInterface::Explain	(	int	id,
		IntegerValue	propagation_slack,
		IntegerVariable	var_to_explain,
		int	trail_index,
		std::vector< Literal > *	literals_reason,
		std::vector< int > *	trail_indices_reason )

pure virtual

When called, this must fill the two vectors so that literals contains any Literal part of the reason and dependencies contains the trail index of any IntegerLiteral that is also part of the reason.

Remark: integer_literal[trail_index] might not exist or has nothing to do with what was propagated.

Todo: (user): {id, propagation_slack, var_to_explain, trail_index} is just a generic "payload" and we should probably rename it as such so that each implementation can store different things.

Implemented in operations_research::sat::GreaterThanAtLeastOneOfPropagator, operations_research::sat::LinearConstraintPropagator< use_int128 >, operations_research::sat::LinearPropagator, and operations_research::sat::LinMinPropagator.

The documentation for this class was generated from the following file: