prolog2/program/
clause.rs

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

prolog2/program/
clause.rs
