Package edu.udel.cis.vsl.sarl.universe.common

Class CommonSymbolicUniverse

java.lang.Object
edu.udel.cis.vsl.sarl.preuniverse.common.CommonPreUniverse
edu.udel.cis.vsl.sarl.universe.common.CommonSymbolicUniverse
All Implemented Interfaces:
CoreUniverse, SymbolicUniverse, PreUniverse
Direct Known Subclasses:
MathUniverse
public class CommonSymbolicUniverse extends CommonPreUniverse implements SymbolicUniverse
A standard implementation of SymbolicUniverse, relying heavily on a given NumericExpressionFactory for dealing with numeric issues and a BooleanExpressionFactory for dealing with boolean expressions.

  • Constructor Details

    • CommonSymbolicUniverse

      public CommonSymbolicUniverse(FactorySystem system)
      Constructs a new CommonSymbolicUniverse from the given system of factories.
      Parameters:
      system - a factory system

  • Method Details

    • reasoner

      public Reasoner reasoner(BooleanExpression context)
      Description copied from interface: SymbolicUniverse
      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.
      Specified by:
      reasoner in interface SymbolicUniverse
      Parameters:
      context - the boolean expression assumed to hold by the Reasoner
      Returns:
      a Reasoner with the given context

    • setReasonerFactory

      public void setReasonerFactory(ReasonerFactory reasonerFactory)

    • extractNumber

      public Number extractNumber(BooleanExpression assumption, NumericExpression expression)
      Description copied from interface: SymbolicUniverse
      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.
      Specified by:
      extractNumber in interface SymbolicUniverse
      Parameters:
      assumption - a boolean expression that is assumed to hold
      expression - a symbolic expression of numeric type
      Returns:
      a concrete Number or null

    • why3Reasoner

      public Reasoner why3Reasoner(BooleanExpression context)
      Description copied from interface: SymbolicUniverse
      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)
      Specified by:
      why3Reasoner in interface SymbolicUniverse
      Parameters:
      context - a non-null boolean expression to be used as the context for the Reasoner
      Returns:
      a Reasoner based on the given context

    • setWhy3ReasonerFactory

      public void setWhy3ReasonerFactory(Why3ReasonerFactory reasonerFactory)

    • enableSARLTestGeneration

      public void enableSARLTestGeneration(boolean enable)
      Description copied from interface: SymbolicUniverse
      Enable SARL test generation. Once it is enabled, clients can call #saveValidCallAsSARLTest(BooleanExpression, BooleanExpression, ProverFunctionInterpretation[], ResultType, String[]) to add new tests and call SymbolicUniverse.generateTestClass(String) to generate Junit test class file.
      Specified by:
      enableSARLTestGeneration in interface SymbolicUniverse
      Parameters:
      enable - true to enable SARL test generation; otherwise, disable SARL test generation

    • saveValidCallAsSARLTest

      public void saveValidCallAsSARLTest(BooleanExpression context, BooleanExpression predicate, ValidityResult.ResultType expectedResult, boolean useWhy3, String testName, String... comments)
      Description copied from interface: SymbolicUniverse

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

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

      Specified by:
      saveValidCallAsSARLTest in interface SymbolicUniverse
      Parameters:
      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

      public void generateTestClass(String name)
      Description copied from interface: SymbolicUniverse

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

      Flush all saved SARLTests to a java class. No-op if pre-condition is not satisified.
      Specified by:
      generateTestClass in interface SymbolicUniverse
      Parameters:
      name - the name of the generated class

    • setLogicFunctions

      public void setLogicFunctions(ProverFunctionInterpretation[] logicFunctions)
      Description copied from interface: SymbolicUniverse

      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

      Specified by:
      setLogicFunctions in interface SymbolicUniverse
      Parameters:
      logicFunctions - an array of ProverFunctionInterpretations