Trait/Object

ap.terfor

ComputationLogger

Related Docs: object ComputationLogger | package terfor

Permalink

trait ComputationLogger extends AnyRef

Trait that can be used to track the computation taking place in systems of equations, inequalities, etc. This is used to produce proofs.

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

Abstract Value Members

  1. abstract def antiSymmetry(leftInEq: LinearCombination, rightInEq: LinearCombination, order: TermOrder): Unit

    Permalink

    Turn two complementary inequalities into an equation

  2. abstract 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

  3. abstract 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

  4. abstract 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.

  5. abstract 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.

  6. abstract 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

  7. abstract val isLogging: Boolean

    Permalink
  8. abstract 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.

  9. abstract 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).

  10. abstract 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).

  11. abstract 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

  12. abstract 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.

  13. abstract 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

Concrete 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. final def asInstanceOf[T0]: T0

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

    Permalink

    Convenient interface for combineEquations

    Convenient interface for combineEquations

  6. val cieScope: LogScope[(IdealInt, LinearCombination, IdealInt, LinearCombination, TermOrder), (LinearCombination, LinearCombination)]

    Permalink

    Convenient interface for combineInequalities

    Convenient interface for combineInequalities

  7. def clone(): AnyRef

    Permalink
    Attributes
    protected[java.lang]
    Definition Classes
    AnyRef
    Annotations
    @throws( ... )
  8. final def eq(arg0: AnyRef): Boolean

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

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

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

    Permalink
    Definition Classes
    AnyRef → Any
  12. def hashCode(): Int

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

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

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

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

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

    Permalink

    Convenient interface for otherComputation

    Convenient interface for otherComputation

  18. final def synchronized[T0](arg0: ⇒ T0): T0

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

    Permalink
    Definition Classes
    AnyRef → Any
  20. final def wait(): Unit

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

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

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

Inherited from AnyRef

Inherited from Any

Ungrouped