Struct ascesis::sat::Formula

pub struct Formula { /* fields omitted */ }

Methods

impl Formula

pub fn new(ctx: &Arc<Mutex<Context>>) -> Formula

pub fn add_antiport(&mut self, port_id: PortID) -> Result<(), AcesError>

Adds an antiport rule to this Formula.

This clause constrains nodes to a single part of a firing component, source or sink, so that the induced graph of any firing component is bipartite. The Formula should contain one such clause for each internal node of the c-e structure under analysis.

pub fn add_link_coherence(&mut self, link_id: LinkID) -> Result<(), AcesError>

Adds a link coherence rule to this Formula.

This firing rule consists of two clauses which are added in order to maintain link coherence, so that any firing component of a c-e structure is itself a proper c-e structure. The Formula should contain one such rule for each link of the c-e structure under analysis.

Returns an error if link_id doesn't identify any Link in the Context of this Formula.

pub fn add_polynomial(
    &mut self,
    port_id: PortID,
    poly: &Polynomial<LinkID>
) -> Result<(), AcesError>

Adds a polynomial rule to this formula.

pub fn add_antiharcs(
    &mut self,
    harc_ids: &[NonZeroUsize],
    antiharc_ids: &[NonZeroUsize]
) -> Result<(), AcesError>

Adds an antiharc rule to this formula.

This set of clauses constrains nodes to a single part of a firing component, source or sink, so that the induced graph of any firing component is bipartite. The Formula should contain one clause for each fork-join pair of each internal node of the c-e structure under analysis.

pub fn add_sideharcs(
    &mut self,
    sideharc_ids: &[NonZeroUsize]
) -> Result<(), AcesError>

Adds a sideharc rule to this formula.

This rule enforces monomiality of firing components.

pub fn add_coharcs(
    &mut self,
    harc_id: NonZeroUsize,
    coharc_ids: Vec<Vec<NonZeroUsize>>
) -> Result<(), AcesError>

Trait Implementations

impl Debug for Formula

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

Formats the value using the given formatter.

impl Display for Formula

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

Formats the value using the given formatter.

impl Eq for Formula

impl PartialEq<Formula> for Formula

fn eq(&self, other: &Formula) -> bool

This method tests for self and other values to be equal, and is used by ==.

#[must_use] fn ne(&self, other: &Rhs) -> bool

This method tests for !=.