Class/Object

ap.proof.certificates

LoggingBranchInferenceCollector

Related Docs: object LoggingBranchInferenceCollector | package certificates

Permalink

class LoggingBranchInferenceCollector extends BranchInferenceCollector

Mutable datastructure for collecting inferences during some computation. To avoid having to pass around collectors all over the place, a dynamic variable is used to realise context collectors.

Linear Supertypes
Ordering
  1. Alphabetic
  2. By inheritance
Inherited
  1. LoggingBranchInferenceCollector
  2. BranchInferenceCollector
  3. ComputationLogger
  4. AnyRef
  5. 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
    LoggingBranchInferenceCollectorComputationLogger
  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
    LoggingBranchInferenceCollectorBranchInferenceCollector
  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
    LoggingBranchInferenceCollectorComputationLogger
  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
    LoggingBranchInferenceCollectorComputationLogger
  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
    LoggingBranchInferenceCollectorComputationLogger
  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
    LoggingBranchInferenceCollectorComputationLogger
  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
    LoggingBranchInferenceCollectorBranchInferenceCollector
  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
    LoggingBranchInferenceCollectorComputationLogger
  21. def hashCode(): Int

    Permalink
    Definition Classes
    AnyRef → Any
  22. var inferences: List[BranchInference]

    Permalink
  23. 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
    LoggingBranchInferenceCollectorBranchInferenceCollector
  24. final def isInstanceOf[T0]: Boolean

    Permalink
    Definition Classes
    Any
  25. val isLogging: Boolean

    Permalink
  26. final def ne(arg0: AnyRef): Boolean

    Permalink
    Definition Classes
    AnyRef
  27. 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
    LoggingBranchInferenceCollectorBranchInferenceCollector
  28. 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
    LoggingBranchInferenceCollectorBranchInferenceCollector
  29. final def notify(): Unit

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

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

    Permalink

    Convenient interface for otherComputation

    Convenient interface for otherComputation

    Definition Classes
    ComputationLogger
  32. def otherComputation(assumptions: Seq[Formula], result: Formula, order: TermOrder, theoryAnyRef: 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
    LoggingBranchInferenceCollectorComputationLogger
  33. 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
    LoggingBranchInferenceCollectorComputationLogger
  34. 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
    LoggingBranchInferenceCollectorComputationLogger
  35. 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
    LoggingBranchInferenceCollectorComputationLogger
  36. final def synchronized[T0](arg0: ⇒ T0): T0

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

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

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

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

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

Inherited from BranchInferenceCollector

Inherited from ComputationLogger

Inherited from AnyRef

Inherited from Any

Ungrouped