prolog2/predicate_modules/
meta_predicates.rs

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

prolog2/predicate_modules/
meta_predicates.rs
