PropaFP.Parsers.DRealSmt

Documentation

parseDRealSmtToF :: [Expression] -> (Maybe F, TypedVarMap)

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

parseDRealVCs :: [Expression] -> Maybe F

parseDRealVC :: Expression -> Maybe F

parseDRealVariables :: [Expression] -> ([Expression], TypedVarMap)

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.

termDRealToF :: Expression -> Maybe F

termDRealToE :: Expression -> Maybe E