Package gprover

Class GTerm

java.lang.Object

gprover.GTerm

public class GTerm
extends java.lang.Object

JGEX supports loading and saving scripts in a simple textual format. Among the examples, these files have no extension (see, e.g. 3_JAR/simson). This class can load and save them. * Represents geometric constructions and their associated operations. * *

This class encapsulates the management of points, construction steps, * and constraints within a geometric theorem proving framework. * It provides methods for adding, retrieving, and processing geometric data, * including the generation of non-degenerate and prerequisite constraints. * Fundamental operations include loading, saving, and validating the structure * of geometric constructions.

* *

Utilize this class to perform geometric analyses and manipulations necessary * for automated theorem proving and geometric constraint solving within the * framework.

Field Summary

Fields

Modifier and Type	Field	Description
Cond	conc

Constructor Summary

Constructors

Constructor	Description
GTerm()	Constructs a new GTerm instance.

Method Summary

Modifier and Type	Method	Description
void	add_eqcons(int a, int b, int c, int d)	Adds an equality constraint equating the distances between the two pairs of points.
void	add_preq(int t, int[] p)	Adds prerequisite equality constraints based on the given type and associated points.
boolean	add_pt(java.lang.String s)	Adds a new point with the specified name if it does not already exist.
void	addauxedCons(Cons c)	Adds an auxiliary constraint to the construction.
void	addauxedPoint(ProPoint pt)	Adds an auxiliary point to the construction.
void	addccc(int a, int b, Cons cs)	Adds a circle constraint between the two specified points to the provided constraint, if the connection does not already exist.
void	addConstant(java.lang.String sf, java.lang.String func)	Adds a constant to the construction.
void	addConsV(java.util.Vector v)	Clears current construction data and sets constraints from the given vector.
void	addInterLS(java.lang.String[] list)	Processes an inter-line constraint.
void	addInterSS(java.lang.String[] list)	Processes an inter-segment constraint.
void	addNdg(Cons c)	Updates and adds a non-degenerate constraint if it is not already present.
void	addNDG(Cons c, java.util.Vector v)	Adds a non-degenerate constraint to the specified vector.
void	clear()	Clears all stored points, construction steps, and resets the construction name.
protected ProPoint	fd_pt(java.lang.String sn)	Retrieves a point with the specified name from the list.
void	ge_cpt()	Recalculates and updates constraint point indexes and conclusion values.
void	ge_pss2ps(Cons c)	Converts the string parameters of the given constraint to point indexes.
boolean	generate(java.util.Vector glines)	Generates the construction based on the provided vector of input lines.
void	generateCons(Cons c, java.util.Vector v)	Generates non-degenerate constraints based on the specified constraint and adds them to the provided vector.
void	generateSd(CNdg dg, java.lang.Object[] pss)	Generates a string description for the specified CNdg object based on the provided parameters.
void	getAllCircles()	Aggregates and computes all circle constraints from the current constraint data.
java.util.Vector	getAllNdgs(java.util.Vector v)	Generates all non-degenerate constraints from the given vector.
java.util.Vector	getAllptsText()	Returns a vector containing the names of all points.
java.lang.String	getAnimateString()	Retrieves the animation string for the term.
Cond	getConc()	Returns the current conclusion condition.
Cons	getConclusion()	Retrieves the conclusion constraint if it exists.
java.lang.String	getConcText()	Retrieves the text representation of the current conclusion.
Cons	getcons(int pt, java.util.Vector v)	Retrieves and removes the first constraint in the vector that contains the specified point.
java.util.Vector	getCons()	Returns the vector containing all constraints.
Cons	getCons(int n)	Returns the constraint at the specified index from the constraint vector.
int	getCons_no()	Returns the number of constraints (as derived from the points vector).
int	getconsNum()	Returns the number of constructions excluding the final conclusion if present.
java.lang.String	getName()	Returns the name of the construction.
java.util.Vector	getNcons()	Returns a vector containing non degenerate constraints.
Cons	getNDG_COLL(int t1, int t2, int t3, java.lang.Object o1, java.lang.Object o2, java.lang.Object o3)	Creates a non-degenerate collinearity constraint from the given point identifiers and associated objects.
Cons	getNDG_NEQ(int t1, int t2, java.lang.Object o1, java.lang.Object o2)	Creates a non-degenerate inequality constraint based on two point identifiers and associated objects.
Cons	getNDG_NON_ISOTROPIC(int t1, int t2, java.lang.Object o1, java.lang.Object o2)	Creates a non-degenerate non-isotropic constraint from two point identifiers and their associated objects.
Cons	getNDG_PARA(int t1, int t2, int t3, int t4, java.lang.Object o1, java.lang.Object o2, java.lang.Object o3, java.lang.Object o4)	Creates a non-degenerate parallel constraint from the provided points and associated objects.
Cons	getNDG_PERP(int t1, int t2, int t3, int t4, java.lang.Object o1, java.lang.Object o2, java.lang.Object o3, java.lang.Object o4)	Creates a non-degenerate perpendicular constraint based on the provided points and associated objects.
Cons	getPcons(int x)	Retrieves a construction constraint based on its 1-based index.
int	getPointsNum()	Returns the number of points in the construction.
ProPoint	getProPoint(int x)	Retrieves a point based on its 1-based index.
java.lang.String	getPtName(int x)	Retrieves the name of a point based on its 1-based index.
boolean	hasConclusion()	Checks if a valid conclusion exists in the construction.
boolean	isFreePoint(int n)	Determines whether the point identified by the given index is free.
boolean	isPositionSet()	Checks if the positions of points have been set.
boolean	isTermAnimated()	Determines if the term is animated based on the animation string.
boolean	NDG_Contains(Cons c, Cons c1)	Checks if the first non-degenerate constraint is considered contained within the second.
java.util.Vector	pc()	Processes and returns a vector of processed constraints.
boolean	readAterm(java.io.BufferedReader in)	Reads an A-term from the provided BufferedReader.
boolean	readAterm(java.io.DataInputStream in)	Reads an A-term from the given DataInputStream.
boolean	readAterm2(java.io.DataInputStream in)	Reads an A-term from the provided DataInputStream while ignoring header lines.
int	setAllcons(Cons[] cn)	Copies all constraints into the given array, starting at index 1.
int	setAllpts(ProPoint[] pp)	Copies all points into the given array, starting at index 1.
boolean	setConclusion(Cons c)	Sets the conclusion constraint and updates the underlying condition.
void	setConclusionNo()	Sets the conclusion number.
void	setName(java.lang.String s)	Sets the name for the construction.
boolean	setPtLoc(java.lang.String sn, double x, double y, int x1, int y1)	Sets the location for the point matching the given name.
java.lang.String	toString()	Returns a string representation of the construction.
boolean	writeAterm(java.io.FileOutputStream out)	Writes the current A-term to the specified FileOutputStream.
boolean	writeAterm2(java.io.DataOutputStream out)	Writes the current A-term to the provided DataOutputStream using an alternative format.

Methods inherited from class java.lang.Object

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

Field Detail

conc

public Cond conc

Constructor Detail

GTerm

public GTerm()

Constructs a new GTerm instance.

Method Detail

getCons

public Cons getCons(int n)

Returns the constraint at the specified index from the constraint vector.

Parameters:

n - the 0-based index of the constraint to retrieve

Returns:

the constraint at index n, or null if n is out of range

getNcons

public java.util.Vector getNcons()

Returns a vector containing non degenerate constraints.

Returns:

a vector of CNdg objects representing non degenerate constraints

generateSd

public void generateSd(CNdg dg,
                       java.lang.Object[] pss)

Generates a string description for the specified CNdg object based on the provided parameters.

Parameters:

dg - the CNdg object to update with its description

pss - the array of parameters used for generating the description

getCons

public java.util.Vector getCons()

Returns the vector containing all constraints.

Returns:

the vector of constraint objects

setAllcons

public int setAllcons(Cons[] cn)

Copies all constraints into the given array, starting at index 1.

Parameters:

cn - the array in which to store the constraint objects

Returns:

the number of constraints copied

setAllpts

public int setAllpts(ProPoint[] pp)

Copies all points into the given array, starting at index 1.

Parameters:

pp - the array in which to store the point objects

Returns:

the number of points copied

getPointsNum

public int getPointsNum()

Returns the number of points in the construction.

Returns:

the number of points

getAllptsText

public java.util.Vector getAllptsText()

Returns a vector containing the names of all points.

Returns:

a vector of point names

getCons_no

public int getCons_no()

Returns the number of constraints (as derived from the points vector).

Returns:

the number of constraints

getConc

public Cond getConc()

Returns the current conclusion condition.

Returns:

the Cond object representing the conclusion

getConclusion

public Cons getConclusion()

Retrieves the conclusion constraint if it exists.

Returns:

the conclusion constraint, or null if none exists

setConclusion

public boolean setConclusion(Cons c)

Sets the conclusion constraint and updates the underlying condition.

Parameters:

c - the conclusion constraint to set

Returns:

true if the conclusion was set successfully, false otherwise

getName

public java.lang.String getName()

Returns the name of the construction.

Returns:

the construction name

setName

public void setName(java.lang.String s)

Sets the name for the construction.

Parameters:

s - the name to set

readAterm

public boolean readAterm(java.io.BufferedReader in)
                  throws java.io.IOException

Reads an A-term from the provided BufferedReader.

Parameters:

in - the BufferedReader to read from

Returns:

true if the term is successfully read; false otherwise

Throws:

java.io.IOException - if an I/O error occurs

writeAterm

public boolean writeAterm(java.io.FileOutputStream out)
                   throws java.io.IOException

Writes the current A-term to the specified FileOutputStream.

Parameters:

out - the FileOutputStream to write to

Returns:

true if the A-term is successfully written; false otherwise

Throws:

java.io.IOException - if an I/O error occurs

readAterm

public boolean readAterm(java.io.DataInputStream in)
                  throws java.io.IOException

Reads an A-term from the given DataInputStream.

Parameters:

in - the DataInputStream to read from

Returns:

true if the A-term is successfully read; false otherwise

Throws:

java.io.IOException - if an I/O error occurs

writeAterm2

public boolean writeAterm2(java.io.DataOutputStream out)
                    throws java.io.IOException

Writes the current A-term to the provided DataOutputStream using an alternative format.

Parameters:

out - the DataOutputStream to write to

Returns:

true if the A-term is successfully written; false otherwise

Throws:

java.io.IOException - if an I/O error occurs

add_pt

public boolean add_pt(java.lang.String s)

Adds a new point with the specified name if it does not already exist.

Parameters:

s - the name of the point to add

Returns:

false if the point already exists, otherwise false after adding the point

setPtLoc

public boolean setPtLoc(java.lang.String sn,
                        double x,
                        double y,
                        int x1,
                        int y1)

Sets the location for the point matching the given name.

Parameters:

sn - the name of the point

x - the x-coordinate of the point

y - the y-coordinate of the point

x1 - the first additional coordinate parameter

y1 - the second additional coordinate parameter

Returns:

true if the point location is successfully set; false otherwise

readAterm2

public boolean readAterm2(java.io.DataInputStream in)
                   throws java.io.IOException

Reads an A-term from the provided DataInputStream while ignoring header lines.

Parameters:

in - the DataInputStream to read from

Returns:

true if the A-term is successfully read; false otherwise

Throws:

java.io.IOException - if an I/O error occurs

clear

public void clear()

Clears all stored points, construction steps, and resets the construction name.

addConsV

public void addConsV(java.util.Vector v)

Clears current construction data and sets constraints from the given vector.

Parameters:

v - the vector containing new constraints

generate

public boolean generate(java.util.Vector glines)

Generates the construction based on the provided vector of input lines.

Parameters:

glines - the vector containing construction lines

Returns:

true if the generation is successful; false otherwise

addauxedPoint

public void addauxedPoint(ProPoint pt)

Adds an auxiliary point to the construction.

Parameters:

pt - the point to be added.

addauxedCons

public void addauxedCons(Cons c)

Adds an auxiliary constraint to the construction. Inserts the constraint appropriately depending on whether a conclusion exists.

Parameters:

c - the constraint to be added.

getconsNum

public int getconsNum()

Returns the number of constructions excluding the final conclusion if present.

Returns:

the count of constructions.

isTermAnimated

public boolean isTermAnimated()

Determines if the term is animated based on the animation string.

Returns:

true if the term is animated, false otherwise.

getAnimateString

public java.lang.String getAnimateString()

Retrieves the animation string for the term.

Returns:

the animation string.

isPositionSet

public boolean isPositionSet()

Checks if the positions of points have been set.

Returns:

true if positions are set, false otherwise.

addInterLS

public void addInterLS(java.lang.String[] list)

Processes an inter-line constraint. Adds a circumcenter point if required before creating the constraint.

Parameters:

list - the array of parameters representing the constraint.

addInterSS

public void addInterSS(java.lang.String[] list)

Processes an inter-segment constraint. Adds circumcenter points if needed before creating the constraint.

Parameters:

list - the array of parameters representing the constraint.

addConstant

public void addConstant(java.lang.String sf,
                        java.lang.String func)

Adds a constant to the construction. Creates a new constant constraint using the provided identifier and function.

Parameters:

sf - the identifier for the constant.

func - the function defining the constant.

getProPoint

public ProPoint getProPoint(int x)

Retrieves a point based on its 1-based index.

Parameters:

x - the 1-based index of the point.

Returns:

the corresponding ProPoint, or null if the index is out of bounds.

getPcons

public Cons getPcons(int x)

Retrieves a construction constraint based on its 1-based index.

Parameters:

x - the 1-based index of the constraint.

Returns:

the corresponding Cons object, or null if the index is out of bounds.

getPtName

public java.lang.String getPtName(int x)

Retrieves the name of a point based on its 1-based index.

Parameters:

x - the 1-based index of the point.

Returns:

the point name, or an empty string if the index is invalid.

ge_cpt

public void ge_cpt()

Recalculates and updates constraint point indexes and conclusion values.

fd_pt

protected ProPoint fd_pt(java.lang.String sn)

Retrieves a point with the specified name from the list.

Parameters:

sn - the name of the point to retrieve

Returns:

the ProPoint if found; null otherwise

ge_pss2ps

public void ge_pss2ps(Cons c)

Converts the string parameters of the given constraint to point indexes.

Parameters:

c - the constraint to process

addNdg

public void addNdg(Cons c)

Updates and adds a non-degenerate constraint if it is not already present.

Parameters:

c - the constraint to add

getConcText

public java.lang.String getConcText()

Retrieves the text representation of the current conclusion.

Returns:

the conclusion text, or "NO" if no conclusion is set

setConclusionNo

public void setConclusionNo()

Sets the conclusion number.

hasConclusion

public boolean hasConclusion()

Checks if a valid conclusion exists in the construction.

Returns:

true if the last condition type is within the valid range (>= 50 and < 100); false otherwise.

isFreePoint

public boolean isFreePoint(int n)

Determines whether the point identified by the given index is free.

Parameters:

n - the 1-based index of the point to check.

Returns:

true if the point is not used as the last element in any constraint; false otherwise.

toString

public java.lang.String toString()

Returns a string representation of the construction.

Overrides:

toString in class java.lang.Object

Returns:

the name of the construction if available; otherwise, the default string representation.

pc

public java.util.Vector pc()

Processes and returns a vector of processed constraints.

Returns:

a vector containing the processed constraints.

getAllCircles

public void getAllCircles()

Aggregates and computes all circle constraints from the current constraint data.

addccc

public void addccc(int a,
                   int b,
                   Cons cs)

Adds a circle constraint between the two specified points to the provided constraint, if the connection does not already exist.

Parameters:

a - the first point index.

b - the second point index.

cs - the constraint to which the circle condition is added.

add_preq

public void add_preq(int t,
                     int[] p)

Adds prerequisite equality constraints based on the given type and associated points.

Parameters:

t - the constraint type.

p - an array of point indices representing the constraint.

add_eqcons

public void add_eqcons(int a,
                       int b,
                       int c,
                       int d)

Adds an equality constraint equating the distances between the two pairs of points.

Parameters:

a - the first point index of the first pair.

b - the second point index of the first pair.

c - the first point index of the second pair.

d - the second point index of the second pair.

getcons

public Cons getcons(int pt,
                    java.util.Vector v)

Retrieves and removes the first constraint in the vector that contains the specified point.

Parameters:

pt - the point identifier to search for in the constraints.

v - the vector of constraints to search through.

Returns:

the constraint that contains the point, or null if no such constraint exists.

getAllNdgs

public java.util.Vector getAllNdgs(java.util.Vector v)

Generates all non-degenerate constraints from the given vector.

Parameters:

v - the vector of constraints from which to generate non-degenerate constraints.

Returns:

a vector containing all non-degenerate constraints.

generateCons

public void generateCons(Cons c,
                         java.util.Vector v)

Generates non-degenerate constraints based on the specified constraint and adds them to the provided vector.

Parameters:

c - the original constraint used as a basis for generating non-degenerate constraints.

v - the vector to which the generated constraints will be added.

getNDG_PARA

public Cons getNDG_PARA(int t1,
                        int t2,
                        int t3,
                        int t4,
                        java.lang.Object o1,
                        java.lang.Object o2,
                        java.lang.Object o3,
                        java.lang.Object o4)

Creates a non-degenerate parallel constraint from the provided points and associated objects.

Parameters:

t1 - the first point identifier.

t2 - the second point identifier.

t3 - the third point identifier.

t4 - the fourth point identifier.

o1 - the first associated object.

o2 - the second associated object.

o3 - the third associated object.

o4 - the fourth associated object.

Returns:

a Cons object representing the non-degenerate parallel constraint, or null if conditions are not met.

getNDG_PERP

public Cons getNDG_PERP(int t1,
                        int t2,
                        int t3,
                        int t4,
                        java.lang.Object o1,
                        java.lang.Object o2,
                        java.lang.Object o3,
                        java.lang.Object o4)

Creates a non-degenerate perpendicular constraint based on the provided points and associated objects.

Parameters:

t1 - the first point identifier.

t2 - the second point identifier.

t3 - the third point identifier.

t4 - the fourth point identifier.

o1 - the first associated object.

o2 - the second associated object.

o3 - the third associated object.

o4 - the fourth associated object.

Returns:

a Cons object representing the non-degenerate perpendicular constraint.

getNDG_COLL

public Cons getNDG_COLL(int t1,
                        int t2,
                        int t3,
                        java.lang.Object o1,
                        java.lang.Object o2,
                        java.lang.Object o3)

Creates a non-degenerate collinearity constraint from the given point identifiers and associated objects.

Parameters:

t1 - the first point identifier.

t2 - the second point identifier.

t3 - the third point identifier.

o1 - the first associated object.

o2 - the second associated object.

o3 - the third associated object.

Returns:

a Cons object representing the non-degenerate collinearity constraint, or null if any two points are equal.

getNDG_NON_ISOTROPIC

public Cons getNDG_NON_ISOTROPIC(int t1,
                                 int t2,
                                 java.lang.Object o1,
                                 java.lang.Object o2)

Creates a non-degenerate non-isotropic constraint from two point identifiers and their associated objects.

Parameters:

t1 - the first point identifier.

t2 - the second point identifier.

o1 - the first associated object.

o2 - the second associated object.

Returns:

a Cons object representing the non-degenerate non-isotropic constraint.

getNDG_NEQ

public Cons getNDG_NEQ(int t1,
                       int t2,
                       java.lang.Object o1,
                       java.lang.Object o2)

Creates a non-degenerate inequality constraint based on two point identifiers and associated objects.

Parameters:

t1 - the first point identifier.

t2 - the second point identifier.

o1 - the first associated object.

o2 - the second associated object.

Returns:

a Cons object representing the non-degenerate inequality constraint.

addNDG

public void addNDG(Cons c,
                   java.util.Vector v)

Adds a non-degenerate constraint to the specified vector. If a similar constraint exists, it avoids duplication or replaces the existing one.

Parameters:

c - the non-degenerate constraint to add.

v - the vector in which the constraint is to be added.

NDG_Contains

public boolean NDG_Contains(Cons c,
                            Cons c1)

Checks if the first non-degenerate constraint is considered contained within the second.

Parameters:

c - the constraint to check for containment.

c1 - the constraint that may contain the first.

Returns:

true if the first constraint is contained within the second, false otherwise.