Trait

ap.proof.certificates

BranchInferenceCollector

Related Doc: package certificates

Permalink

trait BranchInferenceCollector extends ComputationLogger

Linear Supertypes
ComputationLogger, AnyRef, Any
Known Subclasses
Ordering
  1. Alphabetic
  2. By Inheritance
Inherited
  1. BranchInferenceCollector
  2. ComputationLogger
  3. AnyRef
  4. 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

    Turn two complementary inequalities into an equation

    Definition Classes
    ComputationLogger
  2. abstract 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.

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

    Definition Classes
    ComputationLogger
  4. 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

    Definition Classes
    ComputationLogger
  5. 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.

    Definition Classes
    ComputationLogger
  6. 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.

    Definition Classes
    ComputationLogger
  7. abstract 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.

  8. abstract def getCollection: BranchInferenceCollection

    Permalink
  9. 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

    Instantiate a universally quantified formula with ground terms

    Definition Classes
    ComputationLogger
  10. abstract 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.

  11. abstract val isLogging: Boolean

    Permalink
    Definition Classes
    ComputationLogger
  12. abstract def newCertFormula(f: CertFormula): Unit

    Permalink

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

  13. abstract def newFormula(f: Conjunction): Unit

    Permalink

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

  14. 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.

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

    Definition Classes
    ComputationLogger
  15. 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).

    Definition Classes
    ComputationLogger
  16. 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).

    Definition Classes
    ComputationLogger
  17. 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

    Definition Classes
    ComputationLogger
  18. 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.

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

    Definition Classes
    ComputationLogger
  19. 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

    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
    ComputationLogger

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

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

    Permalink

    Convenient interface for combineInequalities

    Convenient interface for combineInequalities

    Definition Classes
    ComputationLogger
  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

    Definition Classes
    ComputationLogger
  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 ComputationLogger

Inherited from AnyRef

Inherited from Any

Ungrouped