Value Members

1.  final def !=(arg0: Any): Boolean

   Definition Classes

   AnyRef → Any

2.  final def ##(): Int

   Definition Classes

   AnyRef → Any

3.  final def ==(arg0: Any): Boolean

   Definition Classes

   AnyRef → Any

4.  def argsOf(fn: Function, fml: Formula): Set[Term]

   Returns a set of variables that are arguments to any application of function 'fn' in the formula fml.

5.  def argumentList(term: Term): List[Term]

   Convert nested pairs to a list of its deassociated non-pair arguments.

   Convert nested pairs to a list of its deassociated non-pair arguments.

   Pair->List[Term]

6.  final def asInstanceOf[T0]: T0

   Definition Classes

   Any

7.  def atomicFormulas(formula: Formula): List[AtomicFormula]

   Read off all atomic subformulas of formula.

   Read off all atomic subformulas of formula. Will not descend into programs to find even further atomic formulas since they are not directly subformulas.

   See also

   negationNormalForm()

8.  def clone(): AnyRef

   Attributes

   protected[java.lang]

   Definition Classes

   AnyRef

   Annotations

   @native() @throws( ... )

9.  def closure(fml: Formula): Formula

   Returns the formula in negation normal form, weakened by replacing strict inequalities with inequalities.

10.  def combinations(l: List[List[Formula]]): List[List[Formula]]

    The element-wise combinations in l, e.g., [ [a,b,c], [p,q] ] ==> [ [a,p], [a,q], [b,p], [b,q], [c,p], [c,q] ].

11.  def conjuncts(formulas: List[Formula]): List[Formula]
    See also

    conjuncts(formula: Formula)

12.  def conjuncts(formula: Formula): List[Formula]

    Split a formula into its conjuncts.

    Split a formula into its conjuncts. Without performing clause form or CNF or DNF transformations.

    Example:

    1. conjuncts(p() & q() & (r() & (s() | t()&u()))) == List(p(), q(), r(), s()|t()&u())

13.  def disjunctiveNormalForm(fml: Formula): Formula

    Turns fml into disjunctive normal form.

14.  def disjuncts(formulas: List[Formula]): List[Formula]
    See also

    disjuncts(formula: Formula)

15.  def disjuncts(formula: Formula): List[Formula]

    Split a formula into its disjuncts.

    Split a formula into its disjuncts. Without performing clause form or CNF or DNF transformations.

    Example:

    1. disjuncts(p() | q() | (r() | (s() & (t()|u())))) == List(p(), q(), r(), s()&(t()|u()))

16.  def distributeOrOverAnd(fml: Formula): Formula

    Distributes disjunctions over conjunctions, e.g., a&(b|c) ==> a&b | a&c.

17.  def dualFree(sequent: Sequent): Boolean

    Check whether sequent is dual-free.

18.  def dualFree(fml: Formula): Boolean

    Check whether fml is dual-free.

19.  def dualFree(program: Program): Boolean

    Check whether given program is dual-free, so a hybrid system and not a proper hybrid game.

    Check whether given program is dual-free, so a hybrid system and not a proper hybrid game.

    See also

    SubstitutionPair.dualFree

20.  final def eq(arg0: AnyRef): Boolean

    Definition Classes

    AnyRef

21.  def equals(arg0: Any): Boolean

    Definition Classes

    AnyRef → Any

22.  def finalize(): Unit

    Attributes

    protected[java.lang]

    Definition Classes

    AnyRef

    Annotations

    @throws( classOf[java.lang.Throwable] )

23.  final def getClass(): Class[_]

    Definition Classes

    AnyRef → Any

    Annotations

    @native()

24.  def hashCode(): Int

    Definition Classes

    AnyRef → Any

    Annotations

    @native()

25.  def interior(fml: Formula): Formula

    Returns the formula in negation normal form, strengthened by replacing inequalities with strict inequalities.

26.  final def isInstanceOf[T0]: Boolean

    Definition Classes

    Any

27.  def kernel(formula: Formula): Formula

    Gets the (unquantified) kernel part of a quantified formula by peeling off quantifiers.

    Gets the (unquantified) kernel part of a quantified formula by peeling off quantifiers.

    Annotations

    @tailrec()

28.  def leftConjuncts(formula: Formula, length: Int = -1): List[Formula]

    Split a formula into length left-hand side conjuncts (-1 for exhaustive splitting), keep right-hand side conjunctions (inverse reduce).

29.  def literalDualFree(sequent: Sequent): Boolean

    Check whether sequent contains literal Dual.

30.  def literalDualFree(fml: Formula): Boolean

    Check whether fml contains literal Dual.

31.  def literalDualFree(program: Program): Boolean

    Check whether given program contains literal Dual.

32.  lazy val logger: Logger

    Attributes

    protected

    Definition Classes

    LazyLogging → LoggerHolder

33.  final val loggerName: String

    Attributes

    protected

    Definition Classes

    LoggerHolder

34.  def makePolarityAt(formula: Formula, pos: PosInExpr, polarity: Int): Formula

    Returns a formula with equivalences turned into implications such that the polarity of the subformula at position pos has the specified polarity.

    Returns a formula with equivalences turned into implications such that the polarity of the subformula at position pos has the specified polarity. Creates a variation of this formula which has equivalences reoriented such that the polarity of the subformula at position pos in the resulting formula will be the desired polarity.

    formula

    The formula.

    pos

    The position within formula for which the polarity is supposed to be changed to the desired polarity.

    polarity

    The desired polarity, must be either 1 (positive polarity) or -1 (negative polarity).

    returns

    The formula with equivalences turned into implications.

35.  final def ne(arg0: AnyRef): Boolean

    Definition Classes

    AnyRef

36.  def negationNormalForm(formula: Formula): Formula

    Negation-normal form transforms such that there are no nested negations and that negated atomic comparisons.

    Negation-normal form transforms such that there are no nested negations and that negated atomic comparisons. Also removes implications/equivalences.

37.  final def notify(): Unit

    Definition Classes

    AnyRef

    Annotations

    @native()

38.  final def notifyAll(): Unit

    Definition Classes

    AnyRef

    Annotations

    @native()

39.  def parentFormulaPos(pos: PosInExpr, fml: Formula): PosInExpr

    Finds the closest parent to pos in formula that is a formula.

40.  def polarityAt(formula: Formula, pos: PosInExpr): Int

    Returns the polarity of the subformula at position pos in formula.

    Returns the polarity of the subformula at position pos in formula.

    formula

    The formula.

    pos

    The position within formula for which the polarity is searched.

    returns

    -1 for negative polarity, 1 for positive polarity, 0 for unknown polarity.

41.  def posOf(formula: Formula, cond: (Expression) ⇒ Boolean): List[PosInExpr]

    Collects the subpositions of formula that satisfy condition cond.

    Collects the subpositions of formula that satisfy condition cond. Ordered: reverse depth (deepest first).

42.  def posOf(expr: Expression, sub: Expression): Option[PosInExpr]

    Returns the first (i.e., left-most) position of sub within expr, if any.

    Returns the first (i.e., left-most) position of sub within expr, if any.

    expr

    The expression to search for containment of sub.

    sub

    The sub-expression.

    returns

    The first position, or None if sub is not contained in expr.

43.  def posOfTerm(term: Term, cond: (Term) ⇒ Boolean): List[PosInExpr]
44.  def quantifyExists(xs: List[Variable], fml: Formula): Formula

    prepends all-quantifiers over given variables to a formula

45.  def quantifyForall(xs: List[Variable], fml: Formula): Formula

    prepends all-quantifiers over given variables to a formula

46.  def reassociate(fml: Formula): Formula

    Reassociates conjunctions and disjunctions into their default right-associative case.

47.  def singularities(program: Program): Set[Term]
48.  def singularities(formula: Formula): Set[Term]
49.  def singularities(term: Term): Set[Term]
50.  def singularities(e: Expression): Set[Term]

    Read off the set of all possible singularities coming from divisors or negative powers.

    Read off the set of all possible singularities coming from divisors or negative powers.

    Example:

    1. singularities("x>5/b+2".asFormula)==Set(b)
       singularities("x/y>z/2+8/(a+b) & [x:=a/c;]x+1/(3*d)>5/3".asFormula)==Set(y,a+b,c,3*d)

51.  def sortsList(s: Sort): List[Sort]

    Convert nested Tuple sorts to a list of its deassociated non-tuple arguments.

    Convert nested Tuple sorts to a list of its deassociated non-tuple arguments.

    Tuple->List[Sort]

52.  def symbolsDiff(fs: Seq[Formula], gs: Seq[Formula]): (Set[NamedSymbol], Set[NamedSymbol], Set[NamedSymbol])

    Union of pairwise symbol difference in fs and gs, returns a tuple of: symbols of fs not in gs, symbols of gs not in fs, their union

53.  def symbolsDiff(f: Formula, g: Formula): (Set[NamedSymbol], Set[NamedSymbol], Set[NamedSymbol])

    Difference between symbols in f and g, returns a tuple of: symbols of f not in g, symbols of g not in f, their union

54.  final def synchronized[T0](arg0: ⇒ T0): T0

    Definition Classes

    AnyRef

55.  def toString(): String

    Definition Classes

    AnyRef → Any

56.  def unnaturalPowers(f: Formula): List[(Term, PosInExpr)]

    Returns all terms

    Returns all terms

    b^e

    such that e is not a natural number occurring in given formula . b^e }}}

    Note

    This is soundness-critical.

57.  final def wait(): Unit

    Definition Classes

    AnyRef

    Annotations

    @throws( ... )

58.  final def wait(arg0: Long, arg1: Int): Unit

    Definition Classes

    AnyRef

    Annotations

    @throws( ... )

59.  final def wait(arg0: Long): Unit

    Definition Classes

    AnyRef

    Annotations

    @native() @throws( ... )