Module dev.civl.sarl
Package dev.civl.sarl.ideal.IF

Interface IdealFactory

All Superinterfaces:
NumericExpressionFactory
public interface IdealFactory extends NumericExpressionFactory

An IdealFactory provides a few services beyond those guaranteed by an arbitrary NumericExpressionFactory.

The ideal factory produces and manipulates the following kinds of numeric expressions:

A Constant represents a concrete value. Each constant has either integer or real type.

A Primitive expression is one which is not concrete and which is to be treated as an atomic expression, such as a variable, from the point of view of ideal mathematical arithmetic. Examples: symbolic constants, array read expressions of integer or real type, tuple read expressions of integer or real types, and function applications for functions returning integer or real are all primitive expressions. In addition, in this factory a Polynomial is a Primitive so that it can be treated as a "variable" in an expression.

Any value which is the result of raising a primitive expression to a concrete positive integer power is an instance of PrimitivePower. Any Primitive is also a PrimitivePower by taking the exponent to be 1.

A Monic is the product of PrimitivePowers. Any PrimitivePower is also a Monic: it is the product of a single primitive-power. The Constant 1 (integer or real) is also a Monic: it is the empty product. The integer and real 1s are the only constants which are also Monics.

A Monomial is the product of a Constant and a Monic. Any Constant is also a Monomial by taking 1 for the monic. Any Monic is also a Monomial by taking 1 for the constant.

A term map is a map from Monic to Monomial with the property that a monic m in the key set maps to a monomial of the form c*m for some non-zero constant c. A term map is a

invalid reference 
SymbolicMap
, not a SymbolicExpression.

A Polynomial is a sum of the Monomial values of a term map. Polynomial is also a sub-type of Primitive, which is a subtype of PrimitivePower, which is a sub-type of Monic, which is a sub-type of Monomial. In this factory, each instance p of Polynomial satisfies all of the following:

  1. p is the sum of at least 2 non-zero monomials
  2. no term of p is a Polynomial
  3. if p has integer type, the GCD of its coefficients is 1 and the leading coefficient is positive
  4. if p has real type, the leading coefficient is 1

The sum of two term maps is defined by combining the two maps by combining two terms with the same monic by adding the coefficients. The product of two term maps is defined in the usual way: by multiplying each element in one with each element in the other, then combining terms with the same monic by adding coefficients. The product of a Constant and a term map is defined by multiplying that constant by each Monomial value in the term map. The n-th power of a term map is the term map obtained by multiplying the term map with itself n times.

Given any Monomial m, the term map of m is defined as follows:

  1. if m is a Polynomial, the term map is the term map of that polynomial
  2. if m is the product of a Constant and a Polynomial , the term map is the product of the constant and the term map of the polynomial
  3. otherwise, the term map is the map with one entry with value m.

The expansion of a Monomial m is the term map defined recursively as follows:

  • If m is a Primitive which is not a Polynomial, the expansion of m is the singleton map with value m.
  • If m is a Polynomial, the expansion of m is the sum of the expansions of the terms of m.
  • The expansion of the product of a Constant and a Monic is the product of the constant with the expansion of the Monic.
  • The expansion of a PrimitivePower p n is the expansion of p raised to the nth power.

In the following examples, suppose X and Y are Primitives which are not Polynomials.

  • the expansion of the Monomial X is {X }
  • the expansion of the Polynomial X+Y is {X, Y}
  • the expansion of the Monomial 2*(X+Y) is {2* X, 2*Y}
  • the expansion of the Polynomial 2*(X+ Y) + X is {3*X, Y}
  • the expansion of the Monomial X2 is {X 2}
  • the expansion of the Monomial (X+Y) 2 is {X2, 2*XY, Y 2

The product of two Monomials is a Monomial and is defined in the obvious way, by multiplying primitive powers.

Suppose m1 and m2 are two Monomials with no primitive factor in common. The sum m 1 + m2 is defined as follows. First, there is the option of using the ordinary term map or the expansion of the two monomials. The choice of whether or not to expand can be made using some heuristic. In any case, the two term maps are added. The resulting term map is factored (if possible) to produce a Monomial; the result may be a Polynomial.

The sum of two arbitrary Monomials m1 and m 2 is defined as follows. First, the greatest common factor is factored out, so m1=d*rr, m 2=d*r2, where d is a Monomial and r1 and r2 are Monomials which have no primitive factor is common. Hence m1 + m 2 = d*(r1+r2), where the product is again monomial product and the sum r1+ r2 is a Monomial computed as described above.

A RationalExpression is the quotient of two Monomials. Any Monomial is also a RationalExpression by taking the denominator to be the (monomial) 1. Any RationalExpression of integer type is also a Monomial. (The result of integer division of two integer polynomials may be a Primitive expression with operator SymbolicExpression.SymbolicOperator.INT_DIVIDE.)

A relational numeric expression will always be in one of the following forms:

  • 0<m
  • 0≤m
  • m<0
  • m≤0
  • 0=p
  • 0≠p
where m is a Monic and p is a Primitive.

Reductions: 0<x2y iff 0<y. Hence we can assume all powers are 1. Furthermore 0<xy iff ((0<x ∧ 0<y) ∨ (0<−x ∧ 0<−y)). This can be used to reduce everything to Primitives, but unfortunately the size of the formula is exponential in the number of factors. A heuristic could be used to determine whether to expand.

Equality and inequality reductions are easier because xy=0 iff ( x=0 ∨ y=0), which does not involve an expansion in formula size. Similarly, xy≠0 iff (x≠0 ∧ y≠0).

  • Field Details

    • emptyTermList

      static final Monomial[] emptyTermList
      An empty array (i.e., one of length 0) of Monomial. A useful constant.

    • emptyPPList

      static final PrimitivePower[] emptyPPList
      An empty array (i.e., one of length 0) of PrimitivePower. A useful constant.

  • Method Details

    • polynomialFactory

      dev.civl.sarl.util.KeySetFactory<Monic,Monomial> polynomialFactory()
      What is the purpose of the polynomial factory. Is it to create only non-trivial polynomials: expressions where operator is + and all arguments are instances of Monomial? Or is it to create all instances of Polynomial???
      Returns:

    • monicFactory

      dev.civl.sarl.util.KeySetFactory<Primitive,PrimitivePower> monicFactory()

    • monicComparator

      Comparator<Monic> monicComparator()
      The Comparator on Monics. This places some well-defined total order on the set of all instances of Monic.
      Returns:
      the comparator on Monics

    • oneIntObject

      IntObject oneIntObject()
      Returns an IntObject wrapping the int 1.
      Returns:
      the integer 1 as an IntObject

    • intConstant

      Constant intConstant(int value)
      Returns an integer Constant wrapping a Java int value.
      Parameters:
      value - any Java int
      Returns:
      the integer Constant wrapping the given value

    • zeroInt

      Constant zeroInt()
      Description copied from interface: NumericExpressionFactory
      Returns a symbolic expression of integer type with the value of 0
      Specified by:
      zeroInt in interface NumericExpressionFactory
      Returns:

    • zeroReal

      Constant zeroReal()
      Description copied from interface: NumericExpressionFactory
      Returns a symbolic expression of real type with the value of 0
      Specified by:
      zeroReal in interface NumericExpressionFactory
      Returns:

    • zero

      Constant zero(SymbolicType type)
      Returns either the integer constant 0 or the real constant 0, according to the given type.
      Parameters:
      type - either a SymbolicIntegerType or a SymbolicRealType
      Returns:
      a value zero of the specified type
      See Also:

    • constant

      Constant constant(Number number)
      Returns a Constant wrapping the given concrete Number.
      Parameters:
      number - any non-null Number
      Returns:
      a Constant wrapping number

    • one

      Constant one(SymbolicType type)
      Returns either the integer number one (1) or the real number 1 (1.0). The choice is made according to the given type. In either case, the object returned is an instance of both Constant and Monic, because one is the empty Monic.
      Parameters:
      type - either a SymbolicIntegerType or a SymbolicRealType
      Returns:
      the number 1 as a symbolic expression

    • primitivePower

      PrimitivePower primitivePower(Primitive primitive, NumberObject exponent)
      Returns an instance of PrimitivePower representing raising the given primitive the given exponent.
      Parameters:
      primitive - the base, a non-null numeric primitive of integer or real type
      exponent - the exponent, is a NumberObject which must represent a non-negative integer
      Returns:
      a PrimitivePower expression representing raising primitive to the power exponent

    • getConcreteExponent

      IntegerNumber getConcreteExponent(RationalExpression exponent)

      Given the exponent in a potential power expression, this method computes a concrete integer that can be factored out of that exponent so that the exponent is in canonical form. Specifically, if the exponent has form p/q, and p=c*m, where p and q are Monomials and c is a Constant, and c=n/d, where n and d are IntegerNumbers, this method returns n. Note that n may be positive or negative. It will only be 0 if exponent is 1.

      The exponent can be safely divided by the integer returned by this method. If this method is given e and returns n, then the power expression can be rewritten as a PrimitivePower with primitive POWER(x,e/n) and exponent n, if n is positive, or as the rational expression 1/PrimitivePower[POWER(x,e/n), -n], if n is negative.

      Parameters:
      exponent - a non-null rational expression of integer or real type
      Returns:
      an concrete positive integer n which can be factored out from exponent

    • monic

      Monic monic(SymbolicType type, PrimitivePower[] factorSet)
      Returns a (possibly trivial) monic as specified. If the given monic map is empty, this returns 1 (an instance of One of the appropriate type). If the monic map has a single entry, this returns the value for that entry, which is a PrimitivePower. Otherwise, returns a non-trivial monic (instance of NTMonic).
      Parameters:
      type - either integer or real type
      factorSet - a monic map with any number of entries; this maps a primitive to a power of that primitive; all keys and values must have type consistent with type
      Returns:
      instance of Monic corresponding to arguments as described above
      See Also:
      • invalid reference 
        #ntMonic(SymbolicType, SymbolicMap)

    • monicMask

      Monic monicMask(Monic monic, boolean[] mask)
      Given a Monic returns the Monic obtained by removing some of the PrimitivePower factors according to the given mask. The mask is an array whose length is the number of PrimitivePower factors in monic. A true mask entry indicates the corresponding factor should be kept; a false entry indicates the corresponding factor should be removed.
      Parameters:
      monic - a non-null Monic
      mask - array of boolean whose length equals number of primitive power factors in monic
      Returns:
      a Monic with same type as monic obtained from monic by keeping only those factors for which the corresponding bit in mask is true

    • monomial

      Monomial monomial(Constant constant, Monic monic)
      Returns a Monomial which is the product of the given constant and the given monic. The two arguments must have the same type. If constant is 1, the Monomial returned may be an instance of Monic; if constant is 0, the Monomial returned may be an instance of Constant (representing 0). This method relieves the use of having to figure out exactly which kind of object to create to represent the product of a Constant and a Monic.
      Parameters:
      constant - any non-null Constant
      monic - a Monic of the same type as the constant
      Returns:
      the product of constant and monic

    • multiplyMonomials

      Monomial multiplyMonomials(Monomial m1, Monomial m2)
      Computes the product of any two Monomials of the same type.
      Parameters:
      m1 - a non-null Monomial
      m2 - a non-null Monomial of the same type as m1
      Returns:
      the product of m1 and m2

    • addMonomials

      Monomial addMonomials(Monomial m1, Monomial m2)
      Computes the sum of any two Monomials of the same type.
      Parameters:
      m1 - a non-null Monomial
      m2 - a non-null Monomial of the same type as m1
      Returns:
      the sum of m1 and m2

    • addMonomials

      Monomial addMonomials(Monomial[] monomials)
      Computes the sum of a non-empty set of Monomials of the same type. The result produced by this method may differ from that produced by repeated applications of the binary method
      invalid @link 
      {@link {@link
      #addMonomials(Monomial, Monomial)}. Example: 
        (xy + x) + z = x(y+1) + z  // two binary additions
   xy + x + z  = xy + x + z  // one invocation of this method
      Parameters:
      monomials - an array of positive length consisting of Monomials which all have the same type
      Returns:
      an expression representing the sum of the monomials

    • multiplyConstantMonomial

      Monomial multiplyConstantMonomial(Constant constant, Monomial monomial)
      Returns the product of a Constant and a Monomial of the same type.
      Parameters:
      constant - a non-null Constant
      monomial - a non-null Monomial of the same type as constant
      Returns:
      a Monomial representing the product

    • isZero

      BooleanExpression isZero(Monomial monomial)
      Computes boolean expression equivalent to m=0.
      Parameters:
      monomial - a non-null Monomial
      Returns:
      a boolean expression equivalent to monomial=0.

    • isNonZero

      BooleanExpression isNonZero(Monomial monomial)
      Computes an expression equivalent to "monomial != 0".
      Parameters:
      monomial - any non-null Monomial
      Returns:
      an expression equivalent to monomial != 0

    • divideIntegerMonomials

      Monomial divideIntegerMonomials(Monomial numerator, Monomial denominator)

      Divides two Monomials of integer type. This will always return a Monomial, never a non-monomial RationalExpression. In the worst case (if the denominator does not evenly divide the numerator), the result will be a primitive expression (NumericPrimitive) in which the operator is SymbolicExpression.SymbolicOperator.INT_DIVIDE.

      Note on integer division: assume all terms positive. (ad)/(bd) = a/b

      Parameters:
      numerator - polynomial of integer type
      denominator - polynomial of integer type
      Returns:
      result of division as Monomial, which might be a new primitive expression

    • modulo

      Monomial modulo(NumericExpression arg0, NumericExpression arg1)
      Returns a symbolic expression which represents arg0 modulo arg1. The two given expressions must have the integer type. What happens for negative integers is unspecified. Since expressions of integer type are always instances of Monomial, this method signature is refined to return Monomial.
      Specified by:
      modulo in interface NumericExpressionFactory
      Parameters:
      arg0 - a symbolic expression of integer type
      arg1 - a symbolic expression of integer type
      Returns:
      arg0 % arg1

    • oneTermMap

      Monomial[] oneTermMap(SymbolicType type)

      Returns a

      invalid reference 
      SymbolicMap
      with a single entry mapping the monic One to itself. The type of One will be the given type.

      A term map represents a set of Monomials, which are considered to be the terms in a sum. The Monomials are indexed by their corresponding Monics for efficient look-up. An entry in a term map is an ordered pair of the form (m,c*m), where m is a Monic and c is a non-0 Constant.

      Parameters:
      type - either a SymbolicIntegerType or a SymbolicRealType
      Returns:
      the term map consisting of a single term, one

    • addTermMaps

      Monomial[] addTermMaps(Monomial[] map1, Monomial[] map2)
      Computes the sum of two term maps as a term map. The sum is defined in the obvious way: the coefficient associated to a monic is the sum of the coefficients associated to that monic in the given maps, where the absence of a monic in a map is understood to be 0 (sparse representation). If the sum is 0, the entry is removed from the result, to maintain the sparse representation.
      Parameters:
      map1 - a non-null term map
      map2 - a non-nullinvalid input: '<'/code term map of the same type as map1
      Returns:
      a term map which represents the sum of the two given maps
      See Also:

    • multiplyTermMaps

      Monomial[] multiplyTermMaps(Monomial[] map1, Monomial[] map2)
      Returns the products of the two term maps as a term map. The product is roughly an O(n^2) operation, where n is the length of each term map. It is defined in the usual way: each term in the first map is multiplied with every term in the second map, and the results are summed.
      Parameters:
      map1 - a non-null term map
      map2 - a non-nullinvalid input: '<'/code term map of the same type as map1
      Returns:
      a term map which represents the sum of the two given maps
      See Also:

    • multiplyConstantTermMap

      Monomial[] multiplyConstantTermMap(Constant constant, Monomial[] map)
      Computes the term map obtained by multiplying the given Constant with every term in a given term map.
      Parameters:
      constant - a non-null Constant
      map - a term map of the same type as constant
      Returns:
      the term map obtained by multiplying constant with every term in map

    • powerTermMap

      Monomial[] powerTermMap(SymbolicType type, Monomial[] map, NumberObject exponent)
      Raises a term map to the given power, returning the result as a term map. This is the same as multiplying the term map with itself exponent times. The exponent is a NumberObject representing a non-negative integer. The type must be provided in case map is empty. Otherwise, the map must have the type type.
      Parameters:
      type - the type of the given map and result
      map - a non-null term map
      exponent - a NumberObject representing a non-negative integer
      Returns:
      the result of multiplying map with itself exponent times

    • factorTermMap

      Monomial factorTermMap(Monomial[] terms)

      Computes a Monomial which is equivalent to the sum of the terms in the given term map. The goal is to attempt to factor the Polynomial as much as practical.

      Pre-condition: maps is non-empty.

      Parameters:
      terms - a term map, i.e., a map from Monic to Monomial with the property that a Monic m maps to a Monomial of the form c*m, for some non-0 Constant c
      Returns:
      a Monomial equivalent to the sum of the Monomial values of map

    • polynomial

      Polynomial polynomial(SymbolicType type, Monomial[] terms)
      Produces the result of summing the Monomials of a term map as a Polynomial.
      Parameters:
      type - the type of terms (needed in case terms is empty)
      terms - a non-null term map
      Returns:
      the result of summing the terms in the term map

    • ntRationalExpression

      RationalExpression ntRationalExpression(Monomial numerator, Monomial denominator)
      Constructs new instance of NTRationalExpression. Nothing is checked.

      Preconditions: numerator is not 0. If real type, denominator has degree at least 1 and leading coefficient 1. The numerator and denominator have no common factors in their factorizations.

      Parameters:
      numerator - the polynomial to use as numerator
      denominator - the polynomial to use as denominator
      Returns:
      rational expression p/q

    • isPositive

      BooleanExpression isPositive(RationalExpression rational)
      Given a rational expression rational returns an expression equivalent to 0<rational. This method will perform basic simplifications; for example, if rational is concrete, this method will return a concrete boolean expression (either "true" or "false").
      Parameters:
      rational - a non-null instance of RationalExpression
      Returns:
      an expression equivalent to 0<rational

    • isNonnegative

      BooleanExpression isNonnegative(RationalExpression rational)
      Given a rational expression rational returns an expression equivalent to 0≤rational. This method will perform basic simplifications; for example, if rational is concrete, this method will return a concrete boolean expression (either "true" or "false").
      Parameters:
      rational - a non-null instance of RationalExpression
      Returns:
      an expression equivalent to 0≤rational

    • power

      RationalExpression power(NumericExpression arg0, NumericExpression arg1)
      Description copied from interface: NumericExpressionFactory
      General power operator: e^b. Both e and b are numeric expressions.
      Specified by:
      power in interface NumericExpressionFactory
      Parameters:
      arg0 - the base expression in the power expression
      arg1 - the exponent in the power expression

    • expression

      RationalExpression expression(SymbolicExpression.SymbolicOperator operator, SymbolicType numericType, SymbolicObject... arguments)
      Description copied from interface: NumericExpressionFactory
      Returns an expression, given the operator, type, and array of arguments
      Specified by:
      expression in interface NumericExpressionFactory
      Parameters:
      operator - A SymbolicOperator
      numericType - A SymbolicType
      arguments - array of arguments
      Returns:
      Returns a NumericExpression

    • add

      RationalExpression add(NumericExpression arg0, NumericExpression arg1)
      Description copied from interface: NumericExpressionFactory
      Returns a symbolic expression which is the result of adding arg1 from arg0. The two given expressions must have the same (numeric) type: either both integers, or both real.
      Specified by:
      add in interface NumericExpressionFactory
      Parameters:
      arg0 - a symbolic expression of a numeric type
      arg1 - a symbolic expression of the same numeric type
      Returns:
      arg0+arg1

    • subtract

      RationalExpression subtract(NumericExpression arg0, NumericExpression arg1)
      Description copied from interface: NumericExpressionFactory
      Returns a symbolic expression which is the result of subtracting arg1 and arg0. The two given expressions must have the same (numeric) type: either both integers, or both real.
      Specified by:
      subtract in interface NumericExpressionFactory
      Parameters:
      arg0 - a symbolic expression of a numeric type
      arg1 - a symbolic expression of the same numeric type
      Returns:
      arg0-arg1

    • multiply

      RationalExpression multiply(NumericExpression arg0, NumericExpression arg1)
      Description copied from interface: NumericExpressionFactory
      Returns a symbolic expression which is the result of multiplying the two given symbolic exprssions. The two given expressions must have the same (numeric) type: either both integers, or both real.
      Specified by:
      multiply in interface NumericExpressionFactory
      Parameters:
      arg0 - a symbolic expression of a numeric type
      arg1 - a symbolic expression of the same numeric type
      Returns:
      arg0 * arg1, the product of arg0 and arg1.

    • divide

      RationalExpression divide(NumericExpression arg0, NumericExpression arg1)
      Description copied from interface: NumericExpressionFactory
      Returns a symbolic expression which is the result of dividing arg0 by arg1. The two given expressions must have the same (numeric) type: either both integers, or both real. In the integer case, division is interpreted as "integer division", which rounds towards 0.
      Specified by:
      divide in interface NumericExpressionFactory
      Parameters:
      arg0 - a symbolic expression of a numeric type
      arg1 - a symbolic expression of the same numeric type
      Returns:
      arg0 / arg1