From 55c7bfc302ec3058a662adc707a91b0755d69b85 Mon Sep 17 00:00:00 2001 From: Ziyang Hu Date: Sat, 7 May 2022 16:58:13 +0800 Subject: [PATCH] CNF transform --- src/db/cnf_transform.rs | 99 ++++++++++++++++++++++++++++++++++++----- src/db/eval.rs | 15 ++++++- 2 files changed, 102 insertions(+), 12 deletions(-) diff --git a/src/db/cnf_transform.rs b/src/db/cnf_transform.rs index 579a64b7..fab72d43 100644 --- a/src/db/cnf_transform.rs +++ b/src/db/cnf_transform.rs @@ -26,17 +26,66 @@ fn do_cnf_transform(val: Value) -> (bool, Value) { } fn cnf_transform_or(args: Vec) -> (bool, Value) { - todo!() + let mut changed = false; + let mut collected = Vec::with_capacity(args.len()); + let mut to_and = None; + for v in args { + let (vc, v) = do_cnf_transform(v); + changed |= vc; + if let Value::Apply(op, args) = v { + match op.as_ref() { + value::OP_OR => { + changed = true; + collected.extend(args) + } + value::OP_AND => { + if to_and == None { + changed = true; + to_and = Some(args); + } else { + collected.push(Value::Apply(op, args)) + } + } + _ => collected.push(Value::Apply(op, args)) + } + } else { + collected.push(v); + } + } + if let Some(to_and) = to_and { + let args = to_and.into_iter().map(|v| { + let mut to_or = collected.clone(); + to_or.push(v); + Value::Apply(value::OP_OR.into(), to_or) + }).collect(); + (true, Value::Apply(value::OP_AND.into(), args)) + } else if collected.is_empty() { + (true, true.into()) + } else if collected.len() == 1 { + (true, collected.pop().unwrap()) + } else { + (changed, Value::Apply(value::OP_OR.into(), collected)) + } } fn cnf_transform_and(args: Vec) -> (bool, Value) { let mut changed = false; let mut collected = Vec::with_capacity(args.len()); + for v in args { + let (vc, v) = do_cnf_transform(v); + changed |= vc; if let Value::Apply(op, args) = v { match op.as_ref() { - value::OP_AND => todo!(), - _ => todo!() + value::OP_AND => { + changed = true; + for v in args { + collected.push(v); + } + } + _ => { + collected.push(Value::Apply(op, args)); + } } } else { collected.push(v); @@ -44,6 +93,8 @@ fn cnf_transform_and(args: Vec) -> (bool, Value) { } if collected.is_empty() { (true, true.into()) + } else if collected.len() == 1 { + (true, collected.pop().unwrap()) } else { (changed, Value::Apply(value::OP_AND.into(), collected)) } @@ -51,23 +102,49 @@ fn cnf_transform_and(args: Vec) -> (bool, Value) { fn cnf_transform_negate(arg: Value) -> (bool, Value) { if let Value::Apply(op, args) = arg { + let mut new_args = Vec::with_capacity(args.len()); + let mut changed = false; + for v in args { + let (vc, v) = do_cnf_transform(v); + changed |= vc; + new_args.push(v); + } match op.as_ref() { - value::OP_OR => (true, Value::Apply(value::OP_AND.into(), args.into_iter().map(|v| { + value::OP_OR => (true, Value::Apply(value::OP_AND.into(), new_args.into_iter().map(|v| { let (_, v) = do_cnf_transform(v); Value::Apply(value::OP_NEGATE.into(), vec![v]) }).collect())), - value::OP_AND => (true, Value::Apply(value::OP_OR.into(), args.into_iter().map(|v| { + value::OP_AND => (true, Value::Apply(value::OP_OR.into(), new_args.into_iter().map(|v| { let (_, v) = do_cnf_transform(v); Value::Apply(value::OP_NEGATE.into(), vec![v]) }).collect())), value::OP_NEGATE => { - let (_, v) = do_cnf_transform(args.into_iter().next().unwrap()); - (true, v) - }, - _ => (false, Value::Apply(value::OP_NEGATE.into(), vec![Value::Apply(op, args)])) + (true, new_args.into_iter().next().unwrap()) + } + _ => (changed, Value::Apply(value::OP_NEGATE.into(), vec![Value::Apply(op, new_args)])) } } else { - let (transformed, arg) = do_cnf_transform(arg); - (transformed, Value::Apply(value::OP_NEGATE.into(), vec![arg])) + (false, Value::Apply(value::OP_NEGATE.into(), vec![arg])) + } +} + + +#[cfg(test)] +mod tests { + use crate::db::cnf_transform::cnf_transform; + use crate::relation::value::Value; + use crate::error::Result; + + #[test] + fn test_cnf() -> Result<()> { + for s in ["a", "!a", "!!a", "!!!a", "!(b || c)", "a && (b && c)", "a && b || c", "a || b && c && d", + "a && (b || d && e)", "a && !b || c && !!d || !!!e && f", "(a || !b || !c) && (!d || e || f)", "(a || b) && c", "a || b"] { + let v = Value::parse_str(s)?; + println!("{}", v); + let v2 = cnf_transform(v); + println!("=> {}", v2); + } + + Ok(()) } } \ No newline at end of file diff --git a/src/db/eval.rs b/src/db/eval.rs index a7ce137a..eae46d20 100644 --- a/src/db/eval.rs +++ b/src/db/eval.rs @@ -2,6 +2,7 @@ use std::borrow::Cow; use std::cmp::{max, min}; use std::collections::{BTreeMap}; use cozorocks::SlicePtr; +use crate::db::cnf_transform::cnf_transform; use crate::db::engine::{Session}; use crate::db::plan::AccessorMap; use crate::relation::value::{Value}; @@ -96,11 +97,23 @@ impl<'s> Session<'s> { } } Value::EndSentinel => { - return Err(LogicError(format!("Encountered end sentinel"))); + return Err(LogicError("Encountered end sentinel".to_string())); } }; Ok(res) } + pub fn partial_cnf_eval<'a>(&self, mut value: Value<'a>, params: &BTreeMap>, + table_bindings: &AccessorMap) -> Result<(bool, Value<'a>)> { + loop { + let (ev, new_v) = self.partial_eval(value.clone(), params, table_bindings)?; + let new_v = cnf_transform(new_v.clone()); + if new_v == value { + return Ok((ev, new_v)) + } else { + value = new_v + } + } + } pub fn partial_eval<'a>(&self, value: Value<'a>, params: &BTreeMap>, table_bindings: &AccessorMap) -> Result<(bool, Value<'a>)> { match value {