Package gprover

Class Cond

  • public class Cond
extends java.lang.Object
    Represents a condition in the proof structure. It contains details like rule, predicate, step number, description, proof structure and related attributes.

    • Field Summary

      Fields 
      Modifier and Type Field Description
      Cond cd
      Additional condition.
      long dep
      Depth of the condition, initialized from Gib.depth.
      static int MAX_GEO
      Maximum number of geometric elements.
      int no
      The number of the current step.
      Cond nx
      Next condition.
      int[] p
      Array of geometric elements.
      int pred
      Predicate identifier.
      protected int rule
      The rule being used in this step (theorems or lemmas).
      java.lang.String sd
      Step description.
      gprover.UStruct u
      Structure holding different geometric entities.
      java.util.Vector vlist
      List of the direct steps in this node.

    • Constructor Summary

      Constructors 
      Constructor Description
      Cond()
      Default condition constructor that initializes required fields.
      Cond​(boolean r)
      Constructs a condition optionally initializing the geometric array.
      Cond​(int t)
      Constructs a condition with a given predicate.
      Cond​(Cond co)
      Copy constructor for creating a duplicate of a given condition.

    • Method Summary

      All Methods Instance Methods Concrete Methods 
      Modifier and Type Method Description
      void add_allco​(java.util.Vector v)
      Adds all conditions from a given vector.
      void addcond​(int r, Cond co)
      Adds a condition with a specified rule.
      void addcond​(int lm, Cond co1, Cond co2)
      Adds two conditions as direct children with a specified rule.
      void addcond​(Cond co)
      Adds a condition as a direct child.
      void addcond​(Cond co1, Cond co2)
      Adds two conditions as direct children.
      CClass get_attr()
      Retrieves the attributes associated with the condition.
      int get_conc_type()
      Determines the type of the condition's conclusion.
      int getNo()
      Retrieves the current step number.
      Cond getPCO()
      Retrieves the condition from the internal structure.
      int getRule()
      Retrieves the current rule.
      void getRuleFromeFacts()
      Sets the rule from the related facts in the internal structure.
      java.lang.String getText()
      Retrieves the step description.
      void gRule()
      Dummy method for rule processing.
      void setCondToBeProveHead()
      Prepends the step description with a language specific "To Prove:" message.
      void setRule​(int r)
      Sets the current rule.
      void setText​(java.lang.String s)
      Sets the step description.
      java.lang.String toString()
      Returns the step description as the string representation.

      • Methods inherited from class java.lang.Object

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

    • Field Detail

      • MAX_GEO

        public static final int MAX_GEO
        Maximum number of geometric elements.
        See Also:
        Constant Field Values

      • rule

        protected int rule
        The rule being used in this step (theorems or lemmas).

      • pred

        public int pred
        Predicate identifier.

      • no

        public int no
        The number of the current step.

      • p

        public int[] p
        Array of geometric elements.

      • u

        public gprover.UStruct u
        Structure holding different geometric entities.

      • nx

        public Cond nx
        Next condition.

      • cd

        public Cond cd
        Additional condition.

      • sd

        public java.lang.String sd
        Step description.

      • vlist

        public java.util.Vector vlist
        List of the direct steps in this node.

      • dep

        public long dep
        Depth of the condition, initialized from Gib.depth.

    • Constructor Detail

      • Cond

        public Cond​(int t)
        Constructs a condition with a given predicate.
        Parameters:
        t - the predicate

      • Cond

        public Cond()
        Default condition constructor that initializes required fields.

      • Cond

        public Cond​(boolean r)
        Constructs a condition optionally initializing the geometric array.
        Parameters:
        r - if true, initializes the geometric array; otherwise leaves it null

      • Cond

        public Cond​(Cond co)
        Copy constructor for creating a duplicate of a given condition.
        Parameters:
        co - the condition to copy

    • Method Detail

      • getText

        public java.lang.String getText()
        Retrieves the step description.
        Returns:
        the step description text

      • setText

        public void setText​(java.lang.String s)
        Sets the step description.
        Parameters:
        s - the new description text

      • getNo

        public int getNo()
        Retrieves the current step number.
        Returns:
        the step number

      • getRule

        public int getRule()
        Retrieves the current rule.
        Returns:
        the rule applied

      • getRuleFromeFacts

        public void getRuleFromeFacts()
        Sets the rule from the related facts in the internal structure.

      • setRule

        public void setRule​(int r)
        Sets the current rule.
        Parameters:
        r - the rule to be set

      • getPCO

        public Cond getPCO()
        Retrieves the condition from the internal structure.
        Returns:
        the condition pointer (PCO)

      • toString

        public java.lang.String toString()
        Returns the step description as the string representation.
        Overrides:
        toString in class java.lang.Object
        Returns:
        the step description

      • setCondToBeProveHead

        public void setCondToBeProveHead()
        Prepends the step description with a language specific "To Prove:" message.

      • addcond

        public void addcond​(Cond co)
        Adds a condition as a direct child.
        Parameters:
        co - the condition to add

      • addcond

        public void addcond​(int r,
                    Cond co)
        Adds a condition with a specified rule.
        Parameters:
        r - the rule value to set
        co - the condition to add

      • add_allco

        public void add_allco​(java.util.Vector v)
        Adds all conditions from a given vector.
        Parameters:
        v - the vector containing conditions to add

      • addcond

        public void addcond​(int lm,
                    Cond co1,
                    Cond co2)
        Adds two conditions as direct children with a specified rule.
        Parameters:
        lm - the rule value to set
        co1 - the first condition to add
        co2 - the second condition to add

      • addcond

        public void addcond​(Cond co1,
                    Cond co2)
        Adds two conditions as direct children.
        Parameters:
        co1 - the first condition to add
        co2 - the second condition to add

      • get_attr

        public CClass get_attr()
        Retrieves the attributes associated with the condition.
        Returns:
        a CClass representing the condition's attributes

      • get_conc_type

        public int get_conc_type()
        Determines the type of the condition's conclusion.
        Returns:
        1 if the internal structure is null; 2 if the condition obtained from the structure is null; otherwise 0

      • gRule

        public void gRule()
        Dummy method for rule processing. Implementation pending.