Packages

p

ap

parser

package parser

Ordering
  1. Alphabetic
Visibility
  1. Public
  2. Protected

Type Members

  1. abstract class AbstractCompleteFunctionPreproc extends FunctionPreproc

    Introduction of triggers using the complete strategy that avoids the need for totality axioms (as in Kanger's calculus).

  2. abstract class AbstractVariableSubstVisitor extends CollectingVisitor[(List[ITerm], Int), IExpression]
  3. class ApParser2InputAbsy extends Parser2InputAbsy[Unit, Sort, Unit, Unit, Sort, Unit]
  4. abstract class CollectingVisitor[A, R] extends AnyRef

    Visitor schema that traverses an expression in depth-first left-first order.

    Visitor schema that traverses an expression in depth-first left-first order. For each node, the method preVisit is called when descending and the method postVisit when returning. The visitor works with iteration (not recursion) and is able to deal also with large expressions

  5. class CompleteFrugalFunctionPreproc extends AbstractCompleteFunctionPreproc

    Introduction of triggers using the complete strategy that avoids the need for totality axioms (as in Kanger's calculus).

  6. class CompleteFunctionPreproc extends AbstractCompleteFunctionPreproc

    Introduction of triggers using the complete strategy that avoids the need for totality axioms (as in Kanger's calculus).

  7. case class Context[A](binders: List[Binder], boundSorts: List[Sort], polarity: Int, a: A) extends Product with Serializable
  8. abstract class ContextAwareVisitor[A, R] extends CollectingVisitor[Context[A], R]

    An extended version of the CollectingVisitor that also keeps track of the sign of a sub-expression (positive or negative), and of the bound variables.

  9. class Environment[ConstantType, VariableType, PredicateType, FunctionType, SortType] extends Cloneable
  10. class FunctionCollector extends CollectingVisitor[Int, Unit]

    Class for collecting the functions occurring in an expression.

  11. class FunctionEncoder extends Cloneable

    Class to generate a relational encoding of functions.

    Class to generate a relational encoding of functions. This means that an (n+1)-ary predicate is introduced for each n-ary function, together with axioms for totality and functionality, and that all applications of the function are replaced referring to the predicate. The state of the class consists of the mapping from functions to relations (so far), as well as the axioms that have been introduced for the relational encoding.

  12. abstract class FunctionPreproc extends AnyRef

    Class managing the generation of triggers for e-matching, and the encoding of functions using relations.

    Class managing the generation of triggers for e-matching, and the encoding of functions using relations. This class is called from Preprocessing.

  13. case class IAtom(pred: Predicate, args: Seq[ITerm]) extends IFormula with Product with Serializable

    Application of an uninterpreted predicate to a list of terms.

  14. case class IBinFormula(j: IBinJunctor.Value, f1: IFormula, f2: IFormula) extends IFormula with Product with Serializable

    Boolean combination of two formulae.

  15. case class IBoolLit(value: Boolean) extends IFormula with Product with Serializable

    Boolean literal.

  16. case class IConstant(c: ConstantTerm) extends ITerm with Product with Serializable

    Symbolic constants.

  17. abstract class IEpsilon extends ITerm with IVariableBinder

    Epsilon term, which is defined to evaluate to an arbitrary value satisfying the formula cond.

    Epsilon term, which is defined to evaluate to an arbitrary value satisfying the formula cond. cond is expected to contain a bound variable with de Bruijn index 0 and the given sort.

  18. case class IEquation(left: ITerm, right: ITerm) extends IFormula with Product with Serializable

    Equation between two terms.

  19. abstract class IExpression extends AnyRef

    Abstract syntax for prover input.

    Abstract syntax for prover input. The language represented by the following constructors is more general than the logic that the prover actually can handle (e.g., there are also functions, equivalence, etc.). The idea is that inputs first have to be normalised in some way so that the prover can handle them.

  20. abstract class IFormula extends IExpression

    Abstract class representing formulae in input-syntax.

  21. case class IFormulaITE(cond: IFormula, left: IFormula, right: IFormula) extends IFormula with Product with Serializable

    If-then-else formula.

  22. case class IFunApp(fun: IFunction, args: Seq[ITerm]) extends ITerm with Product with Serializable

    Application of an uninterpreted function to a list of terms.

  23. class IFunction extends AnyRef

    An uninterpreted function with fixed arity.

    An uninterpreted function with fixed arity. The function can optionally be partial (no totality axiom) or relational (no functionality axiom).

  24. case class IIntFormula(rel: IIntRelation.Value, t: ITerm) extends IFormula with Product with Serializable

    Integer equation or inequality.

  25. case class IIntLit(value: IdealInt) extends ITerm with Product with Serializable

    Integer literals.

  26. case class IInterpolantSpec(left: List[PartName], right: List[PartName]) extends Product with Serializable

    Specification of an interpolation problem, consisting of two lists of formula names.

  27. case class INamedPart(name: PartName, subformula: IFormula) extends IFormula with Product with Serializable

    A labelled formula with name name.

  28. case class INot(subformula: IFormula) extends IFormula with Product with Serializable

    Negation of a formula.

  29. case class IPlus(t1: ITerm, t2: ITerm) extends ITerm with Product with Serializable

    Sum of two terms.

  30. abstract class IQuantified extends IFormula with IVariableBinder

    Application of a quantifier to a formula containing a free variable with de Bruijn index 0 and the given sort.

  31. case class ISortedEpsilon(sort: Sort, cond: IFormula) extends IEpsilon with Product with Serializable

    Epsilon term, which is defined to evaluate to an arbitrary value satisfying the formula cond.

    Epsilon term, which is defined to evaluate to an arbitrary value satisfying the formula cond. cond is expected to contain a bound variable with de Bruijn index 0 and the given sort.

  32. case class ISortedQuantified(quan: Quantifier, sort: Sort, subformula: IFormula) extends IQuantified with Product with Serializable

    Application of a quantifier to a formula containing a free variable with de Bruijn index 0 and the given sort.

  33. case class ISortedVariable(index: Int, sort: Sort) extends IVariable with Product with Serializable

    Bound variables, represented using their de Bruijn index and the sort.

  34. abstract class ITerm extends IExpression

    Abstract class representing terms in input-syntax.

  35. case class ITermITE(cond: IFormula, left: ITerm, right: ITerm) extends ITerm with Product with Serializable

    If-then-else term.

  36. case class ITimes(coeff: IdealInt, subterm: ITerm) extends ITerm with Product with Serializable

    Product between a term and an integer coefficient.

  37. case class ITrigger(patterns: Seq[ITerm], subformula: IFormula) extends IFormula with Product with Serializable

    Trigger/patterns that are used to define in which way a quantified formula is supposed to be instantiated.

    Trigger/patterns that are used to define in which way a quantified formula is supposed to be instantiated. Triggers are only allowed to occur immediately after (inside) a quantifier. This class can both represent uni-triggers (for patterns.size == 1 and multi-triggers.

  38. abstract class IVarShift extends AnyRef
  39. case class IVarShiftList(prefix: List[Int], defaultShift: Int) extends IVarShift with Product with Serializable
  40. case class IVarShiftMap(prefix: List[Int], mapping: Map[Int, Int], defaultShift: Int) extends IVarShift with Product with Serializable
  41. case class IVarShiftMapEmptyPrefix(prefixLength: Int, mapping: Map[Int, Int], defaultShift: Int) extends IVarShift with Product with Serializable

    Special case for a prefix only containing zeroes

  42. abstract class IVariable extends ITerm

    Bound variables, represented using their de Bruijn index and the sort.

  43. trait IVariableBinder extends AnyRef

    Common trait for IExpression classes that bind variables.

    Common trait for IExpression classes that bind variables. Bound variables are represented using de Bruijn indexes.

  44. class Internal2InputAbsy extends AnyRef
  45. class KBO extends Ordering[ITerm]

    Implementation of the Knuth-Bendix term order

    Implementation of the Knuth-Bendix term order

    The used weights are: IFunction, IConstant => as given by the weight functions IIntLit => 1 IVariable => 1 ITimes, IPlus => 0

    The used basic ordering is: functions > + > * > constants > Variables > literals

  46. abstract class Parser2InputAbsy[CT, VT, PT, FT, ST, StackState] extends AnyRef
  47. class PartExtractor extends ContextAwareVisitor[Boolean, Boolean]

    Class to turn an IFormula into a list of IFormula, the disjuncts of the given formula.

    Class to turn an IFormula into a list of IFormula, the disjuncts of the given formula. The boolean result returned by the visitor tells whether the current (sub)formula has been added to the parts map.

  48. class PartName extends AnyRef

    Formula label, used to give names to different partitions used for interpolation.

  49. class Postprocessing extends AnyRef

    Postprocess a formula output by the prover, for instance a model or the result of interpolation or quantifier elimination.

  50. class PredPartNameEliminator extends CollectingVisitor[Unit, IExpression]

    Visitor that eliminates occurrences of the INamedPart operator from a formula.

    Visitor that eliminates occurrences of the INamedPart operator from a formula. All parts with a name accepted by toElim will be stripped of their name.

  51. class PrettyScalaLineariser extends AnyRef

    Class for printing IExpressions in pretty Scala syntax

  52. class QuantifierCollectingVisitor extends ContextAwareVisitor[Unit, Unit]

    Visitor for collecting all quantifiers in a formula.

    Visitor for collecting all quantifiers in a formula. The visitor will not consider quantifiers expressing divisibility constraints.

  53. class QuantifierCountVisitor extends CollectingVisitor[Unit, Unit]

    Count the number of quantifiers in a formula

  54. trait SMTLinearisableTheory extends Theory

    Trait for theories with symbols that can be linearised through the SMT-LIB front-end.

  55. class SMTLineariser extends AnyRef

    Class for printing IFormulas in the SMT-Lib format

  56. trait SMTParseableTheory extends AnyRef

    Trait for theories that can be parsed through the SMT-LIB front-end.

    Trait for theories that can be parsed through the SMT-LIB front-end. For analysing ASTs, the extractors in SMTParsingUtils can be used. The trait does not extend Theory, so that dependencies between theories, the parsing library, and the AST classes can be avoided.

  57. class SMTParser2InputAbsy extends Parser2InputAbsy[SMTType, VariableType, SMTFunctionType, SMTFunctionType, SMTType, (Map[IFunction, (IExpression, SMTType)], AnyRef, Int, Map[PartName, Int])]
  58. class SelectiveQuantifierCountVisitor extends ContextAwareVisitor[Unit, Unit]

    Count the number of quantifiers in a formula

  59. class SimpleClausifier extends AnyRef
  60. class Simplifier extends AnyRef

    Class to simplify input formulas using various rewritings.

    Class to simplify input formulas using various rewritings. Argument splittingLimit controls whether the formula is also (naively) turned into DNF.

  61. class StdFunctionPreproc extends FunctionPreproc

    Introduction of triggers according to the chosen -triggerStrategy.

  62. class SymbolCollector extends CollectingVisitor[Int, Unit]

    Class for collecting the variables, constants, or nullary predicates occurring in an expression.

  63. class TPTPLineariser extends AnyRef

    Class for printing IFormulas in the TPTP format

  64. class TPTPTParser extends Parser2InputAbsy[Type, Type, Rank, Rank, Type, Unit] with JavaTokenParsers with PackratParsers

    A parser for TPTP, both FOF and TFF

  65. class Transform2Prenex extends ContextAwareVisitor[List[IVariable], IExpression]

    Turn a formula into prenex form.

  66. class TriggerGenerator extends ContextAwareVisitor[Int, IExpression]

    Class to automatically generate triggers for quantified formulae, using heuristics similar to Simplify.

    Class to automatically generate triggers for quantified formulae, using heuristics similar to Simplify. The parameter consideredFunctions determines which functions are allowed in triggers. The argument of the visitor determines how many existential quantifiers are immediately above the current position

  67. class UniformSubstVisitor extends CollectingVisitor[Unit, IExpression]

    Uniform substitution of predicates: replace all occurrences of predicates with a formula; the replacement of an n-ary predicate can contain free variables _0, _1, ..., _(n-1) which are replaced with the predicate arguments.

  68. class VariableShiftVisitor extends CollectingVisitor[Int, IExpression]

    Visitor to shift all variables with index >= offset by shift.

Value Members

  1. object ApParser2InputAbsy
  2. object BooleanCompactifier

    Transformation for pulling out common disjuncts/conjuncts from conjunctions/disjunctions.

  3. object CSIsatLineariser

    Class for printing IFormulas in the CSIsat format

    Class for printing IFormulas in the CSIsat format

    Currently, functions are not handled in this class

  4. object CollectingVisitor
  5. object ConstantSubstVisitor extends CollectingVisitor[(Map[ConstantTerm, ITerm], Int), IExpression]

    Substitute some of the constants in an expression with arbitrary terms

  6. object ContainsPredicate

    Check whether the given expression contains some predicate.

  7. object ContainsSymbol extends ContextAwareVisitor[(IExpression) => Boolean, Unit]

    Check whether an expression contains some IVariable, IConstant, IAtom, or IFunApp.

  8. object ContainsVariable

    Check whether an expression contains the variable with index index.

  9. object Context extends Serializable
  10. object DNFConverter

    Functions for converting formulas to DNF.

  11. object Environment
  12. object EquivExpander extends ContextAwareVisitor[Unit, IExpression]

    Class to turn <-> into conjunction and disjunctions, eliminate if-then-else expressions and epsilon terms, and move universal quantifiers outwards (to make later Skolemisation more efficient; currently disabled)

  13. object EquivInliner

    Class to inline equivalences of the form p <-> f, for some Boolean variable p.

  14. object ExMaxiscoper

    Simple class for pulling out EX quantifiers from a formula.

  15. object ExpressionReplacingVisitor extends CollectingVisitor[(IExpression, IExpression), IExpression]

    Visitor to replace occurrences of one expression with another expression.

  16. object FunctionCollector

    Class for collecting the functions occurring in an expression.

  17. object FunctionEncoder
  18. object FunctionPreproc
  19. object IBinJunctor extends Enumeration

    Binary Boolean connectives.

  20. object IEpsilon

    Epsilon term, which is defined to evaluate to an arbitrary value satisfying the formula cond.

    Epsilon term, which is defined to evaluate to an arbitrary value satisfying the formula cond. cond is expected to contain a bound variable with de Bruijn index 0 and any sort.

  21. object IExpression

    Companion object of IExpression, with various helper methods.

  22. object IIntRelation extends Enumeration

    Integer relation operators.

  23. object IQuantified

    Application of a quantifier to a formula containing a free variable with de Bruijn index 0 and any sort.

  24. object ITrigger extends Serializable
  25. object IVarShift
  26. object IVariable

    Bound variables of any sort.

  27. object ImplicationCompressor

    Class to compress chains of implications, for faster constraint propagation

  28. object InputAbsy2Internal
  29. object Internal2InputAbsy

    Converter from the internal formula datastructures to the input level AST datastructures.

  30. object IsUniversalFormulaVisitor extends ContextAwareVisitor[Unit, Unit]

    Visitor for checking whether a formula contains any existential quantifiers without explicitly specified triggers.

    Visitor for checking whether a formula contains any existential quantifiers without explicitly specified triggers.

    TODO: this does not capture all cases, and has quadratic complexity, should be revised.

  31. object LineariseVisitor

    Turn a formula f1 ∗ f2 ∗ ... ∗ fn (where ∗ is some binary operator) into List(f1, f2, ..., fn)

  32. object Parser2InputAbsy
  33. object PartExtractor
  34. object PartName
  35. object PartNameEliminator extends PredPartNameEliminator

    Visitor that eliminates all occurrences of the INamedPart operator from a formula.

  36. object PartialEvaluator extends CollectingVisitor[Unit, IExpression]

    Evaluate all (literally) constant expressions.

  37. object PredicateSubstVisitor extends CollectingVisitor[(Map[Predicate, IFormula], Int), IExpression]

    Substitute some predicates in an expression with arbitrary formulae

  38. object Preprocessing

    Preprocess an InputAbsy formula in order to make it suitable for proving.

    Preprocess an InputAbsy formula in order to make it suitable for proving. The result is a list of formulae, because the original formula may contain named parts (INamedPart).

  39. object PrettyScalaLineariser
  40. object PrincessLineariser

    Class for printing IFormulas in the Princess format

  41. object QuantifierCollectingVisitor
  42. object QuantifierCountVisitor
  43. object Rewriter

    Simple rewriting engine on the input AST datastructures

  44. object SMTLineariser

    Class for printing IFormulas in the SMT-LIB 2 format

  45. object SMTParser2InputAbsy
  46. object SMTParsingUtils
  47. object SMTTypes

    Representation of SMT-LIB types.

    Representation of SMT-LIB types. Those are essentially just wrappers around the corresponding sorts.

  48. object SimpleClausifier
  49. object SimpleMiniscoper

    Simple class for pushing down blocks of EX quantifiers; turn EX x.

    Simple class for pushing down blocks of EX quantifiers; turn EX x. (phi | psi) into (EX x. phi) | (EX x. psi)

  50. object SimplifyingConstantSubstVisitor extends CollectingVisitor[(Map[ConstantTerm, ITerm], Int), IExpression]

    Substitute some of the constants in an expression with arbitrary terms, and immediately simplify the resulting expression if possible.

  51. object SimplifyingVariableSubstVisitor extends AbstractVariableSubstVisitor

    Substitute variables in an expression with arbitrary terms, and immediately simplify the resulting expression if possible.

  52. object SizeVisitor

    Compute the number of operators in an expression.

  53. object SubExprAbbreviator

    Visitor that is able to detect shared sub-expression (i.e., sub-expressions with object identity) and replace them with abbreviations.

  54. object SymbolCollector

    Class for collecting the variables, constants, or nullary predicates occurring in an expression.

  55. object TPTPLineariser

    Class for printing IFormulas in the TPTP format

  56. object TPTPTParser
  57. object Transform2NNF extends CollectingVisitor[Boolean, IExpression]

    Push negations down to the atoms in a formula

  58. object Transform2Prenex
  59. object TriggerGenerator
  60. object UniformSubstVisitor
  61. object VariableIndexCollector extends CollectingVisitor[(Int, (Int) => Unit), Unit]

    Class for collecting the indexes of free variables occurring in an expression.

  62. object VariablePermVisitor extends CollectingVisitor[IVarShift, IExpression]

    More general visitor for renaming variables.

    More general visitor for renaming variables. The argument of the visitor methods is a pair (List[Int], Int) that describes how each variable should be shifted: (List(0, 2, -1), 1) specifies that variable 0 stays the same, variable 1 is increased by 2 (renamed to 3), variable 2 is renamed to 1, and all other variables n are renamed to n+1.

  63. object VariableShiftVisitor

    Visitor to shift all variables with index >= offset by shift.

  64. object VariableSortChecker extends CollectingVisitor[String, Set[IVariable]]

    Visitor that checks whether the sorts of variables are consistent with the sort of their binders.

  65. object VariableSortInferenceVisitor extends CollectingVisitor[Sort, IExpression]

    Visitor to replace quantifiers of sort Any with sorted quantifiers, by inferring the sort of the quantified variables.

  66. object VariableSubstVisitor extends AbstractVariableSubstVisitor

    Substitute variables in an expression with arbitrary terms

Ungrouped