From b2cfe4763e21e8610bbff66216bcf6ac7105a08a Mon Sep 17 00:00:00 2001 From: Hassan Abedi Date: Mon, 9 Mar 2026 17:49:30 +0100 Subject: [PATCH] Make property tests deterministic with explicit seeds --- tests/property_tests.rs | 504 ++++++++++++++++++++++------------------ 1 file changed, 278 insertions(+), 226 deletions(-) diff --git a/tests/property_tests.rs b/tests/property_tests.rs index a04b200..96ecd16 100644 --- a/tests/property_tests.rs +++ b/tests/property_tests.rs @@ -1,9 +1,30 @@ //! Property-based tests for the chase algorithm using proptest. +//! +//! All tests use explicit seeds for reproducibility. use proptest::prelude::*; +use proptest::test_runner::{Config, TestRng, TestRunner}; use chase_rs::chase::rule::RuleBuilder; -use chase_rs::{Atom, Instance, Term, chase}; +use chase_rs::{Atom, Instance, Substitution, Term, chase}; + +// ============================================================================= +// Test Configuration +// ============================================================================= + +/// Create a test runner with an explicit seed for reproducibility. +fn seeded_runner(seed: u64, cases: u32) -> TestRunner { + let config = Config::with_cases(cases); + // Create a deterministic seed from u64 + let mut seed_bytes = [0u8; 32]; + seed_bytes[..8].copy_from_slice(&seed.to_le_bytes()); + let rng = TestRng::from_seed(proptest::test_runner::RngAlgorithm::ChaCha, &seed_bytes); + TestRunner::new_with_rng(config, rng) +} + +// ============================================================================= +// Strategies +// ============================================================================= /// Strategy for generating constant names fn constant_strategy() -> impl Strategy { @@ -57,335 +78,366 @@ fn instance_strategy() -> impl Strategy { // Property: Chase always terminates // ============================================================================= -proptest! { - #![proptest_config(ProptestConfig::with_cases(50))] +#[test] +fn chase_always_terminates() { + const SEED: u64 = 12345; + let mut runner = seeded_runner(SEED, 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(); + runner + .run(&instance_strategy(), |instance| { + let rule = RuleBuilder::new() + .when("P", vec![Term::var("X")]) + .then("Q", vec![Term::var("X")]) + .build(); - let result = chase(instance, &[rule]); + let result = chase(instance, &[rule]); - // Chase should always terminate (either fixpoint or max iterations) - prop_assert!(result.terminated || result.steps > 0); - } + prop_assert!(result.terminated || result.steps > 0); + Ok(()) + }) + .unwrap(); } // ============================================================================= // Property: Chase is monotonic (facts are only added, never removed) // ============================================================================= -proptest! { - #![proptest_config(ProptestConfig::with_cases(50))] +#[test] +fn chase_is_monotonic() { + const SEED: u64 = 23456; + let mut runner = seeded_runner(SEED, 50); - #[test] - fn chase_is_monotonic(instance in instance_strategy()) { - let initial_facts: Vec<_> = instance.iter().cloned().collect(); + runner + .run(&instance_strategy(), |instance| { + 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 rule = RuleBuilder::new() + .when("P", vec![Term::var("X")]) + .then("Q", vec![Term::var("X")]) + .build(); - let result = chase(instance, &[rule]); + 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 - ); - } + 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()); - } + prop_assert!(result.instance.len() >= initial_facts.len()); + Ok(()) + }) + .unwrap(); } // ============================================================================= // Property: Fixpoint is stable (running chase again produces no changes) // ============================================================================= -proptest! { - #![proptest_config(ProptestConfig::with_cases(30))] +#[test] +fn fixpoint_is_stable() { + const SEED: u64 = 34567; + let mut runner = seeded_runner(SEED, 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(); + runner + .run(&instance_strategy(), |instance| { + 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); + let result1 = chase(instance, &[rule.clone()]); + prop_assert!(result1.terminated); - // Run chase again on the result - let result2 = chase(result1.instance.clone(), &[rule]); + 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()); - } + 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()); + Ok(()) + }) + .unwrap(); } // ============================================================================= // Property: All derived facts are ground (no variables) // ============================================================================= -proptest! { - #![proptest_config(ProptestConfig::with_cases(50))] +#[test] +fn all_facts_are_ground() { + const SEED: u64 = 45678; + let mut runner = seeded_runner(SEED, 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(); + runner + .run(&instance_strategy(), |instance| { + 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]); + let result = chase(instance, &[rule]); - for fact in result.instance.iter() { - prop_assert!( - fact.is_ground(), - "Fact {:?} contains variables", fact - ); - } - } + for fact in result.instance.iter() { + prop_assert!(fact.is_ground(), "Fact {:?} contains variables", fact); + } + Ok(()) + }) + .unwrap(); } // ============================================================================= // Property: Rules without existentials don't create nulls // ============================================================================= -proptest! { - #![proptest_config(ProptestConfig::with_cases(50))] +#[test] +fn no_existentials_means_no_nulls() { + const SEED: u64 = 56789; + let mut runner = seeded_runner(SEED, 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(); + runner + .run(&instance_strategy(), |instance| { + let rule = RuleBuilder::new() + .when("P", vec![Term::var("X")]) + .then("Q", vec![Term::var("X")]) + .build(); - let result = chase(instance, &[rule]); + 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 - ); + 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 + ); + } } - } - } + Ok(()) + }) + .unwrap(); } // ============================================================================= // Property: Existential rules create exactly one null per trigger // ============================================================================= -proptest! { - #![proptest_config(ProptestConfig::with_cases(30))] +#[test] +fn existentials_create_unique_nulls() { + const SEED: u64 = 67890; + let mut runner = seeded_runner(SEED, 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(); + runner + .run(&(1usize..5), |num_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 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 result = chase(instance, &[rule]); - let q_facts: Vec<_> = result.instance.facts_for_predicate("Q"); + 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); + 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 - ); - } + 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 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"); - } + let mut unique_nulls = nulls.clone(); + unique_nulls.sort(); + unique_nulls.dedup(); + prop_assert_eq!(nulls.len(), unique_nulls.len(), "Nulls should be unique"); + Ok(()) + }) + .unwrap(); } // ============================================================================= // Property: Transitive closure computes correct number of facts // ============================================================================= -proptest! { - #![proptest_config(ProptestConfig::with_cases(20))] +#[test] +fn transitive_closure_chain() { + const SEED: u64 = 78901; + let mut runner = seeded_runner(SEED, 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(); + runner + .run(&(2usize..6), |chain_length| { + 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(); + 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 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 result = chase(instance, &[rule1, rule2]); + prop_assert!(result.terminated); - let t_facts = result.instance.facts_for_predicate("T"); + 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 - ); - } + 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 + ); + Ok(()) + }) + .unwrap(); } // ============================================================================= // 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(); +#[test] +fn empty_instance_stays_bounded() { + const SEED: u64 = 89012; + let mut runner = seeded_runner(SEED, 100); - let rule = RuleBuilder::new() - .when("P", vec![Term::var("X")]) - .then("Q", vec![Term::var("X")]) - .build(); + runner + .run(&(0u64..1000), |_| { + let instance = Instance::new(); - let result = chase(instance, &[rule]); + let rule = RuleBuilder::new() + .when("P", vec![Term::var("X")]) + .then("Q", vec![Term::var("X")]) + .build(); - prop_assert!(result.terminated); - prop_assert_eq!(result.steps, 0); - prop_assert!(result.instance.is_empty()); - } + let result = chase(instance, &[rule]); + + prop_assert!(result.terminated); + prop_assert_eq!(result.steps, 0); + prop_assert!(result.instance.is_empty()); + Ok(()) + }) + .unwrap(); } // ============================================================================= // Property: Substitution application is idempotent for ground terms // ============================================================================= -use chase_rs::Substitution; +#[test] +fn substitution_ground_term_unchanged() { + const SEED: u64 = 90123; + let mut runner = seeded_runner(SEED, 100); -proptest! { - #![proptest_config(ProptestConfig::with_cases(100))] + runner + .run(&constant_strategy(), |c| { + let term = Term::constant(&c); + let mut subst = Substitution::new(); + subst.bind("X".to_string(), Term::constant("other")); - #[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); - let result = subst.apply_term(&term); - - prop_assert_eq!(result, term, "Ground term should be unchanged by substitution"); - } + prop_assert_eq!( + result, + term, + "Ground term should be unchanged by substitution" + ); + Ok(()) + }) + .unwrap(); } // ============================================================================= // Property: Substitution correctly replaces variables // ============================================================================= -proptest! { - #![proptest_config(ProptestConfig::with_cases(100))] +#[test] +fn substitution_replaces_variable() { + const SEED: u64 = 11111; + let mut runner = seeded_runner(SEED, 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)); + runner + .run( + &(variable_strategy(), constant_strategy()), + |(var, replacement)| { + let term = Term::var(&var); + let mut subst = Substitution::new(); + subst.bind(var.clone(), Term::constant(&replacement)); - let result = subst.apply_term(&term); + let result = subst.apply_term(&term); - prop_assert_eq!( - result, - Term::constant(&replacement), - "Variable should be replaced" - ); - } + prop_assert_eq!( + result, + Term::constant(&replacement), + "Variable should be replaced" + ); + Ok(()) + }, + ) + .unwrap(); } // ============================================================================= // Property: Atom arity is preserved through substitution // ============================================================================= -proptest! { - #![proptest_config(ProptestConfig::with_cases(50))] +#[test] +fn substitution_preserves_arity() { + const SEED: u64 = 22222; + let mut runner = seeded_runner(SEED, 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 strategy = ( + predicate_strategy(), + prop::collection::vec(variable_strategy(), 1..4), + constant_strategy(), + ); - let mut subst = Substitution::new(); - for var in &vars { - subst.bind(var.clone(), Term::constant(&replacement)); - } + runner + .run(&strategy, |(pred, vars, replacement)| { + let atom = Atom::new(&pred, vars.iter().map(|v| Term::var(v)).collect()); - let result = subst.apply_atom(&atom); + let mut subst = Substitution::new(); + for var in &vars { + subst.bind(var.clone(), Term::constant(&replacement)); + } - prop_assert_eq!(result.arity(), atom.arity()); - prop_assert_eq!(result.predicate, atom.predicate); - } + let result = subst.apply_atom(&atom); + + prop_assert_eq!(result.arity(), atom.arity()); + prop_assert_eq!(result.predicate, atom.predicate); + Ok(()) + }) + .unwrap(); }