Add f64 exp, log, and sqrt primitives

src/lib.rs

@@ -2207,13 +2207,13 @@ mod tests {
                 r#"
                 (datatype Math)
                 (constructor container (Math) Math)
-                (constructor exp () Math :cost 100)
+                (constructor expensive () Math :cost 100)
                 (constructor cheap () Math)
                 (constructor cheap-1 () Math)
                 ; we make the container cheap so that it will be extracted if possible, but then we mark it as subsumed
-                ; so the (exp) expr should be extracted instead
+                ; so the (expensive) expr should be extracted instead
                 (let res (container (cheap)))
-                (union res (exp))
+                (union res (expensive))
                 (cheap)
                 (cheap-1)
                 (subsume (container (cheap)))
@@ -2246,7 +2246,7 @@ mod tests {
                 "#,
             )
             .unwrap();
-        assert_eq!(outputs[0].to_string(), "(exp)\n");
+        assert_eq!(outputs[0].to_string(), "(expensive)\n");
     }
 
     #[test]
@@ -2260,9 +2260,9 @@ mod tests {
                 r#"
                 (datatype Math)
                 (constructor container (Math) Math)
-                (constructor exp () Math :cost 100)
+                (constructor expensive () Math :cost 100)
                 (constructor cheap () Math)
-                (exp)
+                (expensive)
                 (let x (cheap))
                 (subsume (cheap))
                 "#,
@@ -2275,7 +2275,7 @@ mod tests {
             .parse_and_run_program(
                 None,
                 r#"
-                (union (exp) x)
+                (union (expensive) x)
                 "#,
             )
             .unwrap();
@@ -2292,6 +2292,6 @@ mod tests {
                 "#,
             )
             .unwrap();
-        assert_eq!(res[0].to_string(), "(exp)\n");
+        assert_eq!(res[0].to_string(), "(expensive)\n");
     }
 }

src/sort/f64.rs

@@ -3,7 +3,8 @@ use super::*;
 /// 64-bit floating point numbers supporting these primitives:
 /// - Arithmetic: `+`, `-`, `*`, `/`, `%`, `^`, `neg`, `abs`
 /// - Comparisons: `<`, `>`, `<=`, `>=`
-/// - Other: `min`, `max`, `to-i64`, `to-string`
+/// - Other: `min`, `max`, `exp`, `log`, `sqrt`
+/// - Conversions: `to-f64`, `to-i64`, `to-string`
 #[derive(Debug)]
 pub struct F64Sort;
 
@@ -35,6 +36,13 @@ impl BaseSort for F64Sort {
         add_literal_prim!(eg, "min" = |a: F, b: F| -> F { a.min(b) });
         add_literal_prim!(eg, "max" = |a: F, b: F| -> F { a.max(b) });
         add_literal_prim!(eg, "abs" = |a: F| -> F { F::from(a.abs()) });
+        add_literal_prim!(eg, "exp" = |a: F| -> F { F::from(OrderedFloat(a.exp())) });
+        add_literal_prim!(eg, "log" = |a: F| -?> F {
+            (*a > OrderedFloat(0.0)).then(|| F::from(OrderedFloat(a.ln())))
+        });
+        add_literal_prim!(eg, "sqrt" = |a: F| -?> F {
+            (*a >= OrderedFloat(0.0)).then(|| F::from(OrderedFloat(a.sqrt())))
+        });
 
         // `to-f64` should be in `i64.rs`, but `F64Sort` wouldn't exist yet
         add_literal_prim!(eg, "to-f64" = |a: i64| -> F { F::from(OrderedFloat(a as f64)) });

tests/f64.egg

@@ -4,7 +4,12 @@
 (check (< 1.5 9.2))
 (check (>= 9.2 1.5))
 (check (= (^ 9.0 2.5) 243.0))
+(check (= (exp 0.0) 1.0))
+(check (= (log 1.0) 0.0))
+(check (= (sqrt 4.0) 2.0))
 (fail (check (= (^ 4.0 2.5) 31.99)))
+(fail (log 0.0))
+(fail (sqrt -1.0))
 (fail (check (< 9.2 1.5)))
 (fail (check (= (+ 1.5 9.2) 10.6)))
 (check (= (to-f64 1) 1.0))

tests/integration_test.rs

@@ -477,10 +477,10 @@ fn test_subsumed_unextractable_action_extract() {
             None,
             r#"
             (datatype Math)
-            (constructor exp () Math :cost 100)
+            (constructor expensive () Math :cost 100)
             (constructor cheap () Math :cost 1)
-            (union (exp) (cheap))
-            (extract (exp))
+            (union (expensive) (cheap))
+            (extract (expensive))
             "#,
         )
         .unwrap();
@@ -501,13 +501,13 @@ fn test_subsumed_unextractable_action_extract() {
             None,
             r#"
             (subsume (cheap))
-            (extract (exp))
+            (extract (expensive))
             "#,
         )
         .unwrap();
     assert!(match &outputs[0] {
         CommandOutput::ExtractBest(termdag, _, term_id) => {
-            matches!(termdag.get(*term_id), Term::App(s, ..) if s == "exp")
+            matches!(termdag.get(*term_id), Term::App(s, ..) if s == "expensive")
         }
         _ => false,
     });
@@ -525,21 +525,21 @@ fn test_subsume_unextractable_insert_and_merge() {
             (datatype Expr
                 (f Expr)
                 (Num i64))
-            (constructor exp () Expr :cost 100)
+            (constructor expensive () Expr :cost 100)
 
               (f (Num 1))
               (subsume (f (Num 1)))
               (f (Num 2))
 
               (union (Num 2) (Num 1))
-              (union (f (Num 2)) (exp))
+              (union (f (Num 2)) (expensive))
               (extract (f (Num 2)))
             "#,
         )
         .unwrap();
     assert!(match &outputs[0] {
         CommandOutput::ExtractBest(termdag, _, term_id) => {
-            matches!(termdag.get(*term_id), Term::App(s, ..) if s == "exp")
+            matches!(termdag.get(*term_id), Term::App(s, ..) if s == "expensive")
         }
         _ => false,
     });
@@ -594,17 +594,17 @@ fn test_rewrite_subsumed_unextractable() {
             None,
             r#"
             (datatype Math)
-            (constructor exp () Math :cost 100)
+            (constructor expensive () Math :cost 100)
             (constructor cheap () Math :cost 1)
-            (rewrite (cheap) (exp) :subsume)
+            (rewrite (cheap) (expensive) :subsume)
             (cheap)
             (run 1)
             (extract (cheap))
             "#,
         )
         .unwrap();
     // Should give back expenive term, because cheap is unextractable
-    assert_eq!(outputs[1].to_string(), "(exp)\n");
+    assert_eq!(outputs[1].to_string(), "(expensive)\n");
 }
 
 #[test]
@@ -619,9 +619,9 @@ fn test_rewrite_subsumed() {
             None,
             r#"
             (datatype Math)
-            (constructor exp () Math :cost 100)
+            (constructor expensive () Math :cost 100)
             (constructor most-exp () Math :cost 1000)
-            (rewrite (most-exp) (exp) :subsume)
+            (rewrite (most-exp) (expensive) :subsume)
             (most-exp)
             (run 1)
             (constructor cheap () Math :cost 1)
@@ -631,7 +631,7 @@ fn test_rewrite_subsumed() {
             "#,
         )
         .unwrap();
-    assert_eq!(outputs[2].to_string(), "(exp)\n");
+    assert_eq!(outputs[2].to_string(), "(expensive)\n");
 }
 
 #[test]
@@ -745,9 +745,9 @@ fn test_value_to_classid() {
             None,
             r#"
             (datatype Math)
-            (constructor exp () Math )
-            (exp)
-            (extract (exp))
+            (constructor expensive () Math )
+            (expensive)
+            (extract (expensive))
             "#,
         )
         .unwrap();