MsmStrategy Class Reference

`#include <MsmStrategy.h>`

Inheritance diagram for MsmStrategy:

## Public Member Functions

| MsmStrategy (TermConsumer *consumer, const SplitStrategy *splitStrategy)
| MsmStrategy (TermConsumer *consumer, const SplitStrategy *splitStrategy, const Ideal &initialSubtract)
virtual void | run (const Ideal &ideal)
| Run the Slice algorithm.
virtual bool | processSlice (TaskEngine &tasks, unique_ptr< Slice > slice)
| Process the parameter slice.
Public Member Functions inherited from SliceStrategyCommon
| SliceStrategyCommon (const SplitStrategy *splitStrategy)
virtual | ~SliceStrategyCommon ()
virtual void | freeSlice (unique_ptr< Slice > slice)
| It is allowed to delete returned slices directly, but it is better to use freeSlice.
virtual void | setUseIndependence (bool use)
| This method should only be called before calling run().
virtual void | setUseSimplification (bool use)
| This method should only be called before calling run().
Public Member Functions inherited from SliceStrategy
virtual | ~SliceStrategy ()

## Protected Member Functions

virtual void | getPivot (Term &pivot, Slice &slice)
| Used by pivotSplit to obtain a pivot.
virtual void | getPivot (Term &pivot, Slice &slice, const TermGrader &grader)
Protected Member Functions inherited from SliceStrategyCommon
virtual bool | simplify (Slice &slice)
| Simplifies slice and returns true if it changed.
unique_ptr< Slice > | newSlice ()
| Returns a slice from the cache that freeSlice adds to, or allocate a new one using allocateSlice.
virtual void | pivotSplit (unique_ptr< Slice > slice)
| Takes over ownership of slice.
bool | getUseIndependence () const
| Returns true if independence splits should be performed when possible.
bool | getUseSimplification () const
| Returns true if slices should be simplified.

## Private Member Functions

unique_ptr< MsmSlice > | newMsmSlice ()
virtual unique_ptr< Slice > | allocateSlice ()
| Directly allocate a slice of the correct type using new.
virtual bool | debugIsValidSlice (Slice *slice)
| Check that this slice is valid for use with this strategy.
void | labelSplit (unique_ptr< Slice > slice)
void | independenceSplit (unique_ptr< Slice > slice)
size_t | getLabelSplitVariable (const Slice &slice)

## Private Attributes

IndependenceSplitter | _indep
TermConsumer * | _consumer
unique_ptr< Ideal > | _initialSubtract

## Additional Inherited Members

Protected Attributes inherited from SliceStrategyCommon
const SplitStrategy * | _split
TaskEngine | _tasks
| This keeps track of pending tasks to process.

## Detailed Description

Definition at line 37 of file MsmStrategy.h.

## Constructor & Destructor Documentation

## MsmStrategy() [1/2]

MsmStrategy::MsmStrategy | ( | TermConsumer * | consumer,
|  | const SplitStrategy * | splitStrategy )

Definition at line 28 of file MsmStrategy.cpp.

## MsmStrategy() [2/2]

MsmStrategy::MsmStrategy | ( | TermConsumer * | consumer,
|  | const SplitStrategy * | splitStrategy,
|  | const Ideal & | initialSubtract )

Definition at line 35 of file MsmStrategy.cpp.

## Member Function Documentation

## allocateSlice()

unique_ptr< Slice > MsmStrategy::allocateSlice | ( |  | ) |

private virtual

Directly allocate a slice of the correct type using new.

Implements SliceStrategyCommon.

Definition at line 93 of file MsmStrategy.cpp.

## debugIsValidSlice()

bool MsmStrategy::debugIsValidSlice | ( | Slice * | slice | ) |

private virtual

Check that this slice is valid for use with this strategy.

No check need be performed unless DEBUG is defined, making it acceptable to check things using ASSERT. This method should not be called if DEBUG is not defined.

Implements SliceStrategyCommon.

Definition at line 97 of file MsmStrategy.cpp.

## getLabelSplitVariable()

size_t MsmStrategy::getLabelSplitVariable | ( | const Slice & | slice | ) |

private

## getPivot() [1/2]

void MsmStrategy::getPivot | ( | Term & | pivot,
|  | Slice & | slice )

protected virtual

Used by pivotSplit to obtain a pivot.

Implements SliceStrategyCommon.

Reimplemented in OptimizeStrategy.

Definition at line 285 of file MsmStrategy.cpp.

## getPivot() [2/2]

void MsmStrategy::getPivot | ( | Term & | pivot,
|  | Slice & | slice,
|  | const TermGrader & | grader )

protected virtual

Definition at line 292 of file MsmStrategy.cpp.

## independenceSplit()

void MsmStrategy::independenceSplit | ( | unique_ptr< Slice > | slice | ) |

private

Definition at line 258 of file MsmStrategy.cpp.

## labelSplit()

void MsmStrategy::labelSplit | ( | unique_ptr< Slice > | slice | ) |

private

Definition at line 103 of file MsmStrategy.cpp.

## newMsmSlice()

unique_ptr< MsmSlice > MsmStrategy::newMsmSlice | ( |  | ) |

private

Definition at line 87 of file MsmStrategy.cpp.

## processSlice()

bool MsmStrategy::processSlice | ( | TaskEngine & | tasks,
|  | unique_ptr< Slice > | slice )

virtual

Process the parameter slice.

Returns true if this is a base case and false otherwise.

Implements SliceStrategy.

Definition at line 67 of file MsmStrategy.cpp.

## run()

void MsmStrategy::run | ( | const Ideal & | ideal | ) |

virtual

Run the Slice algorithm.

Implements SliceStrategy.

Definition at line 44 of file MsmStrategy.cpp.

## Member Data Documentation

## _consumer

TermConsumer* MsmStrategy::_consumer

private

Definition at line 63 of file MsmStrategy.h.

## _indep

IndependenceSplitter MsmStrategy::_indep

private

Definition at line 62 of file MsmStrategy.h.

## _initialSubtract

unique_ptr<Ideal> MsmStrategy::_initialSubtract

private

Definition at line 65 of file MsmStrategy.h.

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

- src/MsmStrategy.h
- src/MsmStrategy.cpp