Uses of Interface
dev.civl.sarl.IF.ValidityResult

Packages that use ValidityResult

Package	Description
dev.civl.sarl.IF	This package and its subpackages provide the "public interface" to SARL.
dev.civl.sarl.prove.IF	Module "prove" constitutes the interface between SARL and (possibly external) theorem provers.

Uses of ValidityResult in dev.civl.sarl.IF

Subinterfaces of ValidityResult in dev.civl.sarl.IF

Modifier and Type	Interface	Description
interface	ModelResult	A result to a validity query which also requested a model in case the answer was "NO", and for which the answer was "NO".

Methods in dev.civl.sarl.IF that return ValidityResult

Modifier and Type	Method	Description
ValidityResult	Reasoner.unsat(BooleanExpression predicate)	Attempts to determine whether the statement p(x) invalid input: '&'invalid input: '&' q(x) is unsatisfiable.
ValidityResult	Reasoner.valid(BooleanExpression predicate)	Attempts to determine whether the statement p(x)=>q(x) is a tautology.
ValidityResult	Reasoner.validOrModel(BooleanExpression predicate)	Attempts to determine whether p(x)=>q(x) is valid, and, if not, also returns a model (counter-example).

Uses of ValidityResult in dev.civl.sarl.prove.IF

Fields in dev.civl.sarl.prove.IF declared as ValidityResult

Modifier and Type	Field	Description
static final ValidityResult	Prove.RESULT_MAYBE	A constant of type ValidityResult which has ValidityResult.ResultType invalid reference ResultType.MAYBE .
static final ValidityResult	Prove.RESULT_NO	A constant of type ValidityResult which has ValidityResult.ResultType invalid reference ResultType.NO .
static final ValidityResult	Prove.RESULT_YES	A constant of type ValidityResult which has ValidityResult.ResultType invalid reference ResultType.YES .

Methods in dev.civl.sarl.prove.IF that return ValidityResult

Modifier and Type	Method	Description
ValidityResult	TheoremProver.unsat(BooleanExpression predicate)	Attempts to determine whether the statement p(x) invalid input: '&'invalid input: '&' q(x) is unsatisfiable.
ValidityResult	TheoremProver.valid(BooleanExpression predicate)	Attempts to determine whether the statement p(x)=>q(x) is valid, i.e., is a tautology.
static ValidityResult	Prove.validityResult(ValidityResult.ResultType type)	Returns one of the constants Prove.RESULT_YES, Prove.RESULT_NO, Prove.RESULT_MAYBE, corresponding to the given type.
ValidityResult	TheoremProver.validOrModel(BooleanExpression predicate)	Attempts to determine whether p(x)=>q(x) is valid, and, if not, also returns a model (counterexample).