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

Class SARLConstants

java.lang.Object
dev.civl.sarl.IF.SARLConstants
public class SARLConstants extends Object

  • Field Summary

    Fields
    Modifier and Type
    Field
    Description
    static boolean
    arrayReadCondSimplify
    Simplifies an expression such as (a WITH i:=x)[j] to i==j?x:a[j].
    static String
    defaultProofDir
    Default directory name for theorem provers to use.
    static IntegerNumber
    polyProbThreshold
    Used in a heuristic to determine when to use probabilistic methods to determine polynomial zero-ness.
    static boolean
    useBackwardSubstitution
    Shall this universe use backwards substitution to solve for certain numeric expressions in terms of others when simplifying? This is used in the Gaussian elimination simplification phase.
    static boolean
    useDoubleOrNegation
    Should an "OR" expression e be simplified as not(simplify(not(e))) ?
    static boolean
    useMultiOrReduction
    A technique for simplifying a context in CNF form that contains multiple or-clauses.

  • Constructor Summary

    Constructors
    Constructor
    Description
    SARLConstants()
     

  • Method Summary

    Methods inherited from class java.lang.Object

    equals, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait

  • Field Details

    • polyProbThreshold

      public static IntegerNumber polyProbThreshold
      Used in a heuristic to determine when to use probabilistic methods to determine polynomial zero-ness. If the product of the number of variables and the total degree is greater than or equal to this number, the polynomial is considered too big to be expanded, and probabilistic techniques will be used instead (unless the probabilistic bound is 0).

    • useBackwardSubstitution

      public static boolean useBackwardSubstitution
      Shall this universe use backwards substitution to solve for certain numeric expressions in terms of others when simplifying? This is used in the Gaussian elimination simplification phase. If this option is false, the results of Gaussian elimination are used only to replace certain expressions with constants. If this option is true, the results are used more generally to replace certain expressions with linear combinations of other expressions. This can reduce the number of symbolic constants occurring in a context, but can be expensive.

    • useMultiOrReduction

      public static boolean useMultiOrReduction
      A technique for simplifying a context in CNF form that contains multiple or-clauses. If two or more or-clauses contain a common factor, a simplification may be possible. This technique looks for all opportunities of that kind. For example, if the context contains clauses p||q1 and p||q2 then it will replace those clauses with the result of p||simplify(q1invalid input: '&'invalid input: '&q2'), where the simplify occurs in the context obtained by removing the two original clauses from the original context.

    • useDoubleOrNegation

      public static boolean useDoubleOrNegation
      Should an "OR" expression e be simplified as not(simplify(not(e))) ?

    • defaultProofDir

      public static String defaultProofDir
      Default directory name for theorem provers to use. Will be created in the system's temporary directory (e.g., /tmp) if it doesn't already exist.

    • arrayReadCondSimplify

      public static boolean arrayReadCondSimplify
      Simplifies an expression such as (a WITH i:=x)[j] to i==j?x:a[j]. This happens immediately in the universe, so the first expression is never even created.

  • Constructor Details

    • SARLConstants

      public SARLConstants()