[−][src]Struct ascesis::sat::Formula
Methods
impl Formula
[src]
pub fn new(ctx: &Arc<Mutex<Context>>) -> Formula
[src]
pub fn add_antiport(&mut self, port_id: PortID) -> Result<(), AcesError>
[src]
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>
[src]
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>
[src]
&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>
[src]
&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>
[src]
&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>
[src]
&mut self,
harc_id: NonZeroUsize,
coharc_ids: Vec<Vec<NonZeroUsize>>
) -> Result<(), AcesError>
Trait Implementations
impl Debug for Formula
[src]
impl Display for Formula
[src]
impl Eq for Formula
[src]
impl PartialEq<Formula> for Formula
[src]
Auto Trait Implementations
impl RefUnwindSafe for Formula
impl Send for Formula
impl Sync for Formula
impl Unpin for Formula
impl UnwindSafe for Formula
Blanket Implementations
impl<T> Any for T where
T: 'static + ?Sized,
[src]
T: 'static + ?Sized,
impl<T> Borrow<T> for T where
T: ?Sized,
[src]
T: ?Sized,
impl<T> BorrowMut<T> for T where
T: ?Sized,
[src]
T: ?Sized,
fn borrow_mut(&mut self) -> &mut T
[src]
impl<T> From<T> for T
[src]
impl<Reference, Outer, OuterFieldType, Inner> HasPart<Nested<Outer, Inner>> for Reference where
Inner: Part,
Outer: Part<PartType = Field<OuterFieldType>>,
OuterFieldType: HasPart<Inner, RawTarget = OuterFieldType> + PartialRefTarget + ?Sized,
Reference: HasPart<Outer> + ?Sized,
Inner: Part,
Outer: Part<PartType = Field<OuterFieldType>>,
OuterFieldType: HasPart<Inner, RawTarget = OuterFieldType> + PartialRefTarget + ?Sized,
Reference: HasPart<Outer> + ?Sized,
unsafe fn part_ptr(
ptr: *const <Reference as PartialRefTarget>::RawTarget
) -> <<Inner as Part>::PartType as PartType>::Ptr
ptr: *const <Reference as PartialRefTarget>::RawTarget
) -> <<Inner as Part>::PartType as PartType>::Ptr
unsafe fn part_ptr_mut(
ptr: *mut <Reference as PartialRefTarget>::RawTarget
) -> <<Inner as Part>::PartType as PartType>::PtrMut
ptr: *mut <Reference as PartialRefTarget>::RawTarget
) -> <<Inner as Part>::PartType as PartType>::PtrMut
impl<T, U> Into<U> for T where
U: From<T>,
[src]
U: From<T>,
impl<T> ToString for T where
T: Display + ?Sized,
[src]
T: Display + ?Sized,
impl<T, U> TryFrom<U> for T where
U: Into<T>,
[src]
U: Into<T>,
type Error = Infallible
The type returned in the event of a conversion error.
fn try_from(value: U) -> Result<T, <T as TryFrom<U>>::Error>
[src]
impl<T, U> TryInto<U> for T where
U: TryFrom<T>,
[src]
U: TryFrom<T>,
type Error = <U as TryFrom<T>>::Error
The type returned in the event of a conversion error.
fn try_into(self) -> Result<U, <U as TryFrom<T>>::Error>
[src]
impl<V, T> VZip<V> for T where
V: MultiLane<T>,
V: MultiLane<T>,