diff --git a/.gitignore b/.gitignore index f96ff5a..a2d59ea 100644 --- a/.gitignore +++ b/.gitignore @@ -81,3 +81,4 @@ Cargo.lock .benchmarks .env .claude/ +*.proptest-regressions diff --git a/Cargo.toml b/Cargo.toml index efb5bed..442c44c 100644 --- a/Cargo.toml +++ b/Cargo.toml @@ -32,6 +32,9 @@ binaries = [] [dependencies] +[dev-dependencies] +proptest = "1.6" + [profile.release] strip = "debuginfo" panic = "unwind" diff --git a/tests/property_tests.rs b/tests/property_tests.rs index 8b13789..a04b200 100644 --- a/tests/property_tests.rs +++ b/tests/property_tests.rs @@ -1 +1,391 @@ +//! Property-based tests for the chase algorithm using proptest. +use proptest::prelude::*; + +use chase_rs::chase::rule::RuleBuilder; +use chase_rs::{Atom, Instance, Term, chase}; + +/// Strategy for generating constant names +fn constant_strategy() -> impl Strategy { + prop::sample::select(vec![ + "a".to_string(), + "b".to_string(), + "c".to_string(), + "d".to_string(), + "e".to_string(), + ]) +} + +/// Strategy for generating variable names +fn variable_strategy() -> impl Strategy { + prop::sample::select(vec![ + "X".to_string(), + "Y".to_string(), + "Z".to_string(), + "W".to_string(), + ]) +} + +/// Strategy for generating predicate names +fn predicate_strategy() -> impl Strategy { + prop::sample::select(vec![ + "P".to_string(), + "Q".to_string(), + "R".to_string(), + "S".to_string(), + ]) +} + +/// Strategy for generating ground atoms (facts) +fn ground_atom_strategy() -> impl Strategy { + ( + predicate_strategy(), + prop::collection::vec(constant_strategy(), 1..=3), + ) + .prop_map(|(pred, consts)| { + Atom::new(pred, consts.into_iter().map(Term::constant).collect()) + }) +} + +/// Strategy for generating a small instance (set of facts) +fn instance_strategy() -> impl Strategy { + prop::collection::vec(ground_atom_strategy(), 0..10) + .prop_map(|atoms| atoms.into_iter().collect()) +} + +// ============================================================================= +// Property: Chase always terminates +// ============================================================================= + +proptest! { + #![proptest_config(ProptestConfig::with_cases(50))] + + #[test] + fn chase_always_terminates(instance in instance_strategy()) { + // Simple rule: P(X) -> Q(X) + let rule = RuleBuilder::new() + .when("P", vec![Term::var("X")]) + .then("Q", vec![Term::var("X")]) + .build(); + + let result = chase(instance, &[rule]); + + // Chase should always terminate (either fixpoint or max iterations) + prop_assert!(result.terminated || result.steps > 0); + } +} + +// ============================================================================= +// Property: Chase is monotonic (facts are only added, never removed) +// ============================================================================= + +proptest! { + #![proptest_config(ProptestConfig::with_cases(50))] + + #[test] + fn chase_is_monotonic(instance in instance_strategy()) { + let initial_facts: Vec<_> = instance.iter().cloned().collect(); + + let rule = RuleBuilder::new() + .when("P", vec![Term::var("X")]) + .then("Q", vec![Term::var("X")]) + .build(); + + let result = chase(instance, &[rule]); + + // All original facts should still be present + for fact in &initial_facts { + prop_assert!( + result.instance.contains(fact), + "Original fact {:?} was removed", fact + ); + } + + // Result should have at least as many facts as the input + prop_assert!(result.instance.len() >= initial_facts.len()); + } +} + +// ============================================================================= +// Property: Fixpoint is stable (running chase again produces no changes) +// ============================================================================= + +proptest! { + #![proptest_config(ProptestConfig::with_cases(30))] + + #[test] + fn fixpoint_is_stable(instance in instance_strategy()) { + let rule = RuleBuilder::new() + .when("P", vec![Term::var("X")]) + .then("Q", vec![Term::var("X")]) + .build(); + + // Run chase to fixpoint + let result1 = chase(instance, &[rule.clone()]); + prop_assert!(result1.terminated); + + // Run chase again on the result + let result2 = chase(result1.instance.clone(), &[rule]); + + // Should terminate immediately with no new facts + prop_assert!(result2.terminated); + prop_assert_eq!(result2.steps, 0, "Second chase should produce no changes"); + prop_assert_eq!(result1.instance.len(), result2.instance.len()); + } +} + +// ============================================================================= +// Property: All derived facts are ground (no variables) +// ============================================================================= + +proptest! { + #![proptest_config(ProptestConfig::with_cases(50))] + + #[test] + fn all_facts_are_ground(instance in instance_strategy()) { + let rule = RuleBuilder::new() + .when("P", vec![Term::var("X"), Term::var("Y")]) + .then("R", vec![Term::var("X"), Term::var("Y")]) + .build(); + + let result = chase(instance, &[rule]); + + for fact in result.instance.iter() { + prop_assert!( + fact.is_ground(), + "Fact {:?} contains variables", fact + ); + } + } +} + +// ============================================================================= +// Property: Rules without existentials don't create nulls +// ============================================================================= + +proptest! { + #![proptest_config(ProptestConfig::with_cases(50))] + + #[test] + fn no_existentials_means_no_nulls(instance in instance_strategy()) { + // Rule with all head variables appearing in body + let rule = RuleBuilder::new() + .when("P", vec![Term::var("X")]) + .then("Q", vec![Term::var("X")]) + .build(); + + let result = chase(instance, &[rule]); + + for fact in result.instance.iter() { + for term in &fact.terms { + prop_assert!( + !matches!(term, Term::Null(_)), + "Found null in fact {:?} but rule has no existentials", fact + ); + } + } + } +} + +// ============================================================================= +// Property: Existential rules create exactly one null per trigger +// ============================================================================= + +proptest! { + #![proptest_config(ProptestConfig::with_cases(30))] + + #[test] + fn existentials_create_unique_nulls( + num_constants in 1usize..5 + ) { + // Create facts P(c0), P(c1), P(c2), ... with unique constants + let constants: Vec = (0..num_constants).map(|i| format!("c{}", i)).collect(); + let instance: Instance = constants + .iter() + .map(|c| Atom::new("P", vec![Term::constant(c)])) + .collect(); + + // Rule: P(X) -> Q(X, Y) where Y is existential + let rule = RuleBuilder::new() + .when("P", vec![Term::var("X")]) + .then("Q", vec![Term::var("X"), Term::var("Y")]) + .build(); + + let result = chase(instance, &[rule]); + + let q_facts: Vec<_> = result.instance.facts_for_predicate("Q"); + + // Should have exactly as many Q facts as P facts + prop_assert_eq!(q_facts.len(), num_constants); + + // Each Q fact should have a null in the second position + for fact in &q_facts { + prop_assert!( + matches!(fact.terms[1], Term::Null(_)), + "Expected null in second position of {:?}", fact + ); + } + + // All nulls should be unique + let nulls: Vec<_> = q_facts + .iter() + .filter_map(|f| match &f.terms[1] { + Term::Null(id) => Some(*id), + _ => None, + }) + .collect(); + + let mut unique_nulls = nulls.clone(); + unique_nulls.sort(); + unique_nulls.dedup(); + prop_assert_eq!(nulls.len(), unique_nulls.len(), "Nulls should be unique"); + } +} + +// ============================================================================= +// Property: Transitive closure computes correct number of facts +// ============================================================================= + +proptest! { + #![proptest_config(ProptestConfig::with_cases(20))] + + #[test] + fn transitive_closure_chain(chain_length in 2usize..6) { + // Create a chain: E(0,1), E(1,2), ..., E(n-1,n) + let mut facts = Vec::new(); + for i in 0..chain_length { + facts.push(Atom::new( + "E", + vec![Term::constant(format!("{}", i)), Term::constant(format!("{}", i + 1))], + )); + } + let instance: Instance = facts.into_iter().collect(); + + // E(X,Y) -> T(X,Y) + let rule1 = RuleBuilder::new() + .when("E", vec![Term::var("X"), Term::var("Y")]) + .then("T", vec![Term::var("X"), Term::var("Y")]) + .build(); + + // T(X,Y), E(Y,Z) -> T(X,Z) + let rule2 = RuleBuilder::new() + .when("T", vec![Term::var("X"), Term::var("Y")]) + .when("E", vec![Term::var("Y"), Term::var("Z")]) + .then("T", vec![Term::var("X"), Term::var("Z")]) + .build(); + + let result = chase(instance, &[rule1, rule2]); + prop_assert!(result.terminated); + + let t_facts = result.instance.facts_for_predicate("T"); + + // For a chain of n edges, transitive closure has n*(n+1)/2 pairs + let expected = chain_length * (chain_length + 1) / 2; + prop_assert_eq!( + t_facts.len(), + expected, + "Chain of {} edges should have {} transitive pairs", + chain_length, + expected + ); + } +} + +// ============================================================================= +// Property: Empty instance with any rules produces empty or stays empty +// ============================================================================= + +proptest! { + #[test] + fn empty_instance_stays_bounded(_seed in 0u64..1000) { + let instance = Instance::new(); + + let rule = RuleBuilder::new() + .when("P", vec![Term::var("X")]) + .then("Q", vec![Term::var("X")]) + .build(); + + let result = chase(instance, &[rule]); + + prop_assert!(result.terminated); + prop_assert_eq!(result.steps, 0); + prop_assert!(result.instance.is_empty()); + } +} + +// ============================================================================= +// Property: Substitution application is idempotent for ground terms +// ============================================================================= + +use chase_rs::Substitution; + +proptest! { + #![proptest_config(ProptestConfig::with_cases(100))] + + #[test] + fn substitution_ground_term_unchanged(c in constant_strategy()) { + let term = Term::constant(&c); + let mut subst = Substitution::new(); + subst.bind("X".to_string(), Term::constant("other")); + + let result = subst.apply_term(&term); + + prop_assert_eq!(result, term, "Ground term should be unchanged by substitution"); + } +} + +// ============================================================================= +// Property: Substitution correctly replaces variables +// ============================================================================= + +proptest! { + #![proptest_config(ProptestConfig::with_cases(100))] + + #[test] + fn substitution_replaces_variable( + var in variable_strategy(), + replacement in constant_strategy() + ) { + let term = Term::var(&var); + let mut subst = Substitution::new(); + subst.bind(var.clone(), Term::constant(&replacement)); + + let result = subst.apply_term(&term); + + prop_assert_eq!( + result, + Term::constant(&replacement), + "Variable should be replaced" + ); + } +} + +// ============================================================================= +// Property: Atom arity is preserved through substitution +// ============================================================================= + +proptest! { + #![proptest_config(ProptestConfig::with_cases(50))] + + #[test] + fn substitution_preserves_arity( + pred in predicate_strategy(), + vars in prop::collection::vec(variable_strategy(), 1..4), + replacement in constant_strategy() + ) { + let atom = Atom::new( + &pred, + vars.iter().map(|v| Term::var(v)).collect(), + ); + + let mut subst = Substitution::new(); + for var in &vars { + subst.bind(var.clone(), Term::constant(&replacement)); + } + + let result = subst.apply_atom(&atom); + + prop_assert_eq!(result.arity(), atom.arity()); + prop_assert_eq!(result.predicate, atom.predicate); + } +}