SMT-RAT  24.02
Toolbox for Strategic and Parallel Satisfiability-Modulo-Theories Solving
Public Member Functions | Data Fields
smtrat::LRAModule< Settings >::Context Struct Reference

Stores a formula, being part of the received formula of this module, and the position of this formula in the passed formula. More...

#include <LRAModule.h>

Public Member Functions

 Context (const FormulaT &_origin, ModuleInput::iterator _pos)
 

Data Fields

FormulaT origin
 The formula in the received formula. More...
 
ModuleInput::iterator position
 The position of this formula in the passed formula. More...
 

Detailed Description

template<class Settings>
struct smtrat::LRAModule< Settings >::Context

Stores a formula, being part of the received formula of this module, and the position of this formula in the passed formula.

TODO: Maybe it is enough to store a mapping of the formula to the position.

Definition at line 52 of file LRAModule.h.

Constructor & Destructor Documentation

◆ Context()

template<class Settings >
smtrat::LRAModule< Settings >::Context::Context ( const FormulaT &  _origin,
ModuleInput::iterator  _pos 
)
inline

Definition at line 59 of file LRAModule.h.

Field Documentation

◆ origin

template<class Settings >
FormulaT smtrat::LRAModule< Settings >::Context::origin

The formula in the received formula.

Definition at line 55 of file LRAModule.h.

◆ position

template<class Settings >
ModuleInput::iterator smtrat::LRAModule< Settings >::Context::position

The position of this formula in the passed formula.

Definition at line 57 of file LRAModule.h.

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