Struct DisjunctionTargetConfig 

pub struct DisjunctionTargetConfig {
    property_name: String,
    targets: Vec<TargetConfig>,
}

Disjunction over multiple target configurations

This type represents a disjunction of TargetConfig

Fields

property_name: String

Name of the property this specification has been derived from

targets: Vec<TargetConfig>

Sets of target configurations

Implementations

impl DisjunctionTargetConfig

fn new_empty(name: String) -> Self

Create a new disjunction without any disjuncts

fn new_with_single_disjunct(name: String, u: TargetConfig) -> Self

Create a disjunction only containing a single disjunct

pub fn new_from_targets<I: IntoIterator<Item = TargetConfig>>( name: String, disj: I, ) -> Self

Create a disjunction from the given disjuncts

pub fn contains_reachability_constraint(&self) -> bool

Check whether the disjunction contains a reachability constraint

A reachability constraint requires at least one location to be empty.

pub fn get_locations_appearing(&self) -> HashSet<&Location>

Get the locations appearing in the specifications

pub fn name(&self) -> &str

Get the name of the property this target has been derived from

pub fn get_target_configs(&self) -> impl Iterator<Item = &TargetConfig>

Get the included target configurations

Trait Implementations

impl And for DisjunctionTargetConfig

fn and(self, other: DisjunctionTargetConfig) -> DisjunctionTargetConfig

Get the conjunction of self and other

impl Clone for DisjunctionTargetConfig

fn clone(&self) -> DisjunctionTargetConfig

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl Debug for DisjunctionTargetConfig

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

Formats the value using the given formatter.

impl Display for DisjunctionTargetConfig

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

Formats the value using the given formatter.

impl<C: SMTVariableContext<Location> + SMTVariableContext<Variable> + SMTVariableContext<Parameter>> EncodeToSMT<DisjunctionTargetConfig, C> for DisjunctionTargetConfig

fn encode_to_smt_with_ctx( &self, solver: &SMTSolver, ctx: &C, ) -> Result<SMTExpr, SMTSolverError>

Encode the type into an SMT expression

impl Or for DisjunctionTargetConfig

fn or(self, other: Self) -> Self

Get the disjunction of self and other

impl PartialEq for DisjunctionTargetConfig

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

Tests for self and other values to be equal, and is used by ==.

fn ne(&self, other: &Rhs) -> bool

Tests for !=. The default implementation is almost always sufficient, and should not be overridden without very good reason.

impl TargetSpec for DisjunctionTargetConfig

fn get_locations_in_target(&self) -> impl IntoIterator<Item = &Location>

Get the locations that appear in the target

fn get_variable_constraint( &self, ) -> impl IntoIterator<Item = &LIAVariableConstraint>

Get the variable constraints that appear in target

impl StructuralPartialEq for DisjunctionTargetConfig