| Safe Haskell | Safe-Inferred |
|---|---|
| Language | Haskell2010 |
PropaFP.Parsers.Smt
Synopsis
- data ParsingMode
- parser :: String -> [Expression]
- parseSMT2 :: FilePath -> IO [Expression]
- findAssertions :: [Expression] -> [Expression]
- findFunctionInputsAndOutputs :: [Expression] -> [(String, ([String], String))]
- findDeclarations :: [Expression] -> [Expression]
- findVariables :: [Expression] -> [(String, String)]
- findIntegerVariables :: [(String, String)] -> [(String, VarType)]
- findGoalsInAssertions :: [Expression] -> [Expression]
- takeGoalFromAssertions :: [Expression] -> (Expression, [Expression])
- 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
- eliminateKnownFunctionGuards :: [Expression] -> [Expression]
- eliminateKnownFunctionGuard :: Expression -> Expression
- termsToF :: [Expression] -> [(String, ([String], String))] -> [F]
- determineFloatTypeE :: E -> [(String, String)] -> Maybe E
- determineFloatTypeF :: F -> [(String, String)] -> Maybe F
- findVariableType :: [String] -> [(String, String)] -> [(String, Integer)] -> Maybe String -> Maybe String
- knownFloatVars :: E -> [(String, Integer)]
- findVariablesInFormula :: F -> [String]
- findVariablesInExpressions :: E -> [String]
- parseRoundingMode :: Expression -> Maybe RoundingMode
- processVC :: [Expression] -> Maybe (F, [(String, String)])
- symbolicallySubstitutePiVars :: F -> F
- deriveVCRanges :: F -> [(String, String)] -> Maybe (F, TypedVarMap)
- eContainsVars :: [String] -> E -> Bool
- fContainsVars :: [String] -> F -> Bool
- inequalityEpsilon :: Rational
- findVarEqualities :: F -> [(String, E)]
- filterOutCircularVarEqualities :: [(String, E)] -> [(String, E)]
- 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)
Documentation
data ParsingMode Source #
parser :: String -> [Expression] Source #
findAssertions :: [Expression] -> [Expression] Source #
Find assertions in a parsed expression Assertions are Application types with the operator being a Variable equal to "assert" Assertions only have one operands
findFunctionInputsAndOutputs :: [Expression] -> [(String, ([String], String))] Source #
findDeclarations :: [Expression] -> [Expression] Source #
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
findVariables :: [Expression] -> [(String, String)] Source #
findGoalsInAssertions :: [Expression] -> [Expression] Source #
Finds goals in assertion operands Goals are S-Expressions with a top level not
takeGoalFromAssertions :: [Expression] -> (Expression, [Expression]) Source #
Takes the last element from a list of assertions We assume that the last element is the goal
parseFCompOp :: String -> Maybe (E -> E -> F) Source #
Attempts to parse FComp Ops, i.e. parse bool_eq to Just (FComp Eq)
parseIte :: Expression -> Expression -> Expression -> [(String, ([String], String))] -> Maybe (E -> F) -> Maybe F Source #
collapseOrs :: [Expression] -> [Expression] Source #
collapseOr :: Expression -> Expression Source #
eliminateKnownFunctionGuards :: [Expression] -> [Expression] Source #
Replace function guards which are known to be always true with true.
eliminateKnownFunctionGuard :: Expression -> Expression Source #
Replace function guard which is known to be always true with true.
determineFloatTypeF :: F -> [(String, String)] -> Maybe F Source #
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.
findVariableType :: [String] -> [(String, String)] -> [(String, Integer)] -> Maybe String -> Maybe String Source #
Find the type for the given variables Type is looked for in the supplied map If all found types match, return this type
findVariablesInFormula :: F -> [String] Source #
findVariablesInExpressions :: E -> [String] Source #
processVC :: [Expression] -> Maybe (F, [(String, String)]) Source #
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.
symbolicallySubstitutePiVars :: F -> F Source #
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.
deriveVCRanges :: F -> [(String, String)] -> Maybe (F, TypedVarMap) Source #
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
filterOutCircularVarEqualities :: [(String, E)] -> [(String, E)] Source #
Filter out var equalities which rely on themselves
filterOutDuplicateVarEqualities :: [(String, E)] -> [(String, E)] Source #
Filter out var equalities which occur multiple times by choosing the var equality with the smallest length
substAllEqualities :: F -> F Source #
addVarMapBoundsToF :: F -> TypedVarMap -> F Source #
eliminateFloatsAndSimplifyVC :: F -> TypedVarMap -> Bool -> FilePath -> IO F Source #
parseVCToF :: FilePath -> FilePath -> IO (Maybe (F, TypedVarMap)) Source #