de.uni_freiburg.informatik.ultimate.logic

Interface Model

public interface Model

A minimal interface for model queries. The model should represent the model generated by an SMT solver. It should be detached from the solver, i.e., a model retrieved from a solver should not be invalidated by an assertion stack command. Note that the model is not a model of the assertion stack at that time, but we want to give the user the freedom to use the model in an interactive way. Note that symbols defined by model generation might be removed once the assertion stack level is popped off the stack. Values for numeric sorts in linear arithmetic logics are ConstantTerms whose value is of type Rational. For non-numeric sorts, we return some term of the corresponding sort. No further guarantees are made.

Author:

Juergen Christ, Jochen Hoenicke

Method Summary

Modifier and Type	Method and Description
Term	evaluate(Term input) Compute the value of an input term.
java.util.Map<Term,Term>	evaluate(Term[] input) Compute the value of some input terms.
java.util.Set<FunctionSymbol>	getDefinedFunctions() Get the set of function symbols for which the model defines the value.
Term	getFunctionDefinition(java.lang.String func, TermVariable[] args) Get the definition of a function.

Method Detail

evaluate

Term evaluate(Term input)

Compute the value of an input term.

Parameters:

input - Term to evaluate.

Returns:

Value of the term.

evaluate

java.util.Map<Term,Term> evaluate(Term[] input)

Compute the value of some input terms.

Parameters:

input - Terms to evaluate.

Returns:

Values of the terms.

getDefinedFunctions

java.util.Set<FunctionSymbol> getDefinedFunctions()

Get the set of function symbols for which the model defines the value. These is the set of uninterpreted function symbols.

Returns:

The set of function symbols.

getFunctionDefinition

Term getFunctionDefinition(java.lang.String func,
                           TermVariable[] args)

Get the definition of a function. This is a term that can be used as last parameter in a

(define-fun ...)

command.

Parameters:

func - the name of the function

args - the variables that should be used in the returned term to refer to the arguments. Their sort must match the function arguments of the function.

Returns:

The defining term.