SMT-RAT
24.02
Toolbox for Strategic and Parallel Satisfiability-Modulo-Theories Solving
|
#include <GBSettings.h>
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 = 511 |
static const bool | iterativeVariableRewriting = true |
static constexpr auto | moduleName = "GBModule<GBSettings5>" |
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 unsigned | maxSearchExponent = 11 |
static const bool | applyNSS = false |
static const unsigned | maxSDPdegree = 4 |
static const unsigned | SDPupperBoundNrVariables = 6 |
Definition at line 227 of file GBSettings.h.
|
inherited |
Definition at line 51 of file GBSettings.h.
typedef carl::Ideal<PolynomialWithReasons> smtrat::GBSettings51A::MultivariateIdeal |
Definition at line 231 of file GBSettings.h.
typedef carl::GrLexOrdering smtrat::GBSettings51A::Order |
Definition at line 229 of file GBSettings.h.
Definition at line 233 of file GBSettings.h.
typedef carl::MultivariatePolynomial<Rational, Order, ReasonPolicy> smtrat::GBSettings51A::PolynomialWithReasons |
Definition at line 230 of file GBSettings.h.
typedef carl::Reductor<PolynomialWithReasons,PolynomialWithReasons> smtrat::GBSettings51A::Reductor |
Definition at line 232 of file GBSettings.h.
|
staticinherited |
Definition at line 59 of file GBSettings.h.
|
staticinherited |
Definition at line 66 of file GBSettings.h.
|
staticinherited |
Definition at line 56 of file GBSettings.h.
|
staticinherited |
Definition at line 54 of file GBSettings.h.
|
static |
Definition at line 235 of file GBSettings.h.
|
static |
Definition at line 236 of file GBSettings.h.
|
staticinherited |
Definition at line 67 of file GBSettings.h.
|
staticinherited |
Definition at line 64 of file GBSettings.h.
|
staticconstexprinherited |
Definition at line 43 of file GBSettings.h.
|
staticinherited |
Definition at line 53 of file GBSettings.h.
|
staticinherited |
Definition at line 57 of file GBSettings.h.
|
staticinherited |
Definition at line 55 of file GBSettings.h.
|
staticinherited |
Definition at line 68 of file GBSettings.h.
|
staticinherited |
Definition at line 60 of file GBSettings.h.
|
staticinherited |
Definition at line 61 of file GBSettings.h.
|
staticinherited |
Definition at line 58 of file GBSettings.h.