SMT-RAT  24.02
Toolbox for Strategic and Parallel Satisfiability-Modulo-Theories Solving
Public Types | Static Public Attributes
smtrat::GBSettings63 Struct Reference

#include <GBSettings.h>

Inheritance diagram for smtrat::GBSettings63:
Inheritance graph
[legend]
Collaboration diagram for smtrat::GBSettings63:
Collaboration graph
[legend]

Public Types

typedef carl::GrLexOrdering Order
 
typedef carl::MultivariatePolynomial< Rational, Order, ReasonPolicy > PolynomialWithReasons
 
typedef carl::Ideal< PolynomialWithReasons > MultivariateIdeal
 
typedef carl::Reductor< PolynomialWithReasons, PolynomialWithReasons > Reductor
 
typedef smtrat::decidePassingPolynomial passPolynomial
 
typedef carl::GBProcedure< PolynomialWithReasons, carl::Buchberger, carl::StdAdding > Groebner
 

Static Public Attributes

static const unsigned identifier = 63
 
static const bool applyNSS = true
 
static const unsigned maxSDPdegree = 4
 
static const unsigned SDPupperBoundNrVariables = 15
 
static const bool iterativeVariableRewriting = true
 
static constexpr auto moduleName = "GBModule<GBSettings6>"
 
static const bool passGB = false
 
static const bool getReasonsForInfeasibility = true
 
static const bool passWithMinimalReasons = false
 
static const check_inequalities checkInequalities = NEVER
 
static const pass_inequalities passInequalities = AS_RECEIVED
 
static const after_firstInfeasibleSubset withInfeasibleSubset = PROCEED_ALLINEQUALITIES
 
static const theory_deductions addTheoryDeductions = ALL_CONSTRAINTS
 
static const unsigned setCheckInequalitiesToBeginAfter = 0
 
static const bool checkInequalitiesForTrivialSumOfSquares = true
 
static const bool checkEqualitiesForTrivialSumOfSquares = true
 
static const transform_inequalities transformIntoEqualities = ALL_INEQUALITIES
 
static const unsigned maxSearchExponent = 11
 
static const unsigned callSDPAfterNMonomials = 6
 
static const unsigned sternBrocotStartPrecisionOneTo = 80
 
static const unsigned sternBrocotHigherPrecisionSteps = 2
 
static const unsigned sternBrocotHigherPrecisionFactor = 10
 

Detailed Description

Definition at line 268 of file GBSettings.h.

Member Typedef Documentation

◆ Groebner

typedef carl::GBProcedure<PolynomialWithReasons, carl::Buchberger, carl::StdAdding> smtrat::GBSettings6::Groebner
inherited

Definition at line 188 of file GBSettings.h.

◆ MultivariateIdeal

typedef carl::Ideal<PolynomialWithReasons> smtrat::GBSettings63::MultivariateIdeal

Definition at line 272 of file GBSettings.h.

◆ Order

typedef carl::GrLexOrdering smtrat::GBSettings63::Order

Definition at line 270 of file GBSettings.h.

◆ passPolynomial

typedef smtrat::decidePassingPolynomial smtrat::GBSettings63::passPolynomial

Definition at line 274 of file GBSettings.h.

◆ PolynomialWithReasons

typedef carl::MultivariatePolynomial<Rational, Order, ReasonPolicy> smtrat::GBSettings63::PolynomialWithReasons

Definition at line 271 of file GBSettings.h.

◆ Reductor

typedef carl::Reductor<PolynomialWithReasons,PolynomialWithReasons> smtrat::GBSettings63::Reductor

Definition at line 273 of file GBSettings.h.

Field Documentation

◆ addTheoryDeductions

const theory_deductions smtrat::GBSettings6::addTheoryDeductions = ALL_CONSTRAINTS
staticinherited

Definition at line 196 of file GBSettings.h.

◆ applyNSS

const bool smtrat::GBSettings63::applyNSS = true
static

Definition at line 279 of file GBSettings.h.

◆ callSDPAfterNMonomials

const unsigned smtrat::GBSettings6::callSDPAfterNMonomials = 6
staticinherited

Definition at line 209 of file GBSettings.h.

◆ checkEqualitiesForTrivialSumOfSquares

const bool smtrat::GBSettings6::checkEqualitiesForTrivialSumOfSquares = true
staticinherited

Definition at line 199 of file GBSettings.h.

◆ checkInequalities

const check_inequalities smtrat::GBSettings6::checkInequalities = NEVER
staticinherited

Definition at line 193 of file GBSettings.h.

◆ checkInequalitiesForTrivialSumOfSquares

const bool smtrat::GBSettings6::checkInequalitiesForTrivialSumOfSquares = true
staticinherited

Definition at line 198 of file GBSettings.h.

◆ getReasonsForInfeasibility

const bool smtrat::GBSettings6::getReasonsForInfeasibility = true
staticinherited

Definition at line 191 of file GBSettings.h.

◆ identifier

const unsigned smtrat::GBSettings63::identifier = 63
static

Definition at line 278 of file GBSettings.h.

◆ iterativeVariableRewriting

const bool smtrat::GBSettings61::iterativeVariableRewriting = true
staticinherited

Definition at line 243 of file GBSettings.h.

◆ maxSDPdegree

const unsigned smtrat::GBSettings63::maxSDPdegree = 4
static

Definition at line 280 of file GBSettings.h.

◆ maxSearchExponent

const unsigned smtrat::GBSettings6::maxSearchExponent = 11
staticinherited

Definition at line 204 of file GBSettings.h.

◆ moduleName

constexpr auto smtrat::GBSettings6::moduleName = "GBModule<GBSettings6>"
staticconstexprinherited

Definition at line 180 of file GBSettings.h.

◆ passGB

const bool smtrat::GBSettings6::passGB = false
staticinherited

Definition at line 190 of file GBSettings.h.

◆ passInequalities

const pass_inequalities smtrat::GBSettings6::passInequalities = AS_RECEIVED
staticinherited

Definition at line 194 of file GBSettings.h.

◆ passWithMinimalReasons

const bool smtrat::GBSettings6::passWithMinimalReasons = false
staticinherited

Definition at line 192 of file GBSettings.h.

◆ SDPupperBoundNrVariables

const unsigned smtrat::GBSettings63::SDPupperBoundNrVariables = 15
static

Definition at line 281 of file GBSettings.h.

◆ setCheckInequalitiesToBeginAfter

const unsigned smtrat::GBSettings6::setCheckInequalitiesToBeginAfter = 0
staticinherited

Definition at line 197 of file GBSettings.h.

◆ sternBrocotHigherPrecisionFactor

const unsigned smtrat::GBSettings6::sternBrocotHigherPrecisionFactor = 10
staticinherited

Definition at line 212 of file GBSettings.h.

◆ sternBrocotHigherPrecisionSteps

const unsigned smtrat::GBSettings6::sternBrocotHigherPrecisionSteps = 2
staticinherited

Definition at line 211 of file GBSettings.h.

◆ sternBrocotStartPrecisionOneTo

const unsigned smtrat::GBSettings6::sternBrocotStartPrecisionOneTo = 80
staticinherited

Definition at line 210 of file GBSettings.h.

◆ transformIntoEqualities

const transform_inequalities smtrat::GBSettings6::transformIntoEqualities = ALL_INEQUALITIES
staticinherited

Definition at line 200 of file GBSettings.h.

◆ withInfeasibleSubset

const after_firstInfeasibleSubset smtrat::GBSettings6::withInfeasibleSubset = PROCEED_ALLINEQUALITIES
staticinherited

Definition at line 195 of file GBSettings.h.

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