Package gprover

Class LLine

  • public class LLine
extends CClass
    Represents a geometric line in the construction.

    The class extends CClass and is used to model a line in a geometric context. It includes properties such as a lemma identifier, a condition object, an integer number to uniquely identify the line, an array of point indices, and a reference to another LLine (for linked constructs).

    • Constructor Summary

      Constructors 
      Constructor Description
      LLine()
      Constructs an LLine object with default values.

    • Method Summary

      All Methods Static Methods Instance Methods Concrete Methods 
      Modifier and Type Method Description
      boolean containPt​(int n)
      Checks if the line contains a specific point.
      void cp_ln​(LLine l1)
      Copies the properties of another LLine object to this one.
      static int get_lpt1​(LLine l1, int p1)
      Gets a point from the line that is not equal to the specified point.
      static int inter_lls​(LLine l1, LLine l2)
      Finds the intersection point of two lines.
      boolean on_ln​(int p)
      Checks if a point is on the line.

      • Methods inherited from class java.lang.Object

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

    • Field Detail

      • co

        public Cond co

      • no

        public int no

      • pt

        public int[] pt

    • Constructor Detail

      • LLine

        public LLine()
        Constructs an LLine object with default values.

    • Method Detail

      • cp_ln

        public void cp_ln​(LLine l1)
        Copies the properties of another LLine object to this one.
        Parameters:
        l1 - the LLine object to copy from

      • containPt

        public boolean containPt​(int n)
        Checks if the line contains a specific point.
        Parameters:
        n - the point to check
        Returns:
        true if the line contains the point, false otherwise

      • inter_lls

        public static int inter_lls​(LLine l1,
                            LLine l2)
        Finds the intersection point of two lines.
        Parameters:
        l1 - the first line
        l2 - the second line
        Returns:
        the intersection point, or 0 if there is no intersection

      • get_lpt1

        public static int get_lpt1​(LLine l1,
                           int p1)
        Gets a point from the line that is not equal to the specified point.
        Parameters:
        l1 - the line
        p1 - the point to exclude
        Returns:
        a point from the line that is not equal to p1, or 0 if no such point exists

      • on_ln

        public final boolean on_ln​(int p)
        Checks if a point is on the line.
        Parameters:
        p - the point to check
        Returns:
        true if the point is on the line, false otherwise