Package

ap.proof

certificates

Permalink

package certificates

Visibility
  1. Public
  2. All

Type Members

  1. case class AlphaInference(splitFormula: CertCompoundFormula, providedFormulas: Set[CertFormula]) extends BranchInference with Product with Serializable

    Permalink

    Inference corresponding to an application of alpha rules.

  2. case class AntiSymmetryInference(leftInEq: CertInequality, rightInEq: CertInequality, result: CertEquation, order: TermOrder) extends BranchInference with Product with Serializable

    Permalink

    Turn two complementary inequalities into an equation

  3. case class BetaCertificate(leftFormula: CertFormula, rightFormula: CertFormula, lemma: Boolean, _leftChild: Certificate, _rightChild: Certificate, _order: TermOrder) extends BinaryCertificate with Product with Serializable

    Permalink

    Certificate corresponding to an application of beta rules with lemmas: the rule describes the splitting of an antecedent formula leftFormula | rightFormula into the cases leftFormula and !leftFormula, rightFormula.

    Certificate corresponding to an application of beta rules with lemmas: the rule describes the splitting of an antecedent formula leftFormula | rightFormula into the cases leftFormula and !leftFormula, rightFormula. (If lemma is not set, the second case is just rightFormula)

  4. abstract class BinaryCertificate extends Certificate

    Permalink

    Abstract superclass of certificates with two children

  5. abstract class BranchInference extends AnyRef

    Permalink

    Abstract superclass of all inferences that do not cause proof splitting and that do not close proof branches

  6. case class BranchInferenceCertificate(inferences: Seq[BranchInference], _child: Certificate, order: TermOrder) extends CertificateOneChild with Product with Serializable

    Permalink

    Inferences that do not cause proof splitting and that do not close a branch are collected in nodes of this class.

  7. class BranchInferenceCollection extends AnyRef

    Permalink

    Class to store sets of branch inferences in goals.

    Class to store sets of branch inferences in goals. Currently, the inferences are just kept in a list, but this might change at a late point. This is an immutable datastructure, for dynamically collecting inferences use BranchInferenceCollector.

  8. trait BranchInferenceCollector extends ComputationLogger

    Permalink
  9. sealed abstract class CertArithLiteral extends CertFormula

    Permalink
  10. case class CertCompoundFormula(f: Conjunction) extends CertFormula with SortedWithOrder[CertCompoundFormula] with Product with Serializable

    Permalink

    Compound formulae in certificates

  11. case class CertEquation(_lhs: LinearCombination) extends CertArithLiteral with SortedWithOrder[CertEquation] with Product with Serializable

    Permalink

    Formula expressing an equation lhs = 0

    Formula expressing an equation lhs = 0

  12. sealed abstract class CertFormula extends AnyRef

    Permalink

    Hierarchy of formulae specifically for representing certificates; the reason is that the standard formula datastructures perform too much simplification implicitly

  13. case class CertInequality(_lhs: LinearCombination) extends CertArithLiteral with SortedWithOrder[CertInequality] with Product with Serializable

    Permalink

    Formula expressing an inequality lhs >= 0

    Formula expressing an inequality lhs >= 0

  14. case class CertNegEquation(_lhs: LinearCombination) extends CertArithLiteral with SortedWithOrder[CertNegEquation] with Product with Serializable

    Permalink

    Formula expressing a negated equation lhs != 0

    Formula expressing a negated equation lhs != 0

  15. case class CertPredLiteral(negated: Boolean, atom: Atom) extends CertFormula with SortedWithOrder[CertPredLiteral] with Product with Serializable

    Permalink

    Formula expressing a positive or negative occurrence of a predicate atom

  16. abstract class Certificate extends AnyRef

    Permalink

    Datastructures used to express and extract whole, detailed proofs, which can independently be checked and be used for further processing (e.g., to compute interpolants).

    Datastructures used to express and extract whole, detailed proofs, which can independently be checked and be used for further processing (e.g., to compute interpolants). Certificates are trees/proof terms, with the following class as the abstract superclass of all tree nodes. Proofs are more or less tableau proofs, with rule applications assuming certain formulae on a branch and producing new formulae.

  17. abstract class CertificateOneChild extends Certificate

    Permalink

    Abstract superclass of all certificate nodes that only have a single subtree

  18. class CertificatePrettyPrinter extends AnyRef

    Permalink
  19. case class CloseCertificate(localAssumedFormulas: Set[CertFormula], order: TermOrder) extends Certificate with Product with Serializable

    Permalink

    Certificate corresponding to an application of the close rule.

  20. case class ColumnReduceInference(oldSymbol: ConstantTerm, newSymbol: ConstantTerm, definingEquation: CertEquation, subst: Boolean, order: TermOrder) extends BranchInference with Product with Serializable

    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 by definingEquation.

  21. case class CombineEquationsInference(equations: Seq[(IdealInt, CertEquation)], result: CertEquation, order: TermOrder) extends BranchInference with Product with Serializable

    Permalink

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

    Inference corresponding to a series of applications of the reduce rule: form the linear combination of a sequence of equations. The result is implicitly made primitive (divided by common coefficients)

  22. case class CombineInequalitiesInference(leftCoeff: IdealInt, leftInEq: CertInequality, rightCoeff: IdealInt, rightInEq: CertInequality, result: CertInequality, order: TermOrder) extends BranchInference with Product with Serializable

    Permalink

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

    Inference corresponding to a series of applications of the reduce rule: form the linear combination of a sequence of equations. The result is implicitly made primitive (divided by common coefficients) and rounded

  23. class DagCertificateConverter extends AnyRef

    Permalink

    Class for converting a given certificate to a DAG, by factoring out shared sub-certificates.

  24. case class DirectStrengthenInference(inequality: CertInequality, equation: CertNegEquation, result: CertInequality, order: TermOrder) extends BranchInference with Product with Serializable

    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. This kind of inference exists as a separate rule to keep certificates more compact.

  25. case class DivRightInference(divisibility: CertCompoundFormula, result: CertCompoundFormula, order: TermOrder) extends BranchInference with Product with Serializable

    Permalink

    An inference that turns a universally quantified divisibility constraint into an existentially quantified conjunction of inequalities and an equation.

  26. class DotLineariser extends AnyRef

    Permalink

    Class for dumping a certificate in the dot/GraphViz format

  27. case class GroundInstInference(quantifiedFormula: CertCompoundFormula, instanceTerms: Seq[LinearCombination], instance: CertFormula, dischargedAtoms: Seq[CertPredLiteral], result: CertFormula, order: TermOrder) extends BranchInference with Product with Serializable

    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.

  28. class LemmaBase extends AnyRef

    Permalink

    Mutable class for managing sets of certificates.

  29. class LoggingBranchInferenceCollector extends BranchInferenceCollector

    Permalink

    Mutable datastructure for collecting inferences during some computation.

    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.

  30. abstract class MacroInference extends BranchInference

    Permalink

    An inference encapsulating multiple inferences, to be expanded on demand.

  31. case class OmegaCertificate(elimConst: ConstantTerm, boundsA: Seq[CertInequality], boundsB: Seq[CertInequality], children: Seq[Certificate], order: TermOrder) extends Certificate with Product with Serializable

    Permalink

    Certificate corresponding to an application of the Omega rule, which has the same effect as repeated application of Strengthen to the inequalities boundsA in a goal.

    Certificate corresponding to an application of the Omega rule, which has the same effect as repeated application of Strengthen to the inequalities boundsA in a goal.

    For each of the inequalities in boundsA, strengthenCases tells how often Strengthen is applied. The counting works just like in StrengthenCertificate, i.e., 1 means that Strenghten is applied once (and there are two cases).

  32. abstract class PartialCertificate extends AnyRef

    Permalink

    Class representing a mapping from a vector of certificates to a single new certificate.

    Class representing a mapping from a vector of certificates to a single new certificate. This is used to handle certificate extraction in branching proofs.

  33. case class PartialCertificateInference(pCert: PartialCertificate, _providedFormulas: Set[CertFormula], _boundConstants: Set[ConstantTerm]) extends BranchInference with Product with Serializable

    Permalink

    An inference encapsulating the application of a unary PartialCertificate.

    An inference encapsulating the application of a unary PartialCertificate.

  34. class PartialCombCertificate extends PartialCertificate

    Permalink

    Partial certificate representing branching proof nodes.

  35. case class PartialCompositionCertificate(first: Seq[PartialCertificate], second: PartialCertificate) extends PartialCertificate with Product with Serializable

    Permalink

    Composition of a partial certificate and a sequence of partial certificates.

  36. class PartialFixedCertificate extends PartialCertificate

    Permalink

    A partial certificate with a fixed result.

  37. class PartialInferenceCertificate extends PartialCertificate

    Permalink

    Partial certificate prepending given inferences to some certificate.

  38. case class PredUnifyInference(leftAtom: Atom, rightAtom: Atom, result: CertFormula, order: TermOrder) extends BranchInference with Product with Serializable

    Permalink

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

  39. case class QuantifierInference(quantifiedFormula: CertCompoundFormula, newConstants: Seq[ConstantTerm], result: CertFormula, order: TermOrder) extends BranchInference with Product with Serializable

    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.

  40. case class ReduceInference(equations: Seq[(IdealInt, CertEquation)], targetLit: CertArithLiteral, result: CertArithLiteral, order: TermOrder) extends BranchInference with Product with Serializable

    Permalink

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

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

  41. case class ReducePredInference(equations: Seq[Seq[(IdealInt, CertEquation)]], targetLit: CertPredLiteral, result: CertPredLiteral, order: TermOrder) extends BranchInference with Product with Serializable

    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 ReduceInference, only that all of the arguments can be reduced simultaneously

  42. case class SimpInference(targetLit: CertArithLiteral, result: CertArithLiteral, order: TermOrder) extends BranchInference with Product with Serializable

    Permalink

    Inference representing the simplification of an equation, a negated equation, or an inequality

  43. case class SplitEqCertificate(leftInEq: CertInequality, rightInEq: CertInequality, _leftChild: Certificate, _rightChild: Certificate, _order: TermOrder) extends BinaryCertificate with Product with Serializable

    Permalink

    Certificate corresponding to splitting a negated equation into two inequalities.

  44. case class StrengthenCertificate(weakInEq: CertInequality, eqCases: IdealInt, children: Seq[Certificate], order: TermOrder) extends Certificate with Product with Serializable

    Permalink

    Certificate corresponding to a (possibly repeated) application of the strengthen rule: the inequality weakInEq(0) >= 0 is strengthened to the equations weakInEq(0) === 0, weakInEq(0) === 1, etc.

    Certificate corresponding to a (possibly repeated) application of the strengthen rule: the inequality weakInEq(0) >= 0 is strengthened to the equations weakInEq(0) === 0, weakInEq(0) === 1, etc. and the inequality weakInEq(0) >= eqCases.

  45. case class TheoryAxiomInference(axiom: CertFormula, theory: Theory) extends BranchInference with Product with Serializable

    Permalink

    An inference describing the introduction of a theory axiom.

Value Members

  1. object AlphaInference extends Serializable

    Permalink
  2. object AntiSymmetryInference extends Serializable

    Permalink
  3. object BetaCertificate extends Serializable

    Permalink
  4. object BetaCertificateHelper

    Permalink
  5. object BranchInference

    Permalink
  6. object BranchInferenceCertificate extends Serializable

    Permalink
  7. object BranchInferenceCollection

    Permalink
  8. object CertCompoundFormula extends Serializable

    Permalink
  9. object CertFormula

    Permalink
  10. object Certificate

    Permalink
  11. object CertificatePrettyPrinter

    Permalink
  12. object CloseCertificate extends Serializable

    Permalink
  13. object ColumnReduceInference extends Serializable

    Permalink
  14. object CombineEquationsInference extends Serializable

    Permalink
  15. object CombineInequalitiesInference extends Serializable

    Permalink
  16. object DagCertificateConverter

    Permalink
  17. object DirectStrengthenInference extends Serializable

    Permalink
  18. object DivRightInference extends Serializable

    Permalink
  19. object DotLineariser

    Permalink
  20. object GroundInstInference extends Serializable

    Permalink
  21. object LemmaBase

    Permalink
  22. object LoggingBranchInferenceCollector

    Permalink
  23. object MacroInference

    Permalink
  24. object NonLoggingBranchInferenceCollector extends NonLoggingLogger with BranchInferenceCollector

    Permalink
  25. object OmegaCertificate extends Serializable

    Permalink
  26. object PartialCertificate

    Permalink
  27. object PartialCertificateInference extends Serializable

    Permalink
  28. object PartialIdentityCertificate extends PartialCertificate with Product with Serializable

    Permalink

    Partial certificate that represents the identify function.

  29. object PredUnifyInference extends Serializable

    Permalink
  30. object QuantifierInference extends Serializable

    Permalink
  31. object ReduceInference extends Serializable

    Permalink
  32. object ReducePredInference extends Serializable

    Permalink
  33. object ReusedProofMarker extends BranchInference

    Permalink

    Inference marking that the following sub-proof has been reused from a previous point.

  34. object SimpInference extends Serializable

    Permalink
  35. object SplitEqCertificate extends Serializable

    Permalink
  36. object StrengthenCertificate extends Serializable

    Permalink
  37. object StrengthenCertificateHelper

    Permalink

Ungrouped