From ecc2fa5631b7768ccac6e2fccd44a977137fd639 Mon Sep 17 00:00:00 2001
From: Tobias Stolzmann <tobias.stolzmann@potassco.com>
Date: Wed, 20 Nov 2024 23:20:12 +0100
Subject: [PATCH] Implement substitute for SymbolicTerms

---
 src/syntax_tree/fol.rs | 15 +++++++++++++++
 1 file changed, 15 insertions(+)

diff --git a/src/syntax_tree/fol.rs b/src/syntax_tree/fol.rs
index ddaef46..41404a2 100644
--- a/src/syntax_tree/fol.rs
+++ b/src/syntax_tree/fol.rs
@@ -143,6 +143,13 @@ impl SymbolicTerm {
             SymbolicTerm::Symbol(_) | SymbolicTerm::Variable(_) => IndexSet::new(),
         }
     }
+
+    pub fn substitute(self, var: Variable, term: SymbolicTerm) -> Self {
+        match self {
+            SymbolicTerm::Variable(s) if var.name == s && var.sort == Sort::Symbol => term,
+            _ => self,
+        }
+    }
 }
 
 #[derive(Clone, Debug, Eq, PartialEq, Hash)]
@@ -202,6 +209,14 @@ impl GeneralTerm {
                     "cannot substitute general term `{term}` for the integer variable `{var}`"
                 ),
             },
+            GeneralTerm::SymbolicTerm(t) if var.sort == Sort::Symbol => match term {
+                GeneralTerm::SymbolicTerm(term) => {
+                    GeneralTerm::SymbolicTerm(t.substitute(var, term))
+                }
+                _ => panic!(
+                    "cannot substitute general term `{term}` for the symbolic variable `{var}`"
+                ),
+            },
             t => t,
         }
     }