From 528f2a040c0c569280df835e699bf06ac4526a0c Mon Sep 17 00:00:00 2001 From: Bajczi Levente Date: Sun, 8 Jun 2025 09:43:03 +0200 Subject: [PATCH] Instead of assuming first line is "sat", find it --- validate-model.py | 21 +++++++++++++-------- 1 file changed, 13 insertions(+), 8 deletions(-) diff --git a/validate-model.py b/validate-model.py index d1084bb..f29907b 100755 --- a/validate-model.py +++ b/validate-model.py @@ -9,16 +9,21 @@ funs = {} + def define_funs(cmds, funs): for cmd in cmds: match cmd: case ("define-fun", name, *args): funs[name] = cmd + if True: file = sys.stdin - status = file.readline().strip() - assert status == "sat" + for line in file: + if line.strip() == "sat": + break + else: + raise ValueError("No line with 'sat' found") content = file.read() model = smtlib.parse_exprs(content) @@ -34,8 +39,8 @@ def define_funs(cmds, funs): define_funs(cmds, funs) with open(chc_file, "r") as file: - content = file.read() - cmds = smtlib.parse_exprs(content) + content = file.read() + cmds = smtlib.parse_exprs(content) defs = [] clauses = [] @@ -54,11 +59,11 @@ def define_funs(cmds, funs): case ("assert", phi): clauses.append(phi) - case ("check-sat", ): + case ("check-sat",): pass - case ("get-model", ): + case ("get-model",): pass - case ("exit", ): + case ("exit",): pass case _: @@ -74,4 +79,4 @@ def define_funs(cmds, funs): print(line) print("(set-info :status unsat)") -print("(check-sat)") \ No newline at end of file +print("(check-sat)")