Stores temporaries used to build or manipulate a CutData. More...

#include <cuts.h>

Public Member Functions
void	ClearIndices ()

void	AddOrMergeTerm (const CutTerm &term, IntegerValue t, CutData *cut)

void	ClearNumMerges ()

int	NumMergesSinceLastClear () const

bool	ConvertToLinearConstraint (const CutData &cut, LinearConstraint *output)
	Returns false if we encounter an integer overflow.

Detailed Description

Stores temporaries used to build or manipulate a CutData.

Definition at line 151 of file cuts.h.

Member Function Documentation

◆ AddOrMergeTerm()

void operations_research::sat::CutDataBuilder::AddOrMergeTerm	(	const CutTerm &	term,
		IntegerValue	t,
		CutData *	cut )

If the referred var is not right, replace the entry.

If the sign is not right, look into secondary hash_map for opposite sign.

If the referred var is not right, replace the entry.

If the sign is not right, replace the entry.

We can only merge the term if term.coeff + old_coeff do not overflow and if t * new_coeff do not overflow.

If we cannot merge the term, we will keep them separate. The produced cut will be less strong, but can still be used.

If we cannot merge the term, we keep them separate.

Definition at line 294 of file cuts.cc.

◆ ClearIndices()

void operations_research::sat::CutDataBuilder::ClearIndices ( )

These function allow to merges entries corresponding to the same variable and complementation. That is (X - lb) and (ub - X) are NOT merged and kept as separate terms. Note that we currently only merge Booleans since this is the only case we need.

Definition at line 273 of file cuts.cc.

◆ ClearNumMerges()

void operations_research::sat::CutDataBuilder::ClearNumMerges ( )

inline

Definition at line 160 of file cuts.h.

◆ ConvertToLinearConstraint()

bool operations_research::sat::CutDataBuilder::ConvertToLinearConstraint	(	const CutData &	cut,
		LinearConstraint *	output )

Returns false if we encounter an integer overflow.

Todo: (user): Divide by gcd first to avoid possible overflow in the conversion? it is however unlikely given that our coeffs should be small.

Definition at line 364 of file cuts.cc.

◆ NumMergesSinceLastClear()

int operations_research::sat::CutDataBuilder::NumMergesSinceLastClear ( ) const