Implements the theory of equalities and uninterpreted functions. More...

#include <Uninterpreted.h>

Inheritance diagram for smtrat::parser::UninterpretedTheory:

Collaboration diagram for smtrat::parser::UninterpretedTheory:

[legend]

Public Member Functions
	UninterpretedTheory (ParserState *state)

FormulaT	coupleBooleanVariables (carl::Variable v, carl::UVariable uv)

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	handleFunctionInstantiation (const carl::UninterpretedFunction &f, const std::vector< types::TermType > &arguments, types::TermType &result, TheoryError &errors)

bool	handleDistinct (const std::vector< types::TermType > &, types::TermType &, 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 > &)
	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
std::map< types::TermType, carl::UTerm >	mInstantiatedArguments

carl::Sort	mBoolSort

carl::UVariable	mTrue

carl::UVariable	mFalse

ParserState *	state

Detailed Description

Implements the theory of equalities and uninterpreted functions.

Definition at line 13 of file Uninterpreted.h.

Constructor & Destructor Documentation

◆ UninterpretedTheory()

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

Definition at line 37 of file Uninterpreted.cpp.

Member Function Documentation

◆ addConstants()

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

inlinestaticinherited

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

inlinestaticinherited

Initialize the global symbol table for simple sorts.

Definition at line 111 of file AbstractTheory.h.

◆ coupleBooleanVariables()

FormulaT smtrat::parser::UninterpretedTheory::coupleBooleanVariables	(	carl::Variable	v,
		carl::UVariable	uv
	)

inline

Definition at line 21 of file Uninterpreted.h.

Here is the caller graph for this function:

◆ 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::UninterpretedTheory::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 47 of file Uninterpreted.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::UninterpretedTheory::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 161 of file Uninterpreted.cpp.

Here is the call graph for this function:

◆ handleDistinct()

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

virtual

Resolve a distinct operator.

Reimplemented from smtrat::parser::AbstractTheory.

Definition at line 152 of file Uninterpreted.cpp.

Here is the call graph for this function:

◆ handleFunctionInstantiation()

bool smtrat::parser::UninterpretedTheory::handleFunctionInstantiation	(	const carl::UninterpretedFunction &	f,
		const std::vector< types::TermType > &	arguments,
		types::TermType &	result,
		TheoryError &	errors
	)

Definition at line 93 of file Uninterpreted.cpp.

Here is the call graph for this function:

Here is the caller graph for this function:

◆ handleITE()

bool smtrat::parser::UninterpretedTheory::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 61 of file Uninterpreted.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

◆ mBoolSort

carl::Sort smtrat::parser::UninterpretedTheory::mBoolSort

Definition at line 15 of file Uninterpreted.h.

◆ mFalse

carl::UVariable smtrat::parser::UninterpretedTheory::mFalse

Definition at line 17 of file Uninterpreted.h.

◆ mInstantiatedArguments

std::map<types::TermType, carl::UTerm> smtrat::parser::UninterpretedTheory::mInstantiatedArguments

Definition at line 14 of file Uninterpreted.h.

◆ mTrue

carl::UVariable smtrat::parser::UninterpretedTheory::mTrue

Definition at line 16 of file Uninterpreted.h.

◆ 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/Uninterpreted.h
cli/parser/theories/Uninterpreted.cpp

Public Member Functions

Static Public Member Functions

Data Fields

Detailed Description

Constructor & Destructor Documentation

◆ UninterpretedTheory()

Member Function Documentation

◆ addConstants()

◆ addSimpleSorts()

◆ coupleBooleanVariables()

◆ declareQuantifiedTerm()

◆ declareVariable()

◆ expandDistinct()

◆ functionCall()

◆ handleDistinct()

◆ handleFunctionInstantiation()

◆ handleITE()

◆ instantiate()

◆ refreshVariable()

◆ resolveSymbol()

Field Documentation

◆ mBoolSort

◆ mFalse

◆ mInstantiatedArguments

◆ mTrue

◆ state