smtrat::internal::OCSettings Struct Reference

#include <BCAll.h>

Inheritance diagram for smtrat::internal::OCSettings:

Collaboration diagram for smtrat::internal::OCSettings:

Public Types
using	op = cadcells::operators::op::mccallum
using	op = cadcells::operators::MccallumFiltered< OpSettings >
using	op = cadcells::operators::MccallumFiltered< OpSettings >
using	op = cadcells::operators::MccallumFiltered< OpSettings >
using	op = cadcells::operators::MccallumFiltered< OpSettings >
using	op = cadcells::operators::MccallumFiltered< OpSettings >
using	op = cadcells::operators::MccallumFiltered< OpSettings >
using	op = cadcells::operators::MccallumFiltered< OpSettings >
using	op = cadcells::operators::MccallumFiltered< OpSettings >
using	op = cadcells::operators::MccallumFiltered< OpSettings >
using	op = cadcells::operators::MccallumFiltered< cadcells::operators::MccallumFilteredSettings >
using	op = cadcells::operators::MccallumFiltered< OpSettings >
using	op = cadcells::operators::MccallumFiltered< OpSettings >
using	op = cadcells::operators::MccallumFiltered< cadcells::operators::MccallumFilteredSettings >

Static Public Attributes
constexpr static bool	exploit_strict_constraints = false
constexpr static auto	cell_heuristic = cadcells::representation::BIGGEST_CELL_FILTER
constexpr static auto	covering_heuristic = cadcells::representation::BIGGEST_CELL_COVERING_FILTER
constexpr static auto	op = cadcells::operators::op::mccallum
static constexpr bool	clause_chain_with_equivalences = false
static constexpr bool	enforce_tarski = false
constexpr static bool	use_approximation = false
static constexpr bool	clause_chain_with_equivalences = false
static constexpr bool	enforce_tarski = false
constexpr static bool	use_approximation = false

Detailed Description

Definition at line 17 of file BCAll.h.

Member Typedef Documentation

op [1/14]

constexpr static auto smtrat::internal::OCSettings::op = cadcells::operators::op::mccallum

constexpr

Definition at line 22 of file BCAll.h.

op [2/14]

using smtrat::internal::OCSettings::op = cadcells::operators::MccallumFiltered<OpSettings>

Definition at line 22 of file BCBc.h.

op [3/14]

using smtrat::internal::OCSettings::op = cadcells::operators::MccallumFiltered<OpSettings>

Definition at line 23 of file BCBoundsOnly.h.

op [4/14]

using smtrat::internal::OCSettings::op = cadcells::operators::MccallumFiltered<OpSettings>

Definition at line 23 of file BCDeg10.h.

op [5/14]

using smtrat::internal::OCSettings::op = cadcells::operators::MccallumFiltered<OpSettings>

Definition at line 23 of file BCDeg2.h.

op [6/14]

using smtrat::internal::OCSettings::op = cadcells::operators::MccallumFiltered<OpSettings>

Definition at line 23 of file BCDeg5.h.

op [7/14]

using smtrat::internal::OCSettings::op = cadcells::operators::MccallumFiltered<OpSettings>

Definition at line 22 of file BCIndep.h.

op [8/14]

using smtrat::internal::OCSettings::op = cadcells::operators::MccallumFiltered<OpSettings>

Definition at line 23 of file BCIntersect.h.

op [9/14]

using smtrat::internal::OCSettings::op = cadcells::operators::MccallumFiltered<OpSettings>

Definition at line 23 of file BCIrred.h.

op [10/14]

using smtrat::internal::OCSettings::op = cadcells::operators::MccallumFiltered<OpSettings>

Definition at line 23 of file BCIrredIndep.h.

op [11/14]

using smtrat::internal::OCSettings::op = cadcells::operators::MccallumFiltered<cadcells::operators::MccallumFilteredSettings>

Definition at line 18 of file BCNoop.h.

op [12/14]

using smtrat::internal::OCSettings::op = cadcells::operators::MccallumFiltered<OpSettings>

Definition at line 23 of file BCRational.h.

op [13/14]

using smtrat::internal::OCSettings::op = cadcells::operators::MccallumFiltered<OpSettings>

Definition at line 23 of file LDBBoundsOnly.h.

op [14/14]

using smtrat::internal::OCSettings::op = cadcells::operators::MccallumFiltered<cadcells::operators::MccallumFilteredSettings>

Definition at line 18 of file LDBNoop.h.

Field Documentation

cell_heuristic

constexpr static auto smtrat::internal::OCSettings::cell_heuristic = cadcells::representation::BIGGEST_CELL_FILTER

staticconstexpr

Definition at line 20 of file BCAll.h.

clause_chain_with_equivalences [1/2]

constexpr bool smtrat::mcsat::onecell::BaseSettings::clause_chain_with_equivalences = false

staticconstexprinherited

Definition at line 21 of file Explanation.h.

clause_chain_with_equivalences [2/2]

constexpr bool smtrat::mcsat::onecell::BaseSettings::clause_chain_with_equivalences = false

staticconstexprinherited

Definition at line 21 of file Explanation.h.

covering_heuristic

constexpr static auto smtrat::internal::OCSettings::covering_heuristic = cadcells::representation::BIGGEST_CELL_COVERING_FILTER

staticconstexpr

Definition at line 21 of file BCAll.h.

enforce_tarski [1/2]

constexpr bool smtrat::mcsat::onecell::BaseSettings::enforce_tarski = false

staticconstexprinherited

Definition at line 22 of file Explanation.h.

enforce_tarski [2/2]

constexpr bool smtrat::mcsat::onecell::BaseSettings::enforce_tarski = false

staticconstexprinherited

Definition at line 22 of file Explanation.h.

exploit_strict_constraints

constexpr static bool smtrat::internal::OCSettings::exploit_strict_constraints = false

staticconstexpr

Definition at line 18 of file BCAll.h.

op

constexpr static auto smtrat::internal::OCSettings::op = cadcells::operators::op::mccallum

staticconstexpr

Definition at line 18 of file OCNewBC.h.

use_approximation [1/2]

constexpr static bool smtrat::mcsat::onecell::BaseSettings::use_approximation = false

staticconstexprinherited

Definition at line 24 of file Explanation.h.

use_approximation [2/2]

constexpr static bool smtrat::mcsat::onecell::BaseSettings::use_approximation = false

staticconstexprinherited

Definition at line 24 of file Explanation.h.

---

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

• smtrat-strategies/strategies/Filter/BCAll.h
• smtrat-strategies/strategies/Filter/BCBc.h
• smtrat-strategies/strategies/Filter/BCBoundsOnly.h
• smtrat-strategies/strategies/Filter/BCDeg10.h
• smtrat-strategies/strategies/Filter/BCDeg2.h
• smtrat-strategies/strategies/Filter/BCDeg5.h
• smtrat-strategies/strategies/Filter/BCIndep.h
• smtrat-strategies/strategies/Filter/BCIntersect.h
• smtrat-strategies/strategies/Filter/BCIrred.h
• smtrat-strategies/strategies/Filter/BCIrredIndep.h
• smtrat-strategies/strategies/Filter/BCNoop.h
• smtrat-strategies/strategies/Filter/BCRational.h
• smtrat-strategies/strategies/Filter/LDBBoundsOnly.h
• smtrat-strategies/strategies/Filter/LDBNoop.h
• smtrat-strategies/strategies/MCSAT/OCNewBC.h
• smtrat-strategies/strategies/MCSAT/OCNewLDB.h
• smtrat-strategies/strategies/MCSAT/OCNewLDBCovering.h
• smtrat-strategies/strategies/MCSAT/OCNewLDBCoveringCache.h
• smtrat-strategies/strategies/MCSAT/OCNewLDBCoveringCacheGlobal.h