Partially revert the implication endpoint

booster/tools/booster/Proxy.hs

@@ -104,19 +104,24 @@ respondEither cfg@ProxyConfig{statsVar, boosterState} booster kore req = case re
                             fromMaybe (error $ "Module " <> show m <> " not found") $
                                 Map.lookup m bState.definitions
                     handleExecute logSettings def start execReq
-    Implies{} -> do
-        -- try the booster end-point first
-        (boosterResult, boosterTime) <- Stats.timed $ booster req
-        case boosterResult of
-            res@Right{} -> do
-                logStats ImpliesM (boosterTime, 0)
-                pure res
-            Left err -> do
-                Log.logWarnNS "proxy" . Text.pack $
-                    "implies error in booster: " <> fromError err
-                (koreRes, koreTime) <- Stats.timed $ kore req
-                logStats ImpliesM (boosterTime + koreTime, koreTime)
-                pure koreRes
+    Implies ImpliesRequest{assumeDefined}
+        | fromMaybe False assumeDefined -> do
+            -- try the booster end-point first
+            (boosterResult, boosterTime) <- Stats.timed $ booster req
+            case boosterResult of
+                res@Right{} -> do
+                    logStats ImpliesM (boosterTime, 0)
+                    pure res
+                Left err -> do
+                    Log.logWarnNS "proxy" . Text.pack $
+                        "implies error in booster: " <> fromError err
+                    (koreRes, koreTime) <- Stats.timed $ kore req
+                    logStats ImpliesM (boosterTime + koreTime, koreTime)
+                    pure koreRes
+        | otherwise -> do
+            (koreRes, koreTime) <- Stats.timed $ kore req
+            logStats ImpliesM (koreTime, koreTime)
+            pure koreRes
     Simplify simplifyReq ->
         liftIO (getTime Monotonic) >>= handleSimplify simplifyReq . Just
     AddModule _ -> do

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

@@ -338,12 +338,15 @@ Not all backends support logging processing time, and some won't have the differ
     "antecedent": {"format": "KORE", "version": 1, "term": {}},
     "consequent": {"format": "KORE", "version": 1, "term": {}},
     "module": "MODULE-NAME",
-    "log-timing": true
+    "log-timing": true,
+    "assume-defined": false
   }
 }
 ```
 
-Optional parameters: `module` (main module name), `log-timing`
+Optional parameters: `module` (main module name), `log-timing`, `assume-defined`.
+
+The `assume-defined` flag defaults to `false`. When set to `true`, the server uses the new simplified implication check in booster, which makes the assumption that the antecedent and consequent are bot defined, i.e. don't simplify to `#Bottom`.
 
 ### Error Response:
 

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

@@ -53,6 +53,7 @@ data ImpliesRequest = ImpliesRequest
     { antecedent :: !KoreJson
     , consequent :: !KoreJson
     , _module :: !(Maybe Text)
+    , assumeDefined :: !(Maybe Bool)
     , logSuccessfulSimplifications :: !(Maybe Bool)
     , logFailedSimplifications :: !(Maybe Bool)
     , logTiming :: !(Maybe Bool)