|
Frobby 0.9.6
|
#include <MsmStrategy.h>
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. | |
Definition at line 37 of file MsmStrategy.h.
| MsmStrategy::MsmStrategy | ( | TermConsumer * | consumer, |
| const SplitStrategy * | splitStrategy | ||
| ) |
Definition at line 28 of file MsmStrategy.cpp.
| MsmStrategy::MsmStrategy | ( | TermConsumer * | consumer, |
| const SplitStrategy * | splitStrategy, | ||
| const Ideal & | initialSubtract | ||
| ) |
Definition at line 35 of file MsmStrategy.cpp.
|
privatevirtual |
Directly allocate a slice of the correct type using new.
Implements SliceStrategyCommon.
Definition at line 93 of file MsmStrategy.cpp.
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.
Used by pivotSplit to obtain a pivot.
Implements SliceStrategyCommon.
Reimplemented in OptimizeStrategy.
Definition at line 285 of file MsmStrategy.cpp.
|
protectedvirtual |
Definition at line 292 of file MsmStrategy.cpp.
|
private |
Definition at line 258 of file MsmStrategy.cpp.
|
private |
Definition at line 103 of file MsmStrategy.cpp.
|
private |
Definition at line 87 of file MsmStrategy.cpp.
|
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.
|
private |
Definition at line 63 of file MsmStrategy.h.
|
private |
Definition at line 62 of file MsmStrategy.h.
|
private |
Definition at line 65 of file MsmStrategy.h.