Skip to content

observation_to_source throws error if the observation is already proved #14

@fzyzcjy

Description

@fzyzcjy

e.g.

Traceback (most recent call last):
  File "/home/jychen/.conda/envs/jychen_main/lib/python3.10/site-packages/IPython/core/interactiveshell.py", line 3433, in run_code
    exec(code_obj, self.user_global_ns, self.user_ns)
  File "/tmp/ipykernel_21573/176925322.py", line 1, in <module>
    evaluate.interact_with_prover_sequentially(
  File "/data/jychen/research/code/research_mono/neural_theorem_prover/evaluate.py", line 186, in interact_with_prover_sequentially
    print('obs_after_action', prover.get_observation_string())
  File "/data/jychen/research/code/research_mono/neural_theorem_prover/wrapped_prover.py", line 25, in get_observation_string
    return self.inner.parser.observation_to_source(self.inner.get_observation())
  File "/data/jychen/research/code/third_party/INT/int_environment/proof_system/graph_seq_conversion.py", line 101, in observation_to_source
    source = source + logic_statement_to_seq_string(observation["objectives"][0])
IndexError: list index out of range

Metadata

Metadata

Assignees

No one assigned

    Labels

    No labels
    No labels

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions