carl::UFModel Class Reference

Implements a sort value, being a value of the uninterpreted domain specified by this sort. More...

#include <UFModel.h>

Collaboration diagram for carl::UFModel:

Public Member Functions
	UFModel (const UninterpretedFunction &uf)
bool	extend (const std::vector< SortValue > &_args, const SortValue &_value)
SortValue	get (const std::vector< SortValue > &_args) const
const auto &	function () const
const auto &	values () const

Private Attributes
UninterpretedFunction	mFunction
std::map< std::vector< SortValue >, SortValue >	mValues

Detailed Description

Implements a sort value, being a value of the uninterpreted domain specified by this sort.

Definition at line 24 of file UFModel.h.

Constructor & Destructor Documentation

UFModel()

carl::UFModel::UFModel ( const UninterpretedFunction &  uf )

inlineexplicit

Definition at line 30 of file UFModel.h.

Member Function Documentation

extend()

bool carl::UFModel::extend	(	const std::vector< SortValue > &	_args,
		const SortValue &	_value
	)

Definition at line 16 of file UFModel.cpp.

function()

const auto& carl::UFModel::function ( ) const

inline

Definition at line 37 of file UFModel.h.

Here is the caller graph for this function:

get()

SortValue carl::UFModel::get

(

const std::vector< SortValue > &

_args

)

const

Definition at line 21 of file UFModel.cpp.

Here is the call graph for this function:

Here is the caller graph for this function:

values()

const auto& carl::UFModel::values ( ) const

inline

Definition at line 40 of file UFModel.h.

Here is the caller graph for this function:

Field Documentation

mFunction

UninterpretedFunction carl::UFModel::mFunction

private

Definition at line 26 of file UFModel.h.

mValues

std::map<std::vector<SortValue>, SortValue> carl::UFModel::mValues

private

Definition at line 27 of file UFModel.h.

---

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

• carl-formula/uninterpreted/UFModel.h
• carl-formula/uninterpreted/UFModel.cpp