Package edu.udel.cis.vsl.sarl.IF

Interface Reasoner

All Known Implementing Classes:
CommonReasoner, ContextMinimizingReasoner, SimpleReasoner
public interface Reasoner

A reasoner provides methods to simplify SymbolicExpressions and prove or disprove certain theorems, all under an over-arching assumption known as the "context". The context is a BooleanExpression which is assumed to hold. The context cannot change after the instantiation of the Reasoner.

Note that the context may be simplified to an equivalent form when the reasoner is instantiated. Example: if the context used to create this Reasoner was N>=0 && N>=1, the actual context may become simply N>=1.

  • Method Details

    • constantSubstitutionMap

      Map<SymbolicConstant,SymbolicExpression> constantSubstitutionMap()
      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 simplify(edu.udel.cis.vsl.sarl.IF.expr.SymbolicExpression) method of this simplifier.
      Returns:
      a mapping from some symbolic constants occurring in original context to their solved values

    • getReducedContext

      BooleanExpression getReducedContext()
      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 getFullContext()). This context will not change after creation.
      Returns:
      the reduced context associated to this Reasoner

    • getFullContext

      BooleanExpression getFullContext()
      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 getReducedContext()). Hence the expression returned is equivalent to the original given expression. This context will not change after creation.
      Returns:
      the reduced context associated to this Reasoner

    • assumptionAsInterval

      Interval assumptionAsInterval(SymbolicConstant symbolicConstant)
      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.
      Parameters:
      symbolicConstant - the variable s around which the context may be expressed as an interval constraint
      Returns:
      the interval constraint or null

    • intervalApproximation

      Interval intervalApproximation(NumericExpression expr)
      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.
      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

    • simplify

      SymbolicExpression simplify(SymbolicExpression expression)

      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

      Parameters:
      expression - any symbolic expression
      Returns:
      simplified version of the expression

    • simplify

      BooleanExpression simplify(BooleanExpression expression)
      Simplifies the given boolean expression. Result is same as that of simplify(SymbolicExpression), but this saves you the trouble of casting to BooleanExpression.
      Parameters:
      expression - any BooleanExpression
      Returns:
      simplified version of the expression

    • simplify

      NumericExpression simplify(NumericExpression expression)
      Simplifies the given numeric expression. Result is same as that of simplify(SymbolicExpression), but this saves you the trouble of casting to NumericExpression.
      Parameters:
      expression - any NumericExpression
      Returns:
      simplified version of the expression

    • valid

      ValidityResult valid(BooleanExpression predicate)

      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.

    • unsat

      ValidityResult unsat(BooleanExpression predicate)

      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.

      Parameters:
      predicate - the boolean expression q(x)
      Returns:
      a ValidityResult whose type must satisfy the constraints described above
      Throws:
      TheoremProverException - if something goes wrong with the automated theorem prover during this call

    • validOrModel

      ValidityResult validOrModel(BooleanExpression predicate)

      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 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.

      Parameters:
      predicate - the predicate q(x)
      Returns:
      a validity result as specified above
      Throws:
      TheoremProverException - if something goes wrong with the automated theorem prover during this call

    • isValid

      boolean isValid(BooleanExpression predicate)
      Equivalent to valid(predicate).getResultType()==ResultType.YES.
      Parameters:
      predicate - a boolean expression
      Returns:
      if true is returned, the predicate is valid; nothing can be concluded if false is returned

    • extractNumber

      Number extractNumber(NumericExpression expression)
      If the given expression can be reduced to a concrete numeric value using the context, returns that concrete value, else returns null.
      Parameters:
      expression - any numeric expression
      Returns:
      the concrete (Number) numeric value of that expression or null

    • checkBigOClaim

      boolean checkBigOClaim(BooleanExpression constraint, NumericExpression lhs, NumericSymbolicConstant[] limitVars, int[] orders)

      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.

      Parameters:
      constraint - 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