Object

ap.proof.certificates

NonLoggingBranchInferenceCollector

Related Doc: package certificates

Permalink

object NonLoggingBranchInferenceCollector extends NonLoggingLogger with BranchInferenceCollector

Linear Supertypes
Ordering
  1. Alphabetic
  2. By inheritance
Inherited
  1. NonLoggingBranchInferenceCollector
  2. BranchInferenceCollector
  3. NonLoggingLogger
  4. ComputationLogger
  5. AnyRef
  6. Any
  1. Hide All
  2. Show all
Visibility
  1. Public
  2. All

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 columnReduce(oldSymbol: ConstantTerm, newSymbol: ConstantTerm, newSymbolDef: LinearCombination, subst: Boolean, newOrder: TermOrder): Unit

    Permalink

    Inference corresponding to an application of the col-red or col-red-subst rule.

    Inference corresponding to an application of the col-red or col-red-subst rule. This will simply introduce a new constant newSymbol that is defined as the term newSymbolDef.

    This method is not added in the ComputationLogger, because it is never used in the ter/for datastructures.

    Definition Classes
    NonLoggingBranchInferenceCollectorBranchInferenceCollector
  10. 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
  11. 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
  12. 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
  13. 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
  14. def divRight(divisibility: Conjunction, result: Conjunction, order: TermOrder): Unit

    Permalink

    An inference that turns a universally quantified divisibility constraint into an existentially quantified disjunction of equations.

    An inference that turns a universally quantified divisibility constraint into an existentially quantified disjunction of equations.

    Definition Classes
    NonLoggingBranchInferenceCollectorBranchInferenceCollector
  15. final def eq(arg0: AnyRef): Boolean

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

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

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

    Permalink
    Definition Classes
    AnyRef → Any
  19. def getCollection: BranchInferenceCollection

    Permalink
  20. 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
  21. def hashCode(): Int

    Permalink
    Definition Classes
    AnyRef → Any
  22. def instantiateQuantifier(quantifiedFormula: Conjunction, newConstants: Seq[ConstantTerm], result: Conjunction, order: TermOrder): Unit

    Permalink

    Inference corresponding to applications of the rules all-left, ex-left, etc.

    Inference corresponding to applications of the rules all-left, ex-left, etc. A uniform prefix of quantifiers (only forall or only exists) is instantiated with a single inference. newConstants are the constants introduced to instantiate the quantifiers, starting with the innermost instantiated quantifier.

    Definition Classes
    NonLoggingBranchInferenceCollectorBranchInferenceCollector
  23. final def isInstanceOf[T0]: Boolean

    Permalink
    Definition Classes
    Any
  24. val isLogging: Boolean

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

    Permalink
    Definition Classes
    AnyRef
  26. def newCertFormula(f: CertFormula): Unit

    Permalink

    Inform the collector that a new formula has occurred on the branch (important for alpha-rules)

    Inform the collector that a new formula has occurred on the branch (important for alpha-rules)

    Definition Classes
    NonLoggingBranchInferenceCollectorBranchInferenceCollector
  27. def newFormula(f: Conjunction): Unit

    Permalink

    Inform the collector that a new formula has occurred on the branch (important for alpha-rules)

    Inform the collector that a new formula has occurred on the branch (important for alpha-rules)

    Definition Classes
    NonLoggingBranchInferenceCollectorBranchInferenceCollector
  28. final def notify(): Unit

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

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

    Permalink

    Convenient interface for otherComputation

    Convenient interface for otherComputation

    Definition Classes
    ComputationLogger
  31. 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
  32. 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
  33. 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
  34. 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
  35. final def synchronized[T0](arg0: ⇒ T0): T0

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

    Permalink
    Definition Classes
    AnyRef → Any
  37. 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
  38. 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
  39. final def wait(): Unit

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

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

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

Inherited from BranchInferenceCollector

Inherited from NonLoggingLogger

Inherited from ComputationLogger

Inherited from AnyRef

Inherited from Any

Ungrouped