{-# LANGUAGE LambdaCase #-}
module PropaFP.Translators.DReal where

import MixedTypesNumPrelude

import PropaFP.Expression

import Data.Ratio
import System.IO.Unsafe (unsafePerformIO)
import PropaFP.VarMap (TypedVarInterval(TypedVar), VarType (Real, Integer), TypedVarMap)

fToConjunction :: F -> [F]
fToConjunction :: F -> [F]
fToConjunction (FConn Conn
And F
f1 F
f2) = F -> [F]
fToConjunction F
f1 [F] -> [F] -> [F]
forall a. [a] -> [a] -> [a]
++ F -> [F]
fToConjunction F
f2
fToConjunction (FNot (FConn Conn
Or F
f1 F
f2)) = F -> [F]
fToConjunction (F -> F
FNot F
f1) [F] -> [F] -> [F]
forall a. [a] -> [a] -> [a]
++ F -> [F]
fToConjunction (F -> F
FNot F
f2)
fToConjunction (FNot (FConn Conn
Impl F
f1 F
f2)) = F -> [F]
fToConjunction F
f1 [F] -> [F] -> [F]
forall a. [a] -> [a] -> [a]
++ F -> [F]
fToConjunction (F -> F
FNot F
f2)
fToConjunction F
f = [F
f]

conjunctionToSMT :: [F] -> String
conjunctionToSMT :: [F] -> String
conjunctionToSMT []       = String
""
conjunctionToSMT (F
f : [F]
fs) = String
"(assert " String -> String -> String
forall a. [a] -> [a] -> [a]
++ F -> Integer -> String
formulaToSMT F
f Integer
1 String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
")\n" String -> String -> String
forall a. [a] -> [a] -> [a]
++ [F] -> String
conjunctionToSMT [F]
fs

formulaToSMT :: F -> Integer -> String
formulaToSMT :: F -> Integer -> String
formulaToSMT (FConn Conn
op F
f1 F
f2) Integer
numTabs = 
  case Conn
op of
    Conn
And   -> String
"\n" String -> String -> String
forall a. [a] -> [a] -> [a]
++ [String] -> String
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat (Integer -> String -> [String]
forall n a. CanBeInteger n => n -> a -> [a]
replicate Integer
numTabs String
"\t") String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"(and " String -> String -> String
forall a. [a] -> [a] -> [a]
++ F -> Integer -> String
formulaToSMT F
f1 (Integer
numTabs Integer -> Integer -> AddType Integer Integer
forall t1 t2. CanAddAsymmetric t1 t2 => t1 -> t2 -> AddType t1 t2
+ Integer
1) String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" " String -> String -> String
forall a. [a] -> [a] -> [a]
++ F -> Integer -> String
formulaToSMT F
f2 (Integer
numTabs Integer -> Integer -> AddType Integer Integer
forall t1 t2. CanAddAsymmetric t1 t2 => t1 -> t2 -> AddType t1 t2
+ Integer
1) String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
")"
    Conn
Or    -> String
"\n" String -> String -> String
forall a. [a] -> [a] -> [a]
++ [String] -> String
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat (Integer -> String -> [String]
forall n a. CanBeInteger n => n -> a -> [a]
replicate Integer
numTabs String
"\t") String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"(or " String -> String -> String
forall a. [a] -> [a] -> [a]
++ F -> Integer -> String
formulaToSMT F
f1 (Integer
numTabs Integer -> Integer -> AddType Integer Integer
forall t1 t2. CanAddAsymmetric t1 t2 => t1 -> t2 -> AddType t1 t2
+ Integer
1) String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" " String -> String -> String
forall a. [a] -> [a] -> [a]
++ F -> Integer -> String
formulaToSMT F
f2 (Integer
numTabs Integer -> Integer -> AddType Integer Integer
forall t1 t2. CanAddAsymmetric t1 t2 => t1 -> t2 -> AddType t1 t2
+ Integer
1) String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
")"
    Conn
Impl  -> String
"\n" String -> String -> String
forall a. [a] -> [a] -> [a]
++ [String] -> String
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat (Integer -> String -> [String]
forall n a. CanBeInteger n => n -> a -> [a]
replicate Integer
numTabs String
"\t") String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"(or " String -> String -> String
forall a. [a] -> [a] -> [a]
++ F -> Integer -> String
formulaToSMT (F -> F
FNot F
f1) (Integer
numTabs Integer -> Integer -> AddType Integer Integer
forall t1 t2. CanAddAsymmetric t1 t2 => t1 -> t2 -> AddType t1 t2
+ Integer
1) String -> String -> String
forall a. [a] -> [a] -> [a]
++ F -> Integer -> String
formulaToSMT F
f2 (Integer
numTabs Integer -> Integer -> AddType Integer Integer
forall t1 t2. CanAddAsymmetric t1 t2 => t1 -> t2 -> AddType t1 t2
+ Integer
1) String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
")"
formulaToSMT (FComp Comp
op E
e1 E
e2) Integer
numTabs = 
  case Comp
op of
    Comp
Ge -> String
"\n" String -> String -> String
forall a. [a] -> [a] -> [a]
++ [String] -> String
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat (Integer -> String -> [String]
forall n a. CanBeInteger n => n -> a -> [a]
replicate Integer
numTabs String
"\t") String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"(>= " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"\n" String -> String -> String
forall a. [a] -> [a] -> [a]
++ [String] -> String
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat (Integer -> String -> [String]
forall n a. CanBeInteger n => n -> a -> [a]
replicate (Integer
numTabs Integer -> Integer -> AddType Integer Integer
forall t1 t2. CanAddAsymmetric t1 t2 => t1 -> t2 -> AddType t1 t2
+ Integer
1) String
"\t") String -> String -> String
forall a. [a] -> [a] -> [a]
++ E -> String
expressionToSMT E
e1 String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"\n" String -> String -> String
forall a. [a] -> [a] -> [a]
++ [String] -> String
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat (Integer -> String -> [String]
forall n a. CanBeInteger n => n -> a -> [a]
replicate (Integer
numTabs Integer -> Integer -> AddType Integer Integer
forall t1 t2. CanAddAsymmetric t1 t2 => t1 -> t2 -> AddType t1 t2
+ Integer
1) String
"\t") String -> String -> String
forall a. [a] -> [a] -> [a]
++ E -> String
expressionToSMT E
e2 String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
")"
    Comp
Gt -> String
"\n" String -> String -> String
forall a. [a] -> [a] -> [a]
++ [String] -> String
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat (Integer -> String -> [String]
forall n a. CanBeInteger n => n -> a -> [a]
replicate Integer
numTabs String
"\t") String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"(> "  String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"\n" String -> String -> String
forall a. [a] -> [a] -> [a]
++ [String] -> String
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat (Integer -> String -> [String]
forall n a. CanBeInteger n => n -> a -> [a]
replicate (Integer
numTabs Integer -> Integer -> AddType Integer Integer
forall t1 t2. CanAddAsymmetric t1 t2 => t1 -> t2 -> AddType t1 t2
+ Integer
1) String
"\t") String -> String -> String
forall a. [a] -> [a] -> [a]
++ E -> String
expressionToSMT E
e1 String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"\n" String -> String -> String
forall a. [a] -> [a] -> [a]
++ [String] -> String
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat (Integer -> String -> [String]
forall n a. CanBeInteger n => n -> a -> [a]
replicate (Integer
numTabs Integer -> Integer -> AddType Integer Integer
forall t1 t2. CanAddAsymmetric t1 t2 => t1 -> t2 -> AddType t1 t2
+ Integer
1) String
"\t") String -> String -> String
forall a. [a] -> [a] -> [a]
++ E -> String
expressionToSMT E
e2 String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
")"
    Comp
Lt -> String
"\n" String -> String -> String
forall a. [a] -> [a] -> [a]
++ [String] -> String
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat (Integer -> String -> [String]
forall n a. CanBeInteger n => n -> a -> [a]
replicate Integer
numTabs String
"\t") String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"(< "  String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"\n" String -> String -> String
forall a. [a] -> [a] -> [a]
++ [String] -> String
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat (Integer -> String -> [String]
forall n a. CanBeInteger n => n -> a -> [a]
replicate (Integer
numTabs Integer -> Integer -> AddType Integer Integer
forall t1 t2. CanAddAsymmetric t1 t2 => t1 -> t2 -> AddType t1 t2
+ Integer
1) String
"\t") String -> String -> String
forall a. [a] -> [a] -> [a]
++ E -> String
expressionToSMT E
e1 String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"\n" String -> String -> String
forall a. [a] -> [a] -> [a]
++ [String] -> String
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat (Integer -> String -> [String]
forall n a. CanBeInteger n => n -> a -> [a]
replicate (Integer
numTabs Integer -> Integer -> AddType Integer Integer
forall t1 t2. CanAddAsymmetric t1 t2 => t1 -> t2 -> AddType t1 t2
+ Integer
1) String
"\t") String -> String -> String
forall a. [a] -> [a] -> [a]
++ E -> String
expressionToSMT E
e2 String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
")"
    Comp
Le -> String
"\n" String -> String -> String
forall a. [a] -> [a] -> [a]
++ [String] -> String
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat (Integer -> String -> [String]
forall n a. CanBeInteger n => n -> a -> [a]
replicate Integer
numTabs String
"\t") String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"(<= " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"\n" String -> String -> String
forall a. [a] -> [a] -> [a]
++ [String] -> String
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat (Integer -> String -> [String]
forall n a. CanBeInteger n => n -> a -> [a]
replicate (Integer
numTabs Integer -> Integer -> AddType Integer Integer
forall t1 t2. CanAddAsymmetric t1 t2 => t1 -> t2 -> AddType t1 t2
+ Integer
1) String
"\t") String -> String -> String
forall a. [a] -> [a] -> [a]
++ E -> String
expressionToSMT E
e1 String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"\n" String -> String -> String
forall a. [a] -> [a] -> [a]
++ [String] -> String
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat (Integer -> String -> [String]
forall n a. CanBeInteger n => n -> a -> [a]
replicate (Integer
numTabs Integer -> Integer -> AddType Integer Integer
forall t1 t2. CanAddAsymmetric t1 t2 => t1 -> t2 -> AddType t1 t2
+ Integer
1) String
"\t") String -> String -> String
forall a. [a] -> [a] -> [a]
++ E -> String
expressionToSMT E
e2 String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
")"
    Comp
Eq -> String
"\n" String -> String -> String
forall a. [a] -> [a] -> [a]
++ [String] -> String
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat (Integer -> String -> [String]
forall n a. CanBeInteger n => n -> a -> [a]
replicate Integer
numTabs String
"\t") String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"(= "  String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"\n" String -> String -> String
forall a. [a] -> [a] -> [a]
++ [String] -> String
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat (Integer -> String -> [String]
forall n a. CanBeInteger n => n -> a -> [a]
replicate (Integer
numTabs Integer -> Integer -> AddType Integer Integer
forall t1 t2. CanAddAsymmetric t1 t2 => t1 -> t2 -> AddType t1 t2
+ Integer
1) String
"\t") String -> String -> String
forall a. [a] -> [a] -> [a]
++ E -> String
expressionToSMT E
e1 String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"\n" String -> String -> String
forall a. [a] -> [a] -> [a]
++ [String] -> String
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat (Integer -> String -> [String]
forall n a. CanBeInteger n => n -> a -> [a]
replicate (Integer
numTabs Integer -> Integer -> AddType Integer Integer
forall t1 t2. CanAddAsymmetric t1 t2 => t1 -> t2 -> AddType t1 t2
+ Integer
1) String
"\t") String -> String -> String
forall a. [a] -> [a] -> [a]
++ E -> String
expressionToSMT E
e2 String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
")"
formulaToSMT (FNot F
f) Integer
numTabs = String
"\n" String -> String -> String
forall a. [a] -> [a] -> [a]
++ [String] -> String
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat (Integer -> String -> [String]
forall n a. CanBeInteger n => n -> a -> [a]
replicate Integer
numTabs String
"\t") String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"(not " String -> String -> String
forall a. [a] -> [a] -> [a]
++ F -> Integer -> String
formulaToSMT F
f (Integer
numTabs Integer -> Integer -> AddType Integer Integer
forall t1 t2. CanAddAsymmetric t1 t2 => t1 -> t2 -> AddType t1 t2
+ Integer
1) String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
")"
formulaToSMT F
FTrue Integer
numTabs = String
"\n" String -> String -> String
forall a. [a] -> [a] -> [a]
++ [String] -> String
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat (Integer -> String -> [String]
forall n a. CanBeInteger n => n -> a -> [a]
replicate Integer
numTabs String
"\t") String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"true"
formulaToSMT F
FFalse Integer
numTabs = String
"\n" String -> String -> String
forall a. [a] -> [a] -> [a]
++ [String] -> String
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat (Integer -> String -> [String]
forall n a. CanBeInteger n => n -> a -> [a]
replicate Integer
numTabs String
"\t") String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"false"

expressionToSMT :: E -> String
expressionToSMT :: E -> String
expressionToSMT (EBinOp BinOp
op E
e1 E
e2) =
  case BinOp
op of
    BinOp
Add -> String
"(+ " String -> String -> String
forall a. [a] -> [a] -> [a]
++ E -> String
expressionToSMT E
e1 String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" " String -> String -> String
forall a. [a] -> [a] -> [a]
++ E -> String
expressionToSMT E
e2 String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
")"
    BinOp
Sub -> String
"(- " String -> String -> String
forall a. [a] -> [a] -> [a]
++ E -> String
expressionToSMT E
e1 String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" " String -> String -> String
forall a. [a] -> [a] -> [a]
++ E -> String
expressionToSMT E
e2 String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
")"
    BinOp
Mul -> String
"(* " String -> String -> String
forall a. [a] -> [a] -> [a]
++ E -> String
expressionToSMT E
e1 String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" " String -> String -> String
forall a. [a] -> [a] -> [a]
++ E -> String
expressionToSMT E
e2 String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
")"
    BinOp
Div -> String
"(/ " String -> String -> String
forall a. [a] -> [a] -> [a]
++ E -> String
expressionToSMT E
e1 String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" " String -> String -> String
forall a. [a] -> [a] -> [a]
++ E -> String
expressionToSMT E
e2 String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
")"
    BinOp
Min -> String
"(min " String -> String -> String
forall a. [a] -> [a] -> [a]
++ E -> String
expressionToSMT E
e1 String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" " String -> String -> String
forall a. [a] -> [a] -> [a]
++ E -> String
expressionToSMT E
e2 String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
")"
    BinOp
Max -> String
"(max " String -> String -> String
forall a. [a] -> [a] -> [a]
++ E -> String
expressionToSMT E
e1 String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" " String -> String -> String
forall a. [a] -> [a] -> [a]
++ E -> String
expressionToSMT E
e2 String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
")"
    BinOp
Pow -> String
"(^ "  String -> String -> String
forall a. [a] -> [a] -> [a]
++ E -> String
expressionToSMT E
e1 String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" " String -> String -> String
forall a. [a] -> [a] -> [a]
++ E -> String
expressionToSMT E
e2 String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
")"
    BinOp
Mod -> String
"(mod "  String -> String -> String
forall a. [a] -> [a] -> [a]
++ E -> String
expressionToSMT E
e1 String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" " String -> String -> String
forall a. [a] -> [a] -> [a]
++ E -> String
expressionToSMT E
e2 String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
")" --TODO: Warn dreal users
expressionToSMT (EUnOp UnOp
op E
e) =
  case UnOp
op of
    UnOp
Sqrt -> String
"(sqrt " String -> String -> String
forall a. [a] -> [a] -> [a]
++ E -> String
expressionToSMT E
e String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
")"
    UnOp
Negate -> String
"(* -1 " String -> String -> String
forall a. [a] -> [a] -> [a]
++ E -> String
expressionToSMT E
e String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
")"
    UnOp
Abs -> String
"(abs " String -> String -> String
forall a. [a] -> [a] -> [a]
++ E -> String
expressionToSMT E
e String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
")"
    UnOp
Sin -> String
"(sin " String -> String -> String
forall a. [a] -> [a] -> [a]
++ E -> String
expressionToSMT E
e String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
")"
    UnOp
Cos -> String
"(cos " String -> String -> String
forall a. [a] -> [a] -> [a]
++ E -> String
expressionToSMT E
e String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
")"
expressionToSMT (PowI E
e Integer
i) = String
"(^ " String -> String -> String
forall a. [a] -> [a] -> [a]
++ E -> String
expressionToSMT E
e String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Integer -> String
forall a. Show a => a -> String
show Integer
i String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
")"
expressionToSMT (Var String
e) = String
e
expressionToSMT (Lit Rational
e) = 
  case Rational -> Integer
forall a. Ratio a -> a
denominator Rational
e of
    Integer
1 -> Integer -> String
forall a. Show a => a -> String
show Integer
numE
    Integer
_ -> String
"(/ " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Integer -> String
forall a. Show a => a -> String
show Integer
numE String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Integer -> String
forall a. Show a => a -> String
show Integer
denE String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
")"
    where
      numE :: Integer
numE = Rational -> Integer
forall a. Ratio a -> a
numerator Rational
e
      denE :: Integer
denE = Rational -> Integer
forall a. Ratio a -> a
denominator Rational
e
expressionToSMT E
Pi = String
"(* 4.0 (atan 1.0))" -- Equivalent to pi
expressionToSMT (RoundToInteger RoundingMode
mode E
e) = 
  -- TODO: Warn about non-standard SMT
  case RoundingMode
mode of
    RoundingMode
RNE -> String
"(to_int_rne " String -> String -> String
forall a. [a] -> [a] -> [a]
++ E -> String
expressionToSMT E
e String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
")"
    RoundingMode
RTP -> String
"(to_int_rtp " String -> String -> String
forall a. [a] -> [a] -> [a]
++ E -> String
expressionToSMT E
e String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
")"
    RoundingMode
RTN -> String
"(to_int_rtn " String -> String -> String
forall a. [a] -> [a] -> [a]
++ E -> String
expressionToSMT E
e String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
")"
    RoundingMode
RTZ -> String
"(to_int_rtz " String -> String -> String
forall a. [a] -> [a] -> [a]
++ E -> String
expressionToSMT E
e String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
")"
    RoundingMode
RNA -> String
"(to_int_rna " String -> String -> String
forall a. [a] -> [a] -> [a]
++ E -> String
expressionToSMT E
e String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
")"
expressionToSMT (Float RoundingMode
mode E
e)   = String -> String
forall a. HasCallStack => String -> a
error String
"Float with unknown precision not supported"
  -- TODO: Warn about non-standard SMT
--   case mode of
--     RNE -> "(float_rne " ++ expressionToSMT e ++ ")"
--     RTP -> "(float_rtp " ++ expressionToSMT e ++ ")"
--     RTN -> "(float_rtn " ++ expressionToSMT e ++ ")"
--     RTZ -> "(float_rtz " ++ expressionToSMT e ++ ")"
--     RNA -> "(float_rne " ++ expressionToSMT e ++ ")"
expressionToSMT (Float32 RoundingMode
mode E
e) =
  -- TODO: Warn about non-standard SMT
  case RoundingMode
mode of
    RoundingMode
RNE -> String
"(float32_rne " String -> String -> String
forall a. [a] -> [a] -> [a]
++ E -> String
expressionToSMT E
e String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
")"
    RoundingMode
RTP -> String
"(float32_rtp " String -> String -> String
forall a. [a] -> [a] -> [a]
++ E -> String
expressionToSMT E
e String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
")"
    RoundingMode
RTN -> String
"(float32_rtn " String -> String -> String
forall a. [a] -> [a] -> [a]
++ E -> String
expressionToSMT E
e String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
")"
    RoundingMode
RTZ -> String
"(float32_rtz " String -> String -> String
forall a. [a] -> [a] -> [a]
++ E -> String
expressionToSMT E
e String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
")"
    RoundingMode
RNA -> String
"(float32_rne " String -> String -> String
forall a. [a] -> [a] -> [a]
++ E -> String
expressionToSMT E
e String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
")"
expressionToSMT (Float64 RoundingMode
mode E
e) =
  -- TODO: Warn about non-standard SMT
  case RoundingMode
mode of
    RoundingMode
RNE -> String
"(float64_rne " String -> String -> String
forall a. [a] -> [a] -> [a]
++ E -> String
expressionToSMT E
e String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
")"
    RoundingMode
RTP -> String
"(float64_rtp " String -> String -> String
forall a. [a] -> [a] -> [a]
++ E -> String
expressionToSMT E
e String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
")"
    RoundingMode
RTN -> String
"(float64_rtn " String -> String -> String
forall a. [a] -> [a] -> [a]
++ E -> String
expressionToSMT E
e String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
")"
    RoundingMode
RTZ -> String
"(float64_rtz " String -> String -> String
forall a. [a] -> [a] -> [a]
++ E -> String
expressionToSMT E
e String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
")"
    RoundingMode
RNA -> String
"(float64_rne " String -> String -> String
forall a. [a] -> [a] -> [a]
++ E -> String
expressionToSMT E
e String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
")"

formulaAndVarMapToDReal :: F -> TypedVarMap -> String
formulaAndVarMapToDReal :: F -> TypedVarMap -> String
formulaAndVarMapToDReal F
f TypedVarMap
typedVarMap =
  String
"(set-logic QF_NRA)\n" String -> String -> String
forall a. [a] -> [a] -> [a]
++
  TypedVarMap -> String
variablesAsString TypedVarMap
typedVarMap String -> String -> String
forall a. [a] -> [a] -> [a]
++
  ([F] -> String
conjunctionToSMT ([F] -> String) -> (F -> [F]) -> F -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. F -> [F]
fToConjunction) F
f String -> String -> String
forall a. [a] -> [a] -> [a]
++
  String
"(check-sat)\n" String -> String -> String
forall a. [a] -> [a] -> [a]
++
  String
"(get-model)\n" String -> String -> String
forall a. [a] -> [a] -> [a]
++
  String
"(exit)\n"
  where
    showVarType :: VarType -> String
showVarType VarType
Integer = String
"Int"
    showVarType VarType
Real = String
"Real"
      
    showRational :: Ratio a -> String
showRational Ratio a
x = String
"(/ " String -> String -> String
forall a. [a] -> [a] -> [a]
++ a -> String
forall a. Show a => a -> String
show (Ratio a -> a
forall a. Ratio a -> a
numerator Ratio a
x) String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" " String -> String -> String
forall a. [a] -> [a] -> [a]
++ a -> String
forall a. Show a => a -> String
show (Ratio a -> a
forall a. Ratio a -> a
denominator Ratio a
x) String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
")"

    variablesAsString :: TypedVarMap -> String
variablesAsString [] = String
""
    variablesAsString ((TypedVar (String
varName, (Rational
leftBound, Rational
rightBound)) VarType
varType) : TypedVarMap
typedVarIntervals) =
      String
"(declare-fun " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
varName String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" () " String -> String -> String
forall a. [a] -> [a] -> [a]
++ VarType -> String
showVarType VarType
varType String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
")\n" String -> String -> String
forall a. [a] -> [a] -> [a]
++
      String
"(assert (<= " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Rational -> String
forall {a}. Show a => Ratio a -> String
showRational Rational
leftBound String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
varName String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"))\n" String -> String -> String
forall a. [a] -> [a] -> [a]
++
      String
"(assert (<= " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
varName String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Rational -> String
forall {a}. Show a => Ratio a -> String
showRational Rational
rightBound String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"))\n" String -> String -> String
forall a. [a] -> [a] -> [a]
++ TypedVarMap -> String
variablesAsString TypedVarMap
typedVarIntervals

disjunctionExpressionsToSMT :: [ESafe] -> String
disjunctionExpressionsToSMT :: [ESafe] -> String
disjunctionExpressionsToSMT [ESafe]
es = 
  String
"\n\t\t\t(or " String -> String -> String
forall a. [a] -> [a] -> [a]
++ 
    (ESafe -> String) -> [ESafe] -> String
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap 
    (\case
      EStrict E
e    -> String
"\n\t\t\t\t(> " String -> String -> String
forall a. [a] -> [a] -> [a]
++ E -> String
expressionToSMT E
e String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" 0)"
      ENonStrict E
e -> String
"\n\t\t\t\t(>= " String -> String -> String
forall a. [a] -> [a] -> [a]
++ E -> String
expressionToSMT E
e String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" 0)"
    ) 
    [ESafe]
es String -> String -> String
forall a. [a] -> [a] -> [a]
++ 
  String
")"

cnfExpressionsToSMT :: [[ESafe]] -> String
cnfExpressionsToSMT :: [[ESafe]] -> String
cnfExpressionsToSMT [[ESafe]]
disjunctions = String
"\n\t\t(and " String -> String -> String
forall a. [a] -> [a] -> [a]
++ ([ESafe] -> String) -> [[ESafe]] -> String
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap [ESafe] -> String
disjunctionExpressionsToSMT [[ESafe]]
disjunctions String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
")"

cnfExpressionAndDomainsToDreal :: [[ESafe]] -> [(String, (Rational, Rational))] -> [(String, (Rational, Rational))] -> String
cnfExpressionAndDomainsToDreal :: [[ESafe]]
-> [(String, (Rational, Rational))]
-> [(String, (Rational, Rational))]
-> String
cnfExpressionAndDomainsToDreal [[ESafe]]
cnf [(String, (Rational, Rational))]
realDomains [(String, (Rational, Rational))]
intDomains =
  String
"(set-option :precision 1e-300)" String -> String -> String
forall a. [a] -> [a] -> [a]
++
  String
"\n(assert " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String -> String
forAll ([[ESafe]] -> String
cnfExpressionsToSMT [[ESafe]]
cnf) String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
")\n(check-sat)\n(exit)"
  where
    forAll :: String -> String
forAll String
vc =
      String
"\n(forall (" String -> String -> String
forall a. [a] -> [a] -> [a]
++ ((String, (Rational, Rational)) -> String)
-> [(String, (Rational, Rational))] -> String
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (\(String
v, (Rational
_, Rational
_)) -> String
"\n\t(" String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
v String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" Real)") [(String, (Rational, Rational))]
realDomains String -> String -> String
forall a. [a] -> [a] -> [a]
++ ((String, (Rational, Rational)) -> String)
-> [(String, (Rational, Rational))] -> String
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (\(String
v, (Rational
_, Rational
_)) -> String
"\n\t(" String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
v String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" Int)") [(String, (Rational, Rational))]
intDomains String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"\n)" String -> String -> String
forall a. [a] -> [a] -> [a]
++ 
      String
"\n\t(=>" String -> String -> String
forall a. [a] -> [a] -> [a]
++ 
      String
"\n\t\t(and " String -> String -> String
forall a. [a] -> [a] -> [a]
++ ((String, (Rational, Rational)) -> String)
-> [(String, (Rational, Rational))] -> String
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (\(String
v, (Rational
vL, Rational
vR)) -> String
"\n\t\t\t(>= " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
v String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" " String -> String -> String
forall a. [a] -> [a] -> [a]
++ E -> String
expressionToSMT (Rational -> E
Lit Rational
vL) String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
") (<= " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
v String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" " String -> String -> String
forall a. [a] -> [a] -> [a]
++ E -> String
expressionToSMT (Rational -> E
Lit Rational
vR) String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
")") ([(String, (Rational, Rational))]
realDomains [(String, (Rational, Rational))]
-> [(String, (Rational, Rational))]
-> [(String, (Rational, Rational))]
forall a. [a] -> [a] -> [a]
++ [(String, (Rational, Rational))]
intDomains) String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"\n\t\t)" String -> String -> String
forall a. [a] -> [a] -> [a]
++
      String
vc String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"))"   
    -- forAll vc =
    --   "(forall (" ++ concatMap (\(v, (_, _)) -> "(" ++ v ++ " Real)") realDomains ++ concatMap (\(v, (_, _)) -> "(" ++ v ++ " Int)") intDomains ++ ")" ++ 
    --   "(=>" ++ 
    --   "(and " ++ concatMap (\(v, (vL, vR)) -> "(>= " ++ v ++ " " ++ expressionToSMT (Lit vL) ++ ")(<= " ++ v ++ " " ++ expressionToSMT (Lit vR) ++ ")") (realDomains ++ intDomains) ++ ")" ++
    --   vc ++ "))"

runDRealTranslatorCNFWithVarMap :: [[ESafe]] -> [(String, (Rational, Rational))] -> [(String, (Rational, Rational))] -> IO ()
runDRealTranslatorCNFWithVarMap :: [[ESafe]]
-> [(String, (Rational, Rational))]
-> [(String, (Rational, Rational))]
-> IO ()
runDRealTranslatorCNFWithVarMap [[ESafe]]
cnf [(String, (Rational, Rational))]
realVarMap [(String, (Rational, Rational))]
intVarMap =
  do
  String -> IO ()
putStrLn String
"Running Haskell to dReal translator for Expressions"
  String -> IO ()
putStr String
"Enter target file name: "
  String
fileName <- IO String
getLine
  String -> String -> IO ()
writeFile String
fileName (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$ [[ESafe]]
-> [(String, (Rational, Rational))]
-> [(String, (Rational, Rational))]
-> String
cnfExpressionAndDomainsToDreal [[ESafe]]
cnf [(String, (Rational, Rational))]
realVarMap [(String, (Rational, Rational))]
intVarMap

runDRealTranslatorCNF :: [[ESafe]] -> IO ()
runDRealTranslatorCNF :: [[ESafe]] -> IO ()
runDRealTranslatorCNF [[ESafe]]
cnf = do
  String -> IO ()
putStrLn String
"Running Haskell to dReal translator for Expressions"
  -- PutStr "Enter tool: "
  String -> IO ()
putStr String
"Enter target file name: "
  String
fileName <- IO String
getLine
  String -> IO ()
putStr String
"How many Real vars in expression? "
  String
numReals <- IO String
getLine
  String -> IO ()
putStr String
"How many Int vars in expression? "
  String
numInts <- IO String
getLine
  String -> String -> IO ()
writeFile String
fileName ([[ESafe]]
-> [(String, (Rational, Rational))]
-> [(String, (Rational, Rational))]
-> String
cnfExpressionAndDomainsToDreal [[ESafe]]
cnf (String -> Integer -> [(String, (Rational, Rational))]
parseDomains String
"real var name? " (String -> Integer
forall a. Read a => String -> a
read String
numReals)) (String -> Integer -> [(String, (Rational, Rational))]
parseDomains String
"integer var name? " (String -> Integer
forall a. Read a => String -> a
read String
numInts)))
  where
    parseDomains :: String -> Integer -> [(String, (Rational, Rational))]
    parseDomains :: String -> Integer -> [(String, (Rational, Rational))]
parseDomains String
_ Integer
0 = []
    parseDomains String
msg Integer
n =

      (IO String -> String
forall a. IO a -> a
unsafePerformIO (String -> IO String
getVar String
msg), (IO Rational -> Rational
forall a. IO a -> a
unsafePerformIO (String -> IO Rational
parseRational String
"lower bound") :: Rational, IO Rational -> Rational
forall a. IO a -> a
unsafePerformIO (String -> IO Rational
parseRational String
"upper bound") :: Rational))
      (String, (Rational, Rational))
-> [(String, (Rational, Rational))]
-> [(String, (Rational, Rational))]
forall a. a -> [a] -> [a]
: String -> Integer -> [(String, (Rational, Rational))]
parseDomains String
msg (Integer
n Integer -> Integer -> SubType Integer Integer
forall t1 t2. CanSub t1 t2 => t1 -> t2 -> SubType t1 t2
- Integer
1)

    getVar :: String -> IO String
getVar String
message = do
      String -> IO ()
putStr String
message
      IO String
getLine

    parseRational :: String -> IO Rational
parseRational String
message = do
      String -> IO ()
putStr (String
message String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" numerator? ")
      String
num <- IO String
getLine
      String -> IO ()
putStr (String
message String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" denominator? ")
      String
den <- IO String
getLine
      Rational -> IO Rational
forall (m :: * -> *) a. Monad m => a -> m a
return ((String -> Integer
forall a. Read a => String -> a
read String
num :: Integer) Integer -> Integer -> DivType Integer Integer
forall t1 t2. CanDiv t1 t2 => t1 -> t2 -> DivType t1 t2
/ (String -> Integer
forall a. Read a => String -> a
read String
den :: Integer))