Wrappers¶

Clause Embeddings Wrapper¶

class gym_saturation.wrappers.clause_embeddings_wrapper.ClauseEmbeddingsWrapper(env: SaturationEnv, embedding_dim: int)¶

A clause embeddings wrapper.

It’s incremental, i.e. it embeds only the new clauses in the observation. It defines the clauses as old if their order numbers are smaller than the previous step maximum.

>>> class ConstantClauseWeight(ClauseEmbeddingsWrapper):
...     def clause_embedder(self, clause: Dict[str, Any]) -> np.ndarray:
...         return np.ones(
...             (self.observation_space[CLAUSE_EMBEDDINGS].shape[1],)
...         )
>>> env = gym.make("Vampire-v0", max_clauses=10)
>>> wrapped_env = ConstantClauseWeight(env, embedding_dim=1)
>>> observation, info = wrapped_env.reset()
>>> observation.keys()
dict_keys(['clause_embeddings'])
>>> info.keys()
dict_keys(['clauses'])
>>> observation[CLAUSE_EMBEDDINGS]
array([[1.],
       [1.],
       [1.],
       [1.],
       [1.],
       [0.],
       [0.],
       [0.],
       [0.],
       [0.]])
>>> _ = wrapped_env.step(0)
>>> observation, _, _, _, _ = wrapped_env.step(1)
>>> observation[CLAUSE_EMBEDDINGS]
array([[1.],
       [1.],
       [1.],
       [1.],
       [1.],
       [0.],
       [0.],
       [0.],
       [0.],
       [0.]])

__init__(env: SaturationEnv, embedding_dim: int)¶: Initialise all the things.

abstract clause_embedder(literals: str) → ndarray¶

Embed the clause.

Parameters:: literals – a TPTP clause literals to embed
Returns:: an embedding vector

observation(observation: Tuple[Dict[str, Any], ...]) → Dict[str, Any]¶

Return a modified observation.

Parameters:: observation – the unwrapped observation
Returns:: the modified observation

reset(*, seed: int | None = None, options: Dict[str, Any] | None = None) → Tuple[Dict[str, Any], Dict[str, Any]]¶

Reset the environment.

Parameters:

seed – seed for compatibility
options – options for compatibility

Returns:

observations and info

ast2vec Wrapper¶

class gym_saturation.wrappers.ast2vec_wrapper.AST2VecWrapper(env, features_num: int, torch_serve_url: str = 'http://127.0.0.1:9080/predictions/ast2vec')¶

An ast2vec wrappers for saturation provers.

The best way is to run TorchServe docker container as described here: https://gitlab.com/inpefess/ast2vec

>>> import gymnasium as gym
>>> env = gym.make("Vampire-v0", max_clauses=9)
>>> wrapped_env = AST2VecWrapper(env, features_num=256)
>>> observation, info = wrapped_env.reset()
>>> observation.keys()
dict_keys(['clause_embeddings'])
>>> from gym_saturation.wrappers.clause_embeddings_wrapper import (
...     CLAUSE_EMBEDDINGS)
>>> observation[CLAUSE_EMBEDDINGS].shape
(9, 256)

__init__(env, features_num: int, torch_serve_url: str = 'http://127.0.0.1:9080/predictions/ast2vec')¶: Initialise all the things.

clause_embedder(literals: str) → ndarray¶

Embed the clause.

Parameters:: literals – a TPTP clause literals to embed
Returns:: an embedding vector

Large Language Model Wrapper¶

class gym_saturation.wrappers.llm_wrapper.LLMWrapper(env, features_num: int, api_url: str = 'http://127.0.0.1:7860/')¶

A Large Language Model wrapper for saturation provers.

An example Docker image: https://gitlab.com/inpefess/codebert-features

>>> import gymnasium as gym
>>> env = gym.make("Vampire-v0", max_clauses=9)
>>> wrapped_env = LLMWrapper(env, features_num=768)
>>> observation, info = wrapped_env.reset()
>>> observation.keys()
dict_keys(['clause_embeddings'])
>>> from gym_saturation.wrappers.clause_embeddings_wrapper import (
...     CLAUSE_EMBEDDINGS)
>>> observation[CLAUSE_EMBEDDINGS].shape
(9, 768)

__init__(env, features_num: int, api_url: str = 'http://127.0.0.1:7860/')¶: Initialise all the things.

clause_embedder(literals: str) → ndarray¶

Embed the clause.

Parameters:: literals – a TPTP clause literals to embed
Returns:: an embedding vector

MultiDiscrete-to-Discrete Wrapper¶

class gym_saturation.wrappers.md2d_wrapper.Md2DWrapper(env: Env)¶

A wrapper transforming a MultiDiscrete action space to a Discrete one.

>>> env = gym.make("Vampair-v0", max_clauses=10)
>>> wrapped_env = Md2DWrapper(env)
>>> wrapped_env.action_space
Discrete(100)
>>> _ = wrapped_env.reset()
>>> _ = wrapped_env.step(2)  # (0, 2)
>>> _, reward, _, _, _ = wrapped_env.step(35)  # (3, 5)
>>> reward
1.0

__init__(env: Env)¶: Redefine the action space.

action(action: int64) → ndarray¶

Return a modified action before step is called.

Parameters:: action – The original actions
Returns:: The modified actions

Useful Actions Wrapper¶

class gym_saturation.wrappers.useful_actions_wrapper.UsefulActionsWrapper(env: Env[ObsType, ActType])¶

A wrapper returning negative reward in observation doesn’t change.

>>> import gymnasium as gym
>>> env = gym.make("Vampair-v0", max_clauses=10)
>>> wrapped_env = UsefulActionsWrapper(env)

although it’s an action wrapper, the action method does nothing

>>> wrapped_env.action(0)
0
>>> _ = wrapped_env.reset()
>>> _, reward, _, _, _ = wrapped_env.step((0, 2))
>>> reward
0.0

repeating an action is useless and results in a negative reward

>>> _, reward, _, _, _ = wrapped_env.step((0, 2))
>>> reward
-1.0

action(action: Any) → Any¶

Return the non-modified action. Left for compatibility.

Parameters:: action – the original actions
Returns:: the non-modified actions

step(action: Any) → Tuple[Any, float, bool, bool, Dict[str, Any]]¶

Run the step and modify action.

Parameters:: action – action selected by an agent
Returns:: standard Gymnasium step results