Coverage for sparkle/solver/verifiers.py: 91%

1"""Classes for verifying solutions.""" 

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 verify(self: SolutionVerifier, 

13 instance: Path, 

14 output: dict, 

15 solver_call: list[str]) -> SolverStatus: 

16 """Verify the solution.""" 

17 raise NotImplementedError 

18 

19 

20class SATVerifier(SolutionVerifier): 

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

22 sat_verifier_path =\ 

23 Path(__file__).parent.parent / "Components/Sparkle-SAT-verifier/SAT" 

24 

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

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

27 return SATVerifier.__name__ 

28 

29 @staticmethod 

30 def verify(instance: Path, output: dict, solver_call: list[str]) -> SolverStatus: 

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

32 if SolverStatus(output["status"]) == SolverStatus.TIMEOUT: 

33 return SolverStatus.TIMEOUT 

34 raw_result = Path([s for s in solver_call if s.endswith(".rawres")][0]) 

35 return SATVerifier.call_sat_raw_result(instance, raw_result) 

36 

37 @staticmethod 

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

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

40 

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

42 """ 

43 return_code = int(sat_output.splitlines()[-1]) 

44 if return_code == 11: # SAT code 

45 return SolverStatus.SAT 

46 if return_code == 10: # UNSAT code 

47 return SolverStatus.UNSAT 

48 # Wrong code OR Unknown code 

49 if return_code == 0 and "Wrong solution." in sat_output: 

50 return SolverStatus.WRONG 

51 # Should not occur 

52 return SolverStatus.UNKNOWN 

53 

54 @staticmethod 

55 def call_sat_raw_result(instance: Path, 

56 raw_result: Path) -> SolverStatus: 

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

58 

59 Args: 

60 instance: path to the instance 

61 raw_result: path to the result to verify 

62 

63 Returns: 

64 The status of the solver on the instance 

65 """ 

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

67 instance, 

68 raw_result], 

69 capture_output=True) 

70 return SATVerifier.sat_verify_output(sat_verify.stdout.decode()) 

71 

72 

73class SolutionFileVerifier(SolutionVerifier): 

74 """Class to handle the file verifier.""" 

75 

76 def __init__(self: SolutionFileVerifier, csv_file: Path) -> None: 

77 """Initialize the verifier by building dictionary from csv. 

78 

79 Args: 

80 csv_file: path to the csv file. Requires lines to be of the form: 

81 instance,objective,solution 

82 """ 

83 self.csv_file = csv_file 

84 lines = [line.split(",", maxsplit=2) 

85 for line in self.csv_file.read_text().splitlines()] 

86 self.solutions = {instance: (objective, solution) 

87 for instance, objective, solution in lines} 

88 

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

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

91 return SolutionFileVerifier.__name__ 

92 

93 def verify(self: SolutionFileVerifier, 

94 instance: Path, 

95 solver_output: dict[str, object], 

96 solver_call: list[str]) -> SolverStatus: 

97 """Verify the solution. 

98 

99 Args: 

100 instance: instance to verify, solution found by instance name as key 

101 solver_output: outcome of the solver to verify 

102 

103 Returns: 

104 The status of the solver on the instance 

105 """ 

106 # If the solver ran out of time, we cannot verify a solution 

107 if SolverStatus(solver_output["status"]) == SolverStatus.TIMEOUT: 

108 return SolverStatus.TIMEOUT 

109 instance = instance.name 

110 if instance not in self.solutions: 

111 return SolverStatus.UNKNOWN 

112 

113 objective, solution = self.solutions[instance] 

114 if objective not in solver_output: 

115 return SolverStatus.UNKNOWN 

116 

117 outcome = solver_output[objective] 

118 if solution in SolverStatus._value2member_map_: # SAT type status 

119 solution, outcome = SolverStatus(solution), SolverStatus(outcome) 

120 if solution == SolverStatus.UNKNOWN or solution == outcome: 

121 # Verify that the presented solution is correct 

122 return SATVerifier.verify(instance, solver_output, solver_call) 

123 else: 

124 return SolverStatus.WRONG 

125 

126 if solution != outcome: 

127 return SolverStatus.WRONG 

128 return SolverStatus.SUCCESS 

129 

130 

131# Define a mapping so we can translate between names and classes 

132mapping = {SATVerifier.__name__: SATVerifier, 

133 SolutionFileVerifier.__name__: SolutionFileVerifier}