Icp Class Reference

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

#include </home/soonhokong/work/dreal4/dreal/solver/icp.h>

Inheritance diagram for Icp:

Public Member Functions
	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
virtual bool	CheckSat (const Contractor &contractor, const std::vector< FormulaEvaluator > &formula_evaluators, ContractorStatus *cs)=0
	Checks the delta-satisfiability of the current assertions. More...

Protected Member Functions
const Config &	config () const

Detailed Description

Abstract Class for ICP (Interval Constraint Propagation) algorithm.

Member Function Documentation

CheckSat()

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

pure virtual

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.

Implemented in IcpParallel, and IcpSeq.

---

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

• /home/soonhokong/work/dreal4/dreal/solver/icp.h
• /home/soonhokong/work/dreal4/dreal/solver/icp.cc