temex 0.10.0

use crate::propform::Propform;
use crate::temex_error::TemexError;
use crate::temex_match::TemexMatch;
use crate::temex_matches::TemexMatches;
use crate::temex_trace::TemexTrace;
use regex::Captures;
use regex::Regex;
use std::str;

/// A compiled temporal expression for matching temex traces.
///
/// It can be used to search temex traces to locate matching
/// subsequences. All searching is done with an implicit `.*?`
/// at the beginning and end of an expression. To force an expression
/// to match prefixes of the trace, one may prepend the anchor `^`
/// to the expression, while to force an expression to match suffixes
/// of the trace, one may append the anchor `$` to the expression. Using
/// both anchors will attempt to match the entire trace.
///
/// Note that every boolean variable occurring in the temex pattern
/// must occur in the traces being searched. If there are extra labels
/// in the trace when attempting a search, the result will be an error.
#[derive(Clone, Debug)]
pub struct Temex {
    labels: Vec<String>,
    width: usize,
    re: regex::bytes::Regex,
    te: String,
}

/// Core temex methods.
impl Temex {
    /// Creates a new temex, which can be used repeatedly to search traces.
    ///
    /// If the temex is an invalid expression, an error is returned.
    pub fn new(te: &str) -> Result<Temex, TemexError> {
        let labels = get_all_boolean_variables(te)?;

        let raw_pattern = pattern_expansion(te, &labels)?;

        let re = regex::bytes::Regex::new(raw_pattern.as_ref())?;
        let width = labels.len() + 1;
        Ok(Temex {
            labels,
            width,
            re,
            te: te.to_owned(),
        })
    }

    /// Returns true if and only if there is a match for the temex in the provided trace.
    pub fn is_match(&self, trace: &TemexTrace) -> Result<bool, TemexError> {
        self.is_match_at(trace, 0)
    }

    /// The same as `is_match`, but the search begins at the `start` index.
    pub fn is_match_at(&self, trace: &TemexTrace, start: usize) -> Result<bool, TemexError> {
        let tnf = trace;
        self.labels_match(tnf)?;

        Ok(self
            .re
            .is_match_at(&tnf.data, self.denormalize_index(start)))
    }

    /// Returns the beginning and end indices of the leftmost-first match in the trace.
    /// Returns `None` if there is no such match.
    pub fn find(&self, trace: &TemexTrace) -> Result<Option<TemexMatch>, TemexError> {
        self.find_at(trace, 0)
    }

    /// The same as `find`, but the search begins at the `start` index.
    pub fn find_at(
        &self,
        trace: &TemexTrace,
        start: usize,
    ) -> Result<Option<TemexMatch>, TemexError> {
        let tnf = trace;
        self.labels_match(tnf)?;
        match self.re.find_at(&tnf.data, self.denormalize_index(start)) {
            Some(m) => Ok(Some(self.normalize_match(m))),
            None => Ok(None),
        }
    }

    /// Returns an iterator for each successive non-overlapping match in the trace,
    /// returning the start and end indices within the trace.
    pub fn find_iter<'r, 't>(&'r self, trace: &'t TemexTrace) -> TemexMatches<'r, 't> {
        let re_matches = self.re.find_iter(&trace.data);

        TemexMatches {
            re_matches,
            width: self.width,
        }
    }

    /// Returns the original string used to create the temex.
    pub fn as_str(&self) -> &str {
        &self.te
    }

    fn labels_match(&self, trace: &TemexTrace) -> Result<(), TemexError> {
        if self.labels != trace.labels {
            Err(TemexError::MismatchedLabels {
                temex_labels: self.labels.clone(),
                trace_labels: trace.labels.clone(),
            })
        } else {
            Ok(())
        }
    }

    fn normalize_match(&self, re: regex::bytes::Match) -> TemexMatch {
        TemexMatch::new(re.start() / self.width, re.end() / self.width)
    }

    fn denormalize_index(&self, idx: usize) -> usize {
        idx * self.width
    }
}

// Expands the propositional formulas of a temex pattern to explicit
// disjunctions of truth assignments.
fn pattern_expansion(raw_pattern: &str, labels: &Vec<String>) -> Result<String, TemexError> {
    // matches the contents of square brackets, which indicates
    // a propositional formula in temex syntax
    let propform_capture = Regex::new(r"\[([^\]]*)\]").unwrap();

    // The closure in the regex cannot return a Result, so instead it will
    // report errors by mutating an error in its environment.
    let mut err: Option<TemexError> = None;

    let pattern = propform_capture.replace_all(raw_pattern, |caps: &Captures| {
        let result = (|| {
            // caps[0] is the full match and caps[1] is the first capturing group,
            // i.e., the propform within square brackets.
            let raw_propform = &caps[1].to_owned();
            let propform = raw_propform.parse::<Propform>()?;
            let expanded = expand_propform(propform, labels)?;
            Ok(expanded)
        })();
        result.map_err(|e| err = Some(e)).unwrap_or_default()
    });

    match err {
        Some(e) => Err(e),
        None => Ok(pattern.to_string()),
    }
}

fn get_all_boolean_variables(raw_pattern: &str) -> Result<Vec<String>, TemexError> {
    // matches the contents of square brackets, which indicates
    // a propositional formula in temex syntax
    // the labeled group ("inner") is the raw propositional formula string, i.e.
    // no brackets
    let propform_capture = Regex::new(r"\[(?P<inner>[^\]]*)\]").unwrap();

    // this accumulates all boolean variables that occur in the temex pattern
    let mut boolean_variables: Vec<String> = vec![];

    for cap in propform_capture.captures_iter(raw_pattern) {
        let mut local_vars = crate::propform::get_boolean_vars(&cap["inner"])?;
        boolean_variables.append(&mut local_vars);
    }

    boolean_variables.sort_unstable();
    boolean_variables.dedup();

    Ok(boolean_variables)
}

// Only valid if s is in labels; will panic otherwise.
fn find_label(s: &str, labels: &[String]) -> usize {
    for (i, label) in labels.iter().enumerate() {
        if label == s {
            return i;
        }
    }
    unreachable!()
}

// Evaluates a propositional interpretation against a propositional formula, and
// returns true if the interpretation makes the formula true, false otherwise.
//
// Interpretation is a binary sequence (here, a sequence of ascii 0's and 1's).
//
// The index of the proposition's label is its index in the binary sequence.
fn propform_eval(prop: &Propform, labels: &Vec<String>, interp: &Vec<u8>) -> bool {
    match *prop {
        Propform::True => true,
        Propform::False => false,
        Propform::BooleanVar(ref s) => {
            let i = find_label(s, labels);
            interp[i] == b'1'
        }
        Propform::Not(ref subform) => !(propform_eval(subform, labels, interp)),
        Propform::And(ref lhs, ref rhs) => {
            propform_eval(lhs, labels, interp) && propform_eval(rhs, labels, interp)
        }
        Propform::Or(ref lhs, ref rhs) => {
            propform_eval(lhs, labels, interp) || propform_eval(rhs, labels, interp)
        }
        Propform::Nand(ref lhs, ref rhs) => {
            !(propform_eval(lhs, labels, interp) && propform_eval(rhs, labels, interp))
        }
        Propform::Nor(ref lhs, ref rhs) => {
            !(propform_eval(lhs, labels, interp) || propform_eval(rhs, labels, interp))
        }
        Propform::Xor(ref lhs, ref rhs) => {
            propform_eval(lhs, labels, interp) && !(propform_eval(rhs, labels, interp))
                || (!propform_eval(lhs, labels, interp) && propform_eval(rhs, labels, interp))
        }
    }
}

// Ensures that every propositional atom in the formula has a label.
fn propform_labels_valid(prop: &Propform, labels: &Vec<String>) -> Result<(), TemexError> {
    match *prop {
        Propform::True => Ok(()),
        Propform::False => Ok(()),
        Propform::BooleanVar(ref s) => {
            if labels.contains(s) {
                Ok(())
            } else {
                Err(TemexError::UnexpectedLabelError(s.to_owned()))
            }
        }
        Propform::Not(ref subform) => propform_labels_valid(subform, labels),
        Propform::And(ref lhs, ref rhs) => {
            propform_labels_valid(lhs, labels)?;
            propform_labels_valid(rhs, labels)
        }
        Propform::Or(ref lhs, ref rhs) => {
            propform_labels_valid(lhs, labels)?;
            propform_labels_valid(rhs, labels)
        }

        Propform::Nand(ref lhs, ref rhs) => {
            propform_labels_valid(lhs, labels)?;
            propform_labels_valid(rhs, labels)
        }
        Propform::Nor(ref lhs, ref rhs) => {
            propform_labels_valid(lhs, labels)?;
            propform_labels_valid(rhs, labels)
        }
        Propform::Xor(ref lhs, ref rhs) => {
            propform_labels_valid(lhs, labels)?;
            propform_labels_valid(rhs, labels)
        }
    }
}
// converts integer to binary representation as sequence of ascii 0's and 1's
fn int_to_charvec(i: u32, len: usize) -> Vec<u8> {
    // binary string of at least len length, prepended with zeros if necessary
    format!("{:0len$b}", i).as_bytes().to_owned()
}

fn propform_to_satisfying_interpretations(
    prop: Propform,
    labels: &Vec<String>,
) -> Result<Vec<String>, TemexError> {
    propform_labels_valid(&prop, labels)?;
    let len = labels.len();
    // a bitstring of length n has 2^n values
    let interps: Vec<String> = (0..2_u32.pow(len as u32))
        // convert each such value to a bitvector representation, which
        // is treated as a propositional interpretation
        // Vec<u8> is used because it allows indexing, while Strings do not
        .map(|x| int_to_charvec(x, len))
        // only keep the interpretations that satisfy the formula
        .filter(|x| propform_eval(&prop, labels, x))
        // convert to String (x is a Vec<u8> consisting entirely of b'0' and b'1',
        // so it is safe to unwrap)
        .map(|x| String::from_utf8(x).unwrap())
        .collect();

    Ok(interps)
}

// Expands a propositional formula into a disjunction of its satisfying interpretations,
// in a format suitable for embedding within a regex.
fn expand_propform(prop: Propform, labels: &Vec<String>) -> Result<String, TemexError> {
    let interps: Vec<String> = propform_to_satisfying_interpretations(prop, labels)?
        .into_iter()
        .collect();
    if interps.is_empty() {
        // the formula is unsatisfiable
        // return a trace-element-length string that will not match any trace element
        return Ok(vec!['F'; labels.len() + 1].into_iter().collect());
    }
    // ?: ensures that the expansion will be a noncapturing group, so the expansion will
    // not clobber the user's capturing groups
    let mut result = "(?:".to_string();
    // interpretations are delimited by newlines, and the regex alternation operator '|'
    // is equivalent to disjunction in this context
    result.push_str(&interps.join("\n|"));
    // one more newline is added to the last interpretation, before the closing paren
    result.push_str("\n)");
    Ok(result)
}

#[cfg(test)]
mod tests {
    use super::*;

    const ONE_VAR: &str = "p1";
    const ONE_VAR_NEG: &str = "not p1";
    const SIMPLE_CONJUNCT: &str = "p1 and p2";
    const SIMPLE_DISJUNCT: &str = "p1 or p2";

    #[test]
    fn expand_propform_works() {
        let prop_1var = ONE_VAR.to_string().parse::<Propform>().unwrap();
        let prop_1var_neg = ONE_VAR_NEG.to_string().parse::<Propform>().unwrap();
        let prop_simple_conjunct = SIMPLE_CONJUNCT.to_string().parse::<Propform>().unwrap();
        let prop_simple_disjunct = SIMPLE_DISJUNCT.to_string().parse::<Propform>().unwrap();

        let labels = vec!["p1".to_owned(), "p2".to_owned(), "p3".to_owned()];

        assert_eq!(
            expand_propform(prop_1var, &labels).unwrap(),
            "(?:100\n|101\n|110\n|111\n)".to_string()
        );
        assert_eq!(
            expand_propform(prop_1var_neg, &labels).unwrap(),
            "(?:000\n|001\n|010\n|011\n)".to_string()
        );
        assert_eq!(
            expand_propform(prop_simple_conjunct, &labels).unwrap(),
            "(?:110\n|111\n)".to_string()
        );
        assert_eq!(
            expand_propform(prop_simple_disjunct, &labels).unwrap(),
            "(?:010\n|011\n|100\n|101\n|110\n|111\n)"
        );
    }

    #[test]
    fn propform_eval_works() {
        let prop_1var = ONE_VAR.to_string().parse::<Propform>().unwrap();
        let prop_1var_neg = ONE_VAR_NEG.to_string().parse::<Propform>().unwrap();
        let prop_simple_conjunct = SIMPLE_CONJUNCT.to_string().parse::<Propform>().unwrap();
        let prop_simple_disjunct = SIMPLE_DISJUNCT.to_string().parse::<Propform>().unwrap();

        let labels = vec!["p1".to_owned(), "p2".to_owned(), "p3".to_owned()];

        let p_true_interp = [b'1', b'1', b'1'];
        let p_false_interp = [b'0', b'1', b'0'];
        let simple_disjunct_false = [b'0', b'0', b'0'];

        assert!(propform_eval(&prop_1var, &labels, &p_true_interp.to_vec()));
        assert!(!propform_eval(
            &prop_1var,
            &labels,
            &p_false_interp.to_vec()
        ));
        assert!(!propform_eval(
            &prop_1var_neg,
            &labels,
            &p_true_interp.to_vec()
        ));
        assert!(propform_eval(
            &prop_1var_neg,
            &labels,
            &p_false_interp.to_vec()
        ));
        assert!(propform_eval(
            &prop_simple_conjunct,
            &labels,
            &p_true_interp.to_vec()
        ));
        assert!(!propform_eval(
            &prop_simple_conjunct,
            &labels,
            &p_false_interp.to_vec()
        ));
        assert!(propform_eval(
            &prop_simple_disjunct,
            &labels,
            &p_false_interp.to_vec()
        ));
        assert!(!propform_eval(
            &prop_simple_disjunct,
            &labels,
            &simple_disjunct_false.to_vec()
        ));
    }

    #[test]
    fn pattern_expansion_works() {
        let labels = vec!["p1".to_owned()];
        let p1_star = "[p1]*".to_string();
        let p1_paren_star = "([p1])*".to_string();

        let p1_concat = "[p1][p1][p1]".to_string();

        assert_eq!(pattern_expansion(&p1_star, &labels).unwrap(), "(?:1\n)*");
        assert_eq!(
            pattern_expansion(&p1_paren_star, &labels).unwrap(),
            "((?:1\n))*"
        );

        assert_eq!(
            pattern_expansion(&p1_concat, &labels).unwrap(),
            "(?:1\n)(?:1\n)(?:1\n)"
        );
    }
}