prolog2/program/
hypothesis.rs

1use std::{
2    ops::{Deref, DerefMut},
3    sync::Arc,
4};
5
6use crate::heap::heap::Heap;
7
8use super::clause::Clause;
9
10/// Constraint set for existentially quantified variables in a learned clause.
11pub type Constraints = Arc<[usize]>;
12
13/// A collection of learned clauses produced during proof search.
14///
15/// During MIL resolution, when a second-order clause matches a goal,
16/// a new first-order clause is invented and added to the hypothesis.
17#[derive(Clone)]
18pub struct Hypothesis {
19    clauses: Vec<Clause>,
20    pub constraints: Vec<Constraints>,
21}
22
23impl Hypothesis {
24    pub fn new() -> Self {
25        Hypothesis {
26            clauses: Vec::new(),
27            constraints: Vec::new(),
28        }
29    }
30
31    pub fn len(&self) -> usize {
32        self.clauses.len()
33    }
34
35    pub fn push_clause(&mut self, clause: Clause, constraints: Constraints) {
36        self.clauses.push(clause);
37        self.constraints.push(constraints);
38    }
39
40    pub fn pop_clause(&mut self) -> Clause {
41        self.constraints.pop();
42        self.clauses.pop().unwrap()
43    }
44
45    pub fn to_string(&self, heap: &impl Heap) -> String {
46        let mut buffer = String::new();
47        for clause in &self.clauses {
48            buffer += &clause.to_string(heap);
49            buffer += "\n"
50        }
51        buffer
52    }
53}
54
55impl Deref for Hypothesis {
56    type Target = Vec<Clause>;
57
58    fn deref(&self) -> &Self::Target {
59        &self.clauses
60    }
61}
62
63impl DerefMut for Hypothesis {
64    fn deref_mut(&mut self) -> &mut Self::Target {
65        &mut self.clauses
66    }
67}
prolog2/program/hypothesis.rs

prolog2/program/
hypothesis.rs
