package util
- Alphabetic
- Public
- Protected
Type Members
- class CountIt extends Iterator[Int]
Simple iterator that enumerates the natural numbers, starting with 0
- class Dijkstra[Node] extends AnyRef
An implementation of Dijkstra's algorithm for computing shortest paths to all reachable nodes in a graph.
- class FastImmutableMap[A, B] extends Map[A, B]
A double-backed map class that initially stores its elements in a
scala.collection.immutable.Map, but copies all data to ascala.collection.mutable.HashMapwhen many accesses are taking place (since the mutable map enables faster access than the immutable map). - class FilterIt[T] extends Iterator[T]
An own class for filtering the elements that are returned by an iterator, because the method
Iterator.filteris so broken - abstract class IdealRange extends Seq[IdealInt]
Extremely simple class for iterating over intervals of integers
Extremely simple class for iterating over intervals of integers
TODO: this should be removed
- class IntervalIdealRange extends IdealRange
- Attributes
- protected
- class IntervalPlainRange extends PlainRange
- Attributes
- protected
- class LRUCache[K, V] extends AnyRef
Naive implementation of a thread-safe LRU cache.
- class LazyIndexedSeqConcat[A] extends IndexedSeq[A]
- class LazyIndexedSeqSlice[A] extends IndexedSeq[A]
- class LazyMappedMap[A, B, C, D] extends Map[C, D]
Transform a
Map mby composing it with two functions into a mapvalueMapping . m . keyUnmapping.Transform a
Map mby composing it with two functions into a mapvalueMapping . m . keyUnmapping.keyMappinghas to be the inverse ofkeyUnmapping, and has to be injective - class LazyMappedSet[A, B] extends Set[B]
Transform a set by applying a given injective function to all of its arguments.
- class POGraph[A] extends AnyRef
A class to explicitly represent partial orders.
A class to explicitly represent partial orders. This is used in various contexts to speed up implication checks.
- trait PeekIterator[+T] extends Iterator[T]
Extension of the iterator trait where the next element can be peeked without popping it
- class PeekIteratorTrafo[T] extends PeekIterator[T]
- abstract class PlainRange extends Seq[Int]
Extremely simple class for iterating over intervals of integers
Extremely simple class for iterating over intervals of integers
TODO: this should be removed
- class PredicatedIdealRange extends IntervalIdealRange
- Attributes
- protected
- class PredicatedPlainRange extends IntervalPlainRange
- Attributes
- protected
- class PriorityQueueWithIterators[A] extends PeekIterator[A]
Priority queue that can handle both single elements and pre-sorted sequences (iterators) of elements
- class Tarjan[Node] extends AnyRef
An implementation of Tarjan's algorithm for computing the strongly connected components of a graph.
- case class Timeout(unfinishedResult: Any) extends Exception with Product with Serializable
Object that is thrown in case of a timeout (or the user stopped the proof search)
- class UnionMap[A, B] extends Map[A, B]
A (lazy)
Mapthat represents the union of twoMaps with disjoint key domains - class UnionSet[A] extends Set[A]
A (lazy)
Setthat represents the union of two (not necessarily disjoint)Sets
Value Members
- object CmdlParser
- object Combinatorics
- object Debug
A collect of methods for writing runtime assertions and inserting debugging information.
A collect of methods for writing runtime assertions and inserting debugging information. In particular, here the different categories and types of assertions are defined and can be switched on and off.
- object Dijkstra
- object FastImmutableMap
- object FilterIt
- object IdealRange
- object LazyIndexedSeqConcat
- object LazyMappedMap
- object LazyMappedSet
- object Logic
- object OpCounters
Object to implement different kinds of performance counters.
Object to implement different kinds of performance counters. Such counters are handled in a thread-local way.
- object POGraph
- object PeekIterator
- object PlainRange
- object RuntimeStatistics
Object to keep track of some prover statistics, such as the number of problems loaded and the amount of time spent constructing proofs.
Object to keep track of some prover statistics, such as the number of problems loaded and the amount of time spent constructing proofs. This class is only used from the
ParallelFileProver. - object Seqs
- object Tarjan
- object Timeout extends Serializable
- object Timer
Object for measuring the time needed by the various tasks, methods, etc.
Object for measuring the time needed by the various tasks, methods, etc. The object, in particular, supports nested operations that call each other and correctly measures the time spent in each of the operations.
The current implementation of the timer is not thread-safe; if we detect that the class is used from multiple threads we disable time measurements altogether. Calls are still counted.
- object UnionMap
- object UnionSet
- object Warmup
Class to run some standard proof-tasks, with the goal of making sure that all the relevant classes have been loaded into the JVM, and JIT compilation has been started.