Class ComponentManager

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 literals
  • lit_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 element
  • value: 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 count
  • assn: 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)
const Component &component(unsigned long comp_idx) const

Return
Parameters
  • comp_idx:

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