# Interface Reasoner

All Known Implementing Classes:
`CommonReasoner`, `ContextMinimizingReasoner`, `SimpleReasoner`

public interface Reasoner

A reasoner provides methods to simplify `SymbolicExpression`s 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 Summary

Modifier and Type
Method
Description
`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, ...).
`boolean`
```checkBigOClaim(BooleanExpression constraint, NumericExpression lhs, NumericSymbolicConstant[] limitVars, int[] orders)```
Attempts to prove a uniform "Big-O" claim.
`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.
`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.
`BooleanExpression`
`getFullContext()`
Returns the full context associated to this Reasoner.
`BooleanExpression`
`getReducedContext()`
Returns the reduced context associated to this Reasoner.
`Interval`
`intervalApproximation(NumericExpression expr)`
Returns an interval over-approximation of the given expression.
`boolean`
`isValid(BooleanExpression predicate)`
Equivalent to `valid(predicate).getResultType()==ResultType.YES`.
`BooleanExpression`
`simplify(BooleanExpression expression)`
Simplifies the given boolean expression.
`NumericExpression`
`simplify(NumericExpression expression)`
Simplifies the given numeric expression.
`SymbolicExpression`
`simplify(SymbolicExpression expression)`
Simplify the given expression under the context.
`ValidityResult`
`unsat(BooleanExpression predicate)`
Attempts to determine whether the statement p(x) && q(x) is unsatisfiable.
`ValidityResult`
`valid(BooleanExpression predicate)`
Attempts to determine whether the statement p(x)=>q(x) is a tautology.
`ValidityResult`
`validOrModel(BooleanExpression predicate)`
Attempts to determine whether p(x)=>q(x) is valid, and, if not, also returns a model (counter-example).
• ## Method Details

• ### constantSubstitutionMap

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

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

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