Fixpoint contractor using the worklist algorithm: apply C₁, ..., Cₙ until it reaches a fixpoint or it satisfies a given termination condition. More...
#include </home/soonhokong/work/dreal4/dreal/contractor/contractor_worklist_fixpoint.h>
Public Member Functions | |
| ContractorWorklistFixpoint ()=delete | |
| Deletes default constructor. | |
| ContractorWorklistFixpoint (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... | |
| ContractorWorklistFixpoint (const ContractorWorklistFixpoint &)=delete | |
| Deleted copy constructor. | |
| ContractorWorklistFixpoint (ContractorWorklistFixpoint &&)=delete | |
| Deleted move constructor. | |
| ContractorWorklistFixpoint & | operator= (const ContractorWorklistFixpoint &)=delete |
| Deleted copy assign operator. | |
| ContractorWorklistFixpoint & | operator= (ContractorWorklistFixpoint &&)=delete |
| Deleted move assign operator. | |
| ~ContractorWorklistFixpoint () override=default | |
| Default destructor. | |
| void | Prune (ContractorStatus *cs) const override |
| Q : list of contractors Ctc : list of all contractors. More... | |
| 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 using the worklist algorithm: apply C₁, ..., Cₙ until it reaches a fixpoint or it satisfies a given termination condition.
Constructor & Destructor Documentation
◆ ContractorWorklistFixpoint()
| ContractorWorklistFixpoint | ( | TerminationCondition | term_cond, |
| std::vector< Contractor > | contractors, | ||
| const Config & | config | ||
| ) |
Member Function Documentation
◆ Prune()
|
overridevirtual |
Q : list of contractors Ctc : list of all contractors.
Need to fill Q using "branched dimensions"
If branched_dimension = -1: Q.push(Ctc) else: Q.push(ctc ∣ ctc ∈ Ctc ∧ branched_dimension ∈ ctc.input())
while ¬Q.empty() ∧ ¬TermCond(b, b'): ctc : contractor ← Q.pop_front(); b' : box ← ctc.prune(b) output : set of integers ← ctc.output() for i in output: Q.push({ctc ∣ ctc ∈ Ctc ∧ i ∈ ctc.input()})
Implements ContractorCell.
The documentation for this class was generated from the following files:
- /home/soonhokong/work/dreal4/dreal/contractor/contractor_worklist_fixpoint.h
- /home/soonhokong/work/dreal4/dreal/contractor/contractor_worklist_fixpoint.cc
