util

Type Members

abstract class APTestCase extends AnyRef
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 a scala.collection.mutable.HashMap when many accesses are taking place (since the mutable map enables faster access than the immutable map).
A double-backed map class that initially stores its elements in a scala.collection.immutable.Map, but copies all data to a scala.collection.mutable.HashMap when 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.filter is so broken
An own class for filtering the elements that are returned by an iterator, because the method Iterator.filter is 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 m by composing it with two functions into a map valueMapping . m . keyUnmapping.
Transform a Map m by composing it with two functions into a map valueMapping . m . keyUnmapping. keyMapping has to be the inverse of keyUnmapping, 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) Map that represents the union of two Maps with disjoint key domains
A (lazy) Map that represents the union of two Maps with disjoint key domains
class UnionSet[A] extends Set[A]

A (lazy) Set that represents the union of two (not necessarily disjoint) Sets
A (lazy) Set that represents the union of two (not necessarily disjoint) Sets

Value Members

object APTestCase
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 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

package util

Type Members

abstract class APTestCase extends AnyRef

class CountIt extends Iterator[Int]

class Dijkstra[Node] extends AnyRef

class FastImmutableMap[A, B] extends Map[A, B]

class FilterIt[T] extends Iterator[T]

abstract class IdealRange extends Seq[IdealInt]

class IntervalIdealRange extends IdealRange

class IntervalPlainRange extends PlainRange

class LRUCache[K, V] extends AnyRef

class LazyIndexedSeqConcat[A] extends IndexedSeq[A]

class LazyIndexedSeqSlice[A] extends IndexedSeq[A]

class LazyMappedMap[A, B, C, D] extends Map[C, D]

class LazyMappedSet[A, B] extends Set[B]

class POGraph[A] extends AnyRef

trait PeekIterator[+T] extends Iterator[T]

class PeekIteratorTrafo[T] extends PeekIterator[T]

abstract class PlainRange extends Seq[Int]

class PredicatedIdealRange extends IntervalIdealRange

class PredicatedPlainRange extends IntervalPlainRange

class PriorityQueueWithIterators[A] extends PeekIterator[A]

class Tarjan[Node] extends AnyRef

case class Timeout(unfinishedResult: Any) extends Exception with Product with Serializable

class UnionMap[A, B] extends Map[A, B]

class UnionSet[A] extends Set[A]

Value Members

object APTestCase

object CmdlParser

object Combinatorics

object Debug

object Dijkstra

object FastImmutableMap

object FilterIt

object IdealRange

object LazyIndexedSeqConcat

object LazyMappedMap

object LazyMappedSet

object Logic

object POGraph

object PeekIterator

object PlainRange

object RuntimeStatistics

object Seqs

object Tarjan

object Timeout extends Serializable

object Timer

object UnionMap

object UnionSet

Ungrouped