From b3bd3cdde87ca40c89a125d77d3af79153ff2bf2 Mon Sep 17 00:00:00 2001 From: Leni Aniva Date: Wed, 2 Oct 2024 11:09:58 -0700 Subject: [PATCH 1/3] feat: Add binder name option in `TacticHave` --- pantograph/expr.py | 1 + pantograph/server.py | 16 ++++++++++++++++ 2 files changed, 17 insertions(+) diff --git a/pantograph/expr.py b/pantograph/expr.py index 895e56a..4312545 100644 --- a/pantograph/expr.py +++ b/pantograph/expr.py @@ -92,6 +92,7 @@ class GoalState: @dataclass(frozen=True) class TacticHave: branch: str + binder_name: Optional[str] = None @dataclass(frozen=True) class TacticCalc: step: str diff --git a/pantograph/server.py b/pantograph/server.py index 17927eb..e0f6870 100644 --- a/pantograph/server.py +++ b/pantograph/server.py @@ -123,6 +123,8 @@ class Server: args["tactic"] = tactic elif isinstance(tactic, TacticHave): args["have"] = tactic.branch + if tactic.binder_name: + args["binderName"] = tactic.binder_name elif isinstance(tactic, TacticCalc): args["calc"] = tactic.step else: @@ -285,6 +287,20 @@ class TestServer(unittest.TestCase): ) ]) + def test_have(self): + server = Server() + state0 = server.goal_start("1 + 1 = 2") + state1 = server.goal_tactic(state0, goal_id=0, tactic=TacticHave(branch="2 = 1 + 1", binder_name="h")) + self.assertEqual(state1.goals, [ + Goal( + variables=[], + target="2 = 1 + 1", + ), + Goal( + variables=[Variable(name="h", t="2 = 1 + 1")], + target="1 + 1 = 2", + ), + ]) def test_conv_calc(self): server = Server(options={"automaticMode": False}) From cfa9d103b9bf4f4ad07a2a1e53b6a838d425cbb4 Mon Sep 17 00:00:00 2001 From: Leni Aniva Date: Fri, 4 Oct 2024 18:41:33 -0700 Subject: [PATCH 2/3] feat: Improve feedback and provide default options --- pantograph/search.py | 21 ++++++++++++--------- pantograph/server.py | 20 ++++++++++++++------ 2 files changed, 26 insertions(+), 15 deletions(-) diff --git a/pantograph/search.py b/pantograph/search.py index 00b4284..cb87a70 100644 --- a/pantograph/search.py +++ b/pantograph/search.py @@ -1,3 +1,4 @@ +from abc import abstractmethod from dataclasses import dataclass from typing import Optional import collections, unittest @@ -44,24 +45,26 @@ class Agent: """ An agent interface for proof search """ + tactic_feedback: Optional[str] = None + @abstractmethod def next_tactic( self, state: GoalState, goal_id: int, - informal_stmt: str, - informal_proof: str) -> Optional[Tactic]: + ) -> Optional[Tactic]: """ Implement this function to generate the next tactic for a goal """ - return None + @abstractmethod def guidance(self, state: GoalState) -> list[float]: """ Return a list of priorities determining which goal should be searched first. This will not be called on states with one or zero goals. """ return [0.0 for _ in state.goals] + @abstractmethod def reset(self): """ Called after search @@ -70,8 +73,6 @@ class Agent: def search(self, server: Server, goal_state: GoalState, - informal_stmt: str = "", - informal_proof: str = "", max_steps: int = 100, max_trials_per_goal: int = 5, verbose: bool = False) -> SearchResult: @@ -111,16 +112,18 @@ class Agent: tactic = None else: # 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: print(f"Next tactic: {tactic}") if not tactic: + # resets the feedback + self.tactic_feedback = None # pop the current state and continue to the next search_stack.pop(-1) if not search_stack: if verbose: - print("Tactic list has been exhausted") + print("Search stack has been exhausted") self.reset() return SearchResult(success=False, steps=i_step) continue @@ -147,6 +150,7 @@ class Agent: except TacticFailure as t: if verbose: print(f"Tactic failed: {t}") + self.tactic_feedback = str(t) # try the next tactic. this one failed if verbose: @@ -179,8 +183,7 @@ class DumbAgent(Agent): self, state: GoalState, goal_id: int, - informal_stmt: str, - informal_proof: str) -> Optional[Tactic]: + ) -> Optional[Tactic]: key = (state.state_id, goal_id) i = self.goal_tactic_id_map[key] diff --git a/pantograph/server.py b/pantograph/server.py index e0f6870..e3770cc 100644 --- a/pantograph/server.py +++ b/pantograph/server.py @@ -19,6 +19,8 @@ class TacticFailure(Exception): class ServerError(Exception): pass +DEFAULT_CORE_OPTIONS=["maxHeartbeats=0", "maxRecDepth=10000"] + class Server: def __init__(self, @@ -28,8 +30,8 @@ class Server: # Options for executing the REPL. # Set `{ "automaticMode" : False }` to handle resumption by yourself. options={}, - core_options=[], - timeout=20, + core_options=DEFAULT_CORE_OPTIONS, + timeout=60, maxread=1000000): """ timeout: Amount of time to wait for execution @@ -86,7 +88,10 @@ class Server: self.proc.sendline(f"{cmd} {s}") try: line = self.proc.readline() - return json.loads(line) + try: + return json.loads(line) + except Exception as e: + raise ServerError(f"Cannot decode: {line}") from e except pexpect.exceptions.TIMEOUT as exc: raise exc @@ -96,9 +101,12 @@ class Server: Must be called periodically. """ - if self.to_remove_goal_states: - self.run('goal.delete', {'stateIds': self.to_remove_goal_states}) - self.to_remove_goal_states.clear() + if not self.to_remove_goal_states: + return + result = self.run('goal.delete', {'stateIds': self.to_remove_goal_states}) + self.to_remove_goal_states.clear() + if "error" in result: + raise ServerError(result["desc"]) def expr_type(self, expr: Expr) -> Expr: """ From 9d9c7063cd49bb19ad216efdb9b20be4d52903d9 Mon Sep 17 00:00:00 2001 From: Leni Aniva Date: Fri, 4 Oct 2024 18:42:33 -0700 Subject: [PATCH 3/3] feat: Remove the goal count restriction on initial state --- pantograph/search.py | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/pantograph/search.py b/pantograph/search.py index cb87a70..7aa3342 100644 --- a/pantograph/search.py +++ b/pantograph/search.py @@ -80,13 +80,12 @@ class Agent: Searches using th """ 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( state=goal_state, parent=None, parent_goal_id=None, - priorities=[0.0] + priorities=[0.0 for _ in goal_state.goals] ) search_stack = [initial_state] """