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

#include <GBSettings.h>

Inheritance diagram for smtrat::GBSettings5:
Inheritance 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 constexpr auto moduleName = "GBModule<GBSettings5>"
 
static const unsigned identifier = 5
 
static const bool passGB = true
 
static const bool getReasonsForInfeasibility = true
 
static const bool passWithMinimalReasons = true
 
static const check_inequalities checkInequalities = ALWAYS
 
static const pass_inequalities passInequalities = FULL_REDUCED
 
static const after_firstInfeasibleSubset withInfeasibleSubset = PROCEED_ALLINEQUALITIES
 
static const theory_deductions addTheoryDeductions = ALL_CONSTRAINTS
 
static const unsigned setCheckInequalitiesToBeginAfter = 0
 
static const transform_inequalities transformIntoEqualities = NO_INEQUALITIES
 
static const bool iterativeVariableRewriting = false
 
static const unsigned maxSearchExponent = 11
 
static const bool applyNSS = false
 
static const unsigned maxSDPdegree = 4
 
static const unsigned SDPupperBoundNrVariables = 6
 

Detailed Description

Definition at line 41 of file GBSettings.h.

Member Typedef Documentation

◆ Groebner

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

Definition at line 51 of file GBSettings.h.

◆ MultivariateIdeal

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

Definition at line 48 of file GBSettings.h.

◆ Order

typedef carl::GrLexOrdering smtrat::GBSettings5::Order

Definition at line 46 of file GBSettings.h.

◆ passPolynomial

typedef smtrat::decidePassingPolynomial smtrat::GBSettings5::passPolynomial

Definition at line 50 of file GBSettings.h.

◆ PolynomialWithReasons

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

Definition at line 47 of file GBSettings.h.

◆ Reductor

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

Definition at line 49 of file GBSettings.h.

Field Documentation

◆ addTheoryDeductions

const theory_deductions smtrat::GBSettings5::addTheoryDeductions = ALL_CONSTRAINTS
static

Definition at line 59 of file GBSettings.h.

◆ applyNSS

const bool smtrat::GBSettings5::applyNSS = false
static

Definition at line 66 of file GBSettings.h.

◆ checkInequalities

const check_inequalities smtrat::GBSettings5::checkInequalities = ALWAYS
static

Definition at line 56 of file GBSettings.h.

◆ getReasonsForInfeasibility

const bool smtrat::GBSettings5::getReasonsForInfeasibility = true
static

Definition at line 54 of file GBSettings.h.

◆ identifier

const unsigned smtrat::GBSettings5::identifier = 5
static

Definition at line 44 of file GBSettings.h.

◆ iterativeVariableRewriting

const bool smtrat::GBSettings5::iterativeVariableRewriting = false
static

Definition at line 62 of file GBSettings.h.

◆ maxSDPdegree

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

Definition at line 67 of file GBSettings.h.

◆ maxSearchExponent

const unsigned smtrat::GBSettings5::maxSearchExponent = 11
static

Definition at line 64 of file GBSettings.h.

◆ moduleName

constexpr auto smtrat::GBSettings5::moduleName = "GBModule<GBSettings5>"
staticconstexpr

Definition at line 43 of file GBSettings.h.

◆ passGB

const bool smtrat::GBSettings5::passGB = true
static

Definition at line 53 of file GBSettings.h.

◆ passInequalities

const pass_inequalities smtrat::GBSettings5::passInequalities = FULL_REDUCED
static

Definition at line 57 of file GBSettings.h.

◆ passWithMinimalReasons

const bool smtrat::GBSettings5::passWithMinimalReasons = true
static

Definition at line 55 of file GBSettings.h.

◆ SDPupperBoundNrVariables

const unsigned smtrat::GBSettings5::SDPupperBoundNrVariables = 6
static

Definition at line 68 of file GBSettings.h.

◆ setCheckInequalitiesToBeginAfter

const unsigned smtrat::GBSettings5::setCheckInequalitiesToBeginAfter = 0
static

Definition at line 60 of file GBSettings.h.

◆ transformIntoEqualities

const transform_inequalities smtrat::GBSettings5::transformIntoEqualities = NO_INEQUALITIES
static

Definition at line 61 of file GBSettings.h.

◆ withInfeasibleSubset

const after_firstInfeasibleSubset smtrat::GBSettings5::withInfeasibleSubset = PROCEED_ALLINEQUALITIES
static

Definition at line 58 of file GBSettings.h.

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