SMT-RAT  24.02
Toolbox for Strategic and Parallel Satisfiability-Modulo-Theories Solving
Data Structures | Public Member Functions | Data Fields
smtrat::parser::ParserState Struct Reference

#include <ParserState.h>

Collaboration diagram for smtrat::parser::ParserState:
Collaboration graph
[legend]

Data Structures

struct  ExpressionScope
 
struct  ScriptScope
 

Public Member Functions

 ParserState (InstructionHandler &ih)
 
 ~ParserState ()
 
void pushExpressionScope ()
 
void popExpressionScope ()
 
void pushScriptScope ()
 
void popScriptScope ()
 
std::size_t script_scope_size () const
 
void reset ()
 
void errorMessage (const std::string &msg)
 
bool isSymbolFree (const std::string &name, bool output=true)
 
template<typename Res , typename T >
bool resolveSymbol (const std::string &name, const std::map< std::string, T > &map, Res &result) const
 
bool resolveSymbol (const std::string &name, types::TermType &r) const
 
bool resolveSymbol (const std::string &name, types::VariableType &r) const
 
void registerFunction (const std::string &name, const FunctionInstantiator *fi)
 
void registerFunction (const std::string &name, const IndexedFunctionInstantiator *fi)
 
void registerFunction (const std::string &name, const UserFunctionInstantiator *fi)
 

Data Fields

carl::Logic logic
 
std::set< types::VariableType > auxiliary_variables
 
std::map< std::string, types::TermType > bindings
 
std::map< std::string, types::TermType > constants
 
std::map< std::string, types::VariableType > variables
 
std::map< std::string, carl::UninterpretedFunction > declared_functions
 
std::map< std::string, const FunctionInstantiator * > defined_functions
 
std::map< std::string, const IndexedFunctionInstantiator * > defined_indexed_functions
 
std::map< std::string, const UserFunctionInstantiator * > defined_user_functions
 
FormulasT global_formulas
 
std::vector< smtrat::ModelVariable > artificialVariables
 
InstructionHandler & handler
 
std::stack< ExpressionScope > expressionScopes
 
std::stack< ScriptScope > scriptScopes
 

Detailed Description

Definition at line 18 of file ParserState.h.

Constructor & Destructor Documentation

◆ ParserState()

smtrat::parser::ParserState::ParserState ( InstructionHandler &  ih)
inline

Definition at line 79 of file ParserState.h.

◆ ~ParserState()

smtrat::parser::ParserState::~ParserState ( )
inline

Definition at line 81 of file ParserState.h.

Here is the call graph for this function:

Member Function Documentation

◆ errorMessage()

void smtrat::parser::ParserState::errorMessage ( const std::string &  msg)
inline

Definition at line 126 of file ParserState.h.

◆ isSymbolFree()

bool smtrat::parser::ParserState::isSymbolFree ( const std::string &  name,
bool  output = true 
)
inline

Definition at line 129 of file ParserState.h.

Here is the caller graph for this function:

◆ popExpressionScope()

void smtrat::parser::ParserState::popExpressionScope ( )
inline

Definition at line 94 of file ParserState.h.

Here is the caller graph for this function:

◆ popScriptScope()

void smtrat::parser::ParserState::popScriptScope ( )
inline

Definition at line 102 of file ParserState.h.

Here is the caller graph for this function:

◆ pushExpressionScope()

void smtrat::parser::ParserState::pushExpressionScope ( )
inline

Definition at line 91 of file ParserState.h.

Here is the caller graph for this function:

◆ pushScriptScope()

void smtrat::parser::ParserState::pushScriptScope ( )
inline

Definition at line 98 of file ParserState.h.

Here is the caller graph for this function:

◆ registerFunction() [1/3]

void smtrat::parser::ParserState::registerFunction ( const std::string &  name,
const FunctionInstantiator *  fi 
)
inline

Definition at line 163 of file ParserState.h.

Here is the call graph for this function:
Here is the caller graph for this function:

◆ registerFunction() [2/3]

void smtrat::parser::ParserState::registerFunction ( const std::string &  name,
const IndexedFunctionInstantiator *  fi 
)
inline

Definition at line 170 of file ParserState.h.

Here is the call graph for this function:

◆ registerFunction() [3/3]

void smtrat::parser::ParserState::registerFunction ( const std::string &  name,
const UserFunctionInstantiator *  fi 
)
inline

Definition at line 177 of file ParserState.h.

Here is the call graph for this function:

◆ reset()

void smtrat::parser::ParserState::reset ( )
inline

Definition at line 112 of file ParserState.h.

Here is the caller graph for this function:

◆ resolveSymbol() [1/3]

template<typename Res , typename T >
bool smtrat::parser::ParserState::resolveSymbol ( const std::string &  name,
const std::map< std::string, T > &  map,
Res &  result 
) const
inline

Definition at line 145 of file ParserState.h.

Here is the caller graph for this function:

◆ resolveSymbol() [2/3]

bool smtrat::parser::ParserState::resolveSymbol ( const std::string &  name,
types::TermType &  r 
) const
inline

Definition at line 152 of file ParserState.h.

Here is the call graph for this function:

◆ resolveSymbol() [3/3]

bool smtrat::parser::ParserState::resolveSymbol ( const std::string &  name,
types::VariableType &  r 
) const
inline

Definition at line 158 of file ParserState.h.

Here is the call graph for this function:

◆ script_scope_size()

std::size_t smtrat::parser::ParserState::script_scope_size ( ) const
inline

Definition at line 108 of file ParserState.h.

Here is the caller graph for this function:

Field Documentation

◆ artificialVariables

std::vector<smtrat::ModelVariable> smtrat::parser::ParserState::artificialVariables

Definition at line 72 of file ParserState.h.

◆ auxiliary_variables

std::set<types::VariableType> smtrat::parser::ParserState::auxiliary_variables

Definition at line 63 of file ParserState.h.

◆ bindings

std::map<std::string, types::TermType> smtrat::parser::ParserState::bindings

Definition at line 64 of file ParserState.h.

◆ constants

std::map<std::string, types::TermType> smtrat::parser::ParserState::constants

Definition at line 65 of file ParserState.h.

◆ declared_functions

std::map<std::string, carl::UninterpretedFunction> smtrat::parser::ParserState::declared_functions

Definition at line 67 of file ParserState.h.

◆ defined_functions

std::map<std::string, const FunctionInstantiator*> smtrat::parser::ParserState::defined_functions

Definition at line 68 of file ParserState.h.

◆ defined_indexed_functions

std::map<std::string, const IndexedFunctionInstantiator*> smtrat::parser::ParserState::defined_indexed_functions

Definition at line 69 of file ParserState.h.

◆ defined_user_functions

std::map<std::string, const UserFunctionInstantiator*> smtrat::parser::ParserState::defined_user_functions

Definition at line 70 of file ParserState.h.

◆ expressionScopes

std::stack<ExpressionScope> smtrat::parser::ParserState::expressionScopes

Definition at line 76 of file ParserState.h.

◆ global_formulas

FormulasT smtrat::parser::ParserState::global_formulas

Definition at line 71 of file ParserState.h.

◆ handler

InstructionHandler& smtrat::parser::ParserState::handler

Definition at line 74 of file ParserState.h.

◆ logic

carl::Logic smtrat::parser::ParserState::logic

Definition at line 61 of file ParserState.h.

◆ scriptScopes

std::stack<ScriptScope> smtrat::parser::ParserState::scriptScopes

Definition at line 77 of file ParserState.h.

◆ variables

std::map<std::string, types::VariableType> smtrat::parser::ParserState::variables

Definition at line 66 of file ParserState.h.

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