Merge branch 'main' of github.com:egraphs-good/egglog into haobinni-0904

src/gj.rs

@@ -959,7 +959,7 @@ impl<'a> TrieAccess<'a> {
         if idxs.is_empty() {
             let rows = self
                 .function
-                .iter_timestamp_range(&self.timestamp_range, true);
+                .iter_timestamp_range(&self.timestamp_range, self.include_subsumed);
             if self.column < arity {
                 for (i, tup, out) in rows {
                     insert(i, tup, out, tup[self.column])

src/sort/macros.rs

@@ -1,20 +1,21 @@
+#[macro_export]
 macro_rules! add_primitives {
     ($type_info:expr,
         $name:literal = |$($param:ident : $param_t:ty),*| -> $ret:ty { $body:expr }
     ) => {{
         let type_info: &mut _ = $type_info;
         #[allow(unused_imports, non_snake_case)]
         {
-            use $crate::{*, sort::*, constraint::*};
+            use $crate::{*, ast::*, sort::*, constraint::*};
 
             struct MyPrim {$(
                 $param: Arc<<$param_t as FromSort>::Sort>,
             )*
                 __out: Arc<<$ret as IntoSort>::Sort>,
             }
 
-            impl $crate::PrimitiveLike for MyPrim {
-                fn name(&self) -> $crate::Symbol {
+            impl PrimitiveLike for MyPrim {
+                fn name(&self) -> Symbol {
                     $name.into()
                 }
 
@@ -44,7 +45,7 @@ macro_rules! add_primitives {
                     }
                 }
             }
-            type_info.add_primitive($crate::Primitive::from(MyPrim {
+            type_info.add_primitive( Primitive::from(MyPrim {
                 $( $param: type_info.get_sort_nofail::<<$param_t as IntoSort>::Sort>(), )*
                 __out: type_info.get_sort_nofail::<<$ret as IntoSort>::Sort>(),
             }))

src/sort/mod.rs

@@ -10,8 +10,6 @@ mod bigrat;
 pub use bigrat::*;
 mod bool;
 pub use self::bool::*;
-mod rational;
-pub use rational::*;
 mod string;
 pub use string::*;
 mod unit;

src/typechecking.rs

@@ -39,7 +39,6 @@ impl Default for TypeInfo {
         res.add_sort(BoolSort, DUMMY_SPAN.clone()).unwrap();
         res.add_sort(I64Sort, DUMMY_SPAN.clone()).unwrap();
         res.add_sort(F64Sort, DUMMY_SPAN.clone()).unwrap();
-        res.add_sort(RationalSort, DUMMY_SPAN.clone()).unwrap();
         res.add_sort(BigIntSort, DUMMY_SPAN.clone()).unwrap();
         res.add_sort(BigRatSort, DUMMY_SPAN.clone()).unwrap();
 

tests/before-proofs.egg

@@ -1,18 +1,18 @@
 (datatype Math
     (Add Math Math)
     (Sub Math Math)
-    (Const Rational)
+    (Const i64)
     (Var String))
 
-(rewrite (Add a b) (Add (Add a b) (Const (rational 0 1))))
+(rewrite (Add a b) (Add (Add a b) (Const 0)))
 
 (rewrite (Add a b) (Add b a))
 
 
 (rewrite (Add a (Add b c))
       (Add (Add a b) c))
 
-(let two (rational 2 1))
+(let two 2)
 (let start1 (Add (Var "x") (Const two)))
 ;; add original proofs
 
@@ -23,7 +23,7 @@
 (check (= (Add (Var "x") (Const two))
           (Add (Const two) (Var "x"))))
 
-(let zero (Const (rational 0 1)))
+(let zero (Const 0))
 (let addx2 (Add (Var "x") (Const two)))
 (let addx20 (Add addx2 zero))
 (let addzerofront (Add (Add zero (Var "x")) (Const two)))

tests/herbie-tutorial.egg

@@ -1,13 +1,13 @@
 (datatype Math
-  (Num Rational)
+  (Num BigRat)
   (Var String)
   (Add Math Math)
   (Div Math Math)
   (Mul Math Math))
 
-(let zero (Num (rational 0 1)))
-(let one (Num (rational 1 1)))
-(let two (Num (rational 2 1)))
+(let zero (Num (bigrat (bigint 0) (bigint 1))))
+(let one (Num (bigrat (bigint 1) (bigint 1))))
+(let two (Num (bigrat (bigint 2) (bigint 1))))
 
 (rewrite (Add a b) (Add b a))
 (rewrite (Add a zero) a)
@@ -19,7 +19,7 @@
 (push)
 (run 1)
 ;; yay, constant folding works
-(check (= one-two (Num (rational 3 1))))
+(check (= one-two (Num (bigrat (bigint 3) (bigint 1)))))
 ;; also, commutativity works
 (check (= (Add two one) one-two))
 (pop)
@@ -35,8 +35,8 @@
 (pop)
 
 ;; we need to detect when things are non-zero
-(function lower-bound (Math) Rational :merge (max old new))
-(function upper-bound (Math) Rational :merge (min old new))
+(function lower-bound (Math) BigRat :merge (max old new))
+(function upper-bound (Math) BigRat :merge (min old new))
 
 (rule ((Num r))
       ((set (lower-bound (Num r)) r)
@@ -63,15 +63,15 @@
                       (* uba ubb)))))))
 
 (rule ((= e (Add a b))
-       (> (lower-bound e) (rational 0 1)))
+       (> (lower-bound e) (bigrat (bigint 0) (bigint 1))))
       ((union one (Div (Add a b) (Add a b)))))
 
 (let x (Var "x"))
 (let x1 (Add x one))
 
 (push)
-(set (lower-bound x) (rational 0 1))
-(set (upper-bound x) (rational 1 1))
+(set (lower-bound x) (bigrat (bigint 0) (bigint 1)))
+(set (upper-bound x) (bigrat (bigint 1) (bigint 1)))
 
 (run 3)
 
@@ -83,8 +83,8 @@
 
 
 ;; Set the variable x to a particular input value 200/201
-(set (lower-bound x) (rational 200 201))
-(set (upper-bound x) (rational 200 201))
+(set (lower-bound x) (bigrat (bigint 200) (bigint 201)))
+(set (upper-bound x) (bigrat (bigint 200) (bigint 201)))
 
 (run 3)
 
@@ -107,7 +107,7 @@
 
 (rule ((Num n))
       ((set (best-error (Num n)) (to-f64 n))))
-(rule ((Add a b)) ((set (best-error (Add a b)) (to-f64 (rational 10000 1)))))
+(rule ((Add a b)) ((set (best-error (Add a b)) (to-f64 (bigrat (bigint 10000) (bigint 1))))))
 
 ;; finally, the mega rule for finding more accurate programs
 (rule ((= expr (Add a b))
@@ -125,13 +125,13 @@
 
 (let target
   (Add 
-    (Add (Num (rational 1 100)) (Num (rational 1 100)))
-    (Num (rational -2 100))))
+    (Add (Num (bigrat (bigint 1) (bigint 100))) (Num (bigrat (bigint 1) (bigint 100))))
+    (Num (bigrat (bigint -2) (bigint 100)))))
 
 (run 1)
 
 ;; set a default
-(set (best-error target) (to-f64 (rational 10000 1)))
+(set (best-error target) (to-f64 (bigrat (bigint 10000) (bigint 1))))
 ;; error is bad, constant folding hasn't fired enough
 (query-extract (best-error target))