Struct ChcSystem 

pub struct ChcSystem { /* private fields */ }

A complete CHC system containing predicates and rules

Implementations

impl ChcSystem

pub fn new() -> Self

Create a new empty CHC system

pub fn declare_predicate( &mut self, name: impl Into<String>, params: impl IntoIterator<Item = SortId>, ) -> PredId

Declare a new predicate

pub fn get_predicate(&self, id: PredId) -> Option<&Predicate>

Get a predicate by ID

pub fn get_predicate_by_name(&self, name: &str) -> Option<&Predicate>

Get a predicate by name

pub fn get_predicate_id(&self, name: &str) -> Option<PredId>

Get a predicate ID by name

pub fn add_rule( &mut self, vars: impl IntoIterator<Item = (String, SortId)>, body: RuleBody, head: RuleHead, name: Option<String>, ) -> RuleId

Add a rule to the system

pub fn add_init_rule( &mut self, vars: impl IntoIterator<Item = (String, SortId)>, constraint: TermId, head_pred: PredId, head_args: impl IntoIterator<Item = TermId>, ) -> RuleId

Add a simple init rule: constraint => P(args)

pub fn add_transition_rule( &mut self, vars: impl IntoIterator<Item = (String, SortId)>, body_preds: impl IntoIterator<Item = PredicateApp>, constraint: TermId, head_pred: PredId, head_args: impl IntoIterator<Item = TermId>, ) -> RuleId

Add a transition rule: P1(args1) /\ ... /\ constraint => P(args)

pub fn add_query( &mut self, vars: impl IntoIterator<Item = (String, SortId)>, body_preds: impl IntoIterator<Item = PredicateApp>, constraint: TermId, ) -> RuleId

Add a query rule: P(args) /\ constraint => false

pub fn get_rule(&self, id: RuleId) -> Option<&Rule>

Get a rule by ID

pub fn rules(&self) -> impl Iterator<Item = &Rule>

Get all rules

pub fn predicates(&self) -> impl Iterator<Item = &Predicate>

Get all predicates

pub fn queries(&self) -> impl Iterator<Item = &Rule>

Get query rules

pub fn entries(&self) -> impl Iterator<Item = &Rule>

Get entry rules (init rules)

pub fn rules_by_head(&self, pred: PredId) -> impl Iterator<Item = &Rule>

Get rules with a given head predicate

pub fn rules_using(&self, pred: PredId) -> impl Iterator<Item = &Rule>

Get rules that use a predicate in the body

pub fn num_predicates(&self) -> usize

Get the number of predicates

pub fn num_rules(&self) -> usize

Get the number of rules

pub fn is_empty(&self) -> bool

Check if the system is empty

pub fn topological_order(&self) -> Option<Vec<PredId>>

Get predicates in topological order (if acyclic)

Trait Implementations

impl Debug for ChcSystem

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

Formats the value using the given formatter.

impl Default for ChcSystem

fn default() -> Self

Returns the “default value” for a type.