object MonixProverTasks
A drop-in replacement for FineProverTasks to test the abstract generators approach; since testing is the goal redundancies and some comments have been removed.
- Alphabetic
- By Inheritance
- MonixProverTasks
- AnyRef
- Any
- Hide All
- Show All
- Public
- Protected
Value Members
- final def !=(arg0: Any): Boolean
- Definition Classes
- AnyRef → Any
- final def ##: Int
- Definition Classes
- AnyRef → Any
- final def ==(arg0: Any): Boolean
- Definition Classes
- AnyRef → Any
- final def asInstanceOf[T0]: T0
- Definition Classes
- Any
- def clone(): AnyRef
- Attributes
- protected[lang]
- Definition Classes
- AnyRef
- Annotations
- @throws(classOf[java.lang.CloneNotSupportedException]) @native() @HotSpotIntrinsicCandidate()
- def dervecTraceTasks(base: FiniteDistribution[Term], tg: TermGenParams, termsTask: Task[FiniteDistribution[Term]], typsTask: Task[FiniteDistribution[Typ[Term]]], maxtime: FiniteDuration, cutoff: Double, scale: Double, trace: Vector[Term], vars: Vector[Term] = Vector()): Task[Vector[Task[(FiniteDistribution[Term], Vector[Term])]]]
bunch of tasks using newly discovered proofs by evolving along unit tangents.
bunch of tasks using newly discovered proofs by evolving along unit tangents. the cutoffs, viewed as resources, are allocated based on values of the new proofs. these tasks return the tangent distributions as well as the path to get there.
- def dervecWeightedTraceTasks(base: FiniteDistribution[Term], tg: TermGenParams, termsTask: Task[FiniteDistribution[Term]], typsTask: Task[FiniteDistribution[Typ[Term]]], maxtime: FiniteDuration, cutoff: Double, scale: Double, trace: Vector[(Term, Double)], vars: Vector[Term] = Vector()): Task[Vector[Task[(FiniteDistribution[Term], Vector[(Term, Double)])]]]
bunch of tasks using newly discovered proofs by evolving along unit tangents.
bunch of tasks using newly discovered proofs by evolving along unit tangents. the cutoffs, viewed as resources, are allocated based on values of the new proofs. these tasks return the tangent distributions as well as the path to get there, plus weights of proofs as they are found.
- final def eq(arg0: AnyRef): Boolean
- Definition Classes
- AnyRef
- def equals(arg0: AnyRef): Boolean
- Definition Classes
- AnyRef → Any
- final def getClass(): Class[_ <: AnyRef]
- Definition Classes
- AnyRef → Any
- Annotations
- @native() @HotSpotIntrinsicCandidate()
- def hashCode(): Int
- Definition Classes
- AnyRef → Any
- Annotations
- @native() @HotSpotIntrinsicCandidate()
- final def isInstanceOf[T0]: Boolean
- Definition Classes
- Any
- final def ne(arg0: AnyRef): Boolean
- Definition Classes
- AnyRef
- final def notify(): Unit
- Definition Classes
- AnyRef
- Annotations
- @native() @HotSpotIntrinsicCandidate()
- final def notifyAll(): Unit
- Definition Classes
- AnyRef
- Annotations
- @native() @HotSpotIntrinsicCandidate()
- final def synchronized[T0](arg0: => T0): T0
- Definition Classes
- AnyRef
- def termdistDerTask(fd: FiniteDistribution[Term], tfd: FiniteDistribution[Term], tg: TermGenParams, cutoff: Double, maxtime: FiniteDuration, vars: Vector[Term] = Vector()): Task[FiniteDistribution[Term]]
- def termdistTask(fd: FiniteDistribution[Term], tg: TermGenParams, cutoff: Double, maxtime: FiniteDuration, vars: Vector[Term] = Vector()): Task[FiniteDistribution[Term]]
- def theoremSearchTraceTask(fd: FiniteDistribution[Term], tg: TermGenParams, cutoff: Double, maxtime: FiniteDuration, goal: Typ[Term], decay: Double = 1.0, scale: Double = 1.0, vars: Vector[Term] = Vector()): Task[Option[(Term, Vector[Term])]]
breadth-first search for a term of a given type, keeping track of the path
breadth-first search for a term of a given type, keeping track of the path
- returns
task giving an optional term of the type together with a vector of proofs of lemmas.
- def theoremsExploreTraceTask(fd: FiniteDistribution[Term], tg: TermGenParams, cutoff: Double, maxtime: FiniteDuration, decay: Double = 1.0, scale: Double = 1.0, vars: Vector[Term] = Vector()): Task[(Vector[(Term, Vector[(Term, Double)], (Int, Double))], FiniteDistribution[Term], FiniteDistribution[Typ[Term]])]
breadth-first exploration to find alll interesting proofs, keeping track of lemmas
breadth-first exploration to find alll interesting proofs, keeping track of lemmas
- returns
task for vector of proofs with lemmas and the corresponding theorems.
- def toString(): String
- Definition Classes
- AnyRef → Any
- def typdistTask(fd: FiniteDistribution[Term], tg: TermGenParams, cutoff: Double, maxtime: FiniteDuration, vars: Vector[Term] = Vector()): Task[FiniteDistribution[Typ[Term]]]
- def typs(fd: FiniteDistribution[Term]): FiniteDistribution[Typ[Term]]
- final def wait(arg0: Long, arg1: Int): Unit
- Definition Classes
- AnyRef
- Annotations
- @throws(classOf[java.lang.InterruptedException])
- final def wait(arg0: Long): Unit
- Definition Classes
- AnyRef
- Annotations
- @throws(classOf[java.lang.InterruptedException]) @native()
- final def wait(): Unit
- Definition Classes
- AnyRef
- Annotations
- @throws(classOf[java.lang.InterruptedException])
Deprecated Value Members
- def finalize(): Unit
- Attributes
- protected[lang]
- Definition Classes
- AnyRef
- Annotations
- @throws(classOf[java.lang.Throwable]) @Deprecated
- Deprecated