SMT-RAT  24.02
Toolbox for Strategic and Parallel Satisfiability-Modulo-Theories Solving
Data Structures | Typedefs | Enumerations | Functions
smtrat::cadcells::representation::approximation Namespace Reference

Data Structures

struct  ApxSettings
 
class  CellApproximator
 
class  ApxCriteria
 

Typedefs

using IR = datastructures::IndexedRoot
 

Enumerations

enum  ApxPoly {
  SIMPLE , LINEAR_GRADIENT , TAYLOR , TAYLOR_LIN ,
  MAXIMIZE
}
 
enum  ApxRoot { SAMPLE_MID , SIMPLE_REPRESENTATION , STERN_BROCOT , FIXED_RATIO }
 

Functions

const ApxSettings & apx_settings ()
 
template<>
IR CellApproximator::apx_bound< ApxPoly::SIMPLE > (const IR &, const RAN &bound, bool below)
 
template<>
IR CellApproximator::apx_bound< ApxPoly::LINEAR_GRADIENT > (const IR &p, const RAN &bound, bool below)
 
template<>
IR CellApproximator::apx_bound< ApxPoly::TAYLOR > (const IR &p, const RAN &bound, bool below)
 
template<>
IR CellApproximator::apx_bound< ApxPoly::TAYLOR_LIN > (const IR &p, const RAN &bound, bool below)
 
template<>
IR CellApproximator::apx_bound< ApxPoly::MAXIMIZE > (const IR &p, const RAN &bound, bool below)
 
template<>
IR CellApproximator::apx_between< ApxPoly::SIMPLE > (const IR &, const IR &, const RAN &l, const RAN &u)
 
Rational mediant (Rational a, Rational b)
 
Rational approximate_RAN (const RAN &r)
 
Rational approximate_RAN_sb (const RAN &r)
 
Rational approximate_RAN_below (const RAN &r)
 
Rational approximate_RAN_above (const RAN &r)
 
template<ApxRoot AR>
Rational approximate_root_above (const RAN &inner, const RAN &outer)
 
template<ApxRoot AR>
Rational approximate_root_below (const RAN &inner, const RAN &outer)
 
template<>
Rational approximate_root_above< ApxRoot::SAMPLE_MID > (const RAN &inner, const RAN &outer)
 
template<>
Rational approximate_root_below< ApxRoot::SAMPLE_MID > (const RAN &inner, const RAN &outer)
 
template<>
Rational approximate_root_above< ApxRoot::SIMPLE_REPRESENTATION > (const RAN &inner, const RAN &outer)
 
template<>
Rational approximate_root_below< ApxRoot::SIMPLE_REPRESENTATION > (const RAN &inner, const RAN &outer)
 
template<>
Rational approximate_root_above< ApxRoot::STERN_BROCOT > (const RAN &inner, const RAN &outer)
 
template<>
Rational approximate_root_below< ApxRoot::STERN_BROCOT > (const RAN &inner, const RAN &outer)
 
template<>
Rational approximate_root_above< ApxRoot::FIXED_RATIO > (const RAN &inner, const RAN &outer)
 
template<>
Rational approximate_root_below< ApxRoot::FIXED_RATIO > (const RAN &inner, const RAN &outer)
 
template<ApxRoot AR>
Rational approximate_root (const RAN &inner, const RAN &outer, bool below)
 

Typedef Documentation

◆ IR

typedef datastructures::IndexedRoot smtrat::cadcells::representation::approximation::IR

Definition at line 8 of file CellApproximator.h.

Enumeration Type Documentation

◆ ApxPoly

enum smtrat::cadcells::representation::approximation::ApxPoly
Enumerator
SIMPLE 
LINEAR_GRADIENT 
TAYLOR 
TAYLOR_LIN 
MAXIMIZE 

Definition at line 3 of file ApproximationSettings.h.

◆ ApxRoot

enum smtrat::cadcells::representation::approximation::ApxRoot
Enumerator
SAMPLE_MID 
SIMPLE_REPRESENTATION 
STERN_BROCOT 
FIXED_RATIO 

Definition at line 5 of file ApproximationSettings.h.

Function Documentation

◆ approximate_RAN()

Rational smtrat::cadcells::representation::approximation::approximate_RAN ( const RAN &  r)
inline

Definition at line 7 of file ran_approximation.h.

Here is the caller graph for this function:

◆ approximate_RAN_above()

Rational smtrat::cadcells::representation::approximation::approximate_RAN_above ( const RAN &  r)
inline

Definition at line 26 of file ran_approximation.h.

Here is the caller graph for this function:

◆ approximate_RAN_below()

Rational smtrat::cadcells::representation::approximation::approximate_RAN_below ( const RAN &  r)
inline

Definition at line 17 of file ran_approximation.h.

Here is the caller graph for this function:

◆ approximate_RAN_sb()

Rational smtrat::cadcells::representation::approximation::approximate_RAN_sb ( const RAN &  r)
inline

Definition at line 12 of file ran_approximation.h.

Here is the caller graph for this function:

◆ approximate_root()

template<ApxRoot AR>
Rational smtrat::cadcells::representation::approximation::approximate_root ( const RAN &  inner,
const RAN &  outer,
bool  below 
)
inline

Definition at line 162 of file ran_approximation.h.

◆ approximate_root_above()

template<ApxRoot AR>
Rational smtrat::cadcells::representation::approximation::approximate_root_above ( const RAN &  inner,
const RAN &  outer 
)
inline

◆ approximate_root_above< ApxRoot::FIXED_RATIO >()

template<>
Rational smtrat::cadcells::representation::approximation::approximate_root_above< ApxRoot::FIXED_RATIO > ( const RAN &  inner,
const RAN &  outer 
)
inline

Definition at line 142 of file ran_approximation.h.

Here is the call graph for this function:

◆ approximate_root_above< ApxRoot::SAMPLE_MID >()

template<>
Rational smtrat::cadcells::representation::approximation::approximate_root_above< ApxRoot::SAMPLE_MID > ( const RAN &  inner,
const RAN &  outer 
)
inline

Definition at line 42 of file ran_approximation.h.

◆ approximate_root_above< ApxRoot::SIMPLE_REPRESENTATION >()

template<>
Rational smtrat::cadcells::representation::approximation::approximate_root_above< ApxRoot::SIMPLE_REPRESENTATION > ( const RAN &  inner,
const RAN &  outer 
)
inline

Definition at line 51 of file ran_approximation.h.

Here is the call graph for this function:

◆ approximate_root_above< ApxRoot::STERN_BROCOT >()

template<>
Rational smtrat::cadcells::representation::approximation::approximate_root_above< ApxRoot::STERN_BROCOT > ( const RAN &  inner,
const RAN &  outer 
)
inline

Definition at line 88 of file ran_approximation.h.

Here is the call graph for this function:

◆ approximate_root_below()

template<ApxRoot AR>
Rational smtrat::cadcells::representation::approximation::approximate_root_below ( const RAN &  inner,
const RAN &  outer 
)

◆ approximate_root_below< ApxRoot::FIXED_RATIO >()

template<>
Rational smtrat::cadcells::representation::approximation::approximate_root_below< ApxRoot::FIXED_RATIO > ( const RAN &  inner,
const RAN &  outer 
)
inline

Definition at line 152 of file ran_approximation.h.

Here is the call graph for this function:

◆ approximate_root_below< ApxRoot::SAMPLE_MID >()

template<>
Rational smtrat::cadcells::representation::approximation::approximate_root_below< ApxRoot::SAMPLE_MID > ( const RAN &  inner,
const RAN &  outer 
)
inline

Definition at line 46 of file ran_approximation.h.

◆ approximate_root_below< ApxRoot::SIMPLE_REPRESENTATION >()

template<>
Rational smtrat::cadcells::representation::approximation::approximate_root_below< ApxRoot::SIMPLE_REPRESENTATION > ( const RAN &  inner,
const RAN &  outer 
)
inline

Definition at line 69 of file ran_approximation.h.

Here is the call graph for this function:

◆ approximate_root_below< ApxRoot::STERN_BROCOT >()

template<>
Rational smtrat::cadcells::representation::approximation::approximate_root_below< ApxRoot::STERN_BROCOT > ( const RAN &  inner,
const RAN &  outer 
)
inline

Definition at line 115 of file ran_approximation.h.

Here is the call graph for this function:

◆ apx_settings()

const ApxSettings& smtrat::cadcells::representation::approximation::apx_settings ( )
inline

Definition at line 36 of file ApproximationSettings.h.

Here is the caller graph for this function:

◆ CellApproximator::apx_between< ApxPoly::SIMPLE >()

template<>
IR smtrat::cadcells::representation::approximation::CellApproximator::apx_between< ApxPoly::SIMPLE > ( const IR &  ,
const IR &  ,
const RAN &  l,
const RAN &  u 
)
inline

Definition at line 304 of file CellApproximator.h.

Here is the call graph for this function:

◆ CellApproximator::apx_bound< ApxPoly::LINEAR_GRADIENT >()

template<>
IR smtrat::cadcells::representation::approximation::CellApproximator::apx_bound< ApxPoly::LINEAR_GRADIENT > ( const IR &  p,
const RAN &  bound,
bool  below 
)
inline

Definition at line 49 of file CellApproximator.h.

Here is the call graph for this function:

◆ CellApproximator::apx_bound< ApxPoly::MAXIMIZE >()

template<>
IR smtrat::cadcells::representation::approximation::CellApproximator::apx_bound< ApxPoly::MAXIMIZE > ( const IR &  p,
const RAN &  bound,
bool  below 
)
inline

Definition at line 221 of file CellApproximator.h.

Here is the call graph for this function:

◆ CellApproximator::apx_bound< ApxPoly::SIMPLE >()

template<>
IR smtrat::cadcells::representation::approximation::CellApproximator::apx_bound< ApxPoly::SIMPLE > ( const IR &  ,
const RAN &  bound,
bool  below 
)
inline

Definition at line 43 of file CellApproximator.h.

Here is the call graph for this function:

◆ CellApproximator::apx_bound< ApxPoly::TAYLOR >()

template<>
IR smtrat::cadcells::representation::approximation::CellApproximator::apx_bound< ApxPoly::TAYLOR > ( const IR &  p,
const RAN &  bound,
bool  below 
)
inline

Definition at line 60 of file CellApproximator.h.

Here is the call graph for this function:

◆ CellApproximator::apx_bound< ApxPoly::TAYLOR_LIN >()

template<>
IR smtrat::cadcells::representation::approximation::CellApproximator::apx_bound< ApxPoly::TAYLOR_LIN > ( const IR &  p,
const RAN &  bound,
bool  below 
)
inline

Definition at line 147 of file CellApproximator.h.

Here is the call graph for this function:

◆ mediant()

Rational smtrat::cadcells::representation::approximation::mediant ( Rational  a,
Rational  b 
)
inline

Definition at line 3 of file ran_approximation.h.

Here is the caller graph for this function: