From 597670ed293733c4d3362543456d6888227b8a00 Mon Sep 17 00:00:00 2001
From: ZachJHansen <zachansen62@gmail.com>
Date: Fri, 3 Nov 2023 12:12:34 -0500
Subject: [PATCH 1/2] Changing default formatting to omit $g sort declaration

---
 src/formatting/fol/default.rs | 10 +++++-----
 1 file changed, 5 insertions(+), 5 deletions(-)

diff --git a/src/formatting/fol/default.rs b/src/formatting/fol/default.rs
index ac275210..7349f24f 100644
--- a/src/formatting/fol/default.rs
+++ b/src/formatting/fol/default.rs
@@ -95,7 +95,7 @@ impl Display for Format<'_, GeneralTerm> {
     fn fmt(&self, f: &mut Formatter<'_>) -> fmt::Result {
         match self.0 {
             GeneralTerm::Symbol(s) => write!(f, "{s}"),
-            GeneralTerm::GeneralVariable(v) => write!(f, "{v}$g"),
+            GeneralTerm::GeneralVariable(v) => write!(f, "{v}"),
             GeneralTerm::IntegerTerm(t) => Format(t).fmt(f),
         }
     }
@@ -180,7 +180,7 @@ impl Display for Format<'_, Variable> {
         let sort = &self.0.sort;
 
         match sort {
-            Sort::General => write!(f, "{name}$g"),
+            Sort::General => write!(f, "{name}"),
             Sort::Integer => write!(f, "{name}$i"),
         }
     }
@@ -436,7 +436,7 @@ mod tests {
                 ]
             })
             .to_string(),
-            "forall X$g Y$i N$g"
+            "forall X Y$i N"
         );
     }
 
@@ -466,7 +466,7 @@ mod tests {
                 }]
             }))
             .to_string(),
-            "5 < I$g"
+            "5 < I"
         );
         assert_eq!(Format(&AtomicFormula::Falsity).to_string(), "#false");
     }
@@ -511,7 +511,7 @@ mod tests {
                 .into()
             })
             .to_string(),
-            "forall X$g p(X$g)"
+            "forall X p(X)"
         );
 
         assert_eq!(

From 56c3f0780e200a4cf926ecc5091e8d7fc2390494 Mon Sep 17 00:00:00 2001
From: ZachJHansen <zachansen62@gmail.com>
Date: Fri, 3 Nov 2023 12:43:43 -0500
Subject: [PATCH 2/2] implementing order on variables and formatting them in a
 deterministic (alphabetical) way

---
 src/formatting/fol/default.rs | 10 +++++++---
 src/syntax_tree/fol.rs        | 22 ++++++++++++++++++++++
 2 files changed, 29 insertions(+), 3 deletions(-)

diff --git a/src/formatting/fol/default.rs b/src/formatting/fol/default.rs
index 7349f24f..8ace9702 100644
--- a/src/formatting/fol/default.rs
+++ b/src/formatting/fol/default.rs
@@ -196,7 +196,12 @@ impl Display for Format<'_, Quantification> {
             Quantifier::Exists => write!(f, "exists"),
         }?;
 
-        let iter = variables.iter().map(Format);
+        let mut sorted_vars = Vec::<Variable>::new();
+        for var in variables.iter() {
+            sorted_vars.push(var.clone());
+        }
+        sorted_vars.sort();
+        let iter = sorted_vars.iter().map(Format);
         for var in iter {
             write!(f, " {var}")?;
         }
@@ -204,7 +209,6 @@ impl Display for Format<'_, Quantification> {
         Ok(())
     }
 }
-
 impl Display for Format<'_, UnaryConnective> {
     fn fmt(&self, f: &mut Formatter<'_>) -> fmt::Result {
         match self.0 {
@@ -436,7 +440,7 @@ mod tests {
                 ]
             })
             .to_string(),
-            "forall X Y$i N"
+            "forall N X Y$i"
         );
     }
 
diff --git a/src/syntax_tree/fol.rs b/src/syntax_tree/fol.rs
index 526e16d0..7c1c0255 100644
--- a/src/syntax_tree/fol.rs
+++ b/src/syntax_tree/fol.rs
@@ -9,6 +9,8 @@ use crate::{
     syntax_tree::{impl_node, Node},
 };
 
+use std::cmp::Ordering;
+
 #[derive(Clone, Debug, Eq, PartialEq)]
 pub enum BasicIntegerTerm {
     Infimum,
@@ -144,6 +146,26 @@ pub struct Variable {
 
 impl_node!(Variable, Format, VariableParser);
 
+impl Ord for Variable {
+    fn cmp(&self, other: &Self) -> Ordering {
+        (&self.name).cmp(&other.name)
+    }
+}
+
+impl PartialOrd for Variable {
+    fn partial_cmp(&self, other: &Self) -> Option<Ordering> {
+        let size1 = self.name.clone();
+        let size2 = other.name.clone();
+        if size1 < size2 {
+            Some(Ordering::Less)
+        } else if size1 > size2 {
+            Some(Ordering::Greater)
+        } else {
+            Some(Ordering::Equal)
+        }
+    }
+}
+
 #[derive(Clone, Debug, Eq, PartialEq)]
 pub enum BinaryConnective {
     Conjunction,