prolog2/predicate_modules/
meta_predicates.rs

1use crate::{
2    heap::{heap::Heap, query_heap::QueryHeap},
3    program::{hypothesis::Hypothesis, predicate_table::PredicateTable},
4    resolution::proof::Proof,
5    Config,
6};
7
8use super::PredReturn;
9
10/// Negation as failure: succeeds if the inner goal cannot be proven
11pub fn not(
12    heap: &mut QueryHeap,
13    hypothesis: &mut Hypothesis,
14    goal: usize,
15    predicate_table: &PredicateTable,
16    config: Config,
17) -> PredReturn {
18    use crate::heap::heap::Tag;
19
20    // The goal is not(X), we want to prove X
21    // Goal may be a Str cell pointing to the Func, or directly a Func cell
22    // We need to find the actual Func cell first, then get the first argument
23
24    // First dereference to handle any Ref indirection
25    let mut func_addr = heap.deref_addr(goal);
26
27    // If it's a Str cell, follow the pointer to the actual Func
28    if let (Tag::Str, pointer) = heap[func_addr] {
29        func_addr = pointer;
30    }
31
32    // Now func_addr points to: Func(2) | Con("not") | InnerGoal
33    // The inner goal is at func_addr + 2
34    // But it might be a Str cell pointing to the actual goal structure
35    let arg_addr = func_addr + 2;
36    let inner_goal = match heap[arg_addr] {
37        (Tag::Str, pointer) => pointer, // Follow Str to actual goal
38        (Tag::Ref, _) => heap.deref_addr(arg_addr), // Follow Ref chain
39        _ => arg_addr,                  // Direct reference
40    };
41
42    // Create a config with learning disabled - we only want to test if the goal
43    // can be proven with the CURRENT hypothesis, not learn new clauses
44    let mut inner_config = config;
45    inner_config.max_clause = 0; // Disable learning by not allowing new clauses
46
47    let inner_heap = heap.branch(1).pop().unwrap();
48
49    // Clone the current hypothesis so the inner proof can use the learned clauses
50    // This is essential: we need to test if the inner goal succeeds given what
51    // we've already learned. If it does, this hypothesis is bad and we backtrack.
52    let hypothesis_clone = hypothesis.clone();
53    let mut inner_proof = Proof::with_hypothesis(inner_heap, &[inner_goal], hypothesis_clone);
54
55    if config.debug {
56        eprintln!(
57            "[NEGATE] {} with {} hypothesis clauses",
58            inner_proof.heap.term_string(inner_goal),
59            inner_proof.hypothesis.len()
60        );
61    }
62
63    // Try to prove the inner goal with the current hypothesis
64    // If it succeeds, not/1 fails (the hypothesis entails something it shouldn't)
65    // If it fails, not/1 succeeds (the hypothesis correctly doesn't entail this)
66    if inner_proof.prove(predicate_table, inner_config) {
67        if config.debug {
68            eprintln!(
69                "[FAILED_TO_NEGATE] {}",
70                inner_proof.heap.term_string(inner_goal)
71            );
72        }
73        PredReturn::False
74    } else {
75        if config.debug {
76            eprintln!(
77                "[NEGATED_THROUGH_FAILURE] {}",
78                inner_proof.heap.term_string(inner_goal)
79            );
80        }
81        PredReturn::True
82    }
83}
prolog2/predicate_modules/meta_predicates.rs

prolog2/predicate_modules/
meta_predicates.rs
