prolog2/program/
clause.rs

1//! Clause representation and metadata.
2
3use std::ops::{Deref, DerefMut};
4
5use smallvec::SmallVec;
6
7use crate::heap::heap::Heap;
8
9/// Compact 64-bit flag set used to mark meta-variables and constrained variables.
10#[derive(Debug, Clone, Copy, PartialEq, Eq, Default)]
11pub struct BitFlag64(u64);
12
13impl BitFlag64 {
14    pub fn set(&mut self, idx: usize) {
15        self.0 = self.0 | 1 << idx;
16    }
17
18    pub fn _unset(&mut self, idx: usize) {
19        self.0 = self.0 & !(1 << idx);
20    }
21
22    pub fn get(&self, idx: usize) -> bool {
23        self.0 & (1 << idx) != 0
24    }
25}
26
27/// A compiled clause: a list of literal heap addresses with metadata
28/// about which variables are second-order (meta) and which are constrained.
29#[derive(Debug, Clone, Eq, PartialEq)]
30pub struct Clause {
31    literals: SmallVec<[usize; 5]>,
32    pub meta_vars: Option<BitFlag64>,
33    pub constrained_vars: BitFlag64,
34}
35
36impl Clause {
37    fn meta_vars_to_bit_flags(meta_vars: Vec<usize>) -> BitFlag64 {
38        let mut bit_flags = BitFlag64::default();
39        for meta_var in meta_vars {
40            if meta_var > 63 {
41                panic!("Cant have more than 64 variables in meta clause")
42            }
43            bit_flags.set(meta_var);
44        }
45        bit_flags
46    }
47
48    pub fn new(
49        literals: Vec<usize>,
50        meta_vars: Option<Vec<usize>>,
51        constrained_vars: Option<Vec<usize>>,
52    ) -> Self {
53        let meta_vars = meta_vars.map(Self::meta_vars_to_bit_flags);
54        let constrained_vars = match constrained_vars {
55            Some(cv) => Self::meta_vars_to_bit_flags(cv),
56            None => meta_vars.unwrap_or_default(),
57        };
58        let literals: SmallVec<[usize; 5]> = SmallVec::from_vec(literals);
59        Clause {
60            literals,
61            meta_vars,
62            constrained_vars,
63        }
64    }
65
66    pub fn head(&self) -> usize {
67        self[0]
68    }
69
70    pub fn body(&self) -> &[usize] {
71        &self[1..]
72    }
73
74    pub fn meta(&self) -> bool {
75        self.meta_vars.is_some()
76    }
77
78    pub fn meta_var(&self, arg_id: usize) -> Result<bool, &'static str> {
79        let meta_vars = self.meta_vars.ok_or("Clause is not a meta clause")?;
80        Ok(meta_vars.get(arg_id))
81    }
82
83    pub fn constrained_var(&self, arg_id: usize) -> bool {
84        self.constrained_vars.get(arg_id)
85    }
86
87    pub fn normalise_clause_vars(&self, heap: &mut impl Heap) {
88        let mut arg_ids: Vec<usize> = Vec::new();
89        for &literal in self.literals.iter() {
90            heap.normalise_args(literal, &mut arg_ids);
91        }
92    }
93
94    pub fn to_string(&self, heap: &impl Heap) -> String {
95        let mut buffer = format!("{}:-", heap.term_string(self.head()));
96        for body_literal in self.body() {
97            buffer += &heap.term_string(*body_literal);
98            buffer += ","
99        }
100        buffer.pop();
101        buffer += ".";
102        buffer
103    }
104}
105
106impl Deref for Clause {
107    type Target = [usize];
108
109    fn deref(&self) -> &[usize] {
110        &self.literals
111    }
112}
113
114impl DerefMut for Clause {
115    fn deref_mut(&mut self) -> &mut Self::Target {
116        &mut self.literals
117    }
118}
prolog2/program/clause.rs

prolog2/program/
clause.rs
