Implements the theory of bitvectors. More...

#include <BooleanEncoding.h>

Inheritance diagram for smtrat::parser::BooleanEncodingTheory:

Collaboration diagram for smtrat::parser::BooleanEncodingTheory:

[legend]

Public Member Functions
	BooleanEncodingTheory (ParserState *state)

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

Implements the theory of bitvectors.

Definition at line 13 of file BooleanEncoding.h.

Constructor & Destructor Documentation

◆ BooleanEncodingTheory()

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

Definition at line 59 of file BooleanEncoding.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()

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.

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

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

inlinevirtualinherited

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
	)

inlineinherited

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
	)

inlinevirtualinherited

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
	)

inlinevirtualinherited

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
	)

inlinevirtualinherited

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
	)

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

Public Member Functions

Static Public Member Functions

Data Fields

Detailed Description

Constructor & Destructor Documentation

◆ BooleanEncodingTheory()

Member Function Documentation

◆ addConstants()

◆ addSimpleSorts()

◆ declareQuantifiedTerm()

◆ declareVariable()

◆ expandDistinct()

◆ functionCall()

◆ handleDistinct()

◆ handleITE()

◆ instantiate()

◆ refreshVariable()

◆ resolveSymbol()

Field Documentation

◆ state