Module dev.civl.sarl

Package dev.civl.sarl.prove.IF

Class ProverFunctionInterpretation

java.lang.Object

dev.civl.sarl.prove.IF.ProverFunctionInterpretation

All Implemented Interfaces:

Comparable<ProverFunctionInterpretation>

public class ProverFunctionInterpretation
extends Object
implements Comparable<ProverFunctionInterpretation>

A data structure that represents the interpretation of a

invalid reference

LogicFunction

. An instance of ProverFunctionInterpretation consists of a String type identifier which identifies a logic function, a list of formal parameters which are SymbolicConstants and a definition which is a SymbolicExpression.

Provers can translate ProverFunctionInterpretation as function definitions in their languages.

Field Summary

Fields

Modifier and Type	Field	Description
final SymbolicExpression	definition
final SymbolicConstant	function
final String	identifier
final SymbolicConstant[]	parameters

Method Summary

Modifier and Type	Method	Description
int	compareTo(ProverFunctionInterpretation o)
boolean	equals(Object obj)
int	hashCode()
static ProverFunctionInterpretation	newProverPredicate(SymbolicUniverse universe, String identifier, SymbolicConstant[] parameters, SymbolicExpression definition)

Methods inherited from class java.lang.Object

getClass, notify, notifyAll, toString, wait, wait, wait

Field Details

definition

public final SymbolicExpression definition

parameters

public final SymbolicConstant[] parameters

function

public final SymbolicConstant function

identifier

public final String identifier

Method Details

newProverPredicate

public static ProverFunctionInterpretation newProverPredicate(SymbolicUniverse universe,
 String identifier,
 SymbolicConstant[] parameters,
 SymbolicExpression definition)

hashCode

public int hashCode()

Overrides:

hashCode in class Object

equals

public boolean equals(Object obj)

Overrides:

equals in class Object

compareTo

public int compareTo(ProverFunctionInterpretation o)

Specified by:

compareTo in interface Comparable<ProverFunctionInterpretation>