Struct Store 

pub struct Store { /* private fields */ }

Arena of hash-consed formula nodes.

Implementations

impl Store

pub fn mk(&mut self, n: Node) -> FormulaId

Interns a node, returning an existing id when the node is already present.

pub fn node(&self, f: FormulaId) -> &Node

The node behind an id.

Panics

If f was not produced by this store.

pub fn len(&self) -> usize

How many distinct nodes are interned.

pub fn is_empty(&self) -> bool

Whether the arena is empty.

pub fn tru(&mut self) -> FormulaId

⊤

pub fn fls(&mut self) -> FormulaId

⊥

pub fn atom(&mut self, a: AtomId) -> FormulaId

An atom.

pub fn not(&mut self, f: FormulaId) -> FormulaId

!f

pub fn and(&mut self, a: FormulaId, b: FormulaId) -> FormulaId

a & b

pub fn or(&mut self, a: FormulaId, b: FormulaId) -> FormulaId

a | b, as !(!a & !b).

pub fn implies(&mut self, a: FormulaId, b: FormulaId) -> FormulaId

a -> b

pub fn all(&mut self, fs: &[FormulaId]) -> FormulaId

Conjunction of a slice; ⊤ when empty.

pub fn any(&mut self, fs: &[FormulaId]) -> FormulaId

Disjunction of a slice; ⊥ when empty.

pub fn knows(&mut self, i: AgentId, f: FormulaId) -> FormulaId

K[i] f

pub fn believes(&mut self, i: AgentId, f: FormulaId) -> FormulaId

B[i] f

pub fn safe(&mut self, i: AgentId, f: FormulaId) -> FormulaId

□[i] f

pub fn cond_bel( &mut self, i: AgentId, psi: FormulaId, phi: FormulaId, ) -> FormulaId

B^psi[i] phi

pub fn common(&mut self, g: AgentMask, f: FormulaId) -> FormulaId

C[g] f

impl Store

pub fn knows_whether(&mut self, i: AgentId, f: FormulaId) -> FormulaId

Kw[i]φ — agent knows whether φ is true: K[i]φ | K[i]!φ.

pub fn believes_whether(&mut self, i: AgentId, f: FormulaId) -> FormulaId

Bw[i]φ — agent has a belief either way: B[i]φ | B[i]!φ.

pub fn ignorant(&mut self, i: AgentId, f: FormulaId) -> FormulaId

?[i]φ — agent is ignorant whether: !K[i]φ & !K[i]!φ.

pub fn undecided(&mut self, i: AgentId, f: FormulaId) -> FormulaId

¿[i]φ — agent suspends judgement: !B[i]φ & !B[i]!φ.

pub fn considers_possible(&mut self, i: AgentId, f: FormulaId) -> FormulaId

K'[i]φ — agent considers φ possible: !K[i]!φ.

pub fn not_ruled_out(&mut self, i: AgentId, f: FormulaId) -> FormulaId

B'[i]φ — agent has not ruled out φ: !B[i]!φ.

pub fn safe_dual(&mut self, i: AgentId, f: FormulaId) -> FormulaId

S'[i]φ — φ is safe for agent to act on: !□[i]!φ.

pub fn knows_all(&mut self, agents: &[AgentId], f: FormulaId) -> FormulaId

K[a,b,…]φ — all agents in the list know φ.

pub fn believes_all(&mut self, agents: &[AgentId], f: FormulaId) -> FormulaId

B[a,b,…]φ — all agents in the list believe φ.

Trait Implementations

impl Clone for Store

fn clone(&self) -> Store

Returns a duplicate of the value.

fn clone_from(&mut self, source: &Self)

Performs copy-assignment from source.

impl Debug for Store

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

Formats the value using the given formatter.

impl Default for Store

fn default() -> Store

Returns the “default value” for a type.