dlinear::smt2::Term Class Reference

Generic term that can be either an expression or a formula. More...

#include <Term.h>

Public Member Functions
	Term ()
	Construct a new term object.
	Term (Expression e)
	Construct a term with the expression e.
	Term (Formula f)
	Construct a term with the formula f.
Type	type () const
	Get read-only access to the type of the term.
const Expression &	expression () const
	Get read-only access to the expression of the term.
Expression &	m_expression ()
	Get read-write access to the expression of the term.
const Formula &	formula () const
	Get read-only access to the formula of the term.
Formula &	m_formula ()
	Get read-write access to the formula of the term.
Term	Substitute (const Variable &v, const Term &t)
	Create a new Term with substitutes the variable v in this term with t.
void	Check (Sort s) const
	Check if this term can be matched with s.
void	Check (Variable::Type t) const
	Check if this term can be matched with t.

Private Attributes
std::variant< Expression, Formula >	term_
	Expression or formula stored by the term.

Detailed Description

Generic term that can be either an expression or a formula.

It is used to store the parsed term from the SMT2 file. They can take many forms, such as:

• variables
• constants
• functions

Definition at line 34 of file Term.h.

Constructor & Destructor Documentation

Term() [1/2]

dlinear::smt2::Term::Term ( Expression e )

explicit

Construct a term with the expression e.

Parameters

e	expression to construct a term with

Definition at line 16 of file Term.cpp.

Term() [2/2]

dlinear::smt2::Term::Term ( Formula f )

explicit

Construct a term with the formula f.

Parameters

f	formula to construct a term with

Definition at line 17 of file Term.cpp.

Member Function Documentation

Check() [1/2]

void dlinear::smt2::Term::Check

(

Sort

s

)

const

Check if this term can be matched with s.

Parameters

s	sort to match with

Exceptions

std::runtime_error

if s is mismatched

Definition at line 72 of file Term.cpp.

Check() [2/2]

void dlinear::smt2::Term::Check

(

Variable::Type

t

)

const

Check if this term can be matched with t.

Parameters

t	type of the variable

Exceptions

std::runtime_error

if t is mismatched

Definition at line 85 of file Term.cpp.

expression()

const Expression & dlinear::smt2::Term::expression ( ) const

nodiscard

Get read-only access to the expression of the term.

Exceptions

std::std::bad_variant_access

if it does not include a expression

Returns

expression of the term

Definition at line 36 of file Term.cpp.

formula()

const Formula & dlinear::smt2::Term::formula ( ) const

nodiscard

Get read-only access to the formula of the term.

Exceptions

std::std::bad_variant_access

if it does not include a formula

Returns

formula of the term

Definition at line 38 of file Term.cpp.

m_expression()

Expression & dlinear::smt2::Term::m_expression

(

)

Get read-write access to the expression of the term.

Exceptions

std::std::bad_variant_access

if it does not include a expression

Returns

expression of the term

Definition at line 37 of file Term.cpp.

m_formula()

Formula & dlinear::smt2::Term::m_formula

(

)

Get read-write access to the formula of the term.

Exceptions

std::std::bad_variant_access

if it does not include a formula

Returns

formula of the term

Definition at line 39 of file Term.cpp.

Substitute()

Term dlinear::smt2::Term::Substitute	(	const Variable &	v,
		const Term &	t )

Create a new Term with substitutes the variable v in this term with t.

Parameters

v	variable to substitute
t	new term that replaces the variable

Returns

new term with the substitution

Definition at line 41 of file Term.cpp.

type()

Term::Type dlinear::smt2::Term::type ( ) const

nodiscard

Get read-only access to the type of the term.

Returns

type of the term

Definition at line 35 of file Term.cpp.

---

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

• dlinear/parser/smt2/Term.h
• dlinear/parser/smt2/Term.cpp