From 53d55df394eed4e17d37b62119e2db63facf87ee Mon Sep 17 00:00:00 2001
From: Georgy Lukyanov <mail@geo2a.info>
Date: Wed, 14 Aug 2024 10:30:07 +0200
Subject: [PATCH] Back-translate the SMTLIB unary minus, ignore models in
 `"get-model"` tests (#4033)

This is a bridge PR that we need before bumping Z3 to 4.13.0.

- modify `test/rpc-server/runTests.py` to not compare the actual model
from `"get-model"` responses, as it may be non-deterministic. Only
compare the `"satisfiable"` field, i.e. model existence;
- when back-translating the results of `"get-model"` from SMTLIB2
s-expression to Kore, allow unary minus.
---
 kore/src/Kore/Rewrite/SMT/Translate.hs | 14 +++++++++--
 test/rpc-server/runTests.py            | 35 ++++++++++++++++++++++++--
 2 files changed, 45 insertions(+), 4 deletions(-)

diff --git a/kore/src/Kore/Rewrite/SMT/Translate.hs b/kore/src/Kore/Rewrite/SMT/Translate.hs
index ba3014fd62..c2f575583f 100644
--- a/kore/src/Kore/Rewrite/SMT/Translate.hs
+++ b/kore/src/Kore/Rewrite/SMT/Translate.hs
@@ -533,6 +533,12 @@ backTranslateWith
         backTranslate (List xs)
             | null xs =
                 throwError "backtranslate: empty list"
+            -- special case for the unary minus, back-translating 'List ["-", "X"]' as '-X'
+            | [Atom "-", arg] <- xs = do
+                arg' <- backTranslate arg
+                case arg' of
+                    InternalInt_ (InternalInt intSort n) -> pure . TermLike.mkInternalInt $ InternalInt intSort (negate n)
+                    other -> throwError $ "unable to translate negation of " <> show other
             -- everything is translated back using symbol declarations,
             -- not ML connectives (translating terms not predicates)
             | (fct@Atom{} : rest) <- xs
@@ -561,12 +567,16 @@ backTranslateWith
             Map.map symbolFrom
                 . invert
                 . Map.map AST.symbolData
-                $ Map.filter (not . isBuiltin . AST.symbolDeclaration) symbols
+                $ Map.filter ((\sym -> (not (isBuiltin sym) || isMinus sym)) . AST.symbolDeclaration) symbols
 
-        isBuiltin :: AST.KoreSymbolDeclaration a b -> Bool
+        isBuiltin :: AST.KoreSymbolDeclaration SExpr SExpr -> Bool
         isBuiltin AST.SymbolBuiltin{} = True
         isBuiltin _other = False
 
+        isMinus :: AST.KoreSymbolDeclaration SExpr SExpr -> Bool
+        isMinus (AST.SymbolBuiltin (AST.IndirectSymbolDeclaration{name})) = name == Atom "-"
+        isMinus _other = False
+
         symbolFrom :: Id -> Symbol
         symbolFrom name =
             Symbol
diff --git a/test/rpc-server/runTests.py b/test/rpc-server/runTests.py
index fad1992984..ed22c81ad5 100644
--- a/test/rpc-server/runTests.py
+++ b/test/rpc-server/runTests.py
@@ -103,7 +103,34 @@ def checkGolden (resp, resp_golden_path):
     info(f"Golden file {red}not found{endred}")
     exit(1)
 
-
+def checkGoldenGetModel(resp, resp_golden_path):
+  '''Almost exactly like checkGolden, but only compares the result->satisfiable field of the reponses'''
+  if os.path.exists(resp_golden_path):
+    debug("Checking against golden file...")
+    with open(resp_golden_path, 'rb') as resp_golden_raw:
+      golden_json = json.loads(resp_golden_raw.read())
+      resp_json = json.loads(resp)
+      if golden_json.get("result", {"IMPOSSIBLE": "IMPOSSIBLE"}).get("satisfiable", "IMPOSSIBLE") != resp_json.get("result", {}).get("satisfiable", ""):
+        print(f"Test '{name}' {red}failed.{endred}")
+        info(diff_strings(str(golden_json), str(resp)))
+        if RECREATE_BROKEN_GOLDEN:
+          with open(resp_golden_path, 'wb') as resp_golden_writer:
+            resp_golden_writer.write(resp)
+        else:
+          info("Expected")
+          info(golden_json)
+          info("but got")
+          info(resp)
+          exit(1)
+      else:
+        info(f"Test '{name}' {green}passed{endgreen}")
+  elif CREATE_MISSING_GOLDEN or RECREATE_BROKEN_GOLDEN:
+    with open(resp_golden_path, 'wb') as resp_golden_writer:
+      resp_golden_writer.write(resp)
+  else:
+    debug(resp)
+    info(f"Golden file {red}not found{endred}")
+    exit(1)
 
 def runTest(def_path, req, resp_golden_path, smt_tactic = None):
     smt_options = ["--smt-tactic", str(smt_tactic)] if smt_tactic else []
@@ -122,7 +149,11 @@ def runTest(def_path, req, resp_golden_path, smt_tactic = None):
           debug(resp)
           process.kill()
 
-          checkGolden(resp, resp_golden_path)
+          req_method = json.loads(req)["method"]
+          if req_method == "get-model":
+              checkGoldenGetModel(resp, resp_golden_path)
+          else:
+              checkGolden(resp, resp_golden_path)
 
 print("Running execute tests:")