Object
- Invariant
- - BinaryInvariant
  - - SequenceScalar

All Implemented Interfaces:

Serializable, Cloneable

Direct Known Subclasses:

Member, SeqIntEqual, SeqIntGreaterEqual, SeqIntGreaterThan, SeqIntLessEqual, SeqIntLessThan
```
public abstract class SequenceScalar
extends BinaryInvariant
```
Abstract base class for comparing long sequences to long variables. Note that the sequence must always be passed in first. An example is x is a member of a[].

See Also:

Serialized Form

Nested Class Summary
- Nested classes/interfaces inherited from class Invariant
  Invariant.ClassVarnameComparator, Invariant.ClassVarnameFormulaComparator, Invariant.InvariantComparatorForPrinting, Invariant.Match

Constructor Summary

Constructors
Modifier Constructor Description

protected SequenceScalar()

protected SequenceScalar(PptSlice ppt)

Method Summary

All Methods Instance Methods Abstract Methods Concrete Methods
Modifier and Type	Method	Description
`InvariantStatus`	`add(@Interned Object val1, @Interned Object val2, int mod_index, int count)`
`abstract InvariantStatus`	`add_modified(long @Interned [] v1, long v2, int count)`	Similar to `check_modified(long[], long, int)` except that it can change the state of the invariant if necessary.
`InvariantStatus`	`add_unmodified(long @Interned [] v1, long v2, int count)`	By default, do nothing if the value hasn't been seen yet.
`InvariantStatus`	`check(@Interned Object val1, @Interned Object val2, int mod_index, int count)`
`abstract InvariantStatus`	`check_modified(long @Interned [] v1, long v2, int count)`	Presents a sample to the invariant.
`InvariantStatus`	`check_unmodified(long @Interned [] v1, long v2, int count)`
`boolean`	`is_symmetric()`	Since the order is determined from the vars and the sequence is always first, this is essentially symmetric.
`protected Invariant`	`resurrect_done(int[] permutation)`	Called on the new invariant just before resurrect() returns it to allow subclasses to fix any information they might have cached from the old Ppt and VarInfos.
`protected Invariant`	`resurrect_done_swapped()`	Since the order is determined from the vars and the sequence is always first, no permute is necesesary.
`protected Invariant`	`resurrect_done_unswapped()`	Subclasses can override in the rare cases they need to fix things even when not swapped.
`protected int`	`scl_index()`
`VarInfo`	`sclvar()`
`VarInfo`	`sclvar(VarInfo[] vis)`	Return the scalar variable in the tuple whose VarInfos are corresponds to this.ppt.var_infos.
`protected boolean`	`seq_first()`
`protected int`	`seq_index()`
`VarInfo`	`seqvar()`
`VarInfo`	`seqvar(VarInfo[] vis)`	Return the sequence variable in the tuple whose VarInfos are corresponds to this.ppt.var_infos.
`boolean`	`valid_types(VarInfo[] vis)`	Returns whether or not the specified types are valid.

Methods inherited from class BinaryInvariant
add_unordered, check_unordered, find, get_swap

Methods inherited from class Invariant
add_sample, asInvClass, checkRep, clear_falsified, clone, clone_and_permute, computeConfidence, conf_is_ge, confidence_and, confidence_and, confidence_or, createGuardedInvariant, createGuardingPredicate, enabled, enoughSamples, falsify, find, format, format_classname, format_too_few_samples, format_unimplemented, format_using, formatFuzzy, get_comparability, get_ni_suppressions, getConfidence, getGuardingList, getGuardingList, hasUninterestingConstant, instantiate, instantiate_dyn, instantiate_ok, is_false, is_ni_suppressed, isActive, isAllPrestate, isEqualityComparison, isExact, isExclusiveFormula, isObvious, isObviousDynamically, isObviousDynamically, isObviousDynamically_SomeInEquality, isObviousDynamically_SomeInEqualityHelper, isObviousStatically, isObviousStatically, isObviousStatically_AllInEquality, isObviousStatically_SomeInEquality, isObviousStatically_SomeInEqualityHelper, isReflexive, isSameFormula, isSameInvariant, isValidEscExpression, isValidExpression, isWorthPrinting, justified, log, log, logDetail, logOn, match, merge, mergeFormulasOk, permute, prob_and, prob_and, prob_is_ge, prob_or, repCheck, repr, repr_prob, resurrect, simplify_format_double, simplify_format_long, simplify_format_string, state_match, toString, toString, transfer, usesVar, usesVar, usesVarDerived, varNames

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

- Constructor Detail
  - SequenceScalar
```
protected SequenceScalar(PptSlice ppt)
```
  - SequenceScalar
```
protected SequenceScalar()
```
- Method Detail
  - valid_types
```
public boolean valid_types(VarInfo[] vis)
```
    Returns whether or not the specified types are valid. All subclasses accept a scalar in one parameter and an array over the same scalar type in the other.
    
    Specified by:
    
    valid_types in class Invariant
    
    See Also:
    
    Invariant.instantiate_ok(VarInfo[])
  - resurrect_done_swapped
```
protected Invariant resurrect_done_swapped()
```
    Since the order is determined from the vars and the sequence is always first, no permute is necesesary. Subclasses can override if necessary.
  - is_symmetric
```
@Pure
public boolean is_symmetric()
```
    Since the order is determined from the vars and the sequence is always first, this is essentially symmetric. Subclasses can override if necessary.
    
    Overrides:
    
    is_symmetric in class BinaryInvariant
  - resurrect_done
```
protected Invariant resurrect_done(int[] permutation)
```
    Description copied from class: Invariant
    
    Called on the new invariant just before resurrect() returns it to allow subclasses to fix any information they might have cached from the old Ppt and VarInfos.
    
    Specified by:
    
    resurrect_done in class Invariant
    
    Parameters:
    
    permutation - the permutation
    
    Returns:
    
    the permuted invariant
  - resurrect_done_unswapped
```
protected Invariant resurrect_done_unswapped()
```
    Subclasses can override in the rare cases they need to fix things even when not swapped.
  - seq_first
```
protected final boolean seq_first(@GuardSatisfied SequenceScalar this)
```
  - seq_index
```
protected final int seq_index(@GuardSatisfied SequenceScalar this)
```
  - scl_index
```
protected final int scl_index(@GuardSatisfied SequenceScalar this)
```
  - seqvar
```
public VarInfo seqvar(@GuardSatisfied SequenceScalar this)
```
  - sclvar
```
public VarInfo sclvar(@GuardSatisfied SequenceScalar this)
```
  - seqvar
```
public VarInfo seqvar(VarInfo[] vis)
```
    Return the sequence variable in the tuple whose VarInfos are corresponds to this.ppt.var_infos.
  - sclvar
```
public VarInfo sclvar(VarInfo[] vis)
```
    Return the scalar variable in the tuple whose VarInfos are corresponds to this.ppt.var_infos.
  - check
```
public InvariantStatus check(@Interned Object val1,
                             @Interned Object val2,
                             int mod_index,
                             int count)
```
    Specified by:
    
    check in class BinaryInvariant
  - add
```
public InvariantStatus add(@Interned Object val1,
                           @Interned Object val2,
                           int mod_index,
                           int count)
```
    Specified by:
    
    add in class BinaryInvariant
  - check_modified
```
public abstract InvariantStatus check_modified(long @Interned [] v1,
                                               long v2,
                                               int count)
```
    Presents a sample to the invariant. Returns whether the sample is consistent with the invariant. Does not change the state of the invariant.
    
    Parameters:
    
    count - how many identical samples were observed in a row. For example, three calls to check_modified with a count parameter of 1 is equivalent to one call to check_modified with a count parameter of 3.
    
    Returns:
    
    whether or not the sample is consistent with the invariant
  - check_unmodified
```
public InvariantStatus check_unmodified(long @Interned [] v1,
                                        long v2,
                                        int count)
```
  - add_modified
```
public abstract InvariantStatus add_modified(long @Interned [] v1,
                                             long v2,
                                             int count)
```
    Similar to check_modified(long[], long, int) except that it can change the state of the invariant if necessary. If the invariant doesn't have any state, then the implementation should simply call check_modified(long[], long, int). This method need not check for falsification; that is done by the caller.
  - add_unmodified
```
public InvariantStatus add_unmodified(long @Interned [] v1,
                                      long v2,
                                      int count)
```
    By default, do nothing if the value hasn't been seen yet. Subclasses can override this.

Class SequenceScalar

Nested Class Summary

Nested classes/interfaces inherited from class Invariant

Field Summary

Fields inherited from class Invariant

Constructor Summary

Method Summary

Methods inherited from class BinaryInvariant

Methods inherited from class Invariant

Methods inherited from class Object

Constructor Detail

SequenceScalar

SequenceScalar

Method Detail

valid_types

resurrect_done_swapped

is_symmetric

resurrect_done

resurrect_done_unswapped

seq_first

seq_index

scl_index

seqvar

sclvar

seqvar

sclvar

check

add

check_modified

check_unmodified

add_modified

add_unmodified

Modifier	Constructor	Description
`protected`	`SequenceScalar()`
`protected`	`SequenceScalar(PptSlice ppt)`