{-# LANGUAGE TupleSections #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE LambdaCase #-}
module PropaFP.Parsers.DRealSmt where

import MixedTypesNumPrelude
import PropaFP.Expression
import qualified PropaFP.Parsers.Lisp.DataTypes as LD
import PropaFP.VarMap
import PropaFP.Parsers.Smt

-- | Parser for SMT files produced by the dReal Translator.
-- 
-- The DReal SMT file will have the first line declaring the SMT logic, which we ignore.
-- The next few lines declare variables (if any)
-- A variable is declared in the following format
-- (declare-fun varName () varType) where varType can be Int or Real
-- (assert (<= lowerBound varName))
-- (assert (<= varName upperBound))
-- 
-- Both lowerBound and upperBound will be rationals, though can be safely converted to Integer for Int vars
-- 
-- Once the declare-fun lines end, we have an assert which contains the entire VC as an argument
-- The rest of the file can be ignored (it will be (check-sat), (get-model), and (exit))
parseDRealSmtToF :: [LD.Expression] -> (Maybe F, TypedVarMap)
parseDRealSmtToF :: [Expression] -> (Maybe F, TypedVarMap)
parseDRealSmtToF [Expression]
parsedExpressions =
  ([Expression] -> Maybe F
parseDRealVCs ([Expression] -> [Expression]
findAssertions [Expression]
parsedVC), TypedVarMap
typedVarMap)
  where
   (Expression
_smtLogic : [Expression]
varsWithParsedVC) = [Expression]
parsedExpressions
   ([Expression]
parsedVC, TypedVarMap
typedVarMap) = [Expression] -> ([Expression], TypedVarMap)
parseDRealVariables [Expression]
varsWithParsedVC

parseDRealVCs :: [LD.Expression] -> Maybe F
parseDRealVCs :: [Expression] -> Maybe F
parseDRealVCs []        = [Char] -> Maybe F
forall a. HasCallStack => [Char] -> a
error [Char]
"Processed parser: Given empty list of assertions"
parseDRealVCs [Expression
p1]      = Expression -> Maybe F
termDRealToF Expression
p1
parseDRealVCs (Expression
p1 : [Expression]
p2) = Conn -> F -> F -> F
FConn Conn
And (F -> F -> F) -> Maybe F -> Maybe (F -> F)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Expression -> Maybe F
termDRealToF Expression
p1 Maybe (F -> F) -> Maybe F -> Maybe F
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> [Expression] -> Maybe F
parseDRealVCs [Expression]
p2

parseDRealVC :: LD.Expression -> Maybe F
parseDRealVC :: Expression -> Maybe F
parseDRealVC (LD.Application (LD.Variable [Char]
"assert") [Expression
parsedVC]) = Expression -> Maybe F
termDRealToF Expression
parsedVC
parseDRealVC Expression
_ = Maybe F
forall a. Maybe a
Nothing
-- | Parses variables from a parsed file.
-- First item must be a variable declaration
-- Continues parsing variables until it reaches a non-variable assertion
-- Returns a TypedVarMap and the rest of the parsed file.
parseDRealVariables :: [LD.Expression] -> ([LD.Expression], TypedVarMap)
parseDRealVariables :: [Expression] -> ([Expression], TypedVarMap)
parseDRealVariables 
  (
    LD.Application (LD.Variable [Char]
"declare-fun") [LD.Variable [Char]
varName, Expression
LD.Null, LD.Variable [Char]
varType] :
    LD.Application (LD.Variable [Char]
"assert") [LD.Application (LD.Variable [Char]
"<=") [LD.Application (LD.Variable [Char]
"/") [LD.Number Rational
lowerNumerator, LD.Number Rational
lowerDenominator], LD.Variable [Char]
_]] :
    LD.Application (LD.Variable [Char]
"assert") [LD.Application (LD.Variable [Char]
"<=") [LD.Variable [Char]
_, LD.Application (LD.Variable [Char]
"/") [LD.Number Rational
upperNumerator, LD.Number Rational
upperDenominator]]] :
    [Expression]
parsedExpressions
  ) =
    let
      ([Expression]
remainingExpressions, TypedVarMap
parsedVarMap) = [Expression] -> ([Expression], TypedVarMap)
parseDRealVariables [Expression]
parsedExpressions
      parsedVarType :: VarType
parsedVarType = 
        case [Char]
varType of
          [Char]
"Real" -> VarType
Real
          [Char]
"Int" -> VarType
Integer
          [Char]
_ -> [Char] -> VarType
forall a. HasCallStack => [Char] -> a
error [Char]
"Unrecognized varType in given dReal SMT file"
    in
      ([Expression]
remainingExpressions, VarInterval -> VarType -> TypedVarInterval
TypedVar ([Char]
varName, (Rational
lowerNumerator Rational -> Rational -> DivType Rational Rational
forall t1 t2. CanDiv t1 t2 => t1 -> t2 -> DivType t1 t2
/ Rational
lowerDenominator, Rational
upperNumerator Rational -> Rational -> DivType Rational Rational
forall t1 t2. CanDiv t1 t2 => t1 -> t2 -> DivType t1 t2
/ Rational
upperDenominator)) VarType
parsedVarType TypedVarInterval -> TypedVarMap -> TypedVarMap
forall a. a -> [a] -> [a]
: TypedVarMap
parsedVarMap)
parseDRealVariables [Expression]
parsedExpressions = ([Expression]
parsedExpressions, [])

termDRealToF :: LD.Expression -> Maybe F
-- FConn
termDRealToF :: Expression -> Maybe F
termDRealToF (LD.Application (LD.Variable [Char]
"and") [Expression
p1, Expression
p2]) = Conn -> F -> F -> F
FConn Conn
And (F -> F -> F) -> Maybe F -> Maybe (F -> F)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Expression -> Maybe F
termDRealToF Expression
p1 Maybe (F -> F) -> Maybe F -> Maybe F
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Expression -> Maybe F
termDRealToF Expression
p2
-- termDRealToF (LD.Application (LD.Variable "or") [LD.Application (LD.Variable "not") [p1], p2])  = FConn Impl <$> termDRealToF p1 <*> termDRealToF p2
termDRealToF (LD.Application (LD.Variable [Char]
"or") [Expression
p1, Expression
p2])  = Conn -> F -> F -> F
FConn Conn
Or (F -> F -> F) -> Maybe F -> Maybe (F -> F)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Expression -> Maybe F
termDRealToF Expression
p1 Maybe (F -> F) -> Maybe F -> Maybe F
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Expression -> Maybe F
termDRealToF Expression
p2 --TODO: parse OR (NOT p1) p2 as impl? possible but is there any benefit?
-- Special case for =
termDRealToF (LD.Application (LD.Variable [Char]
"=") [Expression
p1, Expression
p2])   = 
  case (Expression -> Maybe F
termDRealToF Expression
p1, Expression -> Maybe F
termDRealToF Expression
p2) of
    (Just F
f1, Just F
f2) -> F -> Maybe F
forall a. a -> Maybe a
Just (F -> Maybe F) -> F -> Maybe F
forall a b. (a -> b) -> a -> b
$ Conn -> F -> F -> F
FConn Conn
And (Conn -> F -> F -> F
FConn Conn
Impl F
f1 F
f2) (Conn -> F -> F -> F
FConn Conn
Impl F
f2 F
f1)
    (Maybe F
Nothing, Maybe F
Nothing) ->
      case (Expression -> Maybe E
termDRealToE Expression
p1, Expression -> Maybe E
termDRealToE Expression
p2) of
        (Just E
e1, Just E
e2) -> F -> Maybe F
forall a. a -> Maybe a
Just (F -> Maybe F) -> F -> Maybe F
forall a b. (a -> b) -> a -> b
$ Comp -> E -> E -> F
FComp Comp
Eq E
e1 E
e2
        (Maybe E
_, Maybe E
_) -> Maybe F
forall a. Maybe a
Nothing
    (Maybe F
_, Maybe F
_) -> Maybe F
forall a. Maybe a
Nothing
-- FComp
termDRealToF (LD.Application (LD.Variable [Char]
">=") [Expression
p1, Expression
p2])  = Comp -> E -> E -> F
FComp Comp
Ge (E -> E -> F) -> Maybe E -> Maybe (E -> F)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Expression -> Maybe E
termDRealToE Expression
p1 Maybe (E -> F) -> Maybe E -> Maybe F
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Expression -> Maybe E
termDRealToE Expression
p2
termDRealToF (LD.Application (LD.Variable [Char]
">") [Expression
p1, Expression
p2])   = Comp -> E -> E -> F
FComp Comp
Gt (E -> E -> F) -> Maybe E -> Maybe (E -> F)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Expression -> Maybe E
termDRealToE Expression
p1 Maybe (E -> F) -> Maybe E -> Maybe F
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Expression -> Maybe E
termDRealToE Expression
p2
termDRealToF (LD.Application (LD.Variable [Char]
"<=") [Expression
p1, Expression
p2])  = Comp -> E -> E -> F
FComp Comp
Le (E -> E -> F) -> Maybe E -> Maybe (E -> F)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Expression -> Maybe E
termDRealToE Expression
p1 Maybe (E -> F) -> Maybe E -> Maybe F
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Expression -> Maybe E
termDRealToE Expression
p2
termDRealToF (LD.Application (LD.Variable [Char]
"<") [Expression
p1, Expression
p2])   = Comp -> E -> E -> F
FComp Comp
Lt (E -> E -> F) -> Maybe E -> Maybe (E -> F)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Expression -> Maybe E
termDRealToE Expression
p1 Maybe (E -> F) -> Maybe E -> Maybe F
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Expression -> Maybe E
termDRealToE Expression
p2
termDRealToF (LD.Application (LD.Variable [Char]
"not") [Expression
p])      = F -> F
FNot (F -> F) -> Maybe F -> Maybe F
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Expression -> Maybe F
termDRealToF Expression
p
-- Bools
termDRealToF (LD.Variable [Char]
"true")  = F -> Maybe F
forall a. a -> Maybe a
Just F
FTrue
termDRealToF (LD.Variable [Char]
"false") = F -> Maybe F
forall a. a -> Maybe a
Just F
FFalse
-- Unknown
termDRealToF Expression
_ = Maybe F
forall a. Maybe a
Nothing

termDRealToE :: LD.Expression -> Maybe E
-- Need to deal with Pi first
termDRealToE :: Expression -> Maybe E
termDRealToE (LD.Application (LD.Variable [Char]
"*") [LD.Number Rational
4, LD.Application (LD.Variable [Char]
"atan") [LD.Number Rational
1]]) = E -> Maybe E
forall a. a -> Maybe a
Just (E -> Maybe E) -> E -> Maybe E
forall a b. (a -> b) -> a -> b
$ E
Pi
-- EBinOp
termDRealToE (LD.Application (LD.Variable [Char]
"+") [Expression
p1, Expression
p2])   = BinOp -> E -> E -> E
EBinOp BinOp
Add (E -> E -> E) -> Maybe E -> Maybe (E -> E)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Expression -> Maybe E
termDRealToE Expression
p1 Maybe (E -> E) -> Maybe E -> Maybe E
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Expression -> Maybe E
termDRealToE Expression
p2
termDRealToE (LD.Application (LD.Variable [Char]
"-") [Expression
p1, Expression
p2])   = BinOp -> E -> E -> E
EBinOp BinOp
Sub (E -> E -> E) -> Maybe E -> Maybe (E -> E)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Expression -> Maybe E
termDRealToE Expression
p1 Maybe (E -> E) -> Maybe E -> Maybe E
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Expression -> Maybe E
termDRealToE Expression
p2
termDRealToE (LD.Application (LD.Variable [Char]
"*") [Expression
p1, Expression
p2])   = BinOp -> E -> E -> E
EBinOp BinOp
Mul (E -> E -> E) -> Maybe E -> Maybe (E -> E)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Expression -> Maybe E
termDRealToE Expression
p1 Maybe (E -> E) -> Maybe E -> Maybe E
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Expression -> Maybe E
termDRealToE Expression
p2
termDRealToE (LD.Application (LD.Variable [Char]
"/") [Expression
p1, Expression
p2])   = BinOp -> E -> E -> E
EBinOp BinOp
Div (E -> E -> E) -> Maybe E -> Maybe (E -> E)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Expression -> Maybe E
termDRealToE Expression
p1 Maybe (E -> E) -> Maybe E -> Maybe E
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Expression -> Maybe E
termDRealToE Expression
p2
termDRealToE (LD.Application (LD.Variable [Char]
"min") [Expression
p1, Expression
p2]) = BinOp -> E -> E -> E
EBinOp BinOp
Min (E -> E -> E) -> Maybe E -> Maybe (E -> E)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Expression -> Maybe E
termDRealToE Expression
p1 Maybe (E -> E) -> Maybe E -> Maybe E
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Expression -> Maybe E
termDRealToE Expression
p2
termDRealToE (LD.Application (LD.Variable [Char]
"max") [Expression
p1, Expression
p2]) = BinOp -> E -> E -> E
EBinOp BinOp
Max (E -> E -> E) -> Maybe E -> Maybe (E -> E)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Expression -> Maybe E
termDRealToE Expression
p1 Maybe (E -> E) -> Maybe E -> Maybe E
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Expression -> Maybe E
termDRealToE Expression
p2
termDRealToE (LD.Application (LD.Variable [Char]
"^") [Expression
p1, Expression
p2])   = BinOp -> E -> E -> E
EBinOp BinOp
Pow (E -> E -> E) -> Maybe E -> Maybe (E -> E)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Expression -> Maybe E
termDRealToE Expression
p1 Maybe (E -> E) -> Maybe E -> Maybe E
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Expression -> Maybe E
termDRealToE Expression
p2
termDRealToE (LD.Application (LD.Variable [Char]
"mod") [Expression
p1, Expression
p2]) = BinOp -> E -> E -> E
EBinOp BinOp
Mod (E -> E -> E) -> Maybe E -> Maybe (E -> E)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Expression -> Maybe E
termDRealToE Expression
p1 Maybe (E -> E) -> Maybe E -> Maybe E
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Expression -> Maybe E
termDRealToE Expression
p2
-- EUnOp
termDRealToE (LD.Application (LD.Variable [Char]
"sqrt") [Expression
p]) = UnOp -> E -> E
EUnOp UnOp
Sqrt (E -> E) -> Maybe E -> Maybe E
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Expression -> Maybe E
termDRealToE Expression
p
-- TODO: understand negate?
termDRealToE (LD.Application (LD.Variable [Char]
"abs") [Expression
p])  = UnOp -> E -> E
EUnOp UnOp
Abs (E -> E) -> Maybe E -> Maybe E
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Expression -> Maybe E
termDRealToE Expression
p
termDRealToE (LD.Application (LD.Variable [Char]
"sin") [Expression
p])  = UnOp -> E -> E
EUnOp UnOp
Sin (E -> E) -> Maybe E -> Maybe E
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Expression -> Maybe E
termDRealToE Expression
p
termDRealToE (LD.Application (LD.Variable [Char]
"cos") [Expression
p])  = UnOp -> E -> E
EUnOp UnOp
Cos (E -> E) -> Maybe E -> Maybe E
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Expression -> Maybe E
termDRealToE Expression
p
-- TODO: understand PowI? probably easier to add simplification rule
-- Variables
termDRealToE (LD.Variable [Char]
v) = E -> Maybe E
forall a. a -> Maybe a
Just (E -> Maybe E) -> E -> Maybe E
forall a b. (a -> b) -> a -> b
$ [Char] -> E
Var [Char]
v
-- Literals
termDRealToE (LD.Number Rational
n) = E -> Maybe E
forall a. a -> Maybe a
Just (E -> Maybe E) -> E -> Maybe E
forall a b. (a -> b) -> a -> b
$ Rational -> E
Lit Rational
n
-- RoundToInt
termDRealToE (LD.Application (LD.Variable [Char]
"to_int_rne") [Expression
p])  = RoundingMode -> E -> E
RoundToInteger RoundingMode
RNE (E -> E) -> Maybe E -> Maybe E
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Expression -> Maybe E
termDRealToE Expression
p
termDRealToE (LD.Application (LD.Variable [Char]
"to_int_rtp") [Expression
p])  = RoundingMode -> E -> E
RoundToInteger RoundingMode
RTP (E -> E) -> Maybe E -> Maybe E
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Expression -> Maybe E
termDRealToE Expression
p
termDRealToE (LD.Application (LD.Variable [Char]
"to_int_rtn") [Expression
p])  = RoundingMode -> E -> E
RoundToInteger RoundingMode
RTN (E -> E) -> Maybe E -> Maybe E
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Expression -> Maybe E
termDRealToE Expression
p
termDRealToE (LD.Application (LD.Variable [Char]
"to_int_rtz") [Expression
p])  = RoundingMode -> E -> E
RoundToInteger RoundingMode
RTZ (E -> E) -> Maybe E -> Maybe E
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Expression -> Maybe E
termDRealToE Expression
p
termDRealToE (LD.Application (LD.Variable [Char]
"to_int_rna") [Expression
p])  = RoundingMode -> E -> E
RoundToInteger RoundingMode
RNA (E -> E) -> Maybe E -> Maybe E
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Expression -> Maybe E
termDRealToE Expression
p
-- Float32
termDRealToE (LD.Application (LD.Variable [Char]
"float32_rne") [Expression
p])  = RoundingMode -> E -> E
Float32 RoundingMode
RNE (E -> E) -> Maybe E -> Maybe E
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Expression -> Maybe E
termDRealToE Expression
p
termDRealToE (LD.Application (LD.Variable [Char]
"float32_rtp") [Expression
p])  = RoundingMode -> E -> E
Float32 RoundingMode
RTP (E -> E) -> Maybe E -> Maybe E
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Expression -> Maybe E
termDRealToE Expression
p
termDRealToE (LD.Application (LD.Variable [Char]
"float32_rtn") [Expression
p])  = RoundingMode -> E -> E
Float32 RoundingMode
RTN (E -> E) -> Maybe E -> Maybe E
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Expression -> Maybe E
termDRealToE Expression
p
termDRealToE (LD.Application (LD.Variable [Char]
"float32_rtz") [Expression
p])  = RoundingMode -> E -> E
Float32 RoundingMode
RTZ (E -> E) -> Maybe E -> Maybe E
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Expression -> Maybe E
termDRealToE Expression
p
termDRealToE (LD.Application (LD.Variable [Char]
"float32_rna") [Expression
p])  = RoundingMode -> E -> E
Float32 RoundingMode
RNA (E -> E) -> Maybe E -> Maybe E
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Expression -> Maybe E
termDRealToE Expression
p
-- Float64
termDRealToE (LD.Application (LD.Variable [Char]
"float64_rne") [Expression
p])  = RoundingMode -> E -> E
Float64 RoundingMode
RNE (E -> E) -> Maybe E -> Maybe E
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Expression -> Maybe E
termDRealToE Expression
p
termDRealToE (LD.Application (LD.Variable [Char]
"float64_rtp") [Expression
p])  = RoundingMode -> E -> E
Float64 RoundingMode
RTP (E -> E) -> Maybe E -> Maybe E
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Expression -> Maybe E
termDRealToE Expression
p
termDRealToE (LD.Application (LD.Variable [Char]
"float64_rtn") [Expression
p])  = RoundingMode -> E -> E
Float64 RoundingMode
RTN (E -> E) -> Maybe E -> Maybe E
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Expression -> Maybe E
termDRealToE Expression
p
termDRealToE (LD.Application (LD.Variable [Char]
"float64_rtz") [Expression
p])  = RoundingMode -> E -> E
Float64 RoundingMode
RTZ (E -> E) -> Maybe E -> Maybe E
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Expression -> Maybe E
termDRealToE Expression
p
termDRealToE (LD.Application (LD.Variable [Char]
"float64_rna") [Expression
p])  = RoundingMode -> E -> E
Float64 RoundingMode
RNA (E -> E) -> Maybe E -> Maybe E
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Expression -> Maybe E
termDRealToE Expression
p
-- Unknown
termDRealToE Expression
_ = Maybe E
forall a. Maybe a
Nothing