diff --git a/src/lib.rs b/src/lib.rs index 83166e60c..cab0b69ac 100644 --- a/src/lib.rs +++ b/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"); } } diff --git a/src/sort/f64.rs b/src/sort/f64.rs index b6926112f..84c8ebf83 100755 --- a/src/sort/f64.rs +++ b/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)) }); diff --git a/tests/f64.egg b/tests/f64.egg index 23301bfea..6eb26708e 100644 --- a/tests/f64.egg +++ b/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)) diff --git a/tests/integration_test.rs b/tests/integration_test.rs index 2826b33e1..84e8554eb 100644 --- a/tests/integration_test.rs +++ b/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,9 +594,9 @@ 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)) @@ -604,7 +604,7 @@ fn test_rewrite_subsumed_unextractable() { ) .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();