Struct SolverConfiguration

Struct Documentation

struct SolverConfiguration

solver_config.h

Purpose: Defines the SolverConfiguration() class stores the state of the sampler and counter.

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. Singleton object used for storing the configuration settings for the current execution.

Public Functions

bool store_sampled_models()

When random sampling is enabled, this flag indicates whether the models should currently be stored or other processing is occurring.

Return
True if sample models should be stored.

bool perform_sample_caching()

Cache Sampling State Accessor

Returns whether the cache currently supports sampling.

Return
true if samples are being stored in the cache.

void EnableSampleCaching()

Sample Caching Enabler

This enables storing of samples in the cache. It can only be enabled. It can never be disabled by design since once the caching stage has been enabled, it can never be disabled.

Public Members

bool perform_component_caching = true

Support to modify the default state of this feature is disabled in the sampler.

Forces variable backtracking in the case of a conflict being founded. Support to modify the default state of this feature is disabled in the sampler.

bool perform_failed_lit_test = true

Support to modify the default state of this feature is disabled in the sampler.

bool perform_pre_processing = true

Support to modify the default state of this feature is disabled in the sampler.

bool perform_random_sampling_ = true

Rather than performing standard model counting, sample satisfying models uniformly at random.

bool perform_top_tree_sampling = false

Performs sampling of the top of the tree.

bool disable_samples_write_ = false

Disable writing the samples file.

std::string samples_output_file = ""

Location to write the output sample and sampler information.

bool debug_mode = false

Debug mode has special settings to make debugging the program easier.

uint64_t time_bound_seconds = UINT64_MAX

Stores the maximum execution time of the sampler.

Default is approximately 27 hours.

bool verbose = false

Controls whether verbose state tracking is enabled. When verbose is enabled, a basic trace printing is also enabled.

In some versions of the console, this verbose printing may be multicolored for easier visual tracking.

bool quiet = false

Prevents printing to the console.

Cannot be true if verbose is true.

bool perform_two_pass_sampling_ = false

Forces two pass sample construction. This applies only to the case where the number of samples requested is 1.

unsigned num_samples_to_cache_ = 1

Number of samples that will be cached at once.

bool skip_partial_assignment_fill = false

DEBUG_ONLY MODE - This is an unsupported feature used for debug and development purposes only. Almost no one should use it beyond the core development team.

SampleSize num_samples_ = 0

Number of satisfying assignments to randomly sample. This is a command line parameter.

TreeNodeIndex max_top_tree_depth_ = 25

When trimming the top of the tree, this represents the maximum branch variable depth before sample building stops.

SampleSize max_top_tree_leaf_sample_count = 50

Maximum number of samples that can come from a single top tree node.

std::string top_tree_samples_output_file_

= “.” “/”

“__final_top_tree_samples.txt”


Location to write the top tree samples.