Struct biodivine_sketchbook::sketchbook::properties::static_props::_first_order_formula::FirstOrderFormula
source · pub struct FirstOrderFormula {
tree: FolTreeNode,
}
Expand description
A typesafe representation of a FOL formula used in static properties.
Fields§
§tree: FolTreeNode
Implementations§
source§impl FirstOrderFormula
impl FirstOrderFormula
Creating first-order formulas.
sourcepub fn try_from_str(formula: &str) -> Result<FirstOrderFormula, String>
pub fn try_from_str(formula: &str) -> Result<FirstOrderFormula, String>
Parse FirstOrderFormula
instance directly from a string, which must be in a
correct format.
source§impl FirstOrderFormula
impl FirstOrderFormula
Editing first-order formulas.
source§impl FirstOrderFormula
impl FirstOrderFormula
Observing first-order formulas.
source§impl FirstOrderFormula
impl FirstOrderFormula
Static methods (to check validity of formula strings).
sourcepub fn check_pure_syntax(formula: &str) -> Result<(), String>
pub fn check_pure_syntax(formula: &str) -> Result<(), String>
Check if the formula is correctly formed based on predefined FOL syntactic rules.
sourcepub fn check_syntax_with_model(
formula: &str,
model: &ModelState,
) -> Result<(), String>
pub fn check_syntax_with_model( formula: &str, model: &ModelState, ) -> Result<(), String>
Check if the formula is correctly formed based on predefined FO syntactic rules, and also whether formula respects the model (function symbols must be valid entities in the model and so on).
Trait Implementations§
source§impl Clone for FirstOrderFormula
impl Clone for FirstOrderFormula
source§fn clone(&self) -> FirstOrderFormula
fn clone(&self) -> FirstOrderFormula
Returns a copy of the value. Read more
1.0.0 · source§fn clone_from(&mut self, source: &Self)
fn clone_from(&mut self, source: &Self)
Performs copy-assignment from
source
. Read moresource§impl Debug for FirstOrderFormula
impl Debug for FirstOrderFormula
source§impl<'de> Deserialize<'de> for FirstOrderFormula
impl<'de> Deserialize<'de> for FirstOrderFormula
source§fn deserialize<__D>(__deserializer: __D) -> Result<Self, __D::Error>where
__D: Deserializer<'de>,
fn deserialize<__D>(__deserializer: __D) -> Result<Self, __D::Error>where
__D: Deserializer<'de>,
Deserialize this value from the given Serde deserializer. Read more
source§impl Display for FirstOrderFormula
impl Display for FirstOrderFormula
source§impl Hash for FirstOrderFormula
impl Hash for FirstOrderFormula
source§impl PartialEq for FirstOrderFormula
impl PartialEq for FirstOrderFormula
source§impl Serialize for FirstOrderFormula
impl Serialize for FirstOrderFormula
impl Eq for FirstOrderFormula
impl StructuralPartialEq for FirstOrderFormula
Auto Trait Implementations§
impl Freeze for FirstOrderFormula
impl RefUnwindSafe for FirstOrderFormula
impl Send for FirstOrderFormula
impl Sync for FirstOrderFormula
impl Unpin for FirstOrderFormula
impl UnwindSafe for FirstOrderFormula
Blanket Implementations§
source§impl<T> BorrowMut<T> for Twhere
T: ?Sized,
impl<T> BorrowMut<T> for Twhere
T: ?Sized,
source§fn borrow_mut(&mut self) -> &mut T
fn borrow_mut(&mut self) -> &mut T
Mutably borrows from an owned value. Read more
source§impl<T> CloneToUninit for Twhere
T: Clone,
impl<T> CloneToUninit for Twhere
T: Clone,
source§unsafe fn clone_to_uninit(&self, dst: *mut T)
unsafe fn clone_to_uninit(&self, dst: *mut T)
🔬This is a nightly-only experimental API. (
clone_to_uninit
)§impl<'de, D, R> CommandArg<'de, R> for Dwhere
D: Deserialize<'de>,
R: Runtime,
impl<'de, D, R> CommandArg<'de, R> for Dwhere
D: Deserialize<'de>,
R: Runtime,
§fn from_command(command: CommandItem<'de, R>) -> Result<D, InvokeError>
fn from_command(command: CommandItem<'de, R>) -> Result<D, InvokeError>
§impl<Q, K> Equivalent<K> for Q
impl<Q, K> Equivalent<K> for Q
§fn equivalent(&self, key: &K) -> bool
fn equivalent(&self, key: &K) -> bool
Checks if this value is equivalent to the given key. Read more
§impl<Q, K> Equivalent<K> for Q
impl<Q, K> Equivalent<K> for Q
§fn equivalent(&self, key: &K) -> bool
fn equivalent(&self, key: &K) -> bool
Compare self to
key
and return true
if they are equal.source§impl<Q, K> Equivalent<K> for Q
impl<Q, K> Equivalent<K> for Q
source§fn equivalent(&self, key: &K) -> bool
fn equivalent(&self, key: &K) -> bool
Compare self to
key
and return true
if they are equal.