Class

ap.terfor.ComputationLogger

NonLoggingLogger

Related Doc: package ComputationLogger

Permalink

class NonLoggingLogger extends ComputationLogger

Linear Supertypes
ComputationLogger, AnyRef, Any
Known Subclasses
Ordering
  1. Alphabetic
  2. By inheritance
Inherited
  1. NonLoggingLogger
  2. ComputationLogger
  3. AnyRef
  4. Any
  1. Hide All
  2. Show all
Visibility
  1. Public
  2. All

Instance Constructors

  1. new NonLoggingLogger()

    Permalink

Value Members

  1. final def !=(arg0: Any): Boolean

    Permalink
    Definition Classes
    AnyRef → Any
  2. final def ##(): Int

    Permalink
    Definition Classes
    AnyRef → Any
  3. final def ==(arg0: Any): Boolean

    Permalink
    Definition Classes
    AnyRef → Any
  4. def antiSymmetry(leftInEq: LinearCombination, rightInEq: LinearCombination, order: TermOrder): Unit

    Permalink

    Turn two complementary inequalities into an equation

    Turn two complementary inequalities into an equation

    Definition Classes
    NonLoggingLoggerComputationLogger
  5. final def asInstanceOf[T0]: T0

    Permalink
    Definition Classes
    Any
  6. val ceScope: LogScope[(Seq[(IdealInt, LinearCombination)], TermOrder), (LinearCombination, LinearCombination)]

    Permalink

    Convenient interface for combineEquations

    Convenient interface for combineEquations

    Definition Classes
    ComputationLogger
  7. val cieScope: LogScope[(IdealInt, LinearCombination, IdealInt, LinearCombination, TermOrder), (LinearCombination, LinearCombination)]

    Permalink

    Convenient interface for combineInequalities

    Convenient interface for combineInequalities

    Definition Classes
    ComputationLogger
  8. def clone(): AnyRef

    Permalink
    Attributes
    protected[java.lang]
    Definition Classes
    AnyRef
    Annotations
    @throws( ... )
  9. def combineEquations(equations: Seq[(IdealInt, LinearCombination)], result: LinearCombination, resultAfterRounding: LinearCombination, order: TermOrder): Unit

    Permalink

    Inference corresponding to a series of applications of the reduce rule: form the linear combination of a number of positive equations.

    Inference corresponding to a series of applications of the reduce rule: form the linear combination of a number of positive equations. The given terms (apart from result) shall be primitive, with a positive leading coefficient

    Definition Classes
    NonLoggingLoggerComputationLogger
  10. def combineInequalities(leftCoeff: IdealInt, leftInEq: LinearCombination, rightCoeff: IdealInt, rightInEq: LinearCombination, result: LinearCombination, resultAfterRounding: LinearCombination, order: TermOrder): Unit

    Permalink

    Fourier-Motzkin Inference.

    Fourier-Motzkin Inference. The given terms shall be primitive, and the result will be implicitly rounded

    Definition Classes
    NonLoggingLoggerComputationLogger
  11. def combineInequalitiesLazy(ineqs: Iterator[(IdealInt, LinearCombination)], resultAfterRounding: LinearCombination, order: TermOrder): Unit

    Permalink

    Compute the sum of multiple inequalities, and round the result afterwards.

    Compute the sum of multiple inequalities, and round the result afterwards. The argument ineqs might be stored and evaluated much later, or not at all if the represented inference turns out to be unnecessary.

    Definition Classes
    NonLoggingLoggerComputationLogger
  12. def directStrengthen(inequality: LinearCombination, equation: LinearCombination, result: LinearCombination, order: TermOrder): Unit

    Permalink

    Given the two formulae t >= 0 and t != 0 (or, similarly, t >= 0 and -t != 0), infer the inequality t-1 >= 0.

    Given the two formulae t >= 0 and t != 0 (or, similarly, t >= 0 and -t != 0), infer the inequality t-1 >= 0.

    Definition Classes
    NonLoggingLoggerComputationLogger
  13. final def eq(arg0: AnyRef): Boolean

    Permalink
    Definition Classes
    AnyRef
  14. def equals(arg0: Any): Boolean

    Permalink
    Definition Classes
    AnyRef → Any
  15. def finalize(): Unit

    Permalink
    Attributes
    protected[java.lang]
    Definition Classes
    AnyRef
    Annotations
    @throws( classOf[java.lang.Throwable] )
  16. final def getClass(): Class[_]

    Permalink
    Definition Classes
    AnyRef → Any
  17. def groundInstantiateQuantifier(quantifiedFormula: Conjunction, instanceTerms: Seq[LinearCombination], instance: Conjunction, dischargedAtoms: PredConj, result: Conjunction, order: TermOrder): Unit

    Permalink

    Instantiate a universally quantified formula with ground terms

    Instantiate a universally quantified formula with ground terms

    Definition Classes
    NonLoggingLoggerComputationLogger
  18. def hashCode(): Int

    Permalink
    Definition Classes
    AnyRef → Any
  19. final def isInstanceOf[T0]: Boolean

    Permalink
    Definition Classes
    Any
  20. val isLogging: Boolean

    Permalink
    Definition Classes
    NonLoggingLoggerComputationLogger
  21. final def ne(arg0: AnyRef): Boolean

    Permalink
    Definition Classes
    AnyRef
  22. final def notify(): Unit

    Permalink
    Definition Classes
    AnyRef
  23. final def notifyAll(): Unit

    Permalink
    Definition Classes
    AnyRef
  24. val otherCompScope: LogScope[(Seq[Formula], TermOrder, AnyRef), Formula]

    Permalink

    Convenient interface for otherComputation

    Convenient interface for otherComputation

    Definition Classes
    ComputationLogger
  25. def otherComputation(assumptions: Seq[Formula], result: Formula, order: TermOrder, theory: AnyRef): Unit

    Permalink

    Some other computation, that might in particular be performed by theory plug-ins.

    Some other computation, that might in particular be performed by theory plug-ins.

    Definition Classes
    NonLoggingLoggerComputationLogger
  26. def reduceInequality(equations: Seq[(IdealInt, LinearCombination)], targetLit: LinearCombination, order: TermOrder): Unit

    Permalink

    Inference corresponding to a series of applications of the reduce rule to a an inequality (reduction of positive equalities is described using CombineEquationsInference).

    Inference corresponding to a series of applications of the reduce rule to a an inequality (reduction of positive equalities is described using CombineEquationsInference).

    Definition Classes
    NonLoggingLoggerComputationLogger
  27. def reduceNegEquation(equations: Seq[(IdealInt, LinearCombination)], targetLit: LinearCombination, order: TermOrder): Unit

    Permalink

    Inference corresponding to a series of applications of the reduce rule to a negated equation (reduction of positive equalities is described using CombineEquationsInference).

    Inference corresponding to a series of applications of the reduce rule to a negated equation (reduction of positive equalities is described using CombineEquationsInference).

    Definition Classes
    NonLoggingLoggerComputationLogger
  28. def reducePredFormula(equations: Seq[Seq[(IdealInt, LinearCombination)]], targetLit: Atom, negated: Boolean, result: Atom, order: TermOrder): Unit

    Permalink

    Inference corresponding to a series of applications of the reduce rule to the arguments of a predicate literal.

    Inference corresponding to a series of applications of the reduce rule to the arguments of a predicate literal. This is essentially the same as the reduceArithFormula, only that all of the arguments can be reduced simultaneously

    Definition Classes
    NonLoggingLoggerComputationLogger
  29. final def synchronized[T0](arg0: ⇒ T0): T0

    Permalink
    Definition Classes
    AnyRef
  30. def toString(): String

    Permalink
    Definition Classes
    AnyRef → Any
  31. def unifyFunctionApps(leftApp: Atom, rightApp: Atom, resultEq: LinearCombination, order: TermOrder): Unit

    Permalink

    Apply the functional consistency axiom to derive that the results of two function applications (encoded as predicate atoms) must be the same.

    Apply the functional consistency axiom to derive that the results of two function applications (encoded as predicate atoms) must be the same.

    Definition Classes
    NonLoggingLoggerComputationLogger
  32. def unifyPredicates(leftAtom: Atom, rightAtom: Atom, result: EquationConj, order: TermOrder): Unit

    Permalink

    Unify two predicates, producing a system of equations (in the succedent) that express the unification conditions: the predicate arguments are matched pair-wise

    Unify two predicates, producing a system of equations (in the succedent) that express the unification conditions: the predicate arguments are matched pair-wise

    Definition Classes
    NonLoggingLoggerComputationLogger
  33. final def wait(): Unit

    Permalink
    Definition Classes
    AnyRef
    Annotations
    @throws( ... )
  34. final def wait(arg0: Long, arg1: Int): Unit

    Permalink
    Definition Classes
    AnyRef
    Annotations
    @throws( ... )
  35. final def wait(arg0: Long): Unit

    Permalink
    Definition Classes
    AnyRef
    Annotations
    @throws( ... )

Inherited from ComputationLogger

Inherited from AnyRef

Inherited from Any

Ungrouped