rewrite ground_test, add tests for ground/1 (#2075)
This commit is contained in:
111
src/heap_iter.rs
111
src/heap_iter.rs
@@ -12,6 +12,112 @@ use modular_bitfield::prelude::*;
|
|||||||
use std::ops::Deref;
|
use std::ops::Deref;
|
||||||
use std::vec::Vec;
|
use std::vec::Vec;
|
||||||
|
|
||||||
|
/*
|
||||||
|
* Unlike StackfulPreOrderHeapIter, this iterator not only marks
|
||||||
|
* cyclic terms for the sake of skipping them at the second visit but
|
||||||
|
* leaves them marked until it is dropped. This makes for, e.g., more
|
||||||
|
* efficient ground/1 and term_variables/2 definitions.
|
||||||
|
*/
|
||||||
|
|
||||||
|
pub struct EagerStackfulPreOrderHeapIter<'a> {
|
||||||
|
iter_stack: Vec<HeapCellValue>,
|
||||||
|
mark_stack: Vec<usize>,
|
||||||
|
heap: &'a mut Heap,
|
||||||
|
}
|
||||||
|
|
||||||
|
impl<'a> Drop for EagerStackfulPreOrderHeapIter<'a> {
|
||||||
|
fn drop(&mut self) {
|
||||||
|
while let Some(h) = self.mark_stack.pop() {
|
||||||
|
self.heap[h].set_mark_bit(false);
|
||||||
|
}
|
||||||
|
}
|
||||||
|
}
|
||||||
|
|
||||||
|
impl<'a> EagerStackfulPreOrderHeapIter<'a> {
|
||||||
|
pub fn new(heap: &'a mut Heap, value: HeapCellValue) -> Self {
|
||||||
|
Self {
|
||||||
|
iter_stack: vec![value],
|
||||||
|
mark_stack: vec![],
|
||||||
|
heap,
|
||||||
|
}
|
||||||
|
}
|
||||||
|
|
||||||
|
fn follow(&mut self) -> Option<HeapCellValue> {
|
||||||
|
while let Some(value) = self.iter_stack.pop() {
|
||||||
|
if value.get_mark_bit() {
|
||||||
|
continue;
|
||||||
|
}
|
||||||
|
|
||||||
|
read_heap_cell!(value,
|
||||||
|
(HeapCellValueTag::Str, s) => {
|
||||||
|
if self.heap[s].get_mark_bit() {
|
||||||
|
continue;
|
||||||
|
}
|
||||||
|
|
||||||
|
let arity = cell_as_atom_cell!(self.heap[s]).get_arity();
|
||||||
|
|
||||||
|
self.heap[s].set_mark_bit(true);
|
||||||
|
self.mark_stack.push(s);
|
||||||
|
|
||||||
|
for idx in (s + 1 .. s + arity + 1).rev() {
|
||||||
|
self.iter_stack.push(self.heap[idx]);
|
||||||
|
}
|
||||||
|
}
|
||||||
|
(HeapCellValueTag::Lis, l) => {
|
||||||
|
self.iter_stack.push(self.heap[l+1]);
|
||||||
|
self.iter_stack.push(self.heap[l]);
|
||||||
|
|
||||||
|
self.heap[l].set_mark_bit(true);
|
||||||
|
self.mark_stack.push(l);
|
||||||
|
|
||||||
|
self.heap[l+1].set_mark_bit(true);
|
||||||
|
self.mark_stack.push(l+1);
|
||||||
|
}
|
||||||
|
(HeapCellValueTag::AttrVar | HeapCellValueTag::Var, h) => {
|
||||||
|
let var_value = self.heap[h];
|
||||||
|
|
||||||
|
if !(var_value.is_var() && var_value.get_value() as usize == h) {
|
||||||
|
self.iter_stack.push(self.heap[h]);
|
||||||
|
continue;
|
||||||
|
}
|
||||||
|
}
|
||||||
|
(HeapCellValueTag::PStrLoc, h) => {
|
||||||
|
let h = if self.heap[h].get_tag() == HeapCellValueTag::PStr {
|
||||||
|
h
|
||||||
|
} else {
|
||||||
|
debug_assert_eq!(self.heap[h].get_tag(), HeapCellValueTag::PStrOffset);
|
||||||
|
self.heap[h].get_value() as usize
|
||||||
|
};
|
||||||
|
|
||||||
|
if self.heap[h].get_mark_bit() {
|
||||||
|
continue;
|
||||||
|
}
|
||||||
|
|
||||||
|
self.heap[h].set_mark_bit(true);
|
||||||
|
|
||||||
|
self.iter_stack.push(self.heap[h+1]);
|
||||||
|
self.mark_stack.push(h);
|
||||||
|
}
|
||||||
|
_ => {
|
||||||
|
}
|
||||||
|
);
|
||||||
|
|
||||||
|
return Some(value);
|
||||||
|
}
|
||||||
|
|
||||||
|
None
|
||||||
|
}
|
||||||
|
}
|
||||||
|
|
||||||
|
impl<'a> Iterator for EagerStackfulPreOrderHeapIter<'a> {
|
||||||
|
type Item = HeapCellValue;
|
||||||
|
|
||||||
|
#[inline]
|
||||||
|
fn next(&mut self) -> Option<Self::Item> {
|
||||||
|
self.follow()
|
||||||
|
}
|
||||||
|
}
|
||||||
|
|
||||||
#[derive(BitfieldSpecifier, Clone, Copy, Debug, PartialEq, Eq)]
|
#[derive(BitfieldSpecifier, Clone, Copy, Debug, PartialEq, Eq)]
|
||||||
#[bits = 2]
|
#[bits = 2]
|
||||||
enum IterStackLocTag {
|
enum IterStackLocTag {
|
||||||
@@ -198,11 +304,6 @@ impl<'a, ElideLists> StackfulPreOrderHeapIter<'a, ElideLists> {
|
|||||||
None
|
None
|
||||||
}
|
}
|
||||||
|
|
||||||
#[inline]
|
|
||||||
pub fn stack_len(&self) -> usize {
|
|
||||||
self.stack.len()
|
|
||||||
}
|
|
||||||
|
|
||||||
fn push_if_unmarked(&mut self, loc: IterStackLoc) {
|
fn push_if_unmarked(&mut self, loc: IterStackLoc) {
|
||||||
let cell = self.read_cell_mut(loc);
|
let cell = self.read_cell_mut(loc);
|
||||||
|
|
||||||
|
|||||||
@@ -1621,56 +1621,12 @@ impl MachineState {
|
|||||||
|
|
||||||
// returns true on failure.
|
// returns true on failure.
|
||||||
pub fn ground_test(&mut self) -> bool {
|
pub fn ground_test(&mut self) -> bool {
|
||||||
use fxhash::FxBuildHasher;
|
let iter = EagerStackfulPreOrderHeapIter::new(&mut self.heap, self.registers[1]);
|
||||||
|
|
||||||
if self.registers[1].is_constant() {
|
for term in iter {
|
||||||
return false;
|
if term.is_var() {
|
||||||
}
|
|
||||||
|
|
||||||
let value = self.store(self.deref(self.registers[1]));
|
|
||||||
|
|
||||||
if value.is_stack_var() {
|
|
||||||
return true;
|
|
||||||
}
|
|
||||||
|
|
||||||
let mut visited = IndexSet::with_hasher(FxBuildHasher::default());
|
|
||||||
let mut iter = stackful_preorder_iter::<NonListElider>(&mut self.heap, &mut self.stack, value);
|
|
||||||
let mut stack_len = 0;
|
|
||||||
|
|
||||||
let is_var = |heap: &Heap, value: HeapCellValue| -> bool {
|
|
||||||
let value = unmark_cell_bits!(value);
|
|
||||||
|
|
||||||
if value.is_var() {
|
|
||||||
let value = heap_bound_store(heap, heap_bound_deref(heap, value));
|
|
||||||
|
|
||||||
if value.is_var() {
|
|
||||||
return true;
|
|
||||||
}
|
|
||||||
}
|
|
||||||
|
|
||||||
false
|
|
||||||
};
|
|
||||||
|
|
||||||
while let Some(value) = iter.next() {
|
|
||||||
if is_var(iter.heap, value) {
|
|
||||||
return true;
|
return true;
|
||||||
}
|
}
|
||||||
|
|
||||||
if value.is_ref() {
|
|
||||||
if visited.contains(&value) {
|
|
||||||
while iter.stack_len() > stack_len {
|
|
||||||
if let Some(value) = iter.pop_stack() {
|
|
||||||
if is_var(iter.heap, value) {
|
|
||||||
return true;
|
|
||||||
}
|
|
||||||
}
|
|
||||||
}
|
|
||||||
} else {
|
|
||||||
visited.insert(value);
|
|
||||||
}
|
|
||||||
}
|
|
||||||
|
|
||||||
stack_len = iter.stack_len();
|
|
||||||
}
|
}
|
||||||
|
|
||||||
false
|
false
|
||||||
|
|||||||
83
src/tests/ground.pl
Normal file
83
src/tests/ground.pl
Normal file
@@ -0,0 +1,83 @@
|
|||||||
|
/**/
|
||||||
|
|
||||||
|
:- use_module(library(format)).
|
||||||
|
:- use_module(library(dcgs)).
|
||||||
|
:- use_module(library(lists)).
|
||||||
|
:- use_module(library(debug)).
|
||||||
|
:- use_module(library(atts)).
|
||||||
|
|
||||||
|
:- attribute a/1.
|
||||||
|
|
||||||
|
a(Var) :- put_atts(Var, +a(hello)).
|
||||||
|
|
||||||
|
test("ground#239", (
|
||||||
|
% double negate to avoid residual goal being printed
|
||||||
|
\+ \+ (a(X), var(X), \+ ground(X))
|
||||||
|
)).
|
||||||
|
|
||||||
|
test("ground#1411",(
|
||||||
|
G_0 = ( A=s(A) ), G_0,
|
||||||
|
ground(A), ground(G_0)
|
||||||
|
)).
|
||||||
|
|
||||||
|
test("ground#2065",(
|
||||||
|
A = [B|_C], B = [A], \+ ground(B), \+ground([B])
|
||||||
|
)).
|
||||||
|
|
||||||
|
test("ground#2073",(
|
||||||
|
\+ ground(_-1+_-1),
|
||||||
|
\+ ground(1-1-_)
|
||||||
|
)).
|
||||||
|
|
||||||
|
test("ground#2075",(
|
||||||
|
G_0 = (_,_,ground(_)),
|
||||||
|
G_0 = (D=[D|_],_=D*[],ground(D)),
|
||||||
|
\+ G_0,
|
||||||
|
_=_B*_,_D=_B*_A,_B=_B*_D,\+ ground(_B),
|
||||||
|
A=[A|B],B=A*B,ground(A)
|
||||||
|
)).
|
||||||
|
|
||||||
|
main :-
|
||||||
|
findall(test(Name, Goal), test(Name, Goal), Tests),
|
||||||
|
run_tests(Tests, Failed),
|
||||||
|
show_failed(Failed),
|
||||||
|
halt.
|
||||||
|
|
||||||
|
main_quiet :-
|
||||||
|
findall(test(Name, Goal), test(Name, Goal), Tests),
|
||||||
|
run_tests_quiet(Tests, Failed),
|
||||||
|
( Failed = [] ->
|
||||||
|
format("All tests passed", [])
|
||||||
|
; format("Some tests failed", [])
|
||||||
|
),
|
||||||
|
halt.
|
||||||
|
|
||||||
|
run_tests([], []).
|
||||||
|
run_tests([test(Name, Goal)|Tests], Failed) :-
|
||||||
|
format("Running test \"~s\"~n", [Name]),
|
||||||
|
( call(Goal) ->
|
||||||
|
Failed = Failed1
|
||||||
|
; format("Failed test \"~s\"~n", [Name]),
|
||||||
|
Failed = [Name|Failed1]
|
||||||
|
),
|
||||||
|
run_tests(Tests, Failed1).
|
||||||
|
|
||||||
|
run_tests_quiet([], []).
|
||||||
|
run_tests_quiet([test(Name, Goal)|Tests], Failed) :-
|
||||||
|
( call(Goal) ->
|
||||||
|
Failed = Failed1
|
||||||
|
; Failed = [Name|Failed1]
|
||||||
|
),
|
||||||
|
run_tests_quiet(Tests, Failed1).
|
||||||
|
|
||||||
|
portray_failed_([]) --> [].
|
||||||
|
portray_failed_([F|Fs]) -->
|
||||||
|
"\"", F, "\"", "\n", portray_failed_(Fs).
|
||||||
|
|
||||||
|
portray_failed([]) --> [].
|
||||||
|
portray_failed([F|Fs]) -->
|
||||||
|
"\n", "Failed tests:", "\n", portray_failed_([F|Fs]).
|
||||||
|
|
||||||
|
show_failed(Failed) :-
|
||||||
|
phrase(portray_failed(Failed), F),
|
||||||
|
format("~s", [F]).
|
||||||
@@ -84,3 +84,12 @@ fn dif_tests() {
|
|||||||
"All tests passed",
|
"All tests passed",
|
||||||
);
|
);
|
||||||
}
|
}
|
||||||
|
|
||||||
|
#[test]
|
||||||
|
fn ground_tests() {
|
||||||
|
run_top_level_test_with_args(
|
||||||
|
&["src/tests/ground.pl", "-f", "-g", "main_quiet"],
|
||||||
|
"",
|
||||||
|
"All tests passed",
|
||||||
|
);
|
||||||
|
}
|
||||||
|
|||||||
Reference in New Issue
Block a user