Public Member Functions
	ContractorStatus (Box box, int branching_point=-1)
	Constructs a contractor status with `box` and `branching_point`.

const Box &	box () const
	Returns a const reference of the embedded box.

Box &	mutable_box ()
	Returns a mutable reference of the embedded box.

int	branching_point () const
	Returns the branching_point.

int &	mutable_branching_point ()
	Returns a mutable reference of the branching_point.

const DynamicBitset &	output () const
	Returns a const reference of the output field.

DynamicBitset &	mutable_output ()
	Returns a mutable reference of the output field.

std::set< Formula >	Explanation () const
	Returns explanation, a list of formula responsible for the unsat.

void	AddUsedConstraint (const Formula &f)
	Add a formula `f` into the used constraints.

void	AddUsedConstraint (const std::vector< Formula > &formulas)
	Add a formula `formulas` into the used constraints.

void	AddUnsatWitness (const Variable &var)
	Add a variable `var` which is directly responsible for the unsat.

ContractorStatus &	InplaceJoin (const ContractorStatus &contractor_status)
	Updates the contractor status by taking join with `contractor_status`. More...

Detailed Description

Member Function Documentation

ContractorStatus & InplaceJoin ( const ContractorStatus & contractor_status )

Updates the contractor status by taking join with contractor_status.

Precondition: The boxes of this and contractor_status have the same variables vector.

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