init symbolic unop tests

test/sym/dune

@@ -7,4 +7,8 @@
   binop_i64.wast
   binop_f32.wast
   binop_f64.wast
+  unop_i32.wast
+  unop_i64.wast
+  unop_f32.wast
+  unop_f64.wast
  ))

test/sym/unop.t

@@ -0,0 +1,36 @@
+unop i32:
+  $ dune exec owi -- sym unop_i32.wast --no-stop-at-failure
+  Trap: unreachable
+  Model:
+    (model
+      (symbol_0 i32 (i32 0)))
+  Reached 1 problems!
+unop i64:
+  $ dune exec owi -- sym unop_i64.wast --no-stop-at-failure
+  Trap: unreachable
+  Model:
+    (model
+      (symbol_0 i64 (i64 0)))
+  Reached 1 problems!
+unop f32:
+  $ dune exec owi -- sym unop_f32.wast --no-stop-at-failure
+  Trap: unreachable
+  Model:
+    (model
+      (symbol_0 f32 (f32 42.000000)))
+  Trap: unreachable
+  Model:
+    (model
+      (symbol_0 f32 (f32 -0.000000)))
+  Reached 2 problems!
+unop f64:
+  $ dune exec owi -- sym unop_f64.wast --no-stop-at-failure
+  Trap: unreachable
+  Model:
+    (model
+      (symbol_0 f64 (f64 42.000000)))
+  Trap: unreachable
+  Model:
+    (model
+      (symbol_0 f64 (f64 -0.000000)))
+  Reached 2 problems!

test/sym/unop_f32.wast

@@ -0,0 +1,23 @@
+(module
+  (import "symbolic" "f32_symbol" (func $f32_symbol (result f32)))
+
+  (func $start
+    (local $x f32)
+
+    (local.set $x (call $f32_symbol))
+
+    (f32.ge (f32.abs (local.get $x)) (f32.const 42))
+    (if (then unreachable))
+
+    (f32.le (f32.neg (local.get $x)) (f32.const 42))
+    (if (then unreachable))
+
+    ;; File "lib/z3_mappings.ml", line 408, characters 32-38: Assertion failed
+    ;; (f32.ge (f32.ceil (local.get $x)) (f32.const 42))
+    ;; (if (then unreachable))
+    ;; (f32.le (f32.floor (local.get $x)) (f32.const 42))
+    ;; (if (then unreachable))
+  )
+
+  (start $start)
+)

test/sym/unop_f64.wast

@@ -0,0 +1,17 @@
+(module
+  (import "symbolic" "f64_symbol" (func $f64_symbol (result f64)))
+
+  (func $start
+    (local $x f64)
+
+    (local.set $x (call $f64_symbol))
+
+    (f64.ge (f64.abs (local.get $x)) (f64.const 42))
+    (if (then unreachable))
+
+    (f64.le (f64.neg (local.get $x)) (f64.const 42))
+    (if (then unreachable))
+  )
+
+  (start $start)
+)

test/sym/unop_i32.wast

@@ -0,0 +1,26 @@
+(module
+  (import "symbolic" "i32_symbol" (func $i32_symbol (result i32)))
+
+  (func $start
+    (local $x i32)
+
+    (local.set $x (call $i32_symbol))
+
+    (i32.eqz (local.get $x))
+    (if (then unreachable))
+
+    ;; Memo "lib/z3_mappings.ml" (to be implemented)
+    ;; Clz not supported yet
+    ;; (i32.ge_s (i32.const 2) (i32.clz (local.get $x)) )
+    ;; (if (then unreachable))
+    ;; Ctz: TODO
+    ;; (i32.ge_s (i32.const 2) (i32.ctz (local.get $x)) )
+    ;; (if (then unreachable))
+    ;; Popcnt: TODO
+    ;; (i32.ge_s (i32.const 2) (i32.popcnt (local.get $x)) )
+    ;; (if (then unreachable))
+
+  )
+
+  (start $start)
+)

test/sym/unop_i64.wast

@@ -0,0 +1,14 @@
+(module
+  (import "symbolic" "i64_symbol" (func $i64_symbol (result i64)))
+
+  (func $start
+    (local $x i64)
+
+    (local.set $x (call $i64_symbol))
+
+    (i64.eqz (local.get $x))
+    (if (then unreachable))
+  )
+
+  (start $start)
+)