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

#include <GBPPSettings.h>

Public Types

using ReasonPolicy = carl::StdMultivariatePolynomialPolicies< carl::BVReasons >
 
using Order = carl::GrLexOrdering
 
using PolynomialWithReasons = carl::MultivariatePolynomial< Rational, Order, ReasonPolicy >
 
using Groebner = carl::GBProcedure< PolynomialWithReasons, carl::Buchberger, carl::StdAdding >
 
using Reductor = carl::Reductor< PolynomialWithReasons, PolynomialWithReasons >
 

Static Public Attributes

static constexpr auto moduleName = "GBPPModule<GBPPSettings1>"
 

Detailed Description

Definition at line 17 of file GBPPSettings.h.

Member Typedef Documentation

◆ Groebner

using smtrat::GBPPSettings1::Groebner = carl::GBProcedure<PolynomialWithReasons, carl::Buchberger, carl::StdAdding>

Definition at line 24 of file GBPPSettings.h.

◆ Order

using smtrat::GBPPSettings1::Order = carl::GrLexOrdering

Definition at line 22 of file GBPPSettings.h.

◆ PolynomialWithReasons

using smtrat::GBPPSettings1::PolynomialWithReasons = carl::MultivariatePolynomial<Rational, Order, ReasonPolicy>

Definition at line 23 of file GBPPSettings.h.

◆ ReasonPolicy

using smtrat::GBPPSettings1::ReasonPolicy = carl::StdMultivariatePolynomialPolicies<carl::BVReasons>

Definition at line 21 of file GBPPSettings.h.

◆ Reductor

using smtrat::GBPPSettings1::Reductor = carl::Reductor<PolynomialWithReasons,PolynomialWithReasons>

Definition at line 25 of file GBPPSettings.h.

Field Documentation

◆ moduleName

constexpr auto smtrat::GBPPSettings1::moduleName = "GBPPModule<GBPPSettings1>"
staticconstexpr

Definition at line 19 of file GBPPSettings.h.

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