# `ShotDs.Data.Problem`
[🔗](https://github.com/jcschuster/ShotDs/blob/v1.3.1/lib/shot_ds/data/problem.ex#L1)

A data structure to describe a (TPTP) proof problem.

It contains meta-information about the problem (path to proof file, included
files) as well as the problem definition which consist of:

- A map of types which maps symbols (user types or constants) to their type

- The definitions given by the user

- The axioms defined by the user

- The conjecture to be proven based on the axioms and definitions

Note that definitions are not unfolded in the proof problem but kept as
constants.

# `axiom_input`

```elixir
@type axiom_input() ::
  {String.t(), ShotDs.Data.Term.term_id()} | ShotDs.Data.Term.term_id()
```

A single axiom entry accepted by `new/1`. Either a `{name, term_id}` pair or
a bare `term_id` (in which case a name of the form `"axiom_<n>"` is generated
based on position).

# `conjecture_input`

```elixir
@type conjecture_input() ::
  {String.t(), ShotDs.Data.Term.term_id()} | ShotDs.Data.Term.term_id() | nil
```

A conjecture entry accepted by `new/1`. `nil` if no conjecture is given.
A bare `term_id` gets the default name `"conjecture"`.

# `new_opts`

```elixir
@type new_opts() :: [
  axioms: [axiom_input()],
  conjecture: conjecture_input(),
  path: String.t()
]
```

Options accepted by `new/1` and `new!/1`.

# `t`

```elixir
@type t() :: %ShotDs.Data.Problem{
  axioms: [{String.t(), ShotDs.Data.Term.term_id()}],
  conjecture: {String.t(), ShotDs.Data.Term.term_id()} | nil,
  definitions: %{
    required(ShotDs.Data.Declaration.t()) =&gt; ShotDs.Data.Term.term_id()
  },
  includes: [String.t()],
  path: String.t(),
  types: %{
    required(String.t()) =&gt;
      :base_type | ShotDs.Data.Type.t() | ShotDs.Data.TypeScheme.t()
  }
}
```

A `Problem` is a collection holding the relevant information and
meta-information of a problem stored in separate fields.

The `:path` to a problem file is given as a string. This also includes the
paths to the included files in `:includes`.

The types are given as a map mapping symbol names (or type names) to their
defined types (can be `:base_type` for user-defined base types).

The definitions are given as a map from the symbol's name to the equation
describing it. Note that the equation must first be deconstructed into the
defined constant on the left hand side and it's definition on the right hand
side.

The axioms are stored as a list of pairs containing the axiom's name as
string and term as its corresponding ID.

The conjecture is tuple containing the conjecture's name as string and the
conjecture itself as the term's ID. The field's value is `nil` if no
conjecture could be found.

# `new`

```elixir
@spec new(new_opts()) :: {:ok, t()} | {:error, String.t()}
```

Builds a `Problem` struct from a list of axioms and an optional conjecture.

Axioms may be given as `{name, term_id}` pairs or as bare `term_id`s — bare
entries are auto-named `"axiom_<n>"` based on their position (1-indexed),
which is useful when the caller comes from an intermediate proof state where
the original names have been discarded. The conjecture may be given as
`{name, term_id}`, as a bare `term_id` (named `"conjecture"`), or as `nil`.

The `types` map is populated automatically by scanning all referenced terms:

- Each **constant** occurring in an axiom or conjecture is registered under
  its name with a `ShotDs.Data.TypeScheme`. When the same constant is used at
  multiple types (rank-1 polymorphism), the monotypes are reconciled by
  least-general-generalization and the free type variables are quantified in
  the resulting scheme.
- Each **user-defined base type atom** (any goal other than `:o`, `:i`, or
  `:tType`) is registered as `:base_type`.

Free variables that occur in **only one** formula retain their embedded
types; when the problem is exported to TPTP, they are implicitly universally
quantified in that formula (per the standard THF convention).

Free variables that occur in **more than one** formula (axioms and/or
conjecture) are automatically replaced everywhere by a fresh constant of the
same type so their sharing across formulas is preserved when the problem is
exported and re-parsed. The generated constant is named
`"fv_" <> lowercased(fvar_name)` — the `fv_` prefix makes it visually
distinct from ordinary user constants — with a numeric suffix appended if
that name clashes with an existing constant.

## Options

- `:axioms` — list of `axiom_input()` entries (default `[]`)
- `:conjecture` — `conjecture_input()` (default `nil`)
- `:path` — display path for the constructed problem (default `"memory"`)

Returns `{:ok, problem}` or `{:error, reason}`.

## Examples

    iex> import ShotDs.Hol.Definitions
    iex> alias ShotDs.Stt.TermFactory, as: TF
    iex> a_id = TF.make_const_term("a", type_i())
    iex> p_id = TF.make_const_term("p", Type.new(:o, :i))
    iex> ax = ShotDs.Hol.Dsl.app(p_id, a_id)
    iex> {:ok, %ShotDs.Data.Problem{types: types}} =
    ...>   ShotDs.Data.Problem.new(axioms: [{"ax1", ax}])
    iex> Map.keys(types) |> Enum.sort()
    ["a", "p"]

    iex> import ShotDs.Hol.Definitions
    iex> alias ShotDs.Stt.TermFactory, as: TF
    iex> a_id = TF.make_const_term("a", type_i())
    iex> p_id = TF.make_const_term("p", Type.new(:o, :i))
    iex> ax = ShotDs.Hol.Dsl.app(p_id, a_id)
    iex> {:ok, problem} = ShotDs.Data.Problem.new(axioms: [ax], conjecture: ax)
    iex> Enum.map(problem.axioms, &elem(&1, 0))
    ["axiom_1"]
    iex> elem(problem.conjecture, 0)
    "conjecture"

# `new!`

```elixir
@spec new!(new_opts()) :: t()
```

Same as `new/1` but raises `ArgumentError` on failure.

---

*Consult [api-reference.md](api-reference.md) for complete listing*