Class for Parallel ICP (Interval Constraint Propagation) algorithm. More...

Inheritance diagram for IcpParallel:

Public Member Functions
	IcpParallel (const Config &config)
	Constructs an IcpParallel based on `config`.

bool	CheckSat (const Contractor &contractor, const std::vector< FormulaEvaluator > &formula_evaluators, ContractorStatus *cs) override
	Checks the delta-satisfiability of the current assertions. More...

Public Member Functions inherited from Icp
	Icp (const Config &config)
	Constructs an Icp based on `config`.

	Icp (const Icp &)=default

	Icp (Icp &&)=default

Icp &	operator= (const Icp &)=delete

Icp &	operator= (Icp &&)=delete

Additional Inherited Members
Protected Member Functions inherited from Icp
const Config &	config () const

Detailed Description

Class for Parallel ICP (Interval Constraint Propagation) algorithm.

Member Function Documentation

bool CheckSat	(	const Contractor &	contractor,
		const std::vector< FormulaEvaluator > &	formula_evaluators,
		ContractorStatus *	cs
	)

overridevirtual

Checks the delta-satisfiability of the current assertions.

Parameters

[in]	contractor	Contractor to use in pruning phase
[in]	formula_evaluators	A vector of FormulaEvaluator which determines when to stop and which dimension to branch.
[in,out]	cs	A contractor to be updated. Returns true if it's delta-SAT. Returns false if it's UNSAT.

Implements Icp.

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