GaloisInc/cryptol
1
1
Fork 0
mirror of https://github.com/GaloisInc/cryptol.git synced 2024-12-17 04:44:39 +03:00
Code Issues Projects Releases Wiki Activity

:sat now can provide multiple solutions to equations given to it, the number shown can be set with :set satNum <integer value>, where <0 shows all solutions

Browse Source
This commit is contained in:
yuuko 2014-08-14 03:34:20 +01:00
parent bede37a436
commit 52e82226b5
3 changed files with 17 additions and 12 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

8
cryptol/REPL/Command.hs
View File

@ -337,14 +337,16 @@ satCmd str = do
EnvString proverName <- getUser "prover" EnvString proverName <- getUser "prover"
EnvBool iteSolver <- getUser "iteSolver" EnvBool iteSolver <- getUser "iteSolver"
EnvBool verbose <- getUser "debug" EnvBool verbose <- getUser "debug"
EnvNum n <- getUser "satNum"
result <- liftModuleCmd $ Cryptol.Symbolic.sat (proverName, iteSolver, verbose) (expr, schema) result <- liftModuleCmd $ Cryptol.Symbolic.sat (proverName, iteSolver, verbose) (expr, schema)
ppOpts <- getPPValOpts ppOpts <- getPPValOpts
case result of case result of
Left msg -> io $ putStrLn msg Left msg -> io $ putStrLn msg
Right Nothing -> io $ putStrLn "Unsatisfiable." Right Nothing -> io $ putStrLn "Unsatisfiable."
Right (Just vs) -> io $ print $ hsep (doc : docs) <+> text "= True" Right (Just vs) -> do
where doc = ppPrec 3 parseExpr -- function application has precedence 3 let solutions = map (map (pp . E.WithBase ppOpts)) vs
docs = map (pp . E.WithBase ppOpts) vs io $ print ((ppPrec 3 parseExpr) <+> text "is satisfied by:") -- function application has precedence 3
mapM_ (io . print) (if n < 0 then solutions else take n solutions)
specializeCmd :: String -> REPL () specializeCmd :: String -> REPL ()
specializeCmd str = do specializeCmd str = do

2
cryptol/REPL/Monad.hs
View File

@ -381,6 +381,8 @@ userOptions = mkOptionMap
"display 7- or 8-bit words using ASCII notation." "display 7- or 8-bit words using ASCII notation."
, OptionDescr "infLength" (EnvNum 5) checkInfLength , OptionDescr "infLength" (EnvNum 5) checkInfLength
"The number of elements to display for infinite sequences." "The number of elements to display for infinite sequences."
, OptionDescr "satNum" (EnvNum 1) (const Nothing)
"The number of solutions to display that satisfy an equation (-1 for infinity)."
, OptionDescr "tests" (EnvNum 100) (const Nothing) , OptionDescr "tests" (EnvNum 100) (const Nothing)
"The number of random tests to try." "The number of random tests to try."
, OptionDescr "prover" (EnvString "cvc4") checkProver $ , OptionDescr "prover" (EnvString "cvc4") checkProver $

19
src/Cryptol/Symbolic.hs
View File

@ -80,7 +80,7 @@ prove (proverName, useSolverIte, verbose) (expr, schema) = protectStack useSolve
SBV.ThmResult _ -> Left (show result) SBV.ThmResult _ -> Left (show result)
return (Right (solution, modEnv), []) return (Right (solution, modEnv), [])
sat :: (String, Bool, Bool) -> (Expr, Schema) -> M.ModuleCmd (Either String (Maybe [Eval.Value])) sat :: (String, Bool, Bool) -> (Expr, Schema) -> M.ModuleCmd (Either String (Maybe [[Eval.Value]]))
sat (proverName, useSolverIte, verbose) (expr, schema) = protectStack useSolverIte $ \modEnv -> do sat (proverName, useSolverIte, verbose) (expr, schema) = protectStack useSolverIte $ \modEnv -> do
let extDgs = allDeclGroups modEnv let extDgs = allDeclGroups modEnv
let prover = lookupProver proverName let prover = lookupProver proverName
@ -89,18 +89,19 @@ sat (proverName, useSolverIte, verbose) (expr, schema) = protectStack useSolverI
Right ts -> do when verbose $ putStrLn "Simulating..." Right ts -> do when verbose $ putStrLn "Simulating..."
let env = evalDecls (emptyEnv useSolverIte) extDgs let env = evalDecls (emptyEnv useSolverIte) extDgs
let v = evalExpr env expr let v = evalExpr env expr
result <- SBV.satWith prover $ do SBV.AllSatResult (_, results) <- SBV.allSatWith prover $ do
args <- mapM existsFinType ts args <- mapM existsFinType ts
b <- return $! fromVBit (foldl fromVFun v args) b <- return $! fromVBit (foldl fromVFun v args)
when verbose $ liftIO $ putStrLn $ "Calling " ++ proverName ++ "..." when verbose $ liftIO $ putStrLn $ "Calling " ++ proverName ++ "..."
return b return b
let solution = case result of let solutions = case results of
SBV.SatResult (SBV.Satisfiable {}) -> Right (Just vs) (SBV.Satisfiable {} : _) -> Right (Just vs) where
where Right (_, cws) = SBV.getModel result vs = map (\r -> let
(vs, _) = parseValues ts cws Right (_, cws) = SBV.getModel r
SBV.SatResult (SBV.Unsatisfiable {}) -> Right Nothing (vs, _) = parseValues ts cws
SBV.SatResult _ -> Left (show result) in vs) results
return (Right (solution, modEnv), []) _ -> Right Nothing
return (Right (solutions, modEnv), [])
protectStack :: Bool -> M.ModuleCmd (Either String a) -> M.ModuleCmd (Either String a) protectStack :: Bool -> M.ModuleCmd (Either String a) -> M.ModuleCmd (Either String a)
protectStack usingITE cmd modEnv = X.catchJust isOverflow (cmd modEnv) handler protectStack usingITE cmd modEnv = X.catchJust isOverflow (cmd modEnv) handler