Pipe through "tan" and "tanh" in the SMTWriter. They are not

longer eagerly translated into ratios of sin* and cos*.

what4/src/What4/Protocol/SMTLib2.hs

@@ -549,9 +549,11 @@ instance SupportTermOps Term where
   realDiv x y = x SMT2../ [y]
   realSin = un_app "sin"
   realCos = un_app "cos"
+  realTan = un_app "tan"
   realATan2 = bin_app "atan2"
   realSinh = un_app "sinh"
   realCosh = un_app "cosh"
+  realTanh = un_app "tanh"
   realExp = un_app "exp"
   realLog = un_app "log"
 

what4/src/What4/Protocol/SMTWriter.hs

@@ -429,17 +429,16 @@ class Num v => SupportTermOps v where
   realDiv :: v -> v -> v
 
   realSin :: v -> v
-
   realCos :: v -> v
+  realTan :: v -> v
 
   realATan2 :: v -> v -> v
 
   realSinh :: v -> v
-
   realCosh :: v -> v
+  realTanh :: v -> v
 
   realExp  :: v -> v
-
   realLog  :: v -> v
 
   -- | Apply the arguments to the given function.
@@ -2148,8 +2147,10 @@ appSMTExpr ae = do
       case fn of
         SFn.Sin  -> sf1 realSin  args
         SFn.Cos  -> sf1 realCos  args
+        SFn.Tan  -> sf1 realTan  args
         SFn.Sinh -> sf1 realSinh args
         SFn.Cosh -> sf1 realCosh args
+        SFn.Tanh -> sf1 realTanh args
         SFn.Exp  -> sf1 realExp  args
         SFn.Log  -> sf1 realLog  args
         SFn.Arctan2 ->

what4/src/What4/Solver/Yices.hs

@@ -279,9 +279,11 @@ instance SupportTermOps YicesTerm where
   realDiv x y = term_app "/" [x, y]
   realSin = errorComputableUnsupported
   realCos = errorComputableUnsupported
+  realTan = errorComputableUnsupported
   realATan2 = errorComputableUnsupported
   realSinh = errorComputableUnsupported
   realCosh = errorComputableUnsupported
+  realTanh = errorComputableUnsupported
   realExp = errorComputableUnsupported
   realLog = errorComputableUnsupported