ContractorFixpoint Class Reference

Fixpoint contractor: apply C₁, ..., Cₙ until it reaches a fixpoint (technically, until it satisfies a given termination condition). More...

#include </home/soonhokong/work/dreal4/dreal/contractor/contractor_fixpoint.h>

Inheritance diagram for ContractorFixpoint:

Public Member Functions
	ContractorFixpoint ()=delete
	Deletes default constructor.
	ContractorFixpoint (TerminationCondition term_cond, std::vector< Contractor > contractors, const Config &config)
	Constructs a fixpoint contractor with a termination condition (Box × Box → Bool) and a sequence of Contractors {C₁, ..., Cₙ}. More...
	ContractorFixpoint (const ContractorFixpoint &)=delete
	Deleted copy constructor.
	ContractorFixpoint (ContractorFixpoint &&)=delete
	Deleted move constructor.
ContractorFixpoint &	operator= (const ContractorFixpoint &)=delete
	Deleted copy assign operator.
ContractorFixpoint &	operator= (ContractorFixpoint &&)=delete
	Deleted move assign operator.
	~ContractorFixpoint () override=default
	Default destructor.
void	Prune (ContractorStatus *cs) const override
	Performs pruning on cs.
std::ostream &	display (std::ostream &os) const override
	Outputs this contractor to os.
Public Member Functions inherited from ContractorCell
	ContractorCell (Contractor::Kind kind, DynamicBitset input, Config config)
	Constructs a cell with kind and input.
	ContractorCell ()=delete
	Deleted default constructor.
	ContractorCell (const ContractorCell &)=delete
	Deleted copy constructor.
	ContractorCell (ContractorCell &&)=delete
	Deleted move constructor.
void	operator= (const ContractorCell &)=delete
	Deleted copy assign operator.
void	operator= (ContractorCell &&)=delete
	Deleted move assign operator.
virtual	~ContractorCell ()=default
	Default destructor.
Contractor::Kind	kind () const
	Returns its kind.
const DynamicBitset &	input () const
	Returns its input.
DynamicBitset &	mutable_input ()
	Returns its input.
const Config &	config () const
	Returns config.
bool	include_forall () const
	Returns true if this contractor includes a forall contractor.
void	set_include_forall ()
	Sets include_forall true.

Detailed Description

Fixpoint contractor: apply C₁, ..., Cₙ until it reaches a fixpoint (technically, until it satisfies a given termination condition).

Constructor & Destructor Documentation

ContractorFixpoint()

ContractorFixpoint	(	TerminationCondition	term_cond,
		std::vector< Contractor >	contractors,
		const Config &	config
	)

Constructs a fixpoint contractor with a termination condition (Box × Box → Bool) and a sequence of Contractors {C₁, ..., Cₙ}.

---

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

• /home/soonhokong/work/dreal4/dreal/contractor/contractor_fixpoint.h
• /home/soonhokong/work/dreal4/dreal/contractor/contractor_fixpoint.cc