Class ComponentManager¶
- Defined in File component_management.h
Class Documentation¶
-
class
ComponentManager
¶ Public Functions
-
ComponentManager
(SolverConfiguration &config, DataAndStatistics &statistics, LiteralIndexedVector<TriValue> &lit_values)¶
-
void
initialize
(LiteralIndexedVector<Literal> &literals, std::vector<LiteralID> &lit_pool, bool quiet = false)¶ Initializes the cache, component stack, and component analyzer.
component_management.cpp
- Parameters
literals
: Set of valid literalslit_pool
:quiet
: Quiet parameter used to set whether console printing is enabled.
Purpose: Defines methods for the ComponentManagement() class.
Copyright (C) 2018 Zayd Hammoudeh. All rights reserved.
- Author
- Zayd Hammoudeh zayd@ucsc.edu
- Version
- 0.00.00
This software may be modified and distributed under the terms of the MIT license. See the LICENSE file for details.
Original Author: Marc Thurley.
-
unsigned
scoreOf
(VariableIndex v)¶
-
void
cacheModelCountOf
(VariableIndex stack_comp_id, const mpz_class &value)¶ Cache Model Count Storer
If caching is enabled, this method stores the model count of the component onto the stack.
- Parameters
stack_comp_id
: Component ID of the stack elementvalue
: Model count of the element
-
void
cacheModelCountAndAssignment
(const VariableIndex stack_comp_id, const mpz_class &value, const SampleAssignment &assn, const Component &component)¶ Cache Model Count and Assignment Encoder and Storer
Prepend the component’s MPZ value with the sample assignment.
- Parameters
stack_comp_id
: Component ID of the stack element.value
: Model countassn
: Sample assignment to encode in the cache with the model count.component
: Actual component to get the variables.
-
Component &
superComponentOf
(StackLevel &lev)¶ Gets a pointer to the actual super component that corresponds to passed stack level.
- Return
- Pointer to the super component of the stack item.
- Parameters
lev
: Level in the stack whose super component will be extracted
-
const Component &
super_component
(StackLevel &lev) const¶ Const version of the superComponentOf() method.
- Return
- Pointer to the super component of the stack item.
- Parameters
lev
: Level in the stack whose super component will be extracted
-
VariableIndex
component_stack_size
() const¶ Extracts the number of components currently in the component stack.
- Return
- Number of element in teh component stack.
-
void
cleanRemainingComponentsOf
(StackLevel &top)¶
-
bool
findNextRemainingComponentOf
(StackLevel &top, const std::vector<LiteralID> &literal_stack, SamplesManager &samples)¶ Checks for the next yet to explore remaining component of top returns true if a non-trivial non-cached component has been found and is now stack_.TOS_NextComp() returns false if all components have been processed;
This function has been modified to support sampling. That includes passing the parameter “literal_stack”. This is neeeded to build samples.
- Return
- true if unprocessed components remain.
- Parameters
top
: Top of the decision stack.literal_stack_
: Current assigned literal stack.samples
: Current reservoir sample set.
-
void
recordRemainingCompsFor
(StackLevel &top, const std::vector<LiteralID> &literal_stack)¶ Examines the top of the decision stack. The function will try to decompose the component if applicable. For any new component, the function will check if the new components exists in the cache; if it does, the results are used to update the super component.
Otherwise, the new component is added to the component stack (not the decision stack). The end of unprocessed components is also updated.
Component at the top of the stack is analyzed. If a new and unseen component has never been seen, then the new component is placed on the component stack.
- Parameters
top
: Element at the top of the decision stack.literal_stack
: Current assigned literal stack.
The component stack is then sorted so components with fewer variables are at the top of the stack.
- Parameters
top
: Element at the top of the decision stack.literal_stack_
: Current assigned literal stack.
-
void
buildResidualComponent
(StackLevel &top)¶ Build residual formula component. It uses the contents of the literal stack to decide how to construct remaining components.
- Parameters
top
: Element at the top of the decision stack.
-
Component *
top_stack
()¶ Accessor for the top of the component stack.
- Return
- Pointer to the component on top of the component stack.
-
void
sortComponentStackRange
(unsigned long start, unsigned long end)¶ Sorts the components stack from start (inclusive) to end (exclusive). The components with more variables are placed lower on the stack (i.e., further from the top) and processed later.
- Parameters
start
: Start of component stack to be sorted (inclusive)end
: End of the component stack to sort (exclusive)
-
void
gatherStatistics
()¶
-
void
removeAllCachePollutionsOf
(StackLevel &top)¶
-
std::vector<VariableIndex>
buildFreedVariableList
(const StackLevel &top, const std::vector<LiteralID> &literal_stack)¶ Freed Variable List Builder
When assigning variables in a formula it is common that some variables become free (i.e., no longer appear in any of the clauses). These free variables will not appear on the literal stack but must be tracked to create the sample. This function stores all such freed variables.
- Return
- Vector of the variable indexes of all freed variables
- Parameters
literal_stack
: Current literal stack
-