Add tests for ModelValidation scoring

smtcomp/test_generation.py

@@ -22,6 +22,7 @@
 file_unsat = defs.Smt2File(incremental=False, logic=defs.Logic.QF_ABV, family=daisy_family, name="unsat.smt2")
 
 file_unknown = defs.Smt2File(incremental=False, logic=defs.Logic.QF_ABV, family=daisy_family, name="unkown.smt2")
+""" This file is unsat in the generated single query results"""
 
 file_incremental = defs.Smt2File(
     incremental=True, logic=defs.Logic.QF_ABV, family=daisy_family, name="incremental.smt2"
@@ -45,7 +46,12 @@ def mk_submission(name: str) -> defs.Submission:
             participations=defs.Participations(
                 [
                     defs.Participation(
-                        tracks=[defs.Track.SingleQuery, defs.Track.UnsatCore, defs.Track.Incremental],
+                        tracks=[
+                            defs.Track.SingleQuery,
+                            defs.Track.UnsatCore,
+                            defs.Track.Incremental,
+                            defs.Track.ModelValidation,
+                        ],
                         logics=defs.Logics([defs.Logic.QF_ABV]),
                     )
                 ]
@@ -120,6 +126,15 @@ def mk_uc_results() -> defs.Results:
     )
 
 
+def mk_mv_results() -> defs.Results:
+
+    return defs.Results(
+        results=mk_results(defs.Track.SingleQuery, solver_best, [(file_sat, defs.Answer.Sat, 1)])
+        + mk_results(defs.Track.SingleQuery, solver_sound, [(file_sat, defs.Answer.ModelParsingError, 1)])
+        + mk_results(defs.Track.SingleQuery, solver_error, [(file_sat, defs.Answer.ModelUnsat, 1)])
+    )
+
+
 def mk_inc_results() -> defs.Results:
     results = [(file_incremental, defs.Answer.Incremental, 7)]
 
@@ -142,6 +157,7 @@ def write_test_files(data: Path) -> None:
     for track, gen in [
         (defs.Track.SingleQuery, mk_sq_results),
         (defs.Track.UnsatCore, mk_uc_results),
+        (defs.Track.ModelValidation, mk_mv_results),
         (defs.Track.Incremental, mk_inc_results),
     ]:
         write_cin(config.current_results[track], gen().model_dump_json(indent=2))

tests/test_validate.py

@@ -124,6 +124,32 @@ def test_results_uc_export(config: defs.Config) -> None:
     assert podium.sequential[2].correctScore == 3
 
 
+def test_results_mv_export(config: defs.Config) -> None:
+    print(config.data)
+    track = defs.Track.ModelValidation
+    results, selection = smtcomp.results.helper_get_results(config, [], track)
+    scores = smtcomp.scoring.add_disagreements_info(results, track)
+    sound_solvers = scores.filter(sound_solver=True).select("solver").unique().collect()["solver"].sort().to_list()
+    assert sound_solvers == [gtests.solver_best, gtests.solver_sound]
+    smtcomp.generate_website_page.export_results(config, selection, results, track)
+    page_suffix = smtcomp.generate_website_page.page_track_suffix(track)
+    podium = smtcomp.generate_website_page.PodiumDivision.model_validate_json(
+        (config.web_results / f"{gtests.logic.name.lower()}-{page_suffix}.md").read_text()
+    )
+    print(podium)
+    assert podium.winner_seq == gtests.solver_best
+
+    assert podium.sequential[0].name == gtests.solver_best
+    assert podium.sequential[0].errorScore == 0
+    assert podium.sequential[0].correctScore == 1
+    assert podium.sequential[1].name == gtests.solver_sound
+    assert podium.sequential[1].errorScore == 0
+    assert podium.sequential[1].correctScore == 0
+    assert podium.sequential[2].name == gtests.solver_error
+    assert podium.sequential[2].errorScore == 1
+    assert podium.sequential[2].correctScore == 0
+
+
 def test_results_inc_export(config: defs.Config) -> None:
     print(config.data)
     track = defs.Track.Incremental