Package gprover

Class GDD

  • Direct Known Subclasses:
    GDDAux

    public class GDD
    extends GDDBase
    A class representing the geometric deduction system.

    This class extends GDDBase and implements additional algorithms for geometric constructions, predicate validations, and search operations used in the deduction process.

    • Constructor Detail

      • GDD

        public GDD()
    • Method Detail

      • search_pn_cr

        public void search_pn_cr​(PLine pn)
        Searches for circle intersections within the provided PLine. Finds intersection points between each line in the PLine and the given circle.
        Parameters:
        pn - the PLine to search for circle intersections
      • mcoll

        public boolean mcoll​(int p1,
                             int p2,
                             int p3)
        Checks if three points are collinear.
        Parameters:
        p1 - the first point
        p2 - the second point
        p3 - the third point
        Returns:
        true if the points are collinear; false otherwise
      • mperp

        public boolean mperp​(int p1,
                             int p2,
                             int p3,
                             int p4)
        Checks if the line formed by p1 and p2 is perpendicular to the line formed by p3 and p4.
        Parameters:
        p1 - the first point of the first line
        p2 - the second point of the first line
        p3 - the first point of the second line
        p4 - the second point of the second line
        Returns:
        true if the lines are perpendicular; false otherwise
      • search_cg_ct

        public final void search_cg_ct​(int p1,
                                       int p2,
                                       int p3,
                                       int p4)
        Searches for congruent triangle configurations via side‑side‑side relationships.
        Parameters:
        p1 - the first point of the first segment
        p2 - the second point of the first segment
        p3 - the first point of the second segment
        p4 - the second point of the second segment
      • search_cg_aas

        public final void search_cg_aas​(int p1,
                                        int p2,
                                        int p3,
                                        int p4)
        Searches for congruent triangle configurations using angle‑angle‑side conditions.
        Parameters:
        p1 - the first point of the first segment
        p2 - the second point of the first segment
        p3 - the first point of the second segment
        p4 - the second point of the second segment
      • search_cg_ct0

        public final void search_cg_ct0​(int p1,
                                        int p2,
                                        int p3,
                                        int p4)
        Searches for congruent triangle configurations with trimmed conditions using SSS.
        Parameters:
        p1 - the first reference point
        p2 - the second reference point
        p3 - the third reference point
        p4 - the fourth reference point
      • search_as_ct

        public final void search_as_ct​(int p1,
                                       int p2,
                                       LLine ln1,
                                       LLine ln2,
                                       LLine ln3,
                                       LLine ln4)
        Searches for similar triangle configurations using corresponding line segments.
        Parameters:
        p1 - the reference point from the first triangle
        p2 - the reference point from the second triangle
        ln1 - the line data for the first triangle side
        ln2 - the line data for the second triangle side
        ln3 - the line data for the third triangle side
        ln4 - the line data for the alternative configuration side
      • search_tn_st

        public final void search_tn_st​(int p1,
                                       LLine ln1,
                                       LLine ln2,
                                       TLine tn1)
        Searches for T-line structures by testing intersections and perpendicular conditions.
        Parameters:
        p1 - the first reference point index
        ln1 - the first line of the primary structure
        ln2 - the second line of the primary structure
        tn1 - the candidate T-line structure
      • search_cg_md

        public final void search_cg_md​(int p1,
                                       int p2,
                                       int p3,
                                       int p4)
        Searches for congruent triangle configurations by finding midpoints and establishing congruency.
        Parameters:
        p1 - the first point index of the first segment
        p2 - the second point index of the first segment
        p3 - the first point index of the second segment
        p4 - the second point index of the second segment
      • search_cgs

        public void search_cgs​(CongSeg cg)
        Searches for congruent segment configurations within the current geometric construction.
        Parameters:
        cg - the congruent segment configuration to be evaluated
      • search_cg_cg

        public void search_cg_cg​(CongSeg cg,
                                 CongSeg cg1)
        Searches for congruent configurations between two congruent segment structures.
        Parameters:
        cg - the first congruent segment configuration
        cg1 - the second congruent segment configuration
      • search_cg__plus_or_minus

        public void search_cg__plus_or_minus​(int a,
                                             int b,
                                             int c,
                                             int d,
                                             int t1,
                                             int t2,
                                             int a1,
                                             int b1,
                                             int c1,
                                             int d1,
                                             int t11,
                                             int t22)
        Searches for congruent configurations using plus or minus criteria for segment measures.
        Parameters:
        a - first point of the first segment
        b - second point of the first segment
        c - first point of the second segment
        d - second point of the second segment
        t1 - first measure associated with the first segment
        t2 - second measure associated with the first segment
        a1 - first point of the alternative segment configuration
        b1 - second point of the alternative segment configuration
        c1 - first point of the alternative segment configuration
        d1 - second point of the alternative segment configuration
        t11 - first measure associated with the alternative configuration
        t22 - second measure associated with the alternative configuration
      • search_2cong1

        public void search_2cong1​(CongSeg cg)
        Searches for configurations where two congruent segments share a common intersection.
        Parameters:
        cg - the congruent segment configuration to analyze
      • search_md_cong

        public final void search_md_cong​(MidPt md)
        Searches for congruent configurations based on midpoint relationships.
        Parameters:
        md - the midpoint structure used for establishing congruence
      • search_pn_pn

        public void search_pn_pn​(PLine pn)
        Searches for parallelogram configurations among point-line relationships.
        Parameters:
        pn - the candidate point-line configuration
      • search_as_st

        public final void search_as_st​(int p1,
                                       int p2,
                                       LLine ln1,
                                       LLine ln2,
                                       LLine ln3,
                                       LLine ln4)
        Searches for SAS (Side-Angle-Side) triangle configurations using the specified points and line segments.
        Parameters:
        p1 - the first point identifier
        p2 - the second point identifier
        ln1 - the first line segment container
        ln2 - the second line segment container
        ln3 - the third line segment container
        ln4 - the fourth line segment container
      • search_cg_st0

        public final void search_cg_st0​(int p1,
                                        int p2,
                                        int p3,
                                        int p4,
                                        int r1,
                                        int r2)
        Searches for congruent segment triangle states based on the given points and ratio parameters.
        Parameters:
        p1 - the first point identifier
        p2 - the second point identifier
        p3 - the third point identifier
        p4 - the fourth point identifier
        r1 - the first ratio value
        r2 - the second ratio value
      • search_cong_st

        public void search_cong_st​(int t1,
                                   int t2,
                                   int t3,
                                   int t4,
                                   int t5,
                                   int t6,
                                   int r1,
                                   int r2)
        Searches for congruent triangles by validating angle equality and congruence conditions.
        Parameters:
        t1 - the first triangle base point identifier
        t2 - the second triangle base point identifier
        t3 - the third triangle base point identifier
        t4 - the first point of the second triangle
        t5 - the second point of the second triangle
        t6 - the third point of the second triangle
        r1 - the first ratio value associated with congruence
        r2 - the second ratio value associated with congruence
      • search_st1

        public void search_st1​(int dr,
                               int p1,
                               int p2,
                               int p3,
                               int p4,
                               int p5,
                               int p6)
        Searches for triangle configurations based on segment congruence and structural properties.
        Parameters:
        dr - the directional factor for the configuration
        p1 - the first point identifier of the triangle
        p2 - the second point identifier of the triangle
        p3 - the third point identifier of the triangle
        p4 - the first point identifier of the second triangle
        p5 - the second point identifier of the second triangle
        p6 - the third point identifier of the second triangle
      • add_stct_at

        public void add_stct_at​(int dr,
                                int p1,
                                int p2,
                                int p3,
                                int p4,
                                int p5,
                                int p6)
        Adds structural angle congruency information by comparing two complementary angles from the given points.
        Parameters:
        dr - the directional factor for angle assignment
        p1 - the vertex point of the first angle
        p2 - a point defining the first angle side
        p3 - a point defining the other side of the first angle
        p4 - the vertex point of the second angle
        p5 - a point defining the second angle side
        p6 - a point defining the other side of the second angle
      • adj_st

        public void adj_st​(SimTri st)
        Adjusts similar triangles by checking and adding structural relationships with adjacent triangles.
        Parameters:
        st - the simulated triangle whose adjacent configurations are to be adjusted
      • adj_ct

        public void adj_ct​(SimTri st)
        Adjusts complementary triangles by checking and generating new configurations for triangle relationships.
        Parameters:
        st - the simulated triangle whose complementary relationships are being adjusted
      • search_tn_cg

        public void search_tn_cg​(CongSeg cg)
        Searches for perpendicular congruent segments in a given congruent segment configuration.
        Parameters:
        cg - the congruent segment configuration to be analyzed
      • adj_as0

        public void adj_as0​(int p,
                            LLine l1,
                            LLine l2,
                            LLine l3,
                            LLine l4)
        Adjusts the angle subtraction configuration for the given point using four lines.
        Parameters:
        p - the reference point identifier
        l1 - the first line
        l2 - the second line
        l3 - the third line
        l4 - the fourth line
      • search_as_tn_as

        protected void search_as_tn_as​(int p1,
                                       int p2,
                                       LLine l1,
                                       LLine l2,
                                       LLine l3,
                                       LLine l4)
        Searches and verifies tangent-based angle relationships between two points using four lines.
        Parameters:
        p1 - the first point identifier
        p2 - the second point identifier
        l1 - the first line
        l2 - the second line
        l3 - the third line
        l4 - the fourth line
      • search_at

        public void search_at​(AngleT at)
        Initiates a comprehensive search for angle congruence relationships.
        Parameters:
        at - the angle to be processed
      • search_at_tn

        public void search_at_tn​(AngleT at)
        Searches for tangent-based angle configurations related to the specified angle.
        Parameters:
        at - the angle to be evaluated
      • search_tn_at

        public void search_tn_at​(TLine tn)
        Searches for angle relationships within a tangent line configuration.
        Parameters:
        tn - the tangent line configuration
      • search_tn_ats

        public void search_tn_ats​(LLine l1,
                                  LLine l2,
                                  int p,
                                  TLine tn)
        Searches for tangent angles across two lines with respect to a common intersection point and a tangent line.
        Parameters:
        l1 - the first line
        l2 - the second line
        p - the intersection point identifier
        tn - the tangent line configuration
      • add_tri_tn_at

        public void add_tri_tn_at​(int p,
                                  int p1,
                                  int p2,
                                  int v)
        Adds a triangle configuration based on tangent angle values.
        Parameters:
        p - the vertex point identifier
        p1 - the first adjacent point identifier
        p2 - the second adjacent point identifier
        v - the angle value between points p1 and p2
      • search_at0

        public void search_at0​(AngleT at)
        Searches for direct angle congruence relationships starting from the provided angle.
        Parameters:
        at - the angle to be searched
      • search_at1

        public void search_at1​(AngleT at)
        Searches for alternative angle configurations based on the given angle.
        Parameters:
        at - the angle instance to process
      • search_at_at

        public void search_at_at​(AngleT at,
                                 AngleT at1)
        Searches for angle relationships between two angle instances and creates corresponding configurations.
        Parameters:
        at - the first angle instance
        at1 - the second angle instance to compare
      • search_rg_at

        public void search_rg_at​(CongSeg cg)
        Searches for angle configurations derived from a congruent segment.
        Parameters:
        cg - the congruent segment instance used for calculating angle relationships
      • search_at_as

        public void search_at_as​(AngleT at,
                                 Angles as)
        Searches for angle configurations by comparing the given angle with an angle structure.
        Parameters:
        at - the base angle instance
        as - the angle structure to compare against
      • search_at_ass

        public void search_at_ass​(AngleT at)
        Searches for associated angle structures related to the given angle.
        Parameters:
        at - the angle instance for which to search related angle associations
      • adj_at

        public void adj_at​(AngleT at)
        Adjusts the angle configuration using its defining lines.
        Parameters:
        at - the angle instance to adjust
      • search_tn_atn

        public void search_tn_atn​(TLine tn)
        Searches for tangent-based angle configurations associated with the given tangent line.
        Parameters:
        tn - the tangent line configuration instance to search within
      • search_atn

        public void search_atn​(AngTn atn)
        Searches for angle configurations based on the provided tangent angle instance.
        Parameters:
        atn - the tangent angle instance to process
      • search_atn_atn

        public void search_atn_atn​(AngTn atn)
        Searches for equivalent tangent angle configurations by comparing the provided instance with existing tangent angle configurations.
        Parameters:
        atn - the tangent angle instance to compare
      • search_atn_as

        public void search_atn_as​(AngTn atn)
        Searches for angle structures associated with the given tangent angle configuration.
        Parameters:
        atn - the tangent angle instance for which to search associated angle structures
      • search_atn_at

        public void search_atn_at​(AngTn atn)
        Searches through all angle instances and applies tangent angle evaluation with the given tangent angle instance. Continues until there are no more dependent angle instances.
        Parameters:
        atn - the tangent angle instance used for comparison
      • search_atnas

        public void search_atnas​(AngTn atn,
                                 LLine l1,
                                 LLine l2,
                                 LLine l3,
                                 LLine l4,
                                 Angles as)
        Searches for associated tangent angle configurations by comparing the specified tangent angle instance with provided lines and an angles structure. Creates new tangent angle associations if the configuration meets criteria.
        Parameters:
        atn - the reference tangent angle instance
        l1 - the first line of the primary configuration
        l2 - the second line of the primary configuration
        l3 - the first line of the secondary configuration
        l4 - the second line of the secondary configuration
        as - the angles structure used in association comparison
      • search_atatn

        public void search_atatn​(AngleT at,
                                 AngTn a1)
        Searches for tangent angle configurations that are complementary to the given angle instance. If a valid configuration is found, creates and associates a new angle instance with an adjusted value.
        Parameters:
        at - the base angle instance
        a1 - the tangent angle configuration to compare against
      • ptdr

        public boolean ptdr​(int p,
                            int o,
                            int o1)
        Determines if the point p lies within the range defined by points o and o1.
        Parameters:
        p - the point to check
        o - the first endpoint of the range
        o1 - the second endpoint of the range
        Returns:
        true if p lies between o and o1, otherwise false
      • check_llatn

        public boolean check_llatn​(int p1,
                                   int p2,
                                   LLine l1,
                                   LLine l2,
                                   LLine l3,
                                   LLine l4)
        Checks if the combined angles formed by the specified line segments at points p1 and p2 are approximately complementary. The method evaluates whether the sum of the absolute angles is close to 90 degrees.
        Parameters:
        p1 - the vertex point for the first pair of lines
        p2 - the vertex point for the second pair of lines
        l1 - the first line from p1
        l2 - the second line from p1
        l3 - the first line from p2
        l4 - the second line from p2
        Returns:
        true if the summed angle values are approximately 90 degrees, otherwise false
      • search_ns

        public void search_ns​(LList ns)
        Initiates the search for non-solved structures within the specified list. Skips the search if the last element has already been solved.
        Parameters:
        ns - the list of structures to search
      • search_bk

        public void search_bk​(LList ls)
        Initiates a backup search process.
        Parameters:
        ls - the list of structures to search
      • search_bk_as

        public void search_bk_as​(LList ls)
        Searches through the backup structures contained in the specified list. Iterates over each element in the list and applies transformation based on angle structures.
        Parameters:
        ls - the list of structures to process
      • add_ls_et

        public void add_ls_et​(LList ls,
                              LLine l1,
                              LLine l2,
                              int n)
        Adds a new angle transformation node to the given list. Evaluates if the current transformation in the node matches the provided lines, and if not, creates a new node with the updated angle transformation.
        Parameters:
        ls - the current list of nodes
        l1 - the first line segment for comparison
        l2 - the second line segment for comparison
        n - the index position used for the transformation
      • add_rule_eqag

        public Rule add_rule_eqag​(AngTr t1,
                                  AngTr t2)
        Creates and returns a rule representing an equal angle configuration. Constructs a new rule using the provided angle transformations.
        Parameters:
        t1 - the first angle transformation
        t2 - the second angle transformation
        Returns:
        the constructed Rule object representing equal angles
      • add_ls_node_sub

        public LList add_ls_node_sub​(LList ls,
                                     AngTr t1,
                                     AngTr t2,
                                     int n)
        Creates a new list node as a sub-structure of the existing list. Copies the given list, updates the angle transformation at the specified index, and links the new node to the backup chain.
        Parameters:
        ls - the original list of nodes
        t1 - the original angle transformation
        t2 - the new angle transformation to be applied
        n - the index at which the transformation is updated
        Returns:
        the newly created list node with the updated transformation