IExpression

Type Members

class BooleanFunApplier extends AnyRef

Class implementing prefix-notation for functions that are considered Boolean-valued.
Class implementing prefix-notation for functions that are considered Boolean-valued. Booleans are encoded into integers, mapping true to 0 and false to 1.
type ConstantTerm = terfor.ConstantTerm

Imported type from the terfor package
Imported type from the terfor package
class FunApplier extends AnyRef

Class implementing prefix-notation for functions
class PredApplier extends AnyRef

Class implementing prefix-notation for predicates
type Predicate = terfor.preds.Predicate

Imported type from the terfor package
Imported type from the terfor package
type Quantifier = terfor.conjunctions.Quantifier

Imported type from the terfor package
Imported type from the terfor package
class RichITerm extends AnyRef
class RichITermSeq extends AnyRef

Various functions to work with vectors of terms
type Sort = types.Sort

Imported type from the types package
Imported type from the types package
case class SymbolEquation(symbol: ITerm) extends Product with Serializable

Rewrite an equation to the form coeff * symbol = remainder (where remainder does not contain the atomic term symbol) and determine the coefficient and the remainder
Rewrite an equation to the form coeff * symbol = remainder (where remainder does not contain the atomic term symbol) and determine the coefficient and the remainder
case class SymbolSum(symbol: ITerm) extends Product with Serializable

Rewrite a term to the form coeff * symbol + remainder (where remainder does not contain the atomic term symbol) and determine the coefficient and the remainder
Rewrite a term to the form coeff * symbol + remainder (where remainder does not contain the atomic term symbol) and determine the coefficient and the remainder

Value Members

final def !=(arg0: Any): Boolean

Definition Classes
AnyRef → Any
final def ##(): Int

Definition Classes
AnyRef → Any
final def ==(arg0: Any): Boolean

Definition Classes
AnyRef → Any
val AC: AC_INPUT_ABSY.type

Attributes
protected[ap.parser]
implicit def Boolean2IFormula(value: Boolean): IFormula

Implicit conversion from Booleans to formulas
object Conj

Generate or match a binary conjunction phi & psi.
Generate or match a binary conjunction phi & psi.
object Const

Extract the value of constant terms.
implicit def ConstantTerm2ITerm(c: ConstantTerm): ITerm

Implicit conversion from constants to terms
object Difference

Match on a difference IPlus(a, ITimes(IdealInt.MINUS_ONE, b)) or IPlus(ITimes(IdealInt.MINUS_ONE, b), a)
Match on a difference IPlus(a, ITimes(IdealInt.MINUS_ONE, b)) or IPlus(ITimes(IdealInt.MINUS_ONE, b), a)
object Disj

Generate or match a binary disjunction phi | psi.
Generate or match a binary disjunction phi | psi.
object Divisibility

Generate or match a divisibility expression ex x.
Generate or match a divisibility expression ex x. denom*x = t.
object Eq

Generate or match an equation s === t.
Generate or match an equation s === t.
object EqLit

Generate or match an equation s === lit, where lit is an integer literal.
Generate or match an equation s === lit, where lit is an integer literal.
object EqZ

Generate or match the equation t = 0.
Generate or match the equation t = 0.
object Geq

Generate or match an inequality s >= t.
Generate or match an inequality s >= t.
object GeqZ

Generate or match the inequality t >= 0.
Generate or match the inequality t >= 0.
implicit def IdealInt2ITerm(value: IdealInt): ITerm

Implicit conversion from integers to terms
implicit def Int2ITerm(value: Int): ITerm

Implicit conversion from integers to terms
object LeafFormula

Identify formulae that do not have direct subformulae.
object NonDivisibility

Generate or match a non-divisibility expression forall x.
Generate or match a non-divisibility expression forall x. denom*x != t.
val Quantifier: terfor.conjunctions.Quantifier.type

Imported companion object from the terfor package
Imported companion object from the terfor package
implicit def Range2Interval(range: Range): Interval

Implicit conversion from Scala ranges to interval sorts
object SignConst

Extract the value and sign of constant terms.
object SimpleTerm

Identify terms that only consist of variables, constants, and linear arithmetic operations.
val Sort: types.Sort.type

Imported companion object from the types package
Imported companion object from the types package
def abs(t: ITerm): ITerm

Absolute value
def all(sorts: Seq[Sort], f: IFormula): IFormula

Add sorted universal quantifiers for the variables with de Bruijn index 0, ..., sorts.size - 1.
Add sorted universal quantifiers for the variables with de Bruijn index 0, ..., sorts.size - 1. The first sort in sorts will be the innermost quantifier and corresponds to index 0.
def all(f: (ITerm, ITerm, ITerm, ITerm, ITerm) ⇒ IFormula): IFormula

Higher-order syntax for universal quantifiers.
Higher-order syntax for universal quantifiers. This makes it possible to write a quantifier as all((a, b, c, d, e) => phi(a, b, c, d, e)).
def all(f: (ITerm, ITerm, ITerm, ITerm) ⇒ IFormula): IFormula

Higher-order syntax for universal quantifiers.
Higher-order syntax for universal quantifiers. This makes it possible to write a quantifier as all((a, b, c, d) => phi(a, b, c, d)).
def all(f: (ITerm, ITerm, ITerm) ⇒ IFormula): IFormula

Higher-order syntax for universal quantifiers.
Higher-order syntax for universal quantifiers. This makes it possible to write a quantifier as all((a, b, c) => phi(a, b, c)).
def all(f: (ITerm, ITerm) ⇒ IFormula): IFormula

Higher-order syntax for universal quantifiers.
Higher-order syntax for universal quantifiers. This makes it possible to write a quantifier as all((a, b) => phi(a, b)).
def all(f: (ITerm) ⇒ IFormula): IFormula

Higher-order syntax for universal quantifiers.
Higher-order syntax for universal quantifiers. This makes it possible to write a quantifier as all(a => phi(a)).
def all(f: IFormula): IQuantified

Add an existential quantifier for the variable with de Bruijn index 0.
def and(fors: Iterable[IFormula]): IFormula

Generate the conjunction of the given formulas.
def and(fors: Iterator[IFormula]): IFormula

Generate the conjunction of the given formulas.
final def asInstanceOf[T0]: T0

Definition Classes
Any
def clone(): AnyRef

Attributes
protected[java.lang]
Definition Classes
AnyRef
Annotations
@HotSpotIntrinsicCandidate() @throws( ... )
def connect(fors: Iterator[IFormula], op: IBinJunctor.Value): IFormula
def connect(fors: Iterable[IFormula], op: IBinJunctor.Value): IFormula
def connectSimplify(fors: Iterator[IFormula], op: IBinJunctor.Value): IFormula
def connectSimplify(fors: Iterable[IFormula], op: IBinJunctor.Value): IFormula
implicit def constantSeq2ITermSeq(lcs: Seq[ConstantTerm]): Seq[ITerm]
implicit def constantSeq2RichITermSeq(lcs: Seq[ConstantTerm]): RichITermSeq
def containFunctionApplications(f: IFormula): IFormula

When encoding functions using predicates, make sure that no functions escape.
def distinct(terms: Iterable[ITerm]): IFormula

Generate a formula expressing that the given terms are pairwise distinct
def distinct(terms: Iterator[ITerm]): IFormula

Generate a formula expressing that the given terms are pairwise distinct
def eps(f: (ITerm) ⇒ IFormula): IEpsilon

Higher-order syntax for epsilon-expressions.
Higher-order syntax for epsilon-expressions. This makes it possible to write things like eps(a => phi(a)).
def eps(sort: Sort, f: IFormula): IEpsilon

Generate an epsilon-expression with the given sort.
def eps(f: IFormula): IEpsilon

Generate an epsilon-expression with sort Sort.Integer.
Generate an epsilon-expression with sort Sort.Integer.
final def eq(arg0: AnyRef): Boolean

Definition Classes
AnyRef
def eqZero(t: ITerm): IFormula

Generate the equation t = 0.
Generate the equation t = 0.
def equals(arg0: Any): Boolean

Definition Classes
AnyRef → Any
def ex(sorts: Seq[Sort], f: IFormula): IFormula

Add sorted existential quantifiers for the variables with de Bruijn index 0, ..., sorts.size - 1.
Add sorted existential quantifiers for the variables with de Bruijn index 0, ..., sorts.size - 1. The first sort in sorts will be the innermost quantifier and corresponds to index 0.
def ex(f: (ITerm, ITerm, ITerm, ITerm, ITerm) ⇒ IFormula): IFormula

Higher-order syntax for existential quantifiers.
Higher-order syntax for existential quantifiers. This makes it possible to write a quantifier as ex((a, b, c, d, e) => phi(a, b, c, d, e)).
def ex(f: (ITerm, ITerm, ITerm, ITerm) ⇒ IFormula): IFormula

Higher-order syntax for existential quantifiers.
Higher-order syntax for existential quantifiers. This makes it possible to write a quantifier as ex((a, b, c, d) => phi(a, b, c, d)).
def ex(f: (ITerm, ITerm, ITerm) ⇒ IFormula): IFormula

Higher-order syntax for existential quantifiers.
Higher-order syntax for existential quantifiers. This makes it possible to write a quantifier as ex((a, b, c) => phi(a, b, c)).
def ex(f: (ITerm, ITerm) ⇒ IFormula): IFormula

Higher-order syntax for existential quantifiers.
Higher-order syntax for existential quantifiers. This makes it possible to write a quantifier as ex((a, b) => phi(a, b)).
def ex(f: (ITerm) ⇒ IFormula): IFormula

Higher-order syntax for existential quantifiers.
Higher-order syntax for existential quantifiers. This makes it possible to write a quantifier as ex(a => phi(a)).
def ex(f: IFormula): IQuantified

Add an existential quantifier for the variable with de Bruijn index 0.
def geqZero(t: ITerm): IFormula

Generate the inequality t >= 0.
Generate the inequality t >= 0.
final def getClass(): Class[_]

Definition Classes
AnyRef → Any
Annotations
@HotSpotIntrinsicCandidate()
def guardAll(f: IFormula, guard: IFormula): IFormula

Guard a formula, turning it into f ==> guard.
Guard a formula, turning it into f ==> guard. The guard will be inserted underneath leading universal quantifiers.
def guardEx(f: IFormula, guard: IFormula): IFormula

Guard a formula, turning it into f & guard.
Guard a formula, turning it into f & guard. The guard will be inserted underneath leading existential quantifiers.
def hashCode(): Int

Definition Classes
AnyRef → Any
Annotations
@HotSpotIntrinsicCandidate()
def i(value: Boolean): IFormula

Conversion from Booleans to formulas
def i(c: ConstantTerm): ITerm

Conversion from constants to terms
def i(value: IdealInt): ITerm

Conversion from integers to terms
def i(value: Int): ITerm

Conversion from integers to terms
final def isInstanceOf[T0]: Boolean

Definition Classes
Any
def isSimpleTerm(t: ITerm): Boolean

Identify terms that only consist of variables, constants, and linear arithmetic operations.
def ite(cond: IFormula, left: IFormula, right: IFormula): IFormulaITE

Generate a conditional formula.
def ite(cond: IFormula, left: ITerm, right: ITerm): ITermITE

Generate a conditional term.
implicit def iterm2RichITerm(lc: ITerm): RichITerm
implicit def itermSeq2RichITermSeq(lcs: Seq[ITerm]): RichITermSeq
def max(terms: Iterable[ITerm]): ITerm

Maximum value of a sequence of terms
def min(terms: Iterable[ITerm]): ITerm

Minimum value of a sequence of terms
final def ne(arg0: AnyRef): Boolean

Definition Classes
AnyRef
final def notify(): Unit

Definition Classes
AnyRef
Annotations
@HotSpotIntrinsicCandidate()
final def notifyAll(): Unit

Definition Classes
AnyRef
Annotations
@HotSpotIntrinsicCandidate()
def or(fors: Iterable[IFormula]): IFormula

Generate the disjunction of the given formulas.
def or(fors: Iterator[IFormula]): IFormula

Generate the disjunction of the given formulas.
def quan(quans: Seq[Quantifier], f: IFormula): IFormula

Add quantifiers for the variables with de Bruijn index 0, ..., quans.size - 1.
Add quantifiers for the variables with de Bruijn index 0, ..., quans.size - 1. The first quantifier in quans will be the innermost quantifier and corresponds to index 0.
def quan(q: Quantifier, f: (ITerm, ITerm, ITerm, ITerm, ITerm) ⇒ IFormula): IFormula

Higher-order syntax for quantifiers.
Higher-order syntax for quantifiers. This makes it possible to write a quantifier like in quan(Quantifier.ALL, (a, b, c, d, e) => phi(a, b, c, d, e)).
def quan(q: Quantifier, f: (ITerm, ITerm, ITerm, ITerm) ⇒ IFormula): IFormula

Higher-order syntax for quantifiers.
Higher-order syntax for quantifiers. This makes it possible to write a quantifier like in quan(Quantifier.ALL, (a, b, c, d) => phi(a, b, c, d)).
def quan(q: Quantifier, f: (ITerm, ITerm, ITerm) ⇒ IFormula): IFormula

Higher-order syntax for quantifiers.
Higher-order syntax for quantifiers. This makes it possible to write a quantifier like in quan(Quantifier.ALL, (a, b, c) => phi(a, b, c)).
def quan(q: Quantifier, f: (ITerm, ITerm) ⇒ IFormula): IFormula

Higher-order syntax for quantifiers.
Higher-order syntax for quantifiers. This makes it possible to write a quantifier like in quan(Quantifier.ALL, (a, b) => phi(a, b)).
def quan(q: Quantifier, f: (ITerm) ⇒ IFormula): IFormula

Higher-order syntax for quantifiers.
Higher-order syntax for quantifiers. This makes it possible to write a quantifier like in quan(Quantifier.ALL, a => phi(a)).
def quanConsts(quantifiedConstants: Seq[(Quantifier, ConstantTerm)], f: IFormula): IFormula

Replace the constants in quantifiedConstants with bound variables, and quantify them.
Replace the constants in quantifiedConstants with bound variables, and quantify them.
def quanConsts(quan: Quantifier, consts: Iterable[ConstantTerm], f: IFormula): IFormula

Replace consts with bound variables, and quantify them.
Replace consts with bound variables, and quantify them.
def quanVars(quan: Quantifier, vars: Iterable[IVariable], f: IFormula): IFormula

Quantify some of the variables occurring in a formula.
def quanWithSorts(quans: Seq[(Quantifier, Sort)], f: IFormula): IFormula

Add quantifiers for the variables with de Bruijn index 0, ..., quans.size - 1.
Add quantifiers for the variables with de Bruijn index 0, ..., quans.size - 1. The first quantifier in quans will be the innermost quantifier and corresponds to index 0.
def quanWithSorts(q: Quantifier, sorts: Seq[Sort], f: IFormula): IFormula

Add quantifiers for the variables with de Bruijn index 0, ..., sorts.size - 1.
Add quantifiers for the variables with de Bruijn index 0, ..., sorts.size - 1. The first sort in sorts will be the innermost quantifier and corresponds to index 0.
def removePartName(t: IFormula): IFormula
def shiftVars(t: ITerm, shift: Int): ITerm

Shift all variables by shift.
Shift all variables by shift.
def shiftVars(t: ITerm, offset: Int, shift: Int): ITerm

Shift all variables with index >= offset by shift.
Shift all variables with index >= offset by shift.
def shiftVars(t: IFormula, shift: Int): IFormula

Shift all variables by shift.
Shift all variables by shift.
def shiftVars(t: IFormula, offset: Int, shift: Int): IFormula

Shift all variables with index >= offset by shift.
Shift all variables with index >= offset by shift.
def shiftVars(t: IExpression, shift: Int): IExpression

Shift all variables by shift.
Shift all variables by shift.
def shiftVars(t: IExpression, offset: Int, shift: Int): IExpression

Shift all variables with index >= offset by shift.
Shift all variables with index >= offset by shift.
def subst(t: IExpression, replacement: List[ITerm], shift: Int): IExpression

Substitute terms for the variables with de Bruijn index 0, ..., replacement.size - 1, and increment all other variables by shift.
Substitute terms for the variables with de Bruijn index 0, ..., replacement.size - 1, and increment all other variables by shift.
def subst(t: IFormula, replacement: List[ITerm], shift: Int): IFormula

Substitute terms for the variables with de Bruijn index 0, ..., replacement.size - 1, and increment all other variables by shift.
Substitute terms for the variables with de Bruijn index 0, ..., replacement.size - 1, and increment all other variables by shift.
def subst(t: ITerm, replacement: List[ITerm], shift: Int): ITerm

Substitute terms for the variables with de Bruijn index 0, ..., replacement.size - 1, and increment all other variables by shift.
Substitute terms for the variables with de Bruijn index 0, ..., replacement.size - 1, and increment all other variables by shift.
def sum(terms: Iterator[ITerm]): ITerm

Generate the sum of the given terms.
def sum(terms: Iterable[ITerm]): ITerm

Generate the sum of the given terms.
final def synchronized[T0](arg0: ⇒ T0): T0

Definition Classes
AnyRef
implicit def toFunApplier(fun: IFunction): FunApplier

Implicit conversion, to enable the application of a function to a sequence of terms, like in f(s, t).
Implicit conversion, to enable the application of a function to a sequence of terms, like in f(s, t).
implicit def toPredApplier(pred: Predicate): PredApplier

Implicit conversion, to enable the application of a predicate to a sequence of terms, like in p(s, t).
Implicit conversion, to enable the application of a predicate to a sequence of terms, like in p(s, t).
def toString(): String

Definition Classes
AnyRef → Any
def toTermSeq(newExprs: Seq[IExpression], oldExprs: Seq[ITerm]): Option[Seq[ITerm]]

Attributes
protected[ap.parser]
def trig(f: IFormula, patterns: IExpression*): ITrigger

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. Intended use is, for instance, all(x => trig(f(x) >= 0, f(x))).
def updateAndSimplify(e: ITerm, newSubExpr: Seq[IExpression]): ITerm

Update sub-expressions, and directly check whether simplifications are possible.
def updateAndSimplify(t: IFormula, newSubExpr: Seq[IExpression]): IFormula

Update sub-expressions, and directly check whether simplifications are possible.
def updateAndSimplify(e: IExpression, newSubExpr: Seq[IExpression]): IExpression

Update sub-expressions, and directly check whether simplifications are possible.
def updateAndSimplifyLazily(e: ITerm, newSubExpr: Seq[IExpression]): ITerm

Update sub-expressions; if the expression changed as a result of the update, check whether simplifications are possible.
def updateAndSimplifyLazily(e: IFormula, newSubExpr: Seq[IExpression]): IFormula

Update sub-expressions; if the expression changed as a result of the update, check whether simplifications are possible.
def updateAndSimplifyLazily(e: IExpression, newSubExpr: Seq[IExpression]): IExpression

Update sub-expressions; if the expression changed as a result of the update, check whether simplifications are possible.
def v(index: Int, sort: Sort): IVariable

Generate the variable with de Bruijn index index and the given sort.
Generate the variable with de Bruijn index index and the given sort.
def v(index: Int): IVariable

Generate the variable with de Bruijn index index and sort Sort.Integer.
Generate the variable with de Bruijn index index and sort Sort.Integer.
final def wait(arg0: Long, arg1: Int): Unit

Definition Classes
AnyRef
Annotations
@throws( ... )
final def wait(arg0: Long): Unit

Definition Classes
AnyRef
Annotations
@throws( ... )
final def wait(): Unit

Definition Classes
AnyRef
Annotations
@throws( ... )

Deprecated Value Members

def finalize(): Unit

Attributes
protected[java.lang]
Definition Classes
AnyRef
Annotations
@Deprecated @deprecated @throws( classOf[java.lang.Throwable] )
Deprecated
(Since version ) see corresponding Javadoc for more information.

Related Docs: class IExpression | package parser

object IExpression

Type Members

class BooleanFunApplier extends AnyRef

type ConstantTerm = terfor.ConstantTerm

class FunApplier extends AnyRef

class PredApplier extends AnyRef

type Predicate = terfor.preds.Predicate

type Quantifier = terfor.conjunctions.Quantifier

class RichITerm extends AnyRef

class RichITermSeq extends AnyRef

type Sort = types.Sort

case class SymbolEquation(symbol: ITerm) extends Product with Serializable

case class SymbolSum(symbol: ITerm) extends Product with Serializable

Value Members

final def !=(arg0: Any): Boolean

final def ##(): Int

final def ==(arg0: Any): Boolean

val AC: AC_INPUT_ABSY.type

implicit def Boolean2IFormula(value: Boolean): IFormula

object Conj

object Const

implicit def ConstantTerm2ITerm(c: ConstantTerm): ITerm

object Difference

object Disj

object Divisibility

object Eq

object EqLit

object EqZ

object Geq

object GeqZ

implicit def IdealInt2ITerm(value: IdealInt): ITerm

implicit def Int2ITerm(value: Int): ITerm

object LeafFormula

object NonDivisibility

val Quantifier: terfor.conjunctions.Quantifier.type

implicit def Range2Interval(range: Range): Interval

object SignConst

object SimpleTerm

val Sort: types.Sort.type

def abs(t: ITerm): ITerm

def all(sorts: Seq[Sort], f: IFormula): IFormula

def all(f: (ITerm, ITerm, ITerm, ITerm, ITerm) ⇒ IFormula): IFormula

def all(f: (ITerm, ITerm, ITerm, ITerm) ⇒ IFormula): IFormula

def all(f: (ITerm, ITerm, ITerm) ⇒ IFormula): IFormula

def all(f: (ITerm, ITerm) ⇒ IFormula): IFormula

def all(f: (ITerm) ⇒ IFormula): IFormula

def all(f: IFormula): IQuantified

def and(fors: Iterable[IFormula]): IFormula

def and(fors: Iterator[IFormula]): IFormula

final def asInstanceOf[T0]: T0

def clone(): AnyRef

def connect(fors: Iterator[IFormula], op: IBinJunctor.Value): IFormula

def connect(fors: Iterable[IFormula], op: IBinJunctor.Value): IFormula

def connectSimplify(fors: Iterator[IFormula], op: IBinJunctor.Value): IFormula

def connectSimplify(fors: Iterable[IFormula], op: IBinJunctor.Value): IFormula

implicit def constantSeq2ITermSeq(lcs: Seq[ConstantTerm]): Seq[ITerm]

implicit def constantSeq2RichITermSeq(lcs: Seq[ConstantTerm]): RichITermSeq

def containFunctionApplications(f: IFormula): IFormula

def distinct(terms: Iterable[ITerm]): IFormula

def distinct(terms: Iterator[ITerm]): IFormula

def eps(f: (ITerm) ⇒ IFormula): IEpsilon

def eps(sort: Sort, f: IFormula): IEpsilon

def eps(f: IFormula): IEpsilon

final def eq(arg0: AnyRef): Boolean

def eqZero(t: ITerm): IFormula

def equals(arg0: Any): Boolean

def ex(sorts: Seq[Sort], f: IFormula): IFormula

def ex(f: (ITerm, ITerm, ITerm, ITerm, ITerm) ⇒ IFormula): IFormula

def ex(f: (ITerm, ITerm, ITerm, ITerm) ⇒ IFormula): IFormula

def ex(f: (ITerm, ITerm, ITerm) ⇒ IFormula): IFormula

def ex(f: (ITerm, ITerm) ⇒ IFormula): IFormula

def ex(f: (ITerm) ⇒ IFormula): IFormula

def ex(f: IFormula): IQuantified

def geqZero(t: ITerm): IFormula

final def getClass(): Class[_]

def guardAll(f: IFormula, guard: IFormula): IFormula

def guardEx(f: IFormula, guard: IFormula): IFormula

def hashCode(): Int