Package gprover

Class CST

java.lang.Object

gprover.CST

public class CST
extends java.lang.Object

The CST class contains constants and utility methods for managing geometric constructions and their validations.

This class provides arrays for construction types, intersection types, and conclusion types, along with methods to retrieve indices, generate descriptive strings for geometric constructions, and perform various validations and conversions.

The static method charCons(int, Cons, Cons, Object[]) constructs a new construction by combining two given constructions, performing necessary validations and point adjustments based on geometric rules.

Field Summary

Fields

Modifier and Type	Field	Description
static java.lang.String[]	conclusion
static java.lang.String[]	cst
static java.lang.String[]	inters
static java.lang.String[]	s_conc_detail

Method Summary

Modifier and Type	Method	Description
static void	addPss(Cons c, java.lang.Object[] pss)	Adds additional point specification data to the given construction.
static Cons	charCons(int pt, Cons c1, Cons c2, java.lang.Object[] pss)	Constructs a new construction by combining two given construction objects.
static void	exchange(int i, int j, int[] ps)	Exchanges the elements at indices i and j in the given array.
static int	ge_lt_foot(int t, int[] p)	Adjusts the type code for a line-to-foot construction.
static int	get_pred(java.lang.String s)	Gets the index of a predicate type.
static java.lang.String	get_preds(int n)	Gets the predicate type as a string.
static int	getClu(java.lang.String s)	Gets the index of a conclusion type.
static int	getClu_D(java.lang.String s)	Gets the index of a detailed conclusion description.
static java.lang.String	getClus(int n)	Gets the conclusion or intersection type as a string.
static java.lang.String	getDString(java.lang.Object[] pss, int t)	Gets a descriptive string for a given type and parameters.
static java.lang.String	getDString(java.lang.Object[] pss, int t, boolean d)	Gets a descriptive string for a given type and parameters.
static int[]	pcopy(int[] p)	Creates a copy of the given integer array.
static void	reval(int pt, int[] p, int n)	Revalidates the provided array of point indices based on the reference point and count.
static void	spec(int pt, Cons c)	Adjusts the specification fields of the given construction based on the reference point.
static int	validate_all(int pt, int t1, int[] p1)	Validates and adjusts the type code for a construction based on the reference point and its associated point indices.
static int	validate_cg(int pt, int[] ps)	Validates and adjusts the construction type for a congruence of distances construction.
static int	validate_coll(int pt, int[] ps)	Validates and adjusts the construction type for a collinearity scenario.
static int	validate_ea(int pt, int[] ps)	Validates and adjusts the construction type for an angle-related scenario.
static int	validate_p(int pt, int[] ps)	Validates and adjusts the construction type for a parallel scenario.
static int	validate_t(int pt, int[] ps)	Validates and adjusts the construction type for a perpendicular construction.
static java.lang.String	vprint(int m, int n, java.lang.Object[] ps)	Generates a concatenated String of the non-null elements in the specified subarray.

Methods inherited from class java.lang.Object

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

Field Detail

cst

public static final java.lang.String[] cst

inters

public static final java.lang.String[] inters

conclusion

public static final java.lang.String[] conclusion

s_conc_detail

public static java.lang.String[] s_conc_detail

Method Detail

getClu

public static int getClu(java.lang.String s)

Gets the index of a conclusion type.

Parameters:

s - The conclusion type as a string.

Returns:

The index of the conclusion type.

getClu_D

public static int getClu_D(java.lang.String s)

Gets the index of a detailed conclusion description.

Parameters:

s - The detailed conclusion description as a string.

Returns:

The index of the detailed conclusion description.

getClus

public static java.lang.String getClus(int n)

Gets the conclusion or intersection type as a string.

Parameters:

n - The index of the type.

Returns:

The type as a string.

get_pred

public static int get_pred(java.lang.String s)

Gets the index of a predicate type.

Parameters:

s - The predicate type as a string.

Returns:

The index of the predicate type.

get_preds

public static java.lang.String get_preds(int n)

Gets the predicate type as a string.

Parameters:

n - The index of the type.

Returns:

The type as a string.

getDString

public static java.lang.String getDString(java.lang.Object[] pss,
                                          int t)

Gets a descriptive string for a given type and parameters.

Parameters:

pss - The parameters.

t - The type.

Returns:

The descriptive string.

getDString

public static java.lang.String getDString(java.lang.Object[] pss,
                                          int t,
                                          boolean d)

Gets a descriptive string for a given type and parameters.

Parameters:

pss - The parameters.

t - The type.

d - Whether to include detailed descriptions.

Returns:

The descriptive string.

vprint

public static java.lang.String vprint(int m,
                                      int n,
                                      java.lang.Object[] ps)

Generates a concatenated String of the non-null elements in the specified subarray.

Parameters:

m - the starting index (inclusive)

n - the ending index (inclusive)

ps - the array of Objects

Returns:

a String containing the concatenation of each non-null element's String representation

charCons

public static Cons charCons(int pt,
                            Cons c1,
                            Cons c2,
                            java.lang.Object[] pss)

Constructs a new construction by combining two given construction objects.

This method performs the necessary validations and adjustments of point indices according to geometric rules. If the primary construction (c1) is null, the method uses the secondary construction (c2) as the basis for constructing the new Cons object.

Parameters:

pt - the reference point index used for adjustments

c1 - the primary Cons object; may be null

c2 - the secondary Cons object to use if c1 is null

pss - the array of point information associated with the construction

Returns:

the resulting Cons object after combining and validating the constructions

spec

public static void spec(int pt,
                        Cons c)

Adjusts the specification fields of the given construction based on the reference point.

This method analyzes and modifies the type and point indices of the provided construction (c) according to geometric rules and validations.

Parameters:

pt - the reference point index used for adjustments

c - the construction object to be adjusted; may be null

addPss

public static void addPss(Cons c,
                          java.lang.Object[] pss)

Adds additional point specification data to the given construction.

This method processes the provided array of point specification data and updates the corresponding fields in the construction object accordingly.

Parameters:

c - the construction object to update

pss - the array of additional point specification data

reval

public static void reval(int pt,
                         int[] p,
                         int n)

Revalidates the provided array of point indices based on the reference point and count.

This method applies revalidation rules to adjust the point indices in the array so that they are consistent with the given reference point.

Parameters:

pt - the reference point used for revalidation

p - the array of point indices to validate

n - the number of valid entries in the point indices array

ge_lt_foot

public static int ge_lt_foot(int t,
                             int[] p)

Adjusts the type code for a line-to-foot construction. Applies foot-specific rules and validations on the provided type and point array.

Parameters:

t - the original type code

p - the array of point indices associated with the construction

Returns:

the adjusted type code after applying the foot-specific rules

validate_all

public static int validate_all(int pt,
                               int t1,
                               int[] p1)

Validates and adjusts the type code for a construction based on the reference point and its associated point indices.

This method checks the provided point index array and the initial type code, applying specific geometric rules to ensure the correctness of the construction. It returns an adjusted type code reflecting any validations applied, or 0 if the validation fails.

Parameters:

pt - the reference point index used during validation

t1 - the initial type code of the construction

p1 - an array of point indices associated with the construction (may be modified during validation)

Returns:

the validated (and possibly adjusted) type code, or 0 if validation fails

validate_ea

public static int validate_ea(int pt,
                              int[] ps)

Validates and adjusts the construction type for an angle-related scenario.

This method checks and modifies the provided point indices array for angle-related constructions, applying specific geometric validations. It returns an adjusted type code if the validation is successful, or 0 if validation fails.

Parameters:

pt - the reference point index used for validation

ps - an array of point indices related to the construction

Returns:

the validated (and possibly adjusted) type code, or 0 if validation fails

validate_coll

public static int validate_coll(int pt,
                                int[] ps)

Validates and adjusts the construction type for a collinearity scenario.

This method examines the provided array of point indices and determines if they satisfy the conditions for defining a collinear construction. It returns the validated type code if successful, or 0 if validation fails.

Parameters:

pt - the reference point index used for validation

ps - the array of point indices to validate

Returns:

the validated type code for the collinear construction, or 0 if validation fails

validate_p

public static int validate_p(int pt,
                             int[] ps)

Validates and adjusts the construction type for a parallel scenario.

This method examines the array of point indices and validates them according to the rules for parallel constructions. It returns the validated type code if the validation is successful, or 0 if validation fails.

Parameters:

pt - the reference point index used during validation

ps - the array of point indices associated with the parallel construction

Returns:

the validated construction type code for a parallel configuration, or 0 if invalid

validate_t

public static int validate_t(int pt,
                             int[] ps)

Validates and adjusts the construction type for a perpendicular construction.

This method examines the provided array of point indices and applies perpendicular-specific validation rules. It may reorder or adjust the point indices to ensure consistency with the geometric definition of a perpendicular construction. If the validation is successful, the method returns the adjusted construction type; otherwise, it returns 0.

Parameters:

pt - the reference point index used during validation

ps - the array of point indices associated with the construction

Returns:

the validated (and possibly adjusted) construction type code, or 0 if validation fails

validate_cg

public static int validate_cg(int pt,
                              int[] ps)

Validates and adjusts the construction type for a congruence of distances construction.

This method examines the provided array of point indices associated with a congruence construction (e.g., verifying segment congruence) and applies specific validations. It returns an adjusted type code reflecting the outcome of the validation, or 0 if validation fails.

Parameters:

pt - the reference point index used for validation

ps - the array of point indices associated with the congruence construction

Returns:

the validated construction type code, or 0 if validation fails

exchange

public static void exchange(int i,
                            int j,
                            int[] ps)

Exchanges the elements at indices i and j in the given array.

Parameters:

i - the index of the first element to exchange

j - the index of the second element to exchange

ps - the array in which the elements will be swapped

pcopy

public static int[] pcopy(int[] p)

Creates a copy of the given integer array. This method returns a new array containing the same elements as the input array.

Parameters:

p - the array to copy

Returns:

a new array that is a copy of p