public abstract class AbstractionPredicate extends java.lang.Object implements java.util.function.Function<Term,Term>, Named
Modifier and Type | Field and Description |
---|---|
private Sort |
argSort
The sort for the argument of this
AbstractionPredicate . |
private LocationVariable |
placeholderVariable
The placeholder variable occurring in
predicateFormWithPlaceholder which is to be replaced by the
concrete argument of the predicate. |
private Term |
predicateFormWithPlaceholder
The predicate term.
|
Modifier | Constructor and Description |
---|---|
private |
AbstractionPredicate(Sort argSort)
Creates a new
AbstractionPredicate . |
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() |
private Sort argSort
AbstractionPredicate
.private Term predicateFormWithPlaceholder
placeholderVariable
)
which is to be replaced by the concrete argument of the predicate.
This field is needed to save proofs with abstraction predicates.
private LocationVariable placeholderVariable
predicateFormWithPlaceholder
which is to be replaced by the
concrete argument of the predicate.
This field is needed to save proofs with abstraction predicates.s
private AbstractionPredicate(Sort argSort)
AbstractionPredicate
. Constructor is hidden since
elements fo this class should be created by the factory method
#create(String, Function)
.argSort
- The expected sort for the arguments of the predicate.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