Struct Problem 

pub struct Problem {
    pub store: Store,
    pub sig: Sig,
    pub consts: Constants,
    pub defs: Defs,
    pub state: State,
    pub goal: Option<FormulaId>,
    pub invariants: Vec<(FormulaId, String)>,
    pub actions: Vec<GroundAction>,
}

A fully checked problem: signature, initial state, goal, and ground actions.

Debug is derived because Problem::parse returns it in a Result, and Result::unwrap_err requires the success type to be printable.

Fields

store: Store

Formula arena shared by everything below.

sig: Sig

The checked signature.

consts: Constants

The constant table, kept so later queries lower against the same one.

defs: Defs

The definition table, kept for the same reason: a name that works in the file must work at the prompt, and a query is lowered after the file has been checked.

state: State

The initial state.

goal: Option<FormulaId>

The declared goal, if the file had one.

invariants: Vec<(FormulaId, String)>

Declared invariants, each with the source text that wrote it.

The text is kept so a violation can name the constraint as the author wrote it rather than as a formula id or a re-rendering.

actions: Vec<GroundAction>

Every ground action whose precondition is satisfiable.

Implementations

impl Problem

pub fn parse(src: &str) -> Result<Problem, String>

Parses and checks a source file.

On failure returns every diagnostic rendered against the source, so one call reports all the problems rather than only the first. A construction that produced a state but also raised a diagnostic is a failure too: the state is only as trustworthy as the checks that passed alongside it.

pub fn check(src: &str) -> (Option<Problem>, Diagnostics)

Parses and checks, returning the diagnostics rather than a rendering of them.

A caller that wants to act on a fault — jump a cursor to it, underline it — needs the spans, which parse’s rendered string has already thrown away. The problem comes back even when diagnostics were raised, so a UI can report the errors and still show whatever was successfully built.

pub fn action(&self, name: &str) -> Option<&GroundAction>

A ground action by its display name, e.g. move(alice,hall,study). A zero-parameter action keeps its empty argument list, so peek_c is peek_c().

pub fn entails(&self, f: FormulaId) -> bool

Whether the initial state models f.

Precondition: f was produced by this problem’s Problem::store.

pub fn violated(&self, state: &State) -> Vec<&str>

The declared invariants that state violates, as the author wrote them.

Takes the state rather than using self.state, because the point of an invariant is that it is checked after every action — a version that could only inspect the initial state would be a slower way of writing an initially entry.

Trait Implementations

impl Debug for Problem

fn fmt(&self, f: &mut Formatter<'_>) -> Result

Formats the value using the given formatter.