Interface TheoremProver
 All Known Implementing Classes:
MultiProver
,RobustCVCTheoremProver
,RobustWhy3ProvePlatform
,RobustZ3TheoremProver

Method Summary
Modifier and TypeMethodDescriptionuniverse()
Get the symbolic universe associated with the theorem prover.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 valid, i.e., 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

universe
PreUniverse universe()Get the symbolic universe associated with the theorem prover. This is the object used to create and manipulate symbolic expressions. Returns:
 the symbolic universe associated to this theorem prover

valid
Attempts to determine whether the statement p(x)=>q(x) is valid, i.e., is a tautology. 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 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.
Note that if the context is unsatisfiable then any of the three types could be returned.
Consider the case where the context p is "true". If valid(q) 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). If valid(!q) returns YES then q is not satisfiable; if it returns NO then q is satisfiable.
Note that in the case NO is returned, there is no guarantee this method will attempt to find a model (and return an instance of
ModelResult
). If a model is required in the NO case, use methodvalidOrModel(edu.udel.cis.vsl.sarl.IF.expr.BooleanExpression)
instead. 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

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 forvalid(edu.udel.cis.vsl.sarl.IF.expr.BooleanExpression)
, except that aModelResult
is returned in the NO case. This provides a method to get the model. Note that the model may be null if there was some problem in obtaining or constructing the model. 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 context or predicate. The value associated to a key will be a concrete symbolic expression. Returns:
 a validity result as specified above
 Throws:
TheoremProverException
 if something goes wrong with the automated theorem prover during this call
