mangle_engine/
naive.rs

1// Copyright 2024 Google LLC
2//
3// Licensed under the Apache License, Version 2.0 (the "License");
4// you may not use this file except in compliance with the License.
5// You may obtain a copy of the License at
6//
7//     http://www.apache.org/licenses/LICENSE-2.0
8//
9// Unless required by applicable law or agreed to in writing, software
10// distributed under the License is distributed on an "AS IS" BASIS,
11// WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
12// See the License for the specific language governing permissions and
13// limitations under the License.
14
15use crate::Engine;
16use crate::Result;
17use crate::ast::{Arena, Atom, BaseTerm, Term};
18use anyhow::anyhow;
19use fxhash::FxHashMap;
20
21pub struct Naive {}
22
23impl<'e> Engine<'e> for Naive {
24    fn eval<'p>(
25        &'e self,
26        store: &'e impl mangle_common::FactStore<'e>,
27        program: &'p mangle_analysis::StratifiedProgram<'p>,
28    ) -> Result<()> {
29        // Initial facts.
30        for pred in program.intensional_preds() {
31            for rule in program.rules(pred) {
32                if rule.premises.is_empty() {
33                    store.add(program.arena(), rule.head)?;
34                }
35            }
36        }
37        loop {
38            let mut fact_added = false;
39            for pred in program.intensional_preds() {
40                for rule in program.rules(pred) {
41                    if rule.premises.is_empty() {
42                        continue; // initial facts added previously
43                    }
44                    let arena = Arena::new_with_global_interner();
45                    let subst: FxHashMap<u32, &BaseTerm> = FxHashMap::default();
46                    let mut all_ok = true;
47                    let subst = std::cell::RefCell::new(subst);
48                    for premise in rule.premises.iter() {
49                        let ok: bool = match premise {
50                            Term::Atom(query) => {
51                                // TODO: eval ApplyFn terms.
52                                let query = query.apply_subst(&arena, &subst.borrow());
53                                let found = std::cell::RefCell::new(false);
54                                let _ = store.get(query.sym, query.args, &|atom: &'_ Atom<'_>| {
55                                    let mut mismatch = false;
56                                    for (i, arg) in query.args.iter().enumerate() {
57                                        match arg {
58                                            BaseTerm::Variable(v) => {
59                                                let own_atom_ref = arena
60                                                    .copy_base_term(store.arena(), atom.args[i]);
61                                                subst.borrow_mut().insert(v.0, own_atom_ref);
62                                            }
63                                            c @ BaseTerm::Const(_) => {
64                                                if *c == atom.args[i] {
65                                                    continue;
66                                                }
67                                                mismatch = true;
68                                                break;
69                                            }
70                                            _ => {
71                                                return Err(anyhow!(format!(
72                                                    "Unsupported term: {arg}"
73                                                )));
74                                            }
75                                        }
76                                    }
77                                    *found.borrow_mut() = !mismatch;
78                                    Ok(())
79                                });
80                                !*found.borrow()
81                            }
82                            Term::NegAtom(query) => {
83                                let query = query.apply_subst(&arena, &subst.borrow());
84
85                                let found = std::cell::RefCell::new(false);
86                                let _ = store.get(query.sym, query.args, &|_| {
87                                    *found.borrow_mut() = true;
88                                    Ok(())
89                                });
90                                !*found.borrow()
91                            }
92                            Term::Eq(left, right) => {
93                                let left = left.apply_subst(&arena, &subst.borrow());
94                                let right = right.apply_subst(&arena, &subst.borrow());
95                                left == right
96                            }
97                            Term::Ineq(left, right) => {
98                                let left = left.apply_subst(&arena, &subst.borrow());
99                                let right = right.apply_subst(&arena, &subst.borrow());
100                                left != right
101                            }
102                        };
103                        if !ok {
104                            all_ok = false;
105                            break;
106                        }
107                    }
108                    if all_ok {
109                        let head = rule.head.apply_subst(&arena, &subst.borrow());
110                        fact_added = store.add(program.arena(), head)?;
111                    }
112                }
113            }
114            if !fact_added {
115                break;
116            }
117        }
118        Ok(())
119    }
120}
121
122#[cfg(test)]
123mod test {
124    use super::*;
125    use crate::ast;
126    use anyhow::Result;
127    use mangle_analysis::Program;
128    use mangle_common::{TableConfig, TableStoreImpl, TableStoreSchema};
129
130    #[test]
131    pub fn test_naive() -> Result<()> {
132        let arena = Arena::new_with_global_interner();
133        let edge = arena.predicate_sym("edge", Some(2));
134        let reachable = arena.predicate_sym("reachable", Some(2));
135        let mut schema: TableStoreSchema = FxHashMap::default();
136        schema.insert(edge, TableConfig::InMemory);
137        schema.insert(reachable, TableConfig::InMemory);
138        let store = TableStoreImpl::new(&arena, &schema);
139
140        use crate::factstore::FactStore;
141        store.add(
142            &arena,
143            arena.atom(
144                edge,
145                &[
146                    &ast::BaseTerm::Const(ast::Const::Number(10)),
147                    &ast::BaseTerm::Const(ast::Const::Number(20)),
148                ],
149            ),
150        )?;
151        store.add(
152            &arena,
153            arena.atom(
154                edge,
155                &[
156                    &ast::BaseTerm::Const(ast::Const::Number(20)),
157                    &ast::BaseTerm::Const(ast::Const::Number(30)),
158                ],
159            ),
160        )?;
161        store.add(
162            &arena,
163            arena.atom(
164                edge,
165                &[
166                    &ast::BaseTerm::Const(ast::Const::Number(30)),
167                    &ast::BaseTerm::Const(ast::Const::Number(40)),
168                ],
169            ),
170        )?;
171
172        let mut simple = Program::new(&arena);
173        // Manually set ext_preds since Program::new doesn't take them anymore?
174        // Wait, Program::new initializes ext_preds to empty. The struct definition shows it as public.
175        simple.ext_preds = vec![edge];
176
177        let head = arena.alloc(ast::Atom {
178            sym: reachable,
179            args: arena.alloc_slice_copy(&[arena.variable("X"), arena.variable("Y")]),
180        });
181        // Add a clause.
182        simple.add_clause(
183            &arena,
184            arena.alloc(ast::Clause {
185                head,
186                premises: arena.alloc_slice_copy(&[arena.alloc(ast::Term::Atom(
187                    arena.atom(edge, &[arena.variable("X"), arena.variable("Y")]),
188                ))]),
189                transform: &[],
190            }),
191        );
192        simple.add_clause(
193            &arena,
194            arena.alloc(ast::Clause {
195                head: arena.atom(reachable, &[arena.variable("X"), arena.variable("Z")]),
196                premises: arena.alloc_slice_copy(&[
197                    arena.alloc(ast::Term::Atom(
198                        arena.atom(edge, &[arena.variable("X"), arena.variable("Y")]),
199                    )),
200                    arena.alloc(ast::Term::Atom(
201                        arena.atom(reachable, &[arena.variable("Y"), arena.variable("X")]),
202                    )),
203                ]),
204                transform: &[],
205            }),
206        );
207
208        let stratified_program = simple.stratify().unwrap();
209
210        let engine = Naive {};
211        engine.eval(&store, &stratified_program)?;
212
213        use crate::factstore::ReadOnlyFactStore;
214        assert!(
215            store
216                .contains(
217                    &arena,
218                    arena.atom(
219                        edge,
220                        &[
221                            &ast::BaseTerm::Const(ast::Const::Number(30)),
222                            &ast::BaseTerm::Const(ast::Const::Number(40))
223                        ],
224                    )
225                )
226                .unwrap()
227        );
228        Ok(())
229    }
230}
mangle_engine/naive.rs

mangle_engine/
naive.rs
