Base class for all theories. More...

#include <AbstractTheory.h>

Inheritance diagram for smtrat::parser::AbstractTheory:

[legend]

Collaboration diagram for smtrat::parser::AbstractTheory:

[legend]

Public Member Functions
	AbstractTheory (ParserState *state)

virtual	~AbstractTheory ()

virtual bool	declareVariable (const std::string &, const carl::Sort &, types::VariableType &, TheoryError &errors)
	Declare a new variable with the given name and the given sort. More...

virtual bool	resolveSymbol (const Identifier &, types::TermType &, TheoryError &errors)
	Resolve a symbol that was not declared within the ParserState. More...

virtual bool	handleITE (const FormulaT &, const types::TermType &, const types::TermType &, types::TermType &, TheoryError &errors)
	Resolve an if-then-else operator. More...

virtual bool	handleDistinct (const std::vector< types::TermType > &, types::TermType &, TheoryError &errors)
	Resolve a distinct operator. 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	functionCall (const Identifier &, const std::vector< types::TermType > &, types::TermType &, TheoryError &errors)
	Resolve another unknown function call. More...

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 > &)
	Initialize the global symbol table for simple sorts. More...

static void	addConstants (qi::symbols< char, types::ConstType > &)
	Initialize the global symbol table for constants. More...

Data Fields
ParserState *	state

Detailed Description

Base class for all theories.

A theory represents one or multiple SMT-LIB theories and takes care of converting smtlib constructs into our datastructures.

A theory has two kinds of functions:

Initializer are static functions that initialize global datastructures. These are for example the set of constants.
Handlers are member functions that implement a certain SMT-LIB functionality. Handlers always return a boolean that indicates if the theory could complete the request. Oftentimes, a theory will return false because the request should be handled by another theory. Handlers are used, whenever the parser can not easily decide which theory to use and thus tries to call every theory. The result of a handler is always a term that is returned through a reference argument.

A theory may override any of the following methods.

Definition at line 36 of file AbstractTheory.h.

Constructor & Destructor Documentation

◆ AbstractTheory()

smtrat::parser::AbstractTheory::AbstractTheory ( ParserState * state )

inline

Definition at line 39 of file AbstractTheory.h.

◆ ~AbstractTheory()

virtual smtrat::parser::AbstractTheory::~AbstractTheory ( )

inlinevirtual

Definition at line 40 of file AbstractTheory.h.

Member Function Documentation

◆ addConstants()

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

inlinestatic

Initialize the global symbol table for constants.

Definition at line 115 of file AbstractTheory.h.

◆ addSimpleSorts()

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

inlinestatic

Initialize the global symbol table for simple sorts.

Definition at line 111 of file AbstractTheory.h.

◆ 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
	)

inlinevirtual

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()

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

inlinevirtual

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

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

Definition at line 45 of file AbstractTheory.h.

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
	)

inline

Definition at line 72 of file AbstractTheory.h.

Here is the caller graph for this function:

◆ functionCall()

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

inlinevirtual

Resolve another unknown function call.

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

Definition at line 95 of file AbstractTheory.h.

Here is the call graph for this function:

◆ handleDistinct()

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

inlinevirtual

Resolve a distinct operator.

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

Definition at line 67 of file AbstractTheory.h.

Here is the call graph for this function:

◆ handleITE()

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

inlinevirtual

Resolve an if-then-else operator.

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

Definition at line 60 of file AbstractTheory.h.

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
	)

inlinevirtual

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
	)

inlinevirtual

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
	)

inlinevirtual

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

Definition at line 37 of file AbstractTheory.h.

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

cli/parser/theories/AbstractTheory.h

Public Member Functions

Static Public Member Functions

Data Fields

Detailed Description

Constructor & Destructor Documentation

◆ AbstractTheory()

◆ ~AbstractTheory()

Member Function Documentation

◆ addConstants()

◆ addSimpleSorts()

◆ declareQuantifiedTerm()

◆ declareVariable()

◆ expandDistinct()

◆ functionCall()

◆ handleDistinct()

◆ handleITE()

◆ instantiate()

◆ refreshVariable()

◆ resolveSymbol()

Field Documentation

◆ state