java.lang.Object
- gprover.Prover

```
public class Prover
extends java.lang.Object
```
The Prover class provides static methods for performing geometric proofs and computations. It manages the state of geometric terms and interacts with the geometric database.
This class is not instantiable.

Method Summary

All Methods Static Methods Concrete Methods
Modifier and Type	Method	Description
`static boolean`	`fixpoint(GTerm gt)`	Initializes the database and performs a fixpoint computation using the provided geometric term.
`static GDDBc`	`get_gddbase()`	Retrieves the current geometric database.
`static int`	`get_pt_id(java.lang.String s)`	Retrieves the identifier of the point corresponding to the specified name.
`static java.lang.String`	`get_pt_name(int t)`	Retrieves the name of the point corresponding to the specified identifier.
`static boolean`	`getAllNdgs(GTerm gt, java.util.Vector v1, java.util.Vector v2, java.util.Vector v3, java.util.Vector v4)`	Retrieves all nondiscussed geometric statements and stores them in the provided vectors.
`static AuxPt`	`getConstructedAuxPoint()`	Retrieves the constructed auxiliary point if one was created during the proof.
`static int`	`getErrorType()`	Retrieves the error type code from the full angle proof.
`static Cond`	`getFullconc()`	Retrieves and displays the full conclusion from the geometric term.
`static int`	`getNumberofProperties()`	Retrieves the total number of properties in the database.
`static int`	`getPFullResult()`	Returns the result of the full angle proof.
`static Cond`	`getProveHead()`	Returns the head of the proof condition.
`static LList`	`getProveHead_ls(LList ls)`	Retrieves the next proof head in the given list.
`static boolean`	`prove()`	Attempts to prove the current geometric term.
`static boolean`	`prove(Cond co)`	Attempts to prove the provided geometric condition.
`static GrTerm`	`proveFull(GTerm gt)`	Proves the full angle expression for the specified geometric term.
`static void`	`reset()`	Resets the internal database and state.
`static void`	`run()`	Executes a fixpoint computation on the current geometric term.
`static java.util.Vector`	`search_a_fact(int t, java.lang.String s1, java.lang.String s2, java.lang.String s3)`	Searches for a fact matching the provided criteria.
`static void`	`set_gterm(GTerm g)`	Sets the global geometric term.
`static void`	`setGIB()`	Sets the global database to the full geometric base.
`static void`	`showCondTextF(Cond co)`	Displays the condition text for the given proof condition.

Methods inherited from class java.lang.Object
clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait

- Method Detail
  - set_gterm
```
public static void set_gterm(GTerm g)
```
    Sets the global geometric term.
    
    Parameters:
    
    g - the geometric term to set
  - reset
```
public static void reset()
```
    Resets the internal database and state.
  - run
```
public static void run()
```
    Executes a fixpoint computation on the current geometric term.
  - get_pt_name
```
public static java.lang.String get_pt_name(int t)
```
    Retrieves the name of the point corresponding to the specified identifier.
    
    Parameters:
    
    t - the point identifier
    
    Returns:
    
    the point name, or "null" if the database is not initialized
  - get_pt_id
```
public static int get_pt_id(java.lang.String s)
```
    Retrieves the identifier of the point corresponding to the specified name.
    
    Parameters:
    
    s - the point name
    
    Returns:
    
    the point identifier, or 0 if the database is not initialized
  - getNumberofProperties
```
public static int getNumberofProperties()
```
    Retrieves the total number of properties in the database.
    
    Returns:
    
    the number of properties, or 0 if the database is not initialized
  - fixpoint
```
public static boolean fixpoint(GTerm gt)
```
    Initializes the database and performs a fixpoint computation using the provided geometric term.
    
    Parameters:
    
    gt - the geometric term used for the computation
    
    Returns:
    
    true if the fixpoint computation is successful, false otherwise
  - prove
```
public static boolean prove()
```
    Attempts to prove the current geometric term.
    
    Returns:
    
    true if the proof is successful, false otherwise
  - getConstructedAuxPoint
```
public static AuxPt getConstructedAuxPoint()
```
    Retrieves the constructed auxiliary point if one was created during the proof.
    
    Returns:
    
    the auxiliary point if available, or null otherwise
  - prove
```
public static boolean prove(Cond co)
```
    Attempts to prove the provided geometric condition.
    
    Parameters:
    
    co - the condition to prove
    
    Returns:
    
    true if the condition is successfully proved, false otherwise
  - get_gddbase
```
public static GDDBc get_gddbase()
```
    Retrieves the current geometric database.
    
    Returns:
    
    the current GDDBc instance
  - setGIB
```
public static void setGIB()
```
    Sets the global database to the full geometric base.
  - getProveHead
```
public static Cond getProveHead()
```
    Returns the head of the proof condition.
    
    Returns:
    
    the current proof condition head as a Cond object, or null if the database is not initialized.
  - getProveHead_ls
```
public static LList getProveHead_ls(LList ls)
```
    Retrieves the next proof head in the given list.
    
    Parameters:
    
    ls - the current list of proof heads
    
    Returns:
    
    the next LList proof head from the database
  - search_a_fact
```
public static java.util.Vector search_a_fact(int t,
                                             java.lang.String s1,
                                             java.lang.String s2,
                                             java.lang.String s3)
```
    Searches for a fact matching the provided criteria.
    
    Parameters:
    
    t - the type of fact to search for
    
    s1 - the first search parameter
    
    s2 - the second search parameter
    
    s3 - the third search parameter
    
    Returns:
    
    a Vector of matching facts
  - getFullconc
```
public static Cond getFullconc()
```
    Retrieves and displays the full conclusion from the geometric term.
    
    Returns:
    
    the full conclusion as a Cond object
  - proveFull
```
public static GrTerm proveFull(GTerm gt)
```
    Proves the full angle expression for the specified geometric term.
    
    Parameters:
    
    gt - the geometric term to prove
    
    Returns:
    
    the GrTerm representing the full angle proof head, or null if proof fails
  - getAllNdgs
```
public static boolean getAllNdgs(GTerm gt,
                                 java.util.Vector v1,
                                 java.util.Vector v2,
                                 java.util.Vector v3,
                                 java.util.Vector v4)
```
    Retrieves all nondiscussed geometric statements and stores them in the provided vectors.
    
    Parameters:
    
    gt - the geometric term to process
    
    v1 - vector to store the first group of statements
    
    v2 - vector to store the second group of statements
    
    v3 - vector to store the third group of statements
    
    v4 - vector to store the fourth group of statements
    
    Returns:
    
    true if the nondiscussed statements were successfully retrieved; false otherwise
  - getPFullResult
```
public static int getPFullResult()
```
    Returns the result of the full angle proof.
    
    Returns:
    
    0 if the proof is successful, 1 if it fails, or 2 if it cannot be expressed as a full angle expression
  - getErrorType
```
public static int getErrorType()
```
    Retrieves the error type code from the full angle proof.
    
    Returns:
    
    an integer representing the error type
  - showCondTextF
```
public static void showCondTextF(Cond co)
```
    Displays the condition text for the given proof condition.
    
    Parameters:
    
    co - the condition to be displayed

Class Prover

Method Summary

Methods inherited from class java.lang.Object

Method Detail

set_gterm

reset

run

get_pt_name

get_pt_id

getNumberofProperties

fixpoint

prove

getConstructedAuxPoint

prove

get_gddbase

setGIB

getProveHead

getProveHead_ls

search_a_fact

getFullconc

proveFull

getAllNdgs

getPFullResult

getErrorType

showCondTextF