Struct eqlog_eqlog::Eqlog

pub struct Eqlog { /* private fields */ }

A model of the Eqlog theory.

Implementations

impl Eqlog

pub fn new() -> Self

Creates an empty model.

pub fn close(&mut self)

Closes the model under all axioms. Depending on the axioms and the model, this may run indefinitely.

pub fn close_until(&mut self, condition: impl Fn(&Self) -> bool) -> bool

Closes the model under all axioms until condition is satisfied. Depending on the axioms and condition, this may run indefinitely. Returns true if the condition eventually holds. Returns false if the model could be closed under all axioms but condition still does not hold.

pub fn new_ident(&mut self) -> Ident

Adjoins a new element of sort Ident.

pub fn equate_ident(&mut self, lhs: Ident, rhs: Ident)

Enforces the equality lhs = rhs.

pub fn iter_ident(&self) -> impl '_ + Iterator<Item = Ident>

Returns and iterator over elements of sort Ident. The iterator yields canonical representatives only.

pub fn root_ident(&self, el: Ident) -> Ident

Returns the canonical representative of the equivalence class of el.

pub fn are_equal_ident(&self, lhs: Ident, rhs: Ident) -> bool

Returns true if lhs and rhs are in the same equivalence class.

pub fn new_virt_ident(&mut self) -> VirtIdent

Adjoins a new element of sort VirtIdent.

pub fn equate_virt_ident(&mut self, lhs: VirtIdent, rhs: VirtIdent)

Enforces the equality lhs = rhs.

pub fn iter_virt_ident(&self) -> impl '_ + Iterator<Item = VirtIdent>

Returns and iterator over elements of sort VirtIdent. The iterator yields canonical representatives only.

pub fn root_virt_ident(&self, el: VirtIdent) -> VirtIdent

Returns the canonical representative of the equivalence class of el.

pub fn are_equal_virt_ident(&self, lhs: VirtIdent, rhs: VirtIdent) -> bool

Returns true if lhs and rhs are in the same equivalence class.

pub fn new_type_decl_node(&mut self) -> TypeDeclNode

Adjoins a new element of sort TypeDeclNode.

pub fn equate_type_decl_node(&mut self, lhs: TypeDeclNode, rhs: TypeDeclNode)

Enforces the equality lhs = rhs.

pub fn iter_type_decl_node(&self) -> impl '_ + Iterator<Item = TypeDeclNode>

Returns and iterator over elements of sort TypeDeclNode. The iterator yields canonical representatives only.

pub fn root_type_decl_node(&self, el: TypeDeclNode) -> TypeDeclNode

Returns the canonical representative of the equivalence class of el.

pub fn are_equal_type_decl_node( &self, lhs: TypeDeclNode, rhs: TypeDeclNode ) -> bool

Returns true if lhs and rhs are in the same equivalence class.

pub fn new_arg_decl_node(&mut self) -> ArgDeclNode

Adjoins a new element of sort ArgDeclNode.

pub fn equate_arg_decl_node(&mut self, lhs: ArgDeclNode, rhs: ArgDeclNode)

Enforces the equality lhs = rhs.

pub fn iter_arg_decl_node(&self) -> impl '_ + Iterator<Item = ArgDeclNode>

Returns and iterator over elements of sort ArgDeclNode. The iterator yields canonical representatives only.

pub fn root_arg_decl_node(&self, el: ArgDeclNode) -> ArgDeclNode

Returns the canonical representative of the equivalence class of el.

pub fn are_equal_arg_decl_node( &self, lhs: ArgDeclNode, rhs: ArgDeclNode ) -> bool

Returns true if lhs and rhs are in the same equivalence class.

pub fn new_arg_decl_list_node(&mut self) -> ArgDeclListNode

Adjoins a new element of sort ArgDeclListNode.

pub fn equate_arg_decl_list_node( &mut self, lhs: ArgDeclListNode, rhs: ArgDeclListNode )

Enforces the equality lhs = rhs.

pub fn iter_arg_decl_list_node( &self ) -> impl '_ + Iterator<Item = ArgDeclListNode>

Returns and iterator over elements of sort ArgDeclListNode. The iterator yields canonical representatives only.

pub fn root_arg_decl_list_node(&self, el: ArgDeclListNode) -> ArgDeclListNode

Returns the canonical representative of the equivalence class of el.

pub fn are_equal_arg_decl_list_node( &self, lhs: ArgDeclListNode, rhs: ArgDeclListNode ) -> bool

Returns true if lhs and rhs are in the same equivalence class.

pub fn new_pred_decl_node(&mut self) -> PredDeclNode

Adjoins a new element of sort PredDeclNode.

pub fn equate_pred_decl_node(&mut self, lhs: PredDeclNode, rhs: PredDeclNode)

Enforces the equality lhs = rhs.

pub fn iter_pred_decl_node(&self) -> impl '_ + Iterator<Item = PredDeclNode>

Returns and iterator over elements of sort PredDeclNode. The iterator yields canonical representatives only.

pub fn root_pred_decl_node(&self, el: PredDeclNode) -> PredDeclNode

Returns the canonical representative of the equivalence class of el.

pub fn are_equal_pred_decl_node( &self, lhs: PredDeclNode, rhs: PredDeclNode ) -> bool

Returns true if lhs and rhs are in the same equivalence class.

pub fn new_func_decl_node(&mut self) -> FuncDeclNode

Adjoins a new element of sort FuncDeclNode.

pub fn equate_func_decl_node(&mut self, lhs: FuncDeclNode, rhs: FuncDeclNode)

Enforces the equality lhs = rhs.

pub fn iter_func_decl_node(&self) -> impl '_ + Iterator<Item = FuncDeclNode>

Returns and iterator over elements of sort FuncDeclNode. The iterator yields canonical representatives only.

pub fn root_func_decl_node(&self, el: FuncDeclNode) -> FuncDeclNode

Returns the canonical representative of the equivalence class of el.

pub fn are_equal_func_decl_node( &self, lhs: FuncDeclNode, rhs: FuncDeclNode ) -> bool

Returns true if lhs and rhs are in the same equivalence class.

pub fn new_term_node(&mut self) -> TermNode

Adjoins a new element of sort TermNode.

pub fn equate_term_node(&mut self, lhs: TermNode, rhs: TermNode)

Enforces the equality lhs = rhs.

pub fn iter_term_node(&self) -> impl '_ + Iterator<Item = TermNode>

Returns and iterator over elements of sort TermNode. The iterator yields canonical representatives only.

pub fn root_term_node(&self, el: TermNode) -> TermNode

Returns the canonical representative of the equivalence class of el.

pub fn are_equal_term_node(&self, lhs: TermNode, rhs: TermNode) -> bool

Returns true if lhs and rhs are in the same equivalence class.

pub fn new_term_list_node(&mut self) -> TermListNode

Adjoins a new element of sort TermListNode.

pub fn equate_term_list_node(&mut self, lhs: TermListNode, rhs: TermListNode)

Enforces the equality lhs = rhs.

pub fn iter_term_list_node(&self) -> impl '_ + Iterator<Item = TermListNode>

Returns and iterator over elements of sort TermListNode. The iterator yields canonical representatives only.

pub fn root_term_list_node(&self, el: TermListNode) -> TermListNode

Returns the canonical representative of the equivalence class of el.

pub fn are_equal_term_list_node( &self, lhs: TermListNode, rhs: TermListNode ) -> bool

Returns true if lhs and rhs are in the same equivalence class.

pub fn new_opt_term_node(&mut self) -> OptTermNode

Adjoins a new element of sort OptTermNode.

pub fn equate_opt_term_node(&mut self, lhs: OptTermNode, rhs: OptTermNode)

Enforces the equality lhs = rhs.

pub fn iter_opt_term_node(&self) -> impl '_ + Iterator<Item = OptTermNode>

Returns and iterator over elements of sort OptTermNode. The iterator yields canonical representatives only.

pub fn root_opt_term_node(&self, el: OptTermNode) -> OptTermNode

Returns the canonical representative of the equivalence class of el.

pub fn are_equal_opt_term_node( &self, lhs: OptTermNode, rhs: OptTermNode ) -> bool

Returns true if lhs and rhs are in the same equivalence class.

pub fn new_if_atom_node(&mut self) -> IfAtomNode

Adjoins a new element of sort IfAtomNode.

pub fn equate_if_atom_node(&mut self, lhs: IfAtomNode, rhs: IfAtomNode)

Enforces the equality lhs = rhs.

pub fn iter_if_atom_node(&self) -> impl '_ + Iterator<Item = IfAtomNode>

Returns and iterator over elements of sort IfAtomNode. The iterator yields canonical representatives only.

pub fn root_if_atom_node(&self, el: IfAtomNode) -> IfAtomNode

Returns the canonical representative of the equivalence class of el.

pub fn are_equal_if_atom_node(&self, lhs: IfAtomNode, rhs: IfAtomNode) -> bool

Returns true if lhs and rhs are in the same equivalence class.

pub fn new_then_atom_node(&mut self) -> ThenAtomNode

Adjoins a new element of sort ThenAtomNode.

pub fn equate_then_atom_node(&mut self, lhs: ThenAtomNode, rhs: ThenAtomNode)

Enforces the equality lhs = rhs.

pub fn iter_then_atom_node(&self) -> impl '_ + Iterator<Item = ThenAtomNode>

Returns and iterator over elements of sort ThenAtomNode. The iterator yields canonical representatives only.

pub fn root_then_atom_node(&self, el: ThenAtomNode) -> ThenAtomNode

Returns the canonical representative of the equivalence class of el.

pub fn are_equal_then_atom_node( &self, lhs: ThenAtomNode, rhs: ThenAtomNode ) -> bool

Returns true if lhs and rhs are in the same equivalence class.

pub fn new_stmt_node(&mut self) -> StmtNode

Adjoins a new element of sort StmtNode.

pub fn equate_stmt_node(&mut self, lhs: StmtNode, rhs: StmtNode)

Enforces the equality lhs = rhs.

pub fn iter_stmt_node(&self) -> impl '_ + Iterator<Item = StmtNode>

Returns and iterator over elements of sort StmtNode. The iterator yields canonical representatives only.

pub fn root_stmt_node(&self, el: StmtNode) -> StmtNode

Returns the canonical representative of the equivalence class of el.

pub fn are_equal_stmt_node(&self, lhs: StmtNode, rhs: StmtNode) -> bool

Returns true if lhs and rhs are in the same equivalence class.

pub fn new_stmt_list_node(&mut self) -> StmtListNode

Adjoins a new element of sort StmtListNode.

pub fn equate_stmt_list_node(&mut self, lhs: StmtListNode, rhs: StmtListNode)

Enforces the equality lhs = rhs.

pub fn iter_stmt_list_node(&self) -> impl '_ + Iterator<Item = StmtListNode>

Returns and iterator over elements of sort StmtListNode. The iterator yields canonical representatives only.

pub fn root_stmt_list_node(&self, el: StmtListNode) -> StmtListNode

Returns the canonical representative of the equivalence class of el.

pub fn are_equal_stmt_list_node( &self, lhs: StmtListNode, rhs: StmtListNode ) -> bool

Returns true if lhs and rhs are in the same equivalence class.

pub fn new_rule_decl_node(&mut self) -> RuleDeclNode

Adjoins a new element of sort RuleDeclNode.

pub fn equate_rule_decl_node(&mut self, lhs: RuleDeclNode, rhs: RuleDeclNode)

Enforces the equality lhs = rhs.

pub fn iter_rule_decl_node(&self) -> impl '_ + Iterator<Item = RuleDeclNode>

Returns and iterator over elements of sort RuleDeclNode. The iterator yields canonical representatives only.

pub fn root_rule_decl_node(&self, el: RuleDeclNode) -> RuleDeclNode

Returns the canonical representative of the equivalence class of el.

pub fn are_equal_rule_decl_node( &self, lhs: RuleDeclNode, rhs: RuleDeclNode ) -> bool

Returns true if lhs and rhs are in the same equivalence class.

pub fn new_decl_node(&mut self) -> DeclNode

Adjoins a new element of sort DeclNode.

pub fn equate_decl_node(&mut self, lhs: DeclNode, rhs: DeclNode)

Enforces the equality lhs = rhs.

pub fn iter_decl_node(&self) -> impl '_ + Iterator<Item = DeclNode>

Returns and iterator over elements of sort DeclNode. The iterator yields canonical representatives only.

pub fn root_decl_node(&self, el: DeclNode) -> DeclNode

Returns the canonical representative of the equivalence class of el.

pub fn are_equal_decl_node(&self, lhs: DeclNode, rhs: DeclNode) -> bool

Returns true if lhs and rhs are in the same equivalence class.

pub fn new_decl_list_node(&mut self) -> DeclListNode

Adjoins a new element of sort DeclListNode.

pub fn equate_decl_list_node(&mut self, lhs: DeclListNode, rhs: DeclListNode)

Enforces the equality lhs = rhs.

pub fn iter_decl_list_node(&self) -> impl '_ + Iterator<Item = DeclListNode>

Returns and iterator over elements of sort DeclListNode. The iterator yields canonical representatives only.

pub fn root_decl_list_node(&self, el: DeclListNode) -> DeclListNode

Returns the canonical representative of the equivalence class of el.

pub fn are_equal_decl_list_node( &self, lhs: DeclListNode, rhs: DeclListNode ) -> bool

Returns true if lhs and rhs are in the same equivalence class.

pub fn new_module_node(&mut self) -> ModuleNode

Adjoins a new element of sort ModuleNode.

pub fn equate_module_node(&mut self, lhs: ModuleNode, rhs: ModuleNode)

Enforces the equality lhs = rhs.

pub fn iter_module_node(&self) -> impl '_ + Iterator<Item = ModuleNode>

Returns and iterator over elements of sort ModuleNode. The iterator yields canonical representatives only.

pub fn root_module_node(&self, el: ModuleNode) -> ModuleNode

Returns the canonical representative of the equivalence class of el.

pub fn are_equal_module_node(&self, lhs: ModuleNode, rhs: ModuleNode) -> bool

Returns true if lhs and rhs are in the same equivalence class.

pub fn new_loc(&mut self) -> Loc

Adjoins a new element of sort Loc.

pub fn equate_loc(&mut self, lhs: Loc, rhs: Loc)

Enforces the equality lhs = rhs.

pub fn iter_loc(&self) -> impl '_ + Iterator<Item = Loc>

Returns and iterator over elements of sort Loc. The iterator yields canonical representatives only.

pub fn root_loc(&self, el: Loc) -> Loc

Returns the canonical representative of the equivalence class of el.

pub fn are_equal_loc(&self, lhs: Loc, rhs: Loc) -> bool

Returns true if lhs and rhs are in the same equivalence class.

pub fn new_rule_child_node(&mut self) -> RuleChildNode

Adjoins a new element of sort RuleChildNode.

pub fn equate_rule_child_node(&mut self, lhs: RuleChildNode, rhs: RuleChildNode)

Enforces the equality lhs = rhs.

pub fn iter_rule_child_node(&self) -> impl '_ + Iterator<Item = RuleChildNode>

Returns and iterator over elements of sort RuleChildNode. The iterator yields canonical representatives only.

pub fn root_rule_child_node(&self, el: RuleChildNode) -> RuleChildNode

Returns the canonical representative of the equivalence class of el.

pub fn are_equal_rule_child_node( &self, lhs: RuleChildNode, rhs: RuleChildNode ) -> bool

Returns true if lhs and rhs are in the same equivalence class.

pub fn new_type(&mut self) -> Type

Adjoins a new element of sort Type.

pub fn equate_type(&mut self, lhs: Type, rhs: Type)

Enforces the equality lhs = rhs.

pub fn iter_type(&self) -> impl '_ + Iterator<Item = Type>

Returns and iterator over elements of sort Type. The iterator yields canonical representatives only.

pub fn root_type(&self, el: Type) -> Type

Returns the canonical representative of the equivalence class of el.

pub fn are_equal_type(&self, lhs: Type, rhs: Type) -> bool

Returns true if lhs and rhs are in the same equivalence class.

pub fn new_type_list(&mut self) -> TypeList

Adjoins a new element of sort TypeList.

pub fn equate_type_list(&mut self, lhs: TypeList, rhs: TypeList)

Enforces the equality lhs = rhs.

pub fn iter_type_list(&self) -> impl '_ + Iterator<Item = TypeList>

Returns and iterator over elements of sort TypeList. The iterator yields canonical representatives only.

pub fn root_type_list(&self, el: TypeList) -> TypeList

Returns the canonical representative of the equivalence class of el.

pub fn are_equal_type_list(&self, lhs: TypeList, rhs: TypeList) -> bool

Returns true if lhs and rhs are in the same equivalence class.

pub fn new_pred(&mut self) -> Pred

Adjoins a new element of sort Pred.

pub fn equate_pred(&mut self, lhs: Pred, rhs: Pred)

Enforces the equality lhs = rhs.

pub fn iter_pred(&self) -> impl '_ + Iterator<Item = Pred>

Returns and iterator over elements of sort Pred. The iterator yields canonical representatives only.

pub fn root_pred(&self, el: Pred) -> Pred

Returns the canonical representative of the equivalence class of el.

pub fn are_equal_pred(&self, lhs: Pred, rhs: Pred) -> bool

Returns true if lhs and rhs are in the same equivalence class.

pub fn new_func(&mut self) -> Func

Adjoins a new element of sort Func.

pub fn equate_func(&mut self, lhs: Func, rhs: Func)

Enforces the equality lhs = rhs.

pub fn iter_func(&self) -> impl '_ + Iterator<Item = Func>

Returns and iterator over elements of sort Func. The iterator yields canonical representatives only.

pub fn root_func(&self, el: Func) -> Func

Returns the canonical representative of the equivalence class of el.

pub fn are_equal_func(&self, lhs: Func, rhs: Func) -> bool

Returns true if lhs and rhs are in the same equivalence class.

pub fn new_structure(&mut self) -> Structure

Adjoins a new element of sort Structure.

pub fn equate_structure(&mut self, lhs: Structure, rhs: Structure)

Enforces the equality lhs = rhs.

pub fn iter_structure(&self) -> impl '_ + Iterator<Item = Structure>

Returns and iterator over elements of sort Structure. The iterator yields canonical representatives only.

pub fn root_structure(&self, el: Structure) -> Structure

Returns the canonical representative of the equivalence class of el.

pub fn are_equal_structure(&self, lhs: Structure, rhs: Structure) -> bool

Returns true if lhs and rhs are in the same equivalence class.

pub fn new_el(&mut self) -> El

Adjoins a new element of sort El.

pub fn equate_el(&mut self, lhs: El, rhs: El)

Enforces the equality lhs = rhs.

pub fn iter_el(&self) -> impl '_ + Iterator<Item = El>

Returns and iterator over elements of sort El. The iterator yields canonical representatives only.

pub fn root_el(&self, el: El) -> El

Returns the canonical representative of the equivalence class of el.

pub fn are_equal_el(&self, lhs: El, rhs: El) -> bool

Returns true if lhs and rhs are in the same equivalence class.

pub fn new_el_list(&mut self) -> ElList

Adjoins a new element of sort ElList.

pub fn equate_el_list(&mut self, lhs: ElList, rhs: ElList)

Enforces the equality lhs = rhs.

pub fn iter_el_list(&self) -> impl '_ + Iterator<Item = ElList>

Returns and iterator over elements of sort ElList. The iterator yields canonical representatives only.

pub fn root_el_list(&self, el: ElList) -> ElList

Returns the canonical representative of the equivalence class of el.

pub fn are_equal_el_list(&self, lhs: ElList, rhs: ElList) -> bool

Returns true if lhs and rhs are in the same equivalence class.

pub fn new_morphism(&mut self) -> Morphism

Adjoins a new element of sort Morphism.

pub fn equate_morphism(&mut self, lhs: Morphism, rhs: Morphism)

Enforces the equality lhs = rhs.

pub fn iter_morphism(&self) -> impl '_ + Iterator<Item = Morphism>

Returns and iterator over elements of sort Morphism. The iterator yields canonical representatives only.

pub fn root_morphism(&self, el: Morphism) -> Morphism

Returns the canonical representative of the equivalence class of el.

pub fn are_equal_morphism(&self, lhs: Morphism, rhs: Morphism) -> bool

Returns true if lhs and rhs are in the same equivalence class.

pub fn new_chain(&mut self) -> Chain

Adjoins a new element of sort Chain.

pub fn equate_chain(&mut self, lhs: Chain, rhs: Chain)

Enforces the equality lhs = rhs.

pub fn iter_chain(&self) -> impl '_ + Iterator<Item = Chain>

Returns and iterator over elements of sort Chain. The iterator yields canonical representatives only.

pub fn root_chain(&self, el: Chain) -> Chain

Returns the canonical representative of the equivalence class of el.

pub fn are_equal_chain(&self, lhs: Chain, rhs: Chain) -> bool

Returns true if lhs and rhs are in the same equivalence class.

pub fn new_symbol_kind(&mut self) -> SymbolKind

Adjoins a new element of sort SymbolKind.

pub fn equate_symbol_kind(&mut self, lhs: SymbolKind, rhs: SymbolKind)

Enforces the equality lhs = rhs.

pub fn iter_symbol_kind(&self) -> impl '_ + Iterator<Item = SymbolKind>

Returns and iterator over elements of sort SymbolKind. The iterator yields canonical representatives only.

pub fn root_symbol_kind(&self, el: SymbolKind) -> SymbolKind

Returns the canonical representative of the equivalence class of el.

pub fn are_equal_symbol_kind(&self, lhs: SymbolKind, rhs: SymbolKind) -> bool

Returns true if lhs and rhs are in the same equivalence class.

pub fn new_nat(&mut self) -> Nat

Adjoins a new element of sort Nat.

pub fn equate_nat(&mut self, lhs: Nat, rhs: Nat)

Enforces the equality lhs = rhs.

pub fn iter_nat(&self) -> impl '_ + Iterator<Item = Nat>

Returns and iterator over elements of sort Nat. The iterator yields canonical representatives only.

pub fn root_nat(&self, el: Nat) -> Nat

Returns the canonical representative of the equivalence class of el.

pub fn are_equal_nat(&self, lhs: Nat, rhs: Nat) -> bool

Returns true if lhs and rhs are in the same equivalence class.

pub fn real_virt_ident(&self, arg0: Ident) -> Option<VirtIdent>

Evaluates real_virt_ident(arg0).

pub fn define_real_virt_ident(&mut self, arg0: Ident) -> VirtIdent

Enforces that real_virt_ident(arg0) is defined, adjoining a new element if necessary.

pub fn iter_real_virt_ident( &self ) -> impl '_ + Iterator<Item = (Ident, VirtIdent)>

Returns an iterator over tuples in the graph of the real_virt_ident function. The relation yielded by the iterator need not be functional if the model is not closed.

pub fn insert_real_virt_ident(&mut self, arg0: Ident, result: VirtIdent)

Makes the equation real_virt_ident(arg0) = result hold.

pub fn rule_name(&self, arg0: RuleDeclNode) -> Option<Ident>

Evaluates rule_name(arg0).

pub fn define_rule_name(&mut self, arg0: RuleDeclNode) -> Ident

Enforces that rule_name(arg0) is defined, adjoining a new element if necessary.

pub fn iter_rule_name(&self) -> impl '_ + Iterator<Item = (RuleDeclNode, Ident)>

Returns an iterator over tuples in the graph of the rule_name function. The relation yielded by the iterator need not be functional if the model is not closed.

pub fn insert_rule_name(&mut self, arg0: RuleDeclNode, result: Ident)

Makes the equation rule_name(arg0) = result hold.

pub fn type_decl_node_loc(&self, arg0: TypeDeclNode) -> Option<Loc>

Evaluates type_decl_node_loc(arg0).

pub fn define_type_decl_node_loc(&mut self, arg0: TypeDeclNode) -> Loc

Enforces that type_decl_node_loc(arg0) is defined, adjoining a new element if necessary.

pub fn iter_type_decl_node_loc( &self ) -> impl '_ + Iterator<Item = (TypeDeclNode, Loc)>

Returns an iterator over tuples in the graph of the type_decl_node_loc function. The relation yielded by the iterator need not be functional if the model is not closed.

pub fn insert_type_decl_node_loc(&mut self, arg0: TypeDeclNode, result: Loc)

Makes the equation type_decl_node_loc(arg0) = result hold.

pub fn arg_decl_node_loc(&self, arg0: ArgDeclNode) -> Option<Loc>

Evaluates arg_decl_node_loc(arg0).

pub fn define_arg_decl_node_loc(&mut self, arg0: ArgDeclNode) -> Loc

Enforces that arg_decl_node_loc(arg0) is defined, adjoining a new element if necessary.

pub fn iter_arg_decl_node_loc( &self ) -> impl '_ + Iterator<Item = (ArgDeclNode, Loc)>

Returns an iterator over tuples in the graph of the arg_decl_node_loc function. The relation yielded by the iterator need not be functional if the model is not closed.

pub fn insert_arg_decl_node_loc(&mut self, arg0: ArgDeclNode, result: Loc)

Makes the equation arg_decl_node_loc(arg0) = result hold.

pub fn arg_decl_list_node_loc(&self, arg0: ArgDeclListNode) -> Option<Loc>

Evaluates arg_decl_list_node_loc(arg0).

pub fn define_arg_decl_list_node_loc(&mut self, arg0: ArgDeclListNode) -> Loc

Enforces that arg_decl_list_node_loc(arg0) is defined, adjoining a new element if necessary.

pub fn iter_arg_decl_list_node_loc( &self ) -> impl '_ + Iterator<Item = (ArgDeclListNode, Loc)>

Returns an iterator over tuples in the graph of the arg_decl_list_node_loc function. The relation yielded by the iterator need not be functional if the model is not closed.

pub fn insert_arg_decl_list_node_loc( &mut self, arg0: ArgDeclListNode, result: Loc )

Makes the equation arg_decl_list_node_loc(arg0) = result hold.

pub fn pred_decl_node_loc(&self, arg0: PredDeclNode) -> Option<Loc>

Evaluates pred_decl_node_loc(arg0).

pub fn define_pred_decl_node_loc(&mut self, arg0: PredDeclNode) -> Loc

Enforces that pred_decl_node_loc(arg0) is defined, adjoining a new element if necessary.

pub fn iter_pred_decl_node_loc( &self ) -> impl '_ + Iterator<Item = (PredDeclNode, Loc)>

Returns an iterator over tuples in the graph of the pred_decl_node_loc function. The relation yielded by the iterator need not be functional if the model is not closed.

pub fn insert_pred_decl_node_loc(&mut self, arg0: PredDeclNode, result: Loc)

Makes the equation pred_decl_node_loc(arg0) = result hold.

pub fn func_decl_node_loc(&self, arg0: FuncDeclNode) -> Option<Loc>

Evaluates func_decl_node_loc(arg0).

pub fn define_func_decl_node_loc(&mut self, arg0: FuncDeclNode) -> Loc

Enforces that func_decl_node_loc(arg0) is defined, adjoining a new element if necessary.

pub fn iter_func_decl_node_loc( &self ) -> impl '_ + Iterator<Item = (FuncDeclNode, Loc)>

Returns an iterator over tuples in the graph of the func_decl_node_loc function. The relation yielded by the iterator need not be functional if the model is not closed.

pub fn insert_func_decl_node_loc(&mut self, arg0: FuncDeclNode, result: Loc)

Makes the equation func_decl_node_loc(arg0) = result hold.

pub fn term_node_loc(&self, arg0: TermNode) -> Option<Loc>

Evaluates term_node_loc(arg0).

pub fn define_term_node_loc(&mut self, arg0: TermNode) -> Loc

Enforces that term_node_loc(arg0) is defined, adjoining a new element if necessary.

pub fn iter_term_node_loc(&self) -> impl '_ + Iterator<Item = (TermNode, Loc)>

Returns an iterator over tuples in the graph of the term_node_loc function. The relation yielded by the iterator need not be functional if the model is not closed.

pub fn insert_term_node_loc(&mut self, arg0: TermNode, result: Loc)

Makes the equation term_node_loc(arg0) = result hold.

pub fn term_list_node_loc(&self, arg0: TermListNode) -> Option<Loc>

Evaluates term_list_node_loc(arg0).

pub fn define_term_list_node_loc(&mut self, arg0: TermListNode) -> Loc

Enforces that term_list_node_loc(arg0) is defined, adjoining a new element if necessary.

pub fn iter_term_list_node_loc( &self ) -> impl '_ + Iterator<Item = (TermListNode, Loc)>

Returns an iterator over tuples in the graph of the term_list_node_loc function. The relation yielded by the iterator need not be functional if the model is not closed.

pub fn insert_term_list_node_loc(&mut self, arg0: TermListNode, result: Loc)

Makes the equation term_list_node_loc(arg0) = result hold.

pub fn opt_term_node_loc(&self, arg0: OptTermNode) -> Option<Loc>

Evaluates opt_term_node_loc(arg0).

pub fn define_opt_term_node_loc(&mut self, arg0: OptTermNode) -> Loc

Enforces that opt_term_node_loc(arg0) is defined, adjoining a new element if necessary.

pub fn iter_opt_term_node_loc( &self ) -> impl '_ + Iterator<Item = (OptTermNode, Loc)>

Returns an iterator over tuples in the graph of the opt_term_node_loc function. The relation yielded by the iterator need not be functional if the model is not closed.

pub fn insert_opt_term_node_loc(&mut self, arg0: OptTermNode, result: Loc)

Makes the equation opt_term_node_loc(arg0) = result hold.

pub fn if_atom_node_loc(&self, arg0: IfAtomNode) -> Option<Loc>

Evaluates if_atom_node_loc(arg0).

pub fn define_if_atom_node_loc(&mut self, arg0: IfAtomNode) -> Loc

Enforces that if_atom_node_loc(arg0) is defined, adjoining a new element if necessary.

pub fn iter_if_atom_node_loc( &self ) -> impl '_ + Iterator<Item = (IfAtomNode, Loc)>

Returns an iterator over tuples in the graph of the if_atom_node_loc function. The relation yielded by the iterator need not be functional if the model is not closed.

pub fn insert_if_atom_node_loc(&mut self, arg0: IfAtomNode, result: Loc)

Makes the equation if_atom_node_loc(arg0) = result hold.

pub fn then_atom_node_loc(&self, arg0: ThenAtomNode) -> Option<Loc>

Evaluates then_atom_node_loc(arg0).

pub fn define_then_atom_node_loc(&mut self, arg0: ThenAtomNode) -> Loc

Enforces that then_atom_node_loc(arg0) is defined, adjoining a new element if necessary.

pub fn iter_then_atom_node_loc( &self ) -> impl '_ + Iterator<Item = (ThenAtomNode, Loc)>

Returns an iterator over tuples in the graph of the then_atom_node_loc function. The relation yielded by the iterator need not be functional if the model is not closed.

pub fn insert_then_atom_node_loc(&mut self, arg0: ThenAtomNode, result: Loc)

Makes the equation then_atom_node_loc(arg0) = result hold.

pub fn stmt_node_loc(&self, arg0: StmtNode) -> Option<Loc>

Evaluates stmt_node_loc(arg0).

pub fn define_stmt_node_loc(&mut self, arg0: StmtNode) -> Loc

Enforces that stmt_node_loc(arg0) is defined, adjoining a new element if necessary.

pub fn iter_stmt_node_loc(&self) -> impl '_ + Iterator<Item = (StmtNode, Loc)>

Returns an iterator over tuples in the graph of the stmt_node_loc function. The relation yielded by the iterator need not be functional if the model is not closed.

pub fn insert_stmt_node_loc(&mut self, arg0: StmtNode, result: Loc)

Makes the equation stmt_node_loc(arg0) = result hold.

pub fn stmt_list_node_loc(&self, arg0: StmtListNode) -> Option<Loc>

Evaluates stmt_list_node_loc(arg0).

pub fn define_stmt_list_node_loc(&mut self, arg0: StmtListNode) -> Loc

Enforces that stmt_list_node_loc(arg0) is defined, adjoining a new element if necessary.

pub fn iter_stmt_list_node_loc( &self ) -> impl '_ + Iterator<Item = (StmtListNode, Loc)>

Returns an iterator over tuples in the graph of the stmt_list_node_loc function. The relation yielded by the iterator need not be functional if the model is not closed.

pub fn insert_stmt_list_node_loc(&mut self, arg0: StmtListNode, result: Loc)

Makes the equation stmt_list_node_loc(arg0) = result hold.

pub fn rule_decl_node_loc(&self, arg0: RuleDeclNode) -> Option<Loc>

Evaluates rule_decl_node_loc(arg0).

pub fn define_rule_decl_node_loc(&mut self, arg0: RuleDeclNode) -> Loc

Enforces that rule_decl_node_loc(arg0) is defined, adjoining a new element if necessary.

pub fn iter_rule_decl_node_loc( &self ) -> impl '_ + Iterator<Item = (RuleDeclNode, Loc)>

Returns an iterator over tuples in the graph of the rule_decl_node_loc function. The relation yielded by the iterator need not be functional if the model is not closed.

pub fn insert_rule_decl_node_loc(&mut self, arg0: RuleDeclNode, result: Loc)

Makes the equation rule_decl_node_loc(arg0) = result hold.

pub fn decl_node_loc(&self, arg0: DeclNode) -> Option<Loc>

Evaluates decl_node_loc(arg0).

pub fn define_decl_node_loc(&mut self, arg0: DeclNode) -> Loc

Enforces that decl_node_loc(arg0) is defined, adjoining a new element if necessary.

pub fn iter_decl_node_loc(&self) -> impl '_ + Iterator<Item = (DeclNode, Loc)>

Returns an iterator over tuples in the graph of the decl_node_loc function. The relation yielded by the iterator need not be functional if the model is not closed.

pub fn insert_decl_node_loc(&mut self, arg0: DeclNode, result: Loc)

Makes the equation decl_node_loc(arg0) = result hold.

pub fn decl_list_node_loc(&self, arg0: DeclListNode) -> Option<Loc>

Evaluates decl_list_node_loc(arg0).

pub fn define_decl_list_node_loc(&mut self, arg0: DeclListNode) -> Loc

Enforces that decl_list_node_loc(arg0) is defined, adjoining a new element if necessary.

pub fn iter_decl_list_node_loc( &self ) -> impl '_ + Iterator<Item = (DeclListNode, Loc)>

Returns an iterator over tuples in the graph of the decl_list_node_loc function. The relation yielded by the iterator need not be functional if the model is not closed.

pub fn insert_decl_list_node_loc(&mut self, arg0: DeclListNode, result: Loc)

Makes the equation decl_list_node_loc(arg0) = result hold.

pub fn module_node_loc(&self, arg0: ModuleNode) -> Option<Loc>

Evaluates module_node_loc(arg0).

pub fn define_module_node_loc(&mut self, arg0: ModuleNode) -> Loc

Enforces that module_node_loc(arg0) is defined, adjoining a new element if necessary.

pub fn iter_module_node_loc( &self ) -> impl '_ + Iterator<Item = (ModuleNode, Loc)>

Returns an iterator over tuples in the graph of the module_node_loc function. The relation yielded by the iterator need not be functional if the model is not closed.

pub fn insert_module_node_loc(&mut self, arg0: ModuleNode, result: Loc)

Makes the equation module_node_loc(arg0) = result hold.

pub fn rule_child_term(&self, arg0: TermNode) -> Option<RuleChildNode>

Evaluates rule_child_term(arg0).

pub fn define_rule_child_term(&mut self, arg0: TermNode) -> RuleChildNode

Enforces that rule_child_term(arg0) is defined, adjoining a new element if necessary.

pub fn iter_rule_child_term( &self ) -> impl '_ + Iterator<Item = (TermNode, RuleChildNode)>

Returns an iterator over tuples in the graph of the rule_child_term function. The relation yielded by the iterator need not be functional if the model is not closed.

pub fn insert_rule_child_term(&mut self, arg0: TermNode, result: RuleChildNode)

Makes the equation rule_child_term(arg0) = result hold.

pub fn rule_child_term_list(&self, arg0: TermListNode) -> Option<RuleChildNode>

Evaluates rule_child_term_list(arg0).

pub fn define_rule_child_term_list( &mut self, arg0: TermListNode ) -> RuleChildNode

Enforces that rule_child_term_list(arg0) is defined, adjoining a new element if necessary.

pub fn iter_rule_child_term_list( &self ) -> impl '_ + Iterator<Item = (TermListNode, RuleChildNode)>

Returns an iterator over tuples in the graph of the rule_child_term_list function. The relation yielded by the iterator need not be functional if the model is not closed.

pub fn insert_rule_child_term_list( &mut self, arg0: TermListNode, result: RuleChildNode )

Makes the equation rule_child_term_list(arg0) = result hold.

pub fn rule_child_opt_term(&self, arg0: OptTermNode) -> Option<RuleChildNode>

Evaluates rule_child_opt_term(arg0).

pub fn define_rule_child_opt_term(&mut self, arg0: OptTermNode) -> RuleChildNode

Enforces that rule_child_opt_term(arg0) is defined, adjoining a new element if necessary.

pub fn iter_rule_child_opt_term( &self ) -> impl '_ + Iterator<Item = (OptTermNode, RuleChildNode)>

Returns an iterator over tuples in the graph of the rule_child_opt_term function. The relation yielded by the iterator need not be functional if the model is not closed.

pub fn insert_rule_child_opt_term( &mut self, arg0: OptTermNode, result: RuleChildNode )

Makes the equation rule_child_opt_term(arg0) = result hold.

pub fn rule_child_if_atom(&self, arg0: IfAtomNode) -> Option<RuleChildNode>

Evaluates rule_child_if_atom(arg0).

pub fn define_rule_child_if_atom(&mut self, arg0: IfAtomNode) -> RuleChildNode

Enforces that rule_child_if_atom(arg0) is defined, adjoining a new element if necessary.

pub fn iter_rule_child_if_atom( &self ) -> impl '_ + Iterator<Item = (IfAtomNode, RuleChildNode)>

Returns an iterator over tuples in the graph of the rule_child_if_atom function. The relation yielded by the iterator need not be functional if the model is not closed.

pub fn insert_rule_child_if_atom( &mut self, arg0: IfAtomNode, result: RuleChildNode )

Makes the equation rule_child_if_atom(arg0) = result hold.

pub fn rule_child_then_atom(&self, arg0: ThenAtomNode) -> Option<RuleChildNode>

Evaluates rule_child_then_atom(arg0).

pub fn define_rule_child_then_atom( &mut self, arg0: ThenAtomNode ) -> RuleChildNode

Enforces that rule_child_then_atom(arg0) is defined, adjoining a new element if necessary.

pub fn iter_rule_child_then_atom( &self ) -> impl '_ + Iterator<Item = (ThenAtomNode, RuleChildNode)>

Returns an iterator over tuples in the graph of the rule_child_then_atom function. The relation yielded by the iterator need not be functional if the model is not closed.

pub fn insert_rule_child_then_atom( &mut self, arg0: ThenAtomNode, result: RuleChildNode )

Makes the equation rule_child_then_atom(arg0) = result hold.

pub fn rule_child_stmt(&self, arg0: StmtNode) -> Option<RuleChildNode>

Evaluates rule_child_stmt(arg0).

pub fn define_rule_child_stmt(&mut self, arg0: StmtNode) -> RuleChildNode

Enforces that rule_child_stmt(arg0) is defined, adjoining a new element if necessary.

pub fn iter_rule_child_stmt( &self ) -> impl '_ + Iterator<Item = (StmtNode, RuleChildNode)>

Returns an iterator over tuples in the graph of the rule_child_stmt function. The relation yielded by the iterator need not be functional if the model is not closed.

pub fn insert_rule_child_stmt(&mut self, arg0: StmtNode, result: RuleChildNode)

Makes the equation rule_child_stmt(arg0) = result hold.

pub fn rule_child_stmt_list(&self, arg0: StmtListNode) -> Option<RuleChildNode>

Evaluates rule_child_stmt_list(arg0).

pub fn define_rule_child_stmt_list( &mut self, arg0: StmtListNode ) -> RuleChildNode

Enforces that rule_child_stmt_list(arg0) is defined, adjoining a new element if necessary.

pub fn iter_rule_child_stmt_list( &self ) -> impl '_ + Iterator<Item = (StmtListNode, RuleChildNode)>

Returns an iterator over tuples in the graph of the rule_child_stmt_list function. The relation yielded by the iterator need not be functional if the model is not closed.

pub fn insert_rule_child_stmt_list( &mut self, arg0: StmtListNode, result: RuleChildNode )

Makes the equation rule_child_stmt_list(arg0) = result hold.

pub fn nil_type_list(&self) -> Option<TypeList>

Evaluates nil_type_list().

pub fn define_nil_type_list(&mut self) -> TypeList

Enforces that nil_type_list() is defined, adjoining a new element if necessary.

pub fn iter_nil_type_list(&self) -> impl '_ + Iterator<Item = TypeList>

Returns an iterator over nil_type_list constants. The iterator may yield more than one element if the model is not closed.

pub fn insert_nil_type_list(&mut self, result: TypeList)

Makes the equation nil_type_list() = result hold.

pub fn cons_type_list(&self, arg0: Type, arg1: TypeList) -> Option<TypeList>

Evaluates cons_type_list(arg0, arg1).

pub fn define_cons_type_list(&mut self, arg0: Type, arg1: TypeList) -> TypeList

Enforces that cons_type_list(arg0, arg1) is defined, adjoining a new element if necessary.

pub fn iter_cons_type_list( &self ) -> impl '_ + Iterator<Item = (Type, TypeList, TypeList)>

Returns an iterator over tuples in the graph of the cons_type_list function. The relation yielded by the iterator need not be functional if the model is not closed.

pub fn insert_cons_type_list( &mut self, arg0: Type, arg1: TypeList, result: TypeList )

Makes the equation cons_type_list(arg0, arg1) = result hold.

pub fn semantic_type(&self, arg0: Ident) -> Option<Type>

Evaluates semantic_type(arg0).

pub fn define_semantic_type(&mut self, arg0: Ident) -> Type

Enforces that semantic_type(arg0) is defined, adjoining a new element if necessary.

pub fn iter_semantic_type(&self) -> impl '_ + Iterator<Item = (Ident, Type)>

Returns an iterator over tuples in the graph of the semantic_type function. The relation yielded by the iterator need not be functional if the model is not closed.

pub fn insert_semantic_type(&mut self, arg0: Ident, result: Type)

Makes the equation semantic_type(arg0) = result hold.

pub fn semantic_arg_types(&self, arg0: ArgDeclListNode) -> Option<TypeList>

Evaluates semantic_arg_types(arg0).

pub fn define_semantic_arg_types(&mut self, arg0: ArgDeclListNode) -> TypeList

Enforces that semantic_arg_types(arg0) is defined, adjoining a new element if necessary.

pub fn iter_semantic_arg_types( &self ) -> impl '_ + Iterator<Item = (ArgDeclListNode, TypeList)>

Returns an iterator over tuples in the graph of the semantic_arg_types function. The relation yielded by the iterator need not be functional if the model is not closed.

pub fn insert_semantic_arg_types( &mut self, arg0: ArgDeclListNode, result: TypeList )

Makes the equation semantic_arg_types(arg0) = result hold.

pub fn semantic_pred(&self, arg0: Ident) -> Option<Pred>

Evaluates semantic_pred(arg0).

pub fn define_semantic_pred(&mut self, arg0: Ident) -> Pred

Enforces that semantic_pred(arg0) is defined, adjoining a new element if necessary.

pub fn iter_semantic_pred(&self) -> impl '_ + Iterator<Item = (Ident, Pred)>

Returns an iterator over tuples in the graph of the semantic_pred function. The relation yielded by the iterator need not be functional if the model is not closed.

pub fn insert_semantic_pred(&mut self, arg0: Ident, result: Pred)

Makes the equation semantic_pred(arg0) = result hold.

pub fn arity(&self, arg0: Pred) -> Option<TypeList>

Evaluates arity(arg0).

pub fn define_arity(&mut self, arg0: Pred) -> TypeList

Enforces that arity(arg0) is defined, adjoining a new element if necessary.

pub fn iter_arity(&self) -> impl '_ + Iterator<Item = (Pred, TypeList)>

Returns an iterator over tuples in the graph of the arity function. The relation yielded by the iterator need not be functional if the model is not closed.

pub fn insert_arity(&mut self, arg0: Pred, result: TypeList)

Makes the equation arity(arg0) = result hold.

pub fn semantic_func(&self, arg0: Ident) -> Option<Func>

Evaluates semantic_func(arg0).

pub fn define_semantic_func(&mut self, arg0: Ident) -> Func

Enforces that semantic_func(arg0) is defined, adjoining a new element if necessary.

pub fn iter_semantic_func(&self) -> impl '_ + Iterator<Item = (Ident, Func)>

Returns an iterator over tuples in the graph of the semantic_func function. The relation yielded by the iterator need not be functional if the model is not closed.

pub fn insert_semantic_func(&mut self, arg0: Ident, result: Func)

Makes the equation semantic_func(arg0) = result hold.

pub fn domain(&self, arg0: Func) -> Option<TypeList>

Evaluates domain(arg0).

pub fn define_domain(&mut self, arg0: Func) -> TypeList

Enforces that domain(arg0) is defined, adjoining a new element if necessary.

pub fn iter_domain(&self) -> impl '_ + Iterator<Item = (Func, TypeList)>

Returns an iterator over tuples in the graph of the domain function. The relation yielded by the iterator need not be functional if the model is not closed.

pub fn insert_domain(&mut self, arg0: Func, result: TypeList)

Makes the equation domain(arg0) = result hold.

pub fn codomain(&self, arg0: Func) -> Option<Type>

Evaluates codomain(arg0).

pub fn define_codomain(&mut self, arg0: Func) -> Type

Enforces that codomain(arg0) is defined, adjoining a new element if necessary.

pub fn iter_codomain(&self) -> impl '_ + Iterator<Item = (Func, Type)>

Returns an iterator over tuples in the graph of the codomain function. The relation yielded by the iterator need not be functional if the model is not closed.

pub fn insert_codomain(&mut self, arg0: Func, result: Type)

Makes the equation codomain(arg0) = result hold.

pub fn nil_el_list(&self, arg0: Structure) -> Option<ElList>

Evaluates nil_el_list(arg0).

pub fn define_nil_el_list(&mut self, arg0: Structure) -> ElList

Enforces that nil_el_list(arg0) is defined, adjoining a new element if necessary.

pub fn iter_nil_el_list(&self) -> impl '_ + Iterator<Item = (Structure, ElList)>

Returns an iterator over tuples in the graph of the nil_el_list function. The relation yielded by the iterator need not be functional if the model is not closed.

pub fn insert_nil_el_list(&mut self, arg0: Structure, result: ElList)

Makes the equation nil_el_list(arg0) = result hold.

pub fn cons_el_list(&self, arg0: El, arg1: ElList) -> Option<ElList>

Evaluates cons_el_list(arg0, arg1).

pub fn define_cons_el_list(&mut self, arg0: El, arg1: ElList) -> ElList

Enforces that cons_el_list(arg0, arg1) is defined, adjoining a new element if necessary.

pub fn iter_cons_el_list( &self ) -> impl '_ + Iterator<Item = (El, ElList, ElList)>

Returns an iterator over tuples in the graph of the cons_el_list function. The relation yielded by the iterator need not be functional if the model is not closed.

pub fn insert_cons_el_list(&mut self, arg0: El, arg1: ElList, result: ElList)

Makes the equation cons_el_list(arg0, arg1) = result hold.

pub fn func_app(&self, arg0: Func, arg1: ElList) -> Option<El>

Evaluates func_app(arg0, arg1).

pub fn define_func_app(&mut self, arg0: Func, arg1: ElList) -> El

Enforces that func_app(arg0, arg1) is defined, adjoining a new element if necessary.

pub fn iter_func_app(&self) -> impl '_ + Iterator<Item = (Func, ElList, El)>

Returns an iterator over tuples in the graph of the func_app function. The relation yielded by the iterator need not be functional if the model is not closed.

pub fn insert_func_app(&mut self, arg0: Func, arg1: ElList, result: El)

Makes the equation func_app(arg0, arg1) = result hold.

pub fn var(&self, arg0: Structure, arg1: VirtIdent) -> Option<El>

Evaluates var(arg0, arg1).

pub fn define_var(&mut self, arg0: Structure, arg1: VirtIdent) -> El

Enforces that var(arg0, arg1) is defined, adjoining a new element if necessary.

pub fn iter_var(&self) -> impl '_ + Iterator<Item = (Structure, VirtIdent, El)>

Returns an iterator over tuples in the graph of the var function. The relation yielded by the iterator need not be functional if the model is not closed.

pub fn insert_var(&mut self, arg0: Structure, arg1: VirtIdent, result: El)

Makes the equation var(arg0, arg1) = result hold.

pub fn el_structure(&self, arg0: El) -> Option<Structure>

Evaluates el_structure(arg0).

pub fn define_el_structure(&mut self, arg0: El) -> Structure

Enforces that el_structure(arg0) is defined, adjoining a new element if necessary.

pub fn iter_el_structure(&self) -> impl '_ + Iterator<Item = (El, Structure)>

Returns an iterator over tuples in the graph of the el_structure function. The relation yielded by the iterator need not be functional if the model is not closed.

pub fn insert_el_structure(&mut self, arg0: El, result: Structure)

Makes the equation el_structure(arg0) = result hold.

pub fn els_structure(&self, arg0: ElList) -> Option<Structure>

Evaluates els_structure(arg0).

pub fn define_els_structure(&mut self, arg0: ElList) -> Structure

Enforces that els_structure(arg0) is defined, adjoining a new element if necessary.

pub fn iter_els_structure( &self ) -> impl '_ + Iterator<Item = (ElList, Structure)>

Returns an iterator over tuples in the graph of the els_structure function. The relation yielded by the iterator need not be functional if the model is not closed.

pub fn insert_els_structure(&mut self, arg0: ElList, result: Structure)

Makes the equation els_structure(arg0) = result hold.

pub fn dom(&self, arg0: Morphism) -> Option<Structure>

Evaluates dom(arg0).

pub fn define_dom(&mut self, arg0: Morphism) -> Structure

Enforces that dom(arg0) is defined, adjoining a new element if necessary.

pub fn iter_dom(&self) -> impl '_ + Iterator<Item = (Morphism, Structure)>

Returns an iterator over tuples in the graph of the dom function. The relation yielded by the iterator need not be functional if the model is not closed.

pub fn insert_dom(&mut self, arg0: Morphism, result: Structure)

Makes the equation dom(arg0) = result hold.

pub fn cod(&self, arg0: Morphism) -> Option<Structure>

Evaluates cod(arg0).

pub fn define_cod(&mut self, arg0: Morphism) -> Structure

Enforces that cod(arg0) is defined, adjoining a new element if necessary.

pub fn iter_cod(&self) -> impl '_ + Iterator<Item = (Morphism, Structure)>

Returns an iterator over tuples in the graph of the cod function. The relation yielded by the iterator need not be functional if the model is not closed.

pub fn insert_cod(&mut self, arg0: Morphism, result: Structure)

Makes the equation cod(arg0) = result hold.

pub fn map_el(&self, arg0: Morphism, arg1: El) -> Option<El>

Evaluates map_el(arg0, arg1).

pub fn define_map_el(&mut self, arg0: Morphism, arg1: El) -> El

Enforces that map_el(arg0, arg1) is defined, adjoining a new element if necessary.

pub fn iter_map_el(&self) -> impl '_ + Iterator<Item = (Morphism, El, El)>

Returns an iterator over tuples in the graph of the map_el function. The relation yielded by the iterator need not be functional if the model is not closed.

pub fn insert_map_el(&mut self, arg0: Morphism, arg1: El, result: El)

Makes the equation map_el(arg0, arg1) = result hold.

pub fn map_els(&self, arg0: Morphism, arg1: ElList) -> Option<ElList>

Evaluates map_els(arg0, arg1).

pub fn define_map_els(&mut self, arg0: Morphism, arg1: ElList) -> ElList

Enforces that map_els(arg0, arg1) is defined, adjoining a new element if necessary.

pub fn iter_map_els( &self ) -> impl '_ + Iterator<Item = (Morphism, ElList, ElList)>

Returns an iterator over tuples in the graph of the map_els function. The relation yielded by the iterator need not be functional if the model is not closed.

pub fn insert_map_els(&mut self, arg0: Morphism, arg1: ElList, result: ElList)

Makes the equation map_els(arg0, arg1) = result hold.

pub fn initial_structure(&self) -> Option<Structure>

Evaluates initial_structure().

pub fn define_initial_structure(&mut self) -> Structure

Enforces that initial_structure() is defined, adjoining a new element if necessary.

pub fn iter_initial_structure(&self) -> impl '_ + Iterator<Item = Structure>

Returns an iterator over initial_structure constants. The iterator may yield more than one element if the model is not closed.

pub fn insert_initial_structure(&mut self, result: Structure)

Makes the equation initial_structure() = result hold.

pub fn initiality_morphism(&self, arg0: Structure) -> Option<Morphism>

Evaluates initiality_morphism(arg0).

pub fn define_initiality_morphism(&mut self, arg0: Structure) -> Morphism

Enforces that initiality_morphism(arg0) is defined, adjoining a new element if necessary.

pub fn iter_initiality_morphism( &self ) -> impl '_ + Iterator<Item = (Structure, Morphism)>

Returns an iterator over tuples in the graph of the initiality_morphism function. The relation yielded by the iterator need not be functional if the model is not closed.

pub fn insert_initiality_morphism(&mut self, arg0: Structure, result: Morphism)

Makes the equation initiality_morphism(arg0) = result hold.

pub fn nil_chain(&self) -> Option<Chain>

Evaluates nil_chain().

pub fn define_nil_chain(&mut self) -> Chain

Enforces that nil_chain() is defined, adjoining a new element if necessary.

pub fn iter_nil_chain(&self) -> impl '_ + Iterator<Item = Chain>

Returns an iterator over nil_chain constants. The iterator may yield more than one element if the model is not closed.

pub fn insert_nil_chain(&mut self, result: Chain)

Makes the equation nil_chain() = result hold.

pub fn chain_tail(&self, arg0: Chain) -> Option<Chain>

Evaluates chain_tail(arg0).

pub fn define_chain_tail(&mut self, arg0: Chain) -> Chain

Enforces that chain_tail(arg0) is defined, adjoining a new element if necessary.

pub fn iter_chain_tail(&self) -> impl '_ + Iterator<Item = (Chain, Chain)>

Returns an iterator over tuples in the graph of the chain_tail function. The relation yielded by the iterator need not be functional if the model is not closed.

pub fn insert_chain_tail(&mut self, arg0: Chain, result: Chain)

Makes the equation chain_tail(arg0) = result hold.

pub fn chain_head_structure(&self, arg0: Chain) -> Option<Structure>

Evaluates chain_head_structure(arg0).

pub fn define_chain_head_structure(&mut self, arg0: Chain) -> Structure

Enforces that chain_head_structure(arg0) is defined, adjoining a new element if necessary.

pub fn iter_chain_head_structure( &self ) -> impl '_ + Iterator<Item = (Chain, Structure)>

Returns an iterator over tuples in the graph of the chain_head_structure function. The relation yielded by the iterator need not be functional if the model is not closed.

pub fn insert_chain_head_structure(&mut self, arg0: Chain, result: Structure)

Makes the equation chain_head_structure(arg0) = result hold.

pub fn chain_head_transition(&self, arg0: Chain) -> Option<Morphism>

Evaluates chain_head_transition(arg0).

pub fn define_chain_head_transition(&mut self, arg0: Chain) -> Morphism

Enforces that chain_head_transition(arg0) is defined, adjoining a new element if necessary.

pub fn iter_chain_head_transition( &self ) -> impl '_ + Iterator<Item = (Chain, Morphism)>

Returns an iterator over tuples in the graph of the chain_head_transition function. The relation yielded by the iterator need not be functional if the model is not closed.

pub fn insert_chain_head_transition(&mut self, arg0: Chain, result: Morphism)

Makes the equation chain_head_transition(arg0) = result hold.

pub fn type_symbol(&self) -> Option<SymbolKind>

Evaluates type_symbol().

pub fn define_type_symbol(&mut self) -> SymbolKind

Enforces that type_symbol() is defined, adjoining a new element if necessary.

pub fn iter_type_symbol(&self) -> impl '_ + Iterator<Item = SymbolKind>

Returns an iterator over type_symbol constants. The iterator may yield more than one element if the model is not closed.

pub fn insert_type_symbol(&mut self, result: SymbolKind)

Makes the equation type_symbol() = result hold.

pub fn pred_symbol(&self) -> Option<SymbolKind>

Evaluates pred_symbol().

pub fn define_pred_symbol(&mut self) -> SymbolKind

Enforces that pred_symbol() is defined, adjoining a new element if necessary.

pub fn iter_pred_symbol(&self) -> impl '_ + Iterator<Item = SymbolKind>

Returns an iterator over pred_symbol constants. The iterator may yield more than one element if the model is not closed.

pub fn insert_pred_symbol(&mut self, result: SymbolKind)

Makes the equation pred_symbol() = result hold.

pub fn func_symbol(&self) -> Option<SymbolKind>

Evaluates func_symbol().

pub fn define_func_symbol(&mut self) -> SymbolKind

Enforces that func_symbol() is defined, adjoining a new element if necessary.

pub fn iter_func_symbol(&self) -> impl '_ + Iterator<Item = SymbolKind>

Returns an iterator over func_symbol constants. The iterator may yield more than one element if the model is not closed.

pub fn insert_func_symbol(&mut self, result: SymbolKind)

Makes the equation func_symbol() = result hold.

pub fn rule_symbol(&self) -> Option<SymbolKind>

Evaluates rule_symbol().

pub fn define_rule_symbol(&mut self) -> SymbolKind

Enforces that rule_symbol() is defined, adjoining a new element if necessary.

pub fn iter_rule_symbol(&self) -> impl '_ + Iterator<Item = SymbolKind>

Returns an iterator over rule_symbol constants. The iterator may yield more than one element if the model is not closed.

pub fn insert_rule_symbol(&mut self, result: SymbolKind)

Makes the equation rule_symbol() = result hold.

pub fn zero(&self) -> Option<Nat>

Evaluates zero().

pub fn define_zero(&mut self) -> Nat

Enforces that zero() is defined, adjoining a new element if necessary.

pub fn iter_zero(&self) -> impl '_ + Iterator<Item = Nat>

Returns an iterator over zero constants. The iterator may yield more than one element if the model is not closed.

pub fn insert_zero(&mut self, result: Nat)

Makes the equation zero() = result hold.

pub fn succ(&self, arg0: Nat) -> Option<Nat>

Evaluates succ(arg0).

pub fn define_succ(&mut self, arg0: Nat) -> Nat

Enforces that succ(arg0) is defined, adjoining a new element if necessary.

pub fn iter_succ(&self) -> impl '_ + Iterator<Item = (Nat, Nat)>

Returns an iterator over tuples in the graph of the succ function. The relation yielded by the iterator need not be functional if the model is not closed.

pub fn insert_succ(&mut self, arg0: Nat, result: Nat)

Makes the equation succ(arg0) = result hold.

pub fn type_list_len(&self, arg0: TypeList) -> Option<Nat>

Evaluates type_list_len(arg0).

pub fn define_type_list_len(&mut self, arg0: TypeList) -> Nat

Enforces that type_list_len(arg0) is defined, adjoining a new element if necessary.

pub fn iter_type_list_len(&self) -> impl '_ + Iterator<Item = (TypeList, Nat)>

Returns an iterator over tuples in the graph of the type_list_len function. The relation yielded by the iterator need not be functional if the model is not closed.

pub fn insert_type_list_len(&mut self, arg0: TypeList, result: Nat)

Makes the equation type_list_len(arg0) = result hold.

pub fn term_list_len(&self, arg0: TermListNode) -> Option<Nat>

Evaluates term_list_len(arg0).

pub fn define_term_list_len(&mut self, arg0: TermListNode) -> Nat

Enforces that term_list_len(arg0) is defined, adjoining a new element if necessary.

pub fn iter_term_list_len( &self ) -> impl '_ + Iterator<Item = (TermListNode, Nat)>

Returns an iterator over tuples in the graph of the term_list_len function. The relation yielded by the iterator need not be functional if the model is not closed.

pub fn insert_term_list_len(&mut self, arg0: TermListNode, result: Nat)

Makes the equation term_list_len(arg0) = result hold.

pub fn rule_chain(&self, arg0: RuleDeclNode) -> Option<Chain>

Evaluates rule_chain(arg0).

pub fn define_rule_chain(&mut self, arg0: RuleDeclNode) -> Chain

Enforces that rule_chain(arg0) is defined, adjoining a new element if necessary.

pub fn iter_rule_chain( &self ) -> impl '_ + Iterator<Item = (RuleDeclNode, Chain)>

Returns an iterator over tuples in the graph of the rule_chain function. The relation yielded by the iterator need not be functional if the model is not closed.

pub fn insert_rule_chain(&mut self, arg0: RuleDeclNode, result: Chain)

Makes the equation rule_chain(arg0) = result hold.

pub fn stmt_list_chain(&self, arg0: StmtListNode) -> Option<Chain>

Evaluates stmt_list_chain(arg0).

pub fn define_stmt_list_chain(&mut self, arg0: StmtListNode) -> Chain

Enforces that stmt_list_chain(arg0) is defined, adjoining a new element if necessary.

pub fn iter_stmt_list_chain( &self ) -> impl '_ + Iterator<Item = (StmtListNode, Chain)>

Returns an iterator over tuples in the graph of the stmt_list_chain function. The relation yielded by the iterator need not be functional if the model is not closed.

pub fn insert_stmt_list_chain(&mut self, arg0: StmtListNode, result: Chain)

Makes the equation stmt_list_chain(arg0) = result hold.

pub fn stmt_structure(&self, arg0: StmtNode) -> Option<Structure>

Evaluates stmt_structure(arg0).

pub fn define_stmt_structure(&mut self, arg0: StmtNode) -> Structure

Enforces that stmt_structure(arg0) is defined, adjoining a new element if necessary.

pub fn iter_stmt_structure( &self ) -> impl '_ + Iterator<Item = (StmtNode, Structure)>

Returns an iterator over tuples in the graph of the stmt_structure function. The relation yielded by the iterator need not be functional if the model is not closed.

pub fn insert_stmt_structure(&mut self, arg0: StmtNode, result: Structure)

Makes the equation stmt_structure(arg0) = result hold.

pub fn if_atom_structure(&self, arg0: IfAtomNode) -> Option<Structure>

Evaluates if_atom_structure(arg0).

pub fn define_if_atom_structure(&mut self, arg0: IfAtomNode) -> Structure

Enforces that if_atom_structure(arg0) is defined, adjoining a new element if necessary.

pub fn iter_if_atom_structure( &self ) -> impl '_ + Iterator<Item = (IfAtomNode, Structure)>

Returns an iterator over tuples in the graph of the if_atom_structure function. The relation yielded by the iterator need not be functional if the model is not closed.

pub fn insert_if_atom_structure(&mut self, arg0: IfAtomNode, result: Structure)

Makes the equation if_atom_structure(arg0) = result hold.

pub fn then_atom_structure(&self, arg0: ThenAtomNode) -> Option<Structure>

Evaluates then_atom_structure(arg0).

pub fn define_then_atom_structure(&mut self, arg0: ThenAtomNode) -> Structure

Enforces that then_atom_structure(arg0) is defined, adjoining a new element if necessary.

pub fn iter_then_atom_structure( &self ) -> impl '_ + Iterator<Item = (ThenAtomNode, Structure)>

Returns an iterator over tuples in the graph of the then_atom_structure function. The relation yielded by the iterator need not be functional if the model is not closed.

pub fn insert_then_atom_structure( &mut self, arg0: ThenAtomNode, result: Structure )

Makes the equation then_atom_structure(arg0) = result hold.

pub fn term_structure(&self, arg0: TermNode) -> Option<Structure>

Evaluates term_structure(arg0).

pub fn define_term_structure(&mut self, arg0: TermNode) -> Structure

Enforces that term_structure(arg0) is defined, adjoining a new element if necessary.

pub fn iter_term_structure( &self ) -> impl '_ + Iterator<Item = (TermNode, Structure)>

Returns an iterator over tuples in the graph of the term_structure function. The relation yielded by the iterator need not be functional if the model is not closed.

pub fn insert_term_structure(&mut self, arg0: TermNode, result: Structure)

Makes the equation term_structure(arg0) = result hold.

pub fn terms_structure(&self, arg0: TermListNode) -> Option<Structure>

Evaluates terms_structure(arg0).

pub fn define_terms_structure(&mut self, arg0: TermListNode) -> Structure

Enforces that terms_structure(arg0) is defined, adjoining a new element if necessary.

pub fn iter_terms_structure( &self ) -> impl '_ + Iterator<Item = (TermListNode, Structure)>

Returns an iterator over tuples in the graph of the terms_structure function. The relation yielded by the iterator need not be functional if the model is not closed.

pub fn insert_terms_structure(&mut self, arg0: TermListNode, result: Structure)

Makes the equation terms_structure(arg0) = result hold.

pub fn opt_term_structure(&self, arg0: OptTermNode) -> Option<Structure>

Evaluates opt_term_structure(arg0).

pub fn define_opt_term_structure(&mut self, arg0: OptTermNode) -> Structure

Enforces that opt_term_structure(arg0) is defined, adjoining a new element if necessary.

pub fn iter_opt_term_structure( &self ) -> impl '_ + Iterator<Item = (OptTermNode, Structure)>

Returns an iterator over tuples in the graph of the opt_term_structure function. The relation yielded by the iterator need not be functional if the model is not closed.

pub fn insert_opt_term_structure( &mut self, arg0: OptTermNode, result: Structure )

Makes the equation opt_term_structure(arg0) = result hold.

pub fn semantic_el(&self, arg0: TermNode) -> Option<El>

Evaluates semantic_el(arg0).

pub fn define_semantic_el(&mut self, arg0: TermNode) -> El

Enforces that semantic_el(arg0) is defined, adjoining a new element if necessary.

pub fn iter_semantic_el(&self) -> impl '_ + Iterator<Item = (TermNode, El)>

Returns an iterator over tuples in the graph of the semantic_el function. The relation yielded by the iterator need not be functional if the model is not closed.

pub fn insert_semantic_el(&mut self, arg0: TermNode, result: El)

Makes the equation semantic_el(arg0) = result hold.

pub fn semantic_els(&self, arg0: TermListNode) -> Option<ElList>

Evaluates semantic_els(arg0).

pub fn define_semantic_els(&mut self, arg0: TermListNode) -> ElList

Enforces that semantic_els(arg0) is defined, adjoining a new element if necessary.

pub fn iter_semantic_els( &self ) -> impl '_ + Iterator<Item = (TermListNode, ElList)>

Returns an iterator over tuples in the graph of the semantic_els function. The relation yielded by the iterator need not be functional if the model is not closed.

pub fn insert_semantic_els(&mut self, arg0: TermListNode, result: ElList)

Makes the equation semantic_els(arg0) = result hold.

pub fn wildcard_virt_ident(&self, arg0: TermNode) -> Option<VirtIdent>

Evaluates wildcard_virt_ident(arg0).

pub fn define_wildcard_virt_ident(&mut self, arg0: TermNode) -> VirtIdent

Enforces that wildcard_virt_ident(arg0) is defined, adjoining a new element if necessary.

pub fn iter_wildcard_virt_ident( &self ) -> impl '_ + Iterator<Item = (TermNode, VirtIdent)>

Returns an iterator over tuples in the graph of the wildcard_virt_ident function. The relation yielded by the iterator need not be functional if the model is not closed.

pub fn insert_wildcard_virt_ident(&mut self, arg0: TermNode, result: VirtIdent)

Makes the equation wildcard_virt_ident(arg0) = result hold.

pub fn grouped_rule_chain(&self, arg0: RuleDeclNode) -> Option<Chain>

Evaluates grouped_rule_chain(arg0).

pub fn define_grouped_rule_chain(&mut self, arg0: RuleDeclNode) -> Chain

Enforces that grouped_rule_chain(arg0) is defined, adjoining a new element if necessary.

pub fn iter_grouped_rule_chain( &self ) -> impl '_ + Iterator<Item = (RuleDeclNode, Chain)>

Returns an iterator over tuples in the graph of the grouped_rule_chain function. The relation yielded by the iterator need not be functional if the model is not closed.

pub fn insert_grouped_rule_chain(&mut self, arg0: RuleDeclNode, result: Chain)

Makes the equation grouped_rule_chain(arg0) = result hold.

pub fn grouped_stmt_list_chain(&self, arg0: StmtListNode) -> Option<Chain>

Evaluates grouped_stmt_list_chain(arg0).

pub fn define_grouped_stmt_list_chain(&mut self, arg0: StmtListNode) -> Chain

Enforces that grouped_stmt_list_chain(arg0) is defined, adjoining a new element if necessary.

pub fn iter_grouped_stmt_list_chain( &self ) -> impl '_ + Iterator<Item = (StmtListNode, Chain)>

Returns an iterator over tuples in the graph of the grouped_stmt_list_chain function. The relation yielded by the iterator need not be functional if the model is not closed.

pub fn insert_grouped_stmt_list_chain( &mut self, arg0: StmtListNode, result: Chain )

Makes the equation grouped_stmt_list_chain(arg0) = result hold.

pub fn absurd(&self) -> bool

Returns true if absurd() holds.

pub fn insert_absurd(&mut self)

Makes absurd() hold.

pub fn type_decl(&self, arg0: TypeDeclNode, arg1: Ident) -> bool

Returns true if type_decl(arg0, arg1) holds.

pub fn iter_type_decl(&self) -> impl '_ + Iterator<Item = (TypeDeclNode, Ident)>

Returns an iterator over tuples of elements satisfying the type_decl predicate.

pub fn insert_type_decl(&mut self, arg0: TypeDeclNode, arg1: Ident)

Makes type_decl(arg0, arg1) hold.

pub fn arg_decl_node_name(&self, arg0: ArgDeclNode, arg1: Ident) -> bool

Returns true if arg_decl_node_name(arg0, arg1) holds.

pub fn iter_arg_decl_node_name( &self ) -> impl '_ + Iterator<Item = (ArgDeclNode, Ident)>

Returns an iterator over tuples of elements satisfying the arg_decl_node_name predicate.

pub fn insert_arg_decl_node_name(&mut self, arg0: ArgDeclNode, arg1: Ident)

Makes arg_decl_node_name(arg0, arg1) hold.

pub fn arg_decl_node_type(&self, arg0: ArgDeclNode, arg1: Ident) -> bool

Returns true if arg_decl_node_type(arg0, arg1) holds.

pub fn iter_arg_decl_node_type( &self ) -> impl '_ + Iterator<Item = (ArgDeclNode, Ident)>

Returns an iterator over tuples of elements satisfying the arg_decl_node_type predicate.

pub fn insert_arg_decl_node_type(&mut self, arg0: ArgDeclNode, arg1: Ident)

Makes arg_decl_node_type(arg0, arg1) hold.

pub fn nil_arg_decl_list_node(&self, arg0: ArgDeclListNode) -> bool

Returns true if nil_arg_decl_list_node(arg0) holds.

pub fn iter_nil_arg_decl_list_node( &self ) -> impl '_ + Iterator<Item = ArgDeclListNode>

Returns an iterator over elements satisfying the nil_arg_decl_list_node predicate.

pub fn insert_nil_arg_decl_list_node(&mut self, arg0: ArgDeclListNode)

Makes nil_arg_decl_list_node(arg0) hold.

pub fn cons_arg_decl_list_node( &self, arg0: ArgDeclListNode, arg1: ArgDeclNode, arg2: ArgDeclListNode ) -> bool

Returns true if cons_arg_decl_list_node(arg0, arg1, arg2) holds.

pub fn iter_cons_arg_decl_list_node( &self ) -> impl '_ + Iterator<Item = (ArgDeclListNode, ArgDeclNode, ArgDeclListNode)>

Returns an iterator over tuples of elements satisfying the cons_arg_decl_list_node predicate.

pub fn insert_cons_arg_decl_list_node( &mut self, arg0: ArgDeclListNode, arg1: ArgDeclNode, arg2: ArgDeclListNode )

Makes cons_arg_decl_list_node(arg0, arg1, arg2) hold.

pub fn pred_decl( &self, arg0: PredDeclNode, arg1: Ident, arg2: ArgDeclListNode ) -> bool

Returns true if pred_decl(arg0, arg1, arg2) holds.

pub fn iter_pred_decl( &self ) -> impl '_ + Iterator<Item = (PredDeclNode, Ident, ArgDeclListNode)>

Returns an iterator over tuples of elements satisfying the pred_decl predicate.

pub fn insert_pred_decl( &mut self, arg0: PredDeclNode, arg1: Ident, arg2: ArgDeclListNode )

Makes pred_decl(arg0, arg1, arg2) hold.

pub fn func_decl( &self, arg0: FuncDeclNode, arg1: Ident, arg2: ArgDeclListNode, arg3: Ident ) -> bool

Returns true if func_decl(arg0, arg1, arg2, arg3) holds.

pub fn iter_func_decl( &self ) -> impl '_ + Iterator<Item = (FuncDeclNode, Ident, ArgDeclListNode, Ident)>

Returns an iterator over tuples of elements satisfying the func_decl predicate.

pub fn insert_func_decl( &mut self, arg0: FuncDeclNode, arg1: Ident, arg2: ArgDeclListNode, arg3: Ident )

Makes func_decl(arg0, arg1, arg2, arg3) hold.

pub fn nil_term_list_node(&self, arg0: TermListNode) -> bool

Returns true if nil_term_list_node(arg0) holds.

pub fn iter_nil_term_list_node(&self) -> impl '_ + Iterator<Item = TermListNode>

Returns an iterator over elements satisfying the nil_term_list_node predicate.

pub fn insert_nil_term_list_node(&mut self, arg0: TermListNode)

Makes nil_term_list_node(arg0) hold.

pub fn cons_term_list_node( &self, arg0: TermListNode, arg1: TermNode, arg2: TermListNode ) -> bool

Returns true if cons_term_list_node(arg0, arg1, arg2) holds.

pub fn iter_cons_term_list_node( &self ) -> impl '_ + Iterator<Item = (TermListNode, TermNode, TermListNode)>

Returns an iterator over tuples of elements satisfying the cons_term_list_node predicate.

pub fn insert_cons_term_list_node( &mut self, arg0: TermListNode, arg1: TermNode, arg2: TermListNode )

Makes cons_term_list_node(arg0, arg1, arg2) hold.

pub fn none_term_node(&self, arg0: OptTermNode) -> bool

Returns true if none_term_node(arg0) holds.

pub fn iter_none_term_node(&self) -> impl '_ + Iterator<Item = OptTermNode>

Returns an iterator over elements satisfying the none_term_node predicate.

pub fn insert_none_term_node(&mut self, arg0: OptTermNode)

Makes none_term_node(arg0) hold.

pub fn some_term_node(&self, arg0: OptTermNode, arg1: TermNode) -> bool

Returns true if some_term_node(arg0, arg1) holds.

pub fn iter_some_term_node( &self ) -> impl '_ + Iterator<Item = (OptTermNode, TermNode)>

Returns an iterator over tuples of elements satisfying the some_term_node predicate.

pub fn insert_some_term_node(&mut self, arg0: OptTermNode, arg1: TermNode)

Makes some_term_node(arg0, arg1) hold.

pub fn var_term_node(&self, arg0: TermNode, arg1: Ident) -> bool

Returns true if var_term_node(arg0, arg1) holds.

pub fn iter_var_term_node(&self) -> impl '_ + Iterator<Item = (TermNode, Ident)>

Returns an iterator over tuples of elements satisfying the var_term_node predicate.

pub fn insert_var_term_node(&mut self, arg0: TermNode, arg1: Ident)

Makes var_term_node(arg0, arg1) hold.

pub fn wildcard_term_node(&self, arg0: TermNode) -> bool

Returns true if wildcard_term_node(arg0) holds.

pub fn iter_wildcard_term_node(&self) -> impl '_ + Iterator<Item = TermNode>

Returns an iterator over elements satisfying the wildcard_term_node predicate.

pub fn insert_wildcard_term_node(&mut self, arg0: TermNode)

Makes wildcard_term_node(arg0) hold.

pub fn app_term_node( &self, arg0: TermNode, arg1: Ident, arg2: TermListNode ) -> bool

Returns true if app_term_node(arg0, arg1, arg2) holds.

pub fn iter_app_term_node( &self ) -> impl '_ + Iterator<Item = (TermNode, Ident, TermListNode)>

Returns an iterator over tuples of elements satisfying the app_term_node predicate.

pub fn insert_app_term_node( &mut self, arg0: TermNode, arg1: Ident, arg2: TermListNode )

Makes app_term_node(arg0, arg1, arg2) hold.

pub fn equal_if_atom_node( &self, arg0: IfAtomNode, arg1: TermNode, arg2: TermNode ) -> bool

Returns true if equal_if_atom_node(arg0, arg1, arg2) holds.

pub fn iter_equal_if_atom_node( &self ) -> impl '_ + Iterator<Item = (IfAtomNode, TermNode, TermNode)>

Returns an iterator over tuples of elements satisfying the equal_if_atom_node predicate.

pub fn insert_equal_if_atom_node( &mut self, arg0: IfAtomNode, arg1: TermNode, arg2: TermNode )

Makes equal_if_atom_node(arg0, arg1, arg2) hold.

pub fn defined_if_atom_node(&self, arg0: IfAtomNode, arg1: TermNode) -> bool

Returns true if defined_if_atom_node(arg0, arg1) holds.

pub fn iter_defined_if_atom_node( &self ) -> impl '_ + Iterator<Item = (IfAtomNode, TermNode)>

Returns an iterator over tuples of elements satisfying the defined_if_atom_node predicate.

pub fn insert_defined_if_atom_node(&mut self, arg0: IfAtomNode, arg1: TermNode)

Makes defined_if_atom_node(arg0, arg1) hold.

pub fn pred_if_atom_node( &self, arg0: IfAtomNode, arg1: Ident, arg2: TermListNode ) -> bool

Returns true if pred_if_atom_node(arg0, arg1, arg2) holds.

pub fn iter_pred_if_atom_node( &self ) -> impl '_ + Iterator<Item = (IfAtomNode, Ident, TermListNode)>

Returns an iterator over tuples of elements satisfying the pred_if_atom_node predicate.

pub fn insert_pred_if_atom_node( &mut self, arg0: IfAtomNode, arg1: Ident, arg2: TermListNode )

Makes pred_if_atom_node(arg0, arg1, arg2) hold.

pub fn var_if_atom_node( &self, arg0: IfAtomNode, arg1: TermNode, arg2: Ident ) -> bool

Returns true if var_if_atom_node(arg0, arg1, arg2) holds.

pub fn iter_var_if_atom_node( &self ) -> impl '_ + Iterator<Item = (IfAtomNode, TermNode, Ident)>

Returns an iterator over tuples of elements satisfying the var_if_atom_node predicate.

pub fn insert_var_if_atom_node( &mut self, arg0: IfAtomNode, arg1: TermNode, arg2: Ident )

Makes var_if_atom_node(arg0, arg1, arg2) hold.

pub fn equal_then_atom_node( &self, arg0: ThenAtomNode, arg1: TermNode, arg2: TermNode ) -> bool

Returns true if equal_then_atom_node(arg0, arg1, arg2) holds.

pub fn iter_equal_then_atom_node( &self ) -> impl '_ + Iterator<Item = (ThenAtomNode, TermNode, TermNode)>

Returns an iterator over tuples of elements satisfying the equal_then_atom_node predicate.

pub fn insert_equal_then_atom_node( &mut self, arg0: ThenAtomNode, arg1: TermNode, arg2: TermNode )

Makes equal_then_atom_node(arg0, arg1, arg2) hold.

pub fn defined_then_atom_node( &self, arg0: ThenAtomNode, arg1: OptTermNode, arg2: TermNode ) -> bool

Returns true if defined_then_atom_node(arg0, arg1, arg2) holds.

pub fn iter_defined_then_atom_node( &self ) -> impl '_ + Iterator<Item = (ThenAtomNode, OptTermNode, TermNode)>

Returns an iterator over tuples of elements satisfying the defined_then_atom_node predicate.

pub fn insert_defined_then_atom_node( &mut self, arg0: ThenAtomNode, arg1: OptTermNode, arg2: TermNode )

Makes defined_then_atom_node(arg0, arg1, arg2) hold.

pub fn pred_then_atom_node( &self, arg0: ThenAtomNode, arg1: Ident, arg2: TermListNode ) -> bool

Returns true if pred_then_atom_node(arg0, arg1, arg2) holds.

pub fn iter_pred_then_atom_node( &self ) -> impl '_ + Iterator<Item = (ThenAtomNode, Ident, TermListNode)>

Returns an iterator over tuples of elements satisfying the pred_then_atom_node predicate.

pub fn insert_pred_then_atom_node( &mut self, arg0: ThenAtomNode, arg1: Ident, arg2: TermListNode )

Makes pred_then_atom_node(arg0, arg1, arg2) hold.

pub fn if_stmt_node(&self, arg0: StmtNode, arg1: IfAtomNode) -> bool

Returns true if if_stmt_node(arg0, arg1) holds.

pub fn iter_if_stmt_node( &self ) -> impl '_ + Iterator<Item = (StmtNode, IfAtomNode)>

Returns an iterator over tuples of elements satisfying the if_stmt_node predicate.

pub fn insert_if_stmt_node(&mut self, arg0: StmtNode, arg1: IfAtomNode)

Makes if_stmt_node(arg0, arg1) hold.

pub fn then_stmt_node(&self, arg0: StmtNode, arg1: ThenAtomNode) -> bool

Returns true if then_stmt_node(arg0, arg1) holds.

pub fn iter_then_stmt_node( &self ) -> impl '_ + Iterator<Item = (StmtNode, ThenAtomNode)>

Returns an iterator over tuples of elements satisfying the then_stmt_node predicate.

pub fn insert_then_stmt_node(&mut self, arg0: StmtNode, arg1: ThenAtomNode)

Makes then_stmt_node(arg0, arg1) hold.

pub fn nil_stmt_list_node(&self, arg0: StmtListNode) -> bool

Returns true if nil_stmt_list_node(arg0) holds.

pub fn iter_nil_stmt_list_node(&self) -> impl '_ + Iterator<Item = StmtListNode>

Returns an iterator over elements satisfying the nil_stmt_list_node predicate.

pub fn insert_nil_stmt_list_node(&mut self, arg0: StmtListNode)

Makes nil_stmt_list_node(arg0) hold.

pub fn cons_stmt_list_node( &self, arg0: StmtListNode, arg1: StmtNode, arg2: StmtListNode ) -> bool

Returns true if cons_stmt_list_node(arg0, arg1, arg2) holds.

pub fn iter_cons_stmt_list_node( &self ) -> impl '_ + Iterator<Item = (StmtListNode, StmtNode, StmtListNode)>

Returns an iterator over tuples of elements satisfying the cons_stmt_list_node predicate.

pub fn insert_cons_stmt_list_node( &mut self, arg0: StmtListNode, arg1: StmtNode, arg2: StmtListNode )

Makes cons_stmt_list_node(arg0, arg1, arg2) hold.

pub fn rule_decl(&self, arg0: RuleDeclNode, arg1: StmtListNode) -> bool

Returns true if rule_decl(arg0, arg1) holds.

pub fn iter_rule_decl( &self ) -> impl '_ + Iterator<Item = (RuleDeclNode, StmtListNode)>

Returns an iterator over tuples of elements satisfying the rule_decl predicate.

pub fn insert_rule_decl(&mut self, arg0: RuleDeclNode, arg1: StmtListNode)

Makes rule_decl(arg0, arg1) hold.

pub fn decl_node_type(&self, arg0: DeclNode, arg1: TypeDeclNode) -> bool

Returns true if decl_node_type(arg0, arg1) holds.

pub fn iter_decl_node_type( &self ) -> impl '_ + Iterator<Item = (DeclNode, TypeDeclNode)>

Returns an iterator over tuples of elements satisfying the decl_node_type predicate.

pub fn insert_decl_node_type(&mut self, arg0: DeclNode, arg1: TypeDeclNode)

Makes decl_node_type(arg0, arg1) hold.

pub fn decl_node_pred(&self, arg0: DeclNode, arg1: PredDeclNode) -> bool

Returns true if decl_node_pred(arg0, arg1) holds.

pub fn iter_decl_node_pred( &self ) -> impl '_ + Iterator<Item = (DeclNode, PredDeclNode)>

Returns an iterator over tuples of elements satisfying the decl_node_pred predicate.

pub fn insert_decl_node_pred(&mut self, arg0: DeclNode, arg1: PredDeclNode)

Makes decl_node_pred(arg0, arg1) hold.

pub fn decl_node_func(&self, arg0: DeclNode, arg1: FuncDeclNode) -> bool

Returns true if decl_node_func(arg0, arg1) holds.

pub fn iter_decl_node_func( &self ) -> impl '_ + Iterator<Item = (DeclNode, FuncDeclNode)>

Returns an iterator over tuples of elements satisfying the decl_node_func predicate.

pub fn insert_decl_node_func(&mut self, arg0: DeclNode, arg1: FuncDeclNode)

Makes decl_node_func(arg0, arg1) hold.

pub fn decl_node_rule(&self, arg0: DeclNode, arg1: RuleDeclNode) -> bool

Returns true if decl_node_rule(arg0, arg1) holds.

pub fn iter_decl_node_rule( &self ) -> impl '_ + Iterator<Item = (DeclNode, RuleDeclNode)>

Returns an iterator over tuples of elements satisfying the decl_node_rule predicate.

pub fn insert_decl_node_rule(&mut self, arg0: DeclNode, arg1: RuleDeclNode)

Makes decl_node_rule(arg0, arg1) hold.

pub fn nil_decl_list_node(&self, arg0: DeclListNode) -> bool

Returns true if nil_decl_list_node(arg0) holds.

pub fn iter_nil_decl_list_node(&self) -> impl '_ + Iterator<Item = DeclListNode>

Returns an iterator over elements satisfying the nil_decl_list_node predicate.

pub fn insert_nil_decl_list_node(&mut self, arg0: DeclListNode)

Makes nil_decl_list_node(arg0) hold.

pub fn cons_decl_list_node( &self, arg0: DeclListNode, arg1: DeclNode, arg2: DeclListNode ) -> bool

Returns true if cons_decl_list_node(arg0, arg1, arg2) holds.

pub fn iter_cons_decl_list_node( &self ) -> impl '_ + Iterator<Item = (DeclListNode, DeclNode, DeclListNode)>

Returns an iterator over tuples of elements satisfying the cons_decl_list_node predicate.

pub fn insert_cons_decl_list_node( &mut self, arg0: DeclListNode, arg1: DeclNode, arg2: DeclListNode )

Makes cons_decl_list_node(arg0, arg1, arg2) hold.

pub fn decls_module_node(&self, arg0: ModuleNode, arg1: DeclListNode) -> bool

Returns true if decls_module_node(arg0, arg1) holds.

pub fn iter_decls_module_node( &self ) -> impl '_ + Iterator<Item = (ModuleNode, DeclListNode)>

Returns an iterator over tuples of elements satisfying the decls_module_node predicate.

pub fn insert_decls_module_node(&mut self, arg0: ModuleNode, arg1: DeclListNode)

Makes decls_module_node(arg0, arg1) hold.

pub fn rule_child(&self, arg0: RuleChildNode, arg1: RuleDeclNode) -> bool

Returns true if rule_child(arg0, arg1) holds.

pub fn iter_rule_child( &self ) -> impl '_ + Iterator<Item = (RuleChildNode, RuleDeclNode)>

Returns an iterator over tuples of elements satisfying the rule_child predicate.

pub fn insert_rule_child(&mut self, arg0: RuleChildNode, arg1: RuleDeclNode)

Makes rule_child(arg0, arg1) hold.

pub fn pred_app(&self, arg0: Pred, arg1: ElList) -> bool

Returns true if pred_app(arg0, arg1) holds.

pub fn iter_pred_app(&self) -> impl '_ + Iterator<Item = (Pred, ElList)>

Returns an iterator over tuples of elements satisfying the pred_app predicate.

pub fn insert_pred_app(&mut self, arg0: Pred, arg1: ElList)

Makes pred_app(arg0, arg1) hold.

pub fn el_type(&self, arg0: El, arg1: Type) -> bool

Returns true if el_type(arg0, arg1) holds.

pub fn iter_el_type(&self) -> impl '_ + Iterator<Item = (El, Type)>

Returns an iterator over tuples of elements satisfying the el_type predicate.

pub fn insert_el_type(&mut self, arg0: El, arg1: Type)

Makes el_type(arg0, arg1) hold.

pub fn el_types(&self, arg0: ElList, arg1: TypeList) -> bool

Returns true if el_types(arg0, arg1) holds.

pub fn iter_el_types(&self) -> impl '_ + Iterator<Item = (ElList, TypeList)>

Returns an iterator over tuples of elements satisfying the el_types predicate.

pub fn insert_el_types(&mut self, arg0: ElList, arg1: TypeList)

Makes el_types(arg0, arg1) hold.

pub fn constrained_el(&self, arg0: El) -> bool

Returns true if constrained_el(arg0) holds.

pub fn iter_constrained_el(&self) -> impl '_ + Iterator<Item = El>

Returns an iterator over elements satisfying the constrained_el predicate.

pub fn insert_constrained_el(&mut self, arg0: El)

Makes constrained_el(arg0) hold.

pub fn constrained_els(&self, arg0: ElList) -> bool

Returns true if constrained_els(arg0) holds.

pub fn iter_constrained_els(&self) -> impl '_ + Iterator<Item = ElList>

Returns an iterator over elements satisfying the constrained_els predicate.

pub fn insert_constrained_els(&mut self, arg0: ElList)

Makes constrained_els(arg0) hold.

pub fn in_ker(&self, arg0: Morphism, arg1: El, arg2: El) -> bool

Returns true if in_ker(arg0, arg1, arg2) holds.

pub fn iter_in_ker(&self) -> impl '_ + Iterator<Item = (Morphism, El, El)>

Returns an iterator over tuples of elements satisfying the in_ker predicate.

pub fn insert_in_ker(&mut self, arg0: Morphism, arg1: El, arg2: El)

Makes in_ker(arg0, arg1, arg2) hold.

pub fn el_in_img(&self, arg0: Morphism, arg1: El) -> bool

Returns true if el_in_img(arg0, arg1) holds.

pub fn iter_el_in_img(&self) -> impl '_ + Iterator<Item = (Morphism, El)>

Returns an iterator over tuples of elements satisfying the el_in_img predicate.

pub fn insert_el_in_img(&mut self, arg0: Morphism, arg1: El)

Makes el_in_img(arg0, arg1) hold.

pub fn pred_tuple_in_img( &self, arg0: Morphism, arg1: Pred, arg2: ElList ) -> bool

Returns true if pred_tuple_in_img(arg0, arg1, arg2) holds.

pub fn iter_pred_tuple_in_img( &self ) -> impl '_ + Iterator<Item = (Morphism, Pred, ElList)>

Returns an iterator over tuples of elements satisfying the pred_tuple_in_img predicate.

pub fn insert_pred_tuple_in_img( &mut self, arg0: Morphism, arg1: Pred, arg2: ElList )

Makes pred_tuple_in_img(arg0, arg1, arg2) hold.

pub fn func_app_in_img(&self, arg0: Morphism, arg1: Func, arg2: ElList) -> bool

Returns true if func_app_in_img(arg0, arg1, arg2) holds.

pub fn iter_func_app_in_img( &self ) -> impl '_ + Iterator<Item = (Morphism, Func, ElList)>

Returns an iterator over tuples of elements satisfying the func_app_in_img predicate.

pub fn insert_func_app_in_img( &mut self, arg0: Morphism, arg1: Func, arg2: ElList )

Makes func_app_in_img(arg0, arg1, arg2) hold.

pub fn defined_symbol(&self, arg0: Ident, arg1: SymbolKind, arg2: Loc) -> bool

Returns true if defined_symbol(arg0, arg1, arg2) holds.

pub fn iter_defined_symbol( &self ) -> impl '_ + Iterator<Item = (Ident, SymbolKind, Loc)>

Returns an iterator over tuples of elements satisfying the defined_symbol predicate.

pub fn insert_defined_symbol( &mut self, arg0: Ident, arg1: SymbolKind, arg2: Loc )

Makes defined_symbol(arg0, arg1, arg2) hold.

pub fn should_be_symbol(&self, arg0: Ident, arg1: SymbolKind, arg2: Loc) -> bool

Returns true if should_be_symbol(arg0, arg1, arg2) holds.

pub fn iter_should_be_symbol( &self ) -> impl '_ + Iterator<Item = (Ident, SymbolKind, Loc)>

Returns an iterator over tuples of elements satisfying the should_be_symbol predicate.

pub fn insert_should_be_symbol( &mut self, arg0: Ident, arg1: SymbolKind, arg2: Loc )

Makes should_be_symbol(arg0, arg1, arg2) hold.

pub fn pred_arg_num_should_match(&self, arg0: Nat, arg1: Nat, arg2: Loc) -> bool

Returns true if pred_arg_num_should_match(arg0, arg1, arg2) holds.

pub fn iter_pred_arg_num_should_match( &self ) -> impl '_ + Iterator<Item = (Nat, Nat, Loc)>

Returns an iterator over tuples of elements satisfying the pred_arg_num_should_match predicate.

pub fn insert_pred_arg_num_should_match( &mut self, arg0: Nat, arg1: Nat, arg2: Loc )

Makes pred_arg_num_should_match(arg0, arg1, arg2) hold.

pub fn func_arg_num_should_match(&self, arg0: Nat, arg1: Nat, arg2: Loc) -> bool

Returns true if func_arg_num_should_match(arg0, arg1, arg2) holds.

pub fn iter_func_arg_num_should_match( &self ) -> impl '_ + Iterator<Item = (Nat, Nat, Loc)>

Returns an iterator over tuples of elements satisfying the func_arg_num_should_match predicate.

pub fn insert_func_arg_num_should_match( &mut self, arg0: Nat, arg1: Nat, arg2: Loc )

Makes func_arg_num_should_match(arg0, arg1, arg2) hold.

pub fn var_before_term(&self, arg0: TermNode, arg1: VirtIdent) -> bool

Returns true if var_before_term(arg0, arg1) holds.

pub fn iter_var_before_term( &self ) -> impl '_ + Iterator<Item = (TermNode, VirtIdent)>

Returns an iterator over tuples of elements satisfying the var_before_term predicate.

pub fn insert_var_before_term(&mut self, arg0: TermNode, arg1: VirtIdent)

Makes var_before_term(arg0, arg1) hold.

pub fn var_before_terms(&self, arg0: TermListNode, arg1: VirtIdent) -> bool

Returns true if var_before_terms(arg0, arg1) holds.

pub fn iter_var_before_terms( &self ) -> impl '_ + Iterator<Item = (TermListNode, VirtIdent)>

Returns an iterator over tuples of elements satisfying the var_before_terms predicate.

pub fn insert_var_before_terms(&mut self, arg0: TermListNode, arg1: VirtIdent)

Makes var_before_terms(arg0, arg1) hold.

pub fn var_before_opt_term(&self, arg0: OptTermNode, arg1: VirtIdent) -> bool

Returns true if var_before_opt_term(arg0, arg1) holds.

pub fn iter_var_before_opt_term( &self ) -> impl '_ + Iterator<Item = (OptTermNode, VirtIdent)>

Returns an iterator over tuples of elements satisfying the var_before_opt_term predicate.

pub fn insert_var_before_opt_term(&mut self, arg0: OptTermNode, arg1: VirtIdent)

Makes var_before_opt_term(arg0, arg1) hold.

pub fn var_before_if_atom(&self, arg0: IfAtomNode, arg1: VirtIdent) -> bool

Returns true if var_before_if_atom(arg0, arg1) holds.

pub fn iter_var_before_if_atom( &self ) -> impl '_ + Iterator<Item = (IfAtomNode, VirtIdent)>

Returns an iterator over tuples of elements satisfying the var_before_if_atom predicate.

pub fn insert_var_before_if_atom(&mut self, arg0: IfAtomNode, arg1: VirtIdent)

Makes var_before_if_atom(arg0, arg1) hold.

pub fn var_before_then_atom(&self, arg0: ThenAtomNode, arg1: VirtIdent) -> bool

Returns true if var_before_then_atom(arg0, arg1) holds.

pub fn iter_var_before_then_atom( &self ) -> impl '_ + Iterator<Item = (ThenAtomNode, VirtIdent)>

Returns an iterator over tuples of elements satisfying the var_before_then_atom predicate.

pub fn insert_var_before_then_atom( &mut self, arg0: ThenAtomNode, arg1: VirtIdent )

Makes var_before_then_atom(arg0, arg1) hold.

pub fn var_before_stmt(&self, arg0: StmtNode, arg1: VirtIdent) -> bool

Returns true if var_before_stmt(arg0, arg1) holds.

pub fn iter_var_before_stmt( &self ) -> impl '_ + Iterator<Item = (StmtNode, VirtIdent)>

Returns an iterator over tuples of elements satisfying the var_before_stmt predicate.

pub fn insert_var_before_stmt(&mut self, arg0: StmtNode, arg1: VirtIdent)

Makes var_before_stmt(arg0, arg1) hold.

pub fn var_before_stmts(&self, arg0: StmtListNode, arg1: VirtIdent) -> bool

Returns true if var_before_stmts(arg0, arg1) holds.

pub fn iter_var_before_stmts( &self ) -> impl '_ + Iterator<Item = (StmtListNode, VirtIdent)>

Returns an iterator over tuples of elements satisfying the var_before_stmts predicate.

pub fn insert_var_before_stmts(&mut self, arg0: StmtListNode, arg1: VirtIdent)

Makes var_before_stmts(arg0, arg1) hold.

pub fn var_in_term(&self, arg0: TermNode, arg1: VirtIdent) -> bool

Returns true if var_in_term(arg0, arg1) holds.

pub fn iter_var_in_term( &self ) -> impl '_ + Iterator<Item = (TermNode, VirtIdent)>

Returns an iterator over tuples of elements satisfying the var_in_term predicate.

pub fn insert_var_in_term(&mut self, arg0: TermNode, arg1: VirtIdent)

Makes var_in_term(arg0, arg1) hold.

pub fn var_in_terms(&self, arg0: TermListNode, arg1: VirtIdent) -> bool

Returns true if var_in_terms(arg0, arg1) holds.

pub fn iter_var_in_terms( &self ) -> impl '_ + Iterator<Item = (TermListNode, VirtIdent)>

Returns an iterator over tuples of elements satisfying the var_in_terms predicate.

pub fn insert_var_in_terms(&mut self, arg0: TermListNode, arg1: VirtIdent)

Makes var_in_terms(arg0, arg1) hold.

pub fn var_in_opt_term(&self, arg0: OptTermNode, arg1: VirtIdent) -> bool

Returns true if var_in_opt_term(arg0, arg1) holds.

pub fn iter_var_in_opt_term( &self ) -> impl '_ + Iterator<Item = (OptTermNode, VirtIdent)>

Returns an iterator over tuples of elements satisfying the var_in_opt_term predicate.

pub fn insert_var_in_opt_term(&mut self, arg0: OptTermNode, arg1: VirtIdent)

Makes var_in_opt_term(arg0, arg1) hold.

pub fn var_in_if_atom(&self, arg0: IfAtomNode, arg1: VirtIdent) -> bool

Returns true if var_in_if_atom(arg0, arg1) holds.

pub fn iter_var_in_if_atom( &self ) -> impl '_ + Iterator<Item = (IfAtomNode, VirtIdent)>

Returns an iterator over tuples of elements satisfying the var_in_if_atom predicate.

pub fn insert_var_in_if_atom(&mut self, arg0: IfAtomNode, arg1: VirtIdent)

Makes var_in_if_atom(arg0, arg1) hold.

pub fn var_in_then_atom(&self, arg0: ThenAtomNode, arg1: VirtIdent) -> bool

Returns true if var_in_then_atom(arg0, arg1) holds.

pub fn iter_var_in_then_atom( &self ) -> impl '_ + Iterator<Item = (ThenAtomNode, VirtIdent)>

Returns an iterator over tuples of elements satisfying the var_in_then_atom predicate.

pub fn insert_var_in_then_atom(&mut self, arg0: ThenAtomNode, arg1: VirtIdent)

Makes var_in_then_atom(arg0, arg1) hold.

pub fn var_in_stmt(&self, arg0: StmtNode, arg1: VirtIdent) -> bool

Returns true if var_in_stmt(arg0, arg1) holds.

pub fn iter_var_in_stmt( &self ) -> impl '_ + Iterator<Item = (StmtNode, VirtIdent)>

Returns an iterator over tuples of elements satisfying the var_in_stmt predicate.

pub fn insert_var_in_stmt(&mut self, arg0: StmtNode, arg1: VirtIdent)

Makes var_in_stmt(arg0, arg1) hold.

pub fn term_should_be_epic_ok(&self, arg0: TermNode) -> bool

Returns true if term_should_be_epic_ok(arg0) holds.

pub fn iter_term_should_be_epic_ok(&self) -> impl '_ + Iterator<Item = TermNode>

Returns an iterator over elements satisfying the term_should_be_epic_ok predicate.

pub fn insert_term_should_be_epic_ok(&mut self, arg0: TermNode)

Makes term_should_be_epic_ok(arg0) hold.

pub fn terms_should_be_epic_ok(&self, arg0: TermListNode) -> bool

Returns true if terms_should_be_epic_ok(arg0) holds.

pub fn iter_terms_should_be_epic_ok( &self ) -> impl '_ + Iterator<Item = TermListNode>

Returns an iterator over elements satisfying the terms_should_be_epic_ok predicate.

pub fn insert_terms_should_be_epic_ok(&mut self, arg0: TermListNode)

Makes terms_should_be_epic_ok(arg0) hold.

pub fn should_be_surjective(&self, arg0: Morphism) -> bool

Returns true if should_be_surjective(arg0) holds.

pub fn iter_should_be_surjective(&self) -> impl '_ + Iterator<Item = Morphism>

Returns an iterator over elements satisfying the should_be_surjective predicate.

pub fn insert_should_be_surjective(&mut self, arg0: Morphism)

Makes should_be_surjective(arg0) hold.

pub fn term_surjective_exempted(&self, arg0: TermNode) -> bool

Returns true if term_surjective_exempted(arg0) holds.

pub fn iter_term_surjective_exempted( &self ) -> impl '_ + Iterator<Item = TermNode>

Returns an iterator over elements satisfying the term_surjective_exempted predicate.

pub fn insert_term_surjective_exempted(&mut self, arg0: TermNode)

Makes term_surjective_exempted(arg0) hold.

pub fn terms_surjective_exempted(&self, arg0: TermListNode) -> bool

Returns true if terms_surjective_exempted(arg0) holds.

pub fn iter_terms_surjective_exempted( &self ) -> impl '_ + Iterator<Item = TermListNode>

Returns an iterator over elements satisfying the terms_surjective_exempted predicate.

pub fn insert_terms_surjective_exempted(&mut self, arg0: TermListNode)

Makes terms_surjective_exempted(arg0) hold.

pub fn el_surjective_exempted(&self, arg0: El) -> bool

Returns true if el_surjective_exempted(arg0) holds.

pub fn iter_el_surjective_exempted(&self) -> impl '_ + Iterator<Item = El>

Returns an iterator over elements satisfying the el_surjective_exempted predicate.

pub fn insert_el_surjective_exempted(&mut self, arg0: El)

Makes el_surjective_exempted(arg0) hold.

pub fn el_should_be_surjective_ok(&self, arg0: El) -> bool

Returns true if el_should_be_surjective_ok(arg0) holds.

pub fn iter_el_should_be_surjective_ok(&self) -> impl '_ + Iterator<Item = El>

Returns an iterator over elements satisfying the el_should_be_surjective_ok predicate.

pub fn insert_el_should_be_surjective_ok(&mut self, arg0: El)

Makes el_should_be_surjective_ok(arg0) hold.

pub fn el_is_surjective_ok(&self, arg0: El) -> bool

Returns true if el_is_surjective_ok(arg0) holds.

pub fn iter_el_is_surjective_ok(&self) -> impl '_ + Iterator<Item = El>

Returns an iterator over elements satisfying the el_is_surjective_ok predicate.

pub fn insert_el_is_surjective_ok(&mut self, arg0: El)

Makes el_is_surjective_ok(arg0) hold.

pub fn var_term_in_rule( &self, arg0: TermNode, arg1: Ident, arg2: RuleDeclNode ) -> bool

Returns true if var_term_in_rule(arg0, arg1, arg2) holds.

pub fn iter_var_term_in_rule( &self ) -> impl '_ + Iterator<Item = (TermNode, Ident, RuleDeclNode)>

Returns an iterator over tuples of elements satisfying the var_term_in_rule predicate.

pub fn insert_var_term_in_rule( &mut self, arg0: TermNode, arg1: Ident, arg2: RuleDeclNode )

Makes var_term_in_rule(arg0, arg1, arg2) hold.

pub fn if_after_then(&self, arg0: StmtNode) -> bool

Returns true if if_after_then(arg0) holds.

pub fn iter_if_after_then(&self) -> impl '_ + Iterator<Item = StmtNode>

Returns an iterator over elements satisfying the if_after_then predicate.

pub fn insert_if_after_then(&mut self, arg0: StmtNode)

Makes if_after_then(arg0) hold.

Trait Implementations

impl Clone for Eqlog

fn clone(&self) -> Eqlog

Returns a copy of the value.

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

Performs copy-assignment from source.

impl Debug for Eqlog

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

Formats the value using the given formatter.

impl Display for Eqlog

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

Formats the value using the given formatter.