Skip to content

module lash

solverpy.solver.atp.lash

Lash

Bases: ShellSolver

The lash higher-order automated theorem prover.

The strategy (sid) supplies Lash's command-line options, appended after the static option -p tstp (TSTP output). Output is parsed for Steps and Mode by process. Status is decided by the Tptp plugin from the TSTP SZS status line.

Source code in packages/solverpy/src/solverpy/solver/atp/lash.py 
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
class Lash(ShellSolver):
   """
   The `lash` higher-order automated theorem prover.

   The strategy (sid) supplies Lash's command-line options, appended after
   the static option `-p tstp` (TSTP output). Output is parsed for `Steps`
   and `Mode` by
   [`process`][solverpy.solver.atp.lash.Lash.process]. Status is decided by
   the [`Tptp`][solverpy.solver.plugins.status.tptp.Tptp] plugin from the
   TSTP `SZS status` line.
   """

   _binary = L_BINARY

   def __init__(
      self,
      limit: str,
      binary: str = L_BINARY,
      static: str = L_STATIC,
      complete: bool = True,
      plugins: list["Plugin"] = [],
   ):
      cmd = f"{binary} {static}"
      plugins = plugins + [
         Time(),
         Tptp(complete=complete),
      ]
      ShellSolver.__init__(
         self,
         cmd,
         limit,
         L_BUILDER,
         plugins,
         0,
         complete,
         binary=binary,
      )

   def process(self, output: str) -> "Result":
      """Parse Lash's `Steps`/`Mode` output lines into a result dict."""
      result = patterns.keyval(L_PAT, output, L_TABLE)
      result = patterns.mapval(result, human.numeric)
      return result

process(output: str) -> Result

Parse Lash's Steps/Mode output lines into a result dict.

Source code in packages/solverpy/src/solverpy/solver/atp/lash.py 
66
67
68
69
70
def process(self, output: str) -> "Result":
   """Parse Lash's `Steps`/`Mode` output lines into a result dict."""
   result = patterns.keyval(L_PAT, output, L_TABLE)
   result = patterns.mapval(result, human.numeric)
   return result