relationalization changes

moving equality expansion out of relationalization
adding Relational wrapper around Formula
resetting Relationalizer before each transformation so it can be used to translate multiple formulae

razor-fol/src/syntax/symbol.rs

@@ -255,6 +255,11 @@ impl Generator {
         self.counter += 1;
         result
     }
+
+    /// Resets the generator by setting its internal counter to 0.
+    pub fn reset(&mut self) {
+        self.counter = 0;
+    }
 }
 
 #[cfg(test)]

razor-fol/src/transform.rs

@@ -15,6 +15,7 @@ pub use dnf::DNF;
 pub use gnf::GNF;
 pub use nnf::NNF;
 pub use pnf::PNF;
+pub use relationalize::Relational;
 pub use snf::SNF;
 pub use substitution::{Substitution, TermBased, VariableRenaming};
 

razor-fol/src/transform/cnf.rs

@@ -14,6 +14,7 @@ pub struct CNF(Formula);
 
 impl CNF {
     /// Returns a reference to the formula wrapped in the receiver CNF.
+    #[inline(always)]
     pub fn formula(&self) -> &Formula {
         &self.0
     }

razor-fol/src/transform/dnf.rs

@@ -14,6 +14,7 @@ pub struct DNF(Formula);
 
 impl DNF {
     /// Returns a reference to the formula wrapped in the receiver DNF.
+    #[inline(always)]
     pub fn formula(&self) -> &Formula {
         &self.0
     }

razor-fol/src/transform/gnf.rs

@@ -17,6 +17,7 @@ pub struct GNF(Formula);
 
 impl GNF {
     /// Returns a reference to the formula wrapped in the receiver NNF.
+    #[inline(always)]
     pub fn formula(&self) -> &Formula {
         &self.0
     }

razor-fol/src/transform/nnf.rs

@@ -12,6 +12,7 @@ pub struct NNF(Formula);
 
 impl NNF {
     /// Returns a reference to the formula wrapped in the receiver NNF.
+    #[inline(always)]
     pub fn formula(&self) -> &Formula {
         &self.0
     }

razor-fol/src/transform/pnf.rs

@@ -14,6 +14,7 @@ pub struct PNF(Formula);
 
 impl PNF {
     /// Returns a reference to the formula wrapped in the receiver PNF.
+    #[inline(always)]
     pub fn formula(&self) -> &Formula {
         &self.0
     }