Skip to content

Back-translate the SMTLIB unary minus, ignore models in "get-model" tests #4033

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
merged 3 commits into from
Aug 14, 2024
Merged

Back-translate the SMTLIB unary minus, ignore models in "get-model" tests #4033

Show file tree
Hide file tree
Changes from 1 commit
Commits
Show all changes
3 commits
Select commit Hold shift + click to select a range
6e4bb49
Allow "-" when back-translating
geo2a Aug 13, 2024
eb53a89
Back-translate -X as -X, not 0 - X
geo2a Aug 14, 2024
586cd59
Add default values in checkGoldenGetModel
geo2a Aug 14, 2024
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
13 changes: 11 additions & 2 deletions kore/src/Kore/Rewrite/SMT/Translate.hs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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']
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I think we should rather just negate the InternalInt that we expect inside arg, unless that does not work for some reason...

Suggested change
arg' <- backTranslate arg
pure $ TermLike.mkApplySymbol koreSym [mkInternalInt (InternalInt (simpleSort "SortInt") 0), arg']
arg' <- backTranslate arg
case arg' of
InternalInt intSort n -> pure $ InternalInt intSort (negate n)
other -> throwError $ "unable to translate negation of " <> show other

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Thanks, that worked, modulo juggling Kore's data constructors.

-- everything is translated back using symbol declarations,
-- not ML connectives (translating terms not predicates)
| (fct@Atom{} : rest) <- xs
Expand Down Expand Up @@ -561,12 +566,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
Expand Down
35 changes: 33 additions & 2 deletions test/rpc-server/runTests.py
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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 []
Expand All @@ -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:")

Expand Down
Loading