Skip to content

Commit 71f6302

Browse files
goodlyrottenapplegoodlyrottenapple
authored
Remove simplifierX switch (#3179)
Fixes #3172
1 parent 9936253 commit 71f6302

File tree

16 files changed

+74
-189
lines changed

16 files changed

+74
-189
lines changed

‎kore/app/check-functions/Main.hs‎

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -136,11 +136,11 @@ mainWithOptions localOptions@LocalOptions{execOptions} =
136136
>>= exitWith
137137

138138
koreCheckFunctions :: LocalOptions KoreCheckerOptions -> FilePath -> IO ExitCode
139-
koreCheckFunctions LocalOptions{execOptions, simplifierx} tmpDir =
139+
koreCheckFunctions LocalOptions{execOptions} tmpDir =
140140
do
141141
definitions <- loadDefinitions [fileName]
142142
loadedModule <- loadModule mainModuleName definitions
143-
checkFunctions simplifierx loadedModule
143+
checkFunctions loadedModule
144144
& SMT.runSMT defaultConfig (pure ())
145145
return ExitSuccess
146146
& handle handleSomeException

‎kore/app/exec/Main.hs‎

Lines changed: 8 additions & 14 deletions
Original file line numberDiff line numberDiff line change
@@ -584,7 +584,7 @@ main = do
584584
dispatch the requested command.
585585
-}
586586
mainWithOptions :: LocalOptions KoreExecOptions -> IO ()
587-
mainWithOptions LocalOptions{execOptions, simplifierx} = do
587+
mainWithOptions LocalOptions{execOptions} = do
588588
let KoreExecOptions{koreSolverOptions, bugReportOption, outputFileName} =
589589
execOptions
590590
ensureSmtPreludeExists koreSolverOptions
@@ -596,7 +596,7 @@ mainWithOptions LocalOptions{execOptions, simplifierx} = do
596596
}
597597
writeOptionsAndKoreFiles tmpDir execOptions'
598598
e <-
599-
mainDispatch LocalOptions{execOptions = execOptions', simplifierx}
599+
mainDispatch LocalOptions{execOptions = execOptions'}
600600
& handle handleWithConfiguration
601601
& handle handleSomeException
602602
& runKoreLog
@@ -666,12 +666,12 @@ koreSearch ::
666666
LocalOptions KoreExecOptions ->
667667
KoreSearchOptions ->
668668
Main (KFileLocations, ExitCode)
669-
koreSearch LocalOptions{execOptions, simplifierx} searchOptions = do
669+
koreSearch LocalOptions{execOptions} searchOptions = do
670670
let KoreExecOptions{definitionFileName} = execOptions
671671
let KoreExecOptions{mainModuleName} = execOptions
672672
let KoreExecOptions{koreSolverOptions} = execOptions
673673
SerializedDefinition{serializedModule, lemmas, locations} <-
674-
deserializeDefinition simplifierx koreSolverOptions definitionFileName mainModuleName
674+
deserializeDefinition koreSolverOptions definitionFileName mainModuleName
675675
let SerializedModule{verifiedModule, metadataTools} = serializedModule
676676
let KoreSearchOptions{searchFileName} = searchOptions
677677
target <- mainParseSearchPattern verifiedModule searchFileName
@@ -680,7 +680,6 @@ koreSearch LocalOptions{execOptions, simplifierx} searchOptions = do
680680
final <-
681681
execute koreSolverOptions metadataTools lemmas $
682682
search
683-
simplifierx
684683
depthLimit
685684
breadthLimit
686685
serializedModule
@@ -695,13 +694,12 @@ koreSearch LocalOptions{execOptions, simplifierx} searchOptions = do
695694
KoreExecOptions{breadthLimit, depthLimit} = execOptions
696695

697696
koreRun :: LocalOptions KoreExecOptions -> Main (KFileLocations, ExitCode)
698-
koreRun LocalOptions{execOptions, simplifierx} = do
697+
koreRun LocalOptions{execOptions} = do
699698
let KoreExecOptions{definitionFileName} = execOptions
700699
let KoreExecOptions{mainModuleName} = execOptions
701700
let KoreExecOptions{koreSolverOptions} = execOptions
702701
SerializedDefinition{serializedModule, lemmas, locations} <-
703702
deserializeDefinition
704-
simplifierx
705703
koreSolverOptions
706704
definitionFileName
707705
mainModuleName
@@ -711,7 +709,6 @@ koreRun LocalOptions{execOptions, simplifierx} = do
711709
(exitCode, final) <-
712710
execute koreSolverOptions metadataTools lemmas $
713711
exec
714-
simplifierx
715712
depthLimit
716713
breadthLimit
717714
serializedModule
@@ -730,10 +727,9 @@ koreRun LocalOptions{execOptions, simplifierx} = do
730727
koreSerialize ::
731728
LocalOptions KoreExecOptions ->
732729
Main (KFileLocations, ExitCode)
733-
koreSerialize LocalOptions{execOptions, simplifierx} = do
730+
koreSerialize LocalOptions{execOptions} = do
734731
serializedDefinition@SerializedDefinition{locations} <-
735732
makeSerializedDefinition
736-
simplifierx
737733
koreSolverOptions
738734
definitionFileName
739735
mainModuleName
@@ -758,7 +754,7 @@ koreProve ::
758754
LocalOptions KoreExecOptions ->
759755
KoreProveOptions ->
760756
Main (KFileLocations, ExitCode)
761-
koreProve LocalOptions{execOptions, simplifierx} proveOptions = do
757+
koreProve LocalOptions{execOptions} proveOptions = do
762758
let KoreExecOptions{definitionFileName} = execOptions
763759
KoreProveOptions{specFileName} = proveOptions
764760
definition <- loadDefinitions [definitionFileName, specFileName]
@@ -777,7 +773,6 @@ koreProve LocalOptions{execOptions, simplifierx} proveOptions = do
777773
prove
778774
minDepth
779775
stuckCheck
780-
simplifierx
781776
graphSearch
782777
breadthLimit
783778
depthLimit
@@ -871,7 +866,7 @@ koreBmc ::
871866
LocalOptions KoreExecOptions ->
872867
KoreProveOptions ->
873868
Main (KFileLocations, ExitCode)
874-
koreBmc LocalOptions{execOptions, simplifierx} proveOptions = do
869+
koreBmc LocalOptions{execOptions} proveOptions = do
875870
let KoreExecOptions{definitionFileName} = execOptions
876871
KoreProveOptions{specFileName} = proveOptions
877872
definition <- loadDefinitions [definitionFileName, specFileName]
@@ -885,7 +880,6 @@ koreBmc LocalOptions{execOptions, simplifierx} proveOptions = do
885880
KoreProveOptions{graphSearch} = proveOptions
886881
checkResult <-
887882
boundedModelCheck
888-
simplifierx
889883
breadthLimit
890884
depthLimit
891885
mainModule

‎kore/app/match-disjunction/Main.hs‎

Lines changed: 1 addition & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -144,7 +144,7 @@ mainWithOptions localOptions@LocalOptions{execOptions} = do
144144
KoreMatchDisjunctionOptions{koreLogOptions} = execOptions
145145

146146
koreMatchDisjunction :: LocalOptions KoreMatchDisjunctionOptions -> Main ExitCode
147-
koreMatchDisjunction LocalOptions{execOptions, simplifierx} = do
147+
koreMatchDisjunction LocalOptions{execOptions} = do
148148
definition <- loadDefinitions [definitionFileName]
149149
mainModule <- loadModule mainModuleName definition
150150
matchPattern <- mainParseMatchPattern (indexedModuleSyntax mainModule) matchFileName
@@ -154,7 +154,6 @@ koreMatchDisjunction LocalOptions{execOptions, simplifierx} = do
154154
clockSomethingIO "Executing" $
155155
runNoSMT $
156156
matchDisjunction
157-
simplifierx
158157
mainModule
159158
matchPattern
160159
disjunctionPattern

‎kore/app/repl/Main.hs‎

Lines changed: 1 addition & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -193,7 +193,7 @@ main = do
193193
whenJust (localOptions options) mainWithOptions
194194

195195
mainWithOptions :: LocalOptions KoreReplOptions -> IO ()
196-
mainWithOptions LocalOptions{execOptions, simplifierx} = do
196+
mainWithOptions LocalOptions{execOptions} = do
197197
exitCode <-
198198
withBugReport Main.exeName bugReportOption $ \tempDirectory ->
199199
withLogger tempDirectory koreLogOptions $ \actualLogAction -> do
@@ -247,7 +247,6 @@ mainWithOptions LocalOptions{execOptions, simplifierx} = do
247247
$ proveWithRepl
248248
replMinDepth
249249
replStuckCheck
250-
simplifierx
251250
validatedDefinition
252251
specDefIndexedModule
253252
Nothing

‎kore/app/rpc/Main.hs‎

Lines changed: 2 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -140,10 +140,9 @@ mainWithOptions localOptions@GlobalMain.LocalOptions{execOptions = KoreRpcServer
140140
koreRpcServerRun ::
141141
GlobalMain.LocalOptions KoreRpcServerOptions ->
142142
GlobalMain.Main ExitCode
143-
koreRpcServerRun GlobalMain.LocalOptions{execOptions, simplifierx} = do
143+
koreRpcServerRun GlobalMain.LocalOptions{execOptions} = do
144144
GlobalMain.SerializedDefinition{serializedModule, lemmas} <-
145145
GlobalMain.deserializeDefinition
146-
simplifierx
147146
koreSolverOptions
148147
definitionFileName
149148
mainModuleName
@@ -163,7 +162,7 @@ koreRpcServerRun GlobalMain.LocalOptions{execOptions, simplifierx} = do
163162
(SMT.stopSolver . SMT.refSolverHandle)
164163
$ \solverSetup -> do
165164
-- wrap the call to runServer in the logger monad
166-
Log.LoggerT $ ReaderT $ \loggerEnv -> runServer port solverSetup loggerEnv simplifierx serializedModule
165+
Log.LoggerT $ ReaderT $ \loggerEnv -> runServer port solverSetup loggerEnv serializedModule
167166

168167
pure ExitSuccess
169168
where

‎kore/app/share/GlobalMain.hs‎

Lines changed: 4 additions & 20 deletions
Original file line numberDiff line numberDiff line change
@@ -133,7 +133,6 @@ import Kore.Rewrite.SMT.Lemma
133133
import Kore.Rewrite.Strategy (
134134
GraphSearchOrder (..),
135135
)
136-
import Kore.Simplify.Simplify (SimplifierXSwitch (..))
137136
import Kore.Syntax hiding (Pattern)
138137
import Kore.Syntax.Definition (
139138
ModuleName (..),
@@ -319,9 +318,8 @@ data MainOptions a = MainOptions
319318
, localOptions :: !(Maybe (LocalOptions a))
320319
}
321320

322-
data LocalOptions a = LocalOptions
323-
{ execOptions :: !a
324-
, simplifierx :: !SimplifierXSwitch
321+
newtype LocalOptions a = LocalOptions
322+
{ execOptions :: a
325323
}
326324

327325
{- |
@@ -371,15 +369,6 @@ globalCommandLineParser =
371369
<> help "Print version information"
372370
)
373371

374-
parseSimplifierX :: Parser SimplifierXSwitch
375-
parseSimplifierX =
376-
flag
377-
DisabledSimplifierX
378-
EnabledSimplifierX
379-
( long "simplifierx"
380-
<> help "Enable the experimental simplifier"
381-
)
382-
383372
getArgs ::
384373
-- | environment variable name for extra arguments
385374
Maybe String ->
@@ -418,7 +407,6 @@ commandLineParse (ExeName exeName) maybeEnv parser infoMod = do
418407
parseLocalOptions =
419408
LocalOptions
420409
<$> parser
421-
<*> parseSimplifierX
422410
parseMainOptions =
423411
MainOptions
424412
<$> globalCommandLineParser
@@ -595,13 +583,11 @@ and either deserialize it, or else treat it as a text KORE definition and manual
595583
construct the needed SerializedDefinition object from it.
596584
-}
597585
deserializeDefinition ::
598-
SimplifierXSwitch ->
599586
KoreSolverOptions ->
600587
FilePath ->
601588
ModuleName ->
602589
Main SerializedDefinition
603590
deserializeDefinition
604-
simplifierx
605591
solverOptions
606592
definitionFilePath
607593
mainModuleName =
@@ -613,7 +599,6 @@ deserializeDefinition
613599
return serializedDefinition
614600
Nothing ->
615601
makeSerializedDefinition
616-
simplifierx
617602
solverOptions
618603
definitionFilePath
619604
mainModuleName
@@ -646,19 +631,18 @@ deserializeDefinition
646631
)
647632

648633
makeSerializedDefinition ::
649-
SimplifierXSwitch ->
650634
KoreSolverOptions ->
651635
FilePath ->
652636
ModuleName ->
653637
Main SerializedDefinition
654-
makeSerializedDefinition simplifierx solverOptions definitionFileName mainModuleName = do
638+
makeSerializedDefinition solverOptions definitionFileName mainModuleName = do
655639
definition <- loadDefinitions [definitionFileName]
656640
mainModule <- loadModule mainModuleName definition
657641
let metadataTools = MetadataTools.build mainModule
658642
let lemmas = getSMTLemmas mainModule
659643
serializedModule <-
660644
execute solverOptions metadataTools lemmas $
661-
makeSerializedModule simplifierx mainModule
645+
makeSerializedModule mainModule
662646
let locations = kFileLocations definition
663647
let serializedDefinition =
664648
SerializedDefinition

0 commit comments

Comments
 (0)