-- Hoogle documentation, generated by Haddock
-- See Hoogle, http://www.haskell.org/hoogle/


-- | Auto-active verification of floating-point programs
--   
--   Please see the README on GitHub at
--   <a>https://github.com/rasheedja/PropaFP#readme</a>
@package PropaFP
@version 0.1.2.0

module PropaFP.Parsers.Lisp.DataTypes
type Frame = Map String Expression
data Environment
EmptyEnvironment :: Environment
Environment :: Frame -> Environment -> Environment
data Expression
Null :: Expression
Number :: Rational -> Expression
Boolean :: Bool -> Expression
Variable :: String -> Expression
Pair :: Expression -> Expression -> Expression
Exception :: String -> Expression
Lambda :: [Expression] -> Expression -> Expression
PrimitiveProcedure :: ([Expression] -> Expression) -> Expression
Application :: Expression -> [Expression] -> Expression
Definition :: Expression -> Expression -> Expression
If :: Expression -> Expression -> Expression -> Expression
Cond :: [(Expression, Expression)] -> Expression
addBinding :: Environment -> String -> Expression -> Environment
lookupValue :: Environment -> String -> Expression
extendEnvironment :: Environment -> [Expression] -> [Expression] -> Environment
pairToList :: Expression -> [Expression]
instance GHC.Show.Show PropaFP.Parsers.Lisp.DataTypes.Expression
instance GHC.Classes.Eq PropaFP.Parsers.Lisp.DataTypes.Expression

module PropaFP.Parsers.Lisp.Parser
tokenize :: String -> [String]
parse :: [String] -> (Expression, [String])
parseSequence :: [String] -> [Expression]
analyzeExpression :: Expression -> Expression
analyzeExpressionSequence :: [Expression] -> [Expression]
isScientificNumber :: String -> Bool

module PropaFP.VarMap

-- | An assosciation list mapping variable names to rational interval
--   domains
data VarType
Real :: VarType
Integer :: VarType
type VarInterval = (String, (Rational, Rational))
data TypedVarInterval
TypedVar :: VarInterval -> VarType -> TypedVarInterval
type VarMap = [VarInterval]
type TypedVarMap = [TypedVarInterval]

-- | Get the width of the widest interval Fixme: maxWidth
maxWidth :: VarMap -> Rational
typedMaxWidth :: TypedVarMap -> Rational

-- | Get the sum of the width of each interval
taxicabWidth :: VarMap -> Rational

-- | Increase the diameter of all variables in a varMap by the given
--   rational
increaseDiameter :: VarMap -> Rational -> VarMap

-- | Increase the radius of all variables in a varMap by the given rational
increaseRadius :: VarMap -> Rational -> VarMap

-- | Bisect all elements in a given VarMap
fullBisect :: VarMap -> [VarMap]

-- | Bisect the domain of the given interval, resulting in a pair Vars
bisectInterval :: (String, (Rational, Rational)) -> ((String, (Rational, Rational)), (String, (Rational, Rational)))
bisectTypedInterval :: (String, (Rational, Rational)) -> VarType -> ((String, (Rational, Rational)), (String, (Rational, Rational)))

-- | Bisect the given dimension of the given VarMap, resulting in a pair of
--   VarMaps
bisectN :: Integer -> VarMap -> (VarMap, VarMap)
bisectVar :: VarMap -> String -> (VarMap, VarMap)
bisectTypedVar :: TypedVarMap -> String -> (TypedVarMap, TypedVarMap)

-- | Check whether or not v1 contain v2.
contains :: VarMap -> VarMap -> Bool

-- | Convert VarMap to SearchBox with the provided minimum
toSearchBox :: VarMap -> CN MPBall -> SearchBox
centre :: VarMap -> VarMap
varMapToBox :: VarMap -> Precision -> Box
typedVarMapToBox :: TypedVarMap -> Precision -> Box
boxToVarMap :: Box -> [String] -> VarMap
unsafeBoxToTypedVarMap :: Box -> [(String, VarType)] -> TypedVarMap
safeBoxToTypedVarMap :: Box -> [(String, VarType)] -> Maybe TypedVarMap
typedVarMapToVarMap :: TypedVarMap -> VarMap
unsafeVarMapToTypedVarMap :: VarMap -> [(String, VarType)] -> TypedVarMap
safeVarMapToTypedVarMap :: VarMap -> [(String, VarType)] -> Maybe TypedVarMap
safeIntersectVarMap :: TypedVarMap -> TypedVarMap -> Maybe TypedVarMap

-- | Assumes varMaps have vars appearing in the same order
unsafeIntersectVarMap :: TypedVarMap -> TypedVarMap -> TypedVarMap
isVarMapInverted :: VarMap -> Bool
isTypedVarMapInverted :: TypedVarMap -> Bool
getVarNamesWithTypes :: TypedVarMap -> [(String, VarType)]
getCorners :: VarMap -> [VarMap]
getEdges :: VarMap -> [VarMap]
upperbound :: VarMap -> VarMap
lowerbound :: VarMap -> VarMap

-- | Intersect two varMaps This assumes that both VarMaps have the same
--   variables in the same order
intersectVarMap :: VarMap -> VarMap -> VarMap

-- | Returns the widest interval in the given VarMap
widestInterval :: VarMap -> (String, (Rational, Rational)) -> (String, (Rational, Rational))
widestTypedInterval :: TypedVarMap -> (String, (Rational, Rational)) -> (String, (Rational, Rational))
typedVarIntervalToVarInterval :: TypedVarInterval -> VarInterval
prettyShowVarMap :: VarMap -> String
prettyShowTypedVarMap :: TypedVarMap -> String
instance GHC.Classes.Ord PropaFP.VarMap.VarType
instance GHC.Classes.Eq PropaFP.VarMap.VarType
instance GHC.Show.Show PropaFP.VarMap.VarType
instance GHC.Classes.Ord PropaFP.VarMap.TypedVarInterval
instance GHC.Classes.Eq PropaFP.VarMap.TypedVarInterval
instance GHC.Show.Show PropaFP.VarMap.TypedVarInterval

module PropaFP.Expression
data BinOp
Add :: BinOp
Sub :: BinOp
Mul :: BinOp
Div :: BinOp
Min :: BinOp
Max :: BinOp
Pow :: BinOp
Mod :: BinOp
data UnOp
Sqrt :: UnOp
Negate :: UnOp
Abs :: UnOp
Sin :: UnOp
Cos :: UnOp
data RoundingMode
RNE :: RoundingMode
RTP :: RoundingMode
RTN :: RoundingMode
RTZ :: RoundingMode
RNA :: RoundingMode

-- | The E type represents the inequality: expression :: E &gt;= 0 TODO:
--   Add rounding operator with certain epsilon/floating-point type
data E
EBinOp :: BinOp -> E -> E -> E
EUnOp :: UnOp -> E -> E
Lit :: Rational -> E
Var :: String -> E
PowI :: E -> Integer -> E
Float32 :: RoundingMode -> E -> E
Float64 :: RoundingMode -> E -> E
Float :: RoundingMode -> E -> E
Pi :: E
RoundToInteger :: RoundingMode -> E -> E
data ESafe
EStrict :: E -> ESafe
ENonStrict :: E -> ESafe
data Comp
Gt :: Comp
Ge :: Comp
Lt :: Comp
Le :: Comp
Eq :: Comp
data Conn
And :: Conn
Or :: Conn
Impl :: Conn

-- | The F type is used to specify comparisons between E types and logical
--   connectives between F types
data F
FComp :: Comp -> E -> E -> F
FConn :: Conn -> F -> F -> F
FNot :: F -> F
FTrue :: F
FFalse :: F
lengthF :: F -> Integer
lengthE :: E -> Integer
newtype Name
Name :: String -> Name
flipStrictness :: ESafe -> ESafe

-- | Equivalent to E * -1 Example: ENonStrict e == e &gt;= 0. negateSafeE
--   (ENonStrict e) == e <a>== -e</a> 0 == (EStrict (EUnOp Negate e))
negateSafeE :: ESafe -> ESafe
extractSafeE :: ESafe -> E
fmapESafe :: (E -> E) -> ESafe -> ESafe
fToECNF :: F -> [[ESafe]]
fToEDNF :: F -> [[ESafe]]
fToFDNF :: F -> [[F]]
eSafeToF :: ESafe -> F
eSafeDisjToF :: [ESafe] -> F
eSafeCNFToF :: [[ESafe]] -> F
eSafeCNFToDNF :: [[ESafe]] -> [[ESafe]]

-- | Add bounds for any Float expressions addRoundingBounds :: E -&gt;
--   [[E]] addRoundingBounds (Float e significand) = [[exactExpression -
--   machineEpsilon], [exactExpression + machineEpsilon]] where
--   exactExpression = addRoundingBounds e machineEpsilon = 2^(-23)
--   addRoundingBounds e = e
--   
--   Various rules to simplify expressions
simplifyE :: E -> E
simplifyF :: F -> F
simplifyEDoubleList :: [[E]] -> [[E]]
simplifyFDNF :: [[F]] -> [[F]]
fDNFToFDNFWithoutEq :: [[F]] -> [[F]] -> [[F]]
fDNFToEDNF :: [[F]] -> [[ESafe]]
simplifyFDoubleList :: [[F]] -> [[F]]
simplifyESafeDoubleList :: [[ESafe]] -> [[ESafe]]

-- | compute the value of E with Vars at specified points
computeE :: E -> [(String, Rational)] -> CN Double

-- | Given a list of qualified Es and points for all Vars, compute a list
--   of valid values.
--   
--   A value is the computed result of the second element of the tuple and
--   is valid if all the expressions in the list at the first element of
--   the tuple compute to be above 0.
computeQualifiedEs :: [([E], E)] -> [(String, Rational)] -> [CN Double]
computeEDisjunction :: [E] -> [(String, Rational)] -> [CN Double]
computeECNF :: [[E]] -> [(String, Rational)] -> [[CN Double]]
prettyShowESafeCNF :: [[ESafe]] -> String
prettyShowESafeDNF :: [[ESafe]] -> String
prettyShowFSafeDNF :: [[F]] -> String
prettyShowVC :: F -> TypedVarMap -> String
latexShowE :: E -> String
latexShowF :: F -> Integer -> String
latexShowComp :: Comp -> String
latexShowConn :: Conn -> String

-- | Show an expression in a human-readable format Rationals are converted
--   into doubles
prettyShowE :: E -> String

-- | Show a conjunction of expressions in a human-readable format This is
--   shown as an AND with each disjunction tabbed in with an OR If there is
--   only one term in a disjunction, the expression is shown without an OR
prettyShowECNF :: [[E]] -> String
prettyShowF :: F -> Integer -> String
prettyShowComp :: Comp -> String
prettyShowConn :: Conn -> String

-- | Extract all variables in an expression Will not return duplicationes
extractVariablesE :: E -> [String]

-- | Extract all variables in an expression Will not return duplicationes
extractVariablesF :: F -> [String]
extractVariablesECNF :: [[E]] -> [String]
hasVarsE :: E -> Bool
hasVarsF :: F -> Bool
hasFloatE :: E -> Bool
hasFloatF :: F -> Bool
substVarEWithLit :: E -> String -> Rational -> E
substVarFWithLit :: F -> String -> Rational -> F
substVarEWithE :: String -> E -> E -> E
substVarFWithE :: String -> F -> E -> F
transformImplications :: F -> F
removeVariableFreeComparisons :: F -> F
hasMinMaxAbsE :: E -> Bool
hasMinMaxAbsF :: F -> Bool
replaceEInE :: E -> E -> E -> E
replaceEInF :: F -> E -> E -> F

-- | Normalize to and/or aggressively apply elimination rules
normalizeBoolean :: F -> F
instance GHC.Classes.Ord PropaFP.Expression.BinOp
instance GHC.Classes.Eq PropaFP.Expression.BinOp
instance GHC.Show.Show PropaFP.Expression.BinOp
instance GHC.Classes.Ord PropaFP.Expression.UnOp
instance GHC.Classes.Eq PropaFP.Expression.UnOp
instance GHC.Show.Show PropaFP.Expression.UnOp
instance GHC.Classes.Ord PropaFP.Expression.RoundingMode
instance GHC.Classes.Eq PropaFP.Expression.RoundingMode
instance GHC.Show.Show PropaFP.Expression.RoundingMode
instance GHC.Classes.Ord PropaFP.Expression.E
instance GHC.Classes.Eq PropaFP.Expression.E
instance GHC.Show.Show PropaFP.Expression.E
instance GHC.Classes.Ord PropaFP.Expression.ESafe
instance GHC.Classes.Eq PropaFP.Expression.ESafe
instance GHC.Show.Show PropaFP.Expression.ESafe
instance GHC.Classes.Ord PropaFP.Expression.Comp
instance GHC.Classes.Eq PropaFP.Expression.Comp
instance GHC.Show.Show PropaFP.Expression.Comp
instance GHC.Classes.Ord PropaFP.Expression.Conn
instance GHC.Classes.Eq PropaFP.Expression.Conn
instance GHC.Show.Show PropaFP.Expression.Conn
instance GHC.Classes.Ord PropaFP.Expression.F
instance GHC.Classes.Eq PropaFP.Expression.F
instance GHC.Show.Show PropaFP.Expression.F
instance GHC.Show.Show PropaFP.Expression.Name
instance Test.QuickCheck.Arbitrary.Arbitrary PropaFP.Expression.Name
instance Test.QuickCheck.Arbitrary.Arbitrary PropaFP.Expression.E
instance Test.QuickCheck.Arbitrary.Arbitrary PropaFP.Expression.F
instance Test.QuickCheck.Arbitrary.Arbitrary PropaFP.Expression.Conn
instance Test.QuickCheck.Arbitrary.Arbitrary PropaFP.Expression.Comp
instance Test.QuickCheck.Arbitrary.Arbitrary PropaFP.Expression.ESafe
instance Test.QuickCheck.Arbitrary.Arbitrary PropaFP.Expression.RoundingMode
instance Test.QuickCheck.Arbitrary.Arbitrary PropaFP.Expression.UnOp
instance Test.QuickCheck.Arbitrary.Arbitrary PropaFP.Expression.BinOp

module PropaFP.Translators.MetiTarski
formulaToTPTP :: F -> Integer -> String
expressionToTPTP :: E -> String
formulaAndVarMapToMetiTarski :: F -> TypedVarMap -> String
disjunctionExpressionsToSMT :: [E] -> String
cnfExpressionsToSMT :: [[E]] -> String
disjunctionExpressionsToTptp :: [ESafe] -> String
cnfExpressionsToTptp :: [[ESafe]] -> String
cnfExpressionAndDomainsToMetiTarski :: [[ESafe]] -> [(String, (Rational, Rational))] -> String
runMetiTarskiTranslatorCNFWithVarMap :: [[ESafe]] -> [(String, (Rational, Rational))] -> IO ()

module PropaFP.Translators.FPTaylor

-- | All variables must appear in the VarMap
expressionToFPTaylor :: E -> String
variableBoundsToFPTaylor :: VarMap -> String
showFrac :: Rational -> [Char]
expressionWithVarMapToFPTaylor :: E -> VarMap -> String
parseFPTaylorRational :: String -> Maybe Rational
testOutput :: String

module PropaFP.Translators.DReal
fToConjunction :: F -> [F]
conjunctionToSMT :: [F] -> String
formulaToSMT :: F -> Integer -> String
expressionToSMT :: E -> String
formulaAndVarMapToDReal :: F -> TypedVarMap -> String
disjunctionExpressionsToSMT :: [ESafe] -> String
cnfExpressionsToSMT :: [[ESafe]] -> String
cnfExpressionAndDomainsToDreal :: [[ESafe]] -> [(String, (Rational, Rational))] -> [(String, (Rational, Rational))] -> String
runDRealTranslatorCNFWithVarMap :: [[ESafe]] -> [(String, (Rational, Rational))] -> [(String, (Rational, Rational))] -> IO ()
runDRealTranslatorCNF :: [[ESafe]] -> IO ()

module PropaFP.Eliminator
minMaxAbsEliminatorF :: F -> F

-- | Given an expression, eliminate all Min, Max, and Abs occurences. This
--   is done by:
--   
--   When we come across a Min e1 e2: 1) We have two cases 1a) if e2 &gt;=
--   e1, then choose e1 1b) if e1 &gt;= e2, then choose e2 2) So, we
--   eliminate min and add two elements to the qualified list 2a) Add e2 -
--   e1 to the list of premises, call the eliminiator on e1 and e2
--   recursively, add any new premises from the recursive call to the list
--   of premises, set the qualified value of e1 from the recursive call to
--   be the qualified value in this case 2b) similar to 2a
--   
--   Max e1 e2 is similar to Min e1 e2 Abs is treated as Max e (-e)
--   
--   If we come across any other operator, recursively call the eliminator
--   on any expressions, add any resulting premises, and set the qualified
--   value to be the operator called on the resulting Es
minMaxAbsEliminator :: ESafe -> [([ESafe], ESafe)]
minMaxAbsEliminatorECNF :: [[ESafe]] -> [[ESafe]]

-- | Translate the qualified Es list to a single expression The qualified
--   Es list is basically the following formula: e &gt;= 0 == (p1 &gt;= 0
--   <i> p2 &gt;= 0 </i> p3 &gt;=0 -&gt; q1 &gt;= 0) / repeat... where e is
--   the expression passed to minMaxAbsEliminator
--   
--   This can be rewritten to (-p1 &gt;= 0 / - p2 &gt;= 0 / -p3 &gt;= 0 /
--   q1 &gt;= 0) This is incorrect, strictness is not dealt with correctly
--   qualifiedEsToCNF :: [([E],E)] -&gt; E qualifiedEsToCNF [] = undefined
--   qualifiedEsToCNF [([], q)] = q qualifiedEsToCNF [(ps, q)] = EBinOp Max
--   (buildPs ps) q where buildPs :: [E] -&gt; E buildPs [] = undefined
--   buildPs [p] = (EUnOp Negate p) buildPs (p : ps) = EBinOp Max (EUnOp
--   Negate p) (buildPs ps) qualifiedEsToCNF ((ps, q) : es) = EBinOp Min
--   (qualifiedEsToCNF [(ps, q)]) (qualifiedEsToCNF es)
--   
--   Convert a list of qualified Es to a CNF represented as a list of lists
qualifiedEsToCNF2 :: [([ESafe], ESafe)] -> [[ESafe]]
qualifiedEsToDisjunction :: ([ESafe], ESafe) -> [ESafe]
qualifiedEsToF :: [([ESafe], ESafe)] -> F
qualifiedEToF :: ([ESafe], ESafe) -> F

module PropaFP.EliminateFloats
removeFloats :: E -> E
eliminateFloatsF :: F -> VarMap -> Bool -> FilePath -> IO F

-- | Made for Float32/64 expressions
findAbsoluteErrorUsingFPTaylor :: E -> VarMap -> FilePath -> IO Rational


-- | Deriving ranges for variables from hypotheses inside a formula
module PropaFP.DeriveBounds
_f1 :: F
_f2 :: F
_f3 :: F
_f4 :: F
_f5 :: F
type VarName = String
deriveBoundsAndSimplify :: F -> (F, VarMap, [VarName])
type VarBoundMap = Map VarName (Maybe Rational, Maybe Rational)
scanHypotheses :: F -> VarBoundMap -> VarBoundMap
scanHypothesis :: F -> Bool -> VarBoundMap -> VarBoundMap

-- | Replace within a formula some comparisons with FTrue/FFalse, namely
--   those comparisons that on the given box can be easily seen to be
--   true/false.
evalF_comparisons :: VarBoundMap -> F -> F
evalE_Rational :: VarBoundMap -> E -> (Maybe Rational, Maybe Rational)
updateUpper :: CanMinMaxSameType a => (t, Maybe a) -> (t1, Maybe a) -> (t1, Maybe a)
updateLower :: CanMinMaxSameType a => (Maybe a, t) -> (Maybe a, t1) -> (Maybe a, t1)

-- | compute the value of E with Vars at specified points | (a generalised
--   version of computeE)
evalE :: (Ring v, CanDivSameType v, CanPowBy v Integer, CanMinMaxSameType v, CanAbsSameType v, CanPowBy v v, CanSqrtSameType v, CanSinCosSameType v, IsInterval v, CanAddThis v Integer, HasDyadics v, CanMinMaxSameType (IntervalEndpoint v), _) => (Rational -> v) -> Map VarName v -> Precision -> E -> v
roundMPBall :: (Real (IntervalEndpoint i), IsInterval i, IsInterval p, ConvertibleExactly Integer (IntervalEndpoint p)) => RoundingMode -> i -> p
checkFWithEval :: F -> VarBoundMap -> Maybe Bool

module PropaFP.Translators.BoxFun
expressionToBoxFun :: E -> VarMap -> Precision -> BoxFun

module PropaFP.Parsers.Smt
data ParsingMode
Why3 :: ParsingMode
CNF :: ParsingMode
parser :: String -> [Expression]
parseSMT2 :: FilePath -> IO [Expression]

-- | Find assertions in a parsed expression Assertions are Application
--   types with the operator being a Variable equal to "assert" Assertions
--   only have one <tt>operands</tt>
findAssertions :: [Expression] -> [Expression]
findFunctionInputsAndOutputs :: [Expression] -> [(String, ([String], String))]

-- | Find function declarations in a parsed expression Function
--   declarations are Application types with the operator being a Variable
--   equal to "declare-fun" Function declarations contain 3 operands -
--   Operand 1 is the name of the function - Operand 2 is an Application
--   type which can be thought of as the parameters of the functions If the
--   function has no paramters, this operand is LD.Null - Operand 3 is the
--   type of the function
findDeclarations :: [Expression] -> [Expression]
findVariables :: [Expression] -> [(String, String)]
findIntegerVariables :: [(String, String)] -> [(String, VarType)]

-- | Finds goals in assertion operands Goals are S-Expressions with a top
--   level <a>not</a>
findGoalsInAssertions :: [Expression] -> [Expression]

-- | Takes the last element from a list of assertions We assume that the
--   last element is the goal
takeGoalFromAssertions :: [Expression] -> (Expression, [Expression])

-- | Attempts to parse FComp Ops, i.e. parse bool_eq to Just (FComp Eq)
parseFCompOp :: String -> Maybe (E -> E -> F)
parseIte :: Expression -> Expression -> Expression -> [(String, ([String], String))] -> Maybe (E -> F) -> Maybe F
termToF :: Expression -> [(String, ([String], String))] -> Maybe F
termToE :: Expression -> [(String, ([String], String))] -> Maybe E
collapseOrs :: [Expression] -> [Expression]
collapseOr :: Expression -> Expression

-- | Replace function guards which are known to be always true with true.
eliminateKnownFunctionGuards :: [Expression] -> [Expression]

-- | Replace function guard which is known to be always true with true.
eliminateKnownFunctionGuard :: Expression -> Expression
termsToF :: [Expression] -> [(String, ([String], String))] -> [F]
determineFloatTypeE :: E -> [(String, String)] -> Maybe E

-- | Tries to determine whether a Float operation is single or double
--   precision by searching for the type of all variables appearing in the
--   function. If the types match and are all either Float32/Float64, we
--   can determine the type.
determineFloatTypeF :: F -> [(String, String)] -> Maybe F

-- | Find the type for the given variables Type is looked for in the
--   supplied map If all found types match, return this type
findVariableType :: [String] -> [(String, String)] -> [(String, Integer)] -> Maybe String -> Maybe String
knownFloatVars :: E -> [(String, Integer)]
findVariablesInFormula :: F -> [String]
findVariablesInExpressions :: E -> [String]
parseRoundingMode :: Expression -> Maybe RoundingMode

-- | Process a parsed list of expressions to a VC.
--   
--   If the parsing mode is Why3, everything in the context implies the
--   goal (empty context means we only have a goal). If the goal cannot be
--   parsed, we return Nothing.
--   
--   If the parsing mode is CNF, parse all assertions into a CNF. If any
--   assertion cannot be parsed, return Nothing. If any assertion contains
--   Floats, return Nothing.
processVC :: [Expression] -> Maybe (F, [(String, String)])

-- | Looks for pi vars (vars named pi/pi{i} where {i} is some integer) and
--   symbolic bounds. If the bounds are better than those given to the real
--   pi in Why3, replace the variable with exact pi.
symbolicallySubstitutePiVars :: F -> F

-- | Derive ranges for a VC (Implication where a CNF implies a goal) Remove
--   anything which refers to a variable for which we cannot derive ranges
--   If the goal contains underivable variables, return Nothing
deriveVCRanges :: F -> [(String, String)] -> Maybe (F, TypedVarMap)
eContainsVars :: [String] -> E -> Bool
fContainsVars :: [String] -> F -> Bool
inequalityEpsilon :: Rational
findVarEqualities :: F -> [(String, E)]

-- | Filter out var equalities which rely on themselves
filterOutCircularVarEqualities :: [(String, E)] -> [(String, E)]

-- | Filter out var equalities which occur multiple times by choosing the
--   var equality with the smallest length
filterOutDuplicateVarEqualities :: [(String, E)] -> [(String, E)]
substAllEqualities :: F -> F
addVarMapBoundsToF :: F -> TypedVarMap -> F
eliminateFloatsAndSimplifyVC :: F -> TypedVarMap -> Bool -> FilePath -> IO F
parseVCToF :: FilePath -> FilePath -> IO (Maybe (F, TypedVarMap))
parseVCToSolver :: FilePath -> FilePath -> (F -> TypedVarMap -> String) -> Bool -> IO (Maybe String)

module PropaFP.Parsers.DRealSmt

-- | 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 (&lt;= lowerBound
--   varName)) (assert (&lt;= 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 :: [Expression] -> (Maybe F, TypedVarMap)
parseDRealVCs :: [Expression] -> Maybe F
parseDRealVC :: Expression -> Maybe F

-- | 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 :: [Expression] -> ([Expression], TypedVarMap)
termDRealToF :: Expression -> Maybe F
termDRealToE :: Expression -> Maybe E