Class StackLevel¶

Defined in File stack.h

Class Documentation¶

class StackLevel¶

stack.h

Purpose: Defines the StackLevel() class that encapsulates a single level in the decision stack. The decision stack itself is stored in the DecisionStack() class.

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. Represents a single level in the decision stack.

Public Functions

bool hasUnprocessedComponents() const¶

void nextUnprocessedComponent()¶

Mark the current unprocessed component as processed.

It does verify that at least one unprocessed component exists at this decision level.

This function does not return anything. Rather, the other code operates directly on the component stack and accesses the top of it via the

See: StackLevel:top() method.

void resetRemainingComps()¶: Mark all components in this decision level as processed.

const VariableIndex super_component() const¶

const VariableIndex remaining_components_ofs() const¶

MT - the start offset in the component stack for the remaining components in this decision level all remaining components can hence be found in

[remaining_components_ofs_, “nextLevel”.remaining_components_begin_)

Return: Level in the component stack of the first component for this decision level.

const VariableIndex unprocessed_components_end() const¶

One greater than the location in the component stack of unprocess components for the current decision level.

Return: One greater than the location in the component stack for unprocessed components for teh current point in the decision stack.

void set_unprocessed_components_end(VariableIndex end)¶

Update the location of the unprocessed component reference for this decision level.

Parameters

end: New location of the set of unprocessed components for this decision level.

StackLevel()¶

StackLevel(VariableIndex super_comp, VariableIndex lit_stack_ofs, ClauseOfs comp_stack_ofs)¶

VariableIndex currentRemainingComponent()¶

Access for the total number of remaining components across all decision levels not just the current one.

Return: Total number of remaining components

bool isSecondBranch()¶

Checks if the second (i.e., “true”) branch is now active.

Return: true if the second (“true”) branch is active.

void changeBranch()¶: Set the active branch (i.e., the one being searched to the positive branch.

bool anotherCompProcessible()¶

Checks if there is another processible component left. Lack of processible components could be due to either the branch being unsatisfiable or there being no processible components left

Return: true if a processible component remains.

VariableIndex literal_stack_ofs() const¶

void includeSolution(const mpz_class &solutions)¶

Updates the solution count. If no solution have been found, then the increase is additive. If at least one solution has already been found then the increase is multiplicative.

Parameters

solutions: Number of solutions to increase by.

void includeSolutionSampleMultiplier(const mpz_class &solutions)¶

Updates the multiplier for when doing solution sampling.

Parameters

solutions: Number of solutions to increase by.

void includeSolution(unsigned solutions)¶

Updates the solution count. If no solution have been found, then the increase is additive. If at least one solution has already been found then the increase is multiplicative.

Parameters

solutions: Number of solutions to increase by.

void configureNewLevel(const StackLevel &top, const DecisionLevel decision_level)¶

When variables become free in a residual formula (i.e., they no longer appear in any clauses), the solution count multiplier is stored. This needs to be pushed down the stack to ensure that the sample weights are correct.

This function pushes the current scalar multiplier down the stack.

Parameters

top: Current top of the decision stack.
decision_level: Number of branch variables already assigned. This does not include any implicit partial assignment.

void addFreeVariables(const std::vector<VariableIndex> &freed_vars)¶

Freed Variables Adder

When performing variable assignments, it is common that variables will become free (i.e., no longer appear in any clauses). Those variables will not appear in the literal stack since they are not set. However, they must be assigned as part of the sample generator. This function stores those freed variables.

Parameters

freed_vars: Newly freed variables

void addCachedCompIds(const std::vector<CacheEntryID> &ids)¶

Store the component IDs for the cached components.

Parameters

ids: List of cached entry identification numbers

bool branch_found_unsat() const¶

Checks if the currently active branch variable has been determined to be unsatisfiable.

Return: true if the currently active branch is unsatisfiable.

void mark_branch_unsat()¶: Sets the currently active branch to being unsatisfiable.

const mpz_class getTotalModelCount() const¶

Total number (i.e., sum of false and true) branches of this literal decision in the subtree.

Return: Total model count for both the positive and negative subtrees.

const mpz_class &getActiveModelCount() const¶

Gets the model count for the active branch. If the active branch is false, it will return the model count for negated version of the literal. Otherwise, it return the positive (unnegated) model count.

Return: Model count for the currently active literal state.

const mpz_class &getSamplerSolutionMultiplier() const¶

Gets the multiplier count for when running the solution sampler. It is used for the case when variables become free due to the residual formula no longer containing them.

Return: Solution count multiplier for the sampler.

const bool HasNoDescendentModels()¶

Calculates the total descendent model count for this stack level. It is equal to:

FalseModelCount * FalseCountMultiplier + TrueModelCount * TrueCountMultiplier

Return: Total descendent model count. Checks whether the associated decision level has any descendent models.
Return: True if both the true and false descendents are UNSAT.

const std::vector<VariableIndex> &emancipated_vars() const¶

Emancipated Variable List Accessor

This function is used to access the freed variable list for a specific variable branch. This is used for variable assignments.

Return: List of freed variables for the specified active branch.

const std::vector<CacheEntryID> &cached_comp_ids() const¶

Cached Component ID List Accessor

This function accesses the cached entry identification numbers for this stack level.

Return: Cached component IDs

const bool isComponentSplit() const¶

Component Split State Accessor

Accessor for whether this stack level corresponds with a component split.

It only applies when performing random sampling. Otherwise, it merely returns false.

Return: True if component split and random sampling is running.

void setAsComponentSplit()¶

Marks the decision level as a component split.

It only applies when performing random sampling.

void unsetAsComponentSplit()¶

Unmarks the decision level as a component split.

This function only has an effect when performing random sampling.

const bool isFirstComponent() const¶

Returns whether the first component in a component split has been processed. This is only relevant when performing random sampling.

Return: true if the first component has not been processed

void markFirstComponentComplete()¶: This is used for marking when the first component has been completed. We use this for sample stitching.

void set_cached_assn(CachedAssignment &cached_assn)¶

Cached Assignment Updater

Updates the cached assignment associated with this stack level.

Parameters

cached_assn: Updates the cached assignment information for this StackLevel.

const CachedAssignment &cached_assn() const¶

void ClearCachedAssn()¶: Removes all information associated with the cached assignment including the number of components it contains as well as the assignment itself.

void set_cache_sample(const SampleAssignment &cache_sample)¶

Store the cache sample assignment. It will be automatically associated with the right active branch.

Parameters

cache_sample: Sample that will be used for caching this sample.

SampleAssignment random_cache_sample() const¶

Randomly select the cache sample between the two branches.

Return: A sample that can be stored in the cache for this stack level.

Public Static Functions

static VariableIndex componentSplitDepth()¶

Component Split Depth Accessor

Accesses the global component split depth information.

Return: Current component split depth.

static void set_solver_config_and_statistics(SolverConfiguration &config, DataAndStatistics &statistics)¶

Configuration Updater

Stores the solver configuration. This is used so that global configuration settings (e.g., verbose) can be used for printing.

Parameters

config: Solver configuration