prolog2/program/
hypothesis.rs

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

prolog2/program/
hypothesis.rs
