Coverage for sparkle/solver/verifier.py: 46%

1"""Methods related to SAT specific runs.""" 

2from __future__ import annotations 

3from pathlib import Path 

4import subprocess 

5 

6from sparkle.types import SolverStatus 

7 

8 

9class SolutionVerifier: 

10 """Solution verifier base class.""" 

11 

12 def __init__(self: SolutionVerifier) -> None: 

13 """Initialize the solution verifier.""" 

14 raise NotImplementedError 

15 

16 def verifiy(self: SolutionVerifier) -> SolverStatus: 

17 """Verify the solution.""" 

18 raise NotImplementedError 

19 

20 

21class SATVerifier(SolutionVerifier): 

22 """Class to handle the SAT verifier.""" 

23 sat_verifier_path = Path("sparkle/Components/Sparkle-SAT-verifier/SAT") 

24 

25 def __init__(self: SATVerifier) -> None: 

26 """Initialize the SAT verifier.""" 

27 return 

28 

29 def __str__(self: SATVerifier) -> str: 

30 """Return the name of the SAT verifier.""" 

31 return "SATVerifier" 

32 

33 def verify(self: SATVerifier, instance: Path, raw_result: Path) -> SolverStatus: 

34 """Run a SAT verifier and return its status.""" 

35 return SATVerifier.sat_judge_correctness_raw_result(instance, raw_result) 

36 

37 @staticmethod 

38 def sat_get_verify_string(sat_output: str) -> SolverStatus: 

39 """Return the status of the SAT verifier. 

40 

41 Four statuses are possible: "SAT", "UNSAT", "WRONG", "UNKNOWN" 

42 """ 

43 lines = [line.strip() for line in sat_output.splitlines()] 

44 for index, line in enumerate(lines): 

45 if line == "Solution verified.": 

46 if lines[index + 2] == "11": 

47 return SolverStatus.SAT 

48 elif line == "Solver reported unsatisfiable. I guess it must be right!": 

49 if lines[index + 2] == "10": 

50 return SolverStatus.UNSAT 

51 elif line == "Wrong solution.": 

52 if lines[index + 2] == "0": 

53 return SolverStatus.WRONG 

54 return SolverStatus.UNKNOWN 

55 

56 @staticmethod 

57 def sat_judge_correctness_raw_result(instance: Path, 

58 raw_result: Path) -> SolverStatus: 

59 """Run a SAT verifier to determine correctness of a result. 

60 

61 Args: 

62 instance: path to the instance 

63 raw_result: path to the result to verify 

64 

65 Returns: 

66 The status of the solver on the instance 

67 """ 

68 sat_verify = subprocess.run([SATVerifier.sat_verifier_path, 

69 instance, 

70 raw_result], 

71 capture_output=True) 

72 return SATVerifier.sat_get_verify_string(sat_verify.stdout.decode())