Simple iterator that enumerates the natural numbers, starting with 0
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).
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
Extremely simple class for iterating over intervals of integers
Extremely simple class for iterating over intervals of integers
TODO: this should be removed
Naive implementation of a thread-safe LRU cache.
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
Transform a set by applying a given injective function to all of its arguments.
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.
Extension of the iterator trait where the next element can be peeked without popping it
Extremely simple class for iterating over intervals of integers
Extremely simple class for iterating over intervals of integers
TODO: this should be removed
Priority queue that can handle both single elements and pre-sorted sequences (iterators) of elements
An implementation of Tarjan's algorithm for computing the strongly connected components of a graph.
Object that is thrown in case of a timeout (or the user stopped the proof search)
A (lazy) Map
that represents the union of two Map
s with
disjoint key domains
A (lazy) Map
that represents the union of two Map
s with
disjoint key domains
A (lazy) Set
that represents the union of two
(not necessarily disjoint) Set
s
A (lazy) Set
that represents the union of two
(not necessarily disjoint) Set
s
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 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 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.
A double-backed map class that initially stores its elements in a
scala.collection.immutable.Map
, but copies all data to ascala.collection.mutable.HashMap
when many accesses are taking place (since the mutable map enables faster access than the immutable map).