fix group_by_variants/4 and keysort in setof/3 (#1440, #1856)

This commit is contained in:
Mark
2023-07-14 17:01:46 -06:00
parent b6a81c51ab
commit 101d0548db
6 changed files with 95 additions and 16 deletions

View File

@@ -55,6 +55,12 @@ impl AppendOrPrepend {
}
}
#[derive(Debug)]
pub enum VarComparison {
Indistinct,
Distinct
}
#[derive(Debug, Clone, Copy, PartialEq, Eq, Hash)]
pub enum Level {
Deep,

View File

@@ -883,12 +883,45 @@ set_difference([X|Xs], [Y|Ys], Zs) :-
set_difference([], _, []) :- !.
set_difference(Xs, [], Xs).
% variant/2 checks whether X is a variant of Y per the definition in
% 7.1.6.1 of the ISO standard.
:- non_counted_backtracking variant/4.
variant(X,Y,VPs,VPs0) :-
( var(X) ->
var(Y),
VPs = [X-Y|VPs0]
; var(Y) ->
false
; X =.. [FX | XArgs],
Y =.. [FX | YArgs],
lists:foldl('$call'(builtins:variant), XArgs, YArgs, VPs, VPs0)
).
:- non_counted_backtracking variant/2.
singleton([_]).
variant(X, Y) :-
variant(X,Y, VPs, []),
keysort(VPs, SVPs),
pairs:group_pairs_by_key(SVPs, SVPKs),
pairs:pairs_values(SVPKs, Vals),
lists:maplist('$call'(builtins:term_variables), Vals, Vs),
lists:maplist('$call'(builtins:singleton), Vs),
term_variables(Vs, YVars),
lists:length(SVPKs, N),
lists:length(YVars, N).
:- non_counted_backtracking group_by_variant/4.
group_by_variant([V2-S2 | Pairs], V1-S1, [S2 | Solutions], Pairs0) :-
V1 = V2, % \+ \+ (V1 = V2), % (2) % iso_ext:variant(V1, V2), % (1)
variant(V1, V2),
!,
% V1 = V2, % (3)
V1 = V2,
group_by_variant(Pairs, V2-S2, Solutions, Pairs0).
group_by_variant(Pairs, _, [], Pairs).
@@ -1008,7 +1041,7 @@ setof(Template, Goal, Solution) :-
term_variables(TemplateVars+GoalVars, TGVs),
lists:append(TemplateVars, Witnesses0, TGVs),
findall_with_existential(Template, Goal, PairedSolutions0, Witnesses0, Witnesses),
keysort(PairedSolutions0, PairedSolutions),
'$keysort_with_constant_var_ordering'(PairedSolutions0, PairedSolutions), % see 7.2.1
group_by_variants(PairedSolutions, GroupedSolutions),
iterate_variants_and_sort(GroupedSolutions, Witnesses, Solution).

View File

@@ -141,7 +141,7 @@ impl MachineState {
Ok(())
}
fn keysort(&mut self) -> CallResult {
fn keysort(&mut self, var_comparison: VarComparison) -> CallResult {
self.check_keysort_errors()?;
let stub_gen = || functor_stub(atom!("keysort"), 2);
@@ -155,7 +155,7 @@ impl MachineState {
}
key_pairs.sort_by(|a1, a2| {
compare_term_test!(self, a1.0, a2.0).unwrap_or(Ordering::Less)
compare_term_test!(self, a1.0, a2.0, var_comparison).unwrap_or(Ordering::Less)
});
let key_pairs = key_pairs.into_iter().map(|kp| kp.1);
@@ -1437,11 +1437,11 @@ impl Machine {
step_or_fail!(self, self.machine_st.p = self.machine_st.cp);
}
&Instruction::DefaultCallKeySort => {
try_or_throw!(self.machine_st, self.machine_st.keysort());
try_or_throw!(self.machine_st, self.machine_st.keysort(VarComparison::Distinct));
step_or_fail!(self, self.machine_st.p += 1);
}
&Instruction::DefaultExecuteKeySort => {
try_or_throw!(self.machine_st, self.machine_st.keysort());
try_or_throw!(self.machine_st, self.machine_st.keysort(VarComparison::Distinct));
if self.machine_st.fail {
self.machine_st.backtrack();
@@ -1870,7 +1870,7 @@ impl Machine {
}
}
&Instruction::CallKeySort => {
try_or_throw!(self.machine_st, self.machine_st.keysort());
try_or_throw!(self.machine_st, self.machine_st.keysort(VarComparison::Distinct));
if self.machine_st.fail {
self.machine_st.backtrack();
@@ -1884,7 +1884,35 @@ impl Machine {
}
}
&Instruction::ExecuteKeySort => {
try_or_throw!(self.machine_st, self.machine_st.keysort());
try_or_throw!(self.machine_st, self.machine_st.keysort(VarComparison::Distinct));
if self.machine_st.fail {
self.machine_st.backtrack();
} else {
try_or_throw!(
self.machine_st,
(self.machine_st.increment_call_count_fn)(&mut self.machine_st)
);
self.machine_st.p = self.machine_st.cp;
}
}
&Instruction::CallKeySortWithConstantVarOrdering => {
try_or_throw!(self.machine_st, self.machine_st.keysort(VarComparison::Indistinct));
if self.machine_st.fail {
self.machine_st.backtrack();
} else {
try_or_throw!(
self.machine_st,
(self.machine_st.increment_call_count_fn)(&mut self.machine_st)
);
self.machine_st.p += 1;
}
}
&Instruction::ExecuteKeySortWithConstantVarOrdering => {
try_or_throw!(self.machine_st, self.machine_st.keysort(VarComparison::Indistinct));
if self.machine_st.fail {
self.machine_st.backtrack();

View File

@@ -435,7 +435,7 @@ impl MachineState {
}
}
pub fn compare_term_test(&mut self) -> Option<Ordering> {
pub fn compare_term_test(&mut self, var_comparison: VarComparison) -> Option<Ordering> {
let mut tabu_list = IndexSet::new();
while !self.pdl.is_empty() {
@@ -462,12 +462,14 @@ impl MachineState {
match order_cat_v1 {
Some(TermOrderCategory::Variable) => {
let v1 = v1.as_var().unwrap();
let v2 = v2.as_var().unwrap();
if let VarComparison::Distinct = var_comparison {
let v1 = v1.as_var().unwrap();
let v2 = v2.as_var().unwrap();
if v1 != v2 {
self.pdl.clear();
return Some(v1.cmp(&v2));
if v1 != v2 {
self.pdl.clear();
return Some(v1.cmp(&v2));
}
}
}
Some(TermOrderCategory::FloatingPoint) => {

View File

@@ -625,6 +625,12 @@ macro_rules! compare_term_test {
$machine_st.pdl.push($e2);
$machine_st.pdl.push($e1);
$machine_st.compare_term_test()
$machine_st.compare_term_test(VarComparison::Distinct)
}};
($machine_st:expr, $e1:expr, $e2:expr, $var_comparison:expr) => {{
$machine_st.pdl.push($e2);
$machine_st.pdl.push($e1);
$machine_st.compare_term_test($var_comparison)
}};
}