Implements the theory of bitvectors. More...

#include <Bitvector.h>

Inheritance diagram for smtrat::parser::BitvectorTheory:

Collaboration diagram for smtrat::parser::BitvectorTheory:

[legend]

Public Types
using	OperatorType = carl::BVTermType

Public Member Functions
	BitvectorTheory (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	resolveSymbol (const Identifier &identifier, types::TermType &result, TheoryError &errors)
	Resolve a symbol that was not declared within the ParserState. 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	instantiate (const types::VariableType &var, const types::TermType &replacement, types::TermType &subject, TheoryError &errors)
	Instantiate a variable within a term. More...

bool	refreshVariable (const types::VariableType &var, types::VariableType &subject, TheoryError &errors)

bool	functionCall (const Identifier &identifier, const std::vector< types::TermType > &arguments, types::TermType &result, TheoryError &errors)
	Resolve another unknown function call. More...

template<typename T , typename Builder >
FormulaT	expandDistinct (const std::vector< T > &values, const Builder &neqBuilder)

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

Data Fields
carl::Sort	bvSort

conversion::VectorVariantConverter< types::BVTerm >	vectorConverter

conversion::VariantConverter< types::BVTerm >	termConverter

ParserState *	state

Detailed Description

Implements the theory of bitvectors.

Definition at line 13 of file Bitvector.h.

Member Typedef Documentation

◆ OperatorType

using smtrat::parser::BitvectorTheory::OperatorType = carl::BVTermType

Definition at line 17 of file Bitvector.h.

Constructor & Destructor Documentation

◆ BitvectorTheory()

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

Definition at line 102 of file Bitvector.cpp.

Here is the call graph for this function:

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

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

static

Definition at line 97 of file Bitvector.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::BitvectorTheory::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 149 of file Bitvector.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::BitvectorTheory::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 265 of file Bitvector.cpp.

Here is the call graph for this function:

◆ handleDistinct()

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

virtual

Resolve a distinct operator.

Reimplemented from smtrat::parser::AbstractTheory.

Definition at line 230 of file Bitvector.cpp.

Here is the call graph for this function:

◆ handleITE()

bool smtrat::parser::BitvectorTheory::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 198 of file Bitvector.cpp.

Here is the call graph for this function:

◆ instantiate()

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

virtual

Instantiate a variable within a term.

Reimplemented from smtrat::parser::AbstractTheory.

Definition at line 239 of file Bitvector.cpp.

Here is the call graph for this function:

◆ refreshVariable()

bool smtrat::parser::BitvectorTheory::refreshVariable	(	const types::VariableType &	var,
		types::VariableType &	subject,
		TheoryError &	errors
	)

virtual

Reimplemented from smtrat::parser::AbstractTheory.

Definition at line 254 of file Bitvector.cpp.

Here is the call graph for this function:

◆ resolveSymbol()

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

virtual

Resolve a symbol that was not declared within the ParserState.

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

Reimplemented from smtrat::parser::AbstractTheory.

Definition at line 178 of file Bitvector.cpp.

Here is the call graph for this function:

Field Documentation

◆ bvSort

carl::Sort smtrat::parser::BitvectorTheory::bvSort

Definition at line 14 of file Bitvector.h.

◆ state

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

inherited

Definition at line 37 of file AbstractTheory.h.

◆ termConverter

conversion::VariantConverter<types::BVTerm> smtrat::parser::BitvectorTheory::termConverter

Definition at line 16 of file Bitvector.h.

◆ vectorConverter

conversion::VectorVariantConverter<types::BVTerm> smtrat::parser::BitvectorTheory::vectorConverter

Definition at line 15 of file Bitvector.h.

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

cli/parser/theories/Bitvector.h
cli/parser/theories/Bitvector.cpp

Public Types

Public Member Functions

Static Public Member Functions

Data Fields

Detailed Description

Member Typedef Documentation

◆ OperatorType

Constructor & Destructor Documentation

◆ BitvectorTheory()

Member Function Documentation

◆ addConstants()

◆ addSimpleSorts()

◆ declareQuantifiedTerm()

◆ declareVariable()

◆ expandDistinct()

◆ functionCall()

◆ handleDistinct()

◆ handleITE()

◆ instantiate()

◆ refreshVariable()

◆ resolveSymbol()

Field Documentation

◆ bvSort

◆ state

◆ termConverter

◆ vectorConverter