Rename "assume-state-define" to "assume-defined"

Author: geo2a

booster/library/Booster/JsonRpc.hs

@@ -132,7 +132,7 @@ respond stateVar request =
                                         , req.logFailedRewrites
                                         ]
                             checkConstraintsConsistent =
-                                case req.assumeStateDefined of
+                                case req.assumeDefined of
                                     Nothing -> ApplyEquations.CheckConstraintsConsistent
                                     Just False -> ApplyEquations.CheckConstraintsConsistent
                                     Just True -> ApplyEquations.NoCheckConstraintsConsistent

booster/tools/booster/Proxy.hs

@@ -351,7 +351,7 @@ respondEither cfg@ProxyConfig{boosterState} booster kore req = case req of
                                             r
                                                 { state = execStateToKoreJson simplifiedBoosterState
                                                 , maxDepth = Just $ Depth 1
-                                                , assumeStateDefined = Just True
+                                                , assumeDefined = Just True
                                                 }
                                         )
                             Booster.Log.withContexts [CtxProxy, CtxTiming, CtxKore] $

docs/2022-07-18-JSON-RPC-Server-API.md

@@ -24,7 +24,7 @@ The server runs over sockets and can be interacted with by sending JSON RPC mess
   "method": "execute",
   "params": {
     "max-depth": 4,
-    "assume-state-defined": true,
+    "assume-defined": true,
     "cut-point-rules": ["rule1"],
     "terminal-rules": ["ruleFoo"],
     "moving-average-step-timeout": true,
@@ -41,9 +41,9 @@ The server runs over sockets and can be interacted with by sending JSON RPC mess
 }
 ```
 
-Optional parameters: `max-depth`, `cut-point-rules`, `terminal-rules`, `moving-average-step-timeout`, `step-timeout` (timeout is in milliseconds), `module` (main module name), `assume-state-defined` (description follows) and all the `log-*` options, which default to false if unspecified.
+Optional parameters: `max-depth`, `cut-point-rules`, `terminal-rules`, `moving-average-step-timeout`, `step-timeout` (timeout is in milliseconds), `module` (main module name), `assume-defined` (description follows) and all the `log-*` options, which default to false if unspecified.
 
-The `assume-state-defined` flag has different meaning in Booster and Kore. If set to `true`, Booster will not check the constraints of the initial pattern for satisfiability. It is the responsibility of the caller to ensure that the pattern is not vacuous. In Kore, if `assume-state-defined` is set to `true`, then all sub-terms of `state` will be assumed to be defined before attempting rewrite rules.
+The `assume-defined` flag defaults to `false`. The `assume-defined` flag has different meaning in Booster and Kore. If set to `true`, Booster will not check the constraints of the initial pattern for satisfiability. It is the responsibility of the caller to ensure that the pattern is not vacuous. In Kore, if `assume-defined` is set to `true`, then all sub-terms of `state` will be assumed to be defined before attempting rewrite rules.
 
 _Note: `id` can be an int or a string and each message must have a new `id`. The response objects have the same id as the message._
 

kore-rpc-types/src/Kore/JsonRpc/Types.hs

@@ -43,7 +43,7 @@ data ExecuteRequest = ExecuteRequest
     , terminalRules :: !(Maybe [Text])
     , movingAverageStepTimeout :: !(Maybe Bool)
     , stepTimeout :: !(Maybe Int)
-    , assumeStateDefined :: !(Maybe Bool)
+    , assumeDefined :: !(Maybe Bool)
     , logSuccessfulRewrites :: !(Maybe Bool)
     , logFailedRewrites :: !(Maybe Bool)
     }

kore/src/Kore/JsonRpc.hs

@@ -141,7 +141,7 @@ respond reqId serverState moduleName runSMT =
                 , cutPointRules
                 , terminalRules
                 , movingAverageStepTimeout
-                , assumeStateDefined
+                , assumeDefined
                 , stepTimeout
                 , logSuccessfulRewrites
                 } -> withMainModule (coerce _module) $ \serializedModule lemmas -> do
@@ -167,7 +167,7 @@ respond reqId serverState moduleName runSMT =
                                                 then EnableMovingAverage
                                                 else DisableMovingAverage
                                             )
-                                            ( if fromMaybe False assumeStateDefined
+                                            ( if fromMaybe False assumeDefined
                                                 then EnableAssumeInitialDefined
                                                 else DisableAssumeInitialDefined
                                             )