Package

ap

parser

Permalink

package parser

Visibility
  1. Public
  2. All

Type Members

  1. class ApParser2InputAbsy extends Parser2InputAbsy[Unit, Sort, Unit, Unit, Sort, Unit]

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

  3. case class Context[A](binders: List[Binder], polarity: Int, a: A) extends Product with Serializable

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

    Permalink
  5. class Environment[ConstantType, VariableType, PredicateType, FunctionType, SortType] extends Cloneable

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

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

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

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

    Permalink

    Boolean combination of two formulae.

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

    Permalink

    Boolean literal.

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

    Permalink

    Symbolic constants.

  12. case class IEpsilon(cond: IFormula) extends ITerm 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.

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

  14. abstract class IFormula extends IExpression

    Permalink

    Abstract class representing formulae in input-syntax.

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

    Permalink

    If-then-else formula.

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

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

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

    Permalink

    Equation or inequality.

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

    Permalink

    Integer literals.

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

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

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

    Permalink

    Negation of a formula.

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

    Permalink

    Sum of two terms.

  24. case class IQuantified(quan: Quantifier, subformula: IFormula) extends IFormula with Product with Serializable

    Permalink

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

  25. abstract class ITerm extends IExpression

    Permalink

    Abstract class representing terms in input-syntax.

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

    Permalink

    If-then-else term.

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

    Permalink

    Product between a term and an integer coefficient.

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

  29. abstract class IVarShift extends AnyRef

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

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

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

  33. case class IVariable(index: Int) extends ITerm with Product with Serializable

    Permalink

    Bound variables, represented using their de Bruijn index.

  34. class Internal2InputAbsy extends AnyRef

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

  36. abstract class Parser2InputAbsy[CT, VT, PT, FT, ST, StackState] extends AnyRef

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

  38. class PartName extends AnyRef

    Permalink

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

  39. class PrettyScalaLineariser extends AnyRef

    Permalink

    Class for printing IExpressions in pretty Scala syntax

    Class for printing IExpressions in pretty Scala syntax

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

  41. class QuantifierCountVisitor extends CollectingVisitor[Unit, Unit]

    Permalink

    Count the number of quantifiers in a formula

  42. class SMTLineariser extends AnyRef

    Permalink

    Class for printing IFormulas in the SMT-Lib format

    Class for printing IFormulas in the SMT-Lib format

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

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

    Permalink

    Count the number of quantifiers in a formula

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

  46. class SymbolCollector extends CollectingVisitor[Int, Unit]

    Permalink
  47. class TPTPLineariser extends AnyRef

    Permalink

    Class for printing IFormulas in the TPTP format

    Class for printing IFormulas in the TPTP format

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

    Permalink

    A parser for TPTP, both FOF and TFF

  49. class TestInputAbsyVisitor extends APTestCase

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

    Permalink

    Turn a formula into prenex form.

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

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

  53. class VariableShiftVisitor extends CollectingVisitor[Int, IExpression]

    Permalink

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 Context extends Serializable

    Permalink
  8. object DNFConverter

    Permalink

    Functions for converting formulas to DNF.

  9. object Environment

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

  11. object ExMaxiscoper

    Permalink

    Simple class for pulling out EX quantifiers from a formula.

  12. object FunctionCollector

    Permalink
  13. object FunctionEncoder

    Permalink
  14. object IBinJunctor extends Enumeration

    Permalink

    Binary Boolean connectives.

  15. object IExpression

    Permalink
  16. object IIntRelation extends Enumeration

    Permalink

    Integer relation operators.

  17. object ITrigger extends Serializable

    Permalink
  18. object IVarShift

    Permalink
  19. object ImplicationCompressor

    Permalink

    Class to compress chains of implications, for faster constraint propagation

  20. object InputAbsy2Internal

    Permalink
  21. object Internal2InputAbsy

    Permalink

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

  22. object IsUniversalFormulaVisitor extends ContextAwareVisitor[Unit, Unit]

    Permalink

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

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

  24. object Parser2InputAbsy

    Permalink
  25. object PartExtractor

    Permalink
  26. object PartName

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

  28. object PartialEvaluator extends CollectingVisitor[Unit, IExpression]

    Permalink

    Evaluate all (literally) constant expressions.

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

    Permalink

    Substitute some predicates in an expression with arbitrary formulae

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

  31. object PrettyScalaLineariser

    Permalink
  32. object PrincessLineariser

    Permalink

    Class for printing IFormulas in the Princess format

    Class for printing IFormulas in the Princess format

  33. object QuantifierCollectingVisitor

    Permalink
  34. object QuantifierCountVisitor

    Permalink
  35. object Rewriter

    Permalink

    Simple rewriting engine on the input AST datastructures

  36. object SMTLineariser

    Permalink

    Class for printing IFormulas in the SMT-LIB 2 format

    Class for printing IFormulas in the SMT-LIB 2 format

  37. object SMTParser2InputAbsy

    Permalink
  38. object SimpleClausifier

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

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

  41. object SimplifyingVariableSubstVisitor extends CollectingVisitor[(List[ITerm], Int), IExpression]

    Permalink

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

  42. object SizeVisitor

    Permalink

    Compute the number of operators in an expression.

  43. object SubExprAbbreviator

    Permalink

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

  44. object SymbolCollector

    Permalink
  45. object TPTPLineariser

    Permalink

    Class for printing IFormulas in the TPTP format

    Class for printing IFormulas in the TPTP format

  46. object TPTPTParser

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

    Permalink

    Push negations down to the atoms in a formula

  48. object Transform2Prenex

    Permalink
  49. object TriggerGenerator

    Permalink
  50. object UniformSubstVisitor

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

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

  53. object VariableShiftVisitor

    Permalink
  54. object VariableSubstVisitor extends CollectingVisitor[(List[ITerm], Int), IExpression]

    Permalink

    Substitute variables in an expression with arbitrary terms

Ungrouped