fluidB
/
fluidb
1
0
Fork 0
Code Pull Requests Activity

stratified semi-naive

Browse Source
main
Ziyang Hu 2 years ago
parent 61172da6c5
commit 79b1f66ae4
4 changed files with 95 additions and 32 deletions
Show Stats Download Patch File Download Diff File

2
README.md
Unescape Escape View File

@ -3,7 +3,7 @@
* [x] predicates
* [x] negation
* [x] disjunction
* [ ] stratum
* [x] stratum
* [ ] magic sets
* [ ] aggregation
* [ ] function symbol

20
src/query/eval.rs
Unescape Escape View File

@ -10,13 +10,16 @@ use crate::query::compile::{
BindingHeadFormatter, BindingHeadTerm, DatalogProgram, QueryCompilationError,
};
use crate::query::relation::Relation;
use crate::query::stratify::stratify_program;
use crate::runtime::temp_store::TempStore;
use crate::runtime::transact::SessionTx;
impl SessionTx {
pub(crate) fn semi_naive_evaluate(&mut self, prog: &DatalogProgram) -> Result<TempStore> {
let stores = prog
pub(crate) fn stratified_evaluate(&mut self, prog: &DatalogProgram) -> Result<TempStore> {
let stratified_prog = stratify_program(prog)?;
let stores = stratified_prog
.iter()
.flatten()
.map(|(k, s)| (k.clone(), (self.new_throwaway(), s.arity)))
.collect::<BTreeMap<_, _>>();
let ret_area = stores
@ -24,6 +27,17 @@ impl SessionTx {
.ok_or(QueryCompilationError::EntryNotFound)?
.0
.clone();
for cur_prog in stratified_prog.iter().rev() {
self.semi_naive_evaluate(cur_prog, &stores)?;
}
Ok(ret_area)
}
fn semi_naive_evaluate(
&mut self,
prog: &DatalogProgram,
stores: &BTreeMap<Keyword, (TempStore, usize)>,
) -> Result<()> {
let compiled: BTreeMap<_, _> = prog
.iter()
.map(
@ -129,6 +143,6 @@ impl SessionTx {
break;
}
}
Ok(ret_area)
Ok(())
}
}

6
src/query/mod.rs
Unescape Escape View File

@ -48,7 +48,7 @@ impl SessionTx {
};
match payload.get("out") {
None => {
let res = self.semi_naive_evaluate(&prog)?;
let res = self.stratified_evaluate(&prog)?;
Ok(Box::new(res.scan_all().map_ok(|tuple| {
JsonValue::Array(tuple.0.into_iter().map(JsonValue::from).collect_vec())
})))
@ -57,7 +57,7 @@ impl SessionTx {
let vld = prog.get(&PROG_ENTRY).unwrap().rules.first().unwrap().vld;
let out_spec = out_spec_map.values().cloned().collect_vec();
let pull_specs = self.parse_pull_specs_for_query(&out_spec, &prog)?;
let res = self.semi_naive_evaluate(&prog)?;
let res = self.stratified_evaluate(&prog)?;
let map_keys = out_spec_map.keys().cloned().collect_vec();
Ok(Box::new(
res.scan_all()
@ -102,7 +102,7 @@ impl SessionTx {
Some(JsonValue::Array(out_spec)) => {
let vld = prog.get(&PROG_ENTRY).unwrap().rules.first().unwrap().vld;
let pull_specs = self.parse_pull_specs_for_query(out_spec, &prog)?;
let res = self.semi_naive_evaluate(&prog)?;
let res = self.stratified_evaluate(&prog)?;
Ok(Box::new(
res.scan_all()
.map_ok(move |tuple| -> Result<JsonValue> {

99
src/query/stratify.rs
Unescape Escape View File

@ -6,7 +6,9 @@ use itertools::Itertools;
use crate::data::keyword::{Keyword, PROG_ENTRY};
use crate::query::compile::{Atom, DatalogProgram, RuleSet};
use crate::query::graph::{reachable_components, strongly_connected_components, Graph, StratifiedGraph, generalized_kahn};
use crate::query::graph::{
generalized_kahn, reachable_components, strongly_connected_components, Graph, StratifiedGraph,
};
#[derive(thiserror::Error, Debug)]
pub enum GraphError {
@ -16,7 +18,6 @@ pub enum GraphError {
GraphNotStratified(BTreeSet<Keyword>),
}
impl Atom {
fn contained_rules(&self) -> BTreeMap<&Keyword, bool> {
match self {
@ -27,22 +28,23 @@ impl Atom {
.into_iter()
.map(|(k, is_neg)| (k, !is_neg))
.collect(),
Atom::Conjunction(args) | Atom::Disjunction(args) => {
let mut ret: BTreeMap<&Keyword, bool> = Default::default();
for arg in args {
for (k, v) in arg.contained_rules() {
match ret.entry(k) {
Entry::Vacant(e) => {
e.insert(v);
}
Entry::Occupied(mut e) => {
let old = *e.get();
e.insert(old || v);
}
}
}
}
ret
Atom::Conjunction(_args) | Atom::Disjunction(_args) => {
panic!("expect program in disjunctive normal form");
// let mut ret: BTreeMap<&Keyword, bool> = Default::default();
// for arg in args {
// for (k, v) in arg.contained_rules() {
// match ret.entry(k) {
// Entry::Vacant(e) => {
// e.insert(v);
// }
// Entry::Occupied(mut e) => {
// let old = *e.get();
// e.insert(old || v);
// }
// }
// }
// }
// ret
}
}
}
@ -79,9 +81,9 @@ fn reduce_to_graph<'a>(g: &StratifiedGraph<&'a Keyword>) -> Graph<&'a Keyword> {
.collect()
}
fn verify_no_cycle(g: &StratifiedGraph<&'_ Keyword>, sccs: Vec<BTreeSet<&Keyword>>) -> Result<()> {
fn verify_no_cycle(g: &StratifiedGraph<&'_ Keyword>, sccs: &[BTreeSet<&Keyword>]) -> Result<()> {
for (k, vs) in g {
for scc in &sccs {
for scc in sccs {
if scc.contains(k) {
for (v, negated) in vs {
if *negated && scc.contains(v) {
@ -97,7 +99,39 @@ fn verify_no_cycle(g: &StratifiedGraph<&'_ Keyword>, sccs: Vec<BTreeSet<&Keyword
Ok(())
}
pub(crate) fn stratify_program(prog: DatalogProgram) -> Result<Vec<DatalogProgram>> {
fn make_scc_reduced_graph<'a>(
sccs: &[BTreeSet<&'a Keyword>],
graph: &StratifiedGraph<&Keyword>,
) -> (BTreeMap<&'a Keyword, usize>, StratifiedGraph<usize>) {
let indices = sccs
.iter()
.enumerate()
.flat_map(|(idx, scc)| scc.iter().map(move |k| (*k, idx)))
.collect::<BTreeMap<_, _>>();
let mut ret: BTreeMap<usize, BTreeMap<usize, bool>> = Default::default();
for (from, tos) in graph {
let from_idx = *indices.get(from).unwrap();
let cur_entry = ret.entry(from_idx).or_default();
for (to, poisoned) in tos {
let to_idx = *indices.get(to).unwrap();
if from_idx == to_idx {
continue;
}
match cur_entry.entry(to_idx) {
Entry::Vacant(e) => {
e.insert(*poisoned);
}
Entry::Occupied(mut e) => {
let old_p = *e.get();
e.insert(old_p || *poisoned);
}
}
}
}
(indices, ret)
}
pub(crate) fn stratify_program(prog: &DatalogProgram) -> Result<Vec<DatalogProgram>> {
// prerequisite: the program is already in disjunctive normal form
// 0. build a graph of the program
let prog_entry: &Keyword = &PROG_ENTRY;
@ -115,11 +149,11 @@ pub(crate) fn stratify_program(prog: DatalogProgram) -> Result<Vec<DatalogProgra
// 2. prune the graph of unreachable clauses
let stratified_graph: StratifiedGraph<_> = stratified_graph
.into_iter()
.filter(|(k, _)| !reachable.contains(k))
.filter(|(k, _)| reachable.contains(k))
.collect();
let graph: Graph<_> = graph
.into_iter()
.filter(|(k, _)| !reachable.contains(k))
.filter(|(k, _)| reachable.contains(k))
.collect();
// 3. find SCC of the clauses
let sccs: Vec<BTreeSet<&Keyword>> = strongly_connected_components(&graph)
@ -127,9 +161,24 @@ pub(crate) fn stratify_program(prog: DatalogProgram) -> Result<Vec<DatalogProgra
.map(|scc| scc.into_iter().cloned().collect())
.collect_vec();
// 4. for each SCC, verify that no neg/agg edges are present so that it is really stratifiable
verify_no_cycle(&stratified_graph, sccs)?;
verify_no_cycle(&stratified_graph, &sccs)?;
// 5. build a reduced graph for the SCC's
let (invert_indices, reduced_graph) = make_scc_reduced_graph(&sccs, &stratified_graph);
// 6. topological sort the reduced graph to get a stratification
let sort_result = generalized_kahn(&reduced_graph, stratified_graph.len());
let n_strata = sort_result.len();
let invert_sort_result = sort_result.into_iter().enumerate().flat_map(|(stratum, indices)| {
indices.into_iter().map(move |idx| (idx, stratum))
}).collect::<BTreeMap<_, _>>();
// 7. translate the stratification into datalog program
todo!()
let mut ret: Vec<DatalogProgram> = vec![Default::default(); n_strata];
for (name, ruleset) in prog {
if let Some(scc_idx) = invert_indices.get(&name) {
let stratum_idx = *invert_sort_result.get(scc_idx).unwrap();
let target = ret.get_mut(stratum_idx).unwrap();
target.insert(name.clone(), ruleset.clone());
}
}
Ok(ret)
}

Write Preview
Loading…
Cancel
Save