public abstract class AbstractionPredicate extends java.lang.Object implements java.util.function.Function<Term,Term>, Named
Modifier and Type | Method and Description |
---|---|
abstract Term |
apply(Term t) |
static AbstractionPredicate |
create(Sort argSort,
java.util.function.Function<Term,Term> mapping,
Services services)
Creates a new
AbstractionPredicate with the given name and
mapping. |
static AbstractionPredicate |
create(Term predicate,
LocationVariable placeholder,
Services services)
Creates a new
AbstractionPredicate for the given predicate. |
boolean |
equals(java.lang.Object obj) |
static java.util.List<AbstractionPredicate> |
fromString(java.lang.String s,
Services services,
NamespaceSet localNamespaces)
Parses the String representation of an abstraction predicates.
|
Sort |
getArgSort() |
Pair<LocationVariable,Term> |
getPredicateFormWithPlaceholder() |
java.lang.String |
toParseableString(Services services)
Returns a parseable String representation of this abstraction predicate
of the form "('[[TYPE]] [[PLACEHOLDER]]', '[[PREDICATE]]')".
|
java.lang.String |
toString() |
public Pair<LocationVariable,Term> getPredicateFormWithPlaceholder()
public static AbstractionPredicate create(Sort argSort, java.util.function.Function<Term,Term> mapping, Services services)
AbstractionPredicate
with the given name and
mapping. You may use nice Java 8 lambdas for the second argument!
This method has been created for testing purposes; you should rather user
create(Term, LocationVariable, Services)
instead.
argSort
- The expected sort for the arguments of the predicate.mapping
- The mapping from input terms of the adequate type to formulae,
e.g. "(Term input) -> (tb.gt(input, tb.zero()))" where tb is a
TermBuilder
.services
- The services object.public static AbstractionPredicate create(Term predicate, LocationVariable placeholder, Services services)
AbstractionPredicate
for the given predicate. The
predicate should contain the given placeholder variable, which is
substituted by the argument supplied to the generated mapping.predicate
- The predicate formula containing the placeholder.placeholder
- The placeholder to replace in the generated mapping.services
- The services object.public Sort getArgSort()
public java.lang.String toString()
toString
in class java.lang.Object
public java.lang.String toParseableString(Services services)
services
- The services object.public static java.util.List<AbstractionPredicate> fromString(java.lang.String s, Services services, NamespaceSet localNamespaces) throws ParserException
s
- String
to parse.services
- The Services
object.localNamespaces
- The local NamespaceSet
.String
.ParserException
- If there is a syntax error.javax.naming.NameAlreadyBoundException
- If the given placeholder is already known to the system.SortNotKnownException
- If the given sort is not known to the system.public boolean equals(java.lang.Object obj)
equals
in class java.lang.Object
Copyright © 2003-2019 The KeY-Project.