parser

Type Members

abstract class AbstractCompleteFunctionPreproc extends FunctionPreproc

Introduction of triggers using the complete strategy that avoids the need for totality axioms (as in Kanger's calculus).
abstract class AbstractVariableSubstVisitor extends CollectingVisitor[(List[ITerm], Int), IExpression]
class ApParser2InputAbsy extends Parser2InputAbsy[Unit, Sort, Unit, Unit, Sort, Unit]
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
class CompleteFrugalFunctionPreproc extends AbstractCompleteFunctionPreproc

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

Introduction of triggers using the complete strategy that avoids the need for totality axioms (as in Kanger's calculus).
case class Context[A](binders: List[Binder], boundSorts: List[Sort], polarity: Int, a: A) extends Product with Serializable
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.
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.
class Environment[ConstantType, VariableType, PredicateType, FunctionType, SortType] extends Cloneable
class FunctionCollector extends CollectingVisitor[Int, Unit]

Class for collecting the functions occurring in an expression.
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.
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.
case class IAtom(pred: Predicate, args: Seq[ITerm]) extends IFormula with Product with Serializable

Application of an uninterpreted predicate to a list of terms.
case class IBinFormula(j: IBinJunctor.Value, f1: IFormula, f2: IFormula) extends IFormula with Product with Serializable

Boolean combination of two formulae.
case class IBoolLit(value: Boolean) extends IFormula with Product with Serializable

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

Symbolic constants.
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.
case class IEquation(left: ITerm, right: ITerm) extends IFormula with Product with Serializable

Equation between two terms.
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.
abstract class IFormula extends IExpression

Abstract class representing formulae in input-syntax.
case class IFormulaITE(cond: IFormula, left: IFormula, right: IFormula) extends IFormula with Product with Serializable

If-then-else formula.
case class IFunApp(fun: IFunction, args: Seq[ITerm]) extends ITerm with Product with Serializable

Application of an uninterpreted function to a list of terms.
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).
case class IIntFormula(rel: IIntRelation.Value, t: ITerm) extends IFormula with Product with Serializable

Integer equation or inequality.
case class IIntLit(value: IdealInt) extends ITerm with Product with Serializable

Integer literals.
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.
case class INamedPart(name: PartName, subformula: IFormula) extends IFormula with Product with Serializable

A labelled formula with name name.
A labelled formula with name name.
case class INot(subformula: IFormula) extends IFormula with Product with Serializable

Negation of a formula.
case class IPlus(t1: ITerm, t2: ITerm) extends ITerm with Product with Serializable

Sum of two terms.
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.
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.
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.
case class ISortedVariable(index: Int, sort: Sort) extends IVariable with Product with Serializable

Bound variables, represented using their de Bruijn index and the sort.
abstract class ITerm extends IExpression

Abstract class representing terms in input-syntax.
case class ITermITE(cond: IFormula, left: ITerm, right: ITerm) extends ITerm with Product with Serializable

If-then-else term.
case class ITimes(coeff: IdealInt, subterm: ITerm) extends ITerm with Product with Serializable

Product between a term and an integer coefficient.
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.
abstract class IVarShift extends AnyRef
case class IVarShiftList(prefix: List[Int], defaultShift: Int) extends IVarShift with Product with Serializable
case class IVarShiftMap(prefix: List[Int], mapping: Map[Int, Int], defaultShift: Int) extends IVarShift with Product with Serializable
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
abstract class IVariable extends ITerm

Bound variables, represented using their de Bruijn index and the sort.
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.
class Internal2InputAbsy extends AnyRef
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
abstract class Parser2InputAbsy[CT, VT, PT, FT, ST, StackState] extends AnyRef
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.
class PartName extends AnyRef

Formula label, used to give names to different partitions used for interpolation.
class Postprocessing extends AnyRef

Postprocess a formula output by the prover, for instance a model or the result of interpolation or quantifier elimination.
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.
class PrettyScalaLineariser extends AnyRef

Class for printing IExpressions in pretty Scala syntax
Class for printing IExpressions in pretty Scala syntax
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.
class QuantifierCountVisitor extends CollectingVisitor[Unit, Unit]

Count the number of quantifiers in a formula
trait SMTLinearisableTheory extends Theory

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

Class for printing IFormulas in the SMT-Lib format
Class for printing IFormulas in the SMT-Lib format
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.
class SMTParser2InputAbsy extends Parser2InputAbsy[SMTType, VariableType, SMTFunctionType, SMTFunctionType, SMTType, (Map[IFunction, (IExpression, SMTType)], AnyRef, Int, Map[PartName, Int])]
class SelectiveQuantifierCountVisitor extends ContextAwareVisitor[Unit, Unit]

Count the number of quantifiers in a formula
class SimpleClausifier extends AnyRef
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.
class StdFunctionPreproc extends FunctionPreproc

Introduction of triggers according to the chosen -triggerStrategy.
Introduction of triggers according to the chosen -triggerStrategy.
class SymbolCollector extends CollectingVisitor[Int, Unit]

Class for collecting the variables, constants, or nullary predicates occurring in an expression.
class TPTPLineariser extends AnyRef

Class for printing IFormulas in the TPTP format
Class for printing IFormulas in the TPTP format
class TPTPTParser extends Parser2InputAbsy[Type, Type, Rank, Rank, Type, Unit] with JavaTokenParsers with PackratParsers

A parser for TPTP, both FOF and TFF
class Transform2Prenex extends ContextAwareVisitor[List[IVariable], IExpression]

Turn a formula into prenex form.
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
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.
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.
class VariableShiftVisitor extends CollectingVisitor[Int, IExpression]

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

Value Members

object ApParser2InputAbsy
object BooleanCompactifier

Transformation for pulling out common disjuncts/conjuncts from conjunctions/disjunctions.
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
object CollectingVisitor
object ConstantSubstVisitor extends CollectingVisitor[(Map[ConstantTerm, ITerm], Int), IExpression]

Substitute some of the constants in an expression with arbitrary terms
object ContainsPredicate

Check whether the given expression contains some predicate.
object ContainsSymbol extends ContextAwareVisitor[(IExpression) ⇒ Boolean, Unit]

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

Check whether an expression contains the variable with index index.
Check whether an expression contains the variable with index index.
object Context extends Serializable
object DNFConverter

Functions for converting formulas to DNF.
object Environment
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)
object EquivInliner

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

Simple class for pulling out EX quantifiers from a formula.
object ExpressionReplacingVisitor extends CollectingVisitor[(IExpression, IExpression), IExpression]

Visitor to replace occurrences of one expression with another expression.
object FunctionCollector

Class for collecting the functions occurring in an expression.
object FunctionEncoder
object FunctionPreproc
object IBinJunctor extends Enumeration

Binary Boolean connectives.
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.
object IExpression

Companion object of IExpression, with various helper methods.
Companion object of IExpression, with various helper methods.
object IIntRelation extends Enumeration

Integer relation operators.
object IQuantified

Application of a quantifier to a formula containing a free variable with de Bruijn index 0 and any sort.
object ITrigger extends Serializable
object IVarShift
object IVariable

Bound variables of any sort.
object ImplicationCompressor

Class to compress chains of implications, for faster constraint propagation
object InputAbsy2Internal
object Internal2InputAbsy

Converter from the internal formula datastructures to the input level AST datastructures.
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.
object LineariseVisitor

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)
object Parser2InputAbsy
object PartExtractor
object PartName
object PartNameEliminator extends PredPartNameEliminator

Visitor that eliminates all occurrences of the INamedPart operator from a formula.
Visitor that eliminates all occurrences of the INamedPart operator from a formula.
object PartialEvaluator extends CollectingVisitor[Unit, IExpression]

Evaluate all (literally) constant expressions.
object PredicateSubstVisitor extends CollectingVisitor[(Map[Predicate, IFormula], Int), IExpression]

Substitute some predicates in an expression with arbitrary formulae
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).
object PrettyScalaLineariser
object PrincessLineariser

Class for printing IFormulas in the Princess format
Class for printing IFormulas in the Princess format
object QuantifierCollectingVisitor
object QuantifierCountVisitor
object Rewriter

Simple rewriting engine on the input AST datastructures
object SMTLineariser

Class for printing IFormulas in the SMT-LIB 2 format
Class for printing IFormulas in the SMT-LIB 2 format
object SMTParser2InputAbsy
object SMTParsingUtils
object SMTTypes

Representation of SMT-LIB types.
Representation of SMT-LIB types. Those are essentially just wrappers around the corresponding sorts.
object SimpleClausifier
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)
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.
object SimplifyingVariableSubstVisitor extends AbstractVariableSubstVisitor

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

Compute the number of operators in an expression.
object SubExprAbbreviator

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

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

Class for printing IFormulas in the TPTP format
Class for printing IFormulas in the TPTP format
object TPTPTParser
object Transform2NNF extends CollectingVisitor[Boolean, IExpression]

Push negations down to the atoms in a formula
object Transform2Prenex
object TriggerGenerator
object UniformSubstVisitor
object VariableIndexCollector extends CollectingVisitor[(Int, (Int) ⇒ Unit), Unit]

Class for collecting the indexes of free variables occurring in an expression.
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.
object VariableShiftVisitor

Visitor to shift all variables with index >= offset by shift.
Visitor to shift all variables with index >= offset by shift.
object VariableSortChecker extends CollectingVisitor[String, Set[IVariable]]

Visitor that checks whether the sorts of variables are consistent with the sort of their binders.
object VariableSortInferenceVisitor extends CollectingVisitor[Sort, IExpression]

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

Substitute variables in an expression with arbitrary terms

package parser

Type Members

abstract class AbstractCompleteFunctionPreproc extends FunctionPreproc

abstract class AbstractVariableSubstVisitor extends CollectingVisitor[(List[ITerm], Int), IExpression]

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

abstract class CollectingVisitor[A, R] extends AnyRef

class CompleteFrugalFunctionPreproc extends AbstractCompleteFunctionPreproc

class CompleteFunctionPreproc extends AbstractCompleteFunctionPreproc

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

abstract class ContextAwareVisitor[A, R] extends CollectingVisitor[Context[A], R]

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

class FunctionCollector extends CollectingVisitor[Int, Unit]

class FunctionEncoder extends Cloneable

abstract class FunctionPreproc extends AnyRef

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

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

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

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

abstract class IEpsilon extends ITerm with IVariableBinder

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

abstract class IExpression extends AnyRef

abstract class IFormula extends IExpression

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

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

class IFunction extends AnyRef

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

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

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

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

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

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

abstract class IQuantified extends IFormula with IVariableBinder

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

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

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

abstract class ITerm extends IExpression

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

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

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

abstract class IVarShift extends AnyRef

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

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

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

abstract class IVariable extends ITerm

trait IVariableBinder extends AnyRef

class Internal2InputAbsy extends AnyRef

class KBO extends Ordering[ITerm]

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

class PartExtractor extends ContextAwareVisitor[Boolean, Boolean]

class PartName extends AnyRef

class Postprocessing extends AnyRef

class PredPartNameEliminator extends CollectingVisitor[Unit, IExpression]

class PrettyScalaLineariser extends AnyRef

class QuantifierCollectingVisitor extends ContextAwareVisitor[Unit, Unit]

class QuantifierCountVisitor extends CollectingVisitor[Unit, Unit]

trait SMTLinearisableTheory extends Theory

class SMTLineariser extends AnyRef

trait SMTParseableTheory extends AnyRef

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

class SelectiveQuantifierCountVisitor extends ContextAwareVisitor[Unit, Unit]

class SimpleClausifier extends AnyRef

class Simplifier extends AnyRef

class StdFunctionPreproc extends FunctionPreproc

class SymbolCollector extends CollectingVisitor[Int, Unit]

class TPTPLineariser extends AnyRef

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

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

class TriggerGenerator extends ContextAwareVisitor[Int, IExpression]

class UniformSubstVisitor extends CollectingVisitor[Unit, IExpression]

class VariableShiftVisitor extends CollectingVisitor[Int, IExpression]

Value Members

object ApParser2InputAbsy

object BooleanCompactifier

object CSIsatLineariser

object CollectingVisitor

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

object ContainsPredicate

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

object ContainsVariable