aniva/Pantograph
aniva
/
Pantograph
1
1
Fork 0
Code Issues 13 Pull Requests 4 Packages Projects Releases Wiki Activity

Merge branch 'feat/search' into experiments/minif2f

This commit is contained in:
Leni Aniva 2024-10-04 18:43:14 -07:00
parent 91c8de2ca0 9d9c7063cd
commit 6156f6a297
Signed by: aniva
GPG Key ID: 4D9B1C8D10EA4C50
1 changed files with 4 additions and 9 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

13
pantograph/search.py
View File

@ -52,8 +52,7 @@ class Agent:
self, self,
state: GoalState, state: GoalState,
goal_id: int, goal_id: int,
informal_stmt: str, ) -> Optional[Tactic]:
informal_proof: str) -> Optional[Tactic]:
""" """
Implement this function to generate the next tactic for a goal Implement this function to generate the next tactic for a goal
""" """
@ -74,8 +73,6 @@ class Agent:
def search(self, def search(self,
server: Server, server: Server,
goal_state: GoalState, goal_state: GoalState,
informal_stmt: str = "",
informal_proof: str = "",
max_steps: int = 100, max_steps: int = 100,
max_trials_per_goal: int = 5, max_trials_per_goal: int = 5,
verbose: bool = False) -> SearchResult: verbose: bool = False) -> SearchResult:
@ -83,13 +80,12 @@ class Agent:
Searches using th Searches using th
""" """
assert server.is_automatic(), "Search must be run in automatic mode" assert server.is_automatic(), "Search must be run in automatic mode"
assert len(goal_state.goals) == 1, "Initial state must have exactly one goal"
initial_state = SearchState( initial_state = SearchState(
state=goal_state, state=goal_state,
parent=None, parent=None,
parent_goal_id=None, parent_goal_id=None,
priorities=[0.0] priorities=[0.0 for _ in goal_state.goals]
) )
search_stack = [initial_state] search_stack = [initial_state]
""" """
@ -115,7 +111,7 @@ class Agent:
tactic = None tactic = None
else: else:
# Generate tactic for this goal # Generate tactic for this goal
tactic = self.next_tactic(search_state.state, goal_id, informal_stmt, informal_proof) tactic = self.next_tactic(search_state.state, goal_id)
if verbose: if verbose:
print(f"Next tactic: {tactic}") print(f"Next tactic: {tactic}")
@ -186,8 +182,7 @@ class DumbAgent(Agent):
self, self,
state: GoalState, state: GoalState,
goal_id: int, goal_id: int,
informal_stmt: str, ) -> Optional[Tactic]:
informal_proof: str) -> Optional[Tactic]:
key = (state.state_id, goal_id) key = (state.state_id, goal_id)
i = self.goal_tactic_id_map[key] i = self.goal_tactic_id_map[key]