Interface Reasoner
 All Known Implementing Classes:
CommonReasoner
,ContextMinimizingReasoner
,SimpleReasoner
A reasoner provides methods to simplify SymbolicExpression
s and prove
or disprove certain theorems, all under an overarching 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 TypeMethodDescriptionassumptionAsInterval
(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 "BigO" claim.In the process of simplifying the initial context, this simplifier may have "solved" for some of the symbolic constants occurring in the context.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.Returns the full context associated to this Reasoner.Returns the reduced context associated to this Reasoner.Returns an interval overapproximation of the given expression.boolean
isValid
(BooleanExpression predicate) Equivalent tovalid(predicate).getResultType()==ResultType.YES
.simplify
(BooleanExpression expression) Simplifies the given boolean expression.simplify
(NumericExpression expression) Simplifies the given numeric expression.simplify
(SymbolicExpression expression) Simplify the given expression under the context.unsat
(BooleanExpression predicate) Attempts to determine whether the statement p(x) && q(x) is unsatisfiable.valid
(BooleanExpression predicate) Attempts to determine whether the statement p(x)=>q(x) is a tautology.validOrModel
(BooleanExpression predicate) Attempts to determine whether p(x)=>q(x) is valid, and, if not, also returns a model (counterexample).

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 thesimplify(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 methodgetFullContext()
). 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 methodgetReducedContext()
). 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
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
Returns an interval overapproximation 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
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
Simplifies the given boolean expression. Result is same as that ofsimplify(SymbolicExpression)
, but this saves you the trouble of casting toBooleanExpression
. Parameters:
expression
 any BooleanExpression Returns:
 simplified version of the expression

simplify
Simplifies the given numeric expression. Result is same as that ofsimplify(SymbolicExpression)
, but this saves you the trouble of casting toNumericExpression
. 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 impliesexists 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
Attempts to determine whether p(x)=>q(x) is valid, and, if not, also returns a model (counterexample). The specification is exactly the same as for
valid(edu.udel.cis.vsl.sarl.IF.expr.BooleanExpression)
, except that aValidityResult
is returned. This provides a methodValidityResult.getResultType()
that returns the result type, but also a methodModelResult.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 nonnull, it will be a map in which the key set consists of all the symbolic constants of nonfunction 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
Equivalent tovalid(predicate).getResultType()==ResultType.YES
. Parameters:
predicate
 a boolean expression Returns:
 if
true
is returned, the predicate is valid; nothing can be concluded iffalse
is returned

extractNumber
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 "BigO" 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 variableslhs
 the left hand side expression, an expression of real type involving any or all of the symbolic constants mentioned, as well as otherslimitVars
 the limit variables; an array of length korders
 the orders of the limit variables; the length must be the same as the length oflimitVars
(k) Returns:
true
if the Oclaim can be proved. Afalse
result does not mean the Oclaim is false, it just means it could not be proved
