Term Class Reference

Public Types
enum	Type { EXPRESSION, FORMULA }

Public Member Functions
	Term ()
	Default Constructor. It constructs Term(false).
	Term (Expression e)
	Construct a term with e.
	Term (Formula f)
	Construct a term with f.
	Term (const Term &)=default
	Default copy constructor.
	Term (Term &&)=default
	Default move constructor.
Term &	operator= (const Term &)=default
	Default copy assign operator.
Term &	operator= (Term &&)=default
	Default move assign operator.
	~Term ()=default
	Default destructor.
Term &	operator= (Expression e)
	Assignment operator.
Term &	operator= (Formula f)
	Assignment operator.
Type	type () const
	Returns its type.
const Expression &	expression () const
	Returns the expression inside. More...
Expression &	mutable_expression ()
	Returns the expression inside. More...
const Formula &	formula () const
	Returns the formula inside. More...
Formula &	mutable_formula ()
	Returns the formula inside. More...
Term	Substitute (const Variable &v, const Term &t)
	Creates a new term which substitutes the variable v in this term with t. More...
void	Check (Sort s) const
	Checks if this term can be matched with s. More...
void	Check (Variable::Type t) const
	Checks if this term can be matched with t. More...

Member Function Documentation

Check() [1/2]

void Check

(

Sort

s

)

const

Checks if this term can be matched with s.

Throws std::runtime_error if s is mismatched.

Check() [2/2]

void Check

(

Variable::Type

t

)

const

Checks if this term can be matched with t.

Throws std::runtime_error if t is mismatched.

expression()

const Expression & expression

(

)

const

Returns the expression inside.

Exceptions

runtime_error

if it does not include an expression.

formula()

const Formula & formula

(

)

const

Returns the formula inside.

Exceptions

runtime_error

if it does not include a formula.

mutable_expression()

Expression & mutable_expression

(

)

Returns the expression inside.

Exceptions

runtime_error

if it does not include an expression.

mutable_formula()

Formula & mutable_formula

(

)

Returns the formula inside.

Exceptions

runtime_error

if it does not include a formula.

Substitute()

Term Substitute	(	const Variable &	v,
		const Term &	t
	)

Creates a new term which substitutes the variable v in this term with t.

---

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

• /home/soonhokong/work/dreal4/dreal/smt2/term.h
• /home/soonhokong/work/dreal4/dreal/smt2/term.cc