put term encoding behind flag

src/lib.rs

@@ -375,7 +375,7 @@ impl Default for EGraph {
             node_limit: usize::MAX,
             timestamp: 0,
             proofs_enabled: false,
-            terms_enabled: true,
+            terms_enabled: false,
             term_header_added: false,
             interactive_mode: false,
             test_proofs: false,
@@ -400,8 +400,8 @@ impl EGraph {
     /// including a rust implementation of the union-find
     /// data structure and the rust implementation of
     /// the rebuilding algorithm (maintains congruence closure).
-    pub fn enable_rust_eqsat(&mut self) {
-        self.terms_enabled = false;
+    pub fn enable_terms_encoding(&mut self) {
+        self.terms_enabled = true;
     }
 
     pub fn is_interactive_mode(&self) -> bool {
@@ -444,8 +444,9 @@ impl EGraph {
 
     #[track_caller]
     fn debug_assert_invariants(&self) {
-        // TODO cannot find until added to parent table
-        // so these are not correct when terms are enabled.
+        // we can't use find before something
+        // is added to the parent table, so this
+        // is disabled in terms mode
         if self.terms_enabled {
             return;
         }

src/main.rs

@@ -20,7 +20,7 @@ struct Args {
     /// data structure and the rust implementation of
     /// the rebuilding algorithm (maintains congruence closure).
     #[clap(long)]
-    rust_eqsat: bool,
+    terms_encoding: bool,
     #[clap(long, default_value_t = CompilerPassStop::All)]
     stop: CompilerPassStop,
     // TODO remove this evil hack
@@ -51,8 +51,8 @@ fn main() {
         egraph.set_underscores_for_desugaring(args.num_underscores);
         egraph.fact_directory = args.fact_directory.clone();
         egraph.seminaive = !args.naive;
-        if args.rust_eqsat {
-            egraph.enable_rust_eqsat();
+        if args.terms_encoding {
+            egraph.enable_terms_encoding();
         }
         if args.proofs {
             egraph

tests/files.rs

@@ -8,7 +8,7 @@ struct Run {
     path: PathBuf,
     test_proofs: bool,
     resugar: bool,
-    test_rust_eqsat: bool,
+    test_terms_encoding: bool,
 }
 
 impl Run {
@@ -52,8 +52,8 @@ impl Run {
         if self.test_proofs {
             egraph.test_proofs = true;
         }
-        if self.test_rust_eqsat {
-            egraph.enable_rust_eqsat();
+        if self.test_terms_encoding {
+            egraph.enable_terms_encoding();
         }
         egraph.set_underscores_for_desugaring(5);
         match egraph.parse_and_run_program(program) {
@@ -97,8 +97,8 @@ impl Run {
                 if self.0.resugar {
                     write!(f, "_resugar")?;
                 }
-                if self.0.test_rust_eqsat {
-                    write!(f, "_rust_eqsat")?;
+                if self.0.test_terms_encoding {
+                    write!(f, "_term_encoding")?;
                 }
                 Ok(())
             }
@@ -120,20 +120,25 @@ fn generate_tests(glob: &str) -> Vec<Trial> {
             path: entry.unwrap().clone(),
             test_proofs: false,
             resugar: false,
-            test_rust_eqsat: false,
+            test_terms_encoding: false,
         };
         let should_fail = run.should_fail();
 
         push_trial(run.clone());
         push_trial(Run {
-            test_rust_eqsat: true,
+            test_terms_encoding: true,
             ..run.clone()
         });
         if !should_fail {
             push_trial(Run {
                 resugar: true,
                 ..run.clone()
             });
+            push_trial(Run {
+                resugar: true,
+                test_terms_encoding: true,
+                ..run.clone()
+            });
         }
     }