Package gprover

Class Full

  • Direct Known Subclasses:
    Area
    public class Full
extends Elim
    Implements full angle proof processes and geometric elimination.

    • Constructor Detail

      • Full

        public Full()
        Constructs a new Full object.

    • Method Detail

      • getErrorType

        public int getErrorType()
        Returns the error type encountered during proof processing.
        Returns:
        the error type code.

      • fconc_coll

        public void fconc_coll​(int a,
                       int b,
                       int c)
        Processes the collinearity condition for full angle concatenation.
        Parameters:
        a - first geometric parameter.
        b - second geometric parameter.
        c - third geometric parameter.

      • fconc_cong

        public boolean fconc_cong​(int a,
                          int b,
                          int c,
                          int d)
        Processes the congruence condition for full angle concatenation.
        Parameters:
        a - first geometric parameter.
        b - second geometric parameter.
        c - third geometric parameter.
        d - fourth geometric parameter.
        Returns:
        true if the congruence condition was successfully processed; false otherwise.

      • canExpressedAsFullAngle

        public boolean canExpressedAsFullAngle()
        Returns true if a full angle proof is expressed.
        Returns:
        true if the full angle proof head exists, false otherwise.

      • isProvedTrue

        public boolean isProvedTrue()
        Determines if the proof has been established as true.
        Returns:
        true if last_pr is non-null and equals zero, false otherwise.

      • getFullAngleProofHead

        public GrTerm getFullAngleProofHead()
        Retrieves the head of the full angle proof. This method iterates through the proof elements while printing intermediate proof components. It processes both primary and linked elimination terms.
        Returns:
        the first element in the full angle proof chain, or null if none exists.

      • print_prooftext

        public boolean print_prooftext()
        Prints the proof text. This method iterates through all proof terms and prints their associated elimination information. It assembles the printed proof text by processing both display and elimination terms.
        Returns:
        true if proof text printing succeeds, false otherwise.

      • myprint_p1

        public void myprint_p1​(XTerm p1,
                       boolean first)
        Prints an XTerm (mathematical expression) with its variable and coefficient.

        Constant terms without an associated variable are printed in an angle-signed format. For non-constant terms, the method processes the polynomial parts recursively.

        Parameters:
        p1 - the XTerm to be printed
        first - true if this is the first term (affects sign formatting), false otherwise

      • set_showdetai

        public static void set_showdetai​(boolean d)
        Sets the flag to show details.

        This static method controls whether detailed information should be displayed.

        Parameters:
        d - the boolean value to set for showing details

      • isConstructionType

        public boolean isConstructionType​(int type)
        Determines if a given type represents a valid construction.

        The type is considered valid if it falls within specific ranges and does not require freeCS.

        Parameters:
        type - the construction type to check
        Returns:
        true if the type is a construction type; false otherwise

      • get_ndgs

        public void get_ndgs​(java.util.Vector v1,
                     java.util.Vector v2,
                     java.util.Vector v3,
                     java.util.Vector v4)
        Populates the provided vectors with non-degenerate geometry constraints (NDGs) from constructions.

        This method iterates through constructions, adds valid constructions to the first vector, initializes and filters NDGs, deduces additional constraints, and finally updates the provided vectors.

        Parameters:
        v1 - a vector for constructions used as NDG constraints
        v2 - a vector for initial NDGs
        v3 - a vector for filtered NDGs
        v4 - a vector for deduced NDGs

      • add_n_isotropic

        protected CNdg add_n_isotropic​(int a,
                               int b,
                               java.util.Vector v1)
        Creates and adds a non-isotropic NDG constraint based on two points.

        This method checks that the points are different and valid. It creates a new CNdg for non-isotropic constraints and adds it to the provided vector.

        Parameters:
        a - the first point
        b - the second point
        v1 - the vector to which the NDG is added
        Returns:
        the created CNdg object, or null if the points are identical or invalid

      • add_n_pt

        protected CNdg add_n_pt​(int type,
                        int a,
                        int b,
                        int c,
                        int d,
                        java.util.Vector v1)
        Creates and adds an NDG constraint representing parallelism or perpendicularity.

        This method reorders four points if needed and creates a corresponding NDG depending on the specified type. The resulting constraint is then added to the vector.

        Parameters:
        type - the type of NDG (e.g. NDG_PARA for parallel or NDG_PERP for perpendicular)
        a - the first point of the first line
        b - the second point of the first line
        c - the first point of the second line
        d - the second point of the second line
        v1 - the vector to which the NDG is added
        Returns:
        the created CNdg object

      • add_n_coll

        protected CNdg add_n_coll​(int a,
                          int b,
                          int c,
                          java.util.Vector v1)
        Creates and adds a collinearity NDG constraint based on three points.

        This method reorders the three points to ensure a proper order for establishing collinearity, then creates a new CNdg representing the collinearity constraint and adds it to the given vector.

        Parameters:
        a - the first point
        b - the second point
        c - the third point
        v1 - the vector to which the NDG is added
        Returns:
        the created CNdg object

      • init_ndgs

        public void init_ndgs​(java.util.Vector v1)
        Initializes non-degenerate geometry constraints (NDGs) from existing constructions.

        This method iterates through all constructions, creates appropriate NDG constraints based on the type of each construction, and associates dependencies with the NDGs when modifications occur.

        Parameters:
        v1 - the vector to be populated with NDG constraints

      • add_n_neq

        public void add_n_neq​(int a,
                      int b,
                      java.util.Vector v1)
        Adds a non-equality NDG constraint for the given points.

        This method creates an NDG constraint of type NDG_NEQ (or equivalent) for points a and b, then adds it to the provided vector.

        Parameters:
        a - the first point index
        b - the second point index
        v1 - the vector to add the NDG constraint

      • add_coll_para

        public void add_coll_para​(Cons cs,
                          java.util.Vector v1)
        Creates and adds a collinearity constraint in parallel form based on a construction.

        This method determines the highest point value from the construction's point array, then selects the three remaining points to build a collinearity NDG constraint and adds it to vector v1.

        Parameters:
        cs - the construction containing the points
        v1 - the vector to add the NDG constraint

      • angle_deduction

        public void angle_deduction​(CNdg c,
                            java.util.Vector v4)
        Deduces angle-based NDG constraints and processes them.

        This method handles a given CNdg constraint by checking if all associated points are free. If so, it directly duplicates the constraint into vector v4; otherwise, it computes an XTerm deduction based on the NDG type and adds related non-equality constraints.

        Parameters:
        c - the CNdg constraint to analyze
        v4 - the vector in which the deduced NDG constraints are stored

      • add_neqTo

        protected void add_neqTo​(int a,
                         int b,
                         java.util.Vector v4)
        Checks and adds a non-equality constraint between two points if not already present.

        This method iterates over the vector v4 to determine if an equivalent NDG constraint exists. If none is found, a new NDG constraint (NDG_NEQ) for the pair of points is created and added.

        Parameters:
        a - the first point index
        b - the second point index
        v4 - the vector containing NDG constraints

      • ck_allFree

        protected boolean ck_allFree​(CNdg d)
        Checks whether all points in the given CNdg constraint are free.

        This method iterates over the points associated with the constraint and calls freeCSP for each one. It returns false as soon as any point is not free.

        Parameters:
        d - the CNdg constraint to check
        Returns:
        true if all points are free; false otherwise

      • add_deduction

        protected XTerm add_deduction​(XTerm x)
        Performs angle deduction on the given XTerm.

        If the XTerm has an associated variable, angle-based deduction is applied followed by a final deduction adjustment.

        Parameters:
        x - the XTerm to deduct
        Returns:
        the resulting XTerm after deduction

      • final_deduction

        protected XTerm final_deduction​(XTerm p1)
        Applies a final deduction adjustment to an XTerm.

        If the factor computed by fcc is negative, the XTerm is multiplied by -1.

        Parameters:
        p1 - the XTerm to adjust
        Returns:
        the adjusted XTerm

      • filter_ndg

        protected void filter_ndg​(java.util.Vector v4)
        Filters out redundant NDG constraints in the given vector.

        This method compares each NDG constraint in the vector with the others and removes any that are equal or less significant than another constraint.

        Parameters:
        v4 - the vector containing NDG constraints to filter

      • filter_ndg

        protected void filter_ndg​(java.util.Vector v2,
                          java.util.Vector v3)
        Filters and merges NDG constraints from vector v2 into vector v3.

        This method iterates over the constraints in v2 and checks against those in v3. If an equivalent or less significant constraint exists, it merges or sets an equivalence link.

        Parameters:
        v2 - the source vector of NDG constraints
        v3 - the target vector for filtered NDG constraints

      • add_ndgs

        protected void add_ndgs​(CNdg d,
                        java.util.Vector vlist)
        Adds an NDG constraint to the specified vector.

        This helper method ensures the NDG constraint is valid (non-null), initializes its string representation by calling get_ndgstr, and then adds it to the vector.

        Parameters:
        d - the NDG constraint to add
        vlist - the vector where the NDG constraint is stored

      • ndg_less

        protected boolean ndg_less​(CNdg n1,
                           CNdg n2)
        Compares two NDG constraints to determine if the first is less significant than the second.

        For non-equality NDGs, if the second constraint is of type NDG_COLL and contains both points of the first constraint, the first is considered less significant.

        Parameters:
        n1 - the first NDG constraint
        n2 - the second NDG constraint
        Returns:
        true if n1 is less significant than n2; false otherwise

      • ndg_eq

        protected boolean ndg_eq​(CNdg n1,
                         CNdg n2)
        Checks whether two NDG constraints are equal.

        This method first compares their types (allowing for NDG_NEQ and NDG_NON_ISOTROPIC to be equivalent), then verifies that the number of points and the point values are identical.

        Parameters:
        n1 - the first NDG constraint
        n2 - the second NDG constraint
        Returns:
        true if the two constraints are equal; false otherwise

      • addxtermndg

        protected void addxtermndg​(XTerm x,
                           java.util.Vector v4)
        Converts an XTerm into an NDG constraint and adds its printed representation.

        This method first converts the XTerm into a corresponding NDG constraint via xterm2ndg, then updates its string representation using the printing methods.

        Parameters:
        x - the XTerm to convert and add
        v4 - the vector where the NDG information is stored

      • xterm2ndg

        protected void xterm2ndg​(XTerm x,
                         java.util.Vector vlist)
        Converts an XTerm into NDG constraints and adds them to the provided list.

        Depending on the term number of the XTerm, the method delegates to a helper method to generate the appropriate NDG constraints.

        Parameters:
        x - the XTerm to convert
        vlist - the vector where the generated NDG constraints will be added

      • xterm_1term

        protected void xterm_1term​(XTerm x,
                           java.util.Vector vlist)
        Processes an XTerm with one term to generate NDG constraints.

        The method examines the factor computed by fcc(x) and based on its value, creates and adds NDG constraints using parallel, perpendicular, or triple PI rules.

        Parameters:
        x - the XTerm to process
        vlist - the vector where the generated NDG constraints will be added

      • add_ndg_triplePI

        protected CNdg add_ndg_triplePI​(Var v)
        Creates a Triple PI NDG constraint from the specified variable.

        It initializes the NDG using the points from the variable and reorders them, setting the number of points to 3.

        Parameters:
        v - the variable containing the points for the NDG constraint
        Returns:
        the constructed Triple PI NDG constraint

      • xterm_2term

        protected void xterm_2term​(XTerm x,
                           java.util.Vector vlist)
        Processes an XTerm with two terms to generate NDG constraints.

        The method examines the second term of the XTerm and creates congruency or collinearity NDGs based on the sign of the factor computed by fcc for the second term.

        Parameters:
        x - the XTerm to process
        vlist - the vector where the generated NDG constraints will be added

      • reorder3

        protected void reorder3​(CNdg n)
        Reorders the points in an NDG constraint (with three points) into ascending order.
        Parameters:
        n - the NDG constraint whose points are to be reordered

      • reorder22

        protected void reorder22​(CNdg n)
        Reorders two pairs of points in an NDG constraint so that each pair is in ascending order.

        In addition, it ensures that the first pair is sorted relative to the second pair.

        Parameters:
        n - the NDG constraint whose points are to be reordered

      • add_ndg_neq

        protected CNdg add_ndg_neq​(int a,
                           int b)
        Creates a non-equality NDG constraint for two points.

        Returns null if both points are identical.

        Parameters:
        a - the first point index
        b - the second point index
        Returns:
        the NDG non-equality constraint, or null if the points are identical

      • freeCSP

        public boolean freeCSP​(int index)
        Checks whether the point at the given index is free from constraints.

        It retrieves the associated point object and checks its construction type.

        Parameters:
        index - the index of the point to check
        Returns:
        true if the point is free; false otherwise

      • freeCS

        public boolean freeCS​(int t)
        Determines if the given construction type represents a free state.

        A type is considered free if it matches one of the basic construction types.

        Parameters:
        t - the construction type to check
        Returns:
        true if the type is free; false otherwise

      • add_ndg_coll

        protected CNdg add_ndg_coll​(int a,
                            int b,
                            int c)
        Creates a collinearity NDG constraint from three points.

        The points are reordered to ensure proper ordering. If redundant, then null is returned.

        Parameters:
        a - the first point index
        b - the second point index
        c - the third point index
        Returns:
        the NDG collinearity constraint, or null if the points are redundant

      • add_ndg_cong

        protected CNdg add_ndg_cong​(int a,
                            int b,
                            int c,
                            int d)
        Creates a congruency NDG constraint based on four points.

        The points are reordered; if the set of points is redundant, null is returned.

        Parameters:
        a - the first point index of the first segment
        b - the second point index of the first segment
        c - the first point index of the second segment
        d - the second point index of the second segment
        Returns:
        the NDG congruency constraint, or null if the points are redundant

      • add_ndg_para

        protected CNdg add_ndg_para​(Var v)
        Creates a parallel NDG constraint using the points of a given variable.
        Parameters:
        v - the variable containing the points for the constraint
        Returns:
        the NDG parallel constraint

      • add_ndg_para

        protected CNdg add_ndg_para​(int a,
                            int b,
                            int c,
                            int d)
        Creates a parallel NDG constraint based on four point indices.

        The points are reordered to ascending order; if the set is redundant, an alternative collinearity constraint is constructed instead.

        Parameters:
        a - the first point index of the first segment
        b - the second point index of the first segment
        c - the first point index of the second segment
        d - the second point index of the second segment
        Returns:
        the NDG parallel constraint, or an alternative NDG constraint if redundant

      • add_ndg_perp

        protected CNdg add_ndg_perp​(Var v)
        Creates a perpendicular NDG constraint using the points of a given variable.
        Parameters:
        v - the variable containing the points for the constraint
        Returns:
        the NDG perpendicular constraint

      • add_ndg_perp

        protected CNdg add_ndg_perp​(int a,
                            int b,
                            int c,
                            int d)
        Creates a perpendicular NDG constraint based on four point indices.

        If the two segments are identical, a non-isotropic NDG constraint is created instead.

        Parameters:
        a - the first point index of the first segment
        b - the second point index of the first segment
        c - the first point index of the second segment
        d - the second point index of the second segment
        Returns:
        the NDG perpendicular constraint, or a non-isotropic constraint when applicable

      • get_ndgstr

        protected void get_ndgstr​(CNdg d)
        Sets the string representation (sd) of the given NDG constraint (d) based on its type and associated points. Depending on the type, constructs a descriptive message.
        Parameters:
        d - the NDG constraint for which the string representation is set

      • angle_deduction

        protected XTerm angle_deduction​(XTerm p1)
        Performs angle deduction on the given XTerm. This method initializes necessary properties and iteratively attempts to eliminate terms using various elimination methods. At the end, it optimizes the term based on triangle configurations.
        Parameters:
        p1 - the XTerm on which angle deduction is performed
        Returns:
        the resulting XTerm after angle deduction

      • opt_tri

        public XTerm opt_tri​(XTerm x)
        Optimizes the given XTerm by detecting and processing triangle configurations. It compares factors from the current term and its subterm to determine if any adjustment such as scaling or subtraction should be applied.
        Parameters:
        x - the XTerm to be optimized
        Returns:
        the optimized XTerm

      • ndg_deduction

        public void ndg_deduction​(java.util.Vector v3,
                          java.util.Vector v4)
        Performs NDG (non-degeneracy) deduction on a set of NDG constraints. For each constraint in the source vector v3, if the constraint is marked as existing or if all its points are free, it is directly added or duplicated into the target vector v4. Otherwise, angle deduction is applied.
        Parameters:
        v3 - the source vector of NDG constraints
        v4 - the target vector to store the deduced NDG constraints

      • compare

        public int compare​(CNdg d1,
                   CNdg d2)
        Compares two NDG constraints based on their maximum integer values.
        Parameters:
        d1 - the first NDG constraint
        d2 - the second NDG constraint
        Returns:
        a positive value if d1 > d2, a negative value if d1 < d2, or zero if they are equal

      • sortVector

        public void sortVector​(java.util.Vector v4)
        Sorts a vector of NDG constraints in ascending order based on their significance. It uses the compare method to insert each constraint into its correct position in the vector.
        Parameters:
        v4 - the vector containing NDG constraints to be sorted

      • parse_neq

        public void parse_neq​(java.util.Vector v4)
        Parses non-equality and non-isotropic NDG constraints from the given vector.

        This method sorts the input vector of NDG constraints, filters out those constraints that are non-equality (NDG_NEQ) or non-isotropic (NDG_NON_ISOTROPIC) and have both points free, and then processes the remaining constraints. The remaining constraints are added to a global NDG list after being updated.

        Parameters:
        v4 - the vector containing NDG constraints to be parsed

      • getCS

        public NdgCs getCS​(CNdg d)
        Constructs and returns an NDG constraint set (NdgCs) associated with the given inequality constraint.

        The method iterates through existing constraints and gathers those related to the points of the provided constraint. The collected constraints are then added to a new NdgCs structure and updated.

        Parameters:
        d - the NDG inequality constraint used as a basis for gathering related constraints
        Returns:
        the constructed NDG constraint set (NdgCs)

      • addConsToNdgcs

        public void addConsToNdgcs​(Cons c,
                           NdgCs d)
        Adds the provided constraint to the given NDG constraint set.

        Based on the type of the constraint, it may clone the constraint or generate additional constraints.

        Parameters:
        c - the constraint to be added
        d - the NDG constraint set (NdgCs) that will include the constraint

      • add_cons

        public void add_cons​(int type,
                     int a,
                     int b,
                     int c,
                     int d,
                     int e,
                     int f,
                     int g,
                     NdgCs d1)
        Creates a new constraint with 7 points and adds it to the specified NDG constraint set.
        Parameters:
        type - the type of the new constraint
        a - the first point index
        b - the second point index
        c - the third point index
        d - the fourth point index
        e - the fifth point index
        f - the sixth point index
        g - the seventh point index
        d1 - the NDG constraint set (NdgCs) where the new constraint will be added

      • add_cons

        public void add_cons​(int type,
                     int a,
                     int b,
                     int c,
                     int d,
                     NdgCs d1)
        Creates a new constraint with 4 points and adds it to the specified NDG constraint set.
        Parameters:
        type - the type of the new constraint
        a - the first point index
        b - the second point index
        c - the third point index
        d - the fourth point index
        d1 - the NDG constraint set (NdgCs) where the new constraint will be added

      • ck_right

        public boolean ck_right​(Cons c,
                        NdgCs cs,
                        int type)
        Checks whether the specified constraint is recursively valid with respect to the given NDG type.

        Depending on the type of the constraint, it recursively checks if related NDG constraints already exist.

        Parameters:
        c - the constraint to check
        cs - the NDG constraint set (NdgCs) in which the check is performed
        type - the NDG type against which the constraint is validated
        Returns:
        true if the constraint is valid; false otherwise

      • ck_right

        public boolean ck_right​(NdgCs c,
                        int type)
        Recursively checks constraints in an NDG constraint set for consistency. For leaf nodes, it verifies each constraint against its expected conditions; for non-leaf nodes, it cleans up inconsistent child sets.
        Parameters:
        c - the NDG constraint set to check
        type - the type identifier for the check; usage depends on the context
        Returns:
        true if the constraint set is consistent; false otherwise

      • parse_neq

        public NdgCs parse_neq​(CNdg nd)
        Parses non-equality and non-isotropic NDG constraints by replacing point indices, reordering constraints, and invoking further parsing, cleanup, and optimization steps.
        Parameters:
        nd - the NDG constraint to be parsed
        Returns:
        the updated NDG constraint set after parsing

      • construct_related

        public boolean construct_related​(int t)
        Determines whether a constraint type is considered related to construction operations.

        The method returns false for fundamental geometric element types (e.g., point, triangle, etc.) and for types within a specific range, indicating that additional construction steps are not required.

        Parameters:
        t - the constraint type identifier
        Returns:
        true if the constraint type is construction-related; false otherwise