Skip to content

Commit

Permalink
feat: add state specific tactic feedback
Browse files Browse the repository at this point in the history
  • Loading branch information
sorgfresser authored and lenianiva committed Oct 31, 2024
1 parent 93ecd0d commit b89f3a1
Showing 1 changed file with 3 additions and 3 deletions.
6 changes: 3 additions & 3 deletions pantograph/search.py
Original file line number Diff line number Diff line change
Expand Up @@ -15,6 +15,7 @@ class SearchState:
parent: Optional[int]
parent_goal_id: Optional[int]
priorities: list[float]
tactic_feedback: Optional[str] = None

def __post_init__(self):
assert len(self.priorities) == len(self.state.goals)
Expand Down Expand Up @@ -48,7 +49,6 @@ class Agent:
"""
An agent interface for proof search
"""
tactic_feedback: Optional[str] = None

@abstractmethod
def next_tactic(
Expand Down Expand Up @@ -126,7 +126,7 @@ def search(self,
print(f"Next tactic: {tactic}")
if not tactic:
# resets the feedback
self.tactic_feedback = None
search_state.tactic_feedback = None
# pop the current state and continue to the next
search_stack.pop(-1)
if not search_stack:
Expand Down Expand Up @@ -163,7 +163,7 @@ def search(self,
except TacticFailure as t:
if verbose:
print(f"Tactic failed: {t}")
self.tactic_feedback = str(t)
search_state.tactic_feedback = str(t)
# try the next tactic. this one failed
except ServerError as e:
raise RuntimeError(f"While executing tactic: {tactic}") from e
Expand Down

0 comments on commit b89f3a1

Please sign in to comment.