certificates

Type Members

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

   

   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

   

   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

   

   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

   

   Abstract superclass of certificates with two children

5. abstract class BranchInference extends AnyRef

   

   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

   

   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

   

   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

   

9. sealed abstract class CertArithLiteral extends CertFormula

   

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

    

    Compound formulae in certificates

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

    

    Formula expressing an equation lhs = 0

    Formula expressing an equation lhs = 0

12. sealed abstract class CertFormula extends AnyRef

    

    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

    

    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

    

    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

    

    Formula expressing a positive or negative occurrence of a predicate atom

16. abstract class Certificate extends AnyRef

    

    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

    

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

18. class CertificatePrettyPrinter extends AnyRef

    

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

    

    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

    

    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

    

    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

    

    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. case class CutCertificate(cutFormula: CertFormula, _leftChild: Certificate, _rightChild: Certificate, _order: TermOrder) extends BinaryCertificate with Product with Serializable

    

    Certificate corresponding to an application of the cut rule.

    Certificate corresponding to an application of the cut rule. In the left proof branch, it will be assumed that the cutFormula holds, in the right proof branch it will be assumed that it does not hold.

24. class DagCertificateConverter extends AnyRef

    

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

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

    

    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.

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

    

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

27. class DotLineariser extends AnyRef

    

    Class for dumping a certificate in the dot/GraphViz format

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

    

    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.

29. class LemmaBase extends AnyRef

    

    Mutable class for managing sets of certificates.

30. class LoggingBranchInferenceCollector extends BranchInferenceCollector

    

    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.

31. abstract class MacroInference extends BranchInference

    

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

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

    

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

33. abstract class PartialCertificate extends AnyRef

    

    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.

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

    

    An inference encapsulating the application of a unary PartialCertificate.

    An inference encapsulating the application of a unary PartialCertificate.

35. class PartialCombCertificate extends PartialCertificate

    

    Partial certificate representing branching proof nodes.

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

    

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

37. class PartialFixedCertificate extends PartialCertificate

    

    A partial certificate with a fixed result.

38. class PartialInferenceCertificate extends PartialCertificate

    

    Partial certificate prepending given inferences to some certificate.

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

    

    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

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

    

    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.

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

    

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

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

    

    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

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

    

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

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

    

    Certificate corresponding to splitting a negated equation into two inequalities.

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

    

    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.

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

    

    An inference describing the introduction of a theory axiom.