smtrat::IntBlastSettings1 Struct Reference

#include <IntBlastSettings.h>

Inheritance diagram for smtrat::IntBlastSettings1:

Static Public Attributes
static constexpr auto	moduleName = "IntBlastModule<IntBlastSettings1>"
static const std::size_t	max_variable_encoding_width = 6
	Maximum width used for encoding an integer variable as bit-vector. More...
static const bool	allow_encoding_into_complex_bvterms = true
	Whether to allow the encoding into complex bit-vector terms. More...
static const bool	apply_icp = false
	Whether to apply ICP to obtain smaller bounds for the term encodings. More...
static const bool	use_offsets_in_encoding = false
	Whether to use offsets for annotated bit-vector terms. More...

Detailed Description

Definition at line 32 of file IntBlastSettings.h.

Field Documentation

allow_encoding_into_complex_bvterms

const bool smtrat::IntBlastSettings1::allow_encoding_into_complex_bvterms = true

static

Whether to allow the encoding into complex bit-vector terms.

When set to false, an own bit-vector variable is introduced for each encoded polynomial. When set to true, polynomials may also be encoded by bit-vector terms that consist of bit-vector function symbols.

Definition at line 53 of file IntBlastSettings.h.

apply_icp

const bool smtrat::IntBlastSettings1::apply_icp = false

static

Whether to apply ICP to obtain smaller bounds for the term encodings.

If set to false, the widths for the encoded bit-vector terms are chosen conservatively.

Definition at line 61 of file IntBlastSettings.h.

max_variable_encoding_width

const std::size_t smtrat::IntBlastSettings1::max_variable_encoding_width = 6

static

Maximum width used for encoding an integer variable as bit-vector.

Note that this only applies to the encoding of variables. Intermediate terms (polynomials) are always encoded using a sufficiently high width.

If this value is set to zero, there is no maximal width. Choose this option only if all variables are bounded.

Definition at line 44 of file IntBlastSettings.h.

moduleName

constexpr auto smtrat::IntBlastSettings1::moduleName = "IntBlastModule<IntBlastSettings1>"

staticconstexpr

Definition at line 34 of file IntBlastSettings.h.

use_offsets_in_encoding

const bool smtrat::IntBlastSettings1::use_offsets_in_encoding = false

static

Whether to use offsets for annotated bit-vector terms.

For nonlinear variables, no offset is used (independent of this configuration setting).

Definition at line 68 of file IntBlastSettings.h.

---

The documentation for this struct was generated from the following file:

• smtrat-modules/IntBlastModule/IntBlastSettings.h