Struct SolverConfiguration¶
- Defined in File solver_config.h
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.