Within this dialog, you can choose predicates used in merges by predicate abstraction.

An abstraction predicate is a unary mapping from terms of suitable type to formulae. You can construct such mappings here by registering placeholder variables (e.g., int i or java.lang.String s) and using those in the predicate definition (e.g., s = null). For each sort of placeholder predicates, a finite lattice for merges with abstraction is constructed.

Thus, it does not make sense to register multiple placeholders of the same type. Furthermore, each abstraction predicate definition must contain exactly one placeholder which then also determines the type of the predicate.

There are three lattice types you can choose; your choice determines how abstract domain elements will be constructed from the given abstraction predicates. Your options are:

Simple Predicates Lattice

This lattice type consists out of a bottom element, one abstract domain element for each of your abstraction predicates, and a top element.

Conjunctive Predicates Lattice

In this lattice, all 2^n combinations of your predicates are combined using conjunction. The iterator of this lattice returns a bottom element, then the conjunction of all n predicates, then all conjunctions of length n-1 of the predicates, and so on. Finally, the top element is returned.

Disjunctive Predicates Lattice

Similar to the conjunctive lattice, but with disjunctions and reversed order: After the bottom element, the next elements correspond to one predicate each, then follow all disjunctions of length 2, and so on. You have to make sure that at most the disjunction of all predicates is valid, but no combination before.