Interface SymbolicUniverse

All Superinterfaces:
All Known Implementing Classes:
CommonSymbolicUniverse, MathUniverse

public interface SymbolicUniverse extends CoreUniverse

A symbolic universe is used for the creation and manipulation of SymbolicObjects. The symbolic objects created by this universe are said to belong to this universe. Every symbolic object belongs to one universe, though a reference to the universe is not necessarily stored in the object.

s are one kind of symbolic object. Other symbolic objects include SymbolicCollections (such as sequences, sets, and maps), SymbolicTypes, and various concrete SymbolicObjects.

SymbolicObjects implement the Immutable Pattern: all symbolic objects are immutable, i.e., they cannot be modified after they are created.

  • Method Details

    • reasoner

      Reasoner reasoner(BooleanExpression context)
      Returns a Reasoner for the given context. A Reasoner provides simplification and reasoning services. The context is the boolean expression assumed to hold by the reasoner. The Reasoner can be used to determine if a boolean predicate is valid; it may use an external theorem prover to assist in this task.
      context - the boolean expression assumed to hold by the Reasoner
      a Reasoner with the given context
    • extractNumber

      Number extractNumber(BooleanExpression assumption, NumericExpression expression)
      Attempts to extract a concrete numeric value from the given expression, using the assumption if necessary to simplify the expression. For example, if the assumption is "N=5" and the expression is "N", this method will probably return the number 5. If it cannot obtain a concrete value for whatever reason, it will return null.
      assumption - a boolean expression that is assumed to hold
      expression - a symbolic expression of numeric type
      a concrete Number or null
    • why3Reasoner

      Reasoner why3Reasoner(BooleanExpression context)
      Same as #reasoner(BooleanExpression, boolean) but only Why3 prove platform will be used if it is installed. If Why3 is not installed, this function is equivalent to #reasoner(BooleanExpression, boolean)
      context - a non-null boolean expression to be used as the context for the Reasoner
      a Reasoner based on the given context
    • setLogicFunctions

      void setLogicFunctions(ProverFunctionInterpretation[] logicFunctions)

      Set a list of logic functions with their definitions to the universe so that Reasoners created by this universe can take use of the definitions of the given logic functions.

      Logic functions are instances of ProverFunctionInterpretations

      logicFunctions - an array of ProverFunctionInterpretations
    • enableSARLTestGeneration

      void enableSARLTestGeneration(boolean enable)
      Enable SARL test generation. Once it is enabled, clients can call #saveValidCallAsSARLTest(BooleanExpression, BooleanExpression, ProverFunctionInterpretation[], ResultType, String[]) to add new tests and call generateTestClass(String) to generate Junit test class file.
      enable - true to enable SARL test generation; otherwise, disable SARL test generation
    • saveValidCallAsSARLTest

      void saveValidCallAsSARLTest(BooleanExpression context, BooleanExpression predicate, ValidityResult.ResultType expectedResult, boolean useWhy3, String testName, String... comments)

      pre-condition enableSARLTestGeneration(boolean) has been set to true

      Saving a query as a SARL's Junit test. No-op if pre-condition is not satisified.

      context - a non-null boolean expression to be used as the context for the Reasoner
      predicate - a non-null boolean expression which is the asserted predicate of the saving query
      expectedResult - the expected ValidityResult.ResultType of this query. If the test gets a result that is same as the expectedResult, the test passes, otherwise the test fails.
      useWhy3 - if this valid call must be proved by why3
      testName - name of this saving test
      comments - Variable number of arguments for Java comments over the generated query. One comment block per argument.
    • generateTestClass

      void generateTestClass(String className)

      pre-condition enableSARLTestGeneration(boolean) has been set to true

      Flush all saved SARLTests to a java class. No-op if pre-condition is not satisified.
      className - the name of the generated class