Allow "-" when back-translating

Back-translate (wrongly) unary minus

Special-case the test script for get-model

Remove special case for "-"

Special-case unary minus in a different way

add comment

Author: geo2a

kore/src/Kore/Rewrite/SMT/Translate.hs

@@ -533,6 +533,11 @@ backTranslateWith
         backTranslate (List xs)
             | null xs =
                 throwError "backtranslate: empty list"
+            -- special case for the unary minus, back-translating 'List ["-", "X"]' as '0 - X'
+            | [fct@(Atom "-"), arg] <- xs
+            , Just koreSym <- Map.lookup fct reverseMetadata = do
+                arg' <- backTranslate arg
+                pure $ TermLike.mkApplySymbol koreSym [mkInternalInt (InternalInt (simpleSort "SortInt") 0), arg']
             -- everything is translated back using symbol declarations,
             -- not ML connectives (translating terms not predicates)
             | (fct@Atom{} : rest) <- xs
@@ -563,8 +568,11 @@ backTranslateWith
                 . Map.map AST.symbolData
                 $ Map.filter (not . isBuiltin . AST.symbolDeclaration) symbols
 
-        isBuiltin :: AST.KoreSymbolDeclaration a b -> Bool
-        isBuiltin AST.SymbolBuiltin{} = True
+        isBuiltin :: AST.KoreSymbolDeclaration SExpr SExpr -> Bool
+        isBuiltin (AST.SymbolBuiltin (AST.IndirectSymbolDeclaration{name})) =
+            case name of
+                Atom "-" -> False
+                _ -> True
         isBuiltin _other = False
 
         symbolFrom :: Id -> Symbol

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["result"]["satisfiable"] != resp_json["result"]["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:")