dlinear::smt2::FunctionDefinition Class Reference

A new function defined by the user in the SMT2 language using the define-fun command. More...

#include <FunctionDefinition.h>

Public Member Functions
	FunctionDefinition (std::vector< Variable > parameters, Sort return_type, Term body)
	Construct a new function definition.
Term	operator() (const std::vector< Term > &arguments) const
	Call the function with the given arguments.
Term	operator() (std::same_as< Term > auto... arguments) const
	Call the function with the given arguments.

Private Attributes
std::vector< Variable >	parameters_
	Parameters of the function.
Sort	return_type_
	Return type of the function.
Term	body_
	Body of the function.

Detailed Description

A new function defined by the user in the SMT2 language using the define-fun command.

In the SMT2 language, a function definition is a way to define a function in terms of its parameters and body. A function defined in this way can be called with the operator() method by providing the required arguments.

// Example usage:
const Variable lhs{"lhs"}, rhs{"rhs"};
const FunctionDefinition fun_sum{{lhs_, rhs_}, Sort::Real, Term{lhs_ + rhs_}};
 
Term res = fun_sum(Term{5}, Term{6});
 
std::cout << res << std::endl;
// Output:
// 11

Definition at line 40 of file FunctionDefinition.h.

Constructor & Destructor Documentation

FunctionDefinition()

dlinear::smt2::FunctionDefinition::FunctionDefinition	(	std::vector< Variable >	parameters,
		Sort	return_type,
		Term	body )

Construct a new function definition.

The function will accept parameters of the given types and return a value of the given type when called.

Parameters

parameters	parameters of the function
return_type	return type of the function
body	body of the function

Definition at line 14 of file FunctionDefinition.cpp.

Member Function Documentation

operator()() [1/2]

Term dlinear::smt2::FunctionDefinition::operator()

(

const std::vector< Term > &

arguments

)

const

Call the function with the given arguments.

Parameters

arguments

arguments to the function

Returns

the result of the function

Definition at line 19 of file FunctionDefinition.cpp.

operator()() [2/2]

Term dlinear::smt2::FunctionDefinition::operator() ( std::same_as< Term > auto... arguments ) const

inline

Call the function with the given arguments.

Parameters

arguments

arguments to the function

Returns

the result of the function

Definition at line 63 of file FunctionDefinition.h.

---

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

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