{-# 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
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
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
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 [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
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
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
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
termDRealToF Expression
_ = Maybe F
forall a. Maybe a
Nothing
termDRealToE :: LD.Expression -> Maybe E
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
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
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
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
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
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
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
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
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
termDRealToE Expression
_ = Maybe E
forall a. Maybe a
Nothing