Module dev.civl.sarl
Package dev.civl.sarl.expr.IF

Interface ExpressionFactory

public interface ExpressionFactory
An ExpressionFactory is used to instantiate instances of SymbolicExpression.

  • Method Details

    • init

      void init()
      Initialize this expression factory. This should be called before it is used. Preconditions: the object factory and type factory have already been initialized.

    • numericFactory

      NumericExpressionFactory numericFactory()
      Returns the numeric expression factory used by this expression factory.
      Returns:
      the numeric expression factory

    • booleanFactory

      BooleanExpressionFactory booleanFactory()
      Returns the boolean expression factory used by this expression factory.
      Returns:
      the boolean expression factory

    • typeFactory

      SymbolicTypeFactory typeFactory()
      Returns the symbolic type factory used by this expression factory.
      Returns:
      the symbolic type factory

    • objectFactory

      ObjectFactory objectFactory()
      Returns the object factory used by this expression factory.
      Returns:
      the object factory

    • comparator

      Comparator<SymbolicExpression> comparator()
      Returns a comparator on all SymbolicExpression objects. The comparator defines a total order on the set of symbolic expressions.
      Returns:
      a comparator on symbolic expressions

    • expression

      SymbolicExpression expression(SymbolicExpression.SymbolicOperator operator, SymbolicType type, SymbolicObject... arguments)
      Returns an expression with the given operator, type, and argument sequence.
      Parameters:
      operator - a symbolic operator
      type - a symbolic type
      arguments - the arguments to the operator as an array
      Returns:
      the expression specified by above

    • symbolicConstant

      SymbolicConstant symbolicConstant(StringObject name, SymbolicType type)

    • referenceType

      SymbolicType referenceType()

    • nullExpression

      SymbolicExpression nullExpression()
      Returns the special expression "NULL", which has the NULL operator, null type, and no arguments.
      Returns:
      the NULL symbolic expression

    • nullReference

      ReferenceExpression nullReference()
      Returns the "null reference", a symbolic expression of reference type which is not equal to a reference value returned by any of the other methods, and which cannot be dereferenced.

    • identityReference

      ReferenceExpression identityReference()
      Returns the identity (or "trivial") reference I. This is the reference characterized by the property that dereference(I,v) returns v for any symbolic expression v.

    • arrayElementReference

      ArrayElementReference arrayElementReference(ReferenceExpression arrayReference, NumericExpression index)
      Given a reference to an array and an index (integer), returns a reference to the element of the array at that index

    • tupleComponentReference

      TupleComponentReference tupleComponentReference(ReferenceExpression tupleReference, IntObject fieldIndex)
      Given a reference to a tuple, and a field index, returns a reference to that component of the tuple

    • unionMemberReference

      UnionMemberReference unionMemberReference(ReferenceExpression unionReference, IntObject memberIndex)
      Given a reference to a union (expression of union type) and an index of a member type of that union, returns a reference to the underlying element

    • offsetReference

      OffsetReference offsetReference(ReferenceExpression reference, NumericExpression offset)
      Given a ReferenceExpression and a NumericExpression offset, returns an offsetReference. (reference+offset)
      Parameters:
      reference -
      offset -
      Returns:
      OffsetReference

    • valueSetContains

      BooleanExpression valueSetContains(SymbolicType valueType, SymbolicExpression refArr0, SymbolicExpression refArr1)

      Test if an array of value set references "refArr0", that is associated with the given "valueType", contains another array of value set references "refArr1", that is associated with the given "valueType" as well.

      Parameters:
      valueType - the type of the value where the given value set references in "refArr0" and "refArr1" refer to
      refArr0 - a concrete array of value set references
      refArr1 - a concrete array of value set references
      Returns:
      a boolean expression representing the result of the test

    • valueSetRefereceNoIntersect

      BooleanExpression valueSetRefereceNoIntersect(SymbolicType valueType, ValueSetReference ref0, ValueSetReference ref1)

      Tests if the two given ValueSetReferences have NO intersection, i.e., if applying the two reference to the same object, if their referred parts have no overlap.

      returns the condition that is true iff the given two value set reference have no intersection.

      Parameters:
      valueType - the type of the value that the two given references can be applied to
      ref0 - an instance of ValueSetReference
      ref1 - an instance of ValueSetReference
      Returns:
      the condition that is true iff the two value set references have no intersection

    • valueSetDiff

      SymbolicExpression valueSetDiff(SymbolicType valueType, SymbolicExpression refArr0, SymbolicExpression refArr1)

    • valueSetWidening

      SymbolicExpression valueSetWidening(Reasoner reasoner, SymbolicType valueType, SymbolicExpression refArr)

      Apply a default widening operator to a value set template, which is in the form of an array of value set references and a symbolic type that is referred by these references.

      Parameters:
      reasoner - a reasoner used for more accurate widening
      valueType - the type of the value where the given value set references in "refArr" refer to
      refArr - a concrete array of value set references
      Returns:
      a symbolic expression of valueSetTemplateType() type, where value set references have been widening-ed

    • valueSetProtectiveWidening

      SymbolicExpression valueSetProtectiveWidening(Reasoner reasoner, SymbolicType valueType, SymbolicExpression refArrM, SymbolicExpression refArrP)

    • valueSetElimWidening

      SymbolicExpression valueSetElimWidening(Reasoner reasoner, SymbolicType valueType, SymbolicExpression refArr, SymbolicExpression elimExpr, NumericExpression lower, NumericExpression upper)

    • vsIdentityReference

      VSIdentityReference vsIdentityReference()
      Returns the identity (or "trivial") value set reference I. This is the reference characterized by the property that dereference(I,v) returns v for any symbolic expression v.

    • vsArrayElementReference

      VSArrayElementReference vsArrayElementReference(ValueSetReference parent, NumericExpression index)
      Given a value set reference to a (set-of) array(s) and an index (integer), returns a reference to the (set-of) elements of the (set-of) array(s) at that index

    • vsArraySectionReference

      VSArraySectionReference vsArraySectionReference(ValueSetReference parent, NumericExpression lower, NumericExpression upper, NumericExpression step)
      Given a reference to a (set-of) array(s) and an inclusive lower index bound, an exclusive upper index bound and a step, returns a reference to the (set-of) section(s) of the array(s) with the given bounds.

    • vsTupleComponentReference

      VSTupleComponentReference vsTupleComponentReference(ValueSetReference parent, IntObject fieldIndex)
      Given a reference to a (set-of) tuple(s), and a field index, returns a reference to that (set-of) component(s) of the tuple(s).

    • vsUnionMemberReference

      VSUnionMemberReference vsUnionMemberReference(ValueSetReference parent, IntObject memberIndex)
      Given a reference to a (set-of) union(s) (expression of union type) and an index of a member type of that union, returns a reference to the (set-of) underlying element(s).

    • vsOffsetReference

      VSOffsetReference vsOffsetReference(ValueSetReference parent, NumericExpression offset)
      Given a reference to a (set-of) value(s) and a integral offset, returns a reference to a (set-of) value(s), which is obtained by applying the (set-of) offset(s) to the given (set-of) value(s).

    • valueSetReferenceType

      SymbolicType valueSetReferenceType()
      Returns:
      the symbolic type of ValueSetReferences

    • valueSetTemplate

      SymbolicExpression valueSetTemplate(SymbolicType valueType, ValueSetReference[] vsRefs)

      Given a symbolic type of a symbolic value and a list of ValueSetReferences, returns symbolic expression representing a value set template.

      A value set template consists of a type t of some value and a set of ValueSetReferences. Applying a value set template to a symbolic value v of the type t results in a subset of the value v.

      Parameters:
      valueType - symbolic type of some value v
      vsRefs - references to subsets of some value v
      Returns:
      a symbolic expression which is a value set template

    • valueSetTemplateType

      SymbolicType valueSetTemplateType()
      Returns the type of a value set template. A value set template is a symbolic expression that can be applied to a value, which is a instance of SymbolicExpression, in order to obtain a subset of the value.
      Returns:
      The symbolic type of a value set template.

    • isValueSetTemplateType

      boolean isValueSetTemplateType(SymbolicType type)
      Parameters:
      type - a symbolic type
      Returns:
      true iff the given type is created by the method valueSetTemplateType()