Packages

case class LocalTangentProver(initState: TermState = TermState(FiniteDistribution.empty, FiniteDistribution.empty), initEquations: Set[EquationNode], tangentState: TermState, tg: TermGenParams = TermGenParams(), cutoff: Double = math.pow(10, -4), genMaxDepth: Option[Int] = None, limit: FiniteDuration = 3.minutes, maxRatio: Double = 1.01, resolution: Double = 0.0, scale: Double = 1.0, steps: Int = 10000, maxDepth: Int = 10, hW: Double = 1, klW: Double = 1, smoothing: Option[Double] = None, relativeEval: Boolean = false, stateFromEquation: Boolean = false, exponent: Double = 0.5, decay: Double = 1, maxTime: Option[Long] = None) extends LocalProverStep with Product with Serializable

Linear Supertypes
Serializable, Product, Equals, LocalProverStep, AnyRef, Any
Type Hierarchy
Ordering
  1. Alphabetic
  2. By Inheritance
Inherited
  1. LocalTangentProver
  2. Serializable
  3. Product
  4. Equals
  5. LocalProverStep
  6. AnyRef
  7. Any
Implicitly
  1. by any2stringadd
  2. by StringFormat
  3. by Ensuring
  4. by ArrowAssoc
  1. Hide All
  2. Show All
Visibility
  1. Public
  2. Protected

Instance Constructors

  1. new LocalTangentProver(initState: TermState = TermState(FiniteDistribution.empty, FiniteDistribution.empty), initEquations: Set[EquationNode], tangentState: TermState, tg: TermGenParams = TermGenParams(), cutoff: Double = math.pow(10, -4), genMaxDepth: Option[Int] = None, limit: FiniteDuration = 3.minutes, maxRatio: Double = 1.01, resolution: Double = 0.0, scale: Double = 1.0, steps: Int = 10000, maxDepth: Int = 10, hW: Double = 1, klW: Double = 1, smoothing: Option[Double] = None, relativeEval: Boolean = false, stateFromEquation: Boolean = false, exponent: Double = 0.5, decay: Double = 1, maxTime: Option[Long] = None)

Value Members

  1. def addGoal(goal: Typ[Term], weight: Double): LocalProverStep
    Definition Classes
    LocalProverStep
  2. def addLookup(ts: Set[Term]): LocalProverStep
    Definition Classes
    LocalProverStep
  3. def addSolver(s: TypSolver): LocalProverStep
    Definition Classes
    LocalProverStep
  4. def addVar(term: Term, weight: Double): LocalProverStep
    Definition Classes
    LocalProverStep
  5. def apple(w: Double = 0.1): LocalTangentProver
  6. def bigExpressionEval(additional: Set[Equation]): Task[ExpressionEquationSolver]
    Definition Classes
    LocalProverStep
  7. val cutoff: Double
    Definition Classes
    LocalTangentProver → LocalProverStep
  8. val decay: Double
    Definition Classes
    LocalTangentProver → LocalProverStep
  9. def distTangentProver(fd: FiniteDistribution[Term], tangentCutoff: Double = cutoff): Task[LocalTangentProver]
    Definition Classes
    LocalProverStep
  10. lazy val enhancedEquationNodes: Task[Set[EquationNode]]
    Definition Classes
    LocalProverStep
  11. lazy val enhancedExpressionEval: Task[ExpressionEquationSolver]
    Definition Classes
    LocalProverStep
  12. lazy val equationNodes: Task[Set[EquationNode]]
    Definition Classes
    LocalTangentProver → LocalProverStep
  13. lazy val equations: Task[Set[Equation]]
    Definition Classes
    LocalProverStep
  14. lazy val evolvedState: Task[EvolvedState]
    Definition Classes
    LocalProverStep
  15. val exponent: Double
    Definition Classes
    LocalTangentProver → LocalProverStep
  16. lazy val expressionEval: Task[ExpressionEquationSolver]
    Definition Classes
    LocalProverStep
  17. lazy val functionsForGoals: Task[FiniteDistribution[Term]]
    Definition Classes
    LocalProverStep
  18. val genMaxDepth: Option[Int]
    Definition Classes
    LocalTangentProver → LocalProverStep
  19. lazy val generatorIterant: Iterant[Task, FiniteDistribution[Term]]
    Definition Classes
    LocalProverStep
  20. val hW: Double
    Definition Classes
    LocalTangentProver → LocalProverStep
  21. def halt(): Unit
    Definition Classes
    LocalProverStep
  22. def halted(): Boolean
    Definition Classes
    LocalProverStep
  23. val initEquations: Set[EquationNode]
  24. val initState: TermState
    Definition Classes
    LocalTangentProver → LocalProverStep
  25. val isHalted: Boolean
    Definition Classes
    LocalProverStep
  26. val klW: Double
    Definition Classes
    LocalTangentProver → LocalProverStep
  27. lazy val lemmaProofs: Task[FiniteDistribution[Term]]
    Definition Classes
    LocalProverStep
  28. lazy val lemmas: Task[Vector[(Typ[Term], Double)]]
    Definition Classes
    LocalProverStep
  29. val limit: FiniteDuration
    Definition Classes
    LocalTangentProver → LocalProverStep
  30. val maxDepth: Int
    Definition Classes
    LocalTangentProver → LocalProverStep
  31. val maxRatio: Double
    Definition Classes
    LocalTangentProver → LocalProverStep
  32. val maxTime: Option[Long]
    Definition Classes
    LocalTangentProver → LocalProverStep
  33. val mfd: MonixTangentFiniteDistributionEq[TermState]
  34. lazy val nextState: Task[TermState]
    Definition Classes
    LocalTangentProver → LocalProverStep
  35. def nodeDist[Y](node: GeneratorNode[Y]): Task[FiniteDistribution[Y]]
  36. lazy val orderedUnknowns: Task[Vector[Typ[Term]]]
    Definition Classes
    LocalProverStep
  37. def productElementNames: Iterator[String]
    Definition Classes
    Product
  38. lazy val proofComponents: Task[Vector[(Term, Double)]]
    Definition Classes
    LocalProverStep
  39. def proofTangent(tangentCutoff: Double = cutoff): Task[LocalTangentProver]
    Definition Classes
    LocalProverStep
  40. lazy val proofTerms: Task[Vector[(Term, Double)]]
    Definition Classes
    LocalProverStep
  41. val relativeEval: Boolean
    Definition Classes
    LocalTangentProver → LocalProverStep
  42. def reset(): Unit
    Definition Classes
    LocalProverStep
  43. val resolution: Double
    Definition Classes
    LocalTangentProver → LocalProverStep
  44. val scale: Double
    Definition Classes
    LocalTangentProver → LocalProverStep
  45. def scaleLimit(scale: Double): LocalProverStep
    Definition Classes
    LocalProverStep
  46. def scaledSplitLemmaProvers(scale: Double = 1.0): Task[Vector[LocalTangentProver]]
    Definition Classes
    LocalProverStep
  47. lazy val seek: Task[FiniteDistribution[Term]]
    Definition Classes
    LocalProverStep
  48. def sharpen(scale: Double = 2.0): LocalTangentProver
    Definition Classes
    LocalTangentProver → LocalProverStep
  49. val smoothing: Option[Double]
    Definition Classes
    LocalTangentProver → LocalProverStep
  50. def splitLemmaProvers(scale: Double = 1): Task[Vector[LocalTangentProver]]
    Definition Classes
    LocalProverStep
  51. def splitTangentProvers(terms: Vector[(Term, Double)]): Task[Vector[LocalTangentProver]]
    Definition Classes
    LocalProverStep
  52. val stateFromEquation: Boolean
    Definition Classes
    LocalTangentProver → LocalProverStep
  53. val steps: Int
    Definition Classes
    LocalTangentProver → LocalProverStep
  54. lazy val subGoals: Task[FiniteDistribution[Typ[Term]]]
    Definition Classes
    LocalProverStep
  55. lazy val successes: Task[Vector[(Typ[Term], Double, Term)]]
    Definition Classes
    LocalProverStep
  56. def tangentExpressionEval(x: Term, weight: Double = 1.0): Task[ExpressionEquationSolver]
    Definition Classes
    LocalProverStep
  57. def tangentProver(xs: Term*): Task[LocalTangentProver]
    Definition Classes
    LocalProverStep
  58. val tangentState: TermState
  59. val tg: TermGenParams
    Definition Classes
    LocalTangentProver → LocalProverStep
  60. lazy val theoremsByProof: Task[FiniteDistribution[Typ[Term]]]
    Definition Classes
    LocalProverStep
  61. lazy val theoremsByStatement: Task[FiniteDistribution[Typ[Term]]]
    Definition Classes
    LocalProverStep
  62. lazy val tripleT: Task[(FiniteDistribution[Term], Set[EquationNode], EqDistMemo[TermState])]
  63. lazy val tripleTypT: Task[(FiniteDistribution[Typ[Term]], Set[EquationNode], EqDistMemo[TermState])]
  64. lazy val tunedGenerators: Task[FiniteDistribution[Term]]
    Definition Classes
    LocalProverStep
  65. lazy val unknownStatements: Task[FiniteDistribution[Typ[Term]]]
    Definition Classes
    LocalProverStep
  66. def varDist[Y](rv: RandomVar[Y]): Task[FiniteDistribution[Y]]
  67. def withCutoff(ctf: Double): LocalTangentProver
    Definition Classes
    LocalTangentProver → LocalProverStep
  68. def withInit(ts: TermState): LocalProverStep
    Definition Classes
    LocalTangentProver → LocalProverStep
  69. def withLimit(l: FiniteDuration): LocalTangentProver
    Definition Classes
    LocalTangentProver → LocalProverStep
  70. def withParams(p: TermGenParams): LocalTangentProver
    Definition Classes
    LocalTangentProver → LocalProverStep