Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Enable choice of term ordering for REST #522

Merged
merged 9 commits into from
Feb 16, 2022
Merged
Changes from 1 commit
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
Prev Previous commit
Next Next commit
Fix arg parsing
  • Loading branch information
zgrannan committed Feb 11, 2022
commit da96d82b3d798912479e9dc937c64b7fb4b77d84
2 changes: 1 addition & 1 deletion src/Language/Fixpoint/Solver/PLE.hs
Original file line number Diff line number Diff line change
@@ -122,7 +122,7 @@ savePLEEqualities cfg fi res = when (save cfg) $ do
instEnv :: (Loc a) => Config -> SInfo a -> CMap (SimpC a) -> Maybe SolverHandle -> SMT.Context -> InstEnv a
instEnv cfg fi cs restSolver ctx = InstEnv cfg ctx bEnv aEnv cs γ s0
where
restOC = read (restOrdering cfg)
restOC = FC.restOC cfg
bEnv = bs fi
aEnv = ae fi
γ = knowledge cfg ctx fi
21 changes: 14 additions & 7 deletions src/Language/Fixpoint/Types/Config.hs
Original file line number Diff line number Diff line change
@@ -14,7 +14,9 @@ module Language.Fixpoint.Types.Config (
-- * SMT Solver options
, SMTSolver (..)

-- REST Options
, RESTOrdering (..)
, restOC

-- * Eliminate options
, Eliminate (..)
@@ -124,11 +126,13 @@ instance Show RESTOrdering where
show (RESTFuel n) = "fuel" ++ show n

instance Read RESTOrdering where
readsPrec _ "kbo" = [(RESTKBO, "")]
readsPrec _ "lpo" = [(RESTLPO, "")]
readsPrec _ "rpo" = [(RESTRPO, "")]
readsPrec _ xs | "fuel" `L.isPrefixOf` xs = [(RESTFuel (read (drop 4 xs)), "")]
readsPrec _ xs = error $ "Cannot parse " ++ xs ++ " as an ordering. Expected: kbo|lpo|rpo|fuelN"
readsPrec _ s | "kbo" `L.isPrefixOf` s = [(RESTKBO, drop 3 s)]
readsPrec _ s | "lbo" `L.isPrefixOf` s = [(RESTLPO, drop 3 s)]
readsPrec _ s | "rpo" `L.isPrefixOf` s = [(RESTRPO, drop 3 s)]
readsPrec n s | "fuel" `L.isPrefixOf` s = do
(fuel, rest) <- readsPrec n (drop 4 s)
return $ (RESTFuel fuel, rest)
readsPrec _ _ = []

---------------------------------------------------------------------------------------

@@ -226,12 +230,12 @@ defConfig = Config {
])
, checkCstr = [] &= help "Only check these specific constraint-ids"
, extensionality = False &= help "Allow extensional interpretation of extensionality"
, rwTerminationCheck = False &= help "Disable rewrite divergence checker"
, rwTerminationCheck = False &= help "Enable rewrite divergence checker"
, stdin = False &= help "Read input query from stdin"
, json = False &= help "Render result in JSON"
, noLazyPLE = False &= help "Don't use lazy PLE"
, fuel = Nothing &= help "Maximum fuel (per-function unfoldings) for PLE"
, restOrdering = def
, restOrdering = "rpo"
&= name "rest-ordering"
&= help "Ordering Constraint Algebra to use for REST"
}
@@ -258,6 +262,9 @@ banner :: String
banner = "\n\nLiquid-Fixpoint Copyright 2013-21 Regents of the University of California.\n"
++ "All Rights Reserved.\n"

restOC :: Config -> RESTOrdering
restOC cfg = read (restOrdering cfg)

multicore :: Config -> Bool
multicore cfg = cores cfg /= Just 1