smtrat::parser::CoreTheory Struct Reference

Implements the core theory of the booleans. More...

#include <Core.h>

Inheritance diagram for smtrat::parser::CoreTheory:

Collaboration diagram for smtrat::parser::CoreTheory:

Public Types
using	OperatorType = boost::variant< carl::FormulaType >

Public Member Functions
	CoreTheory (ParserState *state)
bool	declareVariable (const std::string &name, const carl::Sort &sort, types::VariableType &result, TheoryError &errors)
	Declare a new variable with the given name and the given sort. More...
bool	handleITE (const FormulaT &ifterm, const types::TermType &thenterm, const types::TermType &elseterm, types::TermType &result, TheoryError &errors)
	Resolve an if-then-else operator. More...
bool	handleDistinct (const std::vector< types::TermType > &arguments, types::TermType &result, TheoryError &errors)
	Resolve a distinct operator. More...
bool	functionCall (const Identifier &identifier, const std::vector< types::TermType > &arguments, types::TermType &result, TheoryError &errors)
	Resolve another unknown function call. More...
virtual bool	resolveSymbol (const Identifier &, types::TermType &, TheoryError &errors)
	Resolve a symbol that was not declared within the ParserState. More...
template<typename T , typename Builder >
FormulaT	expandDistinct (const std::vector< T > &values, const Builder &neqBuilder)
virtual bool	instantiate (const types::VariableType &, const types::TermType &, types::TermType &, TheoryError &errors)
	Instantiate a variable within a term. More...
virtual bool	refreshVariable (const types::VariableType &, types::VariableType &, TheoryError &errors)
virtual bool	declareQuantifiedTerm (const std::vector< std::pair< std::string, carl::Sort >> &, const carl::FormulaType &, const types::TermType &, types::TermType &, TheoryError &errors)
	Resolve a quantified term. More...

Static Public Member Functions
static void	addSimpleSorts (qi::symbols< char, carl::Sort > &sorts)
static void	addConstants (qi::symbols< char, types::ConstType > &constants)

Data Fields
ParserState *	state

Detailed Description

Implements the core theory of the booleans.

Definition at line 15 of file Core.h.

Member Typedef Documentation

OperatorType

using smtrat::parser::CoreTheory::OperatorType = boost::variant<carl::FormulaType>

Definition at line 16 of file Core.h.

Constructor & Destructor Documentation

CoreTheory()

smtrat::parser::CoreTheory::CoreTheory

(

ParserState *

state

)

Definition at line 84 of file Core.cpp.

Here is the call graph for this function:

Member Function Documentation

addConstants()

void smtrat::parser::CoreTheory::addConstants ( qi::symbols< char, types::ConstType > &  constants )

static

Definition at line 79 of file Core.cpp.

addSimpleSorts()

void smtrat::parser::CoreTheory::addSimpleSorts ( qi::symbols< char, carl::Sort > &  sorts )

static

Definition at line 75 of file Core.cpp.

declareQuantifiedTerm()

virtual bool smtrat::parser::AbstractTheory::declareQuantifiedTerm ( const std::vector< std::pair< std::string, carl::Sort >> &  , const carl::FormulaType &  , const types::TermType &  , types::TermType &  , TheoryError &  errors  )

inlinevirtualinherited

Resolve a quantified term.

Reimplemented in smtrat::parser::ArithmeticTheory.

Definition at line 103 of file AbstractTheory.h.

Here is the call graph for this function:

declareVariable()

bool smtrat::parser::CoreTheory::declareVariable ( const std::string &  , const carl::Sort &  , types::VariableType &  , TheoryError &  errors  )

virtual

Declare a new variable with the given name and the given sort.

Reimplemented from smtrat::parser::AbstractTheory.

Definition at line 97 of file Core.cpp.

Here is the call graph for this function:

expandDistinct()

template<typename T , typename Builder >

FormulaT smtrat::parser::AbstractTheory::expandDistinct ( const std::vector< T > &  values, const Builder &  neqBuilder  )

inlineinherited

Definition at line 72 of file AbstractTheory.h.

Here is the caller graph for this function:

functionCall()

bool smtrat::parser::CoreTheory::functionCall ( const Identifier &  , const std::vector< types::TermType > &  , types::TermType &  , TheoryError &  errors  )

virtual

Resolve another unknown function call.

Reimplemented from smtrat::parser::AbstractTheory.

Definition at line 136 of file Core.cpp.

Here is the call graph for this function:

handleDistinct()

bool smtrat::parser::CoreTheory::handleDistinct ( const std::vector< types::TermType > &  , types::TermType &  , TheoryError &  errors  )

virtual

Resolve a distinct operator.

Reimplemented from smtrat::parser::AbstractTheory.

Definition at line 127 of file Core.cpp.

Here is the call graph for this function:

handleITE()

bool smtrat::parser::CoreTheory::handleITE ( const FormulaT &  , const types::TermType &  , const types::TermType &  , types::TermType &  , TheoryError &  errors  )

virtual

Resolve an if-then-else operator.

Reimplemented from smtrat::parser::AbstractTheory.

Definition at line 113 of file Core.cpp.

Here is the call graph for this function:

instantiate()

virtual bool smtrat::parser::AbstractTheory::instantiate ( const types::VariableType &  , const types::TermType &  , types::TermType &  , TheoryError &  errors  )

inlinevirtualinherited

Instantiate a variable within a term.

Reimplemented in smtrat::parser::BitvectorTheory, and smtrat::parser::ArithmeticTheory.

Definition at line 84 of file AbstractTheory.h.

Here is the call graph for this function:

refreshVariable()

virtual bool smtrat::parser::AbstractTheory::refreshVariable ( const types::VariableType &  , types::VariableType &  , TheoryError &  errors  )

inlinevirtualinherited

Reimplemented in smtrat::parser::BitvectorTheory.

Definition at line 88 of file AbstractTheory.h.

Here is the call graph for this function:

resolveSymbol()

virtual bool smtrat::parser::AbstractTheory::resolveSymbol ( const Identifier &  , types::TermType &  , TheoryError &  errors  )

inlinevirtualinherited

Resolve a symbol that was not declared within the ParserState.

This might be a symbol that actually uses indices, for example bitvector constants.

Reimplemented in smtrat::parser::BitvectorTheory.

Definition at line 53 of file AbstractTheory.h.

Here is the call graph for this function:

Field Documentation

state

ParserState* smtrat::parser::AbstractTheory::state

inherited

Definition at line 37 of file AbstractTheory.h.

---

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

• cli/parser/theories/Core.h
• cli/parser/theories/Core.cpp