Module dev.civl.sarl

Package dev.civl.sarl.prove.IF

Class Prove

java.lang.Object

dev.civl.sarl.prove.IF.Prove

public class Prove
extends Object

This is the entry point for module prove. It provides:

• constants of type ValidityResult corresponding to the three different kinds of validity results: RESULT_YES, RESULT_NO, and RESULT_MAYBE
• methods for producing new TheoremProverFactory instances.
• various other methods dealing with prover results

Field Summary

Fields

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

Constructor Summary

Constructors

Constructor	Description
Prove()

Method Summary

Modifier and Type	Method	Description
static ModelResult	modelResult(Map<SymbolicConstant,SymbolicExpression> model)	Constructs a new ModelResult wrapping the given mapping from symbolic constants to symbolic expressions.
static TheoremProverFactory	newMultiProverFactory(PreUniverse universe, SARLConfig config, Path workingDirectory)	Constructs a new theorem prover factory based on the given configuration.
static TheoremProverFactory	newProverFactory(PreUniverse universe, ProverInfo prover, Path workingDirectory)	Constructs a new theorem prover factory based on a single underlying theorem prover.
static TheoremProverFactory	trivialProverFactory()
static ValidityResult	validityResult(ValidityResult.ResultType type)	Returns one of the constants RESULT_YES, RESULT_NO, RESULT_MAYBE, corresponding to the given type.

Methods inherited from class java.lang.Object

equals, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait

Field Details

RESULT_YES

public static final ValidityResult RESULT_YES

A constant of type ValidityResult which has ValidityResult.ResultType

invalid reference

ResultType.YES

.

RESULT_NO

public static final ValidityResult RESULT_NO

A constant of type ValidityResult which has ValidityResult.ResultType

invalid reference

ResultType.NO

.

RESULT_MAYBE

public static final ValidityResult RESULT_MAYBE

A constant of type ValidityResult which has ValidityResult.ResultType

invalid reference

ResultType.MAYBE

.

Constructor Details

Prove

public Prove()

Method Details

newMultiProverFactory

public static TheoremProverFactory newMultiProverFactory(PreUniverse universe,
 SARLConfig config,
 Path workingDirectory)

Constructs a new theorem prover factory based on the given configuration. A resulting prover resolves a query as follows: it starts by using the first external prover in the given config. If that result is inconclusive, it goes to the next, and so on.

Parameters:

universe - the symbolic universe used to manage and produce symbolic expressions

config - a SARL configuration object specifying some sequence of theorem provers which are available

Returns:

a new theorem prover factory which may use all of the provers specified in the config, in order, until a conclusive result is reached or all provers have been exhausted

newProverFactory

public static TheoremProverFactory newProverFactory(PreUniverse universe,
 ProverInfo prover,
 Path workingDirectory)

Constructs a new theorem prover factory based on a single underlying theorem prover.

Parameters:

universe - the symbolic universe used to produce and manipulate symbolic expressions

prover - a ProverInfo object providing information on the specific underlying theorem prover which will be used

Returns:

the new theorem prover factory based on the given prover

trivialProverFactory

public static TheoremProverFactory trivialProverFactory()

validityResult

public static ValidityResult validityResult(ValidityResult.ResultType type)

Returns one of the constants RESULT_YES, RESULT_NO, RESULT_MAYBE, corresponding to the given type.

Parameters:

type - a non-null ValidityResult.ResultType

Returns:

either RESULT_YES, RESULT_NO, or RESULT_MAYBE, depending on whether type is ValidityResult.ResultType.YES, ValidityResult.ResultType.NO, or ValidityResult.ResultType.MAYBE, respectively.

modelResult

public static ModelResult modelResult(Map<SymbolicConstant,SymbolicExpression> model)

Constructs a new ModelResult wrapping the given mapping from symbolic constants to symbolic expressions. The represents the case where a validity result is ValidityResult.ResultType.NO and, in addition, a specific counter example has been found. The counterexample specifies a concrete value for each symbolic constant which was used in the query, in such a way that the queried predicate evaluates to false and the queried assumption evaluates to true.

Parameters:

model - mapping giving concrete value to each symbolic constant occurring in the query

Returns:

new instance of ModelResult wrapping the given mode.