Skip to content

Commit 164a347

Browse files
adityamukhoadityamukho
authored
Merge pull request #20 from adityamukho/phase/7.1b-not-join
feat(phase-7.1b): not-join (existential negation)
2 parents b071386 + 5f206a0 commit 164a347

6 files changed

Lines changed: 1301 additions & 43 deletions

File tree

‎src/query/datalog/evaluator.rs‎

Lines changed: 291 additions & 30 deletions
Original file line numberDiff line numberDiff line change
@@ -203,6 +203,12 @@ impl RecursiveEvaluator {
203203
"WhereClause::Not in evaluate_rule: use StratifiedEvaluator for rules with negation"
204204
));
205205
}
206+
WhereClause::NotJoin { .. } => {
207+
// NotJoin clauses are handled by StratifiedEvaluator, not here.
208+
return Err(anyhow!(
209+
"WhereClause::NotJoin in evaluate_rule: use StratifiedEvaluator for rules with negation"
210+
));
211+
}
206212
}
207213
}
208214

@@ -229,7 +235,6 @@ impl RecursiveEvaluator {
229235
if list.is_empty() {
230236
return Err(anyhow!("Rule invocation cannot be empty"));
231237
}
232-
233238
let predicate = match &list[0] {
234239
EdnValue::Symbol(s) => s.clone(),
235240
_ => {
@@ -238,31 +243,8 @@ impl RecursiveEvaluator {
238243
));
239244
}
240245
};
241-
242-
match list.len() {
243-
2 => {
244-
// 1-arg: (blocked ?x) → [?x :blocked ?_rule_value]
245-
// ?_rule_value is a wildcard that matches any stored sentinel value.
246-
Ok(Pattern::new(
247-
list[1].clone(),
248-
EdnValue::Keyword(format!(":{}", predicate)),
249-
EdnValue::Symbol("?_rule_value".to_string()),
250-
))
251-
}
252-
3 => {
253-
// 2-arg: (reachable ?from ?to) → [?from :reachable ?to]
254-
Ok(Pattern::new(
255-
list[1].clone(),
256-
EdnValue::Keyword(format!(":{}", predicate)),
257-
list[2].clone(),
258-
))
259-
}
260-
n => Err(anyhow!(
261-
"Rule invocation '{}' must have 1 or 2 arguments, got {}",
262-
predicate,
263-
n - 1
264-
)),
265-
}
246+
let args: Vec<EdnValue> = list[1..].to_vec();
247+
rule_invocation_to_pattern(&predicate, &args)
266248
}
267249

268250
/// Instantiate rule head with variable bindings to create a derived fact.
@@ -375,6 +357,77 @@ pub fn substitute_value(value: &EdnValue, binding: &Bindings) -> EdnValue {
375357
}
376358
}
377359

360+
/// Convert a predicate name + argument list to a Pattern.
361+
///
362+
/// 1-arg: `(blocked ?x)` → `[?x :blocked ?_rule_value]`
363+
/// 2-arg: `(reachable ?from ?to)` → `[?from :reachable ?to]`
364+
pub(super) fn rule_invocation_to_pattern(predicate: &str, args: &[EdnValue]) -> Result<Pattern> {
365+
match args.len() {
366+
1 => Ok(Pattern::new(
367+
args[0].clone(),
368+
EdnValue::Keyword(format!(":{}", predicate)),
369+
EdnValue::Symbol("?_rule_value".to_string()),
370+
)),
371+
2 => Ok(Pattern::new(
372+
args[0].clone(),
373+
EdnValue::Keyword(format!(":{}", predicate)),
374+
args[1].clone(),
375+
)),
376+
n => Err(anyhow!(
377+
"Rule invocation '{}' must have 1 or 2 arguments, got {}",
378+
predicate,
379+
n
380+
)),
381+
}
382+
}
383+
384+
/// Test whether a `not-join` body is satisfiable given a current binding.
385+
///
386+
/// Returns `true` if the body IS satisfiable → outer binding should be **rejected**.
387+
/// Returns `false` if the body cannot be satisfied → outer binding survives.
388+
///
389+
/// Algorithm:
390+
/// 1. Build a partial binding containing only the join_vars entries.
391+
/// 2. For each clause:
392+
/// - Pattern → substitute join_vars via substitute_pattern.
393+
/// - RuleInvocation → convert to Pattern via rule_invocation_to_pattern, then substitute.
394+
/// Rule-derived facts are already present in `storage` (accumulated) from lower strata.
395+
/// 3. Run PatternMatcher::match_patterns on all resulting patterns against `storage`.
396+
/// 4. Any complete match → body is satisfiable → return true (reject outer binding).
397+
pub fn evaluate_not_join(
398+
join_vars: &[String],
399+
clauses: &[WhereClause],
400+
binding: &Bindings,
401+
storage: &FactStorage,
402+
) -> bool {
403+
// Build a partial binding containing only the join variables
404+
let partial: Bindings = join_vars
405+
.iter()
406+
.filter_map(|v| binding.get(v.as_str()).map(|val| (v.clone(), val.clone())))
407+
.collect();
408+
409+
// Convert all clauses to patterns
410+
let substituted: Vec<Pattern> = clauses
411+
.iter()
412+
.filter_map(|c| match c {
413+
WhereClause::Pattern(p) => Some(substitute_pattern(p, &partial)),
414+
WhereClause::RuleInvocation { predicate, args } => {
415+
rule_invocation_to_pattern(predicate, args)
416+
.ok()
417+
.map(|p| substitute_pattern(&p, &partial))
418+
}
419+
_ => None,
420+
})
421+
.collect();
422+
423+
if substituted.is_empty() {
424+
return false;
425+
}
426+
427+
let matcher = PatternMatcher::new(storage.clone());
428+
!matcher.match_patterns(&substituted).is_empty()
429+
}
430+
378431
/// Evaluates Datalog rules with stratified negation support.
379432
///
380433
/// Strata are evaluated in ascending order. Within each stratum, positive-only
@@ -457,7 +510,10 @@ impl StratifiedEvaluator {
457510

458511
for pred in &stratum_preds {
459512
for rule in registry.get_rules(pred) {
460-
let has_not = rule.body.iter().any(|c| matches!(c, WhereClause::Not(_)));
513+
let has_not = rule
514+
.body
515+
.iter()
516+
.any(|c| matches!(c, WhereClause::Not(_) | WhereClause::NotJoin { .. }));
461517
if has_not {
462518
mixed_rules.push((pred.clone(), rule));
463519
} else {
@@ -512,7 +568,7 @@ impl StratifiedEvaluator {
512568
)),
513569
_ => None,
514570
},
515-
WhereClause::Not(_) => None,
571+
WhereClause::Not(_) | WhereClause::NotJoin { .. } => None,
516572
})
517573
.collect();
518574

@@ -525,6 +581,17 @@ impl StratifiedEvaluator {
525581
})
526582
.collect();
527583

584+
let not_join_clauses: Vec<(Vec<String>, Vec<WhereClause>)> = rule
585+
.body
586+
.iter()
587+
.filter_map(|c| match c {
588+
WhereClause::NotJoin { join_vars, clauses } => {
589+
Some((join_vars.clone(), clauses.clone()))
590+
}
591+
_ => None,
592+
})
593+
.collect();
594+
528595
let matcher = PatternMatcher::new(accumulated.clone());
529596
let candidates = matcher.match_patterns(&positive_patterns);
530597

@@ -558,7 +625,7 @@ impl StratifiedEvaluator {
558625
_ => None,
559626
}
560627
}
561-
WhereClause::Not(_) => None,
628+
WhereClause::Not(_) | WhereClause::NotJoin { .. } => None,
562629
})
563630
.collect();
564631

@@ -569,7 +636,13 @@ impl StratifiedEvaluator {
569636
}
570637
}
571638

572-
// All Not conditions held -> derive head fact
639+
for (join_vars, nj_clauses) in &not_join_clauses {
640+
if evaluate_not_join(join_vars, nj_clauses, &binding, &accumulated) {
641+
continue 'binding;
642+
}
643+
}
644+
645+
// All Not / NotJoin conditions held -> derive head fact
573646
if let Ok(fact) = temp_eval.instantiate_head_public(&rule.head, &binding) {
574647
// Use transact (not load_fact) so derived facts get a proper
575648
// tx_id and incremented tx_count, matching spec step (d).
@@ -1095,6 +1168,194 @@ mod tests {
10951168
assert_eq!(eligible_facts.len(), 1, "alice should be eligible");
10961169
}
10971170

1171+
#[test]
1172+
fn test_not_join_rejects_entity_with_matching_inner_var() {
1173+
// Rule: (clean ?x) :- [?x :submitted true], (not-join [?x] [?x :has-dep ?d] [?d :blocked true])
1174+
// alice: submitted=true, has-dep=dep1, dep1:blocked=true -> NOT clean
1175+
// bob: submitted=true -> clean
1176+
let storage = FactStorage::new();
1177+
let alice = Uuid::new_v4();
1178+
let bob = Uuid::new_v4();
1179+
let dep1 = Uuid::new_v4();
1180+
storage
1181+
.transact(
1182+
vec![
1183+
(alice, ":submitted".to_string(), Value::Boolean(true)),
1184+
(alice, ":has-dep".to_string(), Value::Ref(dep1)),
1185+
(dep1, ":blocked".to_string(), Value::Boolean(true)),
1186+
(bob, ":submitted".to_string(), Value::Boolean(true)),
1187+
],
1188+
None,
1189+
)
1190+
.unwrap();
1191+
1192+
let rule = Rule::new(
1193+
vec![
1194+
EdnValue::Symbol("clean".to_string()),
1195+
EdnValue::Symbol("?x".to_string()),
1196+
],
1197+
vec![
1198+
WhereClause::Pattern(Pattern::new(
1199+
EdnValue::Symbol("?x".to_string()),
1200+
EdnValue::Keyword(":submitted".to_string()),
1201+
EdnValue::Boolean(true),
1202+
)),
1203+
WhereClause::NotJoin {
1204+
join_vars: vec!["?x".to_string()],
1205+
clauses: vec![
1206+
WhereClause::Pattern(Pattern::new(
1207+
EdnValue::Symbol("?x".to_string()),
1208+
EdnValue::Keyword(":has-dep".to_string()),
1209+
EdnValue::Symbol("?d".to_string()),
1210+
)),
1211+
WhereClause::Pattern(Pattern::new(
1212+
EdnValue::Symbol("?d".to_string()),
1213+
EdnValue::Keyword(":blocked".to_string()),
1214+
EdnValue::Boolean(true),
1215+
)),
1216+
],
1217+
},
1218+
],
1219+
);
1220+
1221+
let mut registry = RuleRegistry::new();
1222+
registry.register_rule_unchecked("clean".to_string(), rule);
1223+
let rules = Arc::new(RwLock::new(registry));
1224+
let evaluator = StratifiedEvaluator::new(storage, rules, 100);
1225+
let result = evaluator.evaluate(&["clean".to_string()]).unwrap();
1226+
let clean_facts: Vec<_> = result
1227+
.get_facts_by_attribute(&":clean".to_string())
1228+
.unwrap_or_default()
1229+
.into_iter()
1230+
.filter(|f| f.asserted)
1231+
.collect();
1232+
assert_eq!(clean_facts.len(), 1, "only bob should be clean");
1233+
assert_eq!(clean_facts[0].entity, bob, "the clean entity must be bob");
1234+
}
1235+
1236+
#[test]
1237+
fn test_not_join_keeps_entity_when_inner_var_has_no_match() {
1238+
// Only alice has submitted=true and NO has-dep at all -> clean
1239+
let storage = FactStorage::new();
1240+
let alice = Uuid::new_v4();
1241+
storage
1242+
.transact(
1243+
vec![(alice, ":submitted".to_string(), Value::Boolean(true))],
1244+
None,
1245+
)
1246+
.unwrap();
1247+
1248+
let rule = Rule::new(
1249+
vec![
1250+
EdnValue::Symbol("clean".to_string()),
1251+
EdnValue::Symbol("?x".to_string()),
1252+
],
1253+
vec![
1254+
WhereClause::Pattern(Pattern::new(
1255+
EdnValue::Symbol("?x".to_string()),
1256+
EdnValue::Keyword(":submitted".to_string()),
1257+
EdnValue::Boolean(true),
1258+
)),
1259+
WhereClause::NotJoin {
1260+
join_vars: vec!["?x".to_string()],
1261+
clauses: vec![WhereClause::Pattern(Pattern::new(
1262+
EdnValue::Symbol("?x".to_string()),
1263+
EdnValue::Keyword(":has-dep".to_string()),
1264+
EdnValue::Symbol("?d".to_string()),
1265+
))],
1266+
},
1267+
],
1268+
);
1269+
1270+
let mut registry = RuleRegistry::new();
1271+
registry.register_rule_unchecked("clean".to_string(), rule);
1272+
let rules = Arc::new(RwLock::new(registry));
1273+
let evaluator = StratifiedEvaluator::new(storage, rules, 100);
1274+
let result = evaluator.evaluate(&["clean".to_string()]).unwrap();
1275+
let clean_facts: Vec<_> = result
1276+
.get_facts_by_attribute(&":clean".to_string())
1277+
.unwrap_or_default()
1278+
.into_iter()
1279+
.filter(|f| f.asserted)
1280+
.collect();
1281+
assert_eq!(
1282+
clean_facts.len(),
1283+
1,
1284+
"alice must be clean when no deps exist"
1285+
);
1286+
}
1287+
1288+
#[test]
1289+
fn test_not_join_body_with_rule_invocation() {
1290+
// Rule: (blocked ?x) :- [?x :status :banned]
1291+
// Rule: (clean ?x) :- [?x :submitted true], (not-join [?x] (blocked ?x))
1292+
// alice: submitted, banned -> NOT clean
1293+
// bob: submitted, not banned -> clean
1294+
let storage = FactStorage::new();
1295+
let alice = Uuid::new_v4();
1296+
let bob = Uuid::new_v4();
1297+
storage
1298+
.transact(
1299+
vec![
1300+
(alice, ":submitted".to_string(), Value::Boolean(true)),
1301+
(
1302+
alice,
1303+
":status".to_string(),
1304+
Value::Keyword(":banned".to_string()),
1305+
),
1306+
(bob, ":submitted".to_string(), Value::Boolean(true)),
1307+
],
1308+
None,
1309+
)
1310+
.unwrap();
1311+
1312+
let rule_blocked = Rule::new(
1313+
vec![
1314+
EdnValue::Symbol("blocked".to_string()),
1315+
EdnValue::Symbol("?x".to_string()),
1316+
],
1317+
vec![WhereClause::Pattern(Pattern::new(
1318+
EdnValue::Symbol("?x".to_string()),
1319+
EdnValue::Keyword(":status".to_string()),
1320+
EdnValue::Keyword(":banned".to_string()),
1321+
))],
1322+
);
1323+
let rule_clean = Rule::new(
1324+
vec![
1325+
EdnValue::Symbol("clean".to_string()),
1326+
EdnValue::Symbol("?x".to_string()),
1327+
],
1328+
vec![
1329+
WhereClause::Pattern(Pattern::new(
1330+
EdnValue::Symbol("?x".to_string()),
1331+
EdnValue::Keyword(":submitted".to_string()),
1332+
EdnValue::Boolean(true),
1333+
)),
1334+
WhereClause::NotJoin {
1335+
join_vars: vec!["?x".to_string()],
1336+
clauses: vec![WhereClause::RuleInvocation {
1337+
predicate: "blocked".to_string(),
1338+
args: vec![EdnValue::Symbol("?x".to_string())],
1339+
}],
1340+
},
1341+
],
1342+
);
1343+
let mut registry = RuleRegistry::new();
1344+
registry.register_rule_unchecked("blocked".to_string(), rule_blocked);
1345+
registry.register_rule_unchecked("clean".to_string(), rule_clean);
1346+
let rules = Arc::new(RwLock::new(registry));
1347+
let evaluator = StratifiedEvaluator::new(storage, rules, 100);
1348+
let result = evaluator.evaluate(&["clean".to_string()]).unwrap();
1349+
let clean_facts: Vec<_> = result
1350+
.get_facts_by_attribute(&":clean".to_string())
1351+
.unwrap_or_default()
1352+
.into_iter()
1353+
.filter(|f| f.asserted)
1354+
.collect();
1355+
assert_eq!(clean_facts.len(), 1, "only bob should be clean");
1356+
assert_eq!(clean_facts[0].entity, bob, "the clean entity must be bob");
1357+
}
1358+
10981359
#[test]
10991360
fn test_not_filter_with_multiple_not_clauses() {
11001361
// eligible :- [?x :status "active"], not([?x :role "admin"]), not([?x :banned true])

0 commit comments

Comments
 (0)