Object
- Ppt
- - PptTopLevel

All Implemented Interfaces:

Serializable

Direct Known Subclasses:

PptConditional
```
public class PptTopLevel
extends Ppt
```
All information about a single program point. A Ppt may also represent just part of the data: see PptConditional.
PptTopLevel doesn't do any direct computation, instead deferring that to its views that are slices and that actually contain the invariants.
The data layout is as follows:
- A PptMap is a collection of PptTopLevel objects.
- A PptTopLevel contains PptSlice objects, one for each set of variables at the program point. For instance, if a PptTopLevel has variables a, b, and c, then it has three PptSlice1 objects (one for a; one for b; and one for c), three PptSlice2 objects (one for a,b; one for a,c; and one for b,c), and one PptSlice3 object (for a,b,c).
- A PptSlice object contains invariants. When a sample (a tuple of variable values) is fed to a PptTopLevel, it in turn feeds it to all the slices, which feed it to all the invariants, which act on it appropriately.
See Also:

Serialized Form

Nested Class Summary

Nested Classes
Modifier and Type	Class	Description
`class`	`PptTopLevel.CondIterator`	Iterator for all of the conditional ppts.
`static class`	`PptTopLevel.PptFlags`	Ppt attributes (specified in decl records)
`static class`	`PptTopLevel.PptType`	Possible types of program points.
`static interface`	`PptTopLevel.SimplifyInclusionTester`	Interface used by mark_implied_via_simplify to determine what invariants should be considered during the logical redundancy tests.
`static class`	`PptTopLevel.Stats`	Stores various statistics about a ppt.
`static class`	`PptTopLevel.ViewsIteratorIterator`	An iterator whose elements are themselves iterators that return invariants.

Nested classes/interfaces inherited from class Ppt
Ppt.NameComparator

Field Summary

Fields
Modifier and Type	Field	Description
`List<PptRelation>`	`children`	All children relations in the variable/ppt hierarchy.
`@MonotonicNonNull DynamicConstants`	`constants`	List of constant variables.
`static Logger`	`debug`	Main debug tracer.
`static Logger`	`debugAddImplications`	Debug tracer for addImplications.
`static Logger`	`debugConditional`	Debug tracer for adding and processing conditional ppts.
`static Logger`	`debugEqualTo`	Debug tracer for equalTo checks.
`static Logger`	`debugFlow`	Debug tracer for data flow.
`static Logger`	`debugInstantiate`	Debug tracer for instantiated slices.
`static Logger`	`debugMerge`	Debug tracer for up-merging equality sets.
`static Logger`	`debugNISStats`	Debug tracer for NIS suppression statistics.
`static Logger`	`debugTimeMerge`	Debug tracer for timing merges.
`static boolean`	`dkconfig_pairwise_implications`	Boolean.
`static boolean`	`dkconfig_remove_merged_invs`	Remove invariants at lower program points when a matching invariant is created at a higher program point.
`@MonotonicNonNull PptSliceEquality`	`equality_view`	Holds Equality invariants.
`static boolean`	`first_pass_with_sample`	Boolean.
`EnumSet<PptTopLevel.PptFlags>`	`flags`	Attributes of this ppt.
`static Comparator<Invariant>`	`icfp`
`boolean`	`in_merge`
`int`	`instantiated_inv_cnt`	Number of invariants after equality set processing for the last sample.
`int`	`instantiated_slice_cnt`	Number of slices after equality set processing for the last sample.
`boolean`	`invariants_merged`	Flag that indicates whether or not invariants have been merged from all of this ppts children to form the invariants here.
`boolean`	`invariants_removed`	Flag that indicates whether or not invariants that are duplicated at the parent have been removed..
`PptSlice0`	`joiner_view`	Contains invariants that represent a "joining" of two others: implications, and, or, etc.
`String`	`name`
`int`	`num_declvars`
`int`	`num_orig_vars`
`int`	`num_static_constant_vars`
`int`	`num_tracevars`
`List<FileIO.ParentRelation>`	`parent_relations`	List of parent relations in the variable/ppt hierarchy as specified in the declaration record.
`List<PptRelation>`	`parents`	All parent relations in the variable/ppt hierarchy.
`PptName`	`ppt_name`
`Set<Invariant>`	`redundant_invs`	Redundant invariants, except for Equality invariants.
`Set<VarInfo>`	`redundant_invs_equality`	The canonical VarInfo for the equality.
`@MonotonicNonNull ArrayList<PptSplitter>`	`splitters`	List of all of the splitters for this ppt.
`PptTopLevel.PptType`	`type`	Type of this program point.

Fields inherited from class Ppt
emptyInvList, var_infos

Constructor Summary

Constructors
Constructor	Description
`PptTopLevel(String name, PptTopLevel.PptType type, List<FileIO.ParentRelation> parents, EnumSet<PptTopLevel.PptFlags> flags, VarInfo[] var_infos)`
`PptTopLevel(String name, VarInfo[] var_infos)`

Method Summary

All Methods Static Methods Instance Methods Concrete Methods
Modifier and Type	Method	Description
`@Nullable Set<Invariant>`	`add_bottom_up(ValueTuple vt, int count)`	Add the sample to the equality sets, dynamic constants, and invariants at this program point.
`void`	`addConditions(Splitter[] splits)`
`void`	`addImplications()`	Given conditional program points (and invariants detected over them), create implications.
`void`	`addSlice(PptSlice slice)`	Add a single slice to the views variable.
`void`	`addViews(List<PptSlice> slices_vector)`	Add the specified slices to this ppt.
`static int[]`	`build_permute(VarInfo[] vis1, VarInfo[] vis2)`	Builds a permutation from vis1 to vis2.
`boolean`	`check_implied(DiscardInfo di, VarInfo v1, VarInfo v2, Invariant proto)`
`@Nullable DiscardInfo`	`check_implied(Invariant imp_inv, VarInfo v, Invariant proto)`	If the prototype invariant is true over the specified variable returns DiscardInfo indicating that the prototype invariant implies imp_inv.
`@Nullable DiscardInfo`	`check_implied(Invariant imp_inv, VarInfo v1, VarInfo v2, Invariant proto)`	If the prototype invariant is true over the specified variables returns DiscardInfo indicating that the prototype invariant implies imp_inv.
`boolean`	`check_implied_canonical(DiscardInfo di, VarInfo v1, VarInfo v2, Invariant proto)`
`@Nullable DiscardInfo`	`check_implied_canonical(Invariant imp_inv, VarInfo v, Invariant proto)`	If the proto invariant is true over the leader of the specified variable returns DiscardInfo indicating that the proto invariant implies imp_inv.
`@Nullable DiscardInfo`	`check_implied_canonical(Invariant imp_inv, VarInfo v1, VarInfo v2, Invariant proto)`	If the prototype invariant is true over the leader of each specified variables returns DiscardInfo indicating that the prototype invariant implies imp_inv.
`void`	`clean_for_merge()`	Cleans up the ppt so that its invariants can be merged from other ppts.
`Iterable<PptConditional>`	`cond_iterable()`	returns an iterable over all of the PptConditionals at this ppt
`PptTopLevel.CondIterator`	`cond_iterator()`	returns an iterator over all of the PptConditionals at this ppt
`int`	`const_inv_cnt()`	Returns the number of invariants that contain one or more constants.
`int`	`const_slice_cnt()`	Returns the number of slices that contain one or more constants.
`void`	`create_derived_variables()`	Create all the derived variables.
`PptSlice`	`create_equality_inv(VarInfo v1, VarInfo v2, int samples)`	Create an equality invariant over the specified variables.
`void`	`debug_invs(Logger log)`	Debug print to the specified logger information about each invariant at this ppt.
`void`	`debug_print_slice_info(Logger log, String descr, List<PptSlice> slices)`	Debug print slice/inv count information to the specified logger.
`void`	`debug_print_tree(Logger l, int indent, @Nullable PptRelation parent_rel)`	Debug method to print children (in the partial order) recursively.
`void`	`debug_unary_info(Logger log)`	Debug print to the specified logger information about each variable in this ppt.
`String`	`debugSlices()`	Debug method to display all slices.
`String`	`equality_sets_txt()`	Returns a string version of all of the equality sets for this ppt.
`@Nullable List<Invariant>`	`find_assignment_inv(VarInfo v)`	Searches for all of the invariants that that provide an exact value for v.
`@Nullable Invariant`	`find_inv_by_class(VarInfo[] vis, Class<? extends Invariant> cls)`	Returns the invariant in the slice specified by vis that matches the specified class.
`@Nullable PptSlice1`	`findSlice(VarInfo v)`	Returns the unary slice over v.
`@Nullable PptSlice`	`findSlice(VarInfo[] vis)`	Find a pptSlice with an assumed ordering.
`@Nullable PptSlice2`	`findSlice(VarInfo v1, VarInfo v2)`	Returns the binary slice over v1 and v2.
`@Nullable PptSlice3`	`findSlice(VarInfo v1, VarInfo v2, VarInfo v3)`	Returns the ternary slice over v1, v2, and v3.
`@Nullable PptSlice`	`findSlice_unordered(VarInfo[] vis)`	Find a pptSlice without an assumed ordering.
`@Nullable PptSlice2`	`findSlice_unordered(VarInfo v1, VarInfo v2)`	Like findSlice, but it is not required that the variables be supplied in order of varinfo_index.
`@Nullable PptSlice3`	`findSlice_unordered(VarInfo v1, VarInfo v2, VarInfo v3)`	Like findSlice, but it is not required that the variables be supplied in order of varinfo_index.
`static boolean`	`format_simplify_problem(String s)`	Returns true if there was a problem with Simplify formatting (such as the invariant not having a Simplify representation).
`void`	`get_missingOutOfBounds(PptTopLevel ppt, ValueTuple vt)`	Gets any missing out of bounds variables from the specified ppt and applies them to the matching variable in this ppt if the variable is MISSING_NONSENSICAL.
`PptSlice`	`get_or_instantiate_slice(VarInfo vi)`	Return a slice that contains the given VarInfos (creating if needed).
`PptSlice`	`get_or_instantiate_slice(VarInfo[] vis)`	Return a slice that contains the given VarInfos (creating if needed).
`PptSlice`	`get_or_instantiate_slice(VarInfo v1, VarInfo v2)`	Return a slice that contains the given VarInfos (creating if needed).
`PptSlice`	`get_or_instantiate_slice(VarInfo v1, VarInfo v2, VarInfo v3)`	Return a slice that contains the given VarInfos (creating if needed).
`PptSlice`	`get_temp_slice(VarInfo v)`	Looks up the slice for v1.
`PptSlice`	`get_temp_slice(VarInfo v1, VarInfo v2)`	Looks up the slice for v1 and v2.
`List<Invariant>`	`getInvariants()`	Return a List of all the invariants for the program point.
`Set<VarInfo>`	`getParamVars()`	Returns variables in this Ppt that are parameters.
`static @Nullable LemmaStack`	`getProverStack()`
`boolean`	`has_parent(VarInfo v)`	Returns whether or not the specified variable in this ppt has any parents.
`boolean`	`has_splitters()`	Returns whether or not this ppt has any splitters.
`void`	`incSampleNumber()`	Increments the number of samples processed by the program point by 1.
`void`	`instantiate_views_and_invariants()`	This function creates all the views (and thus candidate invariants), but does not check those invariants.
`List<Invariant>`	`inv_add(List<Invariant> inv_list, ValueTuple vt, int count)`	Adds a sample to each invariant in the list.
`int`	`invariant_cnt()`	Returns the number of true invariants at this ppt.
`Map<Class<? extends Invariant>,PptTopLevel.Cnt>`	`invariant_cnt_by_class()`	Returns how many invariants there are of each invariant class.
`Iterator<Invariant>`	`invariants_iterator()`	Iterate over all of the invariants at this ppt (but not any implications).
`List<Invariant>`	`invariants_vector()`	ArrayList version of `getInvariants()`.
`boolean`	`is_class()`	Is this a ppt that represents a class?
`boolean`	`is_combined_exit()`	Is this a combined exit point?
`boolean`	`is_constant(VarInfo v)`	Returns whether or not the specified variable is dynamically constant.
`boolean`	`is_empty(VarInfo varr)`	Returns true if varr is empty.
`boolean`	`is_enter()`	is this an enter ppt
`boolean`	`is_equal(VarInfo v1, VarInfo v2)`	Returns whether or not the specified variables are equal (ie, an equality invariant exists between them).
`boolean`	`is_exit()`	Is this is an exit ppt (combined or specific)?
`boolean`	`is_less_equal(VarInfo v1, int v1_shift, VarInfo v2, int v2_shift)`	Returns true if (v1+v1_shift) ≤ (v2+v2_shift) is known to be true.
`boolean`	`is_missing(VarInfo v)`	Returns whether or not the specified variable has been missing for all samples seen so far.
`boolean`	`is_nonzero(VarInfo v)`	Returns whether or not v1 is always non-zero.
`boolean`	`is_object()`	Is this a ppt that represents an object?
`boolean`	`is_prev_constant(VarInfo v)`	Returns whether or not the specified variable is currently dynamically constant, or was a dynamic constant at the beginning of constant processing.
`boolean`	`is_prev_missing(VarInfo v)`	returns whether the specified variable is currently missing OR was missing at the beginning of constants processing.
`boolean`	`is_slice_ok(VarInfo var1)`	Returns whether or not the specified unary slice should be created.
`boolean`	`is_slice_ok(VarInfo[] vis, int arity)`	Returns whether or not the specified slice should be created.
`boolean`	`is_slice_ok(VarInfo var1, VarInfo var2)`	Returns whether or not the specified binary slice should be created.
`boolean`	`is_slice_ok(VarInfo v1, VarInfo v2, VarInfo v3)`	Returns whether or not the specified ternary slice should be created by checking the variables' qualifications.
`boolean`	`is_subexit()`	Is this a numbered (specific) exit point?
`boolean`	`is_subsequence(VarInfo v1, VarInfo v2)`	Returns true if v1 is known to be a subsequence of v2.
`boolean`	`is_subset(VarInfo v1, VarInfo v2)`	Returns whether or not v1 is a subset of v2.
`void`	`mark_implied_via_simplify(PptMap all_ppts)`	Use the Simplify theorem prover to flag invariants that are logically implied by others.
`void`	`merge_conditionals()`	Merges the conditionals from the children of this ppt to this ppt.
`void`	`merge_invs_multiple_children()`	Merges the invariants from multiple children.
`void`	`merge_invs_one_child()`	Merges one child.
`void`	`mergeInvs()`	Recursively merge invariants from children to create an invariant list at this ppt.
`String`	`name()`
`int`	`num_array_vars()`
`int`	`num_samples()`	The number of samples processed by this program point so far.
`int`	`num_samples(VarInfo vi1)`	Return the number of samples where vi1 is present (not missing)
`int`	`num_samples(VarInfo vi1, VarInfo vi2)`	Return the number of samples where vi1 and vi2 are both present (not missing).
`int`	`num_samples(VarInfo vi1, VarInfo vi2, VarInfo vi3)`	Return the number of samples where vi1, vi2, and vi3 are all present (not missing).
`int`	`num_values(VarInfo vi1)`	The number of distinct values that have been seen.
`int`	`num_values(VarInfo vi1, VarInfo vi2)`	An upper bound on the number of distinct pairs of values that have been seen.
`int`	`num_values(VarInfo vi1, VarInfo vi2, VarInfo vi3)`	An upper bound on the number of distinct values over vi1, vi2, and vi3 that have been seen.
`int`	`numViews()`
`VarInfo @Nullable []`	`parent_vis(PptRelation rel, PptSlice slice)`	Creates a list of parent variables (i.e., variables at the parent program point) that matches slice.
`void`	`postProcessEquality()`	Two things: a) convert Equality invariants into normal IntEqual type for filtering, printing, etc. b) Pivot uninteresting parameter VarInfos so that each equality set contains only the interesting one.
`static void`	`print_equality_stats(Logger log, PptMap all_ppts)`	Print statistics concerning equality sets over the entire set of ppts to the specified logger.
`void`	`processOmissions(boolean[] omitTypes)`	Remove invariants that are marked for omission in omitTypes.
`void`	`remove_child_invs(PptRelation rel)`	Removes any invariant in this ppt which has a matching invariant in the parent (as specified in the relation).
`void`	`remove_equality_invariants()`	Remove the equality invariants added during equality post processing.
`void`	`remove_implications()`	Remove all of the implications from this program point.
`void`	`remove_invs(List<Invariant> rm_list)`	Remove a list of invariants.
`void`	`removeSlice(PptSlice slice)`	Remove a slice from this PptTopLevel.
`void`	`repCheck()`	Check the rep invariants of this.
`void`	`simplify_variable_names()`	Simplify the names of variables before printing them.
`int`	`slice_cnt()`	Returns the number of slices at this ppt.
`String`	`toString()`	Returns the full name of the ppt.
`void`	`trimToSize()`	Trim the collections used here, in hopes of saving space.
`Iterator<VarInfo>`	`var_info_iterator()`	Iterate through each variable at this ppt.
`String`	`var_names()`
`Iterable<PptSlice>`	`views_iterable()`	For some clients, this method may be more efficient than getInvariants.
`Iterator<PptSlice>`	`views_iterator()`	For some clients, this method may be more efficient than getInvariants.
`boolean`	`vis_order_ok(VarInfo[] vis)`	Determines whether the order of the variables in vis is a valid permutation (i.e., their varinfo_index's are ordered).
`static boolean`	`worthDerivingFrom(VarInfo vi)`

Methods inherited from class Ppt
containsVar, find_var_by_name, indexOf, varNames, varNames

Methods inherited from class Object
clone, equals, finalize, getClass, hashCode, notify, notifyAll, wait, wait, wait

- Field Detail
  - dkconfig_pairwise_implications
```
public static boolean dkconfig_pairwise_implications
```
    Boolean. If true, create implications for all pairwise combinations of conditions, and all pairwise combinations of exit points. If false, create implications for only the first two conditions, and create implications only if there are exactly two exit points.
  - dkconfig_remove_merged_invs
```
public static boolean dkconfig_remove_merged_invs
```
    Remove invariants at lower program points when a matching invariant is created at a higher program point. For experimental purposes only.
  - first_pass_with_sample
```
public static boolean first_pass_with_sample
```
    Boolean. Needed by the NIS.falsified method when keeping stats to figure out how many falsified invariants are antecedents. Only the first pass of processing with the sample is counted toward the stats.
  - flags
```
public EnumSet<PptTopLevel.PptFlags> flags
```
    Attributes of this ppt.
  - type
```
public PptTopLevel.PptType type
```
    Type of this program point.
  - instantiated_inv_cnt
```
public int instantiated_inv_cnt
```
    Number of invariants after equality set processing for the last sample.
  - instantiated_slice_cnt
```
public int instantiated_slice_cnt
```
    Number of slices after equality set processing for the last sample.
  - debug
```
public static final Logger debug
```
    Main debug tracer.
  - debugInstantiate
```
public static final Logger debugInstantiate
```
    Debug tracer for instantiated slices.
  - debugTimeMerge
```
public static final Logger debugTimeMerge
```
    Debug tracer for timing merges.
  - debugEqualTo
```
public static final Logger debugEqualTo
```
    Debug tracer for equalTo checks.
  - debugAddImplications
```
public static final Logger debugAddImplications
```
    Debug tracer for addImplications.
  - debugConditional
```
public static final Logger debugConditional
```
    Debug tracer for adding and processing conditional ppts.
  - debugFlow
```
public static final Logger debugFlow
```
    Debug tracer for data flow.
  - debugMerge
```
public static final Logger debugMerge
```
    Debug tracer for up-merging equality sets.
  - debugNISStats
```
public static final Logger debugNISStats
```
    Debug tracer for NIS suppression statistics.
  - name
```
public final String name
```
  - ppt_name
```
public final PptName ppt_name
```
  - constants
```
public @MonotonicNonNull DynamicConstants constants
```
    List of constant variables. Null unless DynamicConstants.dkconfig_use_dynamic_constant_optimization is set.
  - num_declvars
```
public int num_declvars
```
  - num_tracevars
```
public int num_tracevars
```
  - num_orig_vars
```
public int num_orig_vars
```
  - num_static_constant_vars
```
public int num_static_constant_vars
```
  - splitters
```
public @MonotonicNonNull ArrayList<PptSplitter> splitters
```
    List of all of the splitters for this ppt.
  - children
```
public List<PptRelation> children
```
    All children relations in the variable/ppt hierarchy.
  - parents
```
public List<PptRelation> parents
```
    All parent relations in the variable/ppt hierarchy.
  - parent_relations
```
public List<FileIO.ParentRelation> parent_relations
```
    List of parent relations in the variable/ppt hierarchy as specified in the declaration record. These are used to build the detailed parents/children lists of PptRelation above.
  - invariants_merged
```
public boolean invariants_merged
```
    Flag that indicates whether or not invariants have been merged from all of this ppts children to form the invariants here. Necessary because a ppt can have multiple parents and otherwise we'd needlessly merge multiple times.
  - in_merge
```
public boolean in_merge
```
  - invariants_removed
```
public boolean invariants_removed
```
    Flag that indicates whether or not invariants that are duplicated at the parent have been removed..
  - joiner_view
```
public PptSlice0 joiner_view
```
    Contains invariants that represent a "joining" of two others: implications, and, or, etc.
  - equality_view
```
public @MonotonicNonNull PptSliceEquality equality_view
```
    Holds Equality invariants. Never null after invariants are instantiated.
  - redundant_invs
```
public Set<Invariant> redundant_invs
```
    Redundant invariants, except for Equality invariants.
  - redundant_invs_equality
```
public Set<VarInfo> redundant_invs_equality
```
    The canonical VarInfo for the equality.
  - icfp
```
public static final Comparator<Invariant> icfp
```
- Constructor Detail
  - PptTopLevel
```
public PptTopLevel(String name,
                   PptTopLevel.PptType type,
                   List<FileIO.ParentRelation> parents,
                   EnumSet<PptTopLevel.PptFlags> flags,
                   VarInfo[] var_infos)
```
  - PptTopLevel
```
public PptTopLevel(String name,
                   VarInfo[] var_infos)
```
- Method Detail
  - name
```
@Pure
public String name(@GuardSatisfied @UnknownInitialization(PptTopLevel.class) PptTopLevel this)
```
    Specified by:
    
    name in class Ppt
  - cond_iterator
```
public PptTopLevel.CondIterator cond_iterator()
```
    returns an iterator over all of the PptConditionals at this ppt
    
    See Also:
    
    cond_iterable()
  - cond_iterable
```
public Iterable<PptConditional> cond_iterable()
```
    returns an iterable over all of the PptConditionals at this ppt
    
    See Also:
    
    cond_iterator()
  - has_splitters
```
@EnsuresNonNullIf(result=true,
                  expression="splitters")
public boolean has_splitters()
```
    Returns whether or not this ppt has any splitters.
    
    Returns:
    
    whether or not this ppt has any splitters
  - num_array_vars
```
public int num_array_vars()
```
  - var_info_iterator
```
public Iterator<VarInfo> var_info_iterator()
```
    Iterate through each variable at this ppt.
  - toString
```
@SideEffectFree
public String toString(@GuardSatisfied PptTopLevel this)
```
    Returns the full name of the ppt.
    
    Overrides:
    
    toString in class Object
  - trimToSize
```
public void trimToSize()
```
    Trim the collections used here, in hopes of saving space.
    
    Overrides:
    
    trimToSize in class Ppt
  - num_samples
```
public int num_samples()
```
    The number of samples processed by this program point so far.
  - num_samples
```
public int num_samples(VarInfo vi1)
```
    Return the number of samples where vi1 is present (not missing)
  - num_samples
```
public int num_samples(VarInfo vi1,
                       VarInfo vi2)
```
    Return the number of samples where vi1 and vi2 are both present (not missing).
  - num_samples
```
public int num_samples(VarInfo vi1,
                       VarInfo vi2,
                       VarInfo vi3)
```
    Return the number of samples where vi1, vi2, and vi3 are all present (not missing).
  - num_values
```
public int num_values(VarInfo vi1)
```
    The number of distinct values that have been seen.
  - num_values
```
public int num_values(VarInfo vi1,
                      VarInfo vi2)
```
    An upper bound on the number of distinct pairs of values that have been seen. Note that there can't be more pairs of values than there are samples. This matters when there are very few samples due to one of the variables being missing.
  - num_values
```
public int num_values(VarInfo vi1,
                      VarInfo vi2,
                      VarInfo vi3)
```
    An upper bound on the number of distinct values over vi1, vi2, and vi3 that have been seen. Note that there can't be more pairs of values than there are samples. This matters when there are very few samples due to one of the variables being missing.
  - numViews
```
public int numViews()
```
  - worthDerivingFrom
```
public static boolean worthDerivingFrom(VarInfo vi)
```
  - add_bottom_up
```
@RequiresNonNull({"daikon.suppress.NIS.suppressor_map","daikon.suppress.NIS.suppressor_map_suppression_count","daikon.suppress.NIS.all_suppressions","daikon.suppress.NIS.suppressor_proto_invs"})
public @Nullable Set<Invariant> add_bottom_up(ValueTuple vt,
                                              int count)
```
    Add the sample to the equality sets, dynamic constants, and invariants at this program point. This version is specific to the bottom up processing mechanism.
    This routine also instantiates slices/invariants on the first call for the ppt.
    
    Parameters:
    
    vt - the set of values for this to see
    
    count - the number of samples that vt represents
    
    Returns:
    
    the set of all invariants weakened or falsified by this sample
  - inv_add
```
public List<Invariant> inv_add(List<Invariant> inv_list,
                               ValueTuple vt,
                               int count)
```
    Adds a sample to each invariant in the list. Returns the list of weakened invariants. This should only be called when the sample has already been added to the slice containing each invariant. Otherwise the statistics kept in the slice will be incorrect.
    
    Parameters:
    
    inv_list - the invariants to add the sample to
    
    vt - the sample
    
    count - how many instances of the sample to add
    
    Returns:
    
    the invariants that were weakened
  - get_missingOutOfBounds
```
public void get_missingOutOfBounds(PptTopLevel ppt,
                                   ValueTuple vt)
```
    Gets any missing out of bounds variables from the specified ppt and applies them to the matching variable in this ppt if the variable is MISSING_NONSENSICAL. The goal is to set the missing_array_bounds flag only if it was missing in ppt on THIS sample.
    This could fail if missing_array_bounds was set on a previous sample and the MISSING_NONSENSICAL flag is set for a different reason on this sample. This could happen with an array in an object.
    This implementation is also not particularly efficient and the variables must match exactly.
    Missing out of bounds really needs to be implemented as a separate flag in the missing bits. That would clear up all of this mess.
  - is_constant
```
@EnsuresNonNullIf(result=true,
                  expression="constants")
@Pure
public boolean is_constant(VarInfo v)
```
    Returns whether or not the specified variable is dynamically constant.
  - is_prev_constant
```
@EnsuresNonNullIf(result=true,
                  expression="constants")
@Pure
public boolean is_prev_constant(VarInfo v)
```
    Returns whether or not the specified variable is currently dynamically constant, or was a dynamic constant at the beginning of constant processing.
  - is_missing
```
@EnsuresNonNullIf(result=true,
                  expression="constants")
@Pure
public boolean is_missing(VarInfo v)
```
    Returns whether or not the specified variable has been missing for all samples seen so far.
  - is_prev_missing
```
@EnsuresNonNullIf(result=true,
                  expression="constants")
@Pure
public boolean is_prev_missing(VarInfo v)
```
    returns whether the specified variable is currently missing OR was missing at the beginning of constants processing.
  - invariant_cnt
```
public int invariant_cnt()
```
    Returns the number of true invariants at this ppt.
  - const_slice_cnt
```
public int const_slice_cnt()
```
    Returns the number of slices that contain one or more constants.
  - const_inv_cnt
```
public int const_inv_cnt()
```
    Returns the number of invariants that contain one or more constants.
  - debug_invs
```
@RequiresNonNull("daikon.suppress.NIS.suppressor_map")
public void debug_invs(Logger log)
```
    Debug print to the specified logger information about each invariant at this ppt.
  - debug_unary_info
```
public void debug_unary_info(Logger log)
```
    Debug print to the specified logger information about each variable in this ppt. Currently only prints integer and float information using the bound invariants.
  - invariant_cnt_by_class
```
public Map<Class<? extends Invariant>,PptTopLevel.Cnt> invariant_cnt_by_class()
```
    Returns how many invariants there are of each invariant class. The map is from the invariant class to an integer cnt of the number of that class.
  - slice_cnt
```
public int slice_cnt()
```
    Returns the number of slices at this ppt.
  - create_derived_variables
```
public void create_derived_variables()
```
    Create all the derived variables.
  - addViews
```
public void addViews(List<PptSlice> slices_vector)
```
    Add the specified slices to this ppt.
  - addSlice
```
public void addSlice(PptSlice slice)
```
    Add a single slice to the views variable.
  - removeSlice
```
public void removeSlice(PptSlice slice)
```
    Remove a slice from this PptTopLevel.
  - remove_invs
```
public void remove_invs(List<Invariant> rm_list)
```
    Remove a list of invariants.
  - findSlice
```
public @Nullable PptSlice1 findSlice(VarInfo v)
```
    Returns the unary slice over v. Returns null if the slice doesn't exist (which can occur if all of its invariants were falsified).
  - findSlice
```
public @Nullable PptSlice2 findSlice(VarInfo v1,
                                     VarInfo v2)
```
    Returns the binary slice over v1 and v2. Returns null if the slice doesn't exist (which can occur if all of its invariants were falsified).
  - findSlice_unordered
```
public @Nullable PptSlice2 findSlice_unordered(VarInfo v1,
                                               VarInfo v2)
```
    Like findSlice, but it is not required that the variables be supplied in order of varinfo_index.
  - findSlice
```
public @Nullable PptSlice3 findSlice(VarInfo v1,
                                     VarInfo v2,
                                     VarInfo v3)
```
    Returns the ternary slice over v1, v2, and v3. Returns null if the slice doesn't exist (which can occur if all of its invariants were falsified).
  - findSlice_unordered
```
public @Nullable PptSlice3 findSlice_unordered(VarInfo v1,
                                               VarInfo v2,
                                               VarInfo v3)
```
    Like findSlice, but it is not required that the variables be supplied in order of varinfo_index.
  - findSlice_unordered
```
public @Nullable PptSlice findSlice_unordered(VarInfo[] vis)
```
    Find a pptSlice without an assumed ordering.
  - findSlice
```
public @Nullable PptSlice findSlice(VarInfo[] vis)
```
    Find a pptSlice with an assumed ordering.
  - find_inv_by_class
```
public @Nullable Invariant find_inv_by_class(VarInfo[] vis,
                                             Class<? extends Invariant> cls)
```
    Returns the invariant in the slice specified by vis that matches the specified class. If the slice or the invariant does not exist, returns null.
  - find_assignment_inv
```
public @Nullable List<Invariant> find_assignment_inv(VarInfo v)
```
    Searches for all of the invariants that that provide an exact value for v. Intuitively those are invariants of the form 'v = equation'. For example: 'v = 63' or 'v = x * y' The implementation is a little iffy -- each invariant over v is examined and it matches iff it is exact and its daikon format starts with 'v ='.
    
    Returns:
    
    list of matching invariants or null if no matching invariants are found
  - get_temp_slice
```
@Pure
public PptSlice get_temp_slice(VarInfo v)
```
    Looks up the slice for v1. If the slice does not exist, one is created (but not added into the list of slices for this ppt).
  - get_temp_slice
```
@Pure
public PptSlice get_temp_slice(VarInfo v1,
                               VarInfo v2)
```
    Looks up the slice for v1 and v2. They do not have to be in order. If the slice does not exist, one is created (but not added into the list of slices for this ppt).
  - check_implied
```
public @Nullable DiscardInfo check_implied(Invariant imp_inv,
                                           VarInfo v,
                                           Invariant proto)
```
    If the prototype invariant is true over the specified variable returns DiscardInfo indicating that the prototype invariant implies imp_inv. Otherwise returns null.
  - check_implied_canonical
```
public @Nullable DiscardInfo check_implied_canonical(Invariant imp_inv,
                                                     VarInfo v,
                                                     Invariant proto)
```
    If the proto invariant is true over the leader of the specified variable returns DiscardInfo indicating that the proto invariant implies imp_inv. Otherwise returns null.
  - check_implied
```
public @Nullable DiscardInfo check_implied(Invariant imp_inv,
                                           VarInfo v1,
                                           VarInfo v2,
                                           Invariant proto)
```
    If the prototype invariant is true over the specified variables returns DiscardInfo indicating that the prototype invariant implies imp_inv. Otherwise returns null.
  - check_implied
```
public boolean check_implied(DiscardInfo di,
                             VarInfo v1,
                             VarInfo v2,
                             Invariant proto)
```
  - check_implied_canonical
```
public @Nullable DiscardInfo check_implied_canonical(Invariant imp_inv,
                                                     VarInfo v1,
                                                     VarInfo v2,
                                                     Invariant proto)
```
    If the prototype invariant is true over the leader of each specified variables returns DiscardInfo indicating that the prototype invariant implies imp_inv. Otherwise returns null.
  - check_implied_canonical
```
public boolean check_implied_canonical(DiscardInfo di,
                                       VarInfo v1,
                                       VarInfo v2,
                                       Invariant proto)
```
  - is_subset
```
@Pure
public boolean is_subset(VarInfo v1,
                         VarInfo v2)
```
    Returns whether or not v1 is a subset of v2.
  - is_nonzero
```
@Pure
public boolean is_nonzero(VarInfo v)
```
    Returns whether or not v1 is always non-zero.
  - is_equal
```
@Pure
public boolean is_equal(VarInfo v1,
                        VarInfo v2)
```
    Returns whether or not the specified variables are equal (ie, an equality invariant exists between them).
  - is_less_equal
```
@Pure
public boolean is_less_equal(VarInfo v1,
                             int v1_shift,
                             VarInfo v2,
                             int v2_shift)
```
    Returns true if (v1+v1_shift) ≤ (v2+v2_shift) is known to be true. Returns false otherwise. Integers only.
  - is_subsequence
```
@Pure
public boolean is_subsequence(VarInfo v1,
                              VarInfo v2)
```
    Returns true if v1 is known to be a subsequence of v2. This is true if the subsequence invariant exists or if it it suppressed.
  - is_empty
```
@Pure
public boolean is_empty(VarInfo varr)
```
    Returns true if varr is empty. Supports ints, doubles, and strings.
  - instantiate_views_and_invariants
```
public void instantiate_views_and_invariants()
```
    This function creates all the views (and thus candidate invariants), but does not check those invariants. We create NO views over static constant variables, but everything else is fair game. We don't create views over variables which have a higher (controlling) view. This function does NOT cause invariants over the new views to be checked (but it does create invariants).
  - is_slice_ok
```
@Pure
public boolean is_slice_ok(VarInfo[] vis,
                           int arity)
```
    Returns whether or not the specified slice should be created.
  - is_slice_ok
```
@Pure
public boolean is_slice_ok(VarInfo var1)
```
    Returns whether or not the specified unary slice should be created. The slice should not be created if the variable does not meet qualifications for the unary slice.
    
    See Also:
    
    is_var_ok_unary(VarInfo)
  - is_slice_ok
```
@Pure
public boolean is_slice_ok(VarInfo var1,
                           VarInfo var2)
```
    Returns whether or not the specified binary slice should be created. The slice should not be created if any of the following are true:
    - One of the variables does not meet qualifications for the binary slice - Variables are not compatible - Both variables are constant.
    
    See Also:
    
    is_var_ok_binary(VarInfo)
  - is_slice_ok
```
@Pure
public boolean is_slice_ok(VarInfo v1,
                           VarInfo v2,
                           VarInfo v3)
```
    Returns whether or not the specified ternary slice should be created by checking the variables' qualifications. In addition, The slice should not be created if any of the following are true:
    
    One of the variables does not meet qualifications for the ternary slice
    All of the vars are constants
    Any var is not (integral or float)
    Each var is the same and its equality set has only two variables
    Two of the vars are the same and its equality has only one variable. (This last one is currently disabled as x = func(x,y) might still be interesting even if x is the same.)
    See Also:
    
    is_var_ok_ternary(VarInfo)
  - vis_order_ok
```
public boolean vis_order_ok(VarInfo[] vis)
```
    Determines whether the order of the variables in vis is a valid permutation (i.e., their varinfo_index's are ordered). Null elements are ignored (and an all-null list is OK).
  - get_or_instantiate_slice
```
public PptSlice get_or_instantiate_slice(VarInfo[] vis)
```
    Return a slice that contains the given VarInfos (creating if needed). It is incumbent on the caller that the slice be either filled with one or more invariants, or else removed from the views collection.
    When the arity of the slice is known, call one of the overloaded definitions of get_or_instantiate_slice that takes (one or more) VarInfo arguments; they are more efficient.
    
    Parameters:
    
    vis - array of VarInfo objects; is not used internally (so the same value can be passed in repeatedly). Can be unsorted.
  - get_or_instantiate_slice
```
public PptSlice get_or_instantiate_slice(VarInfo vi)
```
    Return a slice that contains the given VarInfos (creating if needed). It is incumbent on the caller that the slice be either filled with one or more invariants, or else removed from the views collection.
  - get_or_instantiate_slice
```
public PptSlice get_or_instantiate_slice(VarInfo v1,
                                         VarInfo v2)
```
    Return a slice that contains the given VarInfos (creating if needed). It is incumbent on the caller that the slice be either filled with one or more invariants, or else removed from the views collection.
  - get_or_instantiate_slice
```
public PptSlice get_or_instantiate_slice(VarInfo v1,
                                         VarInfo v2,
                                         VarInfo v3)
```
    Return a slice that contains the given VarInfos (creating if needed). It is incumbent on the caller that the slice be either filled with one or more invariants, or else removed from the views collection.
  - addConditions
```
public void addConditions(Splitter[] splits)
```
  - getProverStack
```
@Pure
public static @Nullable LemmaStack getProverStack()
```
  - addImplications
```
public void addImplications()
```
    Given conditional program points (and invariants detected over them), create implications. Configuration variable "pairwise_implications" controls whether all or only the first two conditional program points are considered.
  - postProcessEquality
```
public void postProcessEquality()
```
    Two things: a) convert Equality invariants into normal IntEqual type for filtering, printing, etc. b) Pivot uninteresting parameter VarInfos so that each equality set contains only the interesting one.
  - mark_implied_via_simplify
```
public void mark_implied_via_simplify(PptMap all_ppts)
```
    Use the Simplify theorem prover to flag invariants that are logically implied by others. Considers only invariants that pass isWorthPrinting.
    
    Parameters:
    
    all_ppts - all the program points
  - format_simplify_problem
```
public static boolean format_simplify_problem(String s)
```
    Returns true if there was a problem with Simplify formatting (such as the invariant not having a Simplify representation).
  - getParamVars
```
@Pure
public Set<VarInfo> getParamVars()
```
    Returns variables in this Ppt that are parameters.
  - getInvariants
```
public List<Invariant> getInvariants()
```
    Return a List of all the invariants for the program point. Also consider using views_iterator() instead. You can't modify the result of this.
  - invariants_vector
```
public List<Invariant> invariants_vector()
```
    ArrayList version of getInvariants().
  - views_iterator
```
public Iterator<PptSlice> views_iterator()
```
    For some clients, this method may be more efficient than getInvariants.
    
    See Also:
    
    views_iterable()
  - views_iterable
```
public Iterable<PptSlice> views_iterable()
```
    For some clients, this method may be more efficient than getInvariants.
    
    See Also:
    
    views_iterator()
  - invariants_iterator
```
public Iterator<Invariant> invariants_iterator()
```
    Iterate over all of the invariants at this ppt (but not any implications).
  - simplify_variable_names
```
public void simplify_variable_names()
```
    Simplify the names of variables before printing them. For example, "orig(a[post(i)])" might change into "orig(a[i+1])". We might want to switch off this behavior, depending on various heuristics. We'll have to try it and see which output we like best. In any case, we have to do this for ESC output, since ESC doesn't have anything like post().
  - processOmissions
```
public void processOmissions(boolean[] omitTypes)
```
    Remove invariants that are marked for omission in omitTypes.
  - repCheck
```
public void repCheck()
```
    Check the rep invariants of this. Throw an Error if not okay.
  - debugSlices
```
public String debugSlices()
```
    Debug method to display all slices.
  - debug_print_tree
```
public void debug_print_tree(Logger l,
                             int indent,
                             @Nullable PptRelation parent_rel)
```
    Debug method to print children (in the partial order) recursively.
  - equality_sets_txt
```
public String equality_sets_txt()
```
    Returns a string version of all of the equality sets for this ppt. The string is of the form [a,b], [c,d] where a,b and c,d are each in an equality set. Should be used only for debugging.
  - has_parent
```
public boolean has_parent(VarInfo v)
```
    Returns whether or not the specified variable in this ppt has any parents.
  - mergeInvs
```
public void mergeInvs()
```
    Recursively merge invariants from children to create an invariant list at this ppt.
    First, equality sets are created for this ppt. These are the intersection of the equality sets from each child. Then create unary, binary, and ternary slices for each combination of equality sets and build the invariants for each slice.
  - merge_invs_multiple_children
```
@RequiresNonNull("equality_view")
public void merge_invs_multiple_children()
```
    Merges the invariants from multiple children. NI suppression is handled by first creating all of the suppressed invariants in each of the children, performing the merge, and then removing them.
  - merge_invs_one_child
```
public void merge_invs_one_child()
```
    Merges one child. Since there is only one child, the merge is trivial (each invariant can be just copied to the parent).
  - parent_vis
```
public VarInfo @Nullable [] parent_vis(PptRelation rel,
                                       PptSlice slice)
```
    Creates a list of parent variables (i.e., variables at the parent program point) that matches slice. Returns null if any of the variables don't have a corresponding parent variables.
    The corresponding parent variable can match ANY of the members of an equality set. For example, suppose that the child is EXIT with variable A, with equality set members {A, orig(A)}; and suppose that this child is matched against ENTER. A does not have a relation (since it is a post value), but orig(A) does have a relation.
    Note that there are cases where this is not exactly correct. If you wanted to get all of the invariants over A where A is an equality set with B, and A and B were in different equality sets at the parent, the invariants true at A in the child are the union of those true at A and B at the parent.
  - merge_conditionals
```
public void merge_conditionals()
```
    Merges the conditionals from the children of this ppt to this ppt. Only conditionals that exist at each child and whose splitting condition is valid here can be merged.
  - clean_for_merge
```
public void clean_for_merge()
```
    Cleans up the ppt so that its invariants can be merged from other ppts. Not normally necessary unless the merge is taking place over multiple ppts maps based on different data. This allows a ppt to have its invariants recalculated.
  - remove_equality_invariants
```
public void remove_equality_invariants()
```
    Remove the equality invariants added during equality post processing. These are not over leaders and can cause problems in some uses of the ppt. In particular, they cause problems during merging.
  - remove_implications
```
public void remove_implications()
```
    Remove all of the implications from this program point. Can be used when recalculating implications. Actually removes the entire joiner_view.
  - remove_child_invs
```
public void remove_child_invs(PptRelation rel)
```
    Removes any invariant in this ppt which has a matching invariant in the parent (as specified in the relation). Done to save space. Only safe when all processing of this child is complete (i.e., all of the parents of this child must have been merged).
    Another interesting problem arises with this code. As currently set up, it won't process combined exit points (which often have two parents), but it will process enter points. Once the enter point is removed, it can no longer parent filter the combined exit point.
    Also, the dynamic obvious code doesn't work anymore (because it is missing the appropriate invariants). This could be fixed by changing dynamic obvious to search up the tree (blecho!). Fix this by only doing this for ppts whose parent only has one child.
  - build_permute
```
public static int[] build_permute(VarInfo[] vis1,
                                  VarInfo[] vis2)
```
    Builds a permutation from vis1 to vis2. The result is vis1[i] = vis2[permute[i]].
  - debug_print_slice_info
```
public void debug_print_slice_info(Logger log,
                                   String descr,
                                   List<PptSlice> slices)
```
    Debug print slice/inv count information to the specified logger.
  - create_equality_inv
```
public PptSlice create_equality_inv(VarInfo v1,
                                    VarInfo v2,
                                    int samples)
```
    Create an equality invariant over the specified variables. Samples should be the number of samples for the slice over v1 and v2. The slice should not already exist.
  - print_equality_stats
```
public static void print_equality_stats(Logger log,
                                        PptMap all_ppts)
```
    Print statistics concerning equality sets over the entire set of ppts to the specified logger.
  - incSampleNumber
```
public void incSampleNumber()
```
    Increments the number of samples processed by the program point by 1.
  - is_exit
```
@Pure
public boolean is_exit()
```
    Is this is an exit ppt (combined or specific)?
  - is_enter
```
@Pure
public boolean is_enter()
```
    is this an enter ppt
  - is_combined_exit
```
@Pure
public boolean is_combined_exit()
```
    Is this a combined exit point?
  - is_subexit
```
@Pure
public boolean is_subexit()
```
    Is this a numbered (specific) exit point?
  - is_object
```
@Pure
public boolean is_object()
```
    Is this a ppt that represents an object?
  - is_class
```
@EnsuresNonNullIf(result=true,
                  expression="type")
@Pure
public boolean is_class()
```
    Is this a ppt that represents a class?
  - var_names
```
public String var_names()
```

Class PptTopLevel

Nested Class Summary

Nested classes/interfaces inherited from class Ppt

Field Summary

Fields inherited from class Ppt

Constructor Summary

Method Summary

Methods inherited from class Ppt

Methods inherited from class Object

Field Detail

dkconfig_pairwise_implications

dkconfig_remove_merged_invs

first_pass_with_sample

flags

type

instantiated_inv_cnt

instantiated_slice_cnt

debug

debugInstantiate

debugTimeMerge

debugEqualTo

debugAddImplications

debugConditional

debugFlow

debugMerge

debugNISStats

name

ppt_name

constants

num_declvars

num_tracevars

num_orig_vars

num_static_constant_vars

splitters

children

parents

parent_relations

invariants_merged

in_merge

invariants_removed

joiner_view

equality_view

redundant_invs

redundant_invs_equality

icfp

Constructor Detail

PptTopLevel

PptTopLevel

Method Detail

name

cond_iterator

cond_iterable

has_splitters

num_array_vars

var_info_iterator

toString

trimToSize

num_samples

num_samples

num_samples

num_samples

num_values

num_values

num_values

numViews

worthDerivingFrom

add_bottom_up

inv_add

get_missingOutOfBounds

is_constant

is_prev_constant

is_missing

is_prev_missing

invariant_cnt

const_slice_cnt

const_inv_cnt

debug_invs

debug_unary_info

invariant_cnt_by_class

slice_cnt