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

Class SimpleReasoner

java.lang.Object
edu.udel.cis.vsl.sarl.reason.common.SimpleReasoner
All Implemented Interfaces:
Reasoner
public class SimpleReasoner extends Object implements Reasoner
Very basic reasoner that does not use any theorem prover, only simplification.

  • Constructor Details

    • SimpleReasoner

      public SimpleReasoner(Simplifier simplifier)

  • Method Details

    • universe

      public PreUniverse universe()

    • getReducedContext

      public BooleanExpression getReducedContext()
      Description copied from interface: Reasoner
      Returns the reduced context associated to this Reasoner. This expression may differ from the original one used to create the Reasoner because it was simplified or put into a canonical form. Moreover, symbolic constants which have been "solved" may be removed from the context. (For the context with additional equations giving those solved values, use method Reasoner.getFullContext()). This context will not change after creation.
      Specified by:
      getReducedContext in interface Reasoner
      Returns:
      the reduced context associated to this Reasoner

    • getFullContext

      public BooleanExpression getFullContext()
      Description copied from interface: Reasoner
      Returns the full context associated to this Reasoner. This expression may differ from the original one used to create the Reasoner because it was simplified or put into a canonical form. The full context includes equations where one side is a symbolic constant and the other is the solved value. (For the context without those equations, use method Reasoner.getReducedContext()). Hence the expression returned is equivalent to the original given expression. This context will not change after creation.
      Specified by:
      getFullContext in interface Reasoner
      Returns:
      the reduced context associated to this Reasoner

    • assumptionAsInterval

      public Interval assumptionAsInterval(SymbolicConstant symbolicConstant)
      Description copied from interface: Reasoner
      If the context can be represented as a simple interval constraint, i.e., an expression of the form A <= x <= B, where A and B are concrete numbers, x is the given symbolic constant, and <= could be < in either case, this returns the interval [A,B] (or (A,B], or, ...). Else returns null.
      Specified by:
      assumptionAsInterval in interface Reasoner
      Parameters:
      symbolicConstant - the variable s around which the context may be expressed as an interval constraint
      Returns:
      the interval constraint or null

    • simplify

      public SymbolicExpression simplify(SymbolicExpression expression)
      Description copied from interface: Reasoner

      Simplify the given expression under the context. The simplified expression is guaranteed to be equivalent to the given one under the context. I.e., if p and q are the two expressions, and c is the context, then given any assignment of concrete values to symbolic constants for which c holds, p and q will evaluate to the same concrete value.

      Note that the expression can have any type, including array, function, tuple, etc. The simplified expression may have a different type, but the new type is guaranteed to be equivalent to the original under the context. For example, if the given expression has type int[N] (array of int of length N), the simplified expression might have type int[3] (e.g., if the context was "N=3").

      Example: 

       given context: N>=0 && N>=1
 simplified context: N>=1
 result of simplify (N>=1) : true
 result of simplify (N>=2) : N>=2
 result of simplify (N<0)  : false

      Specified by:
      simplify in interface Reasoner
      Parameters:
      expression - any symbolic expression
      Returns:
      simplified version of the expression

    • simplify

      public BooleanExpression simplify(BooleanExpression expression)
      Description copied from interface: Reasoner
      Simplifies the given boolean expression. Result is same as that of Reasoner.simplify(SymbolicExpression), but this saves you the trouble of casting to BooleanExpression.
      Specified by:
      simplify in interface Reasoner
      Parameters:
      expression - any BooleanExpression
      Returns:
      simplified version of the expression

    • simplify

      public NumericExpression simplify(NumericExpression expression)
      Description copied from interface: Reasoner
      Simplifies the given numeric expression. Result is same as that of Reasoner.simplify(SymbolicExpression), but this saves you the trouble of casting to NumericExpression.
      Specified by:
      simplify in interface Reasoner
      Parameters:
      expression - any NumericExpression
      Returns:
      simplified version of the expression

    • valid

      public ValidityResult valid(BooleanExpression predicate)
      Description copied from interface: Reasoner

      Attempts to determine whether the statement p(x)=>q(x) is a tautology. Here, p is the "assumption", q is the "predicate", and x stands for the set of all symbolic constants which occur in p or q.

      A result of YES implies forall x.(p(x)=>q(x)). A result of NO implies nsat(p)||exists x.(p(x)&&!q(x)). Nothing can be concluded from a result of MAYBE.

      nsat(p) means p is not satisfiable, i.e., forall x.!p(x), or equivalently !exists x.p(x). Note that if p is not satisfiable then any of the three possible results could be returned.

      Consider a call to valid(true,q). If this returns YES then forall x.q(x) (i.e., q is a tautology). If it returns NO then exists x.!q(x) (i.e., q is not a tautology).

      Consider a call to valid(true,!q). If this returns YES then q is not satisfiable. If it returns no, then q is satisfiable.

      Specified by:
      valid in interface Reasoner

    • validOrModel

      public ValidityResult validOrModel(BooleanExpression predicate)
      Description copied from interface: Reasoner

      Attempts to determine whether p(x)=>q(x) is valid, and, if not, also returns a model (counter-example). The specification is exactly the same as for Reasoner.valid(edu.udel.cis.vsl.sarl.IF.expr.BooleanExpression), except that a ValidityResult is returned. This provides a method ValidityResult.getResultType() that returns the result type, but also a method ModelResult.getModel() that provides the model. That method will return null if the result type is YES or MAYBE. It may return null even if the result type is NO, either because the assumption is not satisfiable or a model could not be found for some reason.

      If the model is non-null, it will be a map in which the key set consists of all the symbolic constants of non-function type that occur in the assumption or predicate. The value associated to a key will be a concrete symbolic expression.

      Specified by:
      validOrModel in interface Reasoner
      Parameters:
      predicate - the predicate q(x)
      Returns:
      a validity result as specified above

    • constantSubstitutionMap

      public Map<SymbolicConstant,SymbolicExpression> constantSubstitutionMap()
      Description copied from interface: Reasoner
      In the process of simplifying the initial context, this simplifier may have "solved" for some of the symbolic constants occurring in the context. This method returns a map in which the keys are those symbolic constants and the value associated to a key is the "solved" value. The solved value will be substituted for the symbolic constants in any expression given to the Reasoner.simplify(edu.udel.cis.vsl.sarl.IF.expr.SymbolicExpression) method of this simplifier.
      Specified by:
      constantSubstitutionMap in interface Reasoner
      Returns:
      a mapping from some symbolic constants occurring in original context to their solved values

    • isValid

      public boolean isValid(BooleanExpression predicate)
      Description copied from interface: Reasoner
      Equivalent to valid(predicate).getResultType()==ResultType.YES.
      Specified by:
      isValid in interface Reasoner
      Parameters:
      predicate - a boolean expression
      Returns:
      if true is returned, the predicate is valid; nothing can be concluded if false is returned

    • extractNumber

      public Number extractNumber(NumericExpression expression)
      Description copied from interface: Reasoner
      If the given expression can be reduced to a concrete numeric value using the context, returns that concrete value, else returns null.
      Specified by:
      extractNumber in interface Reasoner
      Parameters:
      expression - any numeric expression
      Returns:
      the concrete (Number) numeric value of that expression or null

    • intervalApproximation

      public Interval intervalApproximation(NumericExpression expr)
      Description copied from interface: Reasoner
      Returns an interval over-approximation of the given expression. It is guaranteed that under this reasoner's context, any value taken on by the expression must be contained in the interval returned. The interval returned will have the same type as the expression.
      Specified by:
      intervalApproximation in interface Reasoner
      Parameters:
      expr - the numeric expression (either integer or real type)
      Returns:
      an interval which contains all possible values the expression may assume under the context of this reasoner

    • checkBigOClaim

      public boolean checkBigOClaim(BooleanExpression indexConstraint, NumericExpression lhs, NumericSymbolicConstant[] limitVars, int[] orders)
      Description copied from interface: Reasoner

      Attempts to prove a uniform "Big-O" claim. The claim has the following form: 

       lhs = O(h1^n1) + ... + O(hk^nk)
      Here, lhs or "left hand side expression" is an expression of real type. The h1, ..., hk or "limit variables" are symbolic constants of real type, the variables that are tending towards 0. The n1, ..., nk the corresponding "orders" of the limit variables; they are are concrete nonnegative integers.

      The lhs may involve the hi and also other free variables; typically these will be index variables for indexing into arrays. Assumptions on any of these can be included in the constraint argument.

      Specified by:
      checkBigOClaim in interface Reasoner
      Parameters:
      indexConstraint - any additional constraint (beyond the context) you want to assume when checking the claim; typically range constraints on index variables
      lhs - the left hand side expression, an expression of real type involving any or all of the symbolic constants mentioned, as well as others
      limitVars - the limit variables; an array of length k
      orders - the orders of the limit variables; the length must be the same as the length of limitVars (k)
      Returns:
      true if the O-claim can be proved. A false result does not mean the O-claim is false, it just means it could not be proved

    • unsat

      public ValidityResult unsat(BooleanExpression predicate)
      Description copied from interface: Reasoner

      Attempts to determine whether the statement p(x) && q(x) is unsatisfiable. Here, p is the "context", q is the "predicate", and x stands for the set of all symbolic constants which occur in p or q.

      A result of type YES implies forall x. !(p(x) && q(x)). A result of NO implies exists x. p(x)&&q(x). Nothing can be concluded from a result of MAYBE.

      Specified by:
      unsat in interface Reasoner
      Parameters:
      predicate - the boolean expression q(x)
      Returns:
      a ValidityResult whose type must satisfy the constraints described above