Package

ap

parser

Permalink

package parser

Visibility
  1. Public
  2. All

Type Members

  1. abstract class AbstractCompleteFunctionPreproc extends FunctionPreproc

    Permalink

    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]

    Permalink
  3. class ApParser2InputAbsy extends Parser2InputAbsy[Unit, Sort, Unit, Unit, Sort, Unit]

    Permalink
  4. abstract class CollectingVisitor[A, R] extends AnyRef

    Permalink

    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

    Permalink

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

  6. class CompleteFunctionPreproc extends AbstractCompleteFunctionPreproc

    Permalink

    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

    Permalink
  8. abstract class ContextAwareVisitor[A, R] extends CollectingVisitor[Context[A], R]

    Permalink

    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.

    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

    Permalink
  10. class FunctionCollector extends CollectingVisitor[Int, Unit]

    Permalink

    Class for collecting the functions occurring in an expression.

  11. class FunctionEncoder extends Cloneable

    Permalink

    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

    Permalink

    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

    Permalink

    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

    Permalink

    Boolean combination of two formulae.

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

    Permalink

    Boolean literal.

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

    Permalink

    Symbolic constants.

  17. abstract class IEpsilon extends ITerm with IVariableBinder

    Permalink

    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

    Permalink

    Equation between two terms.

  19. abstract class IExpression extends AnyRef

    Permalink

    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

    Permalink

    Abstract class representing formulae in input-syntax.

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

    Permalink

    If-then-else formula.

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

    Permalink

    Application of an uninterpreted function to a list of terms.

  23. class IFunction extends AnyRef

    Permalink

    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

    Permalink

    Integer equation or inequality.

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

    Permalink

    Integer literals.

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

    Permalink

    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

    Permalink

    A labelled formula with name name.

    A labelled formula with name name.

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

    Permalink

    Negation of a formula.

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

    Permalink

    Sum of two terms.

  30. abstract class IQuantified extends IFormula with IVariableBinder

    Permalink

    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

    Permalink

    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

    Permalink

    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

    Permalink

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

  34. abstract class ITerm extends IExpression

    Permalink

    Abstract class representing terms in input-syntax.

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

    Permalink

    If-then-else term.

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

    Permalink

    Product between a term and an integer coefficient.

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

    Permalink

    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

    Permalink
  39. case class IVarShiftList(prefix: List[Int], defaultShift: Int) extends IVarShift with Product with Serializable

    Permalink
  40. case class IVarShiftMap(prefix: List[Int], mapping: Map[Int, Int], defaultShift: Int) extends IVarShift with Product with Serializable

    Permalink
  41. case class IVarShiftMapEmptyPrefix(prefixLength: Int, mapping: Map[Int, Int], defaultShift: Int) extends IVarShift with Product with Serializable

    Permalink

    Special case for a prefix only containing zeroes

  42. abstract class IVariable extends ITerm

    Permalink

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

  43. trait IVariableBinder extends AnyRef

    Permalink

    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

    Permalink
  45. class KBO extends Ordering[ITerm]

    Permalink

    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

    Permalink
  47. class PartExtractor extends ContextAwareVisitor[Boolean, Boolean]

    Permalink

    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

    Permalink

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

  49. class Postprocessing extends AnyRef

    Permalink

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

  50. class PrettyScalaLineariser extends AnyRef

    Permalink

    Class for printing IExpressions in pretty Scala syntax

    Class for printing IExpressions in pretty Scala syntax

  51. class QuantifierCollectingVisitor extends ContextAwareVisitor[Unit, Unit]

    Permalink

    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.

  52. class QuantifierCountVisitor extends CollectingVisitor[Unit, Unit]

    Permalink

    Count the number of quantifiers in a formula

  53. class SMTLineariser extends AnyRef

    Permalink

    Class for printing IFormulas in the SMT-Lib format

    Class for printing IFormulas in the SMT-Lib format

  54. class SMTParser2InputAbsy extends Parser2InputAbsy[SMTType, VariableType, SMTFunctionType, SMTFunctionType, SMTType, (Map[IFunction, (IExpression, SMTType)], Int, Map[PartName, Int])]

    Permalink
  55. class SelectiveQuantifierCountVisitor extends ContextAwareVisitor[Unit, Unit]

    Permalink

    Count the number of quantifiers in a formula

  56. class Simplifier extends AnyRef

    Permalink

    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.

  57. class StdFunctionPreproc extends FunctionPreproc

    Permalink

    Introduction of triggers according to the chosen -triggerStrategy.

    Introduction of triggers according to the chosen -triggerStrategy.

  58. class SymbolCollector extends CollectingVisitor[Int, Unit]

    Permalink

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

  59. class TPTPLineariser extends AnyRef

    Permalink

    Class for printing IFormulas in the TPTP format

    Class for printing IFormulas in the TPTP format

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

    Permalink

    A parser for TPTP, both FOF and TFF

  61. class TestInputAbsyVisitor extends APTestCase

    Permalink
  62. class Transform2Prenex extends ContextAwareVisitor[List[IVariable], IExpression]

    Permalink

    Turn a formula into prenex form.

  63. class TriggerGenerator extends ContextAwareVisitor[Int, IExpression]

    Permalink

    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

  64. class UniformSubstVisitor extends CollectingVisitor[Unit, IExpression]

    Permalink

    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.

    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.

  65. class VariableShiftVisitor extends CollectingVisitor[Int, IExpression]

    Permalink

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

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

Value Members

  1. object ApParser2InputAbsy

    Permalink
  2. object BooleanCompactifier

    Permalink

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

  3. object CSIsatLineariser

    Permalink

    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

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

    Permalink

    Substitute some of the constants in an expression with arbitrary terms

  6. object ContainsSymbol extends ContextAwareVisitor[(IExpression) ⇒ Boolean, Unit]

    Permalink

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

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

  7. object ContainsVariable

    Permalink

    Check whether an expression contains the variable with index index.

    Check whether an expression contains the variable with index index.

  8. object Context extends Serializable

    Permalink
  9. object DNFConverter

    Permalink

    Functions for converting formulas to DNF.

  10. object Environment

    Permalink
  11. object EquivExpander extends ContextAwareVisitor[Unit, IExpression]

    Permalink

    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)

  12. object ExMaxiscoper

    Permalink

    Simple class for pulling out EX quantifiers from a formula.

  13. object FunctionCollector

    Permalink

    Class for collecting the functions occurring in an expression.

  14. object FunctionEncoder

    Permalink
  15. object FunctionPreproc

    Permalink
  16. object IBinJunctor extends Enumeration

    Permalink

    Binary Boolean connectives.

  17. object IEpsilon

    Permalink

    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.

  18. object IExpression

    Permalink

    Companion object of IExpression, with various helper methods.

    Companion object of IExpression, with various helper methods.

  19. object IIntRelation extends Enumeration

    Permalink

    Integer relation operators.

  20. object IQuantified

    Permalink

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

  21. object ITrigger extends Serializable

    Permalink
  22. object IVarShift

    Permalink
  23. object IVariable

    Permalink

    Bound variables of any sort.

  24. object ImplicationCompressor

    Permalink

    Class to compress chains of implications, for faster constraint propagation

  25. object InputAbsy2Internal

    Permalink
  26. object Internal2InputAbsy

    Permalink

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

  27. object IsUniversalFormulaVisitor extends ContextAwareVisitor[Unit, Unit]

    Permalink

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

  28. object LineariseVisitor

    Permalink

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

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

  29. object Parser2InputAbsy

    Permalink
  30. object PartExtractor

    Permalink
  31. object PartName

    Permalink
  32. object PartNameEliminator extends CollectingVisitor[Unit, IExpression]

    Permalink

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

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

  33. object PartialEvaluator extends CollectingVisitor[Unit, IExpression]

    Permalink

    Evaluate all (literally) constant expressions.

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

    Permalink

    Substitute some predicates in an expression with arbitrary formulae

  35. object Preprocessing

    Permalink

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

  36. object PrettyScalaLineariser

    Permalink
  37. object PrincessLineariser

    Permalink

    Class for printing IFormulas in the Princess format

    Class for printing IFormulas in the Princess format

  38. object QuantifierCollectingVisitor

    Permalink
  39. object QuantifierCountVisitor

    Permalink
  40. object Rewriter

    Permalink

    Simple rewriting engine on the input AST datastructures

  41. object SMTLineariser

    Permalink

    Class for printing IFormulas in the SMT-LIB 2 format

    Class for printing IFormulas in the SMT-LIB 2 format

  42. object SMTParser2InputAbsy

    Permalink
  43. object SimpleClausifier

    Permalink
  44. object SimpleMiniscoper

    Permalink

    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)

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

    Permalink

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

  46. object SimplifyingVariableSubstVisitor extends AbstractVariableSubstVisitor

    Permalink

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

  47. object SizeVisitor

    Permalink

    Compute the number of operators in an expression.

  48. object SubExprAbbreviator

    Permalink

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

  49. object SymbolCollector

    Permalink

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

  50. object TPTPLineariser

    Permalink

    Class for printing IFormulas in the TPTP format

    Class for printing IFormulas in the TPTP format

  51. object TPTPTParser

    Permalink
  52. object Transform2NNF extends CollectingVisitor[Boolean, IExpression]

    Permalink

    Push negations down to the atoms in a formula

  53. object Transform2Prenex

    Permalink
  54. object TriggerGenerator

    Permalink
  55. object UniformSubstVisitor

    Permalink
  56. object VariableIndexCollector extends CollectingVisitor[(Int, (Int) ⇒ Unit), Unit]

    Permalink

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

  57. object VariablePermVisitor extends CollectingVisitor[IVarShift, IExpression]

    Permalink

    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.

  58. object VariableShiftVisitor

    Permalink

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

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

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

    Permalink

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

  60. object VariableSortInferenceVisitor extends CollectingVisitor[Sort, IExpression]

    Permalink

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

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

  61. object VariableSubstVisitor extends AbstractVariableSubstVisitor

    Permalink

    Substitute variables in an expression with arbitrary terms

Ungrouped