Skip to content

Commit

Permalink
Add exclusive property to schema
Browse files Browse the repository at this point in the history
- Exclusive facts are facts which have only one instance in the data.
  Adding multiple facts with the same label results in an error.
- Remove add_exclusive_fact method. There may be a use case to
  dynamically determine if a fact is exclusive, but it can be done with
  existing methods.
  • Loading branch information
bluk committed Sep 8, 2023
1 parent 00ea960 commit ba4b09a
Show file tree
Hide file tree
Showing 3 changed files with 58 additions and 43 deletions.
22 changes: 15 additions & 7 deletions src/facts.rs
Original file line number Diff line number Diff line change
Expand Up @@ -17,8 +17,9 @@ use std::{error, vec::Vec};
use generic_array::{ArrayLength, GenericArray};

use crate::{
error::ErrorKind,
values::{self, BytesId, ConstantId},
Constant, Section, SectionMut,
Constant, Error, Section, SectionMut,
};

/// An interned predicate reference.
Expand Down Expand Up @@ -184,7 +185,8 @@ pub(crate) fn push<N: ArrayLength<ConstantId>>(
mut facts: SectionMut<'_>,
pred: PredicateId,
constants: GenericArray<ConstantId, N>,
) {
is_exclusive: bool,
) -> Result<bool, Error> {
assert!(!constants.is_empty());

facts.init(&SECTION_INIT);
Expand Down Expand Up @@ -234,7 +236,7 @@ pub(crate) fn push<N: ArrayLength<ConstantId>>(

if is_equal {
// Found an equivalent term already
return;
return Ok(false);
}

len = len.checked_sub(bytes_len).unwrap();
Expand All @@ -244,9 +246,13 @@ pub(crate) fn push<N: ArrayLength<ConstantId>>(
let len = u16::from_be_bytes([
facts.data[pred_start_pos + 2],
facts.data[pred_start_pos + 3],
])
.checked_add(u16::try_from(bytes_len).unwrap())
.unwrap();
]);

if is_exclusive && len > 0 {
return Err(Error::with_kind(ErrorKind::ExistingFact));
}

let len = len.checked_add(u16::try_from(bytes_len).unwrap()).unwrap();
let len_bytes = len.to_be_bytes();
facts.data[pred_start_pos + 2] = len_bytes[0];
facts.data[pred_start_pos + 3] = len_bytes[1];
Expand All @@ -264,7 +270,7 @@ pub(crate) fn push<N: ArrayLength<ConstantId>>(
facts.end += bytes_len;
facts.update_len();

return;
return Ok(true);
}

debug_assert_eq!(pos, facts.end);
Expand All @@ -290,6 +296,8 @@ pub(crate) fn push<N: ArrayLength<ConstantId>>(
);
facts.end += bytes_len;
facts.update_len();

Ok(true)
}

/// Errors returned when using [`FactTerms`] methods.
Expand Down
50 changes: 16 additions & 34 deletions src/lib.rs
Original file line number Diff line number Diff line change
Expand Up @@ -292,12 +292,15 @@ impl<'s> Passdata<'s> {
))
}

/// Add a fact explicitly.
/// Add a fact explicitly. Returns true if the fact was added; false if it already existed.
///
/// # Errors
///
/// Returns an error if the values do not match the expected types for the predicate.
pub fn add_fact<'a, T>(&mut self, predicate: &str, constants: T) -> Result<()>
///
/// Returns an error if the fact was set as exclusive in the schema and
/// there is an existing non-equal fact.
pub fn add_fact<'a, T>(&mut self, predicate: &str, constants: T) -> Result<bool>
where
T: IntoArray<Constant<'a>>,
<T as IntoArray<Constant<'a>>>::Length: ArrayLength<ConstantTy>,
Expand Down Expand Up @@ -325,32 +328,9 @@ impl<'s> Passdata<'s> {
};
}

facts::push(self.section_mut(SectionId::Edb), pred, v);
let is_exclusive = self.schema.is_exclusive(predicate);

Ok(())
}

/// Add an exclusive fact explicitly.
///
/// # Errors
///
/// Returns an error if the values do not match the expected types for the predicate.
///
/// If the fact already has been added, then an error is also returned.
pub fn add_exclusive_fact<'a, T>(&mut self, predicate: &str, constants: T) -> Result<()>
where
T: IntoArray<Constant<'a>>,
T::Length: ArrayLength<ExpectedConstantTy>,
<T as IntoArray<Constant<'a>>>::Length: ArrayLength<ConstantTy>,
<T as IntoArray<Constant<'a>>>::Length: ArrayLength<ConstantId>,
{
let constants = constants.into_array();

if self.edb_iter(predicate)?.next().is_some() {
return Err(Error::with_kind(ErrorKind::ExistingFact));
}

self.add_fact(predicate, constants)
facts::push(self.section_mut(SectionId::Edb), pred, v, is_exclusive)
}

/// Query for an explictly declared fact.
Expand Down Expand Up @@ -785,23 +765,25 @@ mod tests {
fn add_exclusive_fact() -> Result<()> {
let mut schema = Schema::new();
schema.insert_tys("a", &[ConstantTy::Bool])?;
schema.set_exclusive("a")?;
schema.insert_tys("b", &[ConstantTy::Bytes, ConstantTy::Num, ConstantTy::Bool])?;
schema.set_exclusive("b")?;

let mut data = Passdata::with_schema(&schema);

data.add_exclusive_fact("a", true)?;
assert_eq!(data.add_fact("a", true), Ok(true));
assert_eq!(data.add_fact("a", true), Ok(false));
assert_eq!(
data.add_exclusive_fact("a", true),
data.add_fact("a", false),
Err(Error::with_kind(ErrorKind::ExistingFact))
);

assert_eq!(
data.add_exclusive_fact("a", false),
Err(Error::with_kind(ErrorKind::ExistingFact))
data.add_fact("b", ([1, 2, 3].as_slice(), 456, false)),
Ok(true)
);

data.add_exclusive_fact("b", ([1, 2, 3].as_slice(), 456, false))?;
assert_eq!(
data.add_exclusive_fact("b", ([].as_slice(), 0, true)),
data.add_fact("b", ([].as_slice(), 0, true)),
Err(Error::with_kind(ErrorKind::ExistingFact))
);

Expand Down
29 changes: 27 additions & 2 deletions src/schema.rs
Original file line number Diff line number Diff line change
Expand Up @@ -3,9 +3,9 @@
//! Schemas are expected to be constant.

#[cfg(all(feature = "alloc", not(feature = "std")))]
use alloc::collections::BTreeMap;
use alloc::collections::{BTreeMap, BTreeSet};
#[cfg(feature = "std")]
use std::collections::BTreeMap;
use std::collections::{BTreeMap, BTreeSet};

use crate::{
error::{Error, ErrorKind, Result},
Expand Down Expand Up @@ -56,6 +56,7 @@ impl ConstantTy {
#[derive(Debug, Default, Clone, PartialEq, Eq)]
pub struct Schema<'a> {
tys: BTreeMap<&'a str, &'a [ConstantTy]>,
exclusive: BTreeSet<&'a str>,
}

impl<'a> Schema<'a> {
Expand All @@ -64,6 +65,7 @@ impl<'a> Schema<'a> {
pub const fn new() -> Self {
Self {
tys: BTreeMap::new(),
exclusive: BTreeSet::new(),
}
}

Expand Down Expand Up @@ -96,6 +98,29 @@ impl<'a> Schema<'a> {
Ok(())
}

/// Returns true if the exclusive bit is set for a predicate.
#[must_use]
pub fn is_exclusive(&self, predicate: &str) -> bool {
self.exclusive.contains(predicate)
}

/// Sets a predicate to be an exclusive fact.
///
/// At most one fact can be added with the given predicate.
///
/// # Errors
///
/// If the predicate's schema types does not exist
pub fn set_exclusive(&mut self, predicate: &'a str) -> Result<()> {
if !self.tys.contains_key(predicate) {
return Err(Error::with_kind(ErrorKind::MismatchSchemaTys));
}

self.exclusive.insert(predicate);

Ok(())
}

pub(crate) fn validate_tys(&self, predicate: &'a str, actual_tys: &[ConstantTy]) -> Result<()> {
let Some(tys) = self.get_tys(predicate) else {
return Err(Error::with_kind(ErrorKind::UnknownPredicate));
Expand Down

0 comments on commit ba4b09a

Please sign in to comment.