operations_research::sat::ProductPropagator Class Reference

#include <integer_expr.h>

Inheritance diagram for operations_research::sat::ProductPropagator:

Public Member Functions
	ProductPropagator (AffineExpression a, AffineExpression b, AffineExpression p, IntegerTrail *integer_trail)
	ProductPropagator (const ProductPropagator &)=delete
	This type is neither copyable nor movable.
ProductPropagator &	operator= (const ProductPropagator &)=delete
bool	Propagate () final
void	RegisterWith (GenericLiteralWatcher *watcher)
Public Member Functions inherited from operations_research::sat::PropagatorInterface
	PropagatorInterface ()=default
virtual	~PropagatorInterface ()=default
virtual bool	IncrementalPropagate (const std::vector< int > &)

Detailed Description

Propagates a * b = p.

The bounds [min, max] of a and b will be propagated perfectly, but not the bounds on p as this require more complex arithmetics.

Definition at line 283 of file integer_expr.h.

Constructor & Destructor Documentation

ProductPropagator() [1/2]

operations_research::sat::ProductPropagator::ProductPropagator	(	AffineExpression	a,
		AffineExpression	b,
		AffineExpression	p,
		IntegerTrail *	integer_trail )

Definition at line 847 of file integer_expr.cc.

ProductPropagator() [2/2]

operations_research::sat::ProductPropagator::ProductPropagator ( const ProductPropagator & )

delete

This type is neither copyable nor movable.

Member Function Documentation

operator=()

ProductPropagator & operations_research::sat::ProductPropagator::operator= ( const ProductPropagator & )

delete

Propagate()

bool operations_research::sat::ProductPropagator::Propagate ( )

finalvirtual

This will be called after one or more literals that are watched by this propagator changed. It will also always be called on the first propagation cycle after registration.

In the most common case, we use better reasons even though the code below would propagate the same.

This was done by CanonicalizeCases().

Lets propagate on p_ first, the max/min is given by one of: max_a * max_b, max_a * min_b, min_a * max_b, min_a * min_b. This is true, because any product x * y, depending on the sign, is dominated by one of these.

Todo

(user): In the reasons, including all 4 bounds is always correct, but we might be able to relax some of them.

Lets propagate on a and b.

We need a bit more propagation to avoid bad cases below.

p = a * b, what is the min/max of a?

If the domain of b contain zero, we can't propagate anything on a. Because of CanonicalizeCases(), we just deal with min_b > 0 here.

Here both a and b are across zero, but zero is not possible.

If a is not across zero, we will deal with this on the next Propagate() call.

This shouldn't happen here. If it does, we should reach the fixed point on the next iteration.

So min_b > 0 and p is across zero: min_p < 0 and max_p > 0.

Implements operations_research::sat::PropagatorInterface.

Definition at line 1007 of file integer_expr.cc.

RegisterWith()

void operations_research::sat::ProductPropagator::RegisterWith

(

GenericLiteralWatcher *

watcher

)

Definition at line 1151 of file integer_expr.cc.

---

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

• ortools/sat/integer_expr.h
• ortools/sat/integer_expr.cc