Package gprover

Class Gib

  • Direct Known Subclasses:
    GDDBase

    public class Gib
    extends java.lang.Object
    The Gib class provides functionality for geometric computations, including operations on angles, lines, circles, triangles, and other geometric constructions.

    This class is a central component within the geometric prover system, facilitating the creation, manipulation, and evaluation of various geometric entities and their relationships.

    • Constructor Detail

      • Gib

        public Gib()
        Constructs a new Gib instance. Initializes all internal data structures and sets default values.
    • Method Detail

      • initRules

        public static void initRules()
        Initializes the rule configuration. Sets all rules to true and then disables specific rules.
      • init_dbase

        public void init_dbase()
        Initializes the database. Resets various lists, counters, and clears auxiliary collections.
      • fd_pt

        public int fd_pt​(java.lang.String s)
        Finds the point index by its name.
        Parameters:
        s - the name of the point
        Returns:
        the index of the point if found; 0 otherwise
      • fd_pt

        public ProPoint fd_pt​(double x,
                              double y)
        Finds a point by its coordinates.
        Parameters:
        x - the x-coordinate to match
        y - the y-coordinate to match
        Returns:
        the point if one exists within tolerance; null otherwise
      • setNoPrint

        public void setNoPrint()
        Disables printing output.
      • isPFull

        public boolean isPFull()
        Checks if the proof status is full.
        Returns:
        true if the proof status is full; false otherwise
      • gexit

        public void gexit​(int id)
        Exits the application with the specified error id.
        Parameters:
        id - the error id for the exit process
      • show_agll

        public final void show_agll​(LLine ln1,
                                    LLine ln2)
        Displays the angle between two lines by determining their intersection point.
        Parameters:
        ln1 - the first LLine object
        ln2 - the second LLine object
      • exit

        public final void exit​(int v)
        Exits the system with the specified exit status.
        Parameters:
        v - the exit status code
      • gerror

        public final void gerror​(java.lang.String s)
        Prints an error message and terminates the program.
        Parameters:
        s - the error message to display before exiting
      • getDefaultCond

        public final Cond getDefaultCond​(CClass cc)
        Returns the default condition for the specified geometric class.
        Parameters:
        cc - the geometric class object
        Returns:
        a default condition associated with the provided class, or null if unsupported
      • check_eqangle

        protected boolean check_eqangle​(int p1,
                                        int p2,
                                        int p3,
                                        int p4,
                                        int p5,
                                        int p6)
        Checks if the angles formed by points (p1, p2, p3) and (p4, p5, p6) are equal.
        Parameters:
        p1 - index of the vertex for the first angle
        p2 - index of the first arm point for the first angle
        p3 - index of the second arm point for the first angle
        p4 - index of the vertex for the second angle
        p5 - index of the first arm point for the second angle
        p6 - index of the second arm point for the second angle
        Returns:
        true if the two angles are equal within a tolerance; false otherwise
      • check_atn

        protected boolean check_atn​(int p1,
                                    int p2,
                                    int p3,
                                    int p4,
                                    int p5,
                                    int p6)
        Checks whether the sum of the two angles defined by the given points equals 90°.
        Parameters:
        p1 - index of the vertex for the first angle
        p2 - index of an arm point for the first angle
        p3 - index of the other arm point for the first angle
        p4 - index of the vertex for the second angle
        p5 - index of an arm point for the second angle
        p6 - index of the other arm point for the second angle
        Returns:
        true if the sum of angles is 90° (within tolerance); false otherwise
      • check_eqangle

        protected boolean check_eqangle​(int p1,
                                        int p2,
                                        int p3,
                                        int p4,
                                        int p5,
                                        int p6,
                                        int p7,
                                        int p8)
        Checks if two angles defined by four points are equal or supplementary.
        Parameters:
        p1 - index of the first point of the first angle
        p2 - index of the second point of the first angle
        p3 - index of the third point of the first angle
        p4 - index of the fourth point of the first angle
        p5 - index of the first point of the second angle
        p6 - index of the second point of the second angle
        p7 - index of the third point of the second angle
        p8 - index of the fourth point of the second angle
        Returns:
        true if the angles are equal or supplementary (within tolerance); false otherwise
      • check_eqangle_t

        protected boolean check_eqangle_t​(int p1,
                                          int p2,
                                          int p3,
                                          int p4,
                                          int p5,
                                          int p6,
                                          int p7,
                                          int p8)
        Checks if two angle values computed via a transformed approach are equal.
        Parameters:
        p1 - index of the first point of the first angle
        p2 - index of the second point of the first angle
        p3 - index of the third point of the first angle
        p4 - index of the fourth point of the first angle
        p5 - index of the first point of the second angle
        p6 - index of the second point of the second angle
        p7 - index of the third point of the second angle
        p8 - index of the fourth point of the second angle
        Returns:
        true if the absolute transformed angle values are equal (within tolerance); false otherwise
      • check_angle_ls_90

        public boolean check_angle_ls_90​(int p1,
                                         int p2,
                                         int p3)
        Determines whether the angle formed by three points is a right angle (90°).
        Parameters:
        p1 - index of the vertex of the angle
        p2 - index of the first arm point
        p3 - index of the second arm point
        Returns:
        true if the angle is 90° (within tolerance); false otherwise
      • x_inside

        protected boolean x_inside​(int p1,
                                   int p2,
                                   int p3)
        Determines if a point lies strictly between two other points along both axes.
        Parameters:
        p1 - index of the point to test
        p2 - index of the first boundary point
        p3 - index of the second boundary point
        Returns:
        true if p1 is inside the interval defined by p2 and p3; false otherwise
      • getAngleValue_t

        protected double getAngleValue_t​(int p1,
                                         int p2,
                                         int p3,
                                         int p4)
        Computes an angle value using transformed points. The method considers special ordering of the points to compute the appropriate angle.
        Parameters:
        p1 - index of the first point
        p2 - index of the second point
        p3 - index of the third point
        p4 - index of the fourth point
        Returns:
        the computed angle value
      • check_eqdistance

        protected boolean check_eqdistance​(int p1,
                                           int p2,
                                           int p3,
                                           int p4,
                                           double t1,
                                           double t2)
        Checks if the distance between two pairs of points are equal after scaling.
        Parameters:
        p1 - index of the first point of the first segment
        p2 - index of the second point of the first segment
        p3 - index of the first point of the second segment
        p4 - index of the second point of the second segment
        t1 - scaling factor for the first segment
        t2 - scaling factor for the second segment
        Returns:
        true if the scaled distances are equal (within tolerance); false otherwise
      • check_eqdistance

        protected boolean check_eqdistance​(int p1,
                                           int p2,
                                           int p3,
                                           int p4)
        Checks if the distances between two pairs of points are equal.
        Parameters:
        p1 - index of the first point of the first segment
        p2 - index of the second point of the first segment
        p3 - index of the first point of the second segment
        p4 - index of the second point of the second segment
        Returns:
        true if the distances are equal (within tolerance); false otherwise
      • check_ratio

        protected boolean check_ratio​(int a,
                                      int b,
                                      int c,
                                      int d,
                                      int p,
                                      int q,
                                      int r,
                                      int s)
        Validates whether the ratio of the squared lengths of two segments remain equal.
        Parameters:
        a - index of the first point of the first segment
        b - index of the second point of the first segment
        c - index of the first point of the second segment
        d - index of the second point of the second segment
        p - index of the first point of the third segment
        q - index of the second point of the third segment
        r - index of the first point of the fourth segment
        s - index of the second point of the fourth segment
        Returns:
        true if the products of squared lengths are equal (within tolerance); false otherwise
      • ck_4peq

        public boolean ck_4peq​(int p1,
                               int p2,
                               int p3,
                               int p4)
        Checks if two pairs of points are equal regardless of order.
        Parameters:
        p1 - the first point of the first pair
        p2 - the second point of the first pair
        p3 - the first point of the second pair
        p4 - the second point of the second pair
        Returns:
        true if the pairs (p1, p2) and (p3, p4) are equal in any order, false otherwise
      • ck_dr

        public boolean ck_dr​(int p1,
                             int p2,
                             int p3,
                             int p4)
        Evaluates directional compatibility between two segments defined by two pairs of points.
        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
        Returns:
        true if the segments satisfy specific directional conditions, false otherwise
      • length2

        protected double length2​(int p1,
                                 int p2)
        Calculates the squared Euclidean distance between two points.
        Parameters:
        p1 - the first point
        p2 - the second point
        Returns:
        the squared distance between p1 and p2
      • getAngleValue

        protected double getAngleValue​(int p1,
                                       int p2,
                                       int p3)
        Computes the angle value at the middle point defined by three points.
        Parameters:
        p1 - the first point
        p2 - the vertex point where the angle is measured
        p3 - the third point
        Returns:
        the angle value at p2 (in radians)
      • getAngleValue

        protected double getAngleValue​(int p,
                                       LLine l1,
                                       LLine l2)
        Determines the angle formed at a common point by two lines.
        Parameters:
        p - the intersection point of the lines
        l1 - the first line
        l2 - the second line
        Returns:
        the angle between l1 and l2 at point p (in radians)
      • check_ateq

        protected boolean check_ateq​(int a,
                                     int b,
                                     int c,
                                     int v)
        Checks if the angle formed by three points is approximately equal to a given value.
        Parameters:
        a - the first point
        b - the vertex point where the angle is measured
        c - the third point
        v - the target angle value in degrees
        Returns:
        true if the measured angle is approximately equal to v, false otherwise
      • getAngleValue

        protected double getAngleValue​(int p1,
                                       int p2,
                                       int p3,
                                       int p4)
        Computes the angle difference between the lines defined by two point pairs.
        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:
        the difference between the angles (in radians) of the two lines
      • same_tri

        public final boolean same_tri​(int p1,
                                      int p2,
                                      int p3,
                                      int q1,
                                      int q2,
                                      int q3)
        Checks if two triangles, defined by three vertex points each, are identical. The comparison is independent of the vertex order.
        Parameters:
        p1 - vertex of the first triangle
        p2 - vertex of the first triangle
        p3 - vertex of the first triangle
        q1 - vertex of the second triangle
        q2 - vertex of the second triangle
        q3 - vertex of the second triangle
        Returns:
        true if the triangles are the same; false otherwise
      • collect_angst

        public void collect_angst()
        Collects angle expressions into a collection. Processes the global list of angle objects and groups unique angle expressions.
      • addAngst

        public void addAngst​(Angles ag,
                             java.util.Vector v)
        Adds an angle expression to a new angle structure. Updates the global angle structure list with the provided angle.
        Parameters:
        ag - the angle expression to add
        v - a vector used for collecting angle structures
      • insertAngle

        public boolean insertAngle​(Angles ag)
        Attempts to insert an angle expression into the existing angle structure list.
        Parameters:
        ag - the angle expression to insert
        Returns:
        true if the angle was merged with an existing structure; false otherwise
      • fd_ast

        public AngSt fd_ast​(LLine l1,
                            LLine l2)
        Finds and returns the angle structure that contains the specified lines.
        Parameters:
        l1 - the first line to search within angle structures
        l2 - the second line to search within angle structures
        Returns:
        the angle structure containing the lines, or null if not found
      • setValue

        public static void setValue​(int n,
                                    boolean v)
        Sets the boolean flag at a given index in a shared values array.
        Parameters:
        n - the 1-based index of the value to set
        v - the boolean value to set