smtrat::IntBlastSettings2 Struct Reference

#include <IntBlastSettings.h>

Inheritance diagram for smtrat::IntBlastSettings2:

Collaboration diagram for smtrat::IntBlastSettings2:

Static Public Attributes
static constexpr auto	moduleName = "IntBlastModule<IntBlastSettings2>"
static const std::size_t	max_variable_encoding_width = 0
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 71 of file IntBlastSettings.h.

Field Documentation

allow_encoding_into_complex_bvterms

const bool smtrat::IntBlastSettings1::allow_encoding_into_complex_bvterms = true

staticinherited

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

staticinherited

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::IntBlastSettings2::max_variable_encoding_width = 0

static

Definition at line 74 of file IntBlastSettings.h.

moduleName

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

staticconstexpr

Definition at line 73 of file IntBlastSettings.h.

use_offsets_in_encoding

const bool smtrat::IntBlastSettings1::use_offsets_in_encoding = false

staticinherited

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