SMT-RAT  24.02
Toolbox for Strategic and Parallel Satisfiability-Modulo-Theories Solving
smtrat::GBSettings41 Struct Reference

#include <GBSettings.h>

Inheritance diagram for smtrat::GBSettings41:
Collaboration diagram for smtrat::GBSettings41:

Public Types

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

Static Public Attributes

static const unsigned identifier = 41
 
static const bool iterativeVariableRewriting = true
 
static constexpr auto moduleName = "GBModule<GBSettings4>"
 
static const bool passGB = false
 
static const bool getReasonsForInfeasibility = true
 
static const bool passWithMinimalReasons = false
 
static const check_inequalities checkInequalities = ALWAYS
 
static const pass_inequalities passInequalities = AS_RECEIVED
 
static const after_firstInfeasibleSubset withInfeasibleSubset = RETURN_DIRECTLY
 
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 = NO_INEQUALITIES
 
static const bool applyNSS = false
 
static const unsigned maxSDPdegree = 4
 
static const unsigned SDPupperBoundNrVariables = 6
 

Detailed Description

Definition at line 215 of file GBSettings.h.

Member Typedef Documentation

◆ Groebner

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

Definition at line 154 of file GBSettings.h.

◆ MultivariateIdeal

Definition at line 151 of file GBSettings.h.

◆ Order

typedef carl::GrLexOrdering smtrat::GBSettings4::Order
inherited

Definition at line 149 of file GBSettings.h.

◆ passPolynomial

◆ PolynomialWithReasons

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

Definition at line 150 of file GBSettings.h.

◆ Reductor

Definition at line 152 of file GBSettings.h.

Field Documentation

◆ addTheoryDeductions

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

Definition at line 162 of file GBSettings.h.

◆ applyNSS

const bool smtrat::GBSettings4::applyNSS = false
staticinherited

Definition at line 170 of file GBSettings.h.

◆ checkEqualitiesForTrivialSumOfSquares

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

Definition at line 165 of file GBSettings.h.

◆ checkInequalities

const check_inequalities smtrat::GBSettings4::checkInequalities = ALWAYS
staticinherited

Definition at line 159 of file GBSettings.h.

◆ checkInequalitiesForTrivialSumOfSquares

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

Definition at line 164 of file GBSettings.h.

◆ getReasonsForInfeasibility

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

Definition at line 157 of file GBSettings.h.

◆ identifier

const unsigned smtrat::GBSettings41::identifier = 41
static

Definition at line 217 of file GBSettings.h.

◆ iterativeVariableRewriting

const bool smtrat::GBSettings41::iterativeVariableRewriting = true
static

Definition at line 218 of file GBSettings.h.

◆ maxSDPdegree

const unsigned smtrat::GBSettings4::maxSDPdegree = 4
staticinherited

Definition at line 171 of file GBSettings.h.

◆ moduleName

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

Definition at line 146 of file GBSettings.h.

◆ passGB

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

Definition at line 156 of file GBSettings.h.

◆ passInequalities

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

Definition at line 160 of file GBSettings.h.

◆ passWithMinimalReasons

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

Definition at line 158 of file GBSettings.h.

◆ SDPupperBoundNrVariables

const unsigned smtrat::GBSettings4::SDPupperBoundNrVariables = 6
staticinherited

Definition at line 172 of file GBSettings.h.

◆ setCheckInequalitiesToBeginAfter

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

Definition at line 163 of file GBSettings.h.

◆ transformIntoEqualities

const transform_inequalities smtrat::GBSettings4::transformIntoEqualities = NO_INEQUALITIES
staticinherited

Definition at line 166 of file GBSettings.h.

◆ withInfeasibleSubset

const after_firstInfeasibleSubset smtrat::GBSettings4::withInfeasibleSubset = RETURN_DIRECTLY
staticinherited

Definition at line 161 of file GBSettings.h.


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