PropaFP.Parsers.Smt

Documentation

data ParsingMode

Constructors

Why3

CNF

parser :: String -> [Expression]

parseSMT2 :: FilePath -> IO [Expression]

findAssertions :: [Expression] -> [Expression]

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))]

findDeclarations :: [Expression] -> [Expression]

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)]

findIntegerVariables :: [(String, String)] -> [(String, VarType)]

findGoalsInAssertions :: [Expression] -> [Expression]

Finds goals in assertion operands Goals are S-Expressions with a top level not

takeGoalFromAssertions :: [Expression] -> (Expression, [Expression])

Takes the last element from a list of assertions We assume that the last element is the goal

parseFCompOp :: String -> Maybe (E -> E -> F)

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

termToF :: Expression -> [(String, ([String], String))] -> Maybe F

termToE :: Expression -> [(String, ([String], String))] -> Maybe E

collapseOrs :: [Expression] -> [Expression]

collapseOr :: Expression -> Expression

eliminateKnownFunctionGuards :: [Expression] -> [Expression]

Replace function guards which are known to be always true with true.

eliminateKnownFunctionGuard :: Expression -> Expression

Replace function guard which is known to be always true with true.

termsToF :: [Expression] -> [(String, ([String], String))] -> [F]

determineFloatTypeE :: E -> [(String, String)] -> Maybe E

determineFloatTypeF :: F -> [(String, String)] -> Maybe F

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

Find the type for the given variables Type is looked for in the supplied map If all found types match, return this type

knownFloatVars :: E -> [(String, Integer)]

findVariablesInFormula :: F -> [String]

findVariablesInExpressions :: E -> [String]

parseRoundingMode :: Expression -> Maybe RoundingMode

processVC :: [Expression] -> Maybe (F, [(String, String)])

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

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)

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

eContainsVars :: [String] -> E -> Bool

fContainsVars :: [String] -> F -> Bool

inequalityEpsilon :: Rational

findVarEqualities :: F -> [(String, E)]

filterOutCircularVarEqualities :: [(String, E)] -> [(String, E)]

Filter out var equalities which rely on themselves

filterOutDuplicateVarEqualities :: [(String, E)] -> [(String, E)]

Filter out var equalities which occur multiple times by choosing the var equality with the smallest length

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)