From 35c71b7add0a8329028382292ade4b470fea7204 Mon Sep 17 00:00:00 2001 From: Fabian Thorand Date: Sun, 24 Nov 2024 13:40:21 +0100 Subject: [PATCH 1/6] Introduce cut term --- src/ast.rs | 5 +++++ src/resolve/arithmetic.rs | 5 ++++- src/search.rs | 4 +++- src/term_arena.rs | 11 +++++++++++ src/textual/lexer.rs | 3 +++ src/textual/pretty.rs | 1 + 6 files changed, 27 insertions(+), 2 deletions(-) diff --git a/src/ast.rs b/src/ast.rs index d3f6679..7a8cc66 100644 --- a/src/ast.rs +++ b/src/ast.rs @@ -78,6 +78,10 @@ pub enum Term { App(AppTerm), /// A signed 64-bit integer Int(i64), + /// The special built-in cut predicate. + /// + /// Evaluating it prunes all further choices for the currently active rule. + Cut, } impl Term { @@ -91,6 +95,7 @@ impl Term { Term::Var(v) => v.0 + 1, Term::App(app) => app.count_var_slots(), Term::Int(_) => 0, + Term::Cut => 0, } } } diff --git a/src/resolve/arithmetic.rs b/src/resolve/arithmetic.rs index ce950ee..f0c98c1 100644 --- a/src/resolve/arithmetic.rs +++ b/src/resolve/arithmetic.rs @@ -84,6 +84,8 @@ impl ArithmeticResolver { Some(ret) } Term::Int(i) => Some(i), + // TODO: log: any other term is an error + _ => None, } } @@ -108,7 +110,8 @@ impl ArithmeticResolver { .then_some(Resolved::Success) } Term::Int(left_val) => (left_val == right_val).then_some(Resolved::Success), - Term::App(_) => None, + // TODO: log invalid terms + _ => None, } } } diff --git a/src/search.rs b/src/search.rs index e2045dc..1c62345 100644 --- a/src/search.rs +++ b/src/search.rs @@ -266,7 +266,7 @@ impl SolutionIter { term_arena::Term::App(app) => self.resolver.resolve(goal_id, app, &mut context), // Other terms are an error _ => { - // TODO: log + // TODO: log invalid goal term None } }; @@ -490,6 +490,7 @@ impl SolutionState { } // Primitive values cannot contain variables term_arena::Term::Int(_) => {} + term_arena::Term::Cut => {} } match self.occurs_stack.pop() { // More terms to check @@ -533,6 +534,7 @@ impl SolutionState { } term_arena::Term::App(app) => ast::Term::App(self.extract_app_term(app)), term_arena::Term::Int(i) => ast::Term::Int(i), + term_arena::Term::Cut => ast::Term::Cut, } } diff --git a/src/term_arena.rs b/src/term_arena.rs index 4fb18c9..24ba7ea 100644 --- a/src/term_arena.rs +++ b/src/term_arena.rs @@ -121,6 +121,13 @@ impl TermArena { term } + /// Allocate a new cut term. + pub fn cut(&mut self) -> TermId { + let term = TermId(self.terms.len()); + self.terms.push(Term::Cut); + term + } + /// Copy terms from another "blueprint" arena into this arena, and apply an offset to all the /// variable indices used inside the blueprint. /// @@ -178,6 +185,7 @@ impl TermArena { }, )), Term::Int(i) => Term::Int(*i), + Term::Cut => Term::Cut, })); self.args.extend( blueprint @@ -201,6 +209,7 @@ impl TermArena { ast::Term::Var(v) => self.var(*v), ast::Term::App(app) => self.insert_ast_appterm(scratch, app), ast::Term::Int(i) => self.int(*i), + ast::Term::Cut => self.cut(), } } @@ -357,6 +366,8 @@ pub enum Term { App(AppTerm), /// A signed 64-bit integer Int(i64), + /// Prune all further alternatives down to the level of the goal that the cut appeared in. + Cut, } /// An application term of the form `foo(arg1, arg2, arg3, ...)` that is part of a [`TermArena`]. diff --git a/src/textual/lexer.rs b/src/textual/lexer.rs index faaf81d..bfa6d67 100644 --- a/src/textual/lexer.rs +++ b/src/textual/lexer.rs @@ -30,6 +30,9 @@ pub enum Token { #[regex("[+-]?[0-9]+", parse_int)] Int(i64), + #[token("!")] + Cut, + // We can also use this variant to define whitespace, // or any other matches we wish to skip. #[regex(r"[ \t\n\f]+", logos::skip)] diff --git a/src/textual/pretty.rs b/src/textual/pretty.rs index 9bcc9c8..b432aee 100644 --- a/src/textual/pretty.rs +++ b/src/textual/pretty.rs @@ -47,6 +47,7 @@ impl<'a> Prettifier<'a> { } Term::App(app) => self.pretty_app(writer, app, scope), Term::Int(int) => write!(writer, "{int}"), + Term::Cut => write!(writer, "!"), } } From df327fe904bb450edd3f11ef94bc74a6ac19378f Mon Sep 17 00:00:00 2001 From: Fabian Thorand Date: Sun, 24 Nov 2024 14:09:46 +0100 Subject: [PATCH 2/6] Allow cut and variables to appear in parsed terms --- src/ast.rs | 32 ++++++++++++++++++++------------ src/lib.rs | 2 +- src/search.rs | 2 +- src/search/test.rs | 14 +++++++------- src/textual/parser.rs | 43 ++++++++++++++++++++++++++++++------------- src/textual/pretty.rs | 6 +++--- src/universe.rs | 2 +- 7 files changed, 63 insertions(+), 38 deletions(-) diff --git a/src/ast.rs b/src/ast.rs index 7a8cc66..8e76c7a 100644 --- a/src/ast.rs +++ b/src/ast.rs @@ -187,7 +187,7 @@ pub struct Rule { pub head: AppTerm, /// The terms that need to hold for the `head` to become true. If the tail is empty, then the /// head is always true. The rule is then called a fact. - pub tail: Vec, + pub tail: Vec, /// Names of the variables used in this rule pub scope: Option, } @@ -213,7 +213,7 @@ impl Rule { functor: pred, args, }; - self.tail.push(app_term); + self.tail.push(Term::App(app_term)); self } } @@ -232,14 +232,14 @@ impl Rule { /// let female = Sym::from_ord(1); /// let bob = Sym::from_ord(2); /// let rule = exists(|[x]| -/// Query::single(grandparent, vec![bob.into(), x.into()]) -/// .and(female, vec![x.into()]) +/// Query::single_app(grandparent, vec![bob.into(), x.into()]) +/// .and_app(female, vec![x.into()]) /// ); /// ``` #[derive(Debug, Clone, PartialEq, Eq)] pub struct Query { /// The conunctive goals that need to be proven as part of this query. - pub goals: Vec, + pub goals: Vec, /// Names of the variables used in this query pub scope: Option, } @@ -251,22 +251,30 @@ impl Query { } /// A query consisting of a set of goals. - pub fn new(goals: Vec, scope: Option) -> Query { + pub fn new(goals: Vec, scope: Option) -> Query { Query { goals, scope } } /// A query with just a single goal. - pub fn single(pred: Sym, args: Vec) -> Query { - Query::new(vec![AppTerm::new(pred, args)], None) + pub fn single_app(pred: Sym, args: Vec) -> Query { + Query::single(Term::App(AppTerm::new(pred, args))) + } + + /// A query with just a single goal. + pub fn single(pred: Term) -> Query { + Query::new(vec![pred], None) } /// Add another goal to this query. - pub fn and(mut self, pred: Sym, args: Vec) -> Self { - let app_term = AppTerm { + pub fn and_app(self, pred: Sym, args: Vec) -> Self { + self.and(Term::App(AppTerm { functor: pred, args, - }; - self.goals.push(app_term); + })) + } + + pub fn and(mut self, pred: Term) -> Self { + self.goals.push(pred); self } diff --git a/src/lib.rs b/src/lib.rs index fceec06..7ec7bab 100644 --- a/src/lib.rs +++ b/src/lib.rs @@ -111,7 +111,7 @@ //! # .when(add, vec![p.into(), q.into(), r.into()]) //! # })); //! let query = ast::exists(|[x]| { -//! ast::Query::single( +//! ast::Query::single_app( //! add, //! vec![ //! x.into(), diff --git a/src/search.rs b/src/search.rs index 1c62345..2043779 100644 --- a/src/search.rs +++ b/src/search.rs @@ -35,7 +35,7 @@ pub fn query_dfs(resolver: R, query: &Query) -> SolutionIter { .goals .iter() .rev() // reverse so that the leftmost goal ends up on the top of the stack - .map(|app| solution.terms.insert_ast_appterm(&mut scratch, app)) + .map(|app| solution.terms.insert_ast_term(&mut scratch, app)) .collect(), checkpoints: vec![], solution, diff --git a/src/search/test.rs b/src/search/test.rs index 7f7e34f..139a97b 100644 --- a/src/search/test.rs +++ b/src/search/test.rs @@ -57,7 +57,7 @@ fn genealogy() { // query all known grandparents of eve let solutions = query_dfs( &mut resolver, - &exists(|[x]| Query::single(grandparent, vec![x.into(), eve.into()])), + &exists(|[x]| Query::single_app(grandparent, vec![x.into(), eve.into()])), ); assert_eq!( solutions.collect::>(), @@ -67,7 +67,7 @@ fn genealogy() { // query all grandchildren of bob let solutions = query_dfs( &mut resolver, - &exists(|[x]| Query::single(grandparent, vec![bob.into(), x.into()])), + &exists(|[x]| Query::single_app(grandparent, vec![bob.into(), x.into()])), ); assert_eq!( solutions.collect::>(), @@ -77,7 +77,7 @@ fn genealogy() { // query all siblings of eve let solutions = query_dfs( &mut resolver, - &exists(|[x]| Query::single(siblings, vec![eve.into(), x.into()])), + &exists(|[x]| Query::single_app(siblings, vec![eve.into(), x.into()])), ); assert_eq!( solutions.collect::>(), @@ -142,14 +142,14 @@ fn arithmetic() { // query all zero numbers let solutions = query_dfs( &mut resolver, - &exists(|[x]| Query::single(is_zero, vec![x.into()])), + &exists(|[x]| Query::single_app(is_zero, vec![x.into()])), ); assert_eq!(solutions.collect::>(), vec![vec![Some(z.into())],]); // query the first natural numbers let solutions = query_dfs( &mut resolver, - &exists(|[x]| Query::single(is_natural, vec![x.into()])), + &exists(|[x]| Query::single_app(is_natural, vec![x.into()])), ); assert_eq!( solutions.take(3).collect::>(), @@ -164,7 +164,7 @@ fn arithmetic() { let solutions = query_dfs( &mut resolver, &exists(|[x]| { - Query::single( + Query::single_app( add, vec![ ast::app(s, vec![ast::app(s, vec![z.into()])]), @@ -186,7 +186,7 @@ fn arithmetic() { let solutions = query_dfs( &mut resolver, &exists(|[x]| { - Query::single( + Query::single_app( add, vec![ x.into(), diff --git a/src/textual/parser.rs b/src/textual/parser.rs index 11c9774..d6bc5e7 100644 --- a/src/textual/parser.rs +++ b/src/textual/parser.rs @@ -71,11 +71,24 @@ pub enum ParseErrorKind { /// The parser reached the end of the input, but expected more tokens to follow. UnexpectedEof, /// The parser encountered a token that doesn't belong in that place. - UnexpectedToken, + UnexpectedToken(Token), + /// The parser encountered input that could not be recognized as a token. + UnrecognizedToken, /// The parser encountered more tokens after the input should have ended. ExpectedEof, } +impl ParseErrorKind { + /// Translate an unexpected item in the token stream (either an unexpected token or a lexer + /// error) into the matching [`ParseErrorKind`]. + pub fn unexpected(res: Result) -> Self { + match res { + Ok(tok) => Self::UnexpectedToken(tok), + Err(()) => Self::UnrecognizedToken, + } + } +} + /// A parser for terms using the Prolog-like syntax of the /// [TextualUniverse](super::TextualUniverse). pub struct Parser<'u> { @@ -127,9 +140,9 @@ impl<'a> Parser<'a> { tokens.advance(); Vec::new() } - Some(_) => { + Some(other) => { let (_, span) = tokens.next().unwrap(); - return Err(ParseError::new(span, ParseErrorKind::UnexpectedToken)); + return Err(ParseError::new(span, ParseErrorKind::unexpected(other))); } None => return Err(ParseError::new(tokens.eof(), ParseErrorKind::UnexpectedEof)), }; @@ -144,21 +157,21 @@ impl<'a> Parser<'a> { &mut self, tokens: &mut TokenStream, scope: &mut VarScope, - ) -> Result, ParseError> { - let mut goals = vec![self.parse_appterm(tokens, scope)?]; + ) -> Result, ParseError> { + let mut goals = vec![self.parse_term(tokens, scope)?]; loop { match tokens.peek_token() { Some(Ok(Token::Comma)) => { tokens.advance(); - goals.push(self.parse_appterm(tokens, scope)?); + goals.push(self.parse_term(tokens, scope)?); } Some(Ok(Token::Period)) => { tokens.advance(); break; } - Some(_) => { + Some(other) => { let (_, span) = tokens.next().unwrap(); - return Err(ParseError::new(span, ParseErrorKind::UnexpectedToken)); + return Err(ParseError::new(span, ParseErrorKind::unexpected(other))); } None => return Err(ParseError::new(tokens.eof(), ParseErrorKind::UnexpectedEof)), } @@ -167,8 +180,8 @@ impl<'a> Parser<'a> { } fn expect_eof(&mut self, tokens: &mut TokenStream) -> Result<(), ParseError> { - if let Some((_, span)) = tokens.next() { - Err(ParseError::new(span, ParseErrorKind::UnexpectedToken)) + if let Some((other, span)) = tokens.next() { + Err(ParseError::new(span, ParseErrorKind::unexpected(other))) } else { Ok(()) } @@ -183,7 +196,7 @@ impl<'a> Parser<'a> { if actual == Ok(expected) { Ok(span) } else { - Err(ParseError::new(span, ParseErrorKind::UnexpectedToken)) + Err(ParseError::new(span, ParseErrorKind::unexpected(actual))) } } else { Err(ParseError::new(tokens.eof(), ParseErrorKind::UnexpectedEof)) @@ -209,9 +222,9 @@ impl<'a> Parser<'a> { tokens.advance(); break; } - Some(_) => { + Some(other) => { let (_, span) = tokens.next().unwrap(); - return Err(ParseError::new(span, ParseErrorKind::UnexpectedToken)); + return Err(ParseError::new(span, ParseErrorKind::unexpected(other))); } None => { return Err(ParseError::new(tokens.eof(), ParseErrorKind::UnexpectedEof)) @@ -237,6 +250,10 @@ impl<'a> Parser<'a> { tokens.advance(); Ok(Term::Int(i)) } + Some(Ok(Token::Cut)) => { + tokens.advance(); + Ok(Term::Cut) + } _ => self.parse_appterm(tokens, scope).map(Term::App), } } diff --git a/src/textual/pretty.rs b/src/textual/pretty.rs index b432aee..e8d3b0e 100644 --- a/src/textual/pretty.rs +++ b/src/textual/pretty.rs @@ -89,14 +89,14 @@ impl<'a> Prettifier<'a> { pub fn pretty_conjunction( &self, writer: &mut W, - goals: &[AppTerm], + goals: &[Term], scope: Option<&VarScope>, ) -> std::fmt::Result { if let Some((first, rest)) = goals.split_first() { - self.pretty_app(writer, first, scope)?; + self.pretty(writer, first, scope)?; for arg in rest { write!(writer, ", ")?; - self.pretty_app(writer, arg, scope)?; + self.pretty(writer, arg, scope)?; } } write!(writer, ".")?; diff --git a/src/universe.rs b/src/universe.rs index 1dee7e1..308c5fd 100644 --- a/src/universe.rs +++ b/src/universe.rs @@ -144,7 +144,7 @@ impl CompiledRule { let tail = rule .tail .iter() - .map(|tail| tail_blueprint.insert_ast_appterm(&mut scratch, tail)) + .map(|tail| tail_blueprint.insert_ast_term(&mut scratch, tail)) .collect(); CompiledRule { head_blueprint, From 348a4284bb994f506416b2ae1c67dbf58d89ddc0 Mon Sep 17 00:00:00 2001 From: Fabian Thorand Date: Sun, 24 Nov 2024 14:32:56 +0100 Subject: [PATCH 3/6] Implement support for cut in solver --- src/search.rs | 67 +++++++++++++++++++++++++++++++++++++++++---------- 1 file changed, 54 insertions(+), 13 deletions(-) diff --git a/src/search.rs b/src/search.rs index 2043779..a0b5a9a 100644 --- a/src/search.rs +++ b/src/search.rs @@ -10,7 +10,7 @@ mod test; use crate::{ ast::{self, Query, Var}, - term_arena::{self, TermArena}, + term_arena::{self, TermArena, TermId}, }; /// Solve queries against the universe using a depth-first-search. @@ -36,6 +36,8 @@ pub fn query_dfs(resolver: R, query: &Query) -> SolutionIter { .iter() .rev() // reverse so that the leftmost goal ends up on the top of the stack .map(|app| solution.terms.insert_ast_term(&mut scratch, app)) + // the initial cut-level is 0 + .map(|goal| (goal, 0)) .collect(), checkpoints: vec![], solution, @@ -65,9 +67,10 @@ pub trait Resolver { /// The interface into the search state that is provided to a [`Resolver`] for resolving goals. pub struct ResolveContext<'c> { solution: &'c mut SolutionState, - goal_stack: &'c mut Vec, + goal_stack: &'c mut Vec<(term_arena::TermId, usize)>, checkpoint: &'c SolutionCheckpoint, goal_len: usize, + cut_level: usize, } impl<'c> ResolveContext<'c> { @@ -86,14 +89,15 @@ impl<'c> ResolveContext<'c> { /// Push an additional goal to the stack, to be resolved later. #[inline(always)] pub fn push_goal(&mut self, goal: term_arena::TermId) { - self.goal_stack.push(goal); + self.goal_stack.push((goal, self.cut_level)); } /// Extend the goal stack from the provided iterator. The last item will end up on top of the /// stack, and thus the next goal to be resolved. #[inline(always)] pub fn extend_goals(&mut self, new_goals: impl Iterator) { - self.goal_stack.extend(new_goals); + let level = self.cut_level; + self.goal_stack.extend(new_goals.map(|goal| (goal, level))); } /// Reset the solution state to the current choice point. @@ -156,7 +160,7 @@ pub struct SolutionIter { /// The rule database that can be used for resolving queries. resolver: R, /// Goals that still need to be solved - unresolved_goals: Vec, + unresolved_goals: Vec<(term_arena::TermId, usize)>, /// Checkpoints created for past decisions, used for backtracking checkpoints: Vec>, /// Current (partial) solution @@ -177,6 +181,9 @@ struct Checkpoint { /// Checkpoint of the partial solution to undo any assignments that have been made since this /// choice point. solution_checkpoint: SolutionCheckpoint, + /// The cut-level associated with this checkpoint. Determined by the context in which it was + /// executed. + cut_level: usize, } /// Status of the solution iterator after performing a step. @@ -221,7 +228,7 @@ impl SolutionIter { /// # .when(is_natural, vec![p.into()]) /// # })); /// # let query = ast::exists(|[x]| { - /// # ast::Query::single( + /// # ast::Query::single_app( /// # add, /// # vec![ /// # x.into(), @@ -248,9 +255,9 @@ impl SolutionIter { pub fn step(&mut self) -> Step { // When there are still unresolved goals left, we create a choice checkpoint for the // top-most one. - if let Some(goal) = self.unresolved_goals.pop() { + if let Some((goal_id, current_cut_level)) = self.unresolved_goals.pop() { // resolve goal - let (goal_id, goal_term) = self.solution.follow_vars(goal); + let goal_term = self.solution.terms.get_term(goal_id); let solution_checkpoint = self.solution.checkpoint(); let goals_checkpoint = self.unresolved_goals.len(); let mut context = ResolveContext { @@ -258,12 +265,28 @@ impl SolutionIter { goal_stack: &mut self.unresolved_goals, checkpoint: &solution_checkpoint, goal_len: goals_checkpoint, + cut_level: self.checkpoints.len(), }; let resolved = match goal_term { - // Unbound variables are vacuously true - term_arena::Term::Var(_) => Some(Resolved::Success), + // Variables are an implicit call to the predicate they are bound to + term_arena::Term::Var(v) => { + if let Some(new_goal) = context.solution.get_var(v) { + // Replace goal + context.push_goal(new_goal); + } + // Unbound variables are vacuously true + Some(Resolved::Success) + } // App terms are resolved term_arena::Term::App(app) => self.resolver.resolve(goal_id, app, &mut context), + // Cut prunes the search alternatives down to `current_cut_level` + term_arena::Term::Cut => { + // Remove choices from all checkpoints between current_cut_level and the top: + for checkpoint in self.checkpoints[current_cut_level..].iter_mut() { + checkpoint.choice = None; + } + Some(Resolved::Success) + } // Other terms are an error _ => { // TODO: log invalid goal term @@ -273,7 +296,7 @@ impl SolutionIter { let choice = match resolved { None => { // Restore before state - self.unresolved_goals.push(goal_id); + self.unresolved_goals.push((goal_id, current_cut_level)); // Then resume from current checkpoint return self.resume_or_backtrack(); } @@ -284,10 +307,11 @@ impl SolutionIter { // At this point, the goal was successfully resolved self.checkpoints.push(Checkpoint { - goal, + goal: goal_id, choice, solution_checkpoint, goals_checkpoint, + cut_level: current_cut_level, }); self.yield_or_continue() } else { @@ -330,6 +354,7 @@ impl SolutionIter { .last_mut() .expect("invariant: there is always a checkpoint when this is called"); + // Any goals resulting from choices on this checkpoint inherit the current cut-level. let success = match &mut checkpoint.choice { None => false, Some(choice) => { @@ -338,6 +363,7 @@ impl SolutionIter { goal_stack: &mut self.unresolved_goals, checkpoint: &checkpoint.solution_checkpoint, goal_len: checkpoint.goals_checkpoint, + cut_level: checkpoint.cut_level, }; self.resolver.resume(choice, checkpoint.goal, &mut context) } @@ -348,7 +374,8 @@ impl SolutionIter { } else { // checkpoint exhausted, discard checkpoint and put goal back let discarded = self.checkpoints.pop().expect("we know there is one here"); - self.unresolved_goals.push(discarded.goal); + self.unresolved_goals + .push((discarded.goal, discarded.cut_level)); false } } @@ -469,6 +496,20 @@ impl SolutionState { true } + /// Return the term assigned to a variable, or `None` if the variable is unbound. + /// + /// Similar to [`SolutionState::follow_vars`], but intended for directly reading the value of a + /// variable, rather than simply resolving any bound variables. + pub fn get_var(&self, mut var: Var) -> Option { + while let Some(term) = self.variables[var.ord()] { + match self.terms.get_term(term) { + term_arena::Term::Var(next) => var = next, + _ => return Some(term), + } + } + None + } + /// Check whether the variable occurs inside the given term. fn occurs(&mut self, var: Var, mut term: term_arena::TermId) -> bool { loop { From e4098b2390121657f9d2ab1c8a6dc01dddadaa58 Mon Sep 17 00:00:00 2001 From: Fabian Thorand Date: Sun, 24 Nov 2024 14:51:19 +0100 Subject: [PATCH 4/6] Add tests for cut behavior --- src/search/test.rs | 62 ++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 62 insertions(+) diff --git a/src/search/test.rs b/src/search/test.rs index 139a97b..7259818 100644 --- a/src/search/test.rs +++ b/src/search/test.rs @@ -1,4 +1,5 @@ use super::*; +use crate::textual::TextualUniverse; use crate::{ast::*, RuleResolver, RuleSet, SymbolStore}; #[test] @@ -201,3 +202,64 @@ fn arithmetic() { vec![vec![Some(ast::app(s, vec![z.into()]))],] ); } + +#[test] +fn cut() { + let mut tu = TextualUniverse::new(); + tu.load_str( + r" + foo(hello). + foo(world). + + world_or_baz(world). + world_or_baz(baz). + + once(X) :- X, !. + + not(X) :- X, !, fail. + not(X). + + bar(X) :- foo(X), !. + bar(baz). + ", + ) + .unwrap(); + + #[track_caller] + fn assert_solutions(tu: &mut TextualUniverse, query: &str, solutions: &[&[Option<&str>]]) { + let query = tu.prepare_query(query).unwrap(); + let rets: Vec<_> = query_dfs(tu.resolver(), &query).collect(); + let pretty_solutions: Vec<_> = rets + .into_iter() + .map(|sol| { + sol.into_iter() + .map(|var| { + var.map(|term| tu.pretty().term_to_string(&term, query.scope.as_ref())) + }) + .collect::>() + }) + .collect(); + let expected_solutions = solutions + .iter() + .map(|sol| { + sol.iter() + .map(|var| var.as_ref().map(|str| str.to_string())) + .collect::>() + }) + .collect::>(); + + assert_eq!(pretty_solutions, expected_solutions); + } + + assert_solutions(&mut tu, "foo(X), !.", &[&[Some("hello")]]); + assert_solutions(&mut tu, "once(foo(X)).", &[&[Some("hello")]]); + assert_solutions(&mut tu, "bar(X).", &[&[Some("hello")]]); + assert_solutions(&mut tu, "bar(baz).", &[&[]]); + assert_solutions( + &mut tu, + "world_or_baz(X), bar(X).", + &[&[Some("world")], &[Some("baz")]], + ); + assert_solutions(&mut tu, "not(foo(bla)).", &[&[]]); + assert_solutions(&mut tu, "not(foo(hello)).", &[]); +} From ce9f97186c25fc80325c207e99890994d61fa410 Mon Sep 17 00:00:00 2001 From: Fabian Thorand Date: Sun, 24 Nov 2024 20:14:26 +0100 Subject: [PATCH 5/6] Improve code structure of cut handling --- src/search.rs | 63 +++++++++++++++++++++++++++++++++++++-------------- 1 file changed, 46 insertions(+), 17 deletions(-) diff --git a/src/search.rs b/src/search.rs index a0b5a9a..47b7fbd 100644 --- a/src/search.rs +++ b/src/search.rs @@ -36,8 +36,7 @@ pub fn query_dfs(resolver: R, query: &Query) -> SolutionIter { .iter() .rev() // reverse so that the leftmost goal ends up on the top of the stack .map(|app| solution.terms.insert_ast_term(&mut scratch, app)) - // the initial cut-level is 0 - .map(|goal| (goal, 0)) + .map(|goal| GoalFrame { goal, cut_level: 0 }) .collect(), checkpoints: vec![], solution, @@ -67,7 +66,7 @@ pub trait Resolver { /// The interface into the search state that is provided to a [`Resolver`] for resolving goals. pub struct ResolveContext<'c> { solution: &'c mut SolutionState, - goal_stack: &'c mut Vec<(term_arena::TermId, usize)>, + goal_stack: &'c mut Vec, checkpoint: &'c SolutionCheckpoint, goal_len: usize, cut_level: usize, @@ -89,7 +88,10 @@ impl<'c> ResolveContext<'c> { /// Push an additional goal to the stack, to be resolved later. #[inline(always)] pub fn push_goal(&mut self, goal: term_arena::TermId) { - self.goal_stack.push((goal, self.cut_level)); + self.goal_stack.push(GoalFrame { + goal, + cut_level: self.cut_level, + }); } /// Extend the goal stack from the provided iterator. The last item will end up on top of the @@ -97,7 +99,10 @@ impl<'c> ResolveContext<'c> { #[inline(always)] pub fn extend_goals(&mut self, new_goals: impl Iterator) { let level = self.cut_level; - self.goal_stack.extend(new_goals.map(|goal| (goal, level))); + self.goal_stack.extend(new_goals.map(|goal| GoalFrame { + goal, + cut_level: level, + })); } /// Reset the solution state to the current choice point. @@ -160,7 +165,7 @@ pub struct SolutionIter { /// The rule database that can be used for resolving queries. resolver: R, /// Goals that still need to be solved - unresolved_goals: Vec<(term_arena::TermId, usize)>, + unresolved_goals: Vec, /// Checkpoints created for past decisions, used for backtracking checkpoints: Vec>, /// Current (partial) solution @@ -186,6 +191,29 @@ struct Checkpoint { cut_level: usize, } +impl Checkpoint { + /// Restore the original [`GoalFrame`] from this checkpoint, used for backtracking. + fn restore_goal_frame(self) -> GoalFrame { + GoalFrame { + goal: self.goal, + cut_level: self.cut_level, + } + } +} + +/// A goal associated with extra information. +/// +/// NOTE: When we need more information, it may no longer be practical to store frames inline, and +/// we may instead want to store the associated data in a deduplicated, refcounted manner. +#[derive(Debug)] +struct GoalFrame { + /// The goal-term to solve + goal: term_arena::TermId, + /// The checkpoint index at which this goal was introduced. Used for search-space pruning via + /// [`term_arena::Term::Cut`]. + cut_level: usize, +} + /// Status of the solution iterator after performing a step. /// /// See [SolutionIter::step] for a usage example. @@ -255,9 +283,9 @@ impl SolutionIter { pub fn step(&mut self) -> Step { // When there are still unresolved goals left, we create a choice checkpoint for the // top-most one. - if let Some((goal_id, current_cut_level)) = self.unresolved_goals.pop() { + if let Some(goal_frame) = self.unresolved_goals.pop() { // resolve goal - let goal_term = self.solution.terms.get_term(goal_id); + let goal_term = self.solution.terms.get_term(goal_frame.goal); let solution_checkpoint = self.solution.checkpoint(); let goals_checkpoint = self.unresolved_goals.len(); let mut context = ResolveContext { @@ -278,11 +306,13 @@ impl SolutionIter { Some(Resolved::Success) } // App terms are resolved - term_arena::Term::App(app) => self.resolver.resolve(goal_id, app, &mut context), - // Cut prunes the search alternatives down to `current_cut_level` + term_arena::Term::App(app) => { + self.resolver.resolve(goal_frame.goal, app, &mut context) + } + // Cut prunes the search alternatives down to the current goal's cut level term_arena::Term::Cut => { - // Remove choices from all checkpoints between current_cut_level and the top: - for checkpoint in self.checkpoints[current_cut_level..].iter_mut() { + // Remove choices from all checkpoints between current cut level and the top: + for checkpoint in self.checkpoints[goal_frame.cut_level..].iter_mut() { checkpoint.choice = None; } Some(Resolved::Success) @@ -296,7 +326,7 @@ impl SolutionIter { let choice = match resolved { None => { // Restore before state - self.unresolved_goals.push((goal_id, current_cut_level)); + self.unresolved_goals.push(goal_frame); // Then resume from current checkpoint return self.resume_or_backtrack(); } @@ -307,11 +337,11 @@ impl SolutionIter { // At this point, the goal was successfully resolved self.checkpoints.push(Checkpoint { - goal: goal_id, + goal: goal_frame.goal, choice, solution_checkpoint, goals_checkpoint, - cut_level: current_cut_level, + cut_level: goal_frame.cut_level, }); self.yield_or_continue() } else { @@ -374,8 +404,7 @@ impl SolutionIter { } else { // checkpoint exhausted, discard checkpoint and put goal back let discarded = self.checkpoints.pop().expect("we know there is one here"); - self.unresolved_goals - .push((discarded.goal, discarded.cut_level)); + self.unresolved_goals.push(discarded.restore_goal_frame()); false } } From 04eac265ee998420ed3d4627ef83c62c23d4b2d5 Mon Sep 17 00:00:00 2001 From: Fabian Thorand Date: Sun, 24 Nov 2024 20:23:31 +0100 Subject: [PATCH 6/6] Update readme and add example --- README.md | 45 ++++++++++++++++++++++++++++++++++++++------- 1 file changed, 38 insertions(+), 7 deletions(-) diff --git a/README.md b/README.md index 540d917..3012d0a 100644 --- a/README.md +++ b/README.md @@ -7,20 +7,19 @@ ## Overview At the heart of this project is a small, efficient Rust library for solving first-order predicate -logic expressions like they can be found in e.g. Prolog. +logic expressions like they can be found in e.g. Prolog. Compare to the latter, this library is much +more simplistic, though extensible. Additionally, there is a [REPL example](examples/repl.rs) for interactively playing around with the implementation. -Compared to Prolog, it currently lacks some features though. Most notable, there are -- no negation or cut, -- no special built-in types (like integers) - Features that are implemented: - Standard (compound) terms - Named variables & wildcards - DFS-based inference -- Custom predicate resolvers (e.g. with side effects) +- A "cut" operation for pruning the search space +- Integer arithmetic +- Extensibility through custom predicate resolvers (e.g. predicates with side effects) ## Showcase @@ -70,6 +69,38 @@ Found solution: No more solutions. ``` +While there is no standard library, using the cut operation, it is possible to build many of the +common combinators, such as `once`: + +``` +?- :define once(X) :- X, !. +Defined! +``` + +Given a predicate producing multiple choices... + +``` +?- :define foo(hello). foo(world). +Defined! +?- foo(X). +Found solution: + X = hello +Found solution: + X = world +No more solutions. +``` + +..., we can now restrict it to produce only the first choice: + +``` +?- once(foo(X)). +Found solution: + X = hello +No more solutions. +``` + +Other combiantors, like negation, can also be implemented using cut. + ## Rust API The core of the API doesn't work with a textual representation of terms like the REPL does, but @@ -139,7 +170,7 @@ this answer: let solutions = query_dfs( &r, &exists(|[x]| { - Query::single( + Query::single_app( add, vec![ x.into(),