Public Types
enum	Kind { ID, INTEGER, SEQ, IBEX_FWDBWD, IBEX_POLYTOPE, FIXPOINT, WORKLIST_FIXPOINT, FORALL, JOIN }

Public Member Functions
	Contractor (const Config &config)

	Contractor (const Contractor &)=default
	Default copy constructor.

	Contractor (Contractor &&)=default
	Default move constructor.

Contractor &	operator= (const Contractor &)=default
	Default copy assign operator.

Contractor &	operator= (Contractor &&)=default
	Default move assign operator.

	~Contractor ()=default
	Default destructor.

const DynamicBitset &	input () const
	Returns the input vector of this contractor. More...

void	Prune (ContractorStatus *cs) const
	Prunes `cs`.

Kind	kind () const
	Returns kind.

bool	include_forall () const
	Returns true if this contractor includes a forall contractor.

void	set_include_forall ()
	Sets include_forall true.

Friends
std::ostream &	operator<< (std::ostream &os, Contractor const &ctc)

Contractor	make_contractor_id (const Config &config)
	Returns an idempotent contractor. More...

Contractor	make_contractor_integer (const Box &box, const Config &config)
	Returns an integer contractor. More...

Contractor	make_contractor_seq (const std::vector< Contractor > &contractors, const Config &config)
	Returns a sequential contractor `C` from a vector of contractors `vec` = [C₁, ..., Cₙ]. More...

Contractor	make_contractor_ibex_fwdbwd (Formula f, const Box &box, const Config &config)
	Returns a contractor wrapping IBEX's forward/backward contractor. More...

Contractor	make_contractor_ibex_polytope (std::vector< Formula > formulas, const Box &box, const Config &config)
	Returns a contractor wrapping IBEX's polytope contractor. More...

Contractor	make_contractor_fixpoint (TerminationCondition term_cond, const std::vector< Contractor > &contractors, const Config &config)
	Returns a fixed-point contractor. More...

Contractor	make_contractor_worklist_fixpoint (TerminationCondition term_cond, const std::vector< Contractor > &contractors, const Config &config)
	Returns a worklist fixed-point contractor. More...

template<typename ContextType >
Contractor	make_contractor_forall (Formula f, const Box &box, double epsilon, double inner_delta, const Config &config)
	Returns a forall contractor. More...

Contractor	make_contractor_join (std::vector< Contractor > vec, const Config &config)
	Returns a join contractor. More...

std::shared_ptr< ContractorId >	to_id (const Contractor &contractor)
	Converts `contractor` to ContractorId.

std::shared_ptr< ContractorInteger >	to_integer (const Contractor &contractor)
	Converts `contractor` to ContractorInteger.

std::shared_ptr< ContractorSeq >	to_seq (const Contractor &contractor)
	Converts `contractor` to ContractorSeq.

std::shared_ptr< ContractorIbexFwdbwd >	to_ibex_fwdbwd (const Contractor &contractor)
	Converts `contractor` to ContractorIbexFwdbwd.

std::shared_ptr< ContractorIbexPolytope >	to_ibex_polytope (const Contractor &contractor)
	Converts `contractor` to ContractorIbexPolytop.

std::shared_ptr< ContractorFixpoint >	to_fixpoint (const Contractor &contractor)
	Converts `contractor` to ContractorFixpoint.

std::shared_ptr< ContractorWorklistFixpoint >	to_worklist_fixpoint (const Contractor &contractor)
	Converts `contractor` to ContractorWorklistFixpoint.

std::shared_ptr< ContractorJoin >	to_join (const Contractor &contractor)
	Converts `contractor` to ContractorJoin.

template<typename ContextType >
std::shared_ptr< ContractorForall< ContextType > >	to_forall (const Contractor &contractor)
	Converts `contractor` to ContractorForall.

Member Function Documentation

◆ input()

const DynamicBitset & input ( ) const

Returns the input vector of this contractor.

input()[i] = true means that this contractor depends on the value of box[i].

Friends And Related Function Documentation

◆ make_contractor_fixpoint

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

friend

Returns a fixed-point contractor.

The returned contractor applies the contractors in vec sequentially until term_cond is met.

See also: ContractorFixpoint.

◆ make_contractor_forall

Contractor make_contractor_forall	(	Formula	f,
		const Box &	box,
		double	epsilon,
		double	inner_delta,
		const Config &	config
	)

friend

Returns a forall contractor.

Note: the implementation is at dreal/contractor/contractor_forall.h file.

See also: ContractorForall.

◆ make_contractor_ibex_fwdbwd

Contractor make_contractor_ibex_fwdbwd	(	Formula	f,
		const Box &	box,
		const Config &	config
	)

friend

Returns a contractor wrapping IBEX's forward/backward contractor.

If the number of jobs (in config) > 1, it creates a multi-threaded version of the contractor, which is based on ContractorIbexFwdbwdMt. Otherwise, it creates an instance of ContractorIbexFwdbwd.

See also: ContractorIbexFwdbwd.; ContractorIbexFwdbwdMt.

◆ make_contractor_ibex_polytope

Contractor make_contractor_ibex_polytope	(	std::vector< Formula >	formulas,
		const Box &	box,
		const Config &	config
	)

friend

Returns a contractor wrapping IBEX's polytope contractor.

If then number of jobs (in config) > 1, it creates a multi-threaded version of the contractor, which is based on ContractorIbexPolytopeMt. Otherwise, it creates an instance of ContractorIbexPolytope.

See also: ContractorIbexPolytope.; ContractorIbexPolytopeMt.

◆ make_contractor_id

Contractor make_contractor_id ( const Config & config )

friend

Returns an idempotent contractor.

See also: ContractorId.

◆ make_contractor_integer

Contractor make_contractor_integer	(	const Box &	box,
		const Config &	config
	)

friend

Returns an integer contractor.

For an integer variable v, it prunes b[v] = [lb, ub] into [ceil(lb), floor(ub)]. It sets the box empty if it detects an empty interval in pruning.

See also: ContractorInteger.

◆ make_contractor_join

Contractor make_contractor_join	(	std::vector< Contractor >	vec,
		const Config &	config
	)

friend

Returns a join contractor.

The returned contractor does the following operation:

    (C₁ ∨ ... ∨ Cₙ)(box) = C₁(box) ∨ ... ∨ Cₙ(box).

See also: ContractorJoin.

◆ make_contractor_seq

Contractor make_contractor_seq	(	const std::vector< Contractor > &	contractors,
		const Config &	config
	)

friend

Returns a sequential contractor C from a vector of contractors vec = [C₁, ..., Cₙ].

It applies Cᵢ sequentially. That is, we have:

    C(box) = (Cₙ∘...∘C₁)(box)

See also: ContractorSeq.

◆ make_contractor_worklist_fixpoint

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

friend

Returns a worklist fixed-point contractor.

The returned contractor applies the contractors in vec sequentially until term_cond is met.

See also: ContractorFixpoint.

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

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

Public Types

Public Member Functions

Friends

Member Function Documentation

◆ input()

Friends And Related Function Documentation

◆ make_contractor_fixpoint

◆ make_contractor_forall

◆ make_contractor_ibex_fwdbwd

◆ make_contractor_ibex_polytope

◆ make_contractor_id

◆ make_contractor_integer

◆ make_contractor_join

◆ make_contractor_seq

◆ make_contractor_worklist_fixpoint